From 149c37655fea04084094084b8ca9295ddf4e92d5 Mon Sep 17 00:00:00 2001 From: Jatin Arora Date: Thu, 7 Nov 2024 09:53:42 -0500 Subject: [PATCH 1/5] implement inlining for call attributed --- Source/Core/Inline.cs | 114 +++++++++++++++++++++++++++++++----------- 1 file changed, 85 insertions(+), 29 deletions(-) diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 60e2c7a33..7a7dc95e0 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -16,8 +16,57 @@ public class Inliner : Duplicator protected Program program; - protected Dictionary /*!*/ /* Procedure.Name -> int */ - recursiveProcUnrollMap; + protected class UnrollDepthTracker + { + protected Dictionary procUnrollDepth = new (); + protected Dictionary procUnrollSrc = new (); + + private string getName (Implementation impl) { + string procName = impl.Name; + Contract.Assert(procName != null); + return procName; + } + + public int getDepth(Implementation impl) { + var procName = getName(impl); + var c = -1; + if (procUnrollDepth.TryGetValue(procName, out c)) { + return c; + } + return -1; + } + + public void setDepth (CallCmd cmd, Implementation impl, int depth) { + var procName = getName(impl); + procUnrollSrc[procName] = cmd; + procUnrollDepth[procName] = depth; + } + + public void increment(Implementation impl) { + var procName = getName(impl); + Debug.Assert (procUnrollSrc.ContainsKey(procName)); + Debug.Assert (procUnrollDepth.ContainsKey(procName)); + procUnrollDepth[procName] = procUnrollDepth[procName] + 1; + } + + public void decrement(Implementation impl) { + var procName = getName(impl); + Debug.Assert (procUnrollSrc.ContainsKey(procName)); + Debug.Assert (procUnrollDepth.ContainsKey(procName)); + procUnrollDepth[procName] = procUnrollDepth[procName] - 1; + } + + public void popCmd(CallCmd cmd, Implementation impl) { + var procName = getName(impl); + if (procUnrollSrc.ContainsKey(procName) && procUnrollSrc[procName] == cmd) { + Debug.Assert (procUnrollDepth.ContainsKey(procName)); + procUnrollSrc.Remove(procName); + procUnrollDepth.Remove(procName); + } + } + } + + protected UnrollDepthTracker depthTracker; protected Dictionary /*!*/ /* Procedure.Name -> int */ inlinedProcLblMap; @@ -28,7 +77,7 @@ protected List /*!*/ newLocalVars; protected string prefix; - + private InlineCallback inlineCallback; private CodeCopier codeCopier; @@ -39,7 +88,7 @@ void ObjectInvariant() Contract.Invariant(program != null); Contract.Invariant(newLocalVars != null); Contract.Invariant(codeCopier != null); - Contract.Invariant(recursiveProcUnrollMap != null); + Contract.Invariant(depthTracker != null); Contract.Invariant(inlinedProcLblMap != null); } @@ -84,7 +133,7 @@ public Inliner(Program program, InlineCallback cb, int inlineDepth, CoreOptions { this.program = program; this.inlinedProcLblMap = new Dictionary(); - this.recursiveProcUnrollMap = new Dictionary(); + this.depthTracker = new UnrollDepthTracker(); this.inlineDepth = inlineDepth; this.options = options; this.codeCopier = new CodeCopier(); @@ -93,7 +142,7 @@ public Inliner(Program program, InlineCallback cb, int inlineDepth, CoreOptions this.prefix = null; } - // This method calculates a prefix (storing it in the prefix field) so that prepending it to any string + // This method calculates a prefix (storing it in the prefix field) so that prepending it to any string // is guaranteed not to create a conflict with the names of variables and blocks in scope inside impl. protected void ComputePrefix(Program program, Implementation impl) { @@ -213,7 +262,7 @@ public void Error(IToken tok, string msg) { //Contract.Requires(msg != null); //Contract.Requires(tok != null); - // FIXME + // FIXME // noop. // This is required because during the resolution, some resolution errors happen // (such as the ones caused addion of loop invariants J_(block.Label) by the AI package @@ -242,31 +291,37 @@ protected void ResolveImpl(Implementation impl) // override this and implement their own inlining policy protected virtual int GetInlineCount(CallCmd callCmd, Implementation impl) { - return GetInlineCount(impl); + return TryDefineCount(callCmd, impl); } - // returns true if it is ok to further unroll the procedure - // otherwise, the procedure is not inlined at the call site - protected int GetInlineCount(Implementation impl) + protected int TryDefineCount(CallCmd callCmd, Implementation impl) { Contract.Requires(impl != null); Contract.Requires(impl.Proc != null); - string /*!*/ - procName = impl.Name; - Contract.Assert(procName != null); - if (recursiveProcUnrollMap.TryGetValue(procName, out var c)) + // getDepth returns -1 when depth for this impl is not defined + var depth = depthTracker.getDepth(impl); + if (depth >= 0) { - return c; + return depth; } - c = -1; // TryGetValue above always overwrites c - impl.CheckIntAttribute("inline", ref c); - // procedure attribute overrides implementation - impl.Proc.CheckIntAttribute("inline", ref c); + int countCall (CallCmd cmd) { + return QKeyValue.FindIntAttribute(cmd.Attributes, "inline", -1); + } - recursiveProcUnrollMap[procName] = c; - return c; + // first check the inline depth on the call command. + depth = countCall(callCmd); + if (depth < 0) { + // if call cmd doesn't define the depth, then check the procedure. + impl.CheckIntAttribute("inline", ref depth); + impl.Proc.CheckIntAttribute("inline", ref depth); + } + if (depth >= 0) { + Console.WriteLine("assinging " + impl.Proc.Name + " depth = " + depth); + depthTracker.setDepth (callCmd, impl, depth); + } + return depth; } void CheckRecursion(Implementation impl, Stack /*!*/ callStack) @@ -325,7 +380,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis } else { - recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1; + depthTracker.decrement(impl); } bool inlinedSomething = true; @@ -337,7 +392,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis } else { - recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1; + depthTracker.increment(impl); } Block /*!*/ @@ -354,7 +409,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis return nextlblCount; } - public virtual List /*!*/ DoInlineBlocks(IList /*!*/ blocks, ref bool inlinedSomething) + public virtual List /*!*/ DoInlineBlocks(IList /*!*/ blocks, ref bool inlinedSomething) { Contract.Requires(cce.NonNullElements(blocks)); Contract.Ensures(cce.NonNullElements(Contract.Result>())); @@ -412,6 +467,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis { newCmds.Add(codeCopier.CopyCmd(callCmd)); } + depthTracker.popCmd(callCmd, impl); } else if (cmd is PredicateCmd) { @@ -801,22 +857,22 @@ public Expr Subst(Variable v) { return substMap[v]; } - + public Expr OldSubst(Variable v) { return oldSubstMap[v]; } - + public Expr PartialSubst(Variable v) { return substMap.ContainsKey(v) ? substMap[v] : null; } - + public Expr PartialOldSubst(Variable v) { return oldSubstMap.ContainsKey(v) ? oldSubstMap[v] : null; } - + public List CopyCmdSeq(List cmds) { Contract.Requires(cmds != null); From 86dd6545014dc815c5ca2ccc086236537f03cdec Mon Sep 17 00:00:00 2001 From: Jatin Arora Date: Thu, 7 Nov 2024 09:58:25 -0500 Subject: [PATCH 2/5] fix space --- Source/Core/Inline.cs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 7a7dc95e0..fb3c1cf99 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -18,8 +18,8 @@ public class Inliner : Duplicator protected class UnrollDepthTracker { - protected Dictionary procUnrollDepth = new (); - protected Dictionary procUnrollSrc = new (); + protected Dictionary procUnrollDepth = new(); + protected Dictionary procUnrollSrc = new(); private string getName (Implementation impl) { string procName = impl.Name; @@ -222,7 +222,7 @@ protected void ProcessImplementation(Program program, Implementation impl) // we need to resolve the new code ResolveImpl(impl); - + Console.WriteLine("printing here for " + impl.Name + " num blocks after inlining = " + impl.Blocks.Count()); if (options.PrintInlined) { EmitImpl(impl); @@ -281,7 +281,7 @@ protected void ResolveImpl(Implementation impl) impl.Proc = null; // to force Resolve() redo the operation impl.Resolve(rc); Debug.Assert(rc.ErrorCount == 0); - + TypecheckingContext tc = new TypecheckingContext(new DummyErrorSink(), options); impl.Typecheck(tc); Debug.Assert(tc.ErrorCount == 0); @@ -512,6 +512,8 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis { newCmds.Add(codeCopier.CopyCmd(cmd)); } + + } Block newBlock = new Block(block.tok, lblCount == 0 ? block.Label : block.Label + "$" + lblCount, From e453d8d05d2bf71dec9b450bc56e1cefd726ce1d Mon Sep 17 00:00:00 2001 From: Jatin Arora Date: Thu, 7 Nov 2024 10:30:02 -0500 Subject: [PATCH 3/5] fix space --- Source/Core/Inline.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index fb3c1cf99..f8caff3e0 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -18,8 +18,8 @@ public class Inliner : Duplicator protected class UnrollDepthTracker { - protected Dictionary procUnrollDepth = new(); - protected Dictionary procUnrollSrc = new(); + protected Dictionary procUnrollDepth = new(); + protected Dictionary procUnrollSrc = new(); private string getName (Implementation impl) { string procName = impl.Name; From a525278b96331407b984c4b25521cde56800eb62 Mon Sep 17 00:00:00 2001 From: Jatin Arora Date: Thu, 7 Nov 2024 10:38:32 -0500 Subject: [PATCH 4/5] rem print --- Source/Core/Inline.cs | 2 -- 1 file changed, 2 deletions(-) diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index f8caff3e0..626e88ec2 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -222,7 +222,6 @@ protected void ProcessImplementation(Program program, Implementation impl) // we need to resolve the new code ResolveImpl(impl); - Console.WriteLine("printing here for " + impl.Name + " num blocks after inlining = " + impl.Blocks.Count()); if (options.PrintInlined) { EmitImpl(impl); @@ -318,7 +317,6 @@ int countCall (CallCmd cmd) { impl.Proc.CheckIntAttribute("inline", ref depth); } if (depth >= 0) { - Console.WriteLine("assinging " + impl.Proc.Name + " depth = " + depth); depthTracker.setDepth (callCmd, impl, depth); } return depth; From bc881cf6907f2ed4fc807f4f9eb56a1824762103 Mon Sep 17 00:00:00 2001 From: Jatin Arora Date: Fri, 8 Nov 2024 16:33:51 -0500 Subject: [PATCH 5/5] tweaks --- Source/Core/Inline.cs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 626e88ec2..f95e5df2a 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -29,8 +29,7 @@ private string getName (Implementation impl) { public int getDepth(Implementation impl) { var procName = getName(impl); - var c = -1; - if (procUnrollDepth.TryGetValue(procName, out c)) { + if (procUnrollDepth.TryGetValue(procName, out var c)) { return c; } return -1; @@ -305,12 +304,12 @@ protected int TryDefineCount(CallCmd callCmd, Implementation impl) return depth; } - int countCall (CallCmd cmd) { + int callInlineDepth (CallCmd cmd) { return QKeyValue.FindIntAttribute(cmd.Attributes, "inline", -1); } // first check the inline depth on the call command. - depth = countCall(callCmd); + depth = callInlineDepth(callCmd); if (depth < 0) { // if call cmd doesn't define the depth, then check the procedure. impl.CheckIntAttribute("inline", ref depth);