From b690ac5f4c856ce682d5248aaa7a0d51acf5795c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 19:02:44 -0800 Subject: [PATCH] update --- Source/Concurrency/LinearRewriter.cs | 108 ++++++++++---------- Source/Core/CivlAttributes.cs | 2 +- Source/Core/base.bpl | 4 +- Test/civl/regression-tests/linear_types.bpl | 4 +- 4 files changed, 57 insertions(+), 61 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index cb1ad0bf7..d1bcb4ae3 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -73,14 +73,14 @@ public List 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 RewriteLheapEmpty(CallCmd callCmd) return cmdSeq; } + private List 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(); + 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 RewriteLheapFree(CallCmd callCmd) + { + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + out Function lsetConstructor, out Function lvalConstructor); + + var cmdSeq = new List(); + 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 RewriteLheapGet(CallCmd callCmd) { GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, @@ -267,58 +315,6 @@ private List RewriteLheapPut(CallCmd callCmd) return cmdSeq; } - private List 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(); - 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 RewriteLheapRemove(CallCmd callCmd) - { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, - out Function lsetConstructor, out Function lvalConstructor); - - var cmdSeq = new List(); - 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 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 index 767fec50c..9c10d93e7 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -183,7 +183,7 @@ public static class CivlPrimitives public static HashSet 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 index 6505d973e..9de61a5d3 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -270,10 +270,10 @@ function {:inline} Lheap_Deref(l: Lheap V, k: Ref V): V { l->val[k] } pure procedure Lheap_Empty() returns (l: Lheap V); +pure procedure Lheap_Alloc(path: Lheap V, v: V) returns (l: Lval (Ref V)); +pure procedure Lheap_Free(path: Lheap V, k: Ref V); pure procedure Lheap_Get(path: Lheap V, k: [Ref V]bool) returns (l: Lheap V); pure procedure Lheap_Put(path: Lheap V, {:linear_in} l: Lheap V); -pure procedure Lheap_Alloc(path: Lheap V, v: V) returns (l: Lval (Ref V)); -pure procedure Lheap_Remove(path: Lheap V, k: Ref V) returns (v: V); /// linear maps datatype Lmap { 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 index e82c1dc3f..bc7552cc4 100644 --- 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) {