Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

implement inlining for call attributes #980

Merged
merged 5 commits into from
Nov 8, 2024
Merged

implement inlining for call attributes #980

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
149c376
implement inlining for call attributed
typerSniper Nov 7, 2024
86dd654
fix space
typerSniper Nov 7, 2024
e453d8d
fix space
typerSniper Nov 7, 2024
a525278
rem print
typerSniper Nov 7, 2024
bc881cf
tweaks
typerSniper Nov 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
117 changes: 86 additions & 31 deletions Source/Core/Inline.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,56 @@ public class Inliner : Duplicator

protected Program program;

protected Dictionary<string /*!*/, int> /*!*/ /* Procedure.Name -> int */
recursiveProcUnrollMap;
protected class UnrollDepthTracker
{
protected Dictionary<string, int> procUnrollDepth = new();
protected Dictionary<string, CallCmd> procUnrollSrc = new();

private string getName (Implementation impl) {
Copy link
Collaborator

@keyboardDrummer keyboardDrummer Nov 8, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove the redundant space and use PascalCase for method names, as is the C# convention. If you use a C# IDE then it'll alert you to the incorrect name. We should add a stylistic checker to the Boogie CI

string procName = impl.Name;
Contract.Assert(procName != null);
return procName;
}

public int getDepth(Implementation impl) {
var procName = getName(impl);
if (procUnrollDepth.TryGetValue(procName, out var 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<string /*!*/, int> /*!*/ /* Procedure.Name -> int */
inlinedProcLblMap;
Expand All @@ -28,7 +76,7 @@ protected List<Variable> /*!*/
newLocalVars;

protected string prefix;

private InlineCallback inlineCallback;

private CodeCopier codeCopier;
Expand All @@ -39,7 +87,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);
}

Expand Down Expand Up @@ -84,7 +132,7 @@ public Inliner(Program program, InlineCallback cb, int inlineDepth, CoreOptions
{
this.program = program;
this.inlinedProcLblMap = new Dictionary<string /*!*/, int>();
this.recursiveProcUnrollMap = new Dictionary<string /*!*/, int>();
this.depthTracker = new UnrollDepthTracker();
this.inlineDepth = inlineDepth;
this.options = options;
this.codeCopier = new CodeCopier();
Expand All @@ -93,7 +141,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)
{
Expand Down Expand Up @@ -173,7 +221,6 @@ protected void ProcessImplementation(Program program, Implementation impl)

// we need to resolve the new code
ResolveImpl(impl);

if (options.PrintInlined)
{
EmitImpl(impl);
Expand Down Expand Up @@ -213,7 +260,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
Expand All @@ -232,7 +279,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);
Expand All @@ -242,31 +289,36 @@ 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 callInlineDepth (CallCmd cmd) {
return QKeyValue.FindIntAttribute(cmd.Attributes, "inline", -1);
}

recursiveProcUnrollMap[procName] = c;
return c;
// first check the inline depth on the call command.
depth = callInlineDepth(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) {
depthTracker.setDepth (callCmd, impl, depth);
}
return depth;
}

void CheckRecursion(Implementation impl, Stack<Procedure /*!*/> /*!*/ callStack)
Expand Down Expand Up @@ -325,7 +377,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;
Expand All @@ -337,7 +389,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis
}
else
{
recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
depthTracker.increment(impl);
}

Block /*!*/
Expand All @@ -354,7 +406,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis
return nextlblCount;
}

public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(IList<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(IList<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
{
Contract.Requires(cce.NonNullElements(blocks));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
Expand Down Expand Up @@ -412,6 +464,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)
{
Expand Down Expand Up @@ -456,6 +509,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,
Expand Down Expand Up @@ -801,22 +856,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<Cmd> CopyCmdSeq(List<Cmd> cmds)
{
Contract.Requires(cmds != null);
Expand Down
Loading