diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs index 598613278..c17c80b70 100644 --- a/Source/Concurrency/CivlCoreTypes.cs +++ b/Source/Concurrency/CivlCoreTypes.cs @@ -42,9 +42,9 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List(), null); PendingAsyncs.ForEach(elim => { - var field = new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType); + var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true); ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}", - new List() { field }); + new List() { field }); }); civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl); DesugarSetChoice(civlTypeChecker, ImplWithChoice); diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index a7c883c03..b554a80b6 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -297,6 +297,15 @@ private void TypeCheckYieldingProcedures() private void InlineAtomicActions(HashSet actionDecls) { + var primitiveImpls = program.TopLevelDeclarations.OfType().Where(impl => + { + var originalDecl = impl.Proc.OriginalDeclWithFormals; + return originalDecl != null && CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name); + }); + primitiveImpls.ForEach(impl => { + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; + }); CivlUtil.AddInlineAttribute(SkipActionDecl); actionDecls.ForEach(proc => { @@ -319,6 +328,10 @@ private void InlineAtomicActions(HashSet actionDecls) impl.OriginalBlocks = null; impl.OriginalLocVars = null; }); + primitiveImpls.ForEach(impl => { + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; + }); } private void CreateAtomicActions(HashSet actionDecls) diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs index 68ba9aa91..a5585fd27 100644 --- a/Source/Concurrency/InductiveSequentialization.cs +++ b/Source/Concurrency/InductiveSequentialization.cs @@ -182,7 +182,6 @@ private Cmd Transform(Dictionary eliminatedPendingAsyn public class InductiveSequentialization : Sequentialization { private Action invariantAction; - private HashSet frame; private IdentifierExpr choice; private Dictionary newPAs; @@ -193,7 +192,6 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target // - the modified set of each of each eliminated and abstract action associated with this invariant. // - the target and refined action of every application of inductive sequentialization that refers to this invariant. this.invariantAction = invariantAction; - frame = new HashSet(invariantAction.ModifiedGlobalVars); choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last()); newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType, decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType)); @@ -202,7 +200,7 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target private List GenerateBaseCaseChecker() { var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)).ToList(); - + var subst = targetAction.GetSubstitution(invariantAction); var cmds = targetAction.GetGateAsserts(subst, $"Gate of {targetAction.Name} fails in IS base check against invariant {invariantAction.Name}").ToList(); @@ -215,7 +213,7 @@ private List GenerateBaseCaseChecker() outputVars.AddRange(targetAction.PendingAsyncs.Select(action => invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[action.PendingAsyncType]])); cmds.Add(CmdHelper.CallCmd(targetAction.Impl.Proc, invariantAction.Impl.InParams, outputVars)); - + // Assign empty multiset to the rest var remainderPendingAsyncs = invariantAction.PendingAsyncs.Except(targetAction.PendingAsyncs); if (remainderPendingAsyncs.Any()) @@ -228,6 +226,7 @@ private List GenerateBaseCaseChecker() cmds.Add(CmdHelper.AssignCmd(lhss, rhss)); } + var frame = new HashSet(invariantAction.ModifiedGlobalVars); cmds.Add(GetCheck(targetAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), $"IS base of {targetAction.Name} failed")); @@ -246,6 +245,7 @@ private List GenerateConclusionChecker() cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams, invariantAction.Impl.OutParams)); cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs)); + var frame = new HashSet(refinedAction.ModifiedGlobalVars); cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)), $"IS conclusion of {targetAction.Name} failed")); @@ -300,6 +300,7 @@ private List GenerateStepChecker(Action pendingAsync) cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); } + var frame = new HashSet(invariantAction.ModifiedGlobalVars); cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame), $"IS step of {invariantAction.Name} with {abs.Name} failed")); @@ -315,7 +316,7 @@ private List GenerateStepChecker(Action pendingAsync) * A key concept used in the generation of this extra assumption is the input-output transition relation of an action. * This relation is obtained by taking the conjunction of the gate and transition relation of the action and * existentially quantifying globals in the pre and the post state. - * + * * There are two parts to the assumption, one for leftMover and the other for action. * Both parts are stated in the context of the input-output relation of the invariant action. * - The invocation of leftMover is identical to the choice made by the invariant. @@ -427,7 +428,7 @@ private List GetCheckerTuple(string checkerName, List req inParams, outParams, requires, - frame.Select(Expr.Ident).ToList(), + invariantAction.ModifiedGlobalVars.Select(Expr.Ident).ToList(), new List()); var impl = DeclHelper.Implementation( proc, @@ -457,7 +458,7 @@ private Expr ChoiceTest(CtorType pendingAsyncType) { return ExprHelper.IsConstructor(choice, invariantAction.ChoiceConstructor(pendingAsyncType).Name); } - + private Expr NoPendingAsyncs { get @@ -468,7 +469,7 @@ private Expr NoPendingAsyncs return expr; } } - + private AssignCmd RemoveChoice(CtorType pendingAsyncType) { var rhs = Expr.Sub(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), Expr.Literal(1)); diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs index c54f76a46..35d86ef5c 100644 --- a/Source/Concurrency/LinearDomainCollector.cs +++ b/Source/Concurrency/LinearDomainCollector.cs @@ -176,11 +176,7 @@ private Type GetPermissionType(Type type) var typeCtorDecl = type.AsCtor.Decl; var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl); var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl); - return - originalTypeCtorDecl.Name == "Lheap" - ? new CtorType(Token.NoToken, program.monomorphizer.InstantiateTypeCtorDecl("Ref", actualTypeParams), - new List()) - : actualTypeParams[0]; + return actualTypeParams[0]; } private Dictionary MakeLinearDomains() @@ -198,14 +194,21 @@ 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 == "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 76b1bd694..bd0466412 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; @@ -8,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); @@ -23,6 +24,9 @@ public static bool IsPrimitive(DeclWithFormals decl) public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl) { + if (IsPrimitive(impl)) { + return; + } var linearRewriter = new LinearRewriter(civlTypeChecker); impl.Blocks.ForEach(block => block.Cmds = linearRewriter.RewriteCmdSeq(block.Cmds)); } @@ -32,9 +36,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) + { + 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) { - newCmdSeq.AddRange(RewriteCallCmd(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 { @@ -48,22 +72,14 @@ public List RewriteCallCmd(CallCmd callCmd) { switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name) { - case "Ref_Alloc": - return RewriteRefAlloc(callCmd); - case "Lheap_Empty": - return RewriteLheapEmpty(callCmd); - case "Lheap_Get": - 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": - return RewriteLheapRemove(callCmd); + case "Loc_New": + case "Lmap_Empty": + case "Lmap_Alloc": + case "Lmap_Create": + case "Lmap_Free": + case "Lmap_Move": + case "Lmap_Assume": + return new List{callCmd}; case "Lset_Empty": return RewriteLsetEmpty(callCmd); case "Lset_Split": @@ -89,7 +105,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", @@ -103,14 +119,14 @@ private Function MapImp(Type domain) private Function MapDiff(Type domain) { - return monomorphizer.InstantiateFunction("MapDiff", new Dictionary() { { "T", domain } }); + return monomorphizer.InstantiateFunction("MapDiff", new Dictionary() { { "T", domain } }); } private Function MapOne(Type domain) { - return monomorphizer.InstantiateFunction("MapOne", new Dictionary() { { "T", domain } }); + return monomorphizer.InstantiateFunction("MapOne", new Dictionary() { { "T", domain } }); } - + private Function MapOr(Type domain) { return monomorphizer.InstantiateFunction("MapOr", new Dictionary() { { "T", domain } }); @@ -121,26 +137,21 @@ private Function MapIte(Type domain, Type range) return monomorphizer.InstantiateFunction("MapIte",new Dictionary() { { "T", domain }, { "U", range } }); } - private Function LheapContains(Type type) - { - return monomorphizer.InstantiateFunction("Lheap_Contains",new Dictionary() { { "V", type } }); - } - - private Function LheapDeref(Type type) + private Function MapContains(Type keyType, Type valueType) { - return monomorphizer.InstantiateFunction("Lheap_Deref",new Dictionary() { { "V", type } }); + return monomorphizer.InstantiateFunction("Map_Contains",new Dictionary() { {"T", keyType}, { "U", valueType } }); } - + private Function LsetContains(Type type) { return monomorphizer.InstantiateFunction("Lset_Contains",new Dictionary() { { "V", type } }); } - + private static Expr Dom(Expr path) { return ExprHelper.FieldAccess(path, "dom"); } - + private static Expr Val(Expr path) { return ExprHelper.FieldAccess(path, "val"); @@ -151,227 +162,25 @@ private Expr Default(Type type) var defaultFunc = monomorphizer.InstantiateFunction("Default", new Dictionary() { { "T", type } }); return ExprHelper.FunctionCall(defaultFunc); } - - private List RewriteRefAlloc(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 k = callCmd.Outs[0]; - - cmdSeq.Add(CmdHelper.HavocCmd(k)); - cmdSeq.Add(CmdHelper.AssumeCmd(Expr.Neq(Val(k), ExprHelper.FunctionCall(nilFunc)))); - - ResolveAndTypecheck(options, cmdSeq); - return cmdSeq; - } - - private List RewriteLheapEmpty(CallCmd callCmd) - { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, - out Function lsetConstructor, out Function lvalConstructor); - - var cmdSeq = new List(); - 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 RewriteLheapGet(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 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; - } - - private List RewriteLheapPut(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 l = callCmd.Ins[1]; - - var mapOrFunc = MapOr(refType); - var mapIteFunc = MapIte(refType, type); - cmdSeq.Add(CmdHelper.AssignCmd( - CmdHelper.ExprToAssignLhs(path), - 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 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) - { - 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]), "Lheap_Write failed")); - return cmdSeq; - } - } - } - throw new cce.UnreachableException(); - } - - 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 RewriteLsetEmpty(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); - + var cmdSeq = new List(); 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 RewriteLsetSplit(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); @@ -394,7 +203,7 @@ private List RewriteLsetSplit(CallCmd callCmd) private List RewriteLsetGet(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); @@ -420,7 +229,7 @@ private List RewriteLsetGet(CallCmd callCmd) private List RewriteLsetPut(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); @@ -431,14 +240,14 @@ private List 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 RewriteLvalSplit(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); @@ -453,14 +262,14 @@ private List 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 RewriteLvalGet(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); @@ -485,40 +294,38 @@ private List RewriteLvalGet(CallCmd callCmd) private List RewriteLvalPut(CallCmd callCmd) { - GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor, + GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor); var cmdSeq = new List(); 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; } - private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, out Function lheapConstructor, + private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, out Function lsetConstructor, out Function lvalConstructor) { 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); - lheapConstructor = lheapTypeCtorDecl.Constructors[0]; var lsetTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lset", actualTypeParams); lsetConstructor = lsetTypeCtorDecl.Constructors[0]; var lvalTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lval", actualTypeParams); lvalConstructor = lvalTypeCtorDecl.Constructors[0]; } - + private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) { var rc = new ResolutionContext(null, options); @@ -533,4 +340,51 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable absys) absys.ForEach(absy => absy.Typecheck(tc)); tc.CheckModifies = oldCheckModifies; } -} \ No newline at end of file + + 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 mapValExpr && + mapValExpr.Fun is FieldAccess fa && + fa.FieldName == "val" && + mapValExpr.Args[0].Type is CtorType ctorType && + Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Map") + { + var cmdSeq = CreateAccessAsserts(mapValExpr.Args[0], tok, msg); + var mapContainsFunc = MapContains(nAryExpr.Args[1].Type, nAryExpr.Type); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(mapContainsFunc, mapValExpr.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.FieldAccess.FieldName == "val" && + fieldAssignLhs1.Datatype.Type is CtorType ctorType && + Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Map") + { + var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg); + var mapContainsFunc = MapContains(mapAssignLhs.Indexes[0].Type, mapAssignLhs.Map.Type); + cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(mapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg)); + return cmdSeq; + } + return new List(); + } +} diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 32927bb45..005fc6367 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 == "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 => @@ -70,6 +173,11 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) public override Implementation VisitImplementation(Implementation node) { + if (IsPrimitive(node)) + { + return node; + } + enclosingProc = node.Proc; node.PruneUnreachableBlocks(civlTypeChecker.Options); @@ -201,12 +309,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 +509,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 +527,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 +586,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 +688,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(); @@ -665,8 +816,61 @@ public override Variable VisitVariable(Variable node) public IEnumerable LinearDomains => domainNameToLinearDomain.Values.Union(linearTypeToLinearDomain.Values); + private void CheckLinearStoreAccessInGuards() + { + program.Implementations.ForEach(impl => { + if (IsPrimitive(impl)) + { + return; + } + 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); @@ -734,7 +938,14 @@ public Expr DisjointnessExprForPermissions(LinearDomain domain, IEnumerable LheapWellFormedExpressions(IEnumerable availableVars) + 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) @@ -742,12 +953,22 @@ 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 "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 = 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/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs index 46faf0eb8..6f760241e 100644 --- a/Source/Concurrency/TransitionRelationComputation.cs +++ b/Source/Concurrency/TransitionRelationComputation.cs @@ -374,6 +374,11 @@ private void TryElimination(IEnumerable extraDefinedVariables) varToExpr[assignment.Var] = SubstitutionHelper.Apply(varToExpr, assignment.Expr); changed = true; } + else if (Defined(assignment.Var) && assignment.Expr is IdentifierExpr ie && !Defined(ie.Decl)) + { + varToExpr[ie.Decl] = SubstitutionHelper.Apply(varToExpr, Expr.Ident(assignment.Var)); + changed = true; + } else { remainingAssignments.Add(assignment); diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index d0811a142..61a20c07d 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -188,32 +188,31 @@ public override Implementation VisitImplementation(Implementation impl) public override Block VisitBlock(Block node) { - Block block = base.VisitBlock(node); + var block = base.VisitBlock(node); absyMap[block] = node; return block; } public override Cmd VisitAssertCmd(AssertCmd node) { - AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); + var assertCmd = (AssertCmd) base.VisitAssertCmd(node); if (!node.Layers.Contains(layerNum)) { assertCmd.Expr = Expr.True; } - return assertCmd; } public override Cmd VisitCallCmd(CallCmd call) { - CallCmd newCall = (CallCmd) base.VisitCallCmd(call); + var newCall = (CallCmd) base.VisitCallCmd(call); absyMap[newCall] = call; return newCall; } public override Cmd VisitParCallCmd(ParCallCmd parCall) { - ParCallCmd newParCall = (ParCallCmd) base.VisitParCallCmd(parCall); + var newParCall = (ParCallCmd) base.VisitParCallCmd(parCall); absyMap[newParCall] = parCall; foreach (var newCall in newParCall.CallCmds) { 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/AST/Absy.cs b/Source/Core/AST/Absy.cs index 420933bf9..8747597ab 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -890,11 +890,10 @@ public bool AddConstructor(DatatypeConstructor constructor) return true; } - public bool AddConstructor(IToken tok, string name, List fields) + public bool AddConstructor(IToken tok, string name, List fields) { var returnType = new CtorType(this.tok, this, new List(this.typeParameters)); - var function = new Function(tok, name, new List(this.typeParameters), - fields.Select(field => new Formal(field.tok, field, true)).ToList(), + var function = new Function(tok, name, new List(this.typeParameters), fields, new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, returnType), false)); var constructor = new DatatypeConstructor(function); return AddConstructor(constructor); @@ -2479,7 +2478,7 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null; this.Condition.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck @@ -2603,7 +2602,7 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ?new LayerRange(Layers[0], Layers[^1]) : null; this.Condition.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 12a681e1b..9287dc836 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -3261,6 +3261,20 @@ public override void Resolve(ResolutionContext rc) (this as ICarriesAttributes).ResolveAttributes(rc); Layers = (this as ICarriesAttributes).FindLayers(); + if (rc.Proc is YieldProcedureDecl callerDecl) { + if (Layers.Count > 2) + { + rc.Error(this, "expected layer range"); + } + else if (Layers.Count == 0) + { + Layers = new List{ LayerRange.Min, callerDecl.Layer }; + } + else if (Layers[^1] > callerDecl.Layer) + { + rc.Error(this, $"layer must be no more than layer {callerDecl.Layer}"); + } + } var id = QKeyValue.FindStringAttribute(Attributes, "id"); if (id != null) @@ -3305,8 +3319,13 @@ public override void Resolve(ResolutionContext rc) // checking calls from atomic actions need type information, hence postponed to type checking } - private void TypecheckCallCmdInYieldProcedureDecl(YieldProcedureDecl callerDecl, TypecheckingContext tc) + private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) { + if (tc.Proc is not YieldProcedureDecl callerDecl) + { + return; + } + var callerModifiedVars = new HashSet(callerDecl.ModifiedVars); void CheckModifies(IEnumerable modifiedVars) @@ -3440,47 +3459,36 @@ void CheckModifies(IEnumerable modifiedVars) else { Debug.Assert(Proc.IsPure); - if (Layers.Count == 0 || Layers.Count > 2) - { - tc.Error(this, "expected layer range"); - } - else if (Layers[^1] > callerDecl.Layer) - { - tc.Error(this, $"layer must be no more than layer {callerDecl.Layer}"); - } - else + var usedVars = VariableCollector.Collect(Ins.Union(Outs)); + if (usedVars.OfType().Any()) { - var usedVars = VariableCollector.Collect(Ins.Union(Outs)); - if (usedVars.OfType().Any()) + if (Layers.Count == 2) { - if (Layers.Count == 2) - { - tc.Error(this, "expected singleton layer range"); - } - else + tc.Error(this, "expected singleton layer range"); + } + else + { + // Check global outputs only; the checking of local outputs is done later + var calleeLayer = Layers[0]; + var globalOutputs = Outs.Select(ie => ie.Decl).OfType().Cast(); + if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name)) { - // Check global outputs only; the checking of local outputs is done later - var calleeLayer = Layers[0]; - var globalOutputs = Outs.Select(ie => ie.Decl).OfType().Cast(); - if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name)) + var modifiedArgument = CivlPrimitives.ModifiedArgument(this); + if (modifiedArgument is { Decl: GlobalVariable }) { - var modifiedArgument = CivlPrimitives.ModifiedArgument(this); - if (modifiedArgument is { Decl: GlobalVariable }) - { - globalOutputs = globalOutputs.Append(modifiedArgument.Decl); - } + globalOutputs = globalOutputs.Append(modifiedArgument.Decl); } - globalOutputs.Where(v => v.LayerRange.LowerLayer != calleeLayer).ForEach(v => + } + globalOutputs.Where(v => v.LayerRange.LowerLayer != calleeLayer).ForEach(v => + { + tc.Error(this, $"variable must be introduced at layer {calleeLayer}: {v.Name}"); + }); + if (calleeLayer < callerDecl.Layer) + { + globalOutputs.Where(v => v.LayerRange.UpperLayer != calleeLayer).ForEach(v => { - tc.Error(this, $"variable must be introduced at layer {calleeLayer}: {v.Name}"); + tc.Error(this, $"variable must be hidden at layer {calleeLayer}: {v.Name}"); }); - if (calleeLayer < callerDecl.Layer) - { - globalOutputs.Where(v => v.LayerRange.UpperLayer != calleeLayer).ForEach(v => - { - tc.Error(this, $"variable must be hidden at layer {calleeLayer}: {v.Name}"); - }); - } } } } @@ -3571,17 +3579,13 @@ public override void Typecheck(TypecheckingContext tc) Contract.Assume(this.Proc != null); // we assume the CallCmd has been successfully resolved before calling this Typecheck method + var errorCount = tc.ErrorCount; + (this as ICarriesAttributes).TypecheckAttributes(tc); List expectedLayerRanges = null; if (tc.Proc is YieldProcedureDecl callerDecl) { - var errorCount = tc.ErrorCount; - TypecheckCallCmdInYieldProcedureDecl(callerDecl, tc); - if (errorCount < tc.ErrorCount) - { - return; - } for (int i = 0; i < Proc.OutParams.Count; i++) { var formal = Proc.OutParams[i]; @@ -3690,6 +3694,11 @@ public override void Typecheck(TypecheckingContext tc) TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters, actualTypeParams); + if (tc.ErrorCount > errorCount) + { + return; + } + TypecheckCallCmdInYieldProcedureDecl(tc); TypecheckCallCmdInActionDecl(tc); } @@ -4389,7 +4398,7 @@ public override void Emit(TokenTextWriter stream, int level) public override void Typecheck(TypecheckingContext tc) { (this as ICarriesAttributes).TypecheckAttributes(tc); - tc.ExpectedLayerRange = Layers == null || Layers.Count == 0 ? null : new LayerRange(Layers[0], Layers[^1]); + tc.ExpectedLayerRange = Layers?.Count > 0 ? new LayerRange(Layers[0], Layers[^1]) : null; Expr.Typecheck(tc); tc.ExpectedLayerRange = null; Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index ab76a6c77..6f1f0c676 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -278,7 +278,7 @@ ProcFormals<.bool incoming, bool allowWhereClauses, out List/*!*/ ds.> var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; .) "(" - [ AttrsIdsTypeWheres + [ AttributesIdsTypeWheres ] ")" . @@ -290,7 +290,7 @@ BoundVars<.out List/*!*/ ds.> ds = new List(); var dsx = ds; .) - AttrsIdsTypeWheres + AttributesIdsTypeWheres . /*------------------------------------------------------------------------*/ @@ -306,8 +306,8 @@ IdsType<.out List/*!*/ tyds.> .) . -/* AttrsIdsTypeWheres is used with the declarations of formals and bound variables */ -AttrsIdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> +/* AttributesIdsTypeWheres is used with the declarations of formals and bound variables */ +AttributesIdsTypeWheres<. bool allowWhereClauses, string context, System.Action action .> = AttributesIdsTypeWhere { "," AttributesIdsTypeWhere } @@ -626,10 +626,10 @@ Constructors . Constructor -= (. IToken name; List fields = new List(); .) += (. IToken name; List fields = new List(); .) Ident "(" - [ IdsTypeWheres ] + [ AttributesIdsTypeWheres ] ")" (. if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) { @@ -716,7 +716,8 @@ ActionDecl(), null); - datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList()); + var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); + datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); } } actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 3dc7f1ddc..1976936ce 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -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 layerRanges) { Debug.Assert(layerRanges.Any()); @@ -55,7 +55,7 @@ public static LayerRange Union(List layerRanges) } return unionLayerRange; } - + public override string ToString() { return $"[{LowerLayer}, {UpperLayer}]"; @@ -169,7 +169,7 @@ public static void RemoveLinearAttributes(ICarriesAttributes obj) { RemoveAttributes(obj, LINEAR_ATTRIBUTES); } - + public static bool IsCallMarked(CallCmd callCmd) { return callCmd.HasAttribute(MARK); @@ -178,12 +178,12 @@ public static bool IsCallMarked(CallCmd callCmd) public static class CivlPrimitives { - public static HashSet LinearTypes = new() { "Lheap", "Lset", "Lval" }; + public static HashSet LinearTypes = new() { "Lmap", "Lset", "Lval" }; public static HashSet LinearPrimitives = new() { - "Ref_Alloc", - "Lheap_Empty", "Lheap_Get", "Lheap_Put", "Lheap_Read", "Lheap_Write", "Lheap_Alloc", "Lheap_Remove", + "Loc_New", + "Lmap_Empty", "Lmap_Alloc", "Lmap_Create", "Lmap_Free", "Lmap_Move", "Lmap_Assume", "Lset_Empty", "Lset_Split", "Lset_Get", "Lset_Put", "Lval_Split", "Lval_Get", "Lval_Put" }; @@ -196,61 +196,35 @@ public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr) } if (expr is NAryExpr nAryExpr) { - if (nAryExpr.Fun is FieldAccess) - { - return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]); - } - if (nAryExpr.Fun is MapSelect) + if (nAryExpr.Fun is FieldAccess or 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; } - + 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": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); - case "Lheap_Read": - return null; - case "Lheap_Write": - case "Lheap_Alloc": - case "Lheap_Remove": - return ExtractRootFromAccessPathExpr(callCmd.Ins[0]); + case "Loc_New": + case "Lmap_Empty": + case "Lmap_Alloc": + case "Lmap_Create": + case "Lmap_Free": + case "Lmap_Move": + case "Lmap_Assume": 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]); } } - + public static HashSet Async = new() { "create_async", "create_asyncs", "create_multi_asyncs", "set_choice" }; } -} \ No newline at end of file +} diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 6eefe668f..871576e28 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -736,7 +736,8 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl, else { datatypeTypeCtorDecl = new DatatypeTypeCtorDecl(name, name.val, new List(), null); - datatypeTypeCtorDecl.AddConstructor(name, name.val, ins.Select(v => new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)).ToList()); + var fields = ins.Select(v => new Formal(v.tok, new TypedIdent(v.TypedIdent.tok, v.Name, v.TypedIdent.Type), true, v.Attributes)).ToList(); + datatypeTypeCtorDecl.AddConstructor(name, name.val, fields); } } actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, mods, datatypeTypeCtorDecl, kv); @@ -791,12 +792,12 @@ void ProcFormals(bool incoming, bool allowWhereClauses, out List/*!*/ Expect(11); if (StartOf(12)) { - AttrsIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); + AttributesIdsTypeWheres(allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } Expect(12); } - void AttrsIdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { + void AttributesIdsTypeWheres(bool allowWhereClauses, string context, System.Action action ) { AttributesIdsTypeWhere(allowWhereClauses, context, action); while (la.kind == 14) { Get(); @@ -810,7 +811,7 @@ void BoundVars(out List/*!*/ ds) { ds = new List(); var dsx = ds; - AttrsIdsTypeWheres(false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } ); + AttributesIdsTypeWheres(false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } ); } void IdsType(out List/*!*/ tyds) { @@ -1076,11 +1077,11 @@ void Constructors(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { } void Constructor(DatatypeTypeCtorDecl datatypeTypeCtorDecl) { - IToken name; List fields = new List(); + IToken name; List fields = new List(); Ident(out name); Expect(11); - if (StartOf(14)) { - IdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti) { fields.Add(ti); }); + if (StartOf(12)) { + AttributesIdsTypeWheres(false, "datatype constructor", delegate(TypedIdent ti, QKeyValue kv) { fields.Add(new Formal(ti.tok, ti, true, kv)); }); } Expect(12); if (!datatypeTypeCtorDecl.AddConstructor(name, name.val, fields)) { diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 7e0b69bc6..a39efd1c2 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -217,65 +217,100 @@ function Set_Intersection(a: Set T, b: Set T): Set T Set(MapAnd(a->val, b->val)) } -function Set_Choose(a: Set T): T; -axiom (forall a: Set T :: {Set_Choose(a)} a == Set_Empty() || Set_Contains(a, Set_Choose(a))); +function Choice(a: [T]bool): T; +axiom (forall a: [T]bool :: {Choice(a)} a == MapConst(false) || a[Choice(a)]); /// finite maps datatype Map { Map(dom: Set T, val: [T]U) } +function {:inline} Map_Empty(): Map T U +{ + Map(Set(MapConst(false)), MapConst(Default())) +} + +function {:inline} Map_Singleton(t: T, u: U): Map T U +{ + Map_Update(Map_Empty(), t, u) +} + function {:inline} Map_Contains(a: Map T U, t: T): bool { - Set_Contains(a->dom, t) + Set_Contains(a->dom, t) +} + +function {:inline} Map_IsDisjoint(a: Map T U, b: Map T U): bool +{ + Set_IsDisjoint(a->dom, b->dom) } function {:inline} Map_At(a: Map T U, t: T): U { - a->val[t] + a->val[t] } function {:inline} Map_Remove(a: Map T U, t: T): Map T U { - Map(Set_Remove(a->dom, t), a->val[t := Default()]) + Map(Set_Remove(a->dom, t), a->val[t := Default()]) } function {:inline} Map_Update(a: Map T U, t: T, u: U): Map T U { - Map(Set_Add(a->dom, t), a->val[t := u]) + Map(Set_Add(a->dom, t), a->val[t := u]) } function {:inline} Map_Swap(a: Map T U, t1: T, t2: T): Map T U { - (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1)) + (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1)) } -/// linear heaps -type Ref _; -procedure Ref_Alloc() returns (k: Lval (Ref V)); +function {:inline} Map_WellFormed(a: Map K V): bool { + a->val == MapIte(a->dom->val, a->val, MapConst(Default())) +} -datatype Lheap { Lheap(dom: [Ref V]bool, val: [Ref V]V) } -function Nil(): Ref V; +/// linear maps +type Loc _; +pure procedure {:inline 1} Loc_New() returns (k: Lval (Loc V)) { -function {:inline} Lheap_WellFormed(l: Lheap V): bool { - l->val == MapIte(l->dom, l->val, MapConst(Default())) } -function {:inline} Lheap_Collector(l: Lheap V): [Ref V]bool { - MapConst(false) +datatype Ref { + Ref(loc: Loc V), + Nil() } -function {:inline} Lheap_Contains(l: Lheap V, k: Ref V): bool { - l->dom[k] + +datatype Lmap { Lmap(val: Map K V) } +type Lheap V = Lmap (Ref V) V; + +function {:inline} Lmap_WellFormed(l: Lmap K V): bool { + Map_WellFormed(l->val) +} +function {:inline} Lmap_Collector(l: Lmap K V): [K]bool { + l->val->dom->val +} +pure procedure {:inline 1} Lmap_Empty() returns (l: Lmap K V) { + l := Lmap(Map_Empty()); } -function {:inline} Lheap_Deref(l: Lheap V, k: Ref V): V { - l->val[k] +pure procedure {:inline 1} Lmap_Alloc(v: V) returns (k: Lval (Loc V), l: Lmap (Ref V) V) { + var r: Ref V; + r := Ref(k->val); + l := Lmap(Map_Singleton(r, v)); +} +pure procedure {:inline 1} Lmap_Create({:linear_in} k: Lset K, val: [K]V) returns (l: Lmap K V) { + l := Lmap(Map(Set(k->dom), val)); +} +pure procedure {:inline 1} Lmap_Free({:linear_in} l: Lmap K V) returns (k: Lset K) { + k := Lset(l->val->dom->val); +} +pure procedure {:inline 1} Lmap_Move({:linear_in} src: Lmap K V, dst: Lmap K V, k: K) returns (src': Lmap K V, dst': Lmap K V) { + assert Map_Contains(src->val, k); + assert Map_IsDisjoint(src->val, dst->val); + dst' := Lmap(Map_Update(dst->val, k, Map_At(src->val, k))); + src' := Lmap(Map_Remove(src->val, k)); +} +pure procedure {:inline 1} Lmap_Assume(src: Lmap K V, dst: Lmap K V) { + assume Map_IsDisjoint(src->val, dst->val); } -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); /// linear sets datatype Lset { Lset(dom: [V]bool) } @@ -313,3 +348,6 @@ pure procedure {:inline 1} Copy(v: T) returns (copy_v: T) { copy_v := v; } + +pure procedure Assume(b: bool); +ensures b; diff --git a/Source/Core/node.bpl b/Source/Core/node.bpl index 64fc6c33f..65964c53e 100644 --- a/Source/Core/node.bpl +++ b/Source/Core/node.bpl @@ -5,31 +5,6 @@ datatype Node { Node(next: RefNode T, val: T) } type RefNode T = Ref (Node T); -function {:inline} Empty(): [RefNode T]bool -{ - MapConst(false) -} - -function {:inline} Singleton(a: RefNode T): [RefNode T]bool -{ - MapOne(a) -} - -function {:inline} Union(x: [RefNode T]bool, y: [RefNode T]bool): [RefNode T]bool -{ - MapOr(x, y) -} - -function {:inline} Difference(x: [RefNode T]bool, y: [RefNode T]bool): [RefNode T]bool -{ - MapDiff(x, y) -} - -function {:inline} Subset(x: [RefNode T]bool, y: [RefNode T]bool): bool -{ - MapDiff(x, y) == MapConst(false) -} - function Between(f: [RefNode T]Node T, x: RefNode T, y: RefNode T, z: RefNode T): bool; function Avoiding(f: [RefNode T]Node T, x: RefNode T, y: RefNode T, z: RefNode T): bool; function {:inline} BetweenSet(f:[RefNode T]Node T, x: RefNode T, z: RefNode T): [RefNode T]bool diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f3fdec444..f4e12d754 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.9 + 3.0.10 net6.0 false Boogie diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 2264bdacd..fc1bbf071 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1091,7 +1091,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing } Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr); - if (Options.ModelViewFile != null && pc is AssumeCmd captureStateAssumeCmd) + if (Options.ExpectingModel && pc is AssumeCmd captureStateAssumeCmd) { string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState"); if (description != null) diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 00055e2c2..9e67e31ac 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -69,9 +69,12 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a } var assume = new AssumeCmd(assrt.tok, expr); - // Copy any {:id ...} from the assertion to the assumption, so - // we can track it while analyzing verification coverage. - (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); + if (expr != Expr.True) { + // Copy any {:id ...} from the assertion to the assumption, so + // we can track it while analyzing verification coverage. But + // skip it if it's `true` because that's never useful to track. + (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); + } return assume; } diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl index 4d04b75ff..29f5c5ba7 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl @@ -5,31 +5,36 @@ const n:int; axiom n >= 1; type val = int; -type {:linear "collect", "broadcast"} pid = int; +type pid = int; + +datatype {:linear "perm"} perm { + Broadcast(i: int), + Collect(i: int) +} function {:inline} pid(i:int) : bool { 1 <= i && i <= n } function {:inline} InitialBroadcastPAs (k:pid) : [BROADCAST]bool { - (lambda pa:BROADCAST :: pid(pa->i) && pa->i < k) + (lambda pa:BROADCAST :: pa->p == Broadcast(pa->i) && pid(pa->i) && pa->i < k) } function {:inline} InitialCollectPAs (k:pid) : [COLLECT]bool { - (lambda pa:COLLECT :: pid(pa->i) && pa->i < k) + (lambda pa:COLLECT :: pa->p == Collect(pa->i) && pid(pa->i) && pa->i < k) } function {:inline} AllBroadcasts () : [BROADCAST]bool -{ (lambda pa:BROADCAST :: pid(pa->i)) } +{ (lambda pa:BROADCAST :: pa->p == Broadcast(pa->i) && pid(pa->i)) } function {:inline} AllCollects () : [COLLECT]bool -{ (lambda pa:COLLECT :: pid(pa->i)) } +{ (lambda pa:COLLECT :: pa->p == Collect(pa->i) && pid(pa->i)) } function {:inline} RemainingBroadcasts (k:pid) : [BROADCAST]bool -{ (lambda {:pool "Broadcast"} pa:BROADCAST :: k < pa->i && pa->i <= n) } +{ (lambda {:pool "Broadcast"} pa:BROADCAST :: pa->p == Broadcast(pa->i) && k < pa->i && pa->i <= n) } function {:inline} RemainingCollects (k:pid) : [COLLECT]bool -{ (lambda {:pool "Collect"} pa:COLLECT :: k < pa->i && pa->i <= n) } +{ (lambda {:pool "Collect"} pa:COLLECT :: pa->p == Collect(pa->i) && k < pa->i && pa->i <= n) } //////////////////////////////////////////////////////////////////////////////// @@ -61,16 +66,11 @@ function value_card(v:val, value:[pid]val, i:pid, j:pid) : int //////////////////////////////////////////////////////////////////////////////// -// NOTE: Civl currently does not support variables to be linear in multiple -// domains (i.e., supplying multiple linear annotations). In the future we -// would like the MAIN action(s) to take a single parameter as follows: -// {:linear_in "broadcast"}{:linear_in "collect"} pids:[pid]bool - atomic action {:layer 4} -MAIN''({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +MAIN''({:linear_in "perm"} ps:[perm]bool) modifies CH, decision; { - assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast; + assert ps == (lambda p:perm :: pid(p->i)); assert CH == MultisetEmpty; CH := (lambda v:val :: value_card(v, value, 1, n)); assume card(CH) == n; @@ -79,13 +79,13 @@ modifies CH, decision; } action {:layer 3} -INV_COLLECT_ELIM({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +INV_COLLECT_ELIM({:linear_in "perm"} ps:[perm]bool) creates COLLECT; modifies CH, decision; { var {:pool "INV_COLLECT"} k: int; - assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast; + assert ps == (lambda p:perm :: pid(p->i)); assert CH == MultisetEmpty; CH := (lambda v:val :: value_card(v, value, 1, n)); @@ -94,23 +94,23 @@ modifies CH, decision; assume {:add_to_pool "INV_COLLECT", k, k+1} - {:add_to_pool "Collect", COLLECT(n)} + {:add_to_pool "Collect", COLLECT(Collect(n), n)} 0 <= k && k <= n; decision := (lambda i:pid :: if 1 <= i && i <= k then max(CH) else decision[i]); call create_asyncs(RemainingCollects(k)); - call set_choice(COLLECT(k+1)); + call set_choice(COLLECT(Collect(k+1), k+1)); } //////////////////////////////////////////////////////////////////////////////// atomic action {:layer 3} -MAIN'({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +MAIN'({:linear_in "perm"} ps:[perm]bool) refines MAIN'' using INV_COLLECT_ELIM; creates COLLECT; eliminates COLLECT using COLLECT'; modifies CH; { - assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast; + assert ps == (lambda p:perm :: pid(p->i)); assert CH == MultisetEmpty; assume {:add_to_pool "INV_COLLECT", 0} true; @@ -121,11 +121,11 @@ modifies CH; } atomic action {:layer 2} -MAIN({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +MAIN({:linear_in "perm"} ps:[perm]bool) refines MAIN' using INV_BROADCAST_ELIM; creates BROADCAST, COLLECT; { - assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast; + assert ps == (lambda p:perm :: pid(p->i)); assume {:add_to_pool "INV_BROADCAST", 0} true; assert CH == MultisetEmpty; @@ -135,52 +135,52 @@ creates BROADCAST, COLLECT; } action {:layer 2} -INV_BROADCAST_ELIM({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +INV_BROADCAST_ELIM({:linear_in "perm"} ps:[perm]bool) creates BROADCAST, COLLECT; modifies CH; { var {:pool "INV_BROADCAST"} k: int; - assert pidsBroadcast == (lambda i:pid :: pid(i)) && pidsCollect == pidsBroadcast; + assert ps == (lambda p:perm :: pid(p->i)); assert CH == MultisetEmpty; assume {:add_to_pool "INV_BROADCAST", k, k+1} - {:add_to_pool "Broadcast", BROADCAST(n)} + {:add_to_pool "Broadcast", BROADCAST(Broadcast(n), n)} 0 <= k && k <= n; CH := (lambda v:val :: value_card(v, value, 1, k)); assume card(CH) == k; assume MultisetSubsetEq(MultisetEmpty, CH); call create_asyncs(RemainingBroadcasts(k)); call create_asyncs(AllCollects()); - call set_choice(BROADCAST(k+1)); + call set_choice(BROADCAST(Broadcast(k+1), k+1)); } -async left action {:layer 2} BROADCAST({:linear_in "broadcast"} i:pid) +async left action {:layer 2} BROADCAST({:linear_in "perm"} p:perm, i:pid) modifies CH; { - assert pid(i); + assert pid(i) && p == Broadcast(i); CH := CH[value[i] := CH[value[i]] + 1]; } -async atomic action {:layer 2,3} COLLECT({:linear_in "collect"} i:pid) +async atomic action {:layer 2,3} COLLECT({:linear_in "perm"} p:perm, i:pid) modifies decision; { var received_values:[val]int; - assert pid(i); + assert pid(i) && p == Collect(i); assume card(received_values) == n; assume MultisetSubsetEq(MultisetEmpty, received_values); assume MultisetSubsetEq(received_values, CH); decision[i] := max(received_values); } -action {:layer 3} COLLECT'({:linear_in "collect"} i:pid) +action {:layer 3} COLLECT'({:linear_in "perm"} p:perm, i:pid) modifies decision; { assert CH == (lambda v:val :: value_card(v, value, 1, n)); assert card(CH) == n; assert MultisetSubsetEq(MultisetEmpty, CH); - call COLLECT(i); + call COLLECT(p, i); } //////////////////////////////////////////////////////////////////////////////// @@ -201,45 +201,43 @@ pure procedure {:inline 1} add_to_multiset (CH:[val]int, x: val) returns (CH':[v //////////////////////////////////////////////////////////////////////////////// yield invariant {:layer 1} -YieldInit({:linear "broadcast"} pidsBroadcast:[pid]bool, {:linear "collect"} pidsCollect:[pid]bool); -invariant pidsBroadcast == (lambda ii:pid :: pid(ii)) && pidsCollect == pidsBroadcast; +YieldInit({:linear "perm"} ps:[perm]bool); +invariant ps == (lambda p:perm :: pid(p->i)); invariant (forall ii:pid :: CH_low[ii] == MultisetEmpty); invariant CH == MultisetEmpty; yield procedure {:layer 1} -Main({:linear_in "broadcast"} pidsBroadcast:[pid]bool, {:linear_in "collect"} pidsCollect:[pid]bool) +Main({:linear_in "perm"} ps:[perm]bool) refines MAIN; -requires call YieldInit(pidsBroadcast, pidsCollect); +requires call YieldInit(ps); { var {:pending_async}{:layer 1} Broadcast_PAs:[BROADCAST]int; var {:pending_async}{:layer 1} Collect_PAs:[COLLECT]int; var i:pid; - var {:linear "broadcast"} s:pid; - var {:linear "collect"} r:pid; - var {:linear "broadcast"} ss:[pid]bool; - var {:linear "collect"} rr:[pid]bool; + var {:linear "perm"} s:perm; + var {:linear "perm"} r:perm; + var {:linear "perm"} ps':[perm]bool; - ss := pidsBroadcast; - rr := pidsCollect; + ps' := ps; i := 1; while (i <= n) invariant {:layer 1} 1 <= i && i <= n + 1; - invariant {:layer 1} ss == (lambda ii:pid :: pid(ii) && ii >= i) && ss == rr; + invariant {:layer 1} ps' == (lambda p:perm :: pid(p->i) && p->i >= i); invariant {:layer 1} Broadcast_PAs == ToMultiset(InitialBroadcastPAs(i)); invariant {:layer 1} Collect_PAs == ToMultiset(InitialCollectPAs(i)); { - call s, r, ss, rr := linear_transfer(i, ss, rr); - async call Broadcast(s); - async call Collect(r); + call s, r, ps' := linear_transfer(i, ps'); + async call Broadcast(s, i); + async call Collect(r, i); i := i + 1; } assert {:layer 1} Broadcast_PAs == ToMultiset(AllBroadcasts()); assert {:layer 1} Collect_PAs == ToMultiset(AllCollects()); } -yield procedure {:layer 1} Broadcast({:linear_in "broadcast"} i:pid) +yield procedure {:layer 1} Broadcast({:linear_in "perm"} p:perm, i:pid) refines BROADCAST; -requires {:layer 1} pid(i); +requires {:layer 1} pid(i) && p == Broadcast(i); { var j: pid; var v: val; @@ -250,7 +248,7 @@ requires {:layer 1} pid(i); j := 1; while (j <= n) invariant {:layer 1} 1 <= j && j <= n+1; - invariant {:layer 1} CH_low == (lambda jj: pid :: (if pid(jj) && jj < j then MultisetPlus(old_CH_low[jj], MultisetSingleton(value[i])) else old_CH_low[jj])); + invariant {:layer 1} CH_low == (lambda jj: pid :: (if pid(jj) && jj < j then MultisetPlus(old_CH_low[jj], MultisetSingleton(value[p->i])) else old_CH_low[jj])); { call send(v, j); j := j + 1; @@ -259,10 +257,10 @@ requires {:layer 1} pid(i); } yield procedure {:layer 1} -Collect({:linear_in "collect"} i:pid) +Collect({:linear_in "perm"} p:perm, i:pid) refines COLLECT; requires call YieldInv(); -requires {:layer 1} pid(i); +requires {:layer 1} pid(i) && p == Collect(i); { var j: pid; var d: val; @@ -287,7 +285,7 @@ requires {:layer 1} pid(i); received_values[v] := received_values[v] + 1; j := j + 1; } - call set_decision(i, d); + call set_decision(p, d); } //////////////////////////////////////////////////////////////////////////////// @@ -297,10 +295,11 @@ both action {:layer 1} GET_VALUE(i:pid) returns (v:val) v := value[i]; } -both action {:layer 1} SET_DECISION({:linear_in "collect"} i:pid, d:val) +both action {:layer 1} SET_DECISION({:linear_in "perm"} p:perm, d:val) modifies decision; { - decision[i] := d; + assert p is Collect; + decision[p->i] := d; } left action {:layer 1} SEND(v:val, i:pid) @@ -317,18 +316,18 @@ modifies CH_low; } both action {:layer 1} -LINEAR_TRANSFER(i:pid, {:linear_in "broadcast"} ss:[pid]bool, {:linear_in "collect"} rr:[pid]bool) -returns ({:linear "broadcast"} s:pid, {:linear "collect"} r:pid, {:linear "broadcast"} ss':[pid]bool, {:linear "collect"} rr':[pid]bool) +LINEAR_TRANSFER(i:pid, {:linear_in "perm"} ps:[perm]bool) +returns ({:linear "perm"} s:perm, {:linear "perm"} r:perm, {:linear "perm"} ps':[perm]bool) { - assert ss[i] && rr[i]; - s, r := i, i; - ss', rr' := ss[i := false], rr[i := false]; + assert ps[Broadcast(i)] && ps[Collect(i)]; + s, r := Broadcast(i), Collect(i); + ps' := ps[s := false][r := false]; } yield procedure {:layer 0} get_value(i:pid) returns (v:val); refines GET_VALUE; -yield procedure {:layer 0} set_decision({:linear_in "collect"} i:pid, d:val); +yield procedure {:layer 0} set_decision({:linear_in "perm"} p:perm, d:val); refines SET_DECISION; yield procedure {:layer 0} send(v:val, i:pid); @@ -337,8 +336,8 @@ refines SEND; yield procedure {:layer 0} receive(i:pid) returns (v:val); refines RECEIVE; -yield procedure {:layer 0} linear_transfer(i:pid, {:linear_in "broadcast"} ss:[pid]bool, {:linear_in "collect"} rr:[pid]bool) -returns ({:linear "broadcast"} s:pid, {:linear "collect"} r:pid, {:linear "broadcast"} ss':[pid]bool, {:linear "collect"} rr':[pid]bool); +yield procedure {:layer 0} linear_transfer(i:pid, {:linear_in "perm"} ps:[perm]bool) +returns ({:linear "perm"} s:perm, {:linear "perm"} r:perm, {:linear "perm"} ps':[perm]bool); refines LINEAR_TRANSFER; //////////////////////////////////////////////////////////////////////////////// diff --git a/Test/civl/inductive-sequentialization/paxos/Paxos.bpl b/Test/civl/inductive-sequentialization/paxos/Paxos.bpl index b5feeac3d..43cb52d39 100644 --- a/Test/civl/inductive-sequentialization/paxos/Paxos.bpl +++ b/Test/civl/inductive-sequentialization/paxos/Paxos.bpl @@ -90,8 +90,8 @@ function {:inline} VotePAs(r: Round, v: Value) : [A_Vote]bool //////////////////////////////////////////////////////////////////////////////// //// Global variables // Abstract -var {:layer 1,3} joinedNodes: [Round]NodeSet; -var {:layer 1,3} voteInfo: [Round]Option VoteInfo; +var {:layer 1,2} joinedNodes: [Round]NodeSet; +var {:layer 1,2} voteInfo: [Round]Option VoteInfo; var {:layer 1,3} decision: [Round]Option Value; // spec // Concrete @@ -106,9 +106,10 @@ var {:layer 1,1} {:linear "perm"} permVoteChannel: VoteResponseChannel; //////////////////////////////////////////////////////////////////////////////// function {:inline} Init ( - rs: [Round]bool) : bool + rs: [Round]bool, decision: [Round]Option Value) : bool { - rs == (lambda r: Round :: true) + rs == (lambda r: Round :: true) && + decision == (lambda r: Round :: None()) } function {:inline} InitLow ( diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl index 664592ab8..2fded11eb 100644 --- a/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl +++ b/Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl @@ -56,7 +56,7 @@ function InvChannels (joinChannel: [Round][JoinResponse]int, permJoinChannel: Jo } yield invariant {:layer 1} YieldInit({:linear "perm"} rs: [Round]bool); -invariant Init(rs); +invariant Init(rs, decision); invariant InitLow(acceptorState, joinChannel, voteChannel, permJoinChannel, permVoteChannel); yield invariant {:layer 1} YieldInv(); diff --git a/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl b/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl index a290e358e..acbed721c 100644 --- a/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl +++ b/Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl @@ -4,22 +4,21 @@ refines A_Paxos' using INV; creates A_StartRound; { var {:pool "NumRounds"} numRounds: int; - assert Init(rs); + assert Init(rs, decision); assume {:add_to_pool "Round", 0, numRounds} {:add_to_pool "NumRounds", numRounds} 0 <= numRounds; joinedNodes := (lambda r: Round:: NoNodes()); voteInfo := (lambda r: Round:: None()); - decision := (lambda r: Round:: None()); call create_asyncs((lambda pa: A_StartRound :: pa->r == pa->r_lin && Round(pa->r) && pa->r <= numRounds)); } atomic action {:layer 3} A_Paxos'({:linear_in "perm"} rs: [Round]bool) -modifies joinedNodes, voteInfo, decision; +modifies decision; { - assert Init(rs); - havoc joinedNodes, voteInfo, decision; + assert Init(rs, decision); + havoc decision; assume (forall r1: Round, r2: Round :: decision[r1] is Some && decision[r2] is Some ==> decision[r1] == decision[r2]); } @@ -32,7 +31,7 @@ modifies joinedNodes, voteInfo, decision; var {:pool "Round"} k: int; var {:pool "Node"} m: Node; - assert Init(rs); + assert Init(rs, decision); havoc joinedNodes, voteInfo, decision; diff --git a/Test/civl/inductive-sequentialization/paxos/is.sh.expect b/Test/civl/inductive-sequentialization/paxos/is.sh.expect index 65d6dd918..773f14960 100644 --- a/Test/civl/inductive-sequentialization/paxos/is.sh.expect +++ b/Test/civl/inductive-sequentialization/paxos/is.sh.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 72 verified, 0 errors +Boogie program verifier finished with 73 verified, 0 errors diff --git a/Test/civl/regression-tests/linear/typecheck.bpl b/Test/civl/regression-tests/linear/typecheck.bpl index e0b728223..9092d00c8 100644 --- a/Test/civl/regression-tests/linear/typecheck.bpl +++ b/Test/civl/regression-tests/linear/typecheck.bpl @@ -2,24 +2,24 @@ // RUN: %diff "%s.expect" "%t" type X; -type {:linear "A", "B", "C", "D", "D2", "x", "", "lin"} Lin = int; +type {:linear "D"} Lin = int; procedure A() { - var {:linear "A"} a: X; - var {:linear "A"} b: int; + var {:linear "D"} a: X; + var {:linear "D"} b: int; } procedure B() { - var {:linear "B"} a: X; - var {:linear "B"} b: [X]bool; + var {:linear "D"} a: X; + var {:linear "D"} b: [X]bool; } procedure C() { - var {:linear "C"} a: X; - var {:linear "C"} c: [X]int; + var {:linear "D"} a: X; + var {:linear "D"} c: [X]int; } function f(X): X; @@ -30,7 +30,7 @@ yield procedure {:layer 1} D() var {:linear "D"} x: X; var {:linear "D"} b: [X]bool; var c: X; - var {:linear "D2"} d: X; + var {:linear "D"} d: X; b[a] := true; @@ -68,20 +68,20 @@ yield procedure {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) retur yield procedure {:layer 1} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X); -var {:linear "x"} g:int; +var {:linear "D"} g:int; -procedure G(i:int) returns({:linear "x"} r:int) +procedure G(i:int) returns({:linear "D"} r:int) { r := g; } -procedure H(i:int) returns({:linear "x"} r:int) +procedure H(i:int) returns({:linear "D"} r:int) modifies g; { g := r; } -yield procedure {:layer 1} I({:linear_in ""} x:int) returns({:linear ""} x':int) +yield procedure {:layer 1} I({:linear_in "D"} x:int) returns({:linear "D"} x':int) { x' := x; } @@ -90,13 +90,13 @@ yield procedure {:layer 1} J() { } -yield procedure {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int) +yield procedure {:layer 1} P1({:linear_in "D"} x:int) returns({:linear "D"} x':int) { par x' := I(x) | J(); call x' := I(x'); } -yield procedure {:layer 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int) +yield procedure {:layer 1} P2({:linear_in "D"} x:int) returns({:linear "D"} x':int) { call x' := I(x); par x' := I(x') | J(); diff --git a/Test/civl/regression-tests/linear/typecheck.bpl.expect b/Test/civl/regression-tests/linear/typecheck.bpl.expect index 15a7a7784..50ffc5805 100644 --- a/Test/civl/regression-tests/linear/typecheck.bpl.expect +++ b/Test/civl/regression-tests/linear/typecheck.bpl.expect @@ -1,14 +1,11 @@ typecheck.bpl(35,9): Error: Only simple assignment allowed on linear variable b typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a -typecheck.bpl(41,6): Error: The domains of source and target of assignment must be the same typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter: f(a) -typecheck.bpl(55,4): Error: The domains of parameter b and argument d must be the same -typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same typecheck.bpl(59,4): Error: Only linear variable can be passed to linear parameter: c typecheck.bpl(67,0): Error: Output variable d must be available at a return typecheck.bpl(76,0): Error: Global variable g must be available at a return typecheck.bpl(81,7): Error: unavailable source for a linear read typecheck.bpl(82,0): Error: Output variable r must be available at a return -13 type checking errors detected in typecheck.bpl +10 type checking errors detected in typecheck.bpl diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl index 85a2cdf30..2060cb3f0 100644 --- a/Test/civl/regression-tests/linear_types.bpl +++ b/Test/civl/regression-tests/linear_types.bpl @@ -1,26 +1,6 @@ // 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) { - 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(); - call k := Lheap_Alloc(path', v); - call v' := Lheap_Remove(path', k->val); -} - atomic action {:layer 1, 2} A3({:linear_in} path: Lset int, {:linear_out} l: Lset int) returns (path': Lset int) { call path' := Lset_Empty(); call Lset_Put(path', path); @@ -40,35 +20,14 @@ atomic action {:layer 1, 2} A5({:linear_in} path: Lheap int) returns (path': Lhe var {:layer 0, 2} g: Lheap int; -atomic action {:layer 1, 2} A6({:linear_in} path: Lheap int) returns (path': Lheap int) -modifies g; -{ - path' := path; - call Lheap_Put(path', g); - call g := Lheap_Empty(); -} - datatype Foo { Foo(f: Lheap int) } -atomic action {:layer 1, 2} A7({:linear_in} path: Lheap Foo, x: Ref Foo, y: Ref int) returns (path': Lheap Foo) -{ - var l: Lheap int; - path' := path; - call l := Lheap_Get(path'->val[x]->f, MapOne(y)); -} - atomic action {:layer 1, 2} A8({:linear_out} l: Lval int, {:linear_in} path: Lset int) returns (path': Lset int) { path' := path; call Lval_Split(path', l); } -atomic action {:layer 1, 2} A9({:linear_in} path1: Lheap int, x: Ref Foo) returns (path2: Lheap Foo) -{ - call path2 := Lheap_Empty(); - call Lheap_Put(path2->val[x]->f, path1); -} - atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo) { var x: Lheap int; diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl index 23e158117..88f607a61 100644 --- a/Test/civl/regression-tests/linear_types_error.bpl +++ b/Test/civl/regression-tests/linear_types_error.bpl @@ -7,58 +7,17 @@ atomic action {:layer 1, 2} A1(path: Lheap int) returns (path': Lheap int) { path' := path; } -atomic action {:layer 1, 2} A2(path: Lheap int) returns (path': Lheap int) { - call path' := Lheap_Empty(); - call Lheap_Put(path', path); +atomic action {:layer 1, 2} A2(path: Lheap int) returns (path': Lheap int) { var k: Lset (Ref int); + call path' := Lmap_Empty(); + call k := Lmap_Free(path); } var {:layer 0, 2} g: Lheap int; -atomic action {:layer 1, 2} A3({:linear_in} path: Lheap int) returns (path': Lheap int) -{ - path' := path; - call Lheap_Put(path', g); -} - datatype Foo { Foo(f: Lheap int) } - -atomic action {:layer 1, 2} A4({:linear_in} path: Lheap Foo, x: Ref Foo, {:linear_in} l: Lheap int) returns (path': Lheap Foo, l': Lheap int) -{ - path' := path; - l' := l; - call Lheap_Put(l', path'->val[x]->f); -} - atomic action {:layer 1, 2} A5({:linear_out} path: Lheap int) { } -atomic action {:layer 1, 2} A6({:linear_in} path: Lheap int) returns (path': Lheap int) -{ - path' := path; - call Lheap_Put(path', path'); -} - -atomic action {:layer 1, 2} A7(path1: Lheap int, {:linear_in} path2: Lheap int) returns (path': Lheap int) -{ - path' := path2; - call Lheap_Put(path', path1); -} - -atomic action {:layer 1, 2} A8({:linear_in} path1: Lheap int, x: Ref Foo) returns (path2: Lheap Foo) -{ - call Lheap_Put(path2->val[x]->f, path1); -} - -atomic action {:layer 1, 2} A9({:linear_in} l: Lheap int) -{ - call Lheap_Put(g, l); -} - -atomic action {:layer 1, 2} A10({:linear_in} l: Lheap int, l': Lheap int) -{ - call Lheap_Put(l', l); -} - atomic action {:layer 1, 2} A11({:linear_in} a: Foo) returns (b: Foo) { var x: Lheap int; @@ -87,3 +46,14 @@ atomic action {:layer 1, 2} A14({:linear_in} a: Lval int) returns (b: Bar) type {:linear "X"} X = int; yield procedure {:layer 1} A15({:linear_in "X"} a: Lval int); + +yield procedure {:layer 1} Foo1(x: Lheap int) +{ + call Lmap_Assume(x, x); +} + +yield procedure {:layer 1} Foo2(x: Foo) +{ + call Lmap_Assume(x->f, x->f); +} + diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect index ac64bcea0..891e35034 100644 --- a/Test/civl/regression-tests/linear_types_error.bpl.expect +++ b/Test/civl/regression-tests/linear_types_error.bpl.expect @@ -1,18 +1,12 @@ -linear_types_error.bpl(89,48): Error: Variable of linear type must not have a domain name +linear_types_error.bpl(48,48): Error: Variable of linear type must not have a domain name linear_types_error.bpl(4,73): Error: Output variable l must be available at a return linear_types_error.bpl(8,0): Error: Input variable path must be available at a return linear_types_error.bpl(13,0): Error: Input variable path must be available at a return -linear_types_error.bpl(21,0): Error: Global variable g must be available at a return -linear_types_error.bpl(30,4): Error: Only variable can be passed to linear parameter: path'->val[x]->f -linear_types_error.bpl(33,64): Error: Input variable path must be available at a return -linear_types_error.bpl(38,4): Error: Linear variable path' can occur only once as an input parameter -linear_types_error.bpl(45,0): Error: Input variable path1 must be available at a return -linear_types_error.bpl(49,19): Error: unavailable source path2 for linear parameter at position 0 -linear_types_error.bpl(50,0): Error: Output variable path2 must be available at a return -linear_types_error.bpl(54,4): Error: Primitive assigns to a global variable that is not in the enclosing action's modifies clause: g -linear_types_error.bpl(59,4): Error: Primitive assigns to input variable: l' -linear_types_error.bpl(66,0): Error: Output variable b must be available at a return -linear_types_error.bpl(72,14): Error: unavailable source for a linear read -linear_types_error.bpl(78,9): Error: unavailable source for a linear read -linear_types_error.bpl(85,6): Error: A source of pack of linear type must be a variable -17 type checking errors detected in linear_types_error.bpl +linear_types_error.bpl(19,64): Error: Input variable path must be available at a return +linear_types_error.bpl(25,0): Error: Output variable b must be available at a return +linear_types_error.bpl(31,14): Error: unavailable source for a linear read +linear_types_error.bpl(37,9): Error: unavailable source for a linear read +linear_types_error.bpl(44,6): Error: A source of pack of linear type must be a variable +linear_types_error.bpl(52,2): Error: Linear variable x can occur only once as an input parameter +linear_types_error.bpl(57,2): Error: Linear variable x can occur only once as an input parameter +11 type checking errors detected in linear_types_error.bpl diff --git a/Test/civl/regression-tests/perm2.bpl b/Test/civl/regression-tests/perm2.bpl deleted file mode 100644 index 22ba8fae9..000000000 --- a/Test/civl/regression-tests/perm2.bpl +++ /dev/null @@ -1,100 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type {:linear "tid", "1", "2"} IntTid = int; - -var {:layer 0,1} g: int; -var {:layer 0,1} h: int; -var {:layer 0,1}{:linear "tid"} unallocated:[int]bool; - -atomic action {:layer 1} AtomicSetG(val:int) -modifies g; -{g := val; } - -yield procedure {:layer 0} SetG(val:int); -refines AtomicSetG; - -atomic action {:layer 1} AtomicSetH(val:int) -modifies h; -{ h := val; } - -yield procedure {:layer 0} SetH(val:int); -refines AtomicSetH; - -yield procedure {:layer 1} Allocate() returns ({:linear "tid"} xl: int) -ensures {:layer 1} xl != 0; -{ - call xl := AllocateLow(); -} - -atomic action {:layer 1} AtomicAllocateLow() returns ({:linear "tid"} xls: int) -modifies unallocated; -{ assume xls != 0; assume unallocated[xls]; unallocated[xls] := false; } - -yield procedure {:layer 0} AllocateLow() returns ({:linear "tid"} xls: int); -refines AtomicAllocateLow; - -yield procedure {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) -requires {:layer 1} x == MapConst(true); -requires {:layer 1} y == MapConst(true); -{ - var {:linear "tid"} tid_child: int; - tid_out := tid_in; - - call SetG(0); - - call Yield_g(x); - - call tid_child := Allocate(); - async call B(tid_child, x); - - call Yield(); - - call SetH(0); - - call Yield_h(y); - - call tid_child := Allocate(); - async call C(tid_child, y); - -} - -yield procedure {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) -requires {:layer 1} x_in != MapConst(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "1"} x: [int]bool; - tid_out := tid_in; - x := x_in; - - call SetG(1); - - call Yield(); - - call SetG(2); -} - -yield procedure {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) -requires {:layer 1} y_in != MapConst(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "2"} y: [int]bool; - tid_out := tid_in; - y := y_in; - - call SetH(1); - - call Yield(); - - call SetH(2); -} - -yield invariant {:layer 1} Yield_g({:linear "1"} x: [int]bool); -invariant x == MapConst(true); -invariant g == 0; - -yield invariant {:layer 1} Yield_h({:linear "2"} y: [int]bool); -invariant y == MapConst(true); -invariant h == 0; - -yield invariant {:layer 1} Yield(); diff --git a/Test/civl/regression-tests/perm2.bpl.expect b/Test/civl/regression-tests/perm2.bpl.expect deleted file mode 100644 index 3e6d423af..000000000 --- a/Test/civl/regression-tests/perm2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/civl/regression-tests/perm4.bpl b/Test/civl/regression-tests/perm4.bpl deleted file mode 100644 index 79b479afa..000000000 --- a/Test/civl/regression-tests/perm4.bpl +++ /dev/null @@ -1,91 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type {:linear "tid", "1", "2"} X = int; -var {:layer 0,1} g: int; -var {:layer 0,1} h: int; - -var {:layer 0,1}{:linear "tid"} unallocated:[int]bool; - -atomic action {:layer 1} AtomicSetG(val:int) -modifies g; -{ g := val; } - -yield procedure {:layer 0} SetG(val:int); -refines AtomicSetG; - -atomic action {:layer 1} AtomicSetH(val:int) -modifies h; -{ h := val; } - -yield procedure {:layer 0} SetH(val:int); -refines AtomicSetH; - -yield invariant {:layer 1} Yield({:linear "1"} x: [int]bool); -invariant x == MapConst(true) && g == 0; - -yield procedure {:layer 1} Allocate() returns ({:linear "tid"} xl: int) -ensures {:layer 1} xl != 0; -{ - call xl := AllocateLow(); -} - -atomic action {:layer 1} AtomicAllocateLow() returns ({:linear "tid"} xls: int) -modifies unallocated; -{ assume xls != 0 && unallocated[xls]; unallocated[xls] := false; } - -yield procedure {:layer 0} AllocateLow() returns ({:linear "tid"} xls: int); -refines AtomicAllocateLow; - -yield procedure {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) -requires {:layer 1} x == MapConst(true); -requires {:layer 1} y == MapConst(true); -{ - var {:linear "tid"} tid_child: int; - tid_out := tid_in; - - call SetG(0); - - par tid_child := Allocate() | Yield(x); - - async call B(tid_child, x); - - call Yield_g(x); - - call SetH(0); - - call Yield_h(y); - - call tid_child := Allocate(); - async call C(tid_child, y); -} - -yield procedure {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) -requires {:layer 1} x_in != MapConst(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "1"} x: [int]bool; - tid_out := tid_in; - x := x_in; - - call SetG(1); -} - -yield procedure {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) -requires {:layer 1} y_in != MapConst(false); -{ - var {:linear "tid"} tid_out: int; - var {:linear "2"} y: [int]bool; - tid_out := tid_in; - y := y_in; - - call SetH(1); -} - -yield invariant {:layer 1} Yield_g(x: [int]bool); -invariant x == MapConst(true); -invariant g == 0; - -yield invariant {:layer 1} Yield_h({:linear "2"} y: [int]bool); -invariant y == MapConst(true); -invariant h == 0; diff --git a/Test/civl/regression-tests/perm4.bpl.expect b/Test/civl/regression-tests/perm4.bpl.expect deleted file mode 100644 index 1b9cf6ab2..000000000 --- a/Test/civl/regression-tests/perm4.bpl.expect +++ /dev/null @@ -1,6 +0,0 @@ -perm4.bpl(87,1): Error: Non-interference check failed -Execution trace: - perm4.bpl(68,13): anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L - -Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/regression-tests/qelim1.bpl b/Test/civl/regression-tests/qelim1.bpl new file mode 100644 index 000000000..739dc5c19 --- /dev/null +++ b/Test/civl/regression-tests/qelim1.bpl @@ -0,0 +1,14 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +atomic action {:layer 2} AtomicFoo() returns (o: int) +{ + var y: int; + o := y; +} +yield procedure {:layer 1} Foo() returns (o: int) +refines AtomicFoo; +{ + var x: int; + o := x; +} \ No newline at end of file diff --git a/Test/civl/regression-tests/qelim1.bpl.expect b/Test/civl/regression-tests/qelim1.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/civl/regression-tests/qelim1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/samples/GC.bpl b/Test/civl/samples/GC.bpl index 5649be258..105d26ee5 100644 --- a/Test/civl/samples/GC.bpl +++ b/Test/civl/samples/GC.bpl @@ -72,29 +72,30 @@ function {:inline} Gray(i:int) returns(bool) { i == 2 } function {:inline} Black(i:int) returns(bool) { i >= 3 } // Top layer -var {:layer 99,101} rootAbs:[idx]obj; -var {:layer 0,101} allocSet:[obj]bool; -var {:layer 99,101} memAbs:[obj][fld]obj; +var {:layer 99,101} rootAbs: [idx]obj; +var {:layer 99,101} allocSet: [obj]bool; +var {:layer 99,101} memAbs: [obj][fld]obj; // Next layer -var {:layer 0,100} root:[idx]int; -var {:layer 0,100} mem:[int][fld]int; -var {:layer 95,100} toAbs:[int]obj; // ghost variable -var {:layer 0,100} Color:[int]int; +var {:layer 0,100} root: [idx]int; +var {:layer 0,100} mem: [int][fld]int; +var {:layer 95,100} toAbs: [int]obj; +var {:layer 0,100} Color: [int]int; var {:layer 0,100} collectorPhase: int; -var {:layer 0,100} mutatorPhase:[X]int; +var {:layer 0,100} mutatorPhase: [X]int; var {:layer 0,100} sweepPtr: int; // Next layer var {:layer 0,99} rootScanOn: bool; var {:layer 0,99} rootScanBarrier: int; -var {:linear "tid"} {:layer 0,99} mutatorsInRootScanBarrier:[int]bool; // ghost variable -var {:layer 0,98} MarkStack:[int]int; -var {:layer 0,98} MarkStackPtr:int; +var {:linear "tid"} {:layer 95,99} mutatorsInRootScanBarrier: [int]bool; +var {:layer 0,98} MarkStack: [int]int; +var {:layer 0,98} MarkStackPtr: int; // Next layer -// Lock is used during allocation, GC. To ensure good performance, it is not used for mutator reads and writes. -var {:layer 0,96} lock:int; // 0 if unheld; thread number of holder if held +// Lock is used during allocation and GC. To ensure good performance, it is not used for mutator reads and writes. +var {:layer 95,96} absLock: int; // 0 if unheld; thread number of holder if held +var {:layer 0,95} lock: bool; // false if unheld; true if held function tidHasLock(tid:Tid, lock:int):bool { (tid == GcTid || mutatorTid(tid)) && lock == tid->i && tid->left } @@ -202,7 +203,7 @@ yield invariant {:layer 100} Yield_SweepPtr_100({:linear "tid"} tid:Tid, tick_sw invariant tid == GcTid; invariant tick_sweepPtr == sweepPtr; -yield invariant {:layer 100} YieldMarkBegin({:linear "tid"} tid:Tid, tick_Color: [int]int); +yield invariant {:layer 100} Yield_MarkBegin({:linear "tid"} tid:Tid, tick_Color: [int]int); invariant tid == GcTid; invariant MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase) && sweepPtr == memHi; invariant (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x]))); @@ -210,14 +211,14 @@ invariant (forall x: int :: memAddr(x) ==> !Black(Color[x])); invariant (forall x: int :: memAddr(x) && !Unalloc(tick_Color[x]) ==> !Unalloc(Color[x])); invariant (forall x: int :: memAddr(x) && !Unalloc(tick_Color[x]) && !White(tick_Color[x]) ==> !White(Color[x])); -yield invariant {:layer 100} YieldMark({:linear "tid"} tid:Tid, tick_Color: [int]int); +yield invariant {:layer 100} Yield_Mark({:linear "tid"} tid:Tid, tick_Color: [int]int); invariant tid == GcTid; invariant MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase) && sweepPtr == memLo; invariant MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); invariant (forall x: int :: memAddr(x) && !Unalloc(tick_Color[x]) ==> !Unalloc(Color[x])); invariant (forall x: int :: memAddr(x) && !Unalloc(tick_Color[x]) && !White(tick_Color[x]) ==> !White(Color[x])); -yield invariant {:layer 100} YieldMarkEnd({:linear "tid"} tid:Tid); +yield invariant {:layer 100} Yield_MarkEnd({:linear "tid"} tid:Tid); invariant tid == GcTid; invariant MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase) && sweepPtr == memLo; invariant MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); @@ -232,7 +233,7 @@ invariant MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); invariant !Unalloc(Color[nodeProcessed]); invariant (forall x: int :: 0 <= x && x < fldIter && memAddr(mem[nodeProcessed][x]) ==> !Unalloc(Color[mem[nodeProcessed][x]]) && !White(Color[mem[nodeProcessed][x]])); -yield invariant {:layer 100} YieldSweepBegin({:linear "tid"} tid:Tid, isInit: bool, tick_Color: [int]int); +yield invariant {:layer 100} Yield_SweepBegin({:linear "tid"} tid:Tid, isInit: bool, tick_Color: [int]int); invariant tid == GcTid; invariant SweepPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); invariant sweepPtr == memLo; @@ -241,7 +242,7 @@ invariant isInit ==> SweepInvInit(root, rootAbs, mem, memAbs, Color, toAbs, allo invariant (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]])); invariant (forall x: int :: memAddr(x) && !Unalloc(tick_Color[x]) ==> tick_Color[x] == Color[x]); -yield invariant {:layer 100} YieldSweepEnd({:linear "tid"} tid:Tid); +yield invariant {:layer 100} Yield_SweepEnd({:linear "tid"} tid:Tid); invariant tid == GcTid; invariant SweepPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); invariant sweepPtr == memHi; @@ -253,20 +254,21 @@ invariant gcAndMutatorTids(tid, mutatorTids); invariant (forall x: idx :: rootAddr(x) ==> rootAbs[x] == Int(0)); yield procedure {:layer 100} -Initialize({:linear_in "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +Initialize({:layer 95, 100} {:linear_in "tid"} tid:Tid, {:layer 95, 100} {:linear "tid"} mutatorTids:[int]bool) requires {:layer 97,98,99} gcAndMutatorTids(tid, mutatorTids); requires call Yield_Initialize_100(tid, mutatorTids); requires call Yield_InitVars99(mutatorTids, MapConst(false) : [int]bool, old(rootScanBarrier)); +requires call Yield_Lock(); ensures call Yield_Iso(); ensures call Yield_RootScanBarrierInv(); ensures call Yield_InitVars99(mutatorTids, MapConst(false) : [int]bool, numMutators); { - call InitVars99(tid, mutatorTids); - call InitVars100(tid, mutatorTids); + par InitVars99(tid, mutatorTids) | Yield_Lock(); + par InitVars100(tid, mutatorTids) | Yield_Lock(); async call GarbageCollect(tid); } -atomic action {:layer 101} AtomicAlloc({:linear "tid"} tid:Tid, y:idx) +atomic action {:layer 101} AtomicAlloc({:linear "tid"} tid:Tid, i: int, y:idx) modifies allocSet, rootAbs, memAbs; { var o: obj; @@ -278,37 +280,41 @@ modifies allocSet, rootAbs, memAbs; } yield procedure {:layer 100} -Alloc({:linear "tid"} tid:Tid, y:idx) +Alloc({:layer 95, 100} {:linear "tid"} tid:Tid, i: int, y:idx) refines AtomicAlloc; requires {:layer 95,96,99,100} mutatorTidWhole(tid); preserves call Yield_Iso(); requires call Yield_RootScanBarrierEnter(tid); requires call Yield_RootScanBarrierInv(); +preserves call Yield_Lock(); +requires {:layer 96} tid->i == i; { var ptr: int; var absPtr: obj; - call TestRootScanBarrier(tid); - call Yield_Iso(); - call UpdateMutatorPhase(tid); - call Yield_Iso(); - call ptr, absPtr := AllocRaw(tid, y); + par TestRootScanBarrier(tid) | Yield_Lock(); + par Yield_Iso(); + call UpdateMutatorPhase(tid, i); + par Yield_Iso(); + par ptr, absPtr := AllocRaw(tid, y) | Yield_Lock(); assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); } -atomic action {:layer 101} AtomicWriteField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) // x.f = y +atomic action {:layer 101} AtomicWriteField({:linear "tid"} tid:Tid, i: int, x: idx, f: fld, y: idx) // x.f = y modifies memAbs; { assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]); memAbs[rootAbs[x]][f] := rootAbs[y]; } yield procedure {:layer 100} -WriteField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) +WriteField({:layer 95, 100} {:linear "tid"} tid:Tid, i: int, x: idx, f: fld, y: idx) refines AtomicWriteField; requires {:layer 98, 100} mutatorTidWhole(tid); preserves call Yield_Iso(); +preserves call Yield_Lock(); +requires {:layer 95, 96, 99} tid->i == i; { - call WriteBarrier(tid, y); + call WriteBarrier(tid, i, y); par Yield_Iso() | Yield_WriteField(tid, x, y); - call WriteFieldRaw(tid, x, f, y); + par WriteFieldRaw(tid, x, f, y) | Yield_Lock(); } atomic action {:layer 101} AtomicReadField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) // y = x.f @@ -316,7 +322,7 @@ modifies rootAbs; { assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]); rootAbs[y] := memAbs[rootAbs[x]][f]; } yield procedure {:layer 100} -ReadField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) +ReadField({:layer 95, 100} {:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) refines AtomicReadField; preserves call Yield_Iso(); { @@ -327,7 +333,7 @@ atomic action {:layer 101} AtomicEq({:linear "tid"} tid:Tid, x: idx, y:idx) retu { assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && rootAddr(y) && tidOwns(tid, y); isEqual := rootAbs[x] == rootAbs[y]; } yield procedure {:layer 100} -Eq({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool) +Eq({:layer 95, 100} {:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool) refines AtomicEq; preserves call Yield_Iso(); { @@ -335,7 +341,7 @@ preserves call Yield_Iso(); } yield procedure {:layer 100} -GarbageCollect({:linear "tid"} tid:Tid) +GarbageCollect({:layer 95, 100} {:linear "tid"} tid:Tid) requires {:layer 97,98,99,100} tid == GcTid; requires call Yield_Iso(); requires call Yield_MsWellFormed(tid, 0); @@ -343,60 +349,64 @@ requires call Yield_RootScanBarrierInv(); requires call Yield_GarbageCollect_100(tid); requires call Yield_CollectorPhase_100(tid, IDLE()); requires call Yield_SweepPtr_100(tid, memHi); +requires call Yield_Lock(); { var nextPhase: int; while (*) - invariant {:yields} true; - invariant call Yield_Iso(); - invariant call Yield_MsWellFormed(tid, 0); - invariant call Yield_RootScanBarrierInv(); - invariant call Yield_GarbageCollect_100(tid); - invariant call Yield_CollectorPhase_100(tid, IDLE()); - invariant call Yield_SweepPtr_100(tid, memHi); + invariant {:yields} true; + invariant call Yield_Iso(); + invariant call Yield_MsWellFormed(tid, 0); + invariant call Yield_RootScanBarrierInv(); + invariant call Yield_GarbageCollect_100(tid); + invariant call Yield_CollectorPhase_100(tid, IDLE()); + invariant call Yield_SweepPtr_100(tid, memHi); + invariant call Yield_Lock(); { call nextPhase := HandshakeCollector(tid); // IDLE --> MARK - par YieldWaitForMutators(tid, collectorPhase, false, 0) | + par Yield_WaitForMutators(tid, collectorPhase, false, 0) | Yield_Iso() | Yield_MsWellFormed(tid, 0) | Yield_RootScanBarrierInv() | Yield_GarbageCollect_100(tid) | Yield_CollectorPhase_100(tid, collectorPhase) | Yield_SweepPtr_100(tid, sweepPtr); - call WaitForMutators(tid, nextPhase); + par WaitForMutators(tid, nextPhase) | Yield_Lock(); call MarkOuterLoop(tid); call nextPhase := HandshakeCollector(tid); // MARK --> SWEEP - par YieldWaitForMutators(tid, collectorPhase, false, 0) | + par Yield_WaitForMutators(tid, collectorPhase, false, 0) | Yield_Iso() | Yield_MsWellFormed(tid, 0) | Yield_RootScanBarrierInv() | Yield_GarbageCollect_100(tid) | Yield_CollectorPhase_100(tid, collectorPhase) | Yield_SweepPtr_100(tid, sweepPtr); - call WaitForMutators(tid, nextPhase); + par WaitForMutators(tid, nextPhase) | Yield_Lock(); call Sweep(tid); call nextPhase := HandshakeCollector(tid); // SWEEP --> IDLE } } yield procedure {:layer 100} -MarkOuterLoop({:linear "tid"} tid:Tid) +MarkOuterLoop({:layer 95, 100} {:linear "tid"} tid:Tid) preserves call Yield_Iso(); -requires call YieldMarkBegin(tid, old(Color)); -ensures call YieldMarkEnd(tid); +requires call Yield_MarkBegin(tid, old(Color)); +ensures call Yield_MarkEnd(tid); preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); preserves call Yield_RootScanBarrierInv(); +preserves call Yield_Lock(); { var canStop: bool; call ResetSweepPtr(tid); while (true) - invariant {:yields} true; - invariant call YieldMark(tid, old(Color)); - invariant call Yield_MsWellFormed(tid, 0); - invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); - invariant call Yield_RootScanBarrierInv(); + invariant {:yields} true; + invariant call Yield_Mark(tid, old(Color)); + invariant call Yield_MsWellFormed(tid, 0); + invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); + invariant call Yield_RootScanBarrierInv(); + invariant call Yield_Lock(); { call canStop := CanMarkStop(tid); if (canStop) @@ -408,12 +418,13 @@ preserves call Yield_RootScanBarrierInv(); } yield procedure {:layer 100} -MarkInnerLoop({:linear "tid"} tid:Tid) +MarkInnerLoop({:layer 95, 100} {:linear "tid"} tid:Tid) preserves call Yield_Iso(); -preserves call YieldMark(tid, old(Color)); +preserves call Yield_Mark(tid, old(Color)); preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); preserves call Yield_RootScanBarrierInv(); +preserves call Yield_Lock(); { var nodeProcessed:int; var fldIter: int; @@ -421,62 +432,66 @@ preserves call Yield_RootScanBarrierInv(); var child: int; while (true) - invariant {:yields} true; - invariant call YieldMark(tid, old(Color)); - invariant call Yield_MsWellFormed(tid, 0); - invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); - invariant call Yield_RootScanBarrierInv(); + invariant {:yields} true; + invariant call Yield_Mark(tid, old(Color)); + invariant call Yield_MsWellFormed(tid, 0); + invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); + invariant call Yield_RootScanBarrierInv(); + invariant call Yield_Lock(); { - call isEmpty, nodeProcessed := SET_Peek(tid); + call isEmpty, nodeProcessed := RemoveFromStack(tid); if (isEmpty) { break; } fldIter := 0; while (fldIter < numFields) - invariant {:yields} true; - invariant call YieldMark(tid, old(Color)); - invariant call Yield_MsWellFormed(tid, nodeProcessed); - invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); - invariant call Yield_RootScanBarrierInv(); - invariant call Yield_MarkInnerLoopFieldIter(tid, fldIter, nodeProcessed); + invariant {:yields} true; + invariant call Yield_Mark(tid, old(Color)); + invariant call Yield_MsWellFormed(tid, nodeProcessed); + invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); + invariant call Yield_RootScanBarrierInv(); + invariant call Yield_MarkInnerLoopFieldIter(tid, fldIter, nodeProcessed); + invariant call Yield_Lock(); { - call child := ReadFieldCollector(tid, nodeProcessed, fldIter); + par child := ReadFieldByCollector(tid, nodeProcessed, fldIter) | Yield_Lock(); if (memAddr(child)) { - call SET_InsertIntoSetIfWhite(tid, nodeProcessed, child); + call InsertIntoSetIfWhiteByCollector(tid, nodeProcessed, child); } fldIter := fldIter + 1; } - call SET_RemoveFromSet(tid, nodeProcessed); + call SetColorToBlack(tid, nodeProcessed); } } yield procedure {:layer 100} -Sweep({:linear "tid"} tid:Tid) +Sweep({:layer 95, 100} {:linear "tid"} tid:Tid) requires {:layer 98,99,100} tid == GcTid; preserves call Yield_Iso(); preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_RootScanBarrierInv(); -requires call YieldSweepBegin(tid, false, old(Color)); -ensures call YieldSweepEnd(tid); +requires call Yield_SweepBegin(tid, false, old(Color)); +ensures call Yield_SweepEnd(tid); +preserves call Yield_Lock(); { var localSweepPtr: int; var {:layer 100} snapColor: [int]int; localSweepPtr := memLo; call ClearToAbsWhite(tid); - par YieldSweepBegin(tid, true, Color) | Yield_MsWellFormed(tid, 0) | Yield_RootScanBarrierInv() | Yield_Iso(); + par Yield_SweepBegin(tid, true, Color) | Yield_MsWellFormed(tid, 0) | Yield_RootScanBarrierInv() | Yield_Iso(); call {:layer 100} snapColor := Copy(Color); while (localSweepPtr < memHi) - invariant {:yields} {:layer 96} true; - invariant {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0); - invariant {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); - invariant {:layer 100} SweepPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); - invariant {:layer 100} localSweepPtr == sweepPtr && memLo <= sweepPtr && sweepPtr <= memHi; - invariant {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(snapColor[root[i]])); - invariant {:layer 100} SweepInvInit(root, rootAbs, mem, memAbs, snapColor, toAbs, allocSet); - invariant {:layer 100} (forall i:int:: memAddr(i) ==> if sweepPtr <= i then Color[i] == snapColor[i] else if Black(snapColor[i]) then White(Color[i]) else Unalloc(Color[i])); + invariant {:yields} {:layer 96} true; + invariant {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0); + invariant {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); + invariant {:layer 100} SweepPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); + invariant {:layer 100} localSweepPtr == sweepPtr && memLo <= sweepPtr && sweepPtr <= memHi; + invariant {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(snapColor[root[i]])); + invariant {:layer 100} SweepInvInit(root, rootAbs, mem, memAbs, snapColor, toAbs, allocSet); + invariant {:layer 100} (forall i:int:: memAddr(i) ==> if sweepPtr <= i then Color[i] == snapColor[i] else if Black(snapColor[i]) then White(Color[i]) else Unalloc(Color[i])); + invariant call Yield_Lock(); { call SweepNext(tid); localSweepPtr := localSweepPtr + 1; @@ -516,7 +531,7 @@ invariant mutatorTidLeft(tid); invariant mutatorsInRootScanBarrier[tid->i]; yield procedure {:layer 99} -InitVars99({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +InitVars99({:layer 95, 99} {:linear "tid"} tid:Tid, {:layer 95, 99} {:linear "tid"} mutatorTids:[int]bool) requires {:layer 98,99} gcAndMutatorTids(tid, mutatorTids); ensures call Yield_InitVars98(tid, mutatorTids, 0); requires call Yield_InitVars99(mutatorTids, old(mutatorsInRootScanBarrier), old(rootScanBarrier)); @@ -527,15 +542,16 @@ ensures call Yield_InitVars99(mutatorTids, old(mutatorsInRootScanBarrier), numMu } yield procedure {:layer 99} -TestRootScanBarrier({:linear "tid"} tid:Tid) +TestRootScanBarrier({:layer 95, 99} {:linear "tid"} tid:Tid) requires {:layer 95,96} mutatorTidWhole(tid); requires call Yield_RootScanBarrierEnter(tid); requires call Yield_RootScanBarrierInv(); +preserves call Yield_Lock(); { var isRootScanOn: bool; - var{:linear "tid"} tid_tmp: Tid; + var {:layer 95, 99} {:linear "tid"} tid_tmp: Tid; - call isRootScanOn := PollMutatorReadBarrierOn(tid); + par isRootScanOn := PollMutatorReadBarrierOn(tid) | Yield_Lock(); par Yield_RootScanBarrierInv() | Yield_RootScanBarrierEnter(tid) | Yield_97() | Yield_98(); if (isRootScanOn) { @@ -544,7 +560,7 @@ requires call Yield_RootScanBarrierInv(); par Yield_RootScanBarrierInv() | Yield_RootScanBarrierWait(tid_tmp) | Yield_97() | Yield_98(); assert{:layer 99} mutatorsInRootScanBarrier == mutatorsInRootScanBarrier[tid_tmp->i := true]; call tid_tmp := MutatorRootScanBarrierWait(tid_tmp); - call TidOutput(tid_tmp, tid); + call {:layer 95, 99} TidOutput(tid_tmp, tid); } } @@ -558,12 +574,13 @@ modifies Color; } yield procedure {:layer 99} -CanMarkStop({:linear "tid"} tid:Tid) returns (canStop: bool) +CanMarkStop({:layer 95, 99} {:linear "tid"} tid:Tid) returns (canStop: bool) refines AtomicCanMarkStop; requires {:layer 99} tid == GcTid; preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); preserves call Yield_RootScanBarrierInv(); +preserves call Yield_Lock(); { var i: int; var o: int; @@ -574,21 +591,22 @@ preserves call Yield_RootScanBarrierInv(); par Yield_MsWellFormed(tid, 0) | Yield_CollectorPhase_98(tid, old(collectorPhase)) | Yield_RootScanBarrierInv() | Yield_RootScanOn(tid, true) | Yield_97(); call {:layer 99} snapColor := Copy(Color); - call CollectorRootScanBarrierWait(tid); + par CollectorRootScanBarrierWait(tid) | Yield_Lock(); i := 0; while (i < numRoots) - invariant {:yields} {:layer 98} true; - invariant call Yield_MsWellFormed(tid, 0); - invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); - invariant {:layer 99} Mutators == mutatorsInRootScanBarrier && rootScanOn; - invariant {:layer 99} 0 <= i && i <= numRoots; - invariant {:layer 99} Color == (lambda u: int :: if memAddr(u) && White(snapColor[u]) && (exists k: int :: 0 <= k && k < i && root[k] == u) then GRAY() else snapColor[u]); + invariant {:yields} {:layer 98} true; + invariant call Yield_MsWellFormed(tid, 0); + invariant call Yield_CollectorPhase_98(tid, old(collectorPhase)); + invariant {:layer 99} Mutators == mutatorsInRootScanBarrier && rootScanOn; + invariant {:layer 99} 0 <= i && i <= numRoots; + invariant {:layer 99} Color == (lambda u: int :: if memAddr(u) && White(snapColor[u]) && (exists k: int :: 0 <= k && k < i && root[k] == u) then GRAY() else snapColor[u]); + invariant call Yield_Lock(); { - call o := ReadRootInRootScanBarrier(tid, i); + par o := ReadRootInRootScanBarrier(tid, i) | Yield_Lock(); if (memAddr(o)) { - call InsertIntoSetIfWhiteInRootScanBarrier(tid, o); + par InsertIntoSetIfWhiteInRootScanBarrier(tid, o) | Yield_Lock(); } i := i + 1; } @@ -604,7 +622,7 @@ modifies memAbs, mem; mem[root[x]][f] := root[y]; } -yield procedure {:layer 99} WriteFieldRaw({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) +yield procedure {:layer 99} WriteFieldRaw({:layer 95, 99} {:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) refines AtomicWriteFieldRaw; requires {:layer 98} mutatorTidWhole(tid); { @@ -613,7 +631,7 @@ requires {:layer 98} mutatorTidWhole(tid); call valx := ReadRoot(tid, x); call valy := ReadRoot(tid, y); - call WriteFieldGeneral(tid, valx, f, valy); + call WriteFieldByMutator(tid, valx, f, valy); call {:layer 99} memAbs := Copy((var a, b := rootAbs[x], rootAbs[y]; memAbs[a := memAbs[a][f := b]])); } @@ -625,14 +643,14 @@ modifies rootAbs, root; root[y] := mem[root[x]][f]; } -yield procedure {:layer 99} ReadFieldRaw({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) +yield procedure {:layer 99} ReadFieldRaw({:layer 95, 99} {:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) refines AtomicReadFieldRaw; { var valx: int; var valy: int; call valx := ReadRoot(tid, x); - call valy := ReadFieldGeneral(tid, valx, f); + call valy := ReadFieldByMutator(tid, valx, f); call WriteRoot(tid, y, valy); call {:layer 99} rootAbs := Copy((var a := rootAbs[x]; rootAbs[y := memAbs[a][f]])); } @@ -640,7 +658,7 @@ refines AtomicReadFieldRaw; atomic action {:layer 100} AtomicEqRaw({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool) { assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && rootAddr(y) && tidOwns(tid, y); isEqual := root[x] == root[y]; } -yield procedure {:layer 99} EqRaw({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool) +yield procedure {:layer 99} EqRaw({:layer 95, 99} {:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool) refines AtomicEqRaw; { var vx:int; @@ -656,8 +674,8 @@ modifies allocSet, rootAbs, root, toAbs, memAbs, Color, mem; { assert mutatorTidWhole(tid) && rootAddr(y) && tidOwns(tid, y); assert (forall x: int, f: fld :: memAddr(x) && Unalloc(Color[x]) ==> toAbs[x] == nil); - assume(memAddr(ptr) && Unalloc(Color[ptr])); - assume(memAddrAbs(absPtr) && !allocSet[absPtr] && absPtr != nil); + assume memAddr(ptr) && Unalloc(Color[ptr]); + assume memAddrAbs(absPtr) && !allocSet[absPtr] && absPtr != nil; allocSet[absPtr] := true; rootAbs[y] := absPtr; root[y] := ptr; @@ -667,17 +685,19 @@ modifies allocSet, rootAbs, root, toAbs, memAbs, Color, mem; mem[ptr] := (lambda z: int :: if (fieldAddr(z)) then ptr else mem[ptr][z]); } -yield procedure {:layer 99} AllocRaw({:linear "tid"} tid:Tid, y:idx) returns (ptr: int, absPtr: obj) +yield procedure {:layer 99} AllocRaw({:layer 95, 99} {:linear "tid"} tid:Tid, y:idx) returns (ptr: int, absPtr: obj) refines AtomicAllocRaw; +preserves call Yield_Lock(); { - call absPtr := PrimitiveFindFreePtrAbs(); + call {:layer 99} Assume(memAddrAbs(absPtr) && !allocSet[absPtr] && absPtr != nil); + call {:layer 99} allocSet := Copy(allocSet[absPtr := true]); call ptr := FindFreePtr(tid, absPtr); - call WriteRoot(tid, y, ptr); + par WriteRoot(tid, y, ptr) | Yield_Lock(); call {:layer 99} memAbs := Copy(memAbs[absPtr := (lambda z: int :: if (fieldAddr(z)) then absPtr else memAbs[absPtr][z])]); call {:layer 99} rootAbs := Copy(rootAbs[y := absPtr]); } -atomic action {:layer 100} AtomicWriteBarrier({:linear "tid"} tid:Tid, y:idx) +atomic action {:layer 100} AtomicWriteBarrier({:linear "tid"} tid:Tid, i: int, y:idx) modifies Color; { var val:int; @@ -688,20 +708,22 @@ modifies Color; } } -yield procedure {:layer 99} WriteBarrier({:linear "tid"} tid:Tid, y:idx) +yield procedure {:layer 99} WriteBarrier({:layer 95, 99} {:linear "tid"} tid:Tid, i: int, y:idx) refines AtomicWriteBarrier; requires {:layer 98} mutatorTidWhole(tid); +requires {:layer 96,99} tid->i == i; +preserves call Yield_Lock(); { var phase: int; var rootVal: int; - call rootVal := ReadRoot(tid, y); + par rootVal := ReadRoot(tid, y) | Yield_Lock(); if (memAddr(rootVal)) { - call phase := ReadMutatorPhase(tid); - if (MarkPhase(phase)) + par phase := ReadMutatorPhaseByMutator(tid, i) | Yield_Lock(); + if (MarkPhase(phase)) { - call SET_InsertIntoSetIfWhiteByMutator(tid, rootVal); + call InsertIntoSetIfWhiteByMutator(tid, rootVal); } } } @@ -733,7 +755,7 @@ invariant gcAndMutatorTids(tid, mutatorTids); invariant MarkStackPtr == tick_MarkStackPtr; yield procedure {:layer 98} -InitVars98({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +InitVars98({:layer 95, 98} {:linear "tid"} tid:Tid, {:layer 95, 98} {:linear "tid"} mutatorTids:[int]bool) requires call Yield_InitVars98(tid, mutatorTids, old(MarkStackPtr)); ensures call Yield_InitVars98(tid, mutatorTids, 0); { @@ -751,22 +773,25 @@ modifies Color, toAbs, mem; mem[ptr] := (lambda z: int :: if (fieldAddr(z)) then ptr else mem[ptr][z]); } -yield procedure {:layer 98} FindFreePtr({:linear "tid"} tid: Tid, absPtr: obj) returns (ptr: int) +yield procedure {:layer 98} FindFreePtr({:layer 95, 98} {:linear "tid"} tid: Tid, absPtr: obj) returns (ptr: int) refines AtomicFindFreePtr; +preserves call Yield_Lock(); { var iter: int; var spaceFound: bool; spaceFound := false; while (true) - invariant {:yields} true; - invariant {:layer 98} !spaceFound; + invariant {:yields} true; + invariant {:layer 98} !spaceFound; + invariant call Yield_Lock(); { iter := memLo; while (iter < memHi) - invariant {:yields} true; - invariant {:layer 98} !spaceFound; - invariant {:layer 98} memLo <= iter && iter <= memHi; + invariant {:yields} true; + invariant {:layer 98} !spaceFound; + invariant {:layer 98} memLo <= iter && iter <= memHi; + invariant call Yield_Lock(); { call spaceFound := AllocIfPtrFree(tid, iter, absPtr); if (spaceFound) @@ -782,7 +807,7 @@ refines AtomicFindFreePtr; } } -atomic action {:layer 99} AtomicSET_InsertIntoSetIfWhiteByMutator({:linear "tid"} tid:Tid, memLocal:int) +atomic action {:layer 99} AtomicInsertIntoSetIfWhiteByMutator({:linear "tid"} tid:Tid, memLocal:int) modifies Color; { assert mutatorTidWhole(tid) && memAddr(memLocal) && MarkPhase(mutatorPhase[tid->i]); @@ -792,13 +817,14 @@ modifies Color; } yield procedure {:layer 98} -SET_InsertIntoSetIfWhiteByMutator({:linear "tid"} tid:Tid, memLocal:int) -refines AtomicSET_InsertIntoSetIfWhiteByMutator; +InsertIntoSetIfWhiteByMutator({:layer 95, 98} {:linear "tid"} tid:Tid, memLocal:int) +refines AtomicInsertIntoSetIfWhiteByMutator; preserves call Yield_MarkPhase(tid, memLocal); +preserves call Yield_Lock(); { var color:int; - call color := ReadColorByMutator3(tid, memLocal); + par color := ReadColorByMutator3(tid, memLocal) | Yield_Lock(); if (!White(color)) { return; @@ -817,10 +843,11 @@ left action {:layer 99} AtomicNoGrayInRootScanBarrier({:linear "tid"} tid:Tid) r } yield procedure {:layer 98} -NoGrayInRootScanBarrier({:linear "tid"} tid:Tid) returns (noGray: bool) +NoGrayInRootScanBarrier({:layer 95, 98} {:linear "tid"} tid:Tid) returns (noGray: bool) refines AtomicNoGrayInRootScanBarrier; preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); +preserves call Yield_Lock(); { call noGray := MsIsEmpty(tid); assert {:layer 98} noGray || MST(0); @@ -836,16 +863,17 @@ modifies Color; } yield procedure {:layer 98} -InsertIntoSetIfWhiteInRootScanBarrier({:linear "tid"} tid:Tid, memLocal:int) +InsertIntoSetIfWhiteInRootScanBarrier({:layer 95, 98} {:linear "tid"} tid:Tid, memLocal:int) refines AtomicInsertIntoSetIfWhiteInRootScanBarrier; preserves call Yield_MsWellFormed(tid, 0); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); +preserves call Yield_Lock(); { call MsPushByCollector(tid, memLocal); assert {:layer 98} MST(MarkStackPtr-1); } -left action {:layer 99,100} AtomicSET_InsertIntoSetIfWhite({:linear "tid"} tid:Tid, parent: int, child:int) +left action {:layer 99,100} AtomicInsertIntoSetIfWhiteByCollector({:linear "tid"} tid:Tid, parent: int, child:int) modifies Color; { assert tid == GcTid; @@ -856,17 +884,18 @@ modifies Color; } yield procedure {:layer 98} -SET_InsertIntoSetIfWhite({:linear "tid"} tid:Tid, parent: int, child:int) -refines AtomicSET_InsertIntoSetIfWhite; +InsertIntoSetIfWhiteByCollector({:layer 95, 98} {:linear "tid"} tid:Tid, parent: int, child:int) +refines AtomicInsertIntoSetIfWhiteByCollector; requires {:layer 98} memAddr(parent) && memAddr(child); preserves call Yield_MsWellFormed(tid, parent); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); +preserves call Yield_Lock(); { call MsPushByCollector(tid, child); assert {:layer 98} MST(MarkStackPtr-1); } -right action {:layer 99,100} AtomicSET_Peek({:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) +right action {:layer 99,100} AtomicRemoveFromStack({:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) { assert tid == GcTid; assert MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); @@ -879,11 +908,12 @@ right action {:layer 99,100} AtomicSET_Peek({:linear "tid"} tid:Tid) returns (is } yield procedure {:layer 98} -SET_Peek({:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) -refines AtomicSET_Peek; +RemoveFromStack({:layer 95, 98} {:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) +refines AtomicRemoveFromStack; requires call Yield_MsWellFormed(tid, 0); ensures call Yield_MsWellFormed(tid, if isEmpty then 0 else val); preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); +preserves call Yield_Lock(); { assert {:layer 98} MST(MarkStackPtr - 1); call isEmpty, val := MsPop(tid); @@ -895,7 +925,7 @@ preserves call Yield_CollectorPhase_98(tid, old(collectorPhase)); yield invariant {:layer 97} Yield_97(); -yield invariant {:layer 97} YieldWaitForMutators({:linear "tid"} tid:Tid, nextPhase: int, done: bool, i: int); +yield invariant {:layer 97} Yield_WaitForMutators({:linear "tid"} tid:Tid, nextPhase: int, done: bool, i: int); invariant tid == GcTid; invariant nextPhase == collectorPhase; invariant done ==> (forall j:int:: 1 <= j && j < i ==> nextPhase == mutatorPhase[j]); @@ -907,26 +937,26 @@ atomic action {:layer 98,100} AtomicWaitForMutators({:linear "tid"} tid:Tid, nex } yield procedure {:layer 97} -WaitForMutators({:linear "tid"} tid:Tid, nextPhase: int) +WaitForMutators({:layer 95, 97} {:linear "tid"} tid:Tid, nextPhase: int) refines AtomicWaitForMutators; -requires call YieldWaitForMutators(tid, nextPhase, false, 0); +requires call Yield_WaitForMutators(tid, nextPhase, false, 0); { var done: bool; var i: int; var mutatorPhaseLocal: int; done := false; - call YieldWaitForMutators(tid, nextPhase, done, 1); + call Yield_WaitForMutators(tid, nextPhase, done, 1); while (!done) - invariant {:yields} true; - invariant call YieldWaitForMutators(tid, nextPhase, done, numMutators+1); + invariant {:yields} true; + invariant call Yield_WaitForMutators(tid, nextPhase, done, numMutators+1); { done := true; i := 1; - call YieldWaitForMutators(tid, nextPhase, done, i); + call Yield_WaitForMutators(tid, nextPhase, done, i); while (i <= numMutators) - invariant {:yields} true; - invariant call YieldWaitForMutators(tid, nextPhase, done, i); + invariant {:yields} true; + invariant call Yield_WaitForMutators(tid, nextPhase, done, i); { call mutatorPhaseLocal := ReadMutatorPhaseByCollector(tid, i); if (nextPhase != mutatorPhaseLocal) @@ -957,7 +987,7 @@ modifies mutatorPhase, root, toAbs, Color, mem, collectorPhase, sweepPtr; sweepPtr := memHi; } -yield procedure {:layer 96} InitVars100({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 96} InitVars100({:layer 95, 96} {:linear "tid"} tid:Tid, {:layer 95, 96} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitVars100; { var n:int; @@ -1019,7 +1049,7 @@ refines AtomicInitVars100; call InitSweepPtr(tid, mutatorTids); } -atomic action {:layer 97,100} AtomicSET_RemoveFromSet({:linear "tid"} tid:Tid, scannedLocal:int) +atomic action {:layer 97,100} AtomicSetColorToBlack({:linear "tid"} tid:Tid, scannedLocal:int) modifies Color; { assert MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase); @@ -1028,11 +1058,12 @@ modifies Color; Color[scannedLocal] := BLACK(); } -yield procedure {:layer 96} SET_RemoveFromSet({:linear "tid"} tid:Tid, scannedLocal:int) -refines AtomicSET_RemoveFromSet; +yield procedure {:layer 96} SetColorToBlack({:layer 95, 96} {:linear "tid"} tid:Tid, scannedLocal:int) +refines AtomicSetColorToBlack; +preserves call Yield_Lock(); { call LockAcquire(tid); - call SetColor2(tid, scannedLocal, BLACK()); + par SetColorInMarkPhase(tid, scannedLocal, BLACK()) | Yield_Lock(); call LockRelease(tid); } @@ -1047,21 +1078,22 @@ modifies Color, MarkStack, MarkStackPtr; } } -yield procedure {:layer 96} MsPushByCollector({:linear "tid"} tid: Tid, val: int) +yield procedure {:layer 96} MsPushByCollector({:layer 95, 96} {:linear "tid"} tid: Tid, val: int) refines AtomicMsPushByCollector; +preserves call Yield_Lock(); { var color:int; var stack:int; call LockAcquire(tid); - call color := ReadColorByCollector(tid, val); + par color := ReadColorByCollector(tid, val) | Yield_Lock(); if (White(color)) { - call SetColor2(tid, val, GRAY()); - call stack := ReadMarkStackPtr(tid); - call WriteMarkStack(tid, stack, val); + par SetColorInMarkPhase(tid, val, GRAY()) | Yield_Lock(); + par stack := ReadMarkStackPtr(tid) | Yield_Lock(); + par WriteMarkStack(tid, stack, val) | Yield_Lock(); stack := stack + 1; - call SetMarkStackPtr(tid, stack); + par SetMarkStackPtr(tid, stack) | Yield_Lock(); } call LockRelease(tid); } @@ -1077,21 +1109,22 @@ modifies Color, MarkStack, MarkStackPtr; } } -yield procedure {:layer 96} MsPushByMutator({:linear "tid"} tid: Tid, val: int) +yield procedure {:layer 96} MsPushByMutator({:layer 95, 96} {:linear "tid"} tid: Tid, val: int) refines AtomicMsPushByMutator; +preserves call Yield_Lock(); { var color:int; var stack:int; call LockAcquire(tid); - call color := ReadColorByMutator2(tid, val); + par color := ReadColorByMutator2(tid, val) | Yield_Lock(); if (White(color)) { - call SetColor2(tid, val, GRAY()); - call stack := ReadMarkStackPtr(tid); - call WriteMarkStack(tid, stack, val); + par SetColorInMarkPhase(tid, val, GRAY()) | Yield_Lock(); + par stack := ReadMarkStackPtr(tid) | Yield_Lock(); + par WriteMarkStack(tid, stack, val) | Yield_Lock(); stack := stack + 1; - call SetMarkStackPtr(tid, stack); + par SetMarkStackPtr(tid, stack) | Yield_Lock(); } call LockRelease(tid); } @@ -1110,18 +1143,19 @@ modifies MarkStackPtr; } } -yield procedure {:layer 96} MsPop({:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) +yield procedure {:layer 96} MsPop({:layer 95, 96} {:linear "tid"} tid:Tid) returns (isEmpty: bool, val:int) refines AtomicMsPop; +preserves call Yield_Lock(); { var stack:int; call LockAcquire(tid); - call stack := ReadMarkStackPtr(tid); + par stack := ReadMarkStackPtr(tid) | Yield_Lock(); if (stack > 0) { stack := stack - 1; - call SetMarkStackPtr(tid, stack); - call val := ReadMarkStack(tid, stack); + par SetMarkStackPtr(tid, stack) | Yield_Lock(); + par val := ReadMarkStack(tid, stack) | Yield_Lock(); isEmpty := false; } else @@ -1135,13 +1169,14 @@ refines AtomicMsPop; atomic action {:layer 97,98} AtomicMsIsEmpty({:linear "tid"} tid: Tid) returns (isEmpty: bool) { assert tid == GcTid; isEmpty := MarkStackPtr == 0; } -yield procedure {:layer 96} MsIsEmpty({:linear "tid"} tid: Tid) returns (isEmpty: bool) +yield procedure {:layer 96} MsIsEmpty({:layer 95, 96} {:linear "tid"} tid: Tid) returns (isEmpty: bool) refines AtomicMsIsEmpty; +preserves call Yield_Lock(); { var v:int; call LockAcquire(tid); - call v := ReadMarkStackPtr(tid); + par v := ReadMarkStackPtr(tid) | Yield_Lock(); isEmpty := v == 0; call LockRelease(tid); } @@ -1150,11 +1185,12 @@ atomic action {:layer 97,100} AtomicResetSweepPtr({:linear "tid"} tid:Tid) modifies sweepPtr; { assert tid == GcTid; sweepPtr := memLo; } -yield procedure {:layer 96} ResetSweepPtr({:linear "tid"} tid:Tid) +yield procedure {:layer 96} ResetSweepPtr({:layer 95, 96} {:linear "tid"} tid:Tid) refines AtomicResetSweepPtr; +preserves call Yield_Lock(); { call LockAcquire(tid); - call SetSweepPtrLocked(tid, memLo); + par SetSweepPtrLocked(tid, memLo) | Yield_Lock(); call LockRelease(tid); } @@ -1169,19 +1205,20 @@ modifies Color, sweepPtr; sweepPtr := sweepPtr + 1; } -yield procedure {:layer 96} SweepNext({:linear "tid"} tid:Tid) +yield procedure {:layer 96} SweepNext({:layer 95, 96} {:linear "tid"} tid:Tid) refines AtomicSweepNext; +preserves call Yield_Lock(); { var color:int; var sweep:int; call LockAcquire(tid); - call sweep := ReadSweepPtr(tid); - call color := ReadColorByCollector(tid, sweep); + par sweep := ReadSweepPtr(tid) | Yield_Lock(); + par color := ReadColorByCollector(tid, sweep) | Yield_Lock(); color := if White(color) then UNALLOC() else if Black(color) then WHITE() else color; - call SetColor(tid, sweep, color); + par SetColor(tid, sweep, color) | Yield_Lock(); sweep := sweep + 1; - call SetSweepPtrLocked(tid, sweep); + par SetSweepPtrLocked(tid, sweep) | Yield_Lock(); call LockRelease(tid); } @@ -1202,30 +1239,33 @@ modifies collectorPhase; } } -yield procedure {:layer 96} HandshakeCollector({:linear "tid"} tid:Tid) returns (nextPhase: int) +yield procedure {:layer 96} HandshakeCollector({:layer 95, 96} {:linear "tid"} tid:Tid) returns (nextPhase: int) refines AtomicHandshakeCollector; +preserves call Yield_Lock(); { var phase:int; call LockAcquire(tid); - call phase := ReadCollectorPhase(tid); + par phase := ReadCollectorPhase(tid) | Yield_Lock(); nextPhase := if IdlePhase(phase) then MARK() else if MarkPhase(phase) then SWEEP() else IDLE(); - call SetCollectorPhase(tid, nextPhase); + par SetCollectorPhase(tid, nextPhase) | Yield_Lock(); call LockRelease(tid); } -atomic action {:layer 97,100} AtomicUpdateMutatorPhase({:linear "tid"} tid: Tid) +atomic action {:layer 97,100} AtomicUpdateMutatorPhase({:linear "tid"} tid: Tid, i: int) modifies mutatorPhase; { assert mutatorTidWhole(tid); mutatorPhase[tid->i] := collectorPhase; } -yield procedure {:layer 96} UpdateMutatorPhase({:linear "tid"} tid: Tid) +yield procedure {:layer 96} UpdateMutatorPhase({:layer 95, 96} {:linear "tid"} tid: Tid, i: int) refines AtomicUpdateMutatorPhase; +preserves call Yield_Lock(); +requires {:layer 96} tid->i == i; { var p:int; call LockAcquire(tid); - call p := ReadCollectorPhaseLocked(tid); - call SetMutatorPhaseLocked(tid, p); + par p := ReadCollectorPhaseLocked(tid) | Yield_Lock(); + par SetMutatorPhaseLocked(tid, i, p) | Yield_Lock(); call LockRelease(tid); } @@ -1233,11 +1273,12 @@ atomic action {:layer 97,99} AtomicCollectorRootScanBarrierStart({:linear "tid"} modifies rootScanOn; { assert tid == GcTid; rootScanOn := true; } -yield procedure {:layer 96} CollectorRootScanBarrierStart({:linear "tid"} tid: Tid) +yield procedure {:layer 96} CollectorRootScanBarrierStart({:layer 95, 96} {:linear "tid"} tid: Tid) refines AtomicCollectorRootScanBarrierStart; +preserves call Yield_Lock(); { call LockAcquire(tid); - call CollectorRootScanBarrierStartLocked(tid); + par CollectorRootScanBarrierStartLocked(tid) | Yield_Lock(); call LockRelease(tid); } @@ -1245,24 +1286,25 @@ left action {:layer 97,99} AtomicCollectorRootScanBarrierEnd({:linear "tid"} tid modifies rootScanOn; { assert tid == GcTid; rootScanOn := false; } -yield procedure {:layer 96} CollectorRootScanBarrierEnd({:linear "tid"} tid: Tid) +yield procedure {:layer 96} CollectorRootScanBarrierEnd({:layer 95, 96} {:linear "tid"} tid: Tid) refines AtomicCollectorRootScanBarrierEnd; +preserves call Yield_Lock(); { call LockAcquire(tid); - call CollectorRootScanBarrierEndLocked(tid); + par CollectorRootScanBarrierEndLocked(tid) | Yield_Lock(); call LockRelease(tid); } atomic action {:layer 97,99} AtomicCollectorRootScanBarrierWait({:linear "tid"} tid: Tid) { assert tid == GcTid; assume rootScanBarrier == 0; } -yield procedure {:layer 96} CollectorRootScanBarrierWait({:linear "tid"} tid: Tid) +yield procedure {:layer 96} CollectorRootScanBarrierWait({:layer 95, 96} {:linear "tid"} tid: Tid) refines AtomicCollectorRootScanBarrierWait; { var v:int; while (true) - invariant {:yields} true; + invariant {:yields} true; { call v := CollectorRootScanBarrierRead(tid); if (v == 0) @@ -1281,17 +1323,18 @@ modifies rootScanBarrier, mutatorsInRootScanBarrier; tid_left := Tid(tid->i, true, false); } -yield procedure {:layer 96} MutatorRootScanBarrierEnter({:linear_in "tid"} tid: Tid) returns({:linear "tid"} tid_left: Tid) +yield procedure {:layer 96} MutatorRootScanBarrierEnter({:layer 95, 96} {:linear_in "tid"} tid: Tid) returns({:layer 95, 96} {:linear "tid"} tid_left: Tid) refines AtomicMutatorRootScanBarrierEnter; requires {:layer 95} mutatorTidWhole(tid); ensures {:layer 95,96} tid_left->i == tid->i && tid_left->left; +preserves call Yield_Lock(); { - var{:linear "tid"} tid_right: Tid; + var {:layer 95, 96} {:linear "tid"} tid_right: Tid; - call tid_left, tid_right := TidSplit(tid); + call {:layer 95, 96} tid_left, tid_right := TidSplit(tid); call LockAcquire(tid_left); - call MutatorsInRootScanBarrierAdd(tid_left, tid_right); - call AddRootScanBarrier(tid_left, -1); + par MutatorsInRootScanBarrierAdd(tid_left, tid_right) | Yield_Lock(); + par AddRootScanBarrier(tid_left, -1) | Yield_Lock(); call LockRelease(tid_left); } @@ -1305,23 +1348,25 @@ modifies rootScanBarrier, mutatorsInRootScanBarrier; tid := Tid(tid_left->i, true, true); } -yield procedure {:layer 96} MutatorRootScanBarrierWait({:linear_in "tid"} tid_left: Tid) returns({:linear "tid"} tid: Tid) +yield procedure {:layer 96} MutatorRootScanBarrierWait({:layer 95, 96} {:linear_in "tid"} tid_left: Tid) returns({:layer 95, 96} {:linear "tid"} tid: Tid) refines AtomicMutatorRootScanBarrierWait; ensures {:layer 95,96} tid->i == tid_left->i && tid->left && tid->right; +preserves call Yield_Lock(); { - var{:linear "tid"} tid_right: Tid; - var b:bool; + var {:layer 95, 96} {:linear "tid"} tid_right: Tid; + var b: bool; loop: assert {:yields} {:layer 96} true; + call Yield_Lock(); call LockAcquire(tid_left); - call b := MutatorReadBarrierOn(tid_left); + par b := MutatorReadBarrierOn(tid_left) | Yield_Lock(); if (!b) { - call AddRootScanBarrier(tid_left, 1); - call tid_right := MutatorsInRootScanBarrierRemove(tid_left); + par AddRootScanBarrier(tid_left, 1) | Yield_Lock(); + par tid_right := MutatorsInRootScanBarrierRemove(tid_left) | Yield_Lock(); call LockRelease(tid_left); - call tid := TidCombine(tid_left, tid_right); + call {:layer 95, 96} tid := TidCombine(tid_left, tid_right); return; } call LockRelease(tid_left); @@ -1343,8 +1388,9 @@ modifies Color, toAbs, mem; } } -yield procedure {:layer 96} AllocIfPtrFree({:linear "tid"} tid:Tid, ptr:int, absPtr:obj) returns (spaceFound:bool) +yield procedure {:layer 96} AllocIfPtrFree({:layer 95, 96} {:linear "tid"} tid:Tid, ptr:int, absPtr:obj) returns (spaceFound:bool) refines AtomicAllocIfPtrFree; +preserves call Yield_Lock(); { var color:int; var sweep:int; @@ -1352,16 +1398,16 @@ refines AtomicAllocIfPtrFree; var fldIter:fld; var {:layer 96} snapMem: [int][fld]int; - call color := ReadColorByMutator1(tid, ptr); + par color := ReadColorByMutator1(tid, ptr) | Yield_Lock(); if (Unalloc(color)) { - call Yield(); + call Yield_96(); call LockAcquire(tid); - call color := ReadColorByMutator2(tid, ptr); + par color := ReadColorByMutator2(tid, ptr) | Yield_Lock(); if (Unalloc(color)) { spaceFound := true; - call sweep := ReadSweepPtr(tid); + par sweep := ReadSweepPtr(tid) | Yield_Lock(); if (sweep <= ptr) { color := BLACK(); @@ -1374,15 +1420,16 @@ refines AtomicAllocIfPtrFree; call {:layer 96} snapMem := Copy(mem); fldIter := 0; while (fldIter < numFields) - invariant {:yields} {:layer 95} true; - invariant {:layer 96} 0 <= fldIter && fldIter <= numFields; - invariant {:layer 96} mem == snapMem[ptr := (lambda z: int :: if (0 <= z && z < fldIter) then ptr else snapMem[ptr][z])]; + invariant {:yields} {:layer 95} true; + invariant {:layer 96} 0 <= fldIter && fldIter <= numFields; + invariant {:layer 96} mem == snapMem[ptr := (lambda z: int :: if (0 <= z && z < fldIter) then ptr else snapMem[ptr][z])]; + invariant call Yield_Lock(); { - call InitializeFieldInAlloc(tid, ptr, fldIter); + par InitializeFieldInAlloc(tid, ptr, fldIter) | Yield_Lock(); fldIter := fldIter + 1; } - call SetColor3(tid, ptr, color, absPtr); + par SetColorInAlloc(tid, ptr, color, absPtr) | Yield_Lock(); call LockRelease(tid); return; } @@ -1394,13 +1441,14 @@ refines AtomicAllocIfPtrFree; atomic action {:layer 97,100} AtomicIsWhiteByCollector({:linear "tid"} tid:Tid, i: int) returns (isWhite: bool) { assert tid == GcTid && memAddr(i); isWhite := White(Color[i]); } -yield procedure {:layer 96} IsWhiteByCollector({:linear "tid"} tid:Tid, i: int) returns (isWhite: bool) +yield procedure {:layer 96} IsWhiteByCollector({:layer 95, 96} {:linear "tid"} tid:Tid, i: int) returns (isWhite: bool) refines AtomicIsWhiteByCollector; +preserves call Yield_Lock(); { var v:int; call LockAcquire(tid); - call v := ReadColorByCollector(tid, i); + par v := ReadColorByCollector(tid, i) | Yield_Lock(); isWhite := White(v); call LockRelease(tid); } @@ -1409,15 +1457,16 @@ atomic action {:layer 97,100} AtomicClearToAbsWhite({:linear "tid"} tid:Tid) modifies toAbs; { assert tid == GcTid; toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]); } -yield procedure {:layer 96} ClearToAbsWhite({:linear "tid"} tid:Tid) +yield procedure {:layer 96} ClearToAbsWhite({:layer 95, 96} {:linear "tid"} tid:Tid) refines AtomicClearToAbsWhite; +preserves call Yield_Lock(); { call LockAcquire(tid); - call LockedClearToAbsWhite(tid); + par LockedClearToAbsWhite(tid) | Yield_Lock(); call LockRelease(tid); } -yield invariant {:layer 96} Yield(); +yield invariant {:layer 96} Yield_96(); ////////////////////////////////////////////////////////////////////////////// // Layer 95 @@ -1425,9 +1474,9 @@ yield invariant {:layer 96} Yield(); atomic action {:layer 96} AtomicLockedClearToAbsWhite({:linear "tid"} tid:Tid) modifies toAbs; -{ assert tid == GcTid && tidHasLock(tid, lock); toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]); } +{ assert tid == GcTid && tidHasLock(tid, absLock); toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]); } -yield procedure {:layer 95} LockedClearToAbsWhite({:linear "tid"} tid:Tid) +yield procedure {:layer 95} LockedClearToAbsWhite({:layer 95} {:linear "tid"} tid:Tid) refines AtomicLockedClearToAbsWhite; { call {:layer 95} toAbs := Copy((lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x])); @@ -1437,54 +1486,54 @@ both action {:layer 96,99} AtomicInitField({:linear "tid"} tid:Tid, {:linear "ti modifies mem; { assert gcAndMutatorTids(tid, mutatorTids) && memAddr(x) && fieldAddr(f); mem[x][f] := x; } -yield procedure {:layer 95} InitField({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, x: int, f: int) +yield procedure {:layer 95} InitField({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool, x: int, f: int) refines AtomicInitField; { call PrimitiveWriteField(x, f, x); } -atomic action {:layer 96,100} AtomicReadFieldCollector({:linear "tid"} tid:Tid, x:int, f: fld) returns (y: int) +atomic action {:layer 96,100} AtomicReadFieldByCollector({:linear "tid"} tid:Tid, x:int, f: fld) returns (y: int) { assert tid == GcTid && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; y := mem[x][f]; } -yield procedure {:layer 95} ReadFieldCollector({:linear "tid"} tid:Tid, x:int, f: fld) returns (y: int) -refines AtomicReadFieldCollector; +yield procedure {:layer 95} ReadFieldByCollector({:layer 95} {:linear "tid"} tid:Tid, x:int, f: fld) returns (y: int) +refines AtomicReadFieldByCollector; { call y := PrimitiveReadField(x, f); } -atomic action {:layer 96,99} AtomicReadFieldGeneral({:linear "tid"} tid:Tid, x: int, f: fld) returns (y: int) +atomic action {:layer 96,99} AtomicReadFieldByMutator({:linear "tid"} tid:Tid, x: int, f: fld) returns (y: int) { assert mutatorTidWhole(tid) && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; y := mem[x][f]; } -yield procedure {:layer 95} ReadFieldGeneral({:linear "tid"} tid:Tid, x: int, f: fld) returns (y: int) -refines AtomicReadFieldGeneral; +yield procedure {:layer 95} ReadFieldByMutator({:layer 95} {:linear "tid"} tid:Tid, x: int, f: fld) returns (y: int) +refines AtomicReadFieldByMutator; { call y := PrimitiveReadField(x, f); } -atomic action {:layer 96,99} AtomicWriteFieldGeneral({:linear "tid"} tid:Tid, x: int, f: fld, y: int) +atomic action {:layer 96,99} AtomicWriteFieldByMutator({:linear "tid"} tid:Tid, x: int, f: fld, y: int) modifies mem; { assert mutatorTidWhole(tid) && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; mem[x][f] := y; } -yield procedure {:layer 95} WriteFieldGeneral({:linear "tid"} tid:Tid, x: int, f: fld, y: int) -refines AtomicWriteFieldGeneral; +yield procedure {:layer 95} WriteFieldByMutator({:layer 95} {:linear "tid"} tid:Tid, x: int, f: fld, y: int) +refines AtomicWriteFieldByMutator; { call PrimitiveWriteField(x, f, y); } right action {:layer 96} AtomicInitializeFieldInAlloc({:linear "tid"} tid: Tid, ptr: int, fld: int) modifies mem; -{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock) && memAddr(ptr) && fieldAddr(fld) && toAbs[ptr] == nil; mem[ptr][fld] := ptr; } +{ assert mutatorTidWhole(tid) && tidHasLock(tid, absLock) && memAddr(ptr) && fieldAddr(fld) && toAbs[ptr] == nil; mem[ptr][fld] := ptr; } -yield procedure {:layer 95} InitializeFieldInAlloc({:linear "tid"} tid: Tid, ptr: int, fld: int) +yield procedure {:layer 95} InitializeFieldInAlloc({:layer 95} {:linear "tid"} tid: Tid, ptr: int, fld: int) refines AtomicInitializeFieldInAlloc; { call PrimitiveWriteField(ptr, fld, ptr); } both action {:layer 96} AtomicReadMarkStackPtr({:linear "tid"} tid:Tid) returns (val: int) -{ assert tidHasLock(tid, lock); val := MarkStackPtr; } +{ assert tidHasLock(tid, absLock); val := MarkStackPtr; } -yield procedure {:layer 95} ReadMarkStackPtr({:linear "tid"} tid:Tid) returns (val: int) +yield procedure {:layer 95} ReadMarkStackPtr({:layer 95} {:linear "tid"} tid:Tid) returns (val: int) refines AtomicReadMarkStackPtr; { call val := PrimitiveReadMarkStackPtr(); @@ -1494,7 +1543,7 @@ atomic action {:layer 96,98} AtomicInitMarkStackPtr({:linear "tid"} tid:Tid, {:l modifies MarkStackPtr; { assert gcAndMutatorTids(tid, mutatorTids); MarkStackPtr := 0; } -yield procedure {:layer 95} InitMarkStackPtr({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 95} InitMarkStackPtr({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitMarkStackPtr; { call PrimitiveSetMarkStackPtr(0); @@ -1502,18 +1551,18 @@ refines AtomicInitMarkStackPtr; both action {:layer 96} AtomicSetMarkStackPtr({:linear "tid"} tid:Tid, val: int) modifies MarkStackPtr; -{ assert tidHasLock(tid, lock); MarkStackPtr := val; } +{ assert tidHasLock(tid, absLock); MarkStackPtr := val; } -yield procedure {:layer 95} SetMarkStackPtr({:linear "tid"} tid:Tid, val: int) +yield procedure {:layer 95} SetMarkStackPtr({:layer 95} {:linear "tid"} tid:Tid, val: int) refines AtomicSetMarkStackPtr; { call PrimitiveSetMarkStackPtr(val); } both action {:layer 96} AtomicReadMarkStack({:linear "tid"} tid:Tid, ptr: int) returns(val: int) -{ assert tidHasLock(tid, lock); val := MarkStack[ptr]; } +{ assert tidHasLock(tid, absLock); val := MarkStack[ptr]; } -yield procedure {:layer 95} ReadMarkStack({:linear "tid"} tid:Tid, ptr: int) returns(val: int) +yield procedure {:layer 95} ReadMarkStack({:layer 95} {:linear "tid"} tid:Tid, ptr: int) returns(val: int) refines AtomicReadMarkStack; { call val := PrimitiveReadMarkStack(ptr); @@ -1521,9 +1570,9 @@ refines AtomicReadMarkStack; both action {:layer 96} AtomicWriteMarkStack({:linear "tid"} tid:Tid, ptr: int, val: int) modifies MarkStack; -{ assert tidHasLock(tid, lock); MarkStack[ptr] := val; } +{ assert tidHasLock(tid, absLock); MarkStack[ptr] := val; } -yield procedure {:layer 95} WriteMarkStack({:linear "tid"} tid:Tid, ptr: int, val: int) +yield procedure {:layer 95} WriteMarkStack({:layer 95} {:linear "tid"} tid:Tid, ptr: int, val: int) refines AtomicWriteMarkStack; { call PrimitiveWriteMarkStack(ptr, val); @@ -1533,7 +1582,7 @@ both action {:layer 96,99} AtomicInitCollectorPhase({:linear "tid"} tid:Tid, {:l modifies collectorPhase; { assert gcAndMutatorTids(tid, mutatorTids); collectorPhase := IDLE(); } -yield procedure {:layer 95} InitCollectorPhase({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 95} InitCollectorPhase({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitCollectorPhase; { call PrimitiveSetCollectorPhase(IDLE()); @@ -1542,16 +1591,16 @@ refines AtomicInitCollectorPhase; atomic action {:layer 96} AtomicReadCollectorPhase({:linear "tid"} tid: Tid) returns (phase:int) { assert tid == GcTid; phase := collectorPhase; } -yield procedure {:layer 95} ReadCollectorPhase({:linear "tid"} tid: Tid) returns (phase:int) +yield procedure {:layer 95} ReadCollectorPhase({:layer 95} {:linear "tid"} tid: Tid) returns (phase:int) refines AtomicReadCollectorPhase; { call phase := PrimitiveReadCollectorPhase(); } right action {:layer 96} AtomicReadCollectorPhaseLocked({:linear "tid"} tid: Tid) returns (phase:int) -{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock); phase := collectorPhase; } +{ assert mutatorTidWhole(tid) && tidHasLock(tid, absLock); phase := collectorPhase; } -yield procedure {:layer 95} ReadCollectorPhaseLocked({:linear "tid"} tid: Tid) returns (phase:int) +yield procedure {:layer 95} ReadCollectorPhaseLocked({:layer 95} {:linear "tid"} tid: Tid) returns (phase:int) refines AtomicReadCollectorPhaseLocked; { call phase := PrimitiveReadCollectorPhase(); @@ -1559,9 +1608,9 @@ refines AtomicReadCollectorPhaseLocked; both action {:layer 96} AtomicSetCollectorPhase({:linear "tid"} tid: Tid, phase:int) modifies collectorPhase; -{ assert tid == GcTid && tidHasLock(tid, lock); collectorPhase := phase; } +{ assert tid == GcTid && tidHasLock(tid, absLock); collectorPhase := phase; } -yield procedure {:layer 95} SetCollectorPhase({:linear "tid"} tid: Tid, phase:int) +yield procedure {:layer 95} SetCollectorPhase({:layer 95} {:linear "tid"} tid: Tid, phase:int) refines AtomicSetCollectorPhase; { call PrimitiveSetCollectorPhase(phase); @@ -1571,7 +1620,7 @@ both action {:layer 96,99} AtomicInitMutatorPhase({:linear "tid"} tid:Tid, {:lin modifies mutatorPhase; { assert gcAndMutatorTids(tid, mutatorTids); mutatorPhase[id] := IDLE(); } -yield procedure {:layer 95} InitMutatorPhase({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, id: int) +yield procedure {:layer 95} InitMutatorPhase({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool, id: int) refines AtomicInitMutatorPhase; { call PrimitiveSetMutatorPhase(id, IDLE()); @@ -1580,45 +1629,45 @@ refines AtomicInitMutatorPhase; atomic action {:layer 96,100} AtomicReadMutatorPhaseByCollector({:linear "tid"} tid: Tid, i: int) returns (phase:int) { assert tid == GcTid; phase := mutatorPhase[i]; } -yield procedure {:layer 95} ReadMutatorPhaseByCollector({:linear "tid"} tid: Tid, i: int) returns (phase:int) +yield procedure {:layer 95} ReadMutatorPhaseByCollector({:layer 95} {:linear "tid"} tid: Tid, i: int) returns (phase:int) refines AtomicReadMutatorPhaseByCollector; { call phase := PrimitiveReadMutatorPhase(i); } -both action {:layer 96,99} AtomicReadMutatorPhase({:linear "tid"} tid: Tid) returns (phase:int) -{ assert mutatorTidWhole(tid); phase := mutatorPhase[tid->i]; } +both action {:layer 96,99} AtomicReadMutatorPhaseByMutator({:linear "tid"} tid: Tid, i: int) returns (phase:int) +{ assert mutatorTidWhole(tid) && tid->i == i; phase := mutatorPhase[i]; } -yield procedure {:layer 95} ReadMutatorPhase({:linear "tid"} tid: Tid) returns (phase:int) -refines AtomicReadMutatorPhase; +yield procedure {:layer 95} ReadMutatorPhaseByMutator({:layer 95} {:linear "tid"} tid: Tid, i: int) returns (phase:int) +refines AtomicReadMutatorPhaseByMutator; { - call phase := PrimitiveReadMutatorPhase(tid->i); + call phase := PrimitiveReadMutatorPhase(i); } -atomic action {:layer 96} AtomicSetMutatorPhaseLocked({:linear "tid"} tid: Tid, phase: int) +atomic action {:layer 96} AtomicSetMutatorPhaseLocked({:linear "tid"} tid: Tid, i: int, phase: int) modifies mutatorPhase; -{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock) && phase == collectorPhase; mutatorPhase[tid->i] := phase; } +{ assert mutatorTidWhole(tid) && tidHasLock(tid, absLock) && phase == collectorPhase && tid->i == i; mutatorPhase[i] := phase; } -yield procedure {:layer 95} SetMutatorPhaseLocked({:linear "tid"} tid: Tid, phase: int) +yield procedure {:layer 95} SetMutatorPhaseLocked({:layer 95} {:linear "tid"} tid: Tid, i: int, phase: int) refines AtomicSetMutatorPhaseLocked; { - call PrimitiveSetMutatorPhase(tid->i, phase); + call PrimitiveSetMutatorPhase(i, phase); } both action {:layer 96,99} AtomicInitSweepPtr({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) modifies sweepPtr; { assert gcAndMutatorTids(tid, mutatorTids); sweepPtr := memHi; } -yield procedure {:layer 95} InitSweepPtr({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 95} InitSweepPtr({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitSweepPtr; { call PrimitiveSetSweepPtr(memHi); } both action {:layer 96} AtomicReadSweepPtr({:linear "tid"} tid:Tid) returns(val:int) -{ assert tidHasLock(tid, lock); val := sweepPtr; } +{ assert tidHasLock(tid, absLock); val := sweepPtr; } -yield procedure {:layer 95} ReadSweepPtr({:linear "tid"} tid:Tid) returns(val:int) +yield procedure {:layer 95} ReadSweepPtr({:layer 95} {:linear "tid"} tid:Tid) returns(val:int) refines AtomicReadSweepPtr; { call val := PrimitiveReadSweepPtr(); @@ -1626,9 +1675,9 @@ refines AtomicReadSweepPtr; atomic action {:layer 96} AtomicSetSweepPtrLocked({:linear "tid"} tid:Tid, val: int) modifies sweepPtr; -{ assert tid == GcTid && tidHasLock(tid, lock); sweepPtr := val; } +{ assert tid == GcTid && tidHasLock(tid, absLock); sweepPtr := val; } -yield procedure {:layer 95} SetSweepPtrLocked({:linear "tid"} tid:Tid, val: int) +yield procedure {:layer 95} SetSweepPtrLocked({:layer 95} {:linear "tid"} tid:Tid, val: int) refines AtomicSetSweepPtrLocked; { call PrimitiveSetSweepPtr(val); @@ -1636,9 +1685,9 @@ refines AtomicSetSweepPtrLocked; atomic action {:layer 96} AtomicCollectorRootScanBarrierStartLocked({:linear "tid"} tid: Tid) modifies rootScanOn; -{ assert tid == GcTid && tidHasLock(tid, lock); rootScanOn := true; } +{ assert tid == GcTid && tidHasLock(tid, absLock); rootScanOn := true; } -yield procedure {:layer 95} CollectorRootScanBarrierStartLocked({:linear "tid"} tid: Tid) +yield procedure {:layer 95} CollectorRootScanBarrierStartLocked({:layer 95} {:linear "tid"} tid: Tid) refines AtomicCollectorRootScanBarrierStartLocked; { call PrimitiveSetRootScanOn(true); @@ -1646,18 +1695,18 @@ refines AtomicCollectorRootScanBarrierStartLocked; atomic action {:layer 96} AtomicCollectorRootScanBarrierEndLocked({:linear "tid"} tid: Tid) modifies rootScanOn; -{ assert tid == GcTid && tidHasLock(tid, lock); rootScanOn := false; } +{ assert tid == GcTid && tidHasLock(tid, absLock); rootScanOn := false; } -yield procedure {:layer 95} CollectorRootScanBarrierEndLocked({:linear "tid"} tid: Tid) +yield procedure {:layer 95} CollectorRootScanBarrierEndLocked({:layer 95} {:linear "tid"} tid: Tid) refines AtomicCollectorRootScanBarrierEndLocked; { call PrimitiveSetRootScanOn(false); } right action {:layer 96} AtomicMutatorReadBarrierOn({:linear "tid"} tid: Tid) returns (val:bool) -{ assert tidHasLock(tid, lock); val := rootScanOn; } +{ assert tidHasLock(tid, absLock); val := rootScanOn; } -yield procedure {:layer 95} MutatorReadBarrierOn({:linear "tid"} tid: Tid) returns (val:bool) +yield procedure {:layer 95} MutatorReadBarrierOn({:layer 95} {:linear "tid"} tid: Tid) returns (val:bool) refines AtomicMutatorReadBarrierOn; { call val := PrimitiveReadRootScanOn(); @@ -1666,7 +1715,7 @@ refines AtomicMutatorReadBarrierOn; both action {:layer 96,99} AtomicPollMutatorReadBarrierOn({:linear "tid"} tid: Tid) returns (val:bool) { } -yield procedure {:layer 95} PollMutatorReadBarrierOn({:linear "tid"} tid: Tid) returns (val:bool) +yield procedure {:layer 95} PollMutatorReadBarrierOn({:layer 95} {:linear "tid"} tid: Tid) returns (val:bool) refines AtomicPollMutatorReadBarrierOn; { call val := PrimitiveReadRootScanOn(); @@ -1676,7 +1725,7 @@ atomic action {:layer 96,99} AtomicInitRootScanBarrier({:linear "tid"} tid:Tid, modifies rootScanBarrier; { assert gcAndMutatorTids(tid, mutatorTids); rootScanBarrier := numMutators; } -yield procedure {:layer 95} InitRootScanBarrier({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 95} InitRootScanBarrier({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitRootScanBarrier; { call PrimitiveSetRootScanBarrier(numMutators); @@ -1685,7 +1734,7 @@ refines AtomicInitRootScanBarrier; atomic action {:layer 96} AtomicCollectorRootScanBarrierRead({:linear "tid"} tid: Tid) returns (val:int) { assert tid == GcTid; val := rootScanBarrier; } -yield procedure {:layer 95} CollectorRootScanBarrierRead({:linear "tid"} tid: Tid) returns (val:int) +yield procedure {:layer 95} CollectorRootScanBarrierRead({:layer 95} {:linear "tid"} tid: Tid) returns (val:int) refines AtomicCollectorRootScanBarrierRead; { call val := PrimitiveReadRootScanBarrier(); @@ -1693,9 +1742,9 @@ refines AtomicCollectorRootScanBarrierRead; atomic action {:layer 96} AtomicAddRootScanBarrier({:linear "tid"} tid_left: Tid, val: int) modifies rootScanBarrier; -{ assert mutatorTidLeft(tid_left) && tidHasLock(tid_left, lock); rootScanBarrier := rootScanBarrier + val; } +{ assert mutatorTidLeft(tid_left) && tidHasLock(tid_left, absLock); rootScanBarrier := rootScanBarrier + val; } -yield procedure {:layer 95} AddRootScanBarrier({:linear "tid"} tid_left: Tid, val: int) +yield procedure {:layer 95} AddRootScanBarrier({:layer 95} {:linear "tid"} tid_left: Tid, val: int) refines AtomicAddRootScanBarrier; { call PrimitiveAddRootScanBarrier(val); @@ -1704,37 +1753,37 @@ refines AtomicAddRootScanBarrier; right action {:layer 96} AtomicMutatorsInRootScanBarrierAdd({:linear "tid"} tid_left: Tid, {:linear_in "tid"} tid_right: Tid) modifies mutatorsInRootScanBarrier; { - assert tidHasLock(tid_left, lock) && mutatorTidRight(tid_right); + assert tidHasLock(tid_left, absLock) && mutatorTidRight(tid_right); mutatorsInRootScanBarrier[tid_right->i] := true; } -yield procedure {:layer 95} MutatorsInRootScanBarrierAdd({:linear "tid"} tid_left: Tid, {:linear_in "tid"} tid_right: Tid) +yield procedure {:layer 95} MutatorsInRootScanBarrierAdd({:layer 95} {:linear "tid"} tid_left: Tid, {:layer 95} {:linear_in "tid"} tid_right: Tid) refines AtomicMutatorsInRootScanBarrierAdd; { - call PrimitiveMutatorsInRootScanBarrierAdd(tid_right); + call {:layer 95} mutatorsInRootScanBarrier := PrimitiveMutatorsInRootScanBarrierAdd(tid_right, mutatorsInRootScanBarrier); } both action {:layer 96} AtomicMutatorsInRootScanBarrierRemove({:linear "tid"} tid_left: Tid) returns({:linear "tid"} tid_right: Tid) modifies mutatorsInRootScanBarrier; { - assert tidHasLock(tid_left, lock) && !rootScanOn && mutatorTidLeft(tid_left) && mutatorsInRootScanBarrier[tid_left->i]; + assert tidHasLock(tid_left, absLock) && !rootScanOn && mutatorTidLeft(tid_left) && mutatorsInRootScanBarrier[tid_left->i]; mutatorsInRootScanBarrier[tid_left->i] := false; tid_right := Tid(tid_left->i, false, true); } -yield procedure {:layer 95} MutatorsInRootScanBarrierRemove({:linear "tid"} tid_left: Tid) returns({:linear "tid"} tid_right: Tid) +yield procedure {:layer 95} MutatorsInRootScanBarrierRemove({:layer 95} {:linear "tid"} tid_left: Tid) returns({:layer 95} {:linear "tid"} tid_right: Tid) refines AtomicMutatorsInRootScanBarrierRemove; ensures {:layer 95} tid_left->i == tid_right->i; ensures {:layer 95} tid_left->left && tid_right->right; { - call tid_right := PrimitiveMutatorsInRootScanBarrierRemove(tid_left); + call {:layer 95} tid_right, mutatorsInRootScanBarrier := PrimitiveMutatorsInRootScanBarrierRemove(tid_left, mutatorsInRootScanBarrier); } both action {:layer 96,99} AtomicInitRoot({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, x: int) modifies root; { assert gcAndMutatorTids(tid, mutatorTids) && rootAddr(x); root[x] := 0; } -yield procedure {:layer 95} InitRoot({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, x: int) +yield procedure {:layer 95} InitRoot({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool, x: int) refines AtomicInitRoot; { call PrimitiveWriteRoot(x, 0); @@ -1743,7 +1792,7 @@ refines AtomicInitRoot; left action {:layer 96,99} AtomicReadRootInRootScanBarrier({:linear "tid"} tid:Tid, x: idx) returns (val: int) { assert tid == GcTid && rootAddr(x) && rootScanOn && mutatorsInRootScanBarrier == Mutators; val := root[x]; } -yield procedure {:layer 95} ReadRootInRootScanBarrier({:linear "tid"} tid:Tid, x: idx) returns (val: int) +yield procedure {:layer 95} ReadRootInRootScanBarrier({:layer 95} {:linear "tid"} tid:Tid, x: idx) returns (val: int) refines AtomicReadRootInRootScanBarrier; { call val := PrimitiveReadRoot(x); @@ -1753,7 +1802,7 @@ both action {:layer 96,99} AtomicWriteRoot({:linear "tid"} tid: Tid, i: idx, val modifies root; { assert mutatorTidWhole(tid) && rootAddr(i) && tidOwns(tid, i); root[i] := val; } -yield procedure {:layer 95} WriteRoot({:linear "tid"} tid: Tid, i: idx, val: int) +yield procedure {:layer 95} WriteRoot({:layer 95} {:linear "tid"} tid: Tid, i: idx, val: int) refines AtomicWriteRoot; { call PrimitiveWriteRoot(i, val); @@ -1762,7 +1811,7 @@ refines AtomicWriteRoot; both action {:layer 96,99} AtomicReadRoot({:linear "tid"} tid: Tid, i: idx) returns (val: int) { assert mutatorTidWhole(tid) && rootAddr(i) && tidOwns(tid, i); val := root[i]; } -yield procedure {:layer 95} ReadRoot({:linear "tid"} tid: Tid, i: idx) returns (val: int) +yield procedure {:layer 95} ReadRoot({:layer 95} {:linear "tid"} tid: Tid, i: idx) returns (val: int) refines AtomicReadRoot; { call val := PrimitiveReadRoot(i); @@ -1772,16 +1821,16 @@ both action {:layer 96,99} AtomicInitColor({:linear "tid"} tid:Tid, {:linear "ti modifies Color; { assert gcAndMutatorTids(tid, mutatorTids) && memAddr(x); Color[x] := UNALLOC(); } -yield procedure {:layer 95} InitColor({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool, x: int) +yield procedure {:layer 95} InitColor({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool, x: int) refines AtomicInitColor; { call PrimitiveSetColor(x, UNALLOC()); } both action {:layer 96} AtomicReadColorByCollector({:linear "tid"} tid:Tid, i: int) returns (val: int) -{ assert tid == GcTid && tidHasLock(tid, lock) && memAddr(i); val := Color[i]; } +{ assert tid == GcTid && tidHasLock(tid, absLock) && memAddr(i); val := Color[i]; } -yield procedure {:layer 95} ReadColorByCollector({:linear "tid"} tid:Tid, i: int) returns (val: int) +yield procedure {:layer 95} ReadColorByCollector({:layer 95} {:linear "tid"} tid:Tid, i: int) returns (val: int) refines AtomicReadColorByCollector; { call val := PrimitiveReadColor(i); @@ -1790,16 +1839,16 @@ refines AtomicReadColorByCollector; atomic action {:layer 96} AtomicReadColorByMutator1({:linear "tid"} tid:Tid, i: int) returns (val: int) { assert mutatorTidWhole(tid) && memAddr(i); } -yield procedure {:layer 95} ReadColorByMutator1({:linear "tid"} tid:Tid, i: int) returns (val: int) +yield procedure {:layer 95} ReadColorByMutator1({:layer 95} {:linear "tid"} tid:Tid, i: int) returns (val: int) refines AtomicReadColorByMutator1; { call val := PrimitiveReadColor(i); } both action {:layer 96} AtomicReadColorByMutator2({:linear "tid"} tid:Tid, i: int) returns (val: int) -{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock) && memAddr(i); val := Color[i]; } +{ assert mutatorTidWhole(tid) && tidHasLock(tid, absLock) && memAddr(i); val := Color[i]; } -yield procedure {:layer 95} ReadColorByMutator2({:linear "tid"} tid:Tid, i: int) returns (val: int) +yield procedure {:layer 95} ReadColorByMutator2({:layer 95} {:linear "tid"} tid:Tid, i: int) returns (val: int) refines AtomicReadColorByMutator2; { call val := PrimitiveReadColor(i); @@ -1811,7 +1860,7 @@ atomic action {:layer 96,98} AtomicReadColorByMutator3({:linear "tid"} tid:Tid, assume White(Color[i]) ==> White(val); } -yield procedure {:layer 95} ReadColorByMutator3({:linear "tid"} tid:Tid, i: int) returns (val: int) +yield procedure {:layer 95} ReadColorByMutator3({:layer 95} {:linear "tid"} tid:Tid, i: int) returns (val: int) refines AtomicReadColorByMutator3; { call val := PrimitiveReadColor(i); @@ -1819,39 +1868,39 @@ refines AtomicReadColorByMutator3; both action {:layer 96} AtomicSetColor({:linear "tid"} tid:Tid, i: int, val: int) modifies Color; -{ assert tidHasLock(tid, lock) && memAddr(i) && PhaseConsistent(collectorPhase, mutatorPhase) && !MarkPhase(collectorPhase); Color[i] := val; } +{ assert tidHasLock(tid, absLock) && memAddr(i) && PhaseConsistent(collectorPhase, mutatorPhase) && !MarkPhase(collectorPhase); Color[i] := val; } -yield procedure {:layer 95} SetColor({:linear "tid"} tid:Tid, i: int, val: int) +yield procedure {:layer 95} SetColor({:layer 95} {:linear "tid"} tid:Tid, i: int, val: int) refines AtomicSetColor; { call PrimitiveSetColor(i, val); } -left action {:layer 96} AtomicSetColor2({:linear "tid"} tid:Tid, i: int, val: int) +left action {:layer 96} AtomicSetColorInMarkPhase({:linear "tid"} tid:Tid, i: int, val: int) modifies Color; { - assert tidHasLock(tid, lock) && memAddr(i); + assert tidHasLock(tid, absLock) && memAddr(i); assert (MarkPhase(collectorPhase) || !PhaseConsistent(collectorPhase, mutatorPhase) ==> !White(val)); Color[i] := val; } -yield procedure {:layer 95} SetColor2({:linear "tid"} tid:Tid, i: int, val: int) -refines AtomicSetColor2; +yield procedure {:layer 95} SetColorInMarkPhase({:layer 95} {:linear "tid"} tid:Tid, i: int, val: int) +refines AtomicSetColorInMarkPhase; { call PrimitiveSetColor(i, val); } -atomic action {:layer 96} AtomicSetColor3({:linear "tid"} tid:Tid, i: int, val: int, o: obj) +atomic action {:layer 96} AtomicSetColorInAlloc({:linear "tid"} tid:Tid, i: int, val: int, o: obj) modifies Color, toAbs; { - assert tidHasLock(tid, lock) && memAddr(i); + assert tidHasLock(tid, absLock) && memAddr(i); assert White(val) ==> Unalloc(Color[i]); Color[i] := val; toAbs[i] := o; } -yield procedure {:layer 95} SetColor3({:linear "tid"} tid:Tid, i: int, val: int, o: obj) -refines AtomicSetColor3; +yield procedure {:layer 95} SetColorInAlloc({:layer 95} {:layer 95} {:linear "tid"} tid:Tid, i: int, val: int, o: obj) +refines AtomicSetColorInAlloc; { call PrimitiveSetColor(i, val); call {:layer 95} toAbs := Copy(toAbs[i := o]); @@ -1864,61 +1913,63 @@ modifies toAbs; toAbs := (lambda i:int :: if memAddr(i) then nil else Int(i)); } -yield procedure {:layer 95} InitToAbs({:linear "tid"} tid:Tid, {:linear "tid"} mutatorTids:[int]bool) +yield procedure {:layer 95} InitToAbs({:layer 95} {:linear "tid"} tid:Tid, {:layer 95} {:linear "tid"} mutatorTids:[int]bool) refines AtomicInitToAbs; { call {:layer 95} toAbs := Copy((lambda i:int :: if memAddr(i) then nil else Int(i))); } right action {:layer 96} AtomicLockAcquire({:linear "tid"} tid: Tid) -modifies lock; -{ assert tid->i != 0; assume lock == 0; lock := tid->i; } +modifies absLock; +{ assert tid->i != 0; assume absLock == 0; absLock := tid->i; } -yield procedure {:layer 95} LockAcquire({:linear "tid"} tid: Tid) +yield procedure {:layer 95} LockAcquire({:layer 95} {:linear "tid"} tid: Tid) refines AtomicLockAcquire; +preserves call Yield_Lock(); { var status:bool; while (true) - invariant {:yields} true; + invariant {:yields} true; + invariant call Yield_Lock(); { - call status := PrimitiveLockCAS(tid->i); + call status := PrimitiveLockCAS(); if (status) { + call {:layer 95} absLock := Copy(tid->i); return; } } } left action {:layer 96} AtomicLockRelease({:linear "tid"} tid:Tid) -modifies lock; -{ assert tidHasLock(tid, lock); lock := 0; } +modifies absLock; +{ assert tidHasLock(tid, absLock); absLock := 0; } -yield procedure {:layer 95} LockRelease({:linear "tid"} tid:Tid) +yield procedure {:layer 95} LockRelease({:layer 95} {:linear "tid"} tid:Tid) refines AtomicLockRelease; +preserves call Yield_Lock(); { - call PrimitiveLockZero(); + call PrimitiveLockClear(); + call {:layer 95} absLock := Copy(0); } +yield invariant {:layer 95} Yield_Lock(); +invariant lock <==> absLock != 0; + ////////////////////////////////////////////////////////////////////////////// // ATOMIC PRIMITIVES // The action specifications, linearity specifications, and requires/ensures below here are trusted. // (Note, though, that Boogie still verifies the mover types (atomic,left,right,both); these are not trusted.) ////////////////////////////////////////////////////////////////////////////// -both action {:layer 1,96} AtomicTidSplit({:linear_in "tid"} tid:Tid) returns({:linear "tid"} tid_left:Tid, {:linear "tid"} tid_right:Tid) +pure action TidSplit({:linear_in "tid"} tid:Tid) returns({:linear "tid"} tid_left:Tid, {:linear "tid"} tid_right:Tid) { assert tid->left && tid->right; tid_left := Tid(tid->i, true, false); tid_right := Tid(tid->i, false, true); } -yield procedure {:layer 0} TidSplit({:linear_in "tid"} tid:Tid) returns({:linear "tid"} tid_left:Tid, {:linear "tid"} tid_right:Tid); -refines AtomicTidSplit; -both action {:layer 1,96} AtomicTidCombine({:linear_in "tid"} tid_left:Tid, {:linear_in "tid"} tid_right:Tid) returns({:linear "tid"} tid:Tid) +pure action TidCombine({:linear_in "tid"} tid_left:Tid, {:linear_in "tid"} tid_right:Tid) returns({:linear "tid"} tid:Tid) { assert tid_left->i == tid_right->i && tid_left->left && tid_right->right; tid := Tid(tid_left->i, true, true); } -yield procedure {:layer 0} TidCombine({:linear_in "tid"} tid_left:Tid, {:linear_in "tid"} tid_right:Tid) returns({:linear "tid"} tid:Tid); -refines AtomicTidCombine; -both action {:layer 1,99} AtomicTidOutput({:linear_in "tid"} tid_in:Tid, {:linear_out "tid"} tid_out:Tid) +pure action TidOutput({:linear_in "tid"} tid_in:Tid, {:linear_out "tid"} tid_out:Tid) { assert tid_in == tid_out; } -yield procedure {:layer 0} TidOutput({:linear_in "tid"} tid_in:Tid, {:linear_out "tid"} tid_out:Tid); -refines AtomicTidOutput; atomic action {:layer 1,95} AtomicPrimitiveReadField(x: int, f: fld) returns (y: int) { assert memAddr(x) && fieldAddr(f); y := mem[x][f]; } @@ -1931,12 +1982,6 @@ modifies mem; yield procedure {:layer 0} PrimitiveWriteField(x: int, f: fld, y: int); refines AtomicPrimitiveWriteField; -right action {:layer 1,99} AtomicPrimitiveFindFreePtrAbs() returns (o: obj) -modifies allocSet; -{ assume (memAddrAbs(o) && !allocSet[o] && o != nil); allocSet[o] := true; } -yield procedure {:layer 0} PrimitiveFindFreePtrAbs() returns (o: obj); -refines AtomicPrimitiveFindFreePtrAbs; - atomic action {:layer 1,95} AtomicPrimitiveReadMarkStackPtr() returns (val: int) { val := MarkStackPtr; } yield procedure {:layer 0} PrimitiveReadMarkStackPtr() returns (val: int); @@ -2020,17 +2065,20 @@ modifies rootScanBarrier; yield procedure {:layer 0} PrimitiveAddRootScanBarrier(val: int); refines AtomicPrimitiveAddRootScanBarrier; -atomic action {:layer 1,95} AtomicPrimitiveMutatorsInRootScanBarrierAdd({:linear_in "tid"} tid_right: Tid) -modifies mutatorsInRootScanBarrier; -{ assert mutatorTidRight(tid_right); mutatorsInRootScanBarrier[tid_right->i] := true; } -yield procedure {:layer 0} PrimitiveMutatorsInRootScanBarrierAdd({:linear_in "tid"} tid_right: Tid); -refines AtomicPrimitiveMutatorsInRootScanBarrierAdd; +pure action PrimitiveMutatorsInRootScanBarrierAdd({:linear_in "tid"} tid_right: Tid, {:linear_in "tid"} mutatorsInRootScanBarrier: [int]bool) + returns ({:linear "tid"} mutatorsInRootScanBarrier': [int]bool) +{ + assert mutatorTidRight(tid_right); + mutatorsInRootScanBarrier' := mutatorsInRootScanBarrier[tid_right->i := true]; +} -atomic action {:layer 1,95} AtomicPrimitiveMutatorsInRootScanBarrierRemove({:linear "tid"} tid_left: Tid) returns({:linear "tid"} tid_right: Tid) -modifies mutatorsInRootScanBarrier; -{ assert mutatorTidLeft(tid_left) && mutatorsInRootScanBarrier[tid_left->i]; mutatorsInRootScanBarrier[tid_left->i] := false; tid_right := Tid(tid_left->i, false, true); } -yield procedure {:layer 0} PrimitiveMutatorsInRootScanBarrierRemove({:linear "tid"} tid_left: Tid) returns({:linear "tid"} tid_right: Tid); -refines AtomicPrimitiveMutatorsInRootScanBarrierRemove; +pure action PrimitiveMutatorsInRootScanBarrierRemove({:linear "tid"} tid_left: Tid, {:linear_in "tid"} mutatorsInRootScanBarrier: [int]bool) + returns({:linear "tid"} tid_right: Tid, {:linear "tid"} mutatorsInRootScanBarrier': [int]bool) +{ + assert mutatorTidLeft(tid_left) && mutatorsInRootScanBarrier[tid_left->i]; + mutatorsInRootScanBarrier' := mutatorsInRootScanBarrier[tid_left->i := false]; + tid_right := Tid(tid_left->i, false, true); +} atomic action {:layer 1,95} AtomicPrimitiveWriteRoot(i: idx, val: int) modifies root; @@ -2054,21 +2102,20 @@ modifies Color; yield procedure {:layer 0} PrimitiveSetColor(i: int, val: int); refines AtomicPrimitiveSetColor; -atomic action {:layer 1,95} AtomicPrimitiveLockCAS(next: int) returns (status: bool) +atomic action {:layer 1,95} AtomicPrimitiveLockCAS() returns (status: bool) modifies lock; { - assert next != 0; if (*) { - assume lock == 0; lock := next; status := true; + assume !lock; lock := true; status := true; } else { status := false; } } -yield procedure {:layer 0} PrimitiveLockCAS(next: int) returns (status: bool); +yield procedure {:layer 0} PrimitiveLockCAS() returns (status: bool); refines AtomicPrimitiveLockCAS; -atomic action {:layer 1,95} AtomicPrimitiveLockZero() +atomic action {:layer 1,95} AtomicPrimitiveLockClear() modifies lock; -{ lock := 0; } -yield procedure {:layer 0} PrimitiveLockZero(); -refines AtomicPrimitiveLockZero; +{ lock := false; } +yield procedure {:layer 0} PrimitiveLockClear(); +refines AtomicPrimitiveLockClear; diff --git a/Test/civl/samples/GC.bpl.expect b/Test/civl/samples/GC.bpl.expect index 3392eb7f1..d4d21cf96 100644 --- a/Test/civl/samples/GC.bpl.expect +++ b/Test/civl/samples/GC.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 730 verified, 0 errors +Boogie program verifier finished with 729 verified, 0 errors diff --git a/Test/civl/samples/StoreBuffer.bpl b/Test/civl/samples/StoreBuffer.bpl index 813759604..8e53467cc 100644 --- a/Test/civl/samples/StoreBuffer.bpl +++ b/Test/civl/samples/StoreBuffer.bpl @@ -1,6 +1,6 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type {:linear "tid", "addr"} X = int; +type {:linear "tid"} X = int; const numMutators: int; axiom 0 < numMutators; diff --git a/Test/civl/samples/alloc-mem.bpl b/Test/civl/samples/alloc-mem.bpl index 67e735f4b..b3a98f59a 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} Map_Contains(local_in->val, 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} Map_Contains(l->val, 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 Map_Contains(l->val, 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} Map_Contains(l->val, 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 Map_Contains(l->val, i); + o := l->val->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 Map_Contains(l->val, i); + l' := l; + l'->val->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} Map_Contains(l->val, 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_Create(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 Map_Contains(l->val, 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 Map_Contains(l->val, i); + l' := l; + l'->val->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 Map_Contains(l->val, i) && Map_At(l->val, 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 diff --git a/Test/civl/samples/civl-paper.bpl b/Test/civl/samples/civl-paper.bpl index 2350a6040..ab7cd87f4 100644 --- a/Test/civl/samples/civl-paper.bpl +++ b/Test/civl/samples/civl-paper.bpl @@ -1,19 +1,10 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type {:linear "tid"} X; -const nil: X; - -type {:linear "mem"} Int = 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); -function emptyDom(l:lmap) : lmap -{ cons((lambda x:int :: false), map(l)) } +type X; +const nil: X; -var {:layer 0,3} {:linear "mem"} g: lmap; +var {:layer 0,3} g: Lmap int int; var {:layer 0,3} lock: X; var {:layer 0,1} b: bool; @@ -23,15 +14,15 @@ yield invariant {:layer 1} InvLock(); invariant lock != nil <==> b; yield invariant {:layer 3} InvMem(); -invariant dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4]; +invariant Map_Contains(g->val, p) && Map_Contains(g->val, p+4) && Map_At(g->val, p) == Map_At(g->val, p+4); -yield procedure {:layer 3} P({:linear "tid"} tid: X) -requires {:layer 1,3} tid != nil; +yield procedure {:layer 3} P(tid: Lval X) +requires {:layer 1,3} tid->val != nil; preserves call InvLock(); preserves call InvMem(); { var t: int; - var {:linear "mem"} l: lmap; + var l: Lmap int int; call AcquireProtected(tid); call l := TransferFromGlobalProtected(tid); @@ -43,60 +34,60 @@ preserves call InvMem(); call ReleaseProtected(tid); } -both action {:layer 3} AtomicTransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) +both action {:layer 3} AtomicTransferToGlobalProtected(tid: Lval X, {:linear_in} l: Lmap int int) modifies g; -{ assert tid != nil && lock == tid; g := l; } +{ assert tid->val != nil && lock == tid->val; g := l; } yield procedure {:layer 2} -TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) +TransferToGlobalProtected(tid: Lval X, {:linear_in} l: Lmap int int) refines AtomicTransferToGlobalProtected; preserves call InvLock(); { call TransferToGlobal(tid, l); } -both action {:layer 3} AtomicTransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) +both action {:layer 3} AtomicTransferFromGlobalProtected(tid: Lval X) returns (l: Lmap int int) modifies g; -{ assert tid != nil && lock == tid; l := g; g := emptyDom(g); } +{ assert tid->val != nil && lock == tid->val; l := g; call g := Lmap_Empty(); } yield procedure {:layer 2} -TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) +TransferFromGlobalProtected(tid: Lval X) returns (l: Lmap int int) refines AtomicTransferFromGlobalProtected; preserves call InvLock(); { call l := TransferFromGlobal(tid); } -right action {:layer 3} AtomicAcquireProtected({:linear "tid"} tid: X) +right action {:layer 3} AtomicAcquireProtected(tid: Lval X) modifies lock; -{ assert tid != nil; assume lock == nil; lock := tid; } +{ assert tid->val != nil; assume lock == nil; lock := tid->val; } -yield procedure {:layer 2} AcquireProtected({:linear "tid"} tid: X) +yield procedure {:layer 2} AcquireProtected(tid: Lval X) refines AtomicAcquireProtected; -requires {:layer 1} tid != nil; +requires {:layer 1} tid->val != nil; preserves call InvLock(); { call Acquire(tid); } -left action {:layer 3} AtomicReleaseProtected({:linear "tid"} tid: X) +left action {:layer 3} AtomicReleaseProtected(tid: Lval X) modifies lock; -{ assert tid != nil && lock == tid; lock := nil; } +{ assert tid->val != nil && lock == tid->val; lock := nil; } -yield procedure {:layer 2} ReleaseProtected({:linear "tid"} tid: X) +yield procedure {:layer 2} ReleaseProtected(tid: Lval X) refines AtomicReleaseProtected; preserves call InvLock(); { call Release(tid); } -atomic action {:layer 2} AtomicAcquire({:linear "tid"} tid: X) +atomic action {:layer 2} AtomicAcquire(tid: Lval X) modifies lock; -{ assume lock == nil; lock := tid; } +{ assume lock == nil; lock := tid->val; } -yield procedure {:layer 1} Acquire({:linear "tid"} tid: X) +yield procedure {:layer 1} Acquire(tid: Lval X) refines AtomicAcquire; -requires {:layer 1} tid != nil; +requires {:layer 1} tid->val != nil; preserves call InvLock(); { var status: bool; @@ -106,48 +97,48 @@ preserves call InvLock(); invariant {:yields} true; invariant call InvLock(); { - call status := CAS(tid, false, true); + call status := CAS(tid->val, false, true); if (status) { return; } } } -atomic action {:layer 2} AtomicRelease({:linear "tid"} tid: X) +atomic action {:layer 2} AtomicRelease(tid: Lval X) modifies lock; { lock := nil; } -yield procedure {:layer 1} Release({:linear "tid"} tid: X) +yield procedure {:layer 1} Release(tid: Lval X) refines AtomicRelease; preserves call InvLock(); { - call CLEAR(tid, false); + call CLEAR(tid->val, false); } -atomic action {:layer 1,2} AtomicTransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) +atomic action {:layer 1,2} AtomicTransferToGlobal(tid: Lval X, {:linear_in} l: Lmap int int) modifies g; { g := l; } -yield procedure {:layer 0} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap); +yield procedure {:layer 0} TransferToGlobal(tid: Lval X, {:linear_in} l: Lmap int int); refines AtomicTransferToGlobal; -atomic action {:layer 1,2} AtomicTransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) +atomic action {:layer 1,2} AtomicTransferFromGlobal(tid: Lval X) returns (l: Lmap int int) modifies g; -{ l := g; g := emptyDom(g); } +{ l := g; call g := Lmap_Empty(); } -yield procedure {:layer 0} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap); +yield procedure {:layer 0} TransferFromGlobal(tid: Lval X) returns (l: Lmap int int); refines AtomicTransferFromGlobal; -both action {:layer 1,3} AtomicLoad({:linear "mem"} l: lmap, a: int) returns (v: int) -{ v := map(l)[a]; } +both action {:layer 1,3} AtomicLoad(l: Lmap int int, a: int) returns (v: int) +{ v := l->val->val[a]; } -yield procedure {:layer 0} Load({:linear "mem"} l: lmap, a: int) returns (v: int); +yield procedure {:layer 0} Load(l: Lmap int int, a: int) returns (v: int); refines AtomicLoad; -both action {:layer 1,3} AtomicStore({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap) -{ l_out := cons(dom(l_in), map(l_in)[a := v]); } +both action {:layer 1,3} AtomicStore({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int) +{ l_out := l_in; l_out->val->val[a] := v; } -yield procedure {:layer 0} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap); +yield procedure {:layer 0} Store({:linear_in} l_in: Lmap int int, a: int, v: int) returns (l_out: Lmap int int); refines AtomicStore; atomic action {:layer 1} AtomicCAS(tid: X, prev: bool, next: bool) returns (status: bool) diff --git a/Test/civl/samples/civl-paper.bpl.expect b/Test/civl/samples/civl-paper.bpl.expect index 129e60e25..42111ae0b 100644 --- a/Test/civl/samples/civl-paper.bpl.expect +++ b/Test/civl/samples/civl-paper.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 39 verified, 0 errors +Boogie program verifier finished with 29 verified, 0 errors diff --git a/Test/civl/samples/reserve.bpl b/Test/civl/samples/reserve.bpl index ad42492d6..b187fd1ec 100644 --- a/Test/civl/samples/reserve.bpl +++ b/Test/civl/samples/reserve.bpl @@ -100,7 +100,7 @@ pure action PreAlloc({:linear "tid"} tid: Tid, set: Set int, allocMap: Bijection { var ptr: int; assert set != Set_Empty(); - ptr := Set_Choose(set); + ptr := Choice(set->val); allocMap' := Bijection(Map_Update(allocMap->tidToPtr, tid, ptr), Map_Update(allocMap->ptrToTid, ptr, tid)); } diff --git a/Test/civl/samples/ticket.bpl b/Test/civl/samples/ticket.bpl index 2b832990a..cc21f0312 100644 --- a/Test/civl/samples/ticket.bpl +++ b/Test/civl/samples/ticket.bpl @@ -1,37 +1,31 @@ // RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -function RightOpen (n: int) : [int]bool; -function RightClosed (n: int) : [int]bool; -axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); -axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); - -type {:linear "tid"} X; -const nil: X; -var {:layer 0,1} t: int; // next ticket to issue -var {:layer 0,2} s: int; // current ticket permitted to critical section -var {:layer 1,2} cs: X; // current thread in critical section -var {:layer 1,2} T: [int]bool; // set of issued tickets +type Tid; + +var {:layer 0,1} t: int; // next ticket to issue +var {:layer 0,2} s: int; // current ticket permitted to critical section +var {:layer 1,2} cs: Option Tid; // current thread in critical section +var {:layer 1,2} T: [int]bool; // set of issued tickets // ########################################################################### // Invariants function {:inline} Inv1 (tickets: [int]bool, ticket: int): (bool) { - tickets == RightOpen(ticket) + (forall i: int :: tickets[i] <==> i < ticket) } -function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: X): (bool) +function {:inline} Inv2 (tickets: [int]bool, ticket: int, lock: Option Tid): (bool) { - if (lock == nil) then tickets == RightOpen(ticket) - else tickets == RightClosed(ticket) + lock is None || tickets[ticket] } // ########################################################################### // Yield invariants -yield invariant {:layer 2} YieldSpec ({:linear "tid"} tid: X); -invariant tid != nil && cs == tid; +yield invariant {:layer 2} YieldSpec (tid: Lval Tid); +invariant cs is Some && cs->t == tid->val; yield invariant {:layer 1} Yield1 (); invariant Inv1(T, t); @@ -39,13 +33,40 @@ invariant Inv1(T, t); yield invariant {:layer 2} Yield2 (); invariant Inv2(T, s, cs); +// ########################################################################### +// Test driver + +yield procedure {:layer 2} main ({:layer 1,2} {:linear_in} _tids: Lset Tid) +requires call Yield1(); +requires call Yield2(); +{ + var {:layer 1,2} tid: Lval Tid; + var {:layer 1,2} tids: Lset Tid; + + tids := _tids; + while (*) + invariant {:yields} true; + invariant call Yield1(); + invariant call Yield2(); + { + call {:layer 1,2} tid, tids := Allocate(tids); + async call Customer(tid); + } +} + +pure procedure {:inline 1} Allocate({:linear_in} _tids: Lset Tid) returns (tid: Lval Tid, tids: Lset Tid) +{ + tids := _tids; + assume {:layer 1,2} tids->dom != MapConst(false); + call {:layer 1,2} tid := Lval_Get(tids, Choice(tids->dom)); +} + // ########################################################################### // Procedures and actions -yield procedure {:layer 2} Customer ({:layer 1,2} {:linear_in "tid"} tid: X) +yield procedure {:layer 2} Customer ({:layer 1,2} tid: Lval Tid) requires call Yield1(); requires call Yield2(); -requires {:layer 2} tid != nil; { while (*) invariant {:yields} true; @@ -58,11 +79,10 @@ requires {:layer 2} tid != nil; } } -yield procedure {:layer 2} Enter ({:layer 1,2} {:linear "tid"} tid: X) +yield procedure {:layer 2} Enter ({:layer 1,2} tid: Lval Tid) preserves call Yield1(); preserves call Yield2(); ensures call YieldSpec(tid); -requires {:layer 2} tid != nil; { var m: int; @@ -70,10 +90,10 @@ requires {:layer 2} tid != nil; call WaitAndEnter(tid, m); } -right action {:layer 2} AtomicGetTicket ({:linear "tid"} tid: X) returns (m: int) +right action {:layer 2} AtomicGetTicket (tid: Lval Tid) returns (m: int) modifies T; { assume !T[m]; T[m] := true; } -yield procedure {:layer 1} GetTicket ({:layer 1} {:linear "tid"} tid: X) returns (m: int) +yield procedure {:layer 1} GetTicket ({:layer 1} tid: Lval Tid) returns (m: int) refines AtomicGetTicket; preserves call Yield1(); { @@ -87,15 +107,15 @@ modifies t; yield procedure {:layer 0} GetTicket#0 () returns (m: int); refines AtomicGetTicket#0; -atomic action {:layer 2} AtomicWaitAndEnter ({:linear "tid"} tid: X, m:int) +atomic action {:layer 2} AtomicWaitAndEnter (tid: Lval Tid, m:int) modifies cs; -{ assume m == s; cs := tid; } -yield procedure {:layer 1} WaitAndEnter ({:layer 1} {:linear "tid"} tid: X, m:int) +{ assume m == s; cs := Some(tid->val); } +yield procedure {:layer 1} WaitAndEnter ({:layer 1} tid: Lval Tid, m:int) refines AtomicWaitAndEnter; preserves call Yield1(); { call WaitAndEnter#0(m); - call {:layer 1} cs := Copy(tid); + call {:layer 1} cs := Copy(Some(tid->val)); } atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int) @@ -103,15 +123,15 @@ atomic action {:layer 1} AtomicWaitAndEnter#0 (m:int) yield procedure {:layer 0} WaitAndEnter#0 (m:int); refines AtomicWaitAndEnter#0; -atomic action {:layer 2} AtomicLeave ({:linear "tid"} tid: X) +atomic action {:layer 2} AtomicLeave (tid: Lval Tid) modifies cs, s; -{ assert cs == tid; s := s + 1; cs := nil; } -yield procedure {:layer 1} Leave ({:layer 1} {:linear "tid"} tid: X) +{ assert cs == Some(tid->val); s := s + 1; cs := None(); } +yield procedure {:layer 1} Leave ({:layer 1} tid: Lval Tid) refines AtomicLeave; preserves call Yield1(); { call Leave#0(); - call {:layer 1} cs := Copy(nil); + call {:layer 1} cs := Copy(None()); } atomic action {:layer 1} AtomicLeave#0 () diff --git a/Test/civl/samples/ticket.bpl.expect b/Test/civl/samples/ticket.bpl.expect index cccffe05d..12041afe1 100644 --- a/Test/civl/samples/ticket.bpl.expect +++ b/Test/civl/samples/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 11 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 18116b21b..cd8d063ee 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -1,68 +1,78 @@ // RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t" // RUN: %diff "%s.expect" "%t" -/* -Highlights: -- Nontrivial use of nested linear maps -- Push and pop use distinct abstractions for read/write of top of stack -- Variable "unused" tracks nodes added to the stack linear map that do - not logically become part of the stack -- Push made atomic first before commutativity reasoning for the pop path -- The final layer transforms the stack into a functional version. The proof - for this layer uses an "abstraction function" specified as a pure procedure. -*/ - datatype Treiber { Treiber(top: RefNode T, stack: Lheap (Node T)) } type RefTreiber T = Ref (Treiber T); type X; // module type parameter -var {:layer 4, 5} Stack: [RefTreiber X]Vec X; +var {:layer 4, 5} Stack: Map (RefTreiber X) (Vec X); var {:layer 0, 4} ts: Lheap (Treiber X); -var {:layer 2, 4} unused: [RefTreiber X][RefNode X]bool; -atomic action {:layer 5} AtomicAlloc() returns (ref_t: Lval (RefTreiber X)) +atomic action {:layer 5} AtomicAlloc() returns (loc_t: Lval (Loc (Treiber X))) modifies Stack; { - call ref_t := Ref_Alloc(); - Stack[ref_t->val] := Vec_Empty(); + var ref_t: RefTreiber X; + call loc_t := Loc_New(); + ref_t := Ref(loc_t->val); + assume !Map_Contains(Stack, ref_t); + Stack := Map_Update(Stack, ref_t, Vec_Empty()); } -yield procedure {:layer 4} Alloc() returns (ref_t: Lval (RefTreiber X)) +yield procedure {:layer 4} Alloc() returns (loc_t: Lval (Loc (Treiber X))) refines AtomicAlloc; +preserves call YieldInvDom#4(); { - call ref_t := Alloc#0(); - call {:layer 4} Stack := Copy(Stack[ref_t->val := Vec_Empty()]); - call {:layer 4} AbsDefinition(ts->val[ref_t->val]->top, ts->val[ref_t->val]->stack->val); + var top: Ref (Node X); + var stack: Lheap (Node X); + var treiber: Treiber X; + var lmap_t: Lheap (Treiber X); + var ref_t: RefTreiber X; + top := Nil(); + call stack := Lmap_Empty(); + treiber := Treiber(top, stack); + call loc_t, lmap_t := Lmap_Alloc(treiber); + call {:layer 4} Lmap_Assume(lmap_t, ts); + ref_t := Ref(loc_t->val); + call AllocTreiber(lmap_t, ref_t); + call {:layer 4} Stack := Copy(Map_Update(Stack, ref_t, Vec_Empty())); + call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val); } atomic action {:layer 5} AtomicPush(ref_t: RefTreiber X, x: X) returns (success: bool) modifies Stack; { if (success) { - Stack[ref_t] := Vec_Append(Stack[ref_t], x); + Stack := Map_Update(Stack, ref_t, Vec_Append(Map_At(Stack, ref_t), x)); } } yield procedure {:layer 4} Push(ref_t: RefTreiber X, x: X) returns (success: bool) refines AtomicPush; preserves call YieldInv#2(ref_t); preserves call YieldInv#4(ref_t); +preserves call YieldInvDom#4(); { + var {:layer 4} old_top: RefNode X; + var {:layer 4} old_stack: Map (RefNode X) (Node X); + call {:layer 4} old_top := Copy(ts->val->val[ref_t]->top); + call {:layer 4} old_stack := Copy(ts->val->val[ref_t]->stack->val); call success := PushIntermediate(ref_t, x); if (success) { - call {:layer 4} Stack := Copy(Stack[ref_t := Vec_Append(Stack[ref_t], x)]); + call {:layer 4} FrameLemma(old_top, old_stack, ts->val->val[ref_t]->stack->val); + call {:layer 4} Stack := Copy(Map_Update(Stack, ref_t, Vec_Append(Map_At(Stack, ref_t), x))); + assert {:layer 4} ts->val->val[ref_t]->top != Nil(); + call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val); } - call {:layer 4} AbsDefinition(ts->val[ref_t]->top, ts->val[ref_t]->stack->val); } atomic action {:layer 5} AtomicPop(ref_t: RefTreiber X) returns (success: bool, x: X) modifies Stack; { var stack: Vec X; - stack := Stack[ref_t]; + stack := Map_At(Stack, ref_t); if (success) { assume Vec_Len(stack) > 0; x := Vec_Nth(stack, Vec_Len(stack) - 1); - Stack[ref_t] := Vec_Remove(stack); + Stack := Map_Update(Stack, ref_t, Vec_Remove(stack)); } } yield procedure {:layer 4} Pop(ref_t: RefTreiber X) returns (success: bool, x: X) @@ -70,12 +80,13 @@ refines AtomicPop; preserves call YieldInv#2(ref_t); preserves call YieldInv#3(ref_t); preserves call YieldInv#4(ref_t); +preserves call YieldInvDom#4(); { - call {:layer 4} AbsDefinition(ts->val[ref_t]->top, ts->val[ref_t]->stack->val); + call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val); call success, x := PopIntermediate(ref_t); if (success) { - assert {:layer 4} Vec_Len(Stack[ref_t]) > 0; - call {:layer 4} Stack := Copy(Stack[ref_t := Vec_Remove(Stack[ref_t])]); + assert {:layer 4} Vec_Len(Map_At(Stack, ref_t)) > 0; + call {:layer 4} Stack := Copy(Map_Update(Stack, ref_t, Vec_Remove(Map_At(Stack, ref_t)))); } } @@ -83,12 +94,12 @@ atomic action {:layer 4} AtomicPopIntermediate(ref_t: RefTreiber X) returns (suc modifies ts; { var new_ref_n: RefNode X; - assume ts->dom[ref_t]; + assume Map_Contains(ts->val, ref_t); if (success) { - 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); + assume ts->val->val[ref_t]->top != Nil(); + assume Map_Contains(ts->val->val[ref_t]->stack->val, ts->val->val[ref_t]->top); + Node(new_ref_n, x) := ts->val->val[ref_t]->stack->val->val[ts->val->val[ref_t]->top]; + ts->val->val[ref_t]->top := new_ref_n; } } yield procedure {:layer 3} PopIntermediate(ref_t: RefTreiber X) returns (success: bool, x: X) @@ -110,39 +121,44 @@ preserves call YieldInv#3(ref_t); } atomic action {:layer 3, 4} AtomicPushIntermediate(ref_t: RefTreiber X, x: X) returns (success: bool) -modifies ts, unused; +modifies ts; { - var {:pool "A"} ref_n: Lval (RefNode X); - var {:pool "A"} new_ref_n: Lval (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)); + var new_loc_n: Lval (Loc (Node X)); + var lmap_n, lmap_n': Lheap (Node X); + var t: RefNode X; + if (success) { - call Lheap_Write(ts->val[ref_t]->top, new_ref_n->val); - } else { - unused[ref_t][new_ref_n->val] := true; + t := ts->val->val[ref_t]->top; + call new_loc_n, lmap_n := Lmap_Alloc(Node(t, x)); + call Lmap_Assume(lmap_n, ts->val->val[ref_t]->stack); + ts->val->val[ref_t]->top := Ref(new_loc_n->val); + call lmap_n, lmap_n' := Lmap_Move(lmap_n, ts->val->val[ref_t]->stack, ts->val->val[ref_t]->top); + ts->val->val[ref_t]->stack := lmap_n'; } - assume {:add_to_pool "A", new_ref_n} true; } yield procedure {:layer 2} PushIntermediate(ref_t: RefTreiber X, x: X) returns (success: bool) refines AtomicPushIntermediate; preserves call YieldInv#2(ref_t); { var ref_n: RefNode X; - var new_ref_n: Lval (RefNode X); + var new_loc_n: Lval (Loc (Node X)); + var lmap_n: Lheap (Node X); + var new_ref_n: RefNode X; call ref_n := ReadTopOfStack#Push(ref_t); - call new_ref_n := AllocInStack(ref_t, Node(ref_n, x)); - call success := WriteTopOfStack(ref_t, ref_n, new_ref_n->val); - assume {:add_to_pool "A", Lval(ref_n), new_ref_n} true; - if (!success) { - call {:layer 2} unused := Copy((var a := unused[ref_t]; unused[ref_t := a[new_ref_n->val := true]])); + call new_loc_n, lmap_n := Lmap_Alloc(Node(ref_n, x)); + call {:layer 2} Lmap_Assume(lmap_n, ts->val->val[ref_t]->stack); + new_ref_n := Ref(new_loc_n->val); + call success := WriteTopOfStack(ref_t, ref_n, new_ref_n); + if (success) { + call AllocNode(ref_t, new_ref_n, lmap_n); } } right action {:layer 3} AtomicReadTopOfStack#Pop(ref_t: RefTreiber X) returns (ref_n: RefNode X) { - assert ts->dom[ref_t]; - assume NilDomain(ts, ref_t, unused)[ref_n]; + assert Map_Contains(ts->val, ref_t); + assume NilDomain(ts, ref_t)[ref_n]; } yield procedure {:layer 2} ReadTopOfStack#Pop(ref_t: RefTreiber X) returns (ref_n: RefNode X) refines AtomicReadTopOfStack#Pop; @@ -153,7 +169,7 @@ preserves call YieldInv#2(ref_t); right action {:layer 2} AtomicReadTopOfStack#Push(ref_t: RefTreiber X) returns (ref_n: RefNode X) { - assert ts->dom[ref_t]; + assert Map_Contains(ts->val, ref_t); } yield procedure {:layer 1} ReadTopOfStack#Push(ref_t: RefTreiber X) returns (ref_n: RefNode X) refines AtomicReadTopOfStack#Push; @@ -161,36 +177,23 @@ refines AtomicReadTopOfStack#Push; call ref_n := ReadTopOfStack(ref_t); } -atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X) -{ - assert ts->dom[ref_t]; - ref_n := ts->val[ref_t]->top; -} -yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X); -refines AtomicReadTopOfStack; - -right action {:layer 1, 3} AtomicLoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X) +right action {:layer 3} AtomicLoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X) { - assert ts->dom[ref_t]; - assert ts->val[ref_t]->stack->dom[ref_n]; - node := ts->val[ref_t]->stack->val[ref_n]; + assert Map_Contains(ts->val, ref_t); + assert Map_Contains(ts->val->val[ref_t]->stack->val, ref_n); + node := ts->val->val[ref_t]->stack->val->val[ref_n]; } -yield procedure {:layer 0} LoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X); +yield procedure {:layer 2} LoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X) refines AtomicLoadNode; - -right action {:layer 1, 2} AtomicAllocInStack(ref_t: RefTreiber X, node: Node X) returns (ref_n: Lval (RefNode X)) -modifies ts; +preserves call YieldInv#2(ref_t); { - assert ts->dom[ref_t]; - call ref_n := Lheap_Alloc(ts->val[ref_t]->stack, node); + call node := LoadNode#0(ref_t, ref_n); } -yield procedure {:layer 0} AllocInStack(ref_t: RefTreiber X, node: Node X) returns (ref_n: Lval (RefNode X)); -refines AtomicAllocInStack; atomic action {:layer 3} AtomicWriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool) modifies ts; { - assert NilDomain(ts, ref_t, unused)[new_ref_n]; + assert NilDomain(ts, ref_t)[new_ref_n]; call r := AtomicWriteTopOfStack(ref_t, old_ref_n, new_ref_n); } yield procedure {:layer 2} WriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool) @@ -200,12 +203,42 @@ preserves call YieldInv#2(ref_t); call r := WriteTopOfStack(ref_t, old_ref_n, new_ref_n); } +atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X) +{ + assert Map_Contains(ts->val, ref_t); + ref_n := ts->val->val[ref_t]->top; +} +yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X); +refines AtomicReadTopOfStack; + +atomic action {:layer 1,2} AtomicLoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X) +{ + assume Map_Contains(ts->val, ref_t); + assume Map_Contains(ts->val->val[ref_t]->stack->val, ref_n); + node := ts->val->val[ref_t]->stack->val->val[ref_n]; +} +yield procedure {:layer 0} LoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X); +refines AtomicLoadNode#0; + +left action {:layer 1, 2} AtomicAllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X)) +modifies ts; +{ + var lmap_n', lmap_n'': Lheap (Node X); + assert Map_Contains(ts->val, ref_t); + call lmap_n'', lmap_n' := Lmap_Move(lmap_n, ts->val->val[ref_t]->stack, ref_n); + ts->val->val[ref_t]->stack := lmap_n'; +} +yield procedure {:layer 0} AllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X)); +refines AtomicAllocNode; + 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; { - 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); + var top: RefNode X; + assert Map_Contains(ts->val, ref_t); + top := ts->val->val[ref_t]->top; + if (old_ref_n == top) { + ts->val->val[ref_t]->top := new_ref_n; r := true; } else { @@ -215,73 +248,80 @@ modifies ts; yield procedure {:layer 0} WriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool); refines AtomicWriteTopOfStack; -atomic action {:layer 1, 4} AtomicAlloc#0() returns (ref_t: Lval (RefTreiber X)) +atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X) modifies ts; { - var top: Ref (Node X); - var stack: Lheap (Node X); - var treiber: Treiber X; - top := Nil(); - call stack := Lheap_Empty(); - treiber := Treiber(top, stack); - call ref_t := Lheap_Alloc(ts, treiber); + var lmap_t': Lheap (Treiber X); + call lmap_t', ts := Lmap_Move(lmap_t, ts, ref_t); } -yield procedure {:layer 0} Alloc#0() returns (ref_t: Lval (RefTreiber X)); -refines AtomicAlloc#0; +yield procedure {:layer 0} AllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X); +refines AtomicAllocTreiber; -function {:inline} Domain(ts: Lheap (Treiber X), ref_t: RefTreiber X, unused: [RefTreiber X][RefNode X]bool): [RefNode X]bool { - Difference(ts->val[ref_t]->stack->dom, unused[ref_t]) +function {:inline} NilDomain(ts: Lheap (Treiber X), ref_t: RefTreiber X): [RefNode X]bool { + ts->val->val[ref_t]->stack->val->dom->val[Nil() := true] } -function {:inline} NilDomain(ts: Lheap (Treiber X), ref_t: RefTreiber X, unused: [RefTreiber X][RefNode X]bool): [RefNode X]bool { - Union(Singleton(Nil()), Domain(ts, ref_t, unused)) -} +yield invariant {:layer 1} YieldInv#1(ref_t: RefTreiber X, ref_n: RefNode X); +invariant Map_Contains(ts->val, ref_t); +invariant ts->val->val[ref_t]->stack->val->dom->val[ref_n]; yield invariant {:layer 2} YieldInv#2(ref_t: RefTreiber X); -invariant ts->dom[ref_t]; -invariant Subset(unused[ref_t], ts->val[ref_t]->stack->dom); -invariant NilDomain(ts, ref_t, unused)[ts->val[ref_t]->top]; +invariant Map_Contains(ts->val, ref_t); +invariant NilDomain(ts, ref_t)[ts->val->val[ref_t]->top]; yield invariant {:layer 3} YieldInv#3(ref_t: RefTreiber X); -invariant ts->dom[ref_t]; -invariant Subset(unused[ref_t], ts->val[ref_t]->stack->dom); -invariant NilDomain(ts, ref_t, unused)[ts->val[ref_t]->top]; -invariant (forall ref_n: RefNode X :: Domain(ts, ref_t, unused)[ref_n] ==> NilDomain(ts, ref_t, unused)[ts->val[ref_t]->stack->val[ref_n]->next]); +invariant Map_Contains(ts->val, ref_t); +invariant NilDomain(ts, ref_t)[ts->val->val[ref_t]->top]; +invariant (var t := ts->val->val[ref_t]; (var m := t->stack->val; (forall ref_n: RefNode X :: m->dom->val[ref_n] ==> NilDomain(ts, ref_t)[m->val[ref_n]->next]))); -// Boogie currently does not support termination proofs for functions or procedures. // The following is a manual encoding of the termination proof for the abstraction. -function Abs(ref_n: RefNode X, stackContents: [RefNode X]Node X): Vec X; -pure procedure AbsDefinition(ref_n: RefNode X, stackContents: [RefNode X]Node X) -requires Between(stackContents, ref_n, ref_n, Nil()); -ensures Abs(ref_n, stackContents) == - if ref_n == Nil() then - Vec_Empty() else - (var n := stackContents[ref_n]; Vec_Append(Abs(n->next, stackContents), n->val)); -{ - var stack: Vec X; - call stack := AbsCompute(ref_n, stackContents); -} -pure procedure AbsCompute(ref_n: RefNode X, stackContents: [RefNode X]Node X) returns (stack: Vec X) -requires Between(stackContents, ref_n, ref_n, Nil()); -ensures stack == +function Abs(ref_n: RefNode X, map: Map (RefNode X) (Node X)): Vec X; + +pure procedure AbsCompute(ref_n: RefNode X, map: Map (RefNode X) (Node X)) returns (absStack: Vec X) +requires Between(map->val, ref_n, ref_n, Nil()); +requires IsSubset(BetweenSet(map->val, ref_n, Nil()), map->dom->val[Nil() := true]); +ensures absStack == if ref_n == Nil() then Vec_Empty() else - (var n := stackContents[ref_n]; Vec_Append(Abs(n->next, stackContents), n->val)); -// trusted fact justified by induction and determinism of AbsCompute -free ensures stack == Abs(ref_n, stackContents); + (var n := Map_At(map, ref_n); Vec_Append(Abs(n->next, map), n->val)); +free ensures absStack == Abs(ref_n, map); { var n: Node X; if (ref_n == Nil()) { - stack := Vec_Empty(); + absStack := Vec_Empty(); } else { - n := stackContents[ref_n]; - // termination argument for induction - assert Between(stackContents, ref_n, n->next, Nil()); - call stack := AbsCompute(n->next, stackContents); - stack := Vec_Append(stack, n->val); + assert Map_Contains(map, ref_n); // soundness of framing + n := Map_At(map, ref_n); + assert Between(map->val, ref_n, n->next, Nil()); // soundness of termination (for induction) + call absStack := AbsCompute(n->next, map); + absStack := Vec_Append(absStack, n->val); } } +pure procedure AbsLemma(ref_n: RefNode X, map: Map (RefNode X) (Node X)) +requires Between(map->val, ref_n, ref_n, Nil()); +requires IsSubset(BetweenSet(map->val, ref_n, Nil()), map->dom->val[Nil() := true]); +ensures Abs(ref_n, map) == + if ref_n == Nil() then + Vec_Empty() else + (var n := Map_At(map, ref_n); Vec_Append(Abs(n->next, map), n->val)); +{ + var absStack: Vec X; + call absStack := AbsCompute(ref_n, map); +} + +pure procedure FrameLemma(ref_n: RefNode X, map: Map (RefNode X) (Node X), map': Map (RefNode X) (Node X)); +requires Between(map->val, ref_n, ref_n, Nil()); +requires IsSubset(BetweenSet(map->val, ref_n, Nil()), map->dom->val[Nil() := true]); +requires IsSubset(map->dom->val, map'->dom->val); +requires MapIte(map->dom->val, map->val, MapConst(Default())) == MapIte(map->dom->val, map'->val, MapConst(Default())); +ensures Abs(ref_n, map) == Abs(ref_n, map'); + yield invariant {:layer 4} YieldInv#4(ref_t: RefTreiber X); -invariant Stack[ref_t] == (var t := ts->val[ref_t]; Abs(t->top, t->stack->val)); -invariant (var t := ts->val[ref_t]; Between(t->stack->val, t->top, t->top, Nil())); +invariant Map_Contains(ts->val, ref_t); +invariant Map_At(Stack, ref_t) == (var t := ts->val->val[ref_t]; Abs(t->top, t->stack->val)); +invariant (var t := ts->val->val[ref_t]; Between(t->stack->val->val, t->top, t->top, Nil())); +invariant (var t := ts->val->val[ref_t]; IsSubset(BetweenSet(t->stack->val->val, t->top, Nil()), NilDomain(ts, ref_t))); + +yield invariant {:layer 4} YieldInvDom#4(); +invariant Stack->dom == ts->val->dom; diff --git a/Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/samples/treiber-stack.bpl.expect index d996ab7ab..f25efc0fa 100644 --- a/Test/civl/samples/treiber-stack.bpl.expect +++ b/Test/civl/samples/treiber-stack.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 43 verified, 0 errors +Boogie program verifier finished with 47 verified, 0 errors diff --git a/Test/datatypes/node-client.bpl b/Test/datatypes/node-client.bpl index f4715b7cd..54b363733 100644 --- a/Test/datatypes/node-client.bpl +++ b/Test/datatypes/node-client.bpl @@ -1,19 +1,19 @@ // RUN: %parallel-boogie /lib:base /lib:node "%s" > "%t" // RUN: %diff "%s.expect" "%t" -datatype Treiber { Treiber(top: RefNode T, stack: Lheap (Node T)) } +datatype Treiber { Treiber(top: RefNode T, stack: Lmap (RefNode T) (Node T)) } type RefTreiber T = Ref (Treiber T); type X; -var ts: Lheap (Treiber X); +var ts: Lmap (RefTreiber X) (Treiber X); procedure YieldInv(ref_t: RefTreiber X) -requires ts->dom[ref_t]; -requires BetweenSet(ts->val[ref_t]->stack->val, ts->val[ref_t]->top, Nil())[ts->val[ref_t]->top]; -requires Subset(BetweenSet(ts->val[ref_t]->stack->val, ts->val[ref_t]->top, Nil()), Union(Singleton(Nil()), ts->val[ref_t]->stack->dom)); -ensures ts->dom[ref_t]; -ensures BetweenSet(ts->val[ref_t]->stack->val, ts->val[ref_t]->top, Nil())[ts->val[ref_t]->top]; -ensures Subset(BetweenSet(ts->val[ref_t]->stack->val, ts->val[ref_t]->top, Nil()), Union(Singleton(Nil()), ts->val[ref_t]->stack->dom)); +requires Map_Contains(ts->val, ref_t); +requires (var t := Map_At(ts->val, ref_t); BetweenSet(t->stack->val->val, t->top, Nil())[t->top]); +requires (var t := Map_At(ts->val, ref_t); (var m := t->stack->val; IsSubset(BetweenSet(m->val, t->top, Nil()), m->dom->val[Nil() := true]))); +ensures Map_Contains(ts->val, ref_t); +ensures (var t := Map_At(ts->val, ref_t); BetweenSet(t->stack->val->val, t->top, Nil())[t->top]); +ensures (var t := Map_At(ts->val, ref_t); (var m := t->stack->val; IsSubset(BetweenSet(m->val, t->top, Nil()), m->dom->val[Nil() := true]))); modifies ts; { var x: X; @@ -25,17 +25,26 @@ procedure {:inline 1} AtomicPopIntermediate(ref_t: RefTreiber X) returns (x: X) modifies ts; { var ref_n: RefNode X; - 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); + assert Map_Contains(ts->val, ref_t); + assume ts->val->val[ref_t]->top != Nil() && Map_Contains(ts->val->val[ref_t]->stack->val, ts->val->val[ref_t]->top); + Node(ref_n, x) := Map_At(ts->val->val[ref_t]->stack->val, ts->val->val[ref_t]->top); + ts->val->val[ref_t]->top := ref_n; } procedure {:inline 1} AtomicPushIntermediate(ref_t: RefTreiber X, x: X) modifies ts; { - 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); + var t: RefNode X; + var ref_n: RefNode X; + var loc_n: Lval (Loc (Node X)); + var lmap_n: Lmap (RefNode X) (Node X); + var lmap_n': Lmap (RefNode X) (Node X); + assert Map_Contains(ts->val, ref_t); + t := ts->val->val[ref_t]->top; + call loc_n, lmap_n := Lmap_Alloc(Node(t, x)); + call Lmap_Assume(lmap_n, ts->val->val[ref_t]->stack); + ref_n := Ref(loc_n->val); + call lmap_n, lmap_n' := Lmap_Move(lmap_n, ts->val->val[ref_t]->stack, ref_n); + ts->val->val[ref_t]->stack := lmap_n'; + ts->val->val[ref_t]->top := ref_n; }