Skip to content

Commit

Permalink
Merge branch 'master' into tokenFixJumpsHandler
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Nov 13, 2024
2 parents 95583cd + 92e40bd commit cc36c8d
Show file tree
Hide file tree
Showing 13 changed files with 289 additions and 259 deletions.
9 changes: 2 additions & 7 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,9 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker)
this.civlTypeChecker = civlTypeChecker;
}

public static bool IsPrimitive(DeclWithFormals decl)
{
return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
}

public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl)
{
if (IsPrimitive(impl)) {
if (CivlPrimitives.IsPrimitive(impl)) {
return;
}
var linearRewriter = new LinearRewriter(civlTypeChecker);
Expand All @@ -38,7 +33,7 @@ private List<Cmd> RewriteCmdSeq(List<Cmd> cmdSeq)
{
if (cmd is CallCmd callCmd)
{
if (IsPrimitive(callCmd.Proc))
if (CivlPrimitives.IsPrimitive(callCmd.Proc))
{
newCmdSeq.AddRange(RewriteCallCmd(callCmd));
}
Expand Down
10 changes: 5 additions & 5 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
}
else if (cmd is CallCmd callCmd)
{
var isPrimitive = LinearRewriter.IsPrimitive(callCmd.Proc);
var isPrimitive = CivlPrimitives.IsPrimitive(callCmd.Proc);
if (!isPrimitive)
{
linearGlobalVariables.Except(start).ForEach(g =>
Expand Down Expand Up @@ -338,7 +338,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)

public override Implementation VisitImplementation(Implementation node)
{
if (LinearRewriter.IsPrimitive(node))
if (CivlPrimitives.IsPrimitive(node))
{
return node;
}
Expand Down Expand Up @@ -538,7 +538,7 @@ public override Cmd VisitUnpackCmd(UnpackCmd node)

public override Cmd VisitCallCmd(CallCmd node)
{
var isPrimitive = LinearRewriter.IsPrimitive(node.Proc);
var isPrimitive = CivlPrimitives.IsPrimitive(node.Proc);
var inVars = new HashSet<Variable>();
var globalInVars = new HashSet<Variable>();
for (int i = 0; i < node.Proc.InParams.Count; i++)
Expand Down Expand Up @@ -752,7 +752,7 @@ enclosingProc is not YieldProcedureDecl &&

public override Cmd VisitParCallCmd(ParCallCmd node)
{
if (node.CallCmds.Any(callCmd => LinearRewriter.IsPrimitive(callCmd.Proc)))
if (node.CallCmds.Any(callCmd => CivlPrimitives.IsPrimitive(callCmd.Proc)))
{
Error(node, "linear primitives may not be invoked in a parallel call");
return node;
Expand Down Expand Up @@ -831,7 +831,7 @@ private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source
private void CheckLinearStoreAccessInGuards()
{
program.Implementations.ForEach(impl => {
if (LinearRewriter.IsPrimitive(impl))
if (CivlPrimitives.IsPrimitive(impl))
{
return;
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Concurrency/YieldingProcDuplicator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ private void ProcessCallCmd(CallCmd newCall)
InjectGate(pureAction, newCall);
newCmdSeq.Add(newCall);
}
else if (LinearRewriter.IsPrimitive(newCall.Proc))
else if (CivlPrimitives.IsPrimitive(newCall.Proc))
{
newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall));
}
Expand Down
9 changes: 9 additions & 0 deletions Source/Core/Analysis/ModSetCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -194,6 +194,15 @@ public override Cmd VisitCallCmd(CallCmd callCmd)
}
}

if (CivlPrimitives.IsPrimitive(callCmd.Proc))
{
var modifiedArgument = CivlPrimitives.ModifiedArgument(callCmd)?.Decl;
if (modifiedArgument != null)
{
ProcessVariable(modifiedArgument);
}
}

return ret;
}

Expand Down
8 changes: 5 additions & 3 deletions Source/Core/BoogiePL.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -759,17 +759,19 @@ SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>

SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
=
(. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
(. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
"refines"
{ Attribute<ref kv> }
(
MoverQualifier<ref moverType>
"action" (. tok = t; .)
{ Attribute<ref akv> }
Ident<out unused>
Ident<out m>
ImplBody<out locals, out stmtList>
(.
if (refinedAction == null) {
if (m.val != "_") {
this.SemErr("expected _ for name of anoonymous action");
} else if (refinedAction == null) {
var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
false, new List<ActionDeclRef>(), null, null,
new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
Expand Down
5 changes: 5 additions & 0 deletions Source/Core/CivlAttributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,11 @@ public static class CivlPrimitives
"Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put"
};

public static bool IsPrimitive(DeclWithFormals decl)
{
return LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
}

public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
{
if (expr is IdentifierExpr identifierExpr)
Expand Down
117 changes: 86 additions & 31 deletions Source/Core/Inline.cs
View file
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) {
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
8 changes: 5 additions & 3 deletions Source/Core/Parser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1219,7 +1219,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) {
}

void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs) {
IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList;
IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList;
Expect(41);
while (la.kind == 26) {
Attribute(ref kv);
Expand All @@ -1231,9 +1231,11 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken
while (la.kind == 26) {
Attribute(ref akv);
}
Ident(out unused);
Ident(out m);
ImplBody(out locals, out stmtList);
if (refinedAction == null) {
if (m.val != "_") {
this.SemErr("expected _ for name of anoonymous action");
} else if (refinedAction == null) {
var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
false, new List<ActionDeclRef>(), null, null,
new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);
Expand Down
Loading

0 comments on commit cc36c8d

Please sign in to comment.