Skip to content

Commit

Permalink
added support for no_collect_keys
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer committed Oct 1, 2024
1 parent 9a819a8 commit dbac5f4
Show file tree
Hide file tree
Showing 5 changed files with 148 additions and 39 deletions.
49 changes: 48 additions & 1 deletion Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,7 +155,6 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
case "Map_MakeEmpty":
case "Map_Pack":
case "Map_Unpack":
case "Map_Assume":
return new List<Cmd>{callCmd};
case "Set_Split":
return RewriteSetSplit(callCmd);
Expand All @@ -177,6 +176,10 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
return RewriteMapGet(callCmd);
case "Map_Put":
return RewriteMapPut(callCmd);
case "Map_GetValue":
return RewriteMapGetValue(callCmd);
case "Map_PutValue":
return RewriteMapPutValue(callCmd);
default:
Contract.Assume(false);
return null;
Expand Down Expand Up @@ -481,6 +484,50 @@ private List<Cmd> RewriteMapPut(CallCmd callCmd)
return cmdSeq;
}

private List<Cmd> RewriteMapGetValue(CallCmd callCmd)
{
var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var v = callCmd.Outs[0];

var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
var domain = instantiation["K"];
var range = instantiation["V"];
var mapContainsFunc = MapContains(domain, range);
var mapRemoveFunc = MapRemove(domain, range);
var mapAtFunc = MapAt(domain, range);
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(mapContainsFunc, path, k), "Map_GetValue failed"));
var oneConstructor = OneConstructor(domain);
cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, ExprHelper.FunctionCall(mapAtFunc, path, k)));
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapRemoveFunc, path, k)));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteMapPutValue(CallCmd callCmd)
{
var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var v = callCmd.Ins[2];

var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
var domain = instantiation["K"];
var range = instantiation["V"];
var mapContainsFunc = MapContains(domain, range);
var mapUpdateFunc = MapUpdate(domain, range);
var attribute = new QKeyValue(Token.NoToken, "linear", new List<object>(), null);
cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, k)), attribute));
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, k, v)));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
{
var rc = new ResolutionContext(null, options);
Expand Down
76 changes: 73 additions & 3 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -462,6 +462,10 @@ public override Cmd VisitAssignCmd(AssignCmd node)
{
Error(rhs, $"linear variable {rhs.Decl.Name} can occur at most once as the source of an assignment");
}
else if (InvalidAssignmentWithKeyCollection(lhs.DeepAssignedVariable, rhs.Decl))
{
Error(rhs, $"Mismatch in key collection between source and target");
}
else
{
rhsVars.Add(rhs.Decl);
Expand All @@ -486,6 +490,10 @@ public override Cmd VisitAssignCmd(AssignCmd node)
{
Error(arg, $"linear variable {ie.Decl.Name} can occur at most once as the source of an assignment");
}
else if (InvalidAssignmentWithKeyCollection(field, ie.Decl))
{
Error(arg, $"Mismatch in key collection between source and target");
}
else
{
rhsVars.Add(ie.Decl);
Expand Down Expand Up @@ -568,6 +576,11 @@ public override Cmd VisitCallCmd(CallCmd node)
Error(node, $"linear variable {actual.Decl.Name} can occur only once as an input parameter");
continue;
}
if (!isPrimitive && InvalidAssignmentWithKeyCollection(formal, actual.Decl))
{
Error(node, $"Mismatch in key collection between source and target");
continue;
}
inVars.Add(actual.Decl);
if (actual.Decl is GlobalVariable && actualKind == LinearKind.LINEAR_IN)
{
Expand All @@ -590,6 +603,11 @@ public override Cmd VisitCallCmd(CallCmd node)
Error(node, $"only linear parameter can be assigned to a linear variable: {formal}");
continue;
}
if (!isPrimitive && InvalidAssignmentWithKeyCollection(actual.Decl, formal))
{
Error(node, $"Mismatch in key collection between source and target");
continue;
}
}

var globalOutVars = node.Outs.Select(ie => ie.Decl).ToHashSet();
Expand All @@ -598,6 +616,8 @@ public override Cmd VisitCallCmd(CallCmd node)
Error(node, $"global variable passed as input to pure call but not received as output: {v}");
});

var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc);

if (isPrimitive)
{
var modifiedArgument = CivlPrimitives.ModifiedArgument(node)?.Decl;
Expand All @@ -612,17 +632,48 @@ public override Cmd VisitCallCmd(CallCmd node)
Error(node, $"primitive assigns to input variable that is also an output variable: {modifiedArgument}");
}
else if (modifiedArgument is GlobalVariable &&
enclosingProc is not YieldProcedureDecl &&
enclosingProc.Modifies.All(v => v.Decl != modifiedArgument))
enclosingProc is not YieldProcedureDecl &&
enclosingProc.Modifies.All(v => v.Decl != modifiedArgument))
{
var str = enclosingProc is ActionDecl ? "action's" : "procedure's";
Error(node,
$"primitive assigns to a global variable that is not in the enclosing {str} modifies clause: {modifiedArgument}");
}

if (originalProc.Name == "Map_Split")
{
if (InvalidAssignmentWithKeyCollection(node.Outs[0].Decl, modifiedArgument))
{
Error(node, $"Mismatch in key collection between source and target");
}
}
else if (originalProc.Name == "Map_Join")
{
if (node.Ins[1] is IdentifierExpr ie)
{
if (InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl))
{
Error(node, $"Mismatch in key collection between source and target");
}
}
}
else if (originalProc.Name == "Map_Get" || originalProc.Name == "Map_Put")
{
if (!AreKeysCollected(modifiedArgument))
{
Error(node, $"Keys must be collected");
}
}
else if (originalProc.Name == "Map_GetValue" || originalProc.Name == "Map_PutValue")
{
if (AreKeysCollected(modifiedArgument))
{
Error(node, $"Keys must not be collected");
}
}
}
}

var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(node.Proc);
if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs")
{
var actionDecl = GetActionDeclFromCreateAsyncs(node);
Expand Down Expand Up @@ -749,6 +800,25 @@ public override Variable VisitVariable(Variable node)
return node;
}

private bool AreKeysCollected(Variable v)
{
var attr = QKeyValue.FindAttribute(v.Attributes, x => x.Key == "linear");
var attrParams = attr == null ? new List<object>() : attr.Params;
foreach (var param in attrParams)
{
if (param is string s && s == "no_collect_keys")
{
return false;
}
}
return true;
}

private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source)
{
return AreKeysCollected(target) && !AreKeysCollected(source);
}

private void CheckLinearStoreAccessInGuards()
{
program.Implementations.ForEach(impl => {
Expand Down
4 changes: 2 additions & 2 deletions Source/Core/CivlAttributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,8 @@ public static class CivlPrimitives
public static HashSet<string> LinearPrimitives = new()
{
"Loc_New", "KeyedLocSet_New",
"Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join", "Map_Get", "Map_Put", "Map_Assume",
"Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Join",
"Map_Get", "Map_Put", "Map_GetValue", "Map_PutValue",
"Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put"
};

Expand Down Expand Up @@ -248,7 +249,6 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
case "Map_MakeEmpty":
case "Map_Pack":
case "Map_Unpack":
case "Map_Assume":
return null;
default:
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
Expand Down
10 changes: 4 additions & 6 deletions Source/Core/base.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,17 +319,15 @@ pure procedure {:inline 1} Map_Pack<K,V>({:linear_in} dom: Set K, val: [K]V) ret
}
pure procedure {:inline 1} Map_Unpack<K,V>({:linear_in} m: Map K V) returns ({:linear} dom: Set K, val: [K]V)
{
dom := m->dom;
val := m->val;
dom := m->dom;
val := m->val;
}
pure procedure Map_Split<K,V>({:linear} path: Map K V, s: Set K) returns ({:linear} m: Map K V);
pure procedure Map_Join<K,V>({:linear} path: Map K V, {:linear_in} m: Map K V);
pure procedure Map_Get<K,V>({:linear} path: Map K V, k: K) returns ({:linear} l: One K, {:linear} v: V);
pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} l: One K, {:linear_in} v: V);
pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst: Map K V)
{
assume Set_IsDisjoint(src->dom, dst->dom);
}
pure procedure Map_GetValue<K,V>({:linear} path: Map K V, k: K) returns ({:linear} v: V);
pure procedure Map_PutValue<K,V>({:linear} path: Map K V, k: K, {:linear_in} v: V);

type Loc;

Expand Down
Loading

0 comments on commit dbac5f4

Please sign in to comment.