Skip to content

Commit

Permalink
[Civl] Add Lmap_Empty (#827)
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer authored Dec 10, 2023
1 parent 5e92b20 commit 132d4cd
Show file tree
Hide file tree
Showing 5 changed files with 77 additions and 52 deletions.
106 changes: 65 additions & 41 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,14 @@ public class LinearRewriter
private CivlTypeChecker civlTypeChecker;

private Monomorphizer monomorphizer => civlTypeChecker.program.monomorphizer;

private ConcurrencyOptions options => civlTypeChecker.Options;

public LinearRewriter(CivlTypeChecker civlTypeChecker)
{
this.civlTypeChecker = civlTypeChecker;
}

public static bool IsPrimitive(DeclWithFormals decl)
{
return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name);
Expand Down Expand Up @@ -81,6 +81,8 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
return RewriteLheapGet(callCmd);
case "Lheap_Put":
return RewriteLheapPut(callCmd);
case "Lmap_Empty":
return RewriteLmapEmpty(callCmd);
case "Lmap_Alloc":
return RewriteLmapAlloc(callCmd);
case "Lmap_Free":
Expand Down Expand Up @@ -114,7 +116,7 @@ private AssertCmd AssertCmd(IToken tok, Expr expr, string msg)
var assertCmd = CmdHelper.AssertCmd(tok, expr, msg);
return assertCmd;
}

private Function MapConst(Type domain, Type range)
{
return monomorphizer.InstantiateFunction("MapConst",
Expand All @@ -128,14 +130,14 @@ private Function MapImp(Type domain)

private Function MapDiff(Type domain)
{
return monomorphizer.InstantiateFunction("MapDiff", new Dictionary<string, Type>() { { "T", domain } });
return monomorphizer.InstantiateFunction("MapDiff", new Dictionary<string, Type>() { { "T", domain } });
}

private Function MapOne(Type domain)
{
return monomorphizer.InstantiateFunction("MapOne", new Dictionary<string, Type>() { { "T", domain } });
return monomorphizer.InstantiateFunction("MapOne", new Dictionary<string, Type>() { { "T", domain } });
}

private Function MapOr(Type domain)
{
return monomorphizer.InstantiateFunction("MapOr", new Dictionary<string, Type>() { { "T", domain } });
Expand All @@ -150,22 +152,22 @@ private Function LheapContains(Type type)
{
return monomorphizer.InstantiateFunction("Lheap_Contains",new Dictionary<string, Type>() { { "V", type } });
}

private Function LheapDeref(Type type)
{
return monomorphizer.InstantiateFunction("Lheap_Deref",new Dictionary<string, Type>() { { "V", type } });
}

private Function LsetContains(Type type)
{
return monomorphizer.InstantiateFunction("Lset_Contains",new Dictionary<string, Type>() { { "V", type } });
}

private static Expr Dom(Expr path)
{
return ExprHelper.FieldAccess(path, "dom");
}

private static Expr Val(Expr path)
{
return ExprHelper.FieldAccess(path, "val");
Expand All @@ -176,7 +178,7 @@ private Expr Default(Type type)
var defaultFunc = monomorphizer.InstantiateFunction("Default", new Dictionary<string, Type>() { { "T", type } });
return ExprHelper.FunctionCall(defaultFunc);
}

private List<Cmd> RewriteRefAlloc(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand All @@ -198,28 +200,28 @@ private List<Cmd> RewriteLheapEmpty(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 l = callCmd.Outs[0].Decl;

var mapConstFunc1 = MapConst(refType, Type.Bool);
var mapConstFunc2 = MapConst(refType, type);

cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lheapConstructor, ExprHelper.FunctionCall(mapConstFunc1, Expr.False),
ExprHelper.FunctionCall(mapConstFunc2, Default(type)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLheapAlloc(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
out Function lsetConstructor, out Function lvalConstructor);
var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
var nilFunc = monomorphizer.InstantiateFunction("Nil", instantiation);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var v = callCmd.Ins[1];
Expand All @@ -234,7 +236,7 @@ private List<Cmd> RewriteLheapAlloc(CallCmd callCmd)
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), Val(l), Expr.True),
Val(path))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}
Expand All @@ -243,11 +245,11 @@ private List<Cmd> RewriteLheapFree(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 lheapContainsFunc = LheapContains(type);
cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lheapContainsFunc, path, k), "Lheap_Free failed"));

Expand All @@ -256,40 +258,40 @@ private List<Cmd> RewriteLheapFree(CallCmd callCmd)
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Dom(path), k, Expr.False),
ExprHelper.FunctionCall(new MapStore(callCmd.tok, 1), Val(path), k, Default(type)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLheapGet(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].Decl;

var mapImpFunc = MapImp(refType);
var mapIteFunc = MapIte(refType, type);
var mapConstFunc1 = MapConst(refType, Type.Bool);
var mapConstFunc2 = MapConst(refType, type);
var mapDiffFunc = MapDiff(refType);

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

cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lheapConstructor, k,
ExprHelper.FunctionCall(mapIteFunc, k, Val(path), ExprHelper.FunctionCall(mapConstFunc2, Default(type))))));

cmdSeq.Add(CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lheapConstructor, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k),
ExprHelper.FunctionCall(mapIteFunc, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k), Val(path),
ExprHelper.FunctionCall(mapConstFunc2, Default(type))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}
Expand All @@ -310,7 +312,25 @@ private List<Cmd> RewriteLheapPut(CallCmd callCmd)
ExprHelper.FunctionCall(lheapConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(l)))));


ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLmapEmpty(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor);

var cmdSeq = new List<Cmd>();
var l = callCmd.Outs[0].Decl;

var mapConstFunc1 = MapConst(keyType, Type.Bool);
var mapConstFunc2 = MapConst(keyType, valType);

cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lmapConstructor, ExprHelper.FunctionCall(mapConstFunc1, Expr.False),
ExprHelper.FunctionCall(mapConstFunc2, Default(valType)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}
Expand All @@ -324,7 +344,11 @@ private List<Cmd> RewriteLmapAlloc(CallCmd callCmd)
var val = callCmd.Ins[1];
var l = callCmd.Outs[0].Decl;

cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lmapConstructor, Dom(k), val)));
var mapIteFunc = MapIte(keyType, valType);
var mapConstFunc = MapConst(keyType, valType);
cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lmapConstructor, Dom(k),
ExprHelper.FunctionCall(mapIteFunc, Dom(k), val, ExprHelper.FunctionCall(mapConstFunc, Default(valType))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
Expand Down Expand Up @@ -402,17 +426,17 @@ private List<Cmd> RewriteLsetEmpty(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 l = callCmd.Outs[0].Decl;

var mapConstFunc = MapConst(type, Type.Bool);
cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lsetConstructor,ExprHelper.FunctionCall(mapConstFunc, Expr.False))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLsetSplit(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand Down Expand Up @@ -475,11 +499,11 @@ private List<Cmd> RewriteLsetPut(CallCmd callCmd)
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lsetConstructor, ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLvalSplit(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand All @@ -497,11 +521,11 @@ private List<Cmd> RewriteLvalSplit(CallCmd callCmd)
cmdSeq.Add(
CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(path, "dom"),
ExprHelper.FunctionCall(mapDiffFunc, Dom(path), ExprHelper.FunctionCall(mapOneFunc, Val(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLvalGet(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand Down Expand Up @@ -535,14 +559,14 @@ private List<Cmd> RewriteLvalPut(CallCmd callCmd)
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(l))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}
Expand All @@ -562,7 +586,7 @@ private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, o
var lvalTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lval", actualTypeParams);
lvalConstructor = lvalTypeCtorDecl.Constructors[0];
}

private void GetRelevantInfo(CallCmd callCmd, out Type keyType, out Type valType, out Function lmapConstructor)
{
var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
Expand Down Expand Up @@ -632,4 +656,4 @@ fieldAssignLhs1.Datatype.Type is CtorType ctorType &&
}
return new List<Cmd>();
}
}
}
3 changes: 1 addition & 2 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
using System;
using System.Collections.Generic;
using System.Collections.Generic;
using System.Linq;

namespace Microsoft.Boogie
Expand Down
15 changes: 8 additions & 7 deletions Source/Core/CivlAttributes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ public static LayerRange Union(LayerRange first, LayerRange second)
{
return new LayerRange(Math.Min(first.LowerLayer, second.LowerLayer), Math.Max(first.UpperLayer, second.UpperLayer));
}

public static LayerRange Union(List<LayerRange> layerRanges)
{
Debug.Assert(layerRanges.Any());
Expand All @@ -55,7 +55,7 @@ public static LayerRange Union(List<LayerRange> layerRanges)
}
return unionLayerRange;
}

public override string ToString()
{
return $"[{LowerLayer}, {UpperLayer}]";
Expand Down Expand Up @@ -169,7 +169,7 @@ public static void RemoveLinearAttributes(ICarriesAttributes obj)
{
RemoveAttributes(obj, LINEAR_ATTRIBUTES);
}

public static bool IsCallMarked(CallCmd callCmd)
{
return callCmd.HasAttribute(MARK);
Expand All @@ -184,7 +184,7 @@ public static class CivlPrimitives
{
"Ref_Alloc",
"Lheap_Empty", "Lheap_Alloc", "Lheap_Free", "Lheap_Get", "Lheap_Put",
"Lmap_Alloc", "Lmap_Free", "Lmap_Get", "Lmap_Put",
"Lmap_Empty", "Lmap_Alloc", "Lmap_Free", "Lmap_Get", "Lmap_Put",
"Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put",
"Lval_Split", "Lval_Get", "Lval_Put"
};
Expand All @@ -204,13 +204,14 @@ public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr)
}
return null;
}

public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
{
switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
{
case "Ref_Alloc":
case "Lheap_Empty":
case "Lmap_Empty":
case "Lmap_Alloc":
case "Lmap_Free":
case "Lset_Empty":
Expand All @@ -219,10 +220,10 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
return ExtractRootFromAccessPathExpr(callCmd.Ins[0]);
}
}

public static HashSet<string> Async = new()
{
"create_async", "create_asyncs", "create_multi_asyncs", "set_choice"
};
}
}
}
1 change: 1 addition & 0 deletions Source/Core/base.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -290,6 +290,7 @@ function {:inline} Lmap_Contains<K,V>(l: Lmap K V, k: K): bool {
function {:inline} Lmap_Deref<K,V>(l: Lmap K V, k: K): V {
l->val[k]
}
pure procedure Lmap_Empty<K,V>() returns (l: Lmap K V);
pure procedure Lmap_Alloc<K,V>({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V);
pure procedure Lmap_Free<K,V>({:linear_in} l: Lmap K V) returns (k: Lset K);
pure procedure Lmap_Get<K,V>(path: Lmap K V, k: [K]bool) returns (l: Lmap K V);
Expand Down
Loading

0 comments on commit 132d4cd

Please sign in to comment.