From e31dcd6e545c2ba4be4e67107f8f9d8f58c0ef0d Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 14:16:13 -0800 Subject: [PATCH 1/5] first commit --- Source/Concurrency/LinearRewriter.cs | 86 ++++----- Source/Concurrency/LinearTypeChecker.cs | 192 +++++++++++++++++--- Source/Core/CivlAttributes.cs | 6 +- Source/Core/base.bpl | 2 - Test/civl/regression-tests/linear_types.bpl | 9 +- Test/civl/samples/treiber-stack.bpl | 10 +- Test/datatypes/node-client.bpl | 8 +- 7 files changed, 226 insertions(+), 87 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 76b1bd694..17937cc50 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -32,9 +33,29 @@ private List RewriteCmdSeq(List cmdSeq) var newCmdSeq = new List(); foreach (var cmd in cmdSeq) { - if (cmd is CallCmd callCmd && IsPrimitive(callCmd.Proc)) + if (cmd is AssignCmd assignCmd) { - newCmdSeq.AddRange(RewriteCallCmd(callCmd)); + assignCmd.Rhss.Where(LinearStoreVisitor.HasLinearStoreAccess).ForEach(expr => { + CreateAccessAsserts(expr, expr.tok, "Illegal access"); + }); + assignCmd.Lhss.Where(LinearStoreVisitor.HasLinearStoreAccess).ForEach(assignLhs => { + CreateAccessAsserts(assignLhs, assignLhs.tok, "Illegal access"); + }); + newCmdSeq.Add(cmd); + } + else if (cmd is CallCmd callCmd) + { + callCmd.Ins.Where(LinearStoreVisitor.HasLinearStoreAccess).ForEach(expr => { + CreateAccessAsserts(expr, expr.tok, "Illegal access"); + }); + if (IsPrimitive(callCmd.Proc)) + { + newCmdSeq.AddRange(RewriteCallCmd(callCmd)); + } + else + { + newCmdSeq.Add(cmd); + } } else { @@ -56,10 +77,6 @@ public List RewriteCallCmd(CallCmd callCmd) return RewriteLheapGet(callCmd); case "Lheap_Put": return RewriteLheapPut(callCmd); - case "Lheap_Read": - return RewriteLheapRead(callCmd); - case "Lheap_Write": - return RewriteLheapWrite(callCmd); case "Lheap_Alloc": return RewriteLheapAlloc(callCmd); case "Lheap_Remove": @@ -242,42 +259,8 @@ private List RewriteLheapPut(CallCmd callCmd) return cmdSeq; } - private List RewriteLheapRead(CallCmd callCmd) - { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, - out Function lsetConstructor, out Function lvalConstructor); - - var path = callCmd.Ins[0]; - var v = callCmd.Outs[0]; - - var cmdSeq = CreateAccessAsserts(path, callCmd.tok, "Lheap_Read failed"); - cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, path)); - - ResolveAndTypecheck(options, cmdSeq); - return cmdSeq; - } - - private List RewriteLheapWrite(CallCmd callCmd) - { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, - out Function lsetConstructor, out Function lvalConstructor); - - var path = callCmd.Ins[0]; - var v = callCmd.Ins[1]; - - var cmdSeq = CreateAccessAsserts(path, callCmd.tok, "Lheap_Write failed"); - cmdSeq.Add(CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), v)); - - ResolveAndTypecheck(options, cmdSeq); - return cmdSeq; - } - private List CreateAccessAsserts(Expr expr, IToken tok, string msg) { - if (expr is IdentifierExpr identifierExpr) - { - return new List(); - } if (expr is NAryExpr nAryExpr) { if (nAryExpr.Fun is FieldAccess) @@ -294,12 +277,31 @@ lheapValExpr.Args[0].Type is CtorType ctorType && { var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg); var lheapContainsFunc = LheapContains(nAryExpr.Type); - cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), "Lheap_Write failed")); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), msg)); return cmdSeq; } } } - throw new cce.UnreachableException(); + return new List(); + } + + private List CreateAccessAsserts(AssignLhs assignLhs, IToken tok, string msg) + { + if (assignLhs is FieldAssignLhs fieldAssignLhs) + { + return CreateAccessAsserts(fieldAssignLhs.Datatype, tok, msg); + } + if (assignLhs is MapAssignLhs mapAssignLhs && + mapAssignLhs.Map is FieldAssignLhs fieldAssignLhs1 && + fieldAssignLhs1.Datatype.Type is CtorType ctorType && + Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") + { + var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg); + var lheapContainsFunc = LheapContains(mapAssignLhs.Map.Type); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg)); + return cmdSeq; + } + return new List(); } private List RewriteLheapAlloc(CallCmd callCmd) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 32927bb45..569f34cc9 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -1,9 +1,52 @@ -using System; -using System.Collections.Generic; +using System.Collections.Generic; using System.Linq; namespace Microsoft.Boogie { + public class LinearStoreVisitor : ReadOnlyVisitor + { + private bool hasLinearStoreAccess = false; + + public static bool HasLinearStoreAccess(Expr expr) + { + var heapLookupVisitor = new LinearStoreVisitor(); + heapLookupVisitor.Visit(expr); + return heapLookupVisitor.hasLinearStoreAccess; + } + + public static bool HasLinearStoreAccess(AssignLhs assignLhs) + { + var heapLookupVisitor = new LinearStoreVisitor(); + heapLookupVisitor.Visit(assignLhs); + return heapLookupVisitor.hasLinearStoreAccess; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + CheckType(node.Type); + return base.VisitIdentifierExpr(node); + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + CheckType(node.Type); + return base.VisitNAryExpr(node); + } + + private void CheckType(Type type) + { + if (type is not CtorType ctorType) + { + return; + } + var typeCtorDeclName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name; + if (typeCtorDeclName == "Lheap" || typeCtorDeclName == "Lmap") + { + hasLinearStoreAccess = true; + } + } + } + public class LinearTypeChecker : ReadOnlyVisitor { public Program program; @@ -22,6 +65,66 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker) // other fields are initialized in the TypeCheck method } + private static bool IsLegalAssignmentTarget(AssignLhs assignLhs) + { + if (LinearStoreVisitor.HasLinearStoreAccess(assignLhs)) + { + return IsAccessPathAssignLhs(assignLhs); + } + return true; + } + + private static bool IsAccessPathAssignLhs(AssignLhs assignLhs) + { + if (assignLhs is SimpleAssignLhs) + { + return true; + } + if (assignLhs is FieldAssignLhs fieldAssignLhs) + { + return IsAccessPathAssignLhs(fieldAssignLhs.Datatype); + } + if (assignLhs is MapAssignLhs mapAssignLhs) + { + return IsAccessPathAssignLhs(mapAssignLhs.Map) && + mapAssignLhs.Indexes.All(expr => !LinearStoreVisitor.HasLinearStoreAccess(expr)); + } + throw new cce.UnreachableException(); + } + + private static bool IsLegalAssignmentSource(Expr expr) + { + if (LinearStoreVisitor.HasLinearStoreAccess(expr)) + { + if (expr is NAryExpr nAryExpr && nAryExpr.Fun is FunctionCall functionCall && functionCall.Func is DatatypeConstructor) + { + return nAryExpr.Args.All(x => x is IdentifierExpr); + } + return IsAccessPathExpr(expr); + } + return true; + } + + private static bool IsAccessPathExpr(Expr expr) + { + if (expr is IdentifierExpr identifierExpr) + { + return true; + } + if (expr is NAryExpr nAryExpr) + { + if (nAryExpr.Fun is FieldAccess) + { + return IsAccessPathExpr(nAryExpr.Args[0]); + } + if (nAryExpr.Fun is MapSelect) + { + return IsAccessPathExpr(nAryExpr.Args[0]) && nAryExpr.Args.Skip(1).All(expr => !LinearStoreVisitor.HasLinearStoreAccess(expr)); + } + } + return false; + } + #region Visitor Implementation private IEnumerable LinearGlobalVariables => @@ -201,12 +304,18 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) var lhsVarsToAdd = new HashSet(); for (int i = 0; i < assignCmd.Lhss.Count; i++) { - var lhsVar = assignCmd.Lhss[i].DeepAssignedVariable; + var lhs = assignCmd.Lhss[i]; + var lhsVar = lhs.DeepAssignedVariable; if (SkipCheck(lhsVar)) { continue; } var lhsDomainName = LinearDomainCollector.FindDomainName(lhsVar); + if (lhsDomainName == null && !linearTypes.Contains(lhs.Type)) + { + // ordinary assignment + continue; + } var rhsExpr = assignCmd.Rhss[i]; if (rhsExpr is IdentifierExpr ie) { @@ -395,6 +504,15 @@ private bool SkipCheck(Variable v) public override Cmd VisitAssignCmd(AssignCmd node) { + node.Lhss.Where(lhs => !IsLegalAssignmentTarget(lhs)).ForEach(lhs => + { + Error(lhs, "Illegal access to linear store"); + }); + node.Rhss.Where(rhs => !IsLegalAssignmentSource(rhs)).ForEach(rhs => + { + Error(rhs, "Illegal access to linear store"); + }); + HashSet rhsVars = new HashSet(); for (int i = 0; i < node.Lhss.Count; i++) { @@ -404,14 +522,50 @@ public override Cmd VisitAssignCmd(AssignCmd node) { continue; } - if (!(lhs is SimpleAssignLhs)) + var lhsDomainName = LinearDomainCollector.FindDomainName(lhsVar); + var rhsExpr = node.Rhss[i]; + if (lhsDomainName == null) + { + if (!linearTypes.Contains(lhs.Type)) + { + // ordinary assignment + continue; + } + if (rhsExpr is IdentifierExpr) + { + // complete permission transfer + continue; + } + if (rhsExpr is NAryExpr { Fun: FunctionCall { Func: DatatypeConstructor } } nAryExpr) + { + // pack + nAryExpr.Args.Where(arg => linearTypes.Contains(arg.Type)).ForEach(arg => + { + if (arg is not IdentifierExpr ie) + { + Error(node, $"A source of pack of linear type must be a variable"); + } + else if (rhsVars.Contains(ie.Decl)) + { + Error(node, $"Linear variable {ie.Decl.Name} can occur only once in the right-hand-side of an assignment"); + } + else + { + rhsVars.Add(ie.Decl); + } + }); + } + else + { + Error(node, "illegal linear assignment"); + } + } + else if (lhs is not SimpleAssignLhs) { Error(node, $"Only simple assignment allowed on linear variable {lhsVar.Name}"); continue; } - var rhsExpr = node.Rhss[i]; - var lhsDomainName = LinearDomainCollector.FindDomainName(lhsVar); - if (rhsExpr is IdentifierExpr rhs) + else if (rhsExpr is IdentifierExpr rhs) { var rhsKind = LinearDomainCollector.FindLinearKind(rhs.Decl); if (rhsKind == LinearKind.ORDINARY) @@ -427,24 +581,11 @@ public override Cmd VisitAssignCmd(AssignCmd node) if (rhsVars.Contains(rhs.Decl)) { Error(node, $"Linear variable {rhs.Decl.Name} can occur only once in the right-hand-side of an assignment"); - continue; } - rhsVars.Add(rhs.Decl); - } - else if (lhsDomainName == null && rhsExpr is NAryExpr { Fun: FunctionCall { Func: DatatypeConstructor } } nAryExpr) - { - // pack - nAryExpr.Args.Where(arg => linearTypes.Contains(arg.Type)).ForEach(arg => + else { - if (arg is IdentifierExpr ie) - { - rhsVars.Add(ie.Decl); - } - else - { - Error(node, $"A source of pack of linear type must be a variable"); - } - }); + rhsVars.Add(rhs.Decl); + } } } return base.VisitAssignCmd(node); @@ -542,6 +683,11 @@ public int CheckLinearParameters(CallCmd callCmd, HashSet availableLin public override Cmd VisitCallCmd(CallCmd node) { + node.Ins.Where(expr => !IsLegalAssignmentSource(expr)).ForEach(rhs => + { + Error(rhs, "Illegal access to linear store"); + }); + var isPrimitive = IsPrimitive(node.Proc); var inVars = new HashSet(); var globalInVars = new HashSet(); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 3dc7f1ddc..aae9c0ea6 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_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove", + "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Alloc", "Lheap_Remove", "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put", "Lval_Split", "Lval_Get", "Lval_Put" }; @@ -226,10 +226,6 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) return null; case "Lheap_Get": case "Lheap_Put": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); - case "Lheap_Read": - return null; - case "Lheap_Write": case "Lheap_Alloc": case "Lheap_Remove": return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 7e0b69bc6..1b7063a1a 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -272,8 +272,6 @@ function {:inline} Lheap_Deref(l: Lheap V, k: Ref V): V { pure procedure Lheap_Empty() returns (l: Lheap 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_Read(path: V) returns (v: V); -pure procedure Lheap_Write(path: V, v: 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); diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl index 85a2cdf30..e82c1dc3f 100644 --- a/Test/civl/regression-tests/linear_types.bpl +++ b/Test/civl/regression-tests/linear_types.bpl @@ -1,19 +1,12 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -atomic action {:layer 1, 2} A0({:linear_in} path: Lheap int, k: [Ref int]bool) returns (path': Lheap int, l: Lheap int) { +atomic action {:layer 1, 2} A1({:linear_in} path: Lheap int, k: [Ref int]bool) returns (path': Lheap int, l: Lheap int) { call path' := Lheap_Empty(); call Lheap_Put(path', path); call l := Lheap_Get(path', k); } -atomic action {:layer 1, 2} A1({:linear_in} path: Lheap int, k: Ref int, v: int) returns (path': Lheap int, v': int) { - call path' := Lheap_Empty(); - call Lheap_Put(path', path); - call Lheap_Write(path'->val[k], v); - call v' := Lheap_Read(path'->val[k]); -} - atomic action {:layer 1, 2} A2(v: int) returns (path': Lheap int, v': int) { var k: Lval (Ref int); call path' := Lheap_Empty(); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 18116b21b..1ad2c0752 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -88,7 +88,7 @@ modifies ts; assume ts->val[ref_t]->top != Nil(); assume ts->val[ref_t]->stack->dom[ts->val[ref_t]->top]; Node(new_ref_n, x) := ts->val[ref_t]->stack->val[ts->val[ref_t]->top]; - call Lheap_Write(ts->val[ref_t]->top, new_ref_n); + ts->val[ref_t]->top := new_ref_n; } } yield procedure {:layer 3} PopIntermediate(ref_t: RefTreiber X) returns (success: bool, x: X) @@ -114,10 +114,12 @@ modifies ts, unused; { var {:pool "A"} ref_n: Lval (RefNode X); var {:pool "A"} new_ref_n: Lval (RefNode X); + var t: RefNode X; assume {:add_to_pool "A", ref_n} ts->dom[ref_t]; - call new_ref_n := Lheap_Alloc(ts->val[ref_t]->stack, Node(if success then ts->val[ref_t]->top else ref_n->val, x)); + t := ts->val[ref_t]->top; + call new_ref_n := Lheap_Alloc(ts->val[ref_t]->stack, Node(if success then t else ref_n->val, x)); if (success) { - call Lheap_Write(ts->val[ref_t]->top, new_ref_n->val); + ts->val[ref_t]->top := new_ref_n->val; } else { unused[ref_t][new_ref_n->val] := true; } @@ -205,7 +207,7 @@ modifies ts; { assert ts->dom[ref_t]; if (old_ref_n == ts->val[ref_t]->top) { - call Lheap_Write(ts->val[ref_t]->top, new_ref_n); + ts->val[ref_t]->top := new_ref_n; r := true; } else { diff --git a/Test/datatypes/node-client.bpl b/Test/datatypes/node-client.bpl index f4715b7cd..68641e9b5 100644 --- a/Test/datatypes/node-client.bpl +++ b/Test/datatypes/node-client.bpl @@ -28,14 +28,16 @@ modifies ts; assert ts->dom[ref_t]; assume ts->val[ref_t]->top != Nil() && ts->val[ref_t]->stack->dom[ts->val[ref_t]->top]; Node(ref_n, x) := ts->val[ref_t]->stack->val[ts->val[ref_t]->top]; - call Lheap_Write(ts->val[ref_t]->top, ref_n); + ts->val[ref_t]->top := ref_n; } procedure {:inline 1} AtomicPushIntermediate(ref_t: RefTreiber X, x: X) modifies ts; { + var t: RefNode X; var ref_n: Lval (RefNode X); assert ts->dom[ref_t]; - call ref_n := Lheap_Alloc(ts->val[ref_t]->stack, Node(ts->val[ref_t]->top, x)); - call Lheap_Write(ts->val[ref_t]->top, ref_n->val); + t := ts->val[ref_t]->top; + call ref_n := Lheap_Alloc(ts->val[ref_t]->stack, Node(t, x)); + ts->val[ref_t]->top := ref_n->val; } From 04246255dba65a226b6294924631835b844aca50 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 15:47:49 -0800 Subject: [PATCH 2/5] second commit --- Source/Concurrency/LinearTypeChecker.cs | 49 +++++++++++++++++++++++++ Test/civl/samples/treiber-stack.bpl | 4 +- 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 569f34cc9..36b5a74c4 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -811,8 +811,57 @@ public override Variable VisitVariable(Variable node) public IEnumerable LinearDomains => domainNameToLinearDomain.Values.Union(linearTypeToLinearDomain.Values); + private void CheckLinearStoreAccessInGuards() + { + program.Implementations.ForEach(impl => { + Stack stmtLists = new Stack(); + if (impl.StructuredStmts != null) + { + stmtLists.Push(impl.StructuredStmts); + } + while (stmtLists.Count > 0) + { + var stmtList = stmtLists.Pop(); + stmtList.BigBlocks.Where(bigBlock => bigBlock.ec != null).ForEach(bigBlock => { + switch (bigBlock.ec) { + case IfCmd ifCmd: + void ProcessIfCmd(IfCmd ifCmd) + { + if (ifCmd.Guard != null && LinearStoreVisitor.HasLinearStoreAccess(ifCmd.Guard)) + { + checkingContext.Error(ifCmd.tok, "Access to linear store not allowed"); + } + stmtLists.Push(ifCmd.thn); + if (ifCmd.elseIf != null) + { + ProcessIfCmd(ifCmd.elseIf); + } + else if (ifCmd.elseBlock != null) + { + stmtLists.Push(ifCmd.elseBlock); + } + } + ProcessIfCmd(ifCmd); + break; + case WhileCmd whileCmd: + if (whileCmd.Guard != null && LinearStoreVisitor.HasLinearStoreAccess(whileCmd.Guard)) + { + checkingContext.Error(whileCmd.tok, "Access to linear store not allowed"); + } + stmtLists.Push(whileCmd.Body); + break; + default: + break; + } + }); + } + }); + } + public void TypeCheck() { + CheckLinearStoreAccessInGuards(); + (this.domainNameToLinearDomain, this.linearTypeToLinearDomain, this.linearTypes) = LinearDomainCollector.Collect(program, checkingContext); this.availableLinearVars = new Dictionary>(); this.VisitProgram(program); diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 1ad2c0752..248672c45 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -205,8 +205,10 @@ preserves call YieldInv#2(ref_t); atomic action {:layer 1, 3} AtomicWriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool) modifies ts; { + var top: RefNode X; assert ts->dom[ref_t]; - if (old_ref_n == ts->val[ref_t]->top) { + top := ts->val[ref_t]->top; + if (old_ref_n == top) { ts->val[ref_t]->top := new_ref_n; r := true; } From f34413d2968d2adbb9cae2b096ac656cff32532c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 17:15:21 -0800 Subject: [PATCH 3/5] third commit --- Source/Concurrency/LinearDomainCollector.cs | 25 ++- .../LinearPermissionInstrumentation.cs | 4 +- Source/Concurrency/LinearRewriter.cs | 175 +++++++++++++----- Source/Concurrency/LinearTypeChecker.cs | 39 +++- Source/Concurrency/MoverCheck.cs | 2 +- Source/Core/CivlAttributes.cs | 35 +--- Source/Core/base.bpl | 19 ++ 7 files changed, 206 insertions(+), 93 deletions(-) diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs index c54f76a46..c883f57f6 100644 --- a/Source/Concurrency/LinearDomainCollector.cs +++ b/Source/Concurrency/LinearDomainCollector.cs @@ -198,14 +198,23 @@ private Dictionary MakeLinearDomains() } if (!permissionTypeToCollectors[permissionType].ContainsKey(type)) { - var typeParamInstantiationMap = new Dictionary { { "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); + if (originalTypeCtorDecl.Name == "Lmap") + { + var typeParamInstantiationMap = new Dictionary { { "K", actualTypeParams[0] }, { "V", actualTypeParams[1] } }; + var collector = program.monomorphizer.InstantiateFunction("Lmap_Collector", typeParamInstantiationMap); + permissionTypeToCollectors[permissionType].Add(type, collector); + } + else + { + var typeParamInstantiationMap = new Dictionary { { "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); + } } } var permissionTypeToLinearDomain = diff --git a/Source/Concurrency/LinearPermissionInstrumentation.cs b/Source/Concurrency/LinearPermissionInstrumentation.cs index fe388aaec..7ed2b3abd 100644 --- a/Source/Concurrency/LinearPermissionInstrumentation.cs +++ b/Source/Concurrency/LinearPermissionInstrumentation.cs @@ -46,7 +46,7 @@ public List ProcDisjointnessAndWellFormedAssumeCmds(Procedure proc, bool at ? FilterInParams(proc.InParams) : FilterInOutParams(proc.InParams.Union(proc.OutParams)); return DisjointnessExprs(availableVars) - .Union(civlTypeChecker.linearTypeChecker.LheapWellFormedExpressions(availableVars)) + .Union(civlTypeChecker.linearTypeChecker.LstoreWellFormedExpressions(availableVars)) .Select(expr => CmdHelper.AssumeCmd(expr)).ToList(); } @@ -54,7 +54,7 @@ public List DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals) { var availableVars = AvailableLinearLocalVars(absy).Union(addGlobals ? LinearGlobalVars() : new List()); return DisjointnessExprs(availableVars) - .Union(civlTypeChecker.linearTypeChecker.LheapWellFormedExpressions(availableVars)) + .Union(civlTypeChecker.linearTypeChecker.LstoreWellFormedExpressions(availableVars)) .Select(expr => CmdHelper.AssumeCmd(expr)).ToList(); } diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index 17937cc50..c79acc267 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -81,6 +81,12 @@ public List RewriteCallCmd(CallCmd callCmd) return RewriteLheapAlloc(callCmd); case "Lheap_Remove": return RewriteLheapRemove(callCmd); + case "Lmap_Create": + return RewriteLmapCreate(callCmd); + case "Lmap_Get": + return RewriteLmapGet(callCmd); + case "Lmap_Put": + return RewriteLmapPut(callCmd); case "Lset_Empty": return RewriteLsetEmpty(callCmd); case "Lset_Split": @@ -259,51 +265,6 @@ private List RewriteLheapPut(CallCmd callCmd) return cmdSeq; } - private List CreateAccessAsserts(Expr expr, IToken tok, string msg) - { - if (expr is NAryExpr nAryExpr) - { - if (nAryExpr.Fun is FieldAccess) - { - return CreateAccessAsserts(nAryExpr.Args[0], tok, msg); - } - if (nAryExpr.Fun is MapSelect) - { - var mapExpr = nAryExpr.Args[0]; - if (mapExpr is NAryExpr lheapValExpr && - lheapValExpr.Fun is FieldAccess && - lheapValExpr.Args[0].Type is CtorType ctorType && - Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") - { - var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg); - var lheapContainsFunc = LheapContains(nAryExpr.Type); - cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), msg)); - return cmdSeq; - } - } - } - return new List(); - } - - private List CreateAccessAsserts(AssignLhs assignLhs, IToken tok, string msg) - { - if (assignLhs is FieldAssignLhs fieldAssignLhs) - { - return CreateAccessAsserts(fieldAssignLhs.Datatype, tok, msg); - } - if (assignLhs is MapAssignLhs mapAssignLhs && - mapAssignLhs.Map is FieldAssignLhs fieldAssignLhs1 && - fieldAssignLhs1.Datatype.Type is CtorType ctorType && - Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") - { - var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg); - var lheapContainsFunc = LheapContains(mapAssignLhs.Map.Type); - cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg)); - return cmdSeq; - } - return new List(); - } - private List RewriteLheapAlloc(CallCmd callCmd) { GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, @@ -356,6 +317,73 @@ private List RewriteLheapRemove(CallCmd callCmd) return cmdSeq; } + private List RewriteLmapCreate(CallCmd callCmd) + { + GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor); + + var cmdSeq = new List(); + var k = callCmd.Ins[0]; + var val = callCmd.Ins[1]; + var l = callCmd.Outs[0].Decl; + + cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lmapConstructor, k, val))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + + private List RewriteLmapGet(CallCmd callCmd) + { + GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor); + + var cmdSeq = new List(); + var path = callCmd.Ins[0]; + var k = callCmd.Ins[1]; + var l = callCmd.Outs[0].Decl; + + var mapImpFunc = MapImp(keyType); + var mapIteFunc = MapIte(keyType, valType); + var mapConstFunc1 = MapConst(keyType, Type.Bool); + var mapConstFunc2 = MapConst(keyType, valType); + var mapDiffFunc = MapDiff(keyType); + + cmdSeq.Add(AssertCmd(callCmd.tok, + Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc1, Expr.True)), + "Lmap_Get failed")); + + cmdSeq.Add(CmdHelper.AssignCmd(l, + ExprHelper.FunctionCall(lmapConstructor, k, + ExprHelper.FunctionCall(mapIteFunc, k, Val(path), ExprHelper.FunctionCall(mapConstFunc2, Default(valType)))))); + + cmdSeq.Add(CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), + ExprHelper.FunctionCall(lmapConstructor, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k), + ExprHelper.FunctionCall(mapIteFunc, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k), Val(path), + ExprHelper.FunctionCall(mapConstFunc2, Default(valType)))))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + + private List RewriteLmapPut(CallCmd callCmd) + { + GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor); + + var cmdSeq = new List(); + var path = callCmd.Ins[0]; + var l = callCmd.Ins[1]; + + var mapOrFunc = MapOr(keyType); + var mapIteFunc = MapIte(keyType, valType); + cmdSeq.Add(CmdHelper.AssignCmd( + CmdHelper.ExprToAssignLhs(path), + ExprHelper.FunctionCall(lmapConstructor, + ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)), + ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(l))))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + private List RewriteLsetEmpty(CallCmd callCmd) { GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, @@ -510,7 +538,7 @@ private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, o { var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); type = instantiation["V"]; - var actualTypeParams = new List() { instantiation["V"] }; + var actualTypeParams = new List() { type }; var refTypeCtorDecl = monomorphizer.InstantiateTypeCtorDecl("Ref", actualTypeParams); refType = new CtorType(Token.NoToken, refTypeCtorDecl, new List()); var lheapTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lheap", actualTypeParams); @@ -521,6 +549,16 @@ private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, o lvalConstructor = lvalTypeCtorDecl.Constructors[0]; } + private void GetRelevantInfo(CallCmd callCmd, out Type keyType, out Type valType, out Function lmapConstructor) + { + var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc); + keyType = instantiation["K"]; + valType = instantiation["V"]; + var actualTypeParams = new List() { keyType, valType }; + var lmapTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lmap", actualTypeParams); + lmapConstructor = lmapTypeCtorDecl.Constructors[0]; + } + private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) { var rc = new ResolutionContext(null, options); @@ -535,4 +573,49 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) absys.ForEach(absy => absy.Typecheck(tc)); tc.CheckModifies = oldCheckModifies; } + + private List CreateAccessAsserts(Expr expr, IToken tok, string msg) + { + if (expr is NAryExpr nAryExpr) + { + if (nAryExpr.Fun is FieldAccess) + { + return CreateAccessAsserts(nAryExpr.Args[0], tok, msg); + } + if (nAryExpr.Fun is MapSelect) + { + var mapExpr = nAryExpr.Args[0]; + if (mapExpr is NAryExpr lheapValExpr && + lheapValExpr.Fun is FieldAccess && + lheapValExpr.Args[0].Type is CtorType ctorType && + Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") + { + var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg); + var lheapContainsFunc = LheapContains(nAryExpr.Type); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), msg)); + return cmdSeq; + } + } + } + return new List(); + } + + private List CreateAccessAsserts(AssignLhs assignLhs, IToken tok, string msg) + { + if (assignLhs is FieldAssignLhs fieldAssignLhs) + { + return CreateAccessAsserts(fieldAssignLhs.Datatype, tok, msg); + } + if (assignLhs is MapAssignLhs mapAssignLhs && + mapAssignLhs.Map is FieldAssignLhs fieldAssignLhs1 && + fieldAssignLhs1.Datatype.Type is CtorType ctorType && + Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") + { + var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg); + var lheapContainsFunc = LheapContains(mapAssignLhs.Map.Type); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg)); + return cmdSeq; + } + return new List(); + } } \ No newline at end of file diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 36b5a74c4..4ca44ac76 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -1,4 +1,5 @@ -using System.Collections.Generic; +using System; +using System.Collections.Generic; using System.Linq; namespace Microsoft.Boogie @@ -929,7 +930,21 @@ public Expr DisjointnessExprForPermissions(LinearDomain domain, IEnumerable LheapWellFormedExpressions(IEnumerable availableVars) + private Function LheapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl typeCtorDecl) + { + var typeInstantiation = monomorphizer.GetTypeInstantiation(typeCtorDecl); + var typeParamInstantiationMap = new Dictionary() { { "V", typeInstantiation[0] } }; + return monomorphizer.InstantiateFunction("Lheap_WellFormed", typeParamInstantiationMap); + } + + private Function LmapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl typeCtorDecl) + { + var typeInstantiation = monomorphizer.GetTypeInstantiation(typeCtorDecl); + var typeParamInstantiationMap = new Dictionary() { { "K", typeInstantiation[0] }, { "V", typeInstantiation[1] } }; + return monomorphizer.InstantiateFunction("Lmap_WellFormed", typeParamInstantiationMap); + } + + public IEnumerable LstoreWellFormedExpressions(IEnumerable availableVars) { var monomorphizer = civlTypeChecker.program.monomorphizer; if (monomorphizer == null) @@ -937,12 +952,24 @@ public IEnumerable LheapWellFormedExpressions(IEnumerable availa return Enumerable.Empty(); } return availableVars.Where(v => - v.TypedIdent.Type is CtorType ctorType && Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select( - v => + { + if (v.TypedIdent.Type is not CtorType ctorType) + { + return false; + } + var declName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name; + if (declName is "Lheap" or "Lmap") + { + return true; + } + return false; + }).Select(v => { var ctorType = (CtorType)v.TypedIdent.Type; - var func = monomorphizer.InstantiateFunction("Lheap_WellFormed", - new Dictionary() { { "V", monomorphizer.GetTypeInstantiation(ctorType.Decl)[0] } }); + var declName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name; + var func = declName == "Lheap" + ? LheapWellFormedFunction(monomorphizer, ctorType.Decl) + : LmapWellFormedFunction(monomorphizer, ctorType.Decl); return ExprHelper.FunctionCall(func, Expr.Ident(v)); }); } diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 28c7d724b..3f146bb40 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -88,7 +88,7 @@ private IEnumerable DisjointnessAndWellFormedRequires(IEnumerable new Requires(false, expr)); } diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index aae9c0ea6..a3ac34fde 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -178,12 +178,13 @@ public static bool IsCallMarked(CallCmd callCmd) public static class CivlPrimitives { - public static HashSet LinearTypes = new() { "Lheap", "Lset", "Lval" }; + public static HashSet LinearTypes = new() { "Lheap", "Lmap", "Lset", "Lval" }; public static HashSet LinearPrimitives = new() { "Ref_Alloc", "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Alloc", "Lheap_Remove", + "Lmap_Create", "Lmap_Get", "Lmap_Put", "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put", "Lval_Split", "Lval_Get", "Lval_Put" }; @@ -196,22 +197,10 @@ public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr) } if (expr is NAryExpr nAryExpr) { - if (nAryExpr.Fun is FieldAccess) + if (nAryExpr.Fun is FieldAccess or MapSelect) { return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]); } - if (nAryExpr.Fun is MapSelect) - { - var mapExpr = nAryExpr.Args[0]; - if (mapExpr is NAryExpr lheapValExpr && - lheapValExpr.Fun is FieldAccess && - lheapValExpr.Args[0].Type is CtorType ctorType && - Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap") - { - return ExtractRootFromAccessPathExpr(lheapValExpr.Args[0]); - } - return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]); - } } return null; } @@ -221,26 +210,12 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { case "Ref_Alloc": - return null; case "Lheap_Empty": - return null; - case "Lheap_Get": - case "Lheap_Put": - case "Lheap_Alloc": - case "Lheap_Remove": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); + case "Lmap_Create": case "Lset_Empty": return null; - case "Lset_Split": - case "Lset_Get": - case "Lset_Put": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); - case "Lval_Split": - case "Lval_Get": - case "Lval_Put": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); default: - throw new cce.UnreachableException(); + return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); } } diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 1b7063a1a..f9a6b22b0 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -275,6 +275,25 @@ 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) } + +function {:inline} Lmap_WellFormed(l: Lmap K V): bool { + l->val == MapIte(l->dom, l->val, MapConst(Default())) +} +function {:inline} Lmap_Collector(l: Lmap K V): [K]bool { + l->dom +} +function {:inline} Lmap_Contains(l: Lmap K V, k: K): bool { + l->dom[k] +} +function {:inline} Lmap_Deref(l: Lmap K V, k: K): V { + l->val[k] +} +pure procedure Lmap_Create({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V); +pure procedure Lmap_Get(path: Lmap K V, k: [K]bool) returns (l: Lmap K V); +pure procedure Lmap_Put(path: Lmap K V, {:linear_in} l: Lmap K V); + /// linear sets datatype Lset { Lset(dom: [V]bool) } From 29d73b22f15c172ce3ccc7e3e98aa50a56cf81dd Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 18:44:09 -0800 Subject: [PATCH 4/5] added Lmap --- Source/Concurrency/LinearRewriter.cs | 26 ++++- .../YieldingProcInstrumentation.cs | 2 +- Source/Core/CivlAttributes.cs | 5 +- Source/Core/base.bpl | 3 +- Test/civl/samples/alloc-mem.bpl | 100 ++++++++---------- Test/civl/samples/alloc-mem.bpl.expect | 2 +- 6 files changed, 76 insertions(+), 62 deletions(-) diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index c79acc267..cb1ad0bf7 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -81,8 +81,10 @@ public List RewriteCallCmd(CallCmd callCmd) return RewriteLheapAlloc(callCmd); case "Lheap_Remove": return RewriteLheapRemove(callCmd); - case "Lmap_Create": - return RewriteLmapCreate(callCmd); + case "Lmap_Alloc": + return RewriteLmapAlloc(callCmd); + case "Lmap_Free": + return RewriteLmapFree(callCmd); case "Lmap_Get": return RewriteLmapGet(callCmd); case "Lmap_Put": @@ -317,7 +319,7 @@ private List RewriteLheapRemove(CallCmd callCmd) return cmdSeq; } - private List RewriteLmapCreate(CallCmd callCmd) + private List RewriteLmapAlloc(CallCmd callCmd) { GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor); @@ -326,7 +328,23 @@ private List RewriteLmapCreate(CallCmd callCmd) var val = callCmd.Ins[1]; var l = callCmd.Outs[0].Decl; - cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lmapConstructor, k, val))); + cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lmapConstructor, Dom(k), val))); + + ResolveAndTypecheck(options, cmdSeq); + return cmdSeq; + } + + private List RewriteLmapFree(CallCmd callCmd) + { + GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor); + var lsetTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lset", new List() { keyType }); + var lsetConstructor = lsetTypeCtorDecl.Constructors[0]; + + var cmdSeq = new List(); + var l = callCmd.Ins[0]; + var k = callCmd.Outs[0].Decl; + + cmdSeq.Add(CmdHelper.AssignCmd(k, ExprHelper.FunctionCall(lsetConstructor, Dom(l)))); ResolveAndTypecheck(options, cmdSeq); return cmdSeq; diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 1165f3243..53d03cdd6 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -198,7 +198,7 @@ private void AddNoninterferenceCheckers() return; } - foreach (var yieldInvariant in civlTypeChecker.program.TopLevelDeclarations.OfType()) + foreach (var yieldInvariant in civlTypeChecker.program.TopLevelDeclarations.OfType().ToList()) { if (layerNum == yieldInvariant.Layer) { diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index a3ac34fde..767fec50c 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -184,7 +184,7 @@ public static class CivlPrimitives { "Ref_Alloc", "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Alloc", "Lheap_Remove", - "Lmap_Create", "Lmap_Get", "Lmap_Put", + "Lmap_Alloc", "Lmap_Free", "Lmap_Get", "Lmap_Put", "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put", "Lval_Split", "Lval_Get", "Lval_Put" }; @@ -211,7 +211,8 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd) { case "Ref_Alloc": case "Lheap_Empty": - case "Lmap_Create": + case "Lmap_Alloc": + case "Lmap_Free": case "Lset_Empty": return null; default: diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index f9a6b22b0..6505d973e 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -290,7 +290,8 @@ function {:inline} Lmap_Contains(l: Lmap K V, k: K): bool { function {:inline} Lmap_Deref(l: Lmap K V, k: K): V { l->val[k] } -pure procedure Lmap_Create({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V); +pure procedure Lmap_Alloc({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V); +pure procedure Lmap_Free({:linear_in} l: Lmap K V) returns (k: Lset K); pure procedure Lmap_Get(path: Lmap K V, k: [K]bool) returns (l: Lmap K V); pure procedure Lmap_Put(path: Lmap K V, {:linear_in} l: Lmap K V); diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl index 67e735f4b..b5c2931e2 100644 --- a/Test/civl/samples/alloc-mem.bpl +++ b/Test/civl/samples/alloc-mem.bpl @@ -1,30 +1,15 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type {:linear "mem"} ref = int; - -type lmap; -function {:linear "mem"} dom(lmap) : [int]bool; -function map(lmap) : [int]int; -function cons([int]bool, [int]int) : lmap; -axiom (forall x:[int]bool, y:[int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y); -axiom (forall x: lmap :: {dom(x)} {map(x)} cons(dom(x), map(x)) == x); - -function Add(x:lmap, i:int): lmap; -axiom (forall x:lmap, i:int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x)); - -function Remove(x:lmap, i:int): lmap; -axiom (forall x:lmap, i:int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); - -function {:inline} PoolInv(unallocated:[int]bool, pool:lmap) : (bool) +function {:inline} PoolInv(unallocated:[int]bool, pool:Lset int) : (bool) { - (forall x:int :: unallocated[x] ==> dom(pool)[x]) + (forall x:int :: unallocated[x] ==> Lset_Contains(pool, x)) } yield procedure {:layer 2} Main () preserves call Yield(); { - var {:layer 1,2} {:linear "mem"} l:lmap; + var {:layer 1,2} l:Lmap int int; var i:int; while (*) invariant {:yields} true; @@ -35,13 +20,13 @@ preserves call Yield(); } } -yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in "mem"} local_in:lmap, i:int) +yield procedure {:layer 2} Thread ({:layer 1,2} {:linear_in} local_in:Lmap int int, i:int) preserves call Yield(); -requires {:layer 1,2} dom(local_in)[i]; +requires {:layer 1,2} Lmap_Contains(local_in, i); { var y, o:int; - var {:layer 1,2} {:linear "mem"} local:lmap; - var {:layer 1,2} {:linear "mem"} l:lmap; + var {:layer 1,2} local:Lmap int int; + var {:layer 1,2} l:Lmap int int; call local := Write(local_in, i, 42); call o := Read(local, i); @@ -58,53 +43,56 @@ requires {:layer 1,2} dom(local_in)[i]; } } -right action {:layer 2} atomic_Alloc() returns ({:linear "mem"} l:lmap, i:int) +right action {:layer 2} atomic_Alloc() returns (l:Lmap int int, i:int) modifies pool; { - assume dom(pool)[i]; + assume Lset_Contains(pool, i); call l, pool := AllocLinear(i, pool); } yield procedure {:layer 1} -Alloc() returns ({:layer 1} {:linear "mem"} l:lmap, i:int) +Alloc() returns ({:layer 1} l:Lmap int int, i:int) refines atomic_Alloc; preserves call Yield(); -ensures {:layer 1} dom(l)[i]; +ensures {:layer 1} Lmap_Contains(l, i); { call i := PickAddr(); call {:layer 1} l, pool := AllocLinear(i, pool); } -left action {:layer 2} atomic_Free({:linear_in "mem"} l:lmap, i:int) +left action {:layer 2} atomic_Free({:linear_in} l:Lmap int int, i:int) modifies pool; { - assert dom(l)[i]; - pool := Add(pool, i); + var t:Lset int; + assert Lmap_Contains(l, i); + call t := Lmap_Free(l); + call Lset_Put(pool, t); } -yield procedure {:layer 1} Free({:layer 1} {:linear_in "mem"} l:lmap, i:int) +yield procedure {:layer 1} Free({:layer 1} {:linear_in} l:Lmap int int, i:int) refines atomic_Free; -requires {:layer 1} dom(l)[i]; +requires {:layer 1} Lmap_Contains(l, i); preserves call Yield(); { call {:layer 1} pool := FreeLinear(l, i, pool); call ReturnAddr(i); } -both action {:layer 2} atomic_Read ({:linear "mem"} l:lmap, i:int) returns (o:int) +both action {:layer 2} atomic_Read (l:Lmap int int, i:int) returns (o:int) { - assert dom(l)[i]; - o := map(l)[i]; + assert Lmap_Contains(l, i); + o := l->val[i]; } -both action {:layer 2} atomic_Write ({:linear_in "mem"} l:lmap, i:int, o:int) returns ({:linear "mem"} l':lmap) +both action {:layer 2} atomic_Write ({:linear_in} l:Lmap int int, i:int, o:int) returns (l':Lmap int int) { - assert dom(l)[i]; - l' := cons(dom(l), map(l)[i := o]); + assert Lmap_Contains(l, i); + l' := l; + l'->val[i] := o; } yield procedure {:layer 1} -Read ({:layer 1} {:linear "mem"} l:lmap, i:int) returns (o:int) +Read ({:layer 1} l:Lmap int int, i:int) returns (o:int) refines atomic_Read; requires call YieldMem(l, i); ensures call Yield(); @@ -113,44 +101,50 @@ ensures call Yield(); } yield procedure {:layer 1} -Write ({:layer 1} {:linear_in "mem"} l:lmap, i:int, o:int) returns ({:layer 1} {:linear "mem"} l':lmap) +Write ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int) refines atomic_Write; requires call Yield(); -requires {:layer 1} dom(l)[i]; +requires {:layer 1} Lmap_Contains(l, i); ensures call YieldMem(l', i); { call WriteLow(i, o); call {:layer 1} l' := WriteLinear(l, i, o); } -pure action AllocLinear (i:int, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} l:lmap, {:linear "mem"} pool':lmap) +pure action AllocLinear (i:int, {:linear_in} pool:Lset int) returns (l:Lmap int int, pool':Lset int) { var m:[int]int; - assert dom(pool)[i]; - pool' := Remove(pool, i); - l := cons(MapConst(false)[i := true], m); + var t:Lset int; + assert Lset_Contains(pool, i); + pool' := pool; + call t := Lset_Get(pool', MapOne(i)); + call l := Lmap_Alloc(t, m); } -pure action FreeLinear ({:linear_in "mem"} l:lmap, i:int, {:linear_in "mem"} pool:lmap) returns ({:linear "mem"} pool':lmap) +pure action FreeLinear ({:linear_in} l:Lmap int int, i:int, {:linear_in} pool:Lset int) returns (pool':Lset int) { - assert dom(l)[i]; - pool' := Add(pool, i); + var t: Lset int; + assert Lmap_Contains(l, i); + call t := Lmap_Free(l); + pool' := pool; + call Lset_Put(pool', t); } -pure action WriteLinear ({:layer 1} {:linear_in "mem"} l:lmap, i:int, o:int) returns ({:layer 1} {:linear "mem"} l':lmap) +pure action WriteLinear ({:layer 1} {:linear_in} l:Lmap int int, i:int, o:int) returns ({:layer 1} l':Lmap int int) { - assert dom(l)[i]; - l' := cons(dom(l), map(l)[i := o]); + assert Lmap_Contains(l, i); + l' := l; + l'->val[i] := o; } yield invariant {:layer 1} Yield (); invariant PoolInv(unallocated, pool); -yield invariant {:layer 1} YieldMem ({:layer 1} {:linear "mem"} l:lmap, i:int); +yield invariant {:layer 1} YieldMem ({:layer 1} l:Lmap int int, i:int); invariant PoolInv(unallocated, pool); -invariant dom(l)[i] && map(l)[i] == mem[i]; +invariant Lmap_Contains(l, i) && Lmap_Deref(l, i) == mem[i]; -var {:layer 1, 2} {:linear "mem"} pool:lmap; +var {:layer 1, 2} pool:Lset int; var {:layer 0, 1} mem:[int]int; var {:layer 0, 1} unallocated:[int]bool; diff --git a/Test/civl/samples/alloc-mem.bpl.expect b/Test/civl/samples/alloc-mem.bpl.expect index 0c0d03d71..0999d9ead 100644 --- a/Test/civl/samples/alloc-mem.bpl.expect +++ b/Test/civl/samples/alloc-mem.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 20 verified, 0 errors +Boogie program verifier finished with 13 verified, 0 errors From b690ac5f4c856ce682d5248aaa7a0d51acf5795c Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 9 Dec 2023 19:02:44 -0800 Subject: [PATCH 5/5] 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) {