Skip to content

Commit

Permalink
[Civl] Cleaned up linear primitives (#820)
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer authored Dec 5, 2023
1 parent 14194ca commit 0e4cea1
Show file tree
Hide file tree
Showing 17 changed files with 192 additions and 109 deletions.
18 changes: 8 additions & 10 deletions Source/Concurrency/LinearDomainCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ private bool ContainsPermissionType(Type type)
{
var originalDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
var originalDeclName = originalDecl.Name;
if (originalDeclName == "Lheap" || originalDeclName == "Lset" || originalDeclName == "Lval")
if (CivlPrimitives.LinearTypes.Contains(originalDeclName))
{
permissionTypes.Add(type);
linearTypes.Add(type);
Expand Down Expand Up @@ -198,15 +198,13 @@ private Dictionary<Type, LinearDomain> MakeLinearDomains()
}
if (!permissionTypeToCollectors[permissionType].ContainsKey(type))
{
var collector =
originalTypeCtorDecl.Name == "Lheap"
? program.monomorphizer.InstantiateFunction("Lheap_Collector",
new Dictionary<string, Type> { { "V", actualTypeParams[0] } }) :
originalTypeCtorDecl.Name == "Lset"
? program.monomorphizer.InstantiateFunction("Lset_Collector",
new Dictionary<string, Type> { { "V", actualTypeParams[0] } }) :
program.monomorphizer.InstantiateFunction("Lval_Collector",
new Dictionary<string, Type> { { "V", actualTypeParams[0] } });
var typeParamInstantiationMap = new Dictionary<string, Type> { { "V", actualTypeParams[0] } };
var collector =
originalTypeCtorDecl.Name == "Lheap"
? program.monomorphizer.InstantiateFunction("Lheap_Collector", typeParamInstantiationMap) :
originalTypeCtorDecl.Name == "Lset"
? program.monomorphizer.InstantiateFunction("Lset_Collector", typeParamInstantiationMap) :
program.monomorphizer.InstantiateFunction("Lval_Collector", typeParamInstantiationMap);
permissionTypeToCollectors[permissionType].Add(type, collector);
}
}
Expand Down
123 changes: 89 additions & 34 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker)

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

public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl)
Expand Down Expand Up @@ -52,10 +52,10 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
return RewriteRefAlloc(callCmd);
case "Lheap_Empty":
return RewriteLheapEmpty(callCmd);
case "Lheap_Split":
return RewriteLheapSplit(callCmd);
case "Lheap_Transfer":
return RewriteLheapTransfer(callCmd);
case "Lheap_Get":
return RewriteLheapGet(callCmd);
case "Lheap_Put":
return RewriteLheapPut(callCmd);
case "Lheap_Read":
return RewriteLheapRead(callCmd);
case "Lheap_Write":
Expand All @@ -68,12 +68,16 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
return RewriteLsetEmpty(callCmd);
case "Lset_Split":
return RewriteLsetSplit(callCmd);
case "Lset_Transfer":
return RewriteLsetTransfer(callCmd);
case "Lset_Get":
return RewriteLsetGet(callCmd);
case "Lset_Put":
return RewriteLsetPut(callCmd);
case "Lval_Split":
return RewriteLvalSplit(callCmd);
case "Lval_Transfer":
return RewriteLvalTransfer(callCmd);
case "Lval_Get":
return RewriteLvalGet(callCmd);
case "Lval_Put":
return RewriteLvalPut(callCmd);
default:
Contract.Assume(false);
return null;
Expand Down Expand Up @@ -184,7 +188,7 @@ private List<Cmd> RewriteLheapEmpty(CallCmd callCmd)
return cmdSeq;
}

private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
private List<Cmd> RewriteLheapGet(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);
Expand All @@ -202,7 +206,7 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)

cmdSeq.Add(AssertCmd(callCmd.tok,
Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc1, Expr.True)),
"Lheap_Split failed"));
"Lheap_Get failed"));

cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lheapConstructor, k,
Expand All @@ -217,22 +221,22 @@ private List<Cmd> RewriteLheapSplit(CallCmd callCmd)
return cmdSeq;
}

private List<Cmd> RewriteLheapTransfer(CallCmd callCmd)
private List<Cmd> RewriteLheapPut(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var path1 = callCmd.Ins[1];
var l = callCmd.Ins[1];

var mapOrFunc = MapOr(refType);
var mapIteFunc = MapIte(refType, type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(path1)))));
ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand Down Expand Up @@ -308,16 +312,16 @@ private List<Cmd> RewriteLheapAlloc(CallCmd callCmd)
var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var v = callCmd.Ins[1];
var k = callCmd.Outs[0];
var l = callCmd.Outs[0];

cmdSeq.Add(CmdHelper.HavocCmd(k));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Neq(Val(k), ExprHelper.FunctionCall(nilFunc))));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Not(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Dom(path), Val(k)))));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Eq(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Val(path), Val(k)), v)));
cmdSeq.Add(CmdHelper.HavocCmd(l));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Neq(Val(l), ExprHelper.FunctionCall(nilFunc))));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Not(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Dom(path), Val(l)))));
cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Eq(ExprHelper.FunctionCall(new MapSelect(callCmd.tok, 1), Val(path), Val(l)), v)));
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), Val(k), Expr.True),
ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), Val(l), Expr.True),
Val(path))));

ResolveAndTypecheck(options, cmdSeq);
Expand Down Expand Up @@ -369,38 +373,64 @@ private List<Cmd> RewriteLsetSplit(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Ins[1];

var mapConstFunc = MapConst(type, Type.Bool);
var mapImpFunc = MapImp(type);
cmdSeq.Add(AssertCmd(callCmd.tok,
Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, Dom(k), Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, Dom(l), Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
"Lset_Split failed"));

var mapDiffFunc = MapDiff(type);
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), Dom(k))));

CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), Dom(l))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLsetGet(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Outs[0];

var mapConstFunc = MapConst(type, Type.Bool);
var mapImpFunc = MapImp(type);
cmdSeq.Add(AssertCmd(callCmd.tok,
Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc, Expr.True)),
"Lset_Get failed"));

var mapDiffFunc = MapDiff(type);
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k)));

cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(lsetConstructor, k)));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLsetTransfer(CallCmd callCmd)
private List<Cmd> RewriteLsetPut(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var path1 = callCmd.Ins[1];
var l = callCmd.Ins[1];

var mapOrFunc = MapOr(type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(path1)))));
ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand All @@ -413,36 +443,61 @@ private List<Cmd> RewriteLvalSplit(CallCmd callCmd)

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Ins[1];

var lsetContainsFunc = LsetContains(type);
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(k)), "Lval_Split failed"));
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, Val(l)), "Lval_Split failed"));

var mapOneFunc = MapOne(type);
var mapDiffFunc = MapDiff(type);
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),
ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k)))));
ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLvalTransfer(CallCmd callCmd)
private List<Cmd> RewriteLvalGet(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Outs[0];

var lsetContainsFunc = LsetContains(type);
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lsetContainsFunc, path, k), "Lval_Get failed"));

var mapOneFunc = MapOne(type);
var mapDiffFunc = MapDiff(type);
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),
ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, k))));

cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(lvalConstructor, k)));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLvalPut(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var l = callCmd.Ins[1];

var mapOneFunc = MapOne(type);
var mapOrFunc = MapOr(type);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lsetConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(k))))));
ExprHelper.FunctionCall(mapOrFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(l))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand Down
3 changes: 1 addition & 2 deletions Source/Core/AST/Absy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3273,10 +3273,9 @@ public override void Register(ResolutionContext rc)

public override void Resolve(ResolutionContext rc)
{
rc.Proc = this;
base.Resolve(rc);

var oldStateMode = rc.StateMode;
rc.Proc = this;
rc.StateMode = ResolutionContext.State.Two;
rc.PushVarContext();
RegisterFormals(InParams, rc);
Expand Down
6 changes: 3 additions & 3 deletions Source/Core/AST/AbsyCmd.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3462,7 +3462,7 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
// Check global outputs only; the checking of local outputs is done later
var calleeLayer = Layers[0];
var globalOutputs = Outs.Select(ie => ie.Decl).OfType<GlobalVariable>().Cast<Variable>();
if (CivlPrimitives.Linear.Contains(Proc.Name))
if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
{
var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
if (modifiedArgument is { Decl: GlobalVariable })
Expand Down Expand Up @@ -3494,7 +3494,7 @@ private void TypecheckCallCmdInActionDecl(TypecheckingContext tc)
return;
}

if (CivlPrimitives.Linear.Contains(Proc.Name))
if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
{
// ok
}
Expand Down Expand Up @@ -3603,7 +3603,7 @@ public override void Typecheck(TypecheckingContext tc)
}
}
// primitive calls have inout parameters that must be checked here
if (CivlPrimitives.Linear.Contains(Proc.Name))
if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name))
{
var modifiedArgument = CivlPrimitives.ModifiedArgument(this);
if (modifiedArgument == null)
Expand Down
25 changes: 12 additions & 13 deletions Source/Core/CivlAttributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,12 +178,14 @@ public static bool IsCallMarked(CallCmd callCmd)

public static class CivlPrimitives
{
public static HashSet<string> Linear = new()
public static HashSet<string> LinearTypes = new() { "Lheap", "Lset", "Lval" };

public static HashSet<string> LinearPrimitives = new()
{
"Ref_Alloc",
"Lheap_Empty", "Lheap_Split", "Lheap_Transfer", "Lheap_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove",
"Lset_Empty", "Lset_Split", "Lset_Transfer",
"Lval_Split", "Lval_Transfer"
"Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove",
"Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put",
"Lval_Split", "Lval_Get", "Lval_Put"
};

public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
Expand Down Expand Up @@ -222,27 +224,24 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
return null;
case "Lheap_Empty":
return null;
case "Lheap_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Transfer":
case "Lheap_Get":
case "Lheap_Put":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Read":
return null;
case "Lheap_Write":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Alloc":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lheap_Remove":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lset_Empty":
return null;
case "Lset_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lset_Transfer":
case "Lset_Get":
case "Lset_Put":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lval_Split":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
case "Lval_Transfer":
case "Lval_Get":
case "Lval_Put":
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
default:
throw new cce.UnreachableException();
Expand Down
Loading

0 comments on commit 0e4cea1

Please sign in to comment.