update

boogie-org · Dec 10, 2023 · b690ac5 · b690ac5
1 parent 29d73b2
commit b690ac5
Show file tree

Hide file tree

Showing 4 changed files with 57 additions and 61 deletions.
diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
@@ -73,14 +73,14 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
         return RewriteRefAlloc(callCmd);
       case "Lheap_Empty":
         return RewriteLheapEmpty(callCmd);
+      case "Lheap_Alloc":
+        return RewriteLheapAlloc(callCmd);
+      case "Lheap_Free":
+        return RewriteLheapFree(callCmd);
       case "Lheap_Get":
         return RewriteLheapGet(callCmd);
       case "Lheap_Put":
         return RewriteLheapPut(callCmd);
-      case "Lheap_Alloc":
-        return RewriteLheapAlloc(callCmd);
-      case "Lheap_Remove":
-        return RewriteLheapRemove(callCmd);
       case "Lmap_Alloc":
         return RewriteLmapAlloc(callCmd);
       case "Lmap_Free":
@@ -213,6 +213,54 @@ private List<Cmd> RewriteLheapEmpty(CallCmd callCmd)
     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];
+    var l = callCmd.Outs[0];
+
+    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(l), Expr.True),
+        Val(path))));
+
+    ResolveAndTypecheck(options, cmdSeq);
+    return cmdSeq;
+  }
+
+  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"));
+
+    cmdSeq.Add(
+      CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path),
+      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,
@@ -267,58 +315,6 @@ private List<Cmd> RewriteLheapPut(CallCmd callCmd)
     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];
-    var l = callCmd.Outs[0];
-
-    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(l), Expr.True),
-        Val(path))));
-
-    ResolveAndTypecheck(options, cmdSeq);
-    return cmdSeq;
-  }
-
-  private List<Cmd> RewriteLheapRemove(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 v = callCmd.Outs[0];
-
-    var lheapContainsFunc = LheapContains(type);
-    cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(lheapContainsFunc, path, k), "Lheap_Remove failed"));
-
-    var lheapDerefFunc = LheapDeref(type);
-    cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, ExprHelper.FunctionCall(lheapDerefFunc, path, k)));
-
-    cmdSeq.Add(
-      CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path),
-      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> RewriteLmapAlloc(CallCmd callCmd)
   {
     GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor);

diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
@@ -183,7 +183,7 @@ public static class CivlPrimitives
     public static HashSet<string> LinearPrimitives = new()
     {
       "Ref_Alloc",
-      "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Alloc", "Lheap_Remove",
+      "Lheap_Empty", "Lheap_Alloc", "Lheap_Free", "Lheap_Get", "Lheap_Put",
       "Lmap_Alloc", "Lmap_Free", "Lmap_Get", "Lmap_Put",
       "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put",
       "Lval_Split", "Lval_Get", "Lval_Put"

diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
@@ -270,10 +270,10 @@ function {:inline} Lheap_Deref<V>(l: Lheap V, k: Ref V): V {
     l->val[k]
 }
 pure procedure Lheap_Empty<V>() returns (l: Lheap V);
+pure procedure Lheap_Alloc<V>(path: Lheap V, v: V) returns (l: Lval (Ref V));
+pure procedure Lheap_Free<V>(path: Lheap V, k: Ref V);
 pure procedure Lheap_Get<V>(path: Lheap V, k: [Ref V]bool) returns (l: Lheap V);
 pure procedure Lheap_Put<V>(path: Lheap V, {:linear_in} l: Lheap V);
-pure procedure Lheap_Alloc<V>(path: Lheap V, v: V) returns (l: Lval (Ref V));
-pure procedure Lheap_Remove<V>(path: Lheap V, k: Ref V) returns (v: V);
 
 /// linear maps
 datatype Lmap<K,V> { Lmap(dom: [K]bool, val: [K]V) }

diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
@@ -7,11 +7,11 @@ atomic action {:layer 1, 2} A1({:linear_in} path: Lheap int, k: [Ref int]bool) r
     call l := Lheap_Get(path', k);
 }
 
-atomic action {:layer 1, 2} A2(v: int) returns (path': Lheap int, v': int) {
+atomic action {:layer 1, 2} A2(v: int) returns (path': Lheap int) {
     var k: Lval (Ref int);
     call path' := Lheap_Empty();
     call k := Lheap_Alloc(path', v);
-    call v' := Lheap_Remove(path', k->val);
+    call Lheap_Free(path', k->val);
 }
 
 atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lset int) returns (path': Lset int) {