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) }