diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 00525562c..03c502191 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -19,6 +19,7 @@ public class YieldingProcDuplicator : Duplicator private Dictionary procToDuplicate; /* Original -> Duplicate */ private AbsyMap absyMap; /* Duplicate -> Original */ private Dictionary asyncCallPreconditionCheckers; + private Dictionary noRequiresPureProcedures; private LinearRewriter linearRewriter; @@ -31,6 +32,7 @@ public YieldingProcDuplicator(CivlTypeChecker civlTypeChecker, int layerNum, boo this.procToDuplicate = []; this.absyMap = new AbsyMap(); this.asyncCallPreconditionCheckers = []; + this.noRequiresPureProcedures = []; this.linearRewriter = new LinearRewriter(civlTypeChecker); this.doRefinementCheck = doRefinementCheck; } @@ -129,13 +131,9 @@ public override Ensures VisitEnsures(Ensures node) #region Implementation duplication private YieldProcedureDecl enclosingYieldingProc; - private Block enclosingBlock; - private bool inPredicatePhase; private List newCmdSeq; - private Dictionary returnedPAs; - private Dictionary addedLocalVariables; public override Implementation VisitImplementation(Implementation impl) @@ -143,13 +141,11 @@ public override Implementation VisitImplementation(Implementation impl) enclosingYieldingProc = (YieldProcedureDecl)impl.Proc; Debug.Assert(layerNum <= enclosingYieldingProc.Layer); - returnedPAs = new Dictionary(); addedLocalVariables = new Dictionary(); Implementation newImpl = base.VisitImplementation(impl); newImpl.Name = newImpl.Proc.Name; - newImpl.LocVars.AddRange(returnedPAs.Values); newImpl.LocVars.AddRange(addedLocalVariables.Values); absyMap[newImpl] = impl; @@ -158,9 +154,7 @@ public override Implementation VisitImplementation(Implementation impl) public override Block VisitBlock(Block node) { - enclosingBlock = node; var block = base.VisitBlock(node); - enclosingBlock = null; absyMap[block] = node; return block; } @@ -173,19 +167,7 @@ public override Cmd VisitAssertCmd(AssertCmd node) assertCmd.Expr = Expr.True; return assertCmd; } - if (layerNum != enclosingYieldingProc.Layer) - { - return assertCmd; - } - bool insideLoopInvariantOfYieldingLoop = enclosingYieldingProc.IsYieldingLoopHeaderAtProcedureLayer(enclosingBlock) && inPredicatePhase; - if (insideLoopInvariantOfYieldingLoop) - { - return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd; - } - else - { - return doRefinementCheck ? assertCmd : new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes); - } + return doRefinementCheck ? new AssumeCmd(node.tok, assertCmd.Expr, node.Attributes) : assertCmd; } public override Cmd VisitCallCmd(CallCmd call) @@ -209,7 +191,6 @@ public override Cmd VisitParCallCmd(ParCallCmd parCall) public override List VisitCmdSeq(List cmdSeq) { newCmdSeq = new List(); - inPredicatePhase = true; foreach (var cmd in cmdSeq) { Cmd newCmd = (Cmd) Visit(cmd); @@ -225,7 +206,6 @@ public override List VisitCmdSeq(List cmdSeq) { newCmdSeq.Add(newCmd); } - inPredicatePhase = inPredicatePhase && (cmd is PredicateCmd || cmd is CallCmd callCmd && callCmd.Proc is YieldInvariantDecl); } return newCmdSeq; } @@ -302,7 +282,7 @@ cmd is AssertCmd assertCmd && makeAssume } else { - newCmdSeq.Add(newCall); + DesugarPureCall(newCall); } } return; @@ -553,21 +533,39 @@ private void AddDuplicateCall(CallCmd newCall, bool makeParallel) private void DesugarAsyncCall(CallCmd newCall) { - if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name)) + if (!asyncCallPreconditionCheckers.TryGetValue(newCall.Proc.Name, out Procedure checker)) { - asyncCallPreconditionCheckers[newCall.Proc.Name] = DeclHelper.Procedure( + checker = DeclHelper.Procedure( civlTypeChecker.AddNamePrefix($"AsyncCall_{newCall.Proc.Name}_{layerNum}"), newCall.Proc.InParams, newCall.Proc.OutParams, procToDuplicate[newCall.Proc].Requires, [], [], []); + asyncCallPreconditionCheckers[newCall.Proc.Name] = checker; } - - var asyncCallPreconditionChecker = asyncCallPreconditionCheckers[newCall.Proc.Name]; newCall.IsAsync = false; - newCall.Proc = asyncCallPreconditionChecker; + newCall.Proc = checker; newCall.callee = newCall.Proc.Name; newCmdSeq.Add(newCall); } + private void DesugarPureCall(CallCmd newCall) + { + if (doRefinementCheck) + { + if (!noRequiresPureProcedures.TryGetValue(newCall.Proc.Name, out Procedure checker)) + { + checker = DeclHelper.Procedure( + civlTypeChecker.AddNamePrefix($"NoRequires_{newCall.Proc.Name}_{layerNum}"), + newCall.Proc.InParams, newCall.Proc.OutParams, + [], [], new List(newCall.Proc.Ensures), []); + noRequiresPureProcedures[newCall.Proc.Name] = checker; + } + newCall.IsAsync = false; + newCall.Proc = checker; + newCall.callee = newCall.Proc.Name; + } + newCmdSeq.Add(newCall); + } + #endregion public List Collect() @@ -577,6 +575,7 @@ public List Collect() var newImpls = absyMap.Keys.OfType(); decls.AddRange(newImpls); decls.AddRange(asyncCallPreconditionCheckers.Values); + decls.AddRange(noRequiresPureProcedures.Values); decls.AddRange(YieldingProcInstrumentation.TransformImplementations( civlTypeChecker, layerNum, diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 5d8bb4b40..915ce10cf 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -3301,11 +3301,6 @@ public bool IsYieldingLoopHeader(Block block, int layerNum) } return layerNum <= YieldingLoops[block].Layer; } - - public bool IsYieldingLoopHeaderAtProcedureLayer(Block block) - { - return IsYieldingLoopHeader(block, Layer); - } } public class LoopProcedure : Procedure diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs index e3a0ee3ae..e3e84687a 100644 --- a/Source/Core/AST/Commands/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -283,55 +283,59 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) return; } + void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureDecl calleeDecl) + { + var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer); + var calleeRefinedAction = calleeDecl.RefinedAction; + while (calleeRefinedAction != null) + { + var calleeActionDecl = calleeRefinedAction.ActionDecl; + if (!calleeActionDecl.IsLeftMover) + { + tc.Error(this, + $"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}"); + break; + } + if (calleeActionDecl == highestRefinedActionDecl) + { + break; + } + calleeRefinedAction = calleeActionDecl.RefinedAction; + } + } + // check layers if (Proc is YieldProcedureDecl calleeDecl) { - var isSynchronized = this.HasAttribute(CivlAttributes.SYNC); if (calleeDecl.Layer > callerDecl.Layer) { tc.Error(this, "layer of callee must not be more than layer of caller"); + return; + } + if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null) + { + return; } - else if (!calleeDecl.HasMoverType) + var isSynchronized = this.HasAttribute(CivlAttributes.SYNC); + if (IsAsync && !isSynchronized) { + tc.Error(this, "async call must be synchronized"); + return; + } + // call is synchronous or synchronized + if (!calleeDecl.HasMoverType) + { + Debug.Assert(calleeDecl.RefinedAction != null); if (callerDecl.Layer > calleeDecl.Layer) { - if (calleeDecl.RefinedAction != null) + var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer); + if (highestRefinedActionDecl == null) { - var highestRefinedActionDecl = calleeDecl.RefinedActionAtLayer(callerDecl.Layer); - if (highestRefinedActionDecl == null) - { - tc.Error(this, $"called action is not available at layer {callerDecl.Layer}"); - } - else - { - if (IsAsync) - { - if (isSynchronized) - { - // check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers - var calleeRefinedAction = calleeDecl.RefinedAction; - while (calleeRefinedAction != null) - { - var calleeActionDecl = calleeRefinedAction.ActionDecl; - if (!calleeActionDecl.IsLeftMover) - { - tc.Error(this, - $"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}"); - break; - } - if (calleeActionDecl == highestRefinedActionDecl) - { - break; - } - calleeRefinedAction = calleeActionDecl.RefinedAction; - } - } - else if (callerDecl.HasMoverType) - { - tc.Error(this, "async call must be synchronized in mover procedure"); - } - } - } + tc.Error(this, $"called action is not available at layer {callerDecl.Layer}"); + } + else if (IsAsync) + { + CheckRefinedChainIsLeftMover(callerDecl, calleeDecl); } } else // callerDecl.Layer == calleeDecl.Layer @@ -340,20 +344,9 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) { tc.Error(this, "caller must not be a mover procedure"); } - else if (IsAsync && calleeDecl.RefinedAction != null) + else if (IsAsync) { - if (isSynchronized) - { - tc.Error(this, "layer of callee in synchronized call must be less than layer of caller"); - } - else - { - var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1); - if (highestRefinedAction == null) - { - tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}"); - } - } + tc.Error(this, "layer of callee in synchronized call must be less than layer of caller"); } } } @@ -363,18 +356,12 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) { tc.Error(this, "layer of caller must be equal to layer of callee"); } - else + else if (IsAsync) { - if (IsAsync) + Debug.Assert(isSynchronized); + if (!calleeDecl.IsLeftMover) { - if (!isSynchronized) - { - tc.Error(this, "async call to mover procedure must be synchronized"); - } - else if (!calleeDecl.IsLeftMover) - { - tc.Error(this, "callee in synchronized call must be a left mover"); - } + tc.Error(this, "callee in synchronized call must be a left mover"); } } } @@ -402,7 +389,7 @@ private void TypecheckCallCmdInYieldProcedureDecl(TypecheckingContext tc) } else { - // Check global outputs only; the checking of local outputs is done later + // Check global outputs only; the checking of local outputs is done separately var calleeLayer = Layers[0]; var globalOutputs = Outs.Select(ie => ie.Decl).OfType().Cast(); if (CivlPrimitives.LinearPrimitives.Contains(Proc.Name)) @@ -513,7 +500,8 @@ public override void Typecheck(TypecheckingContext tc) var actual = Outs[i]; if (actual.Decl is GlobalVariable) { - if (!Proc.IsPure) // global outputs of pure calls already checked + // layer range for global outputs of pure calls checked in TypecheckCallCmdInYieldProcedureDecl + if (!Proc.IsPure) { tc.Error(actual, $"global variable directly modified in a yield procedure: {actual.Decl.Name}"); } @@ -537,7 +525,7 @@ public override void Typecheck(TypecheckingContext tc) } else if (modifiedArgument is { Decl: GlobalVariable }) { - // already done in TypecheckCallCmdInYieldProcedureDecl + // checked in TypecheckCallCmdInYieldProcedureDecl } else { diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 01eb323c1..5437c72ad 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -338,3 +338,8 @@ datatype Unit { Unit() } function {:inline} UnitSet(): Set Unit { Set_Add(Set_Empty(), Unit()) } + +pure action Assert(b: bool) +{ + assert b; +} diff --git a/Test/civl/large-samples/GC.bpl b/Test/civl/large-samples/GC.bpl index deff1b20c..9afc7773a 100644 --- a/Test/civl/large-samples/GC.bpl +++ b/Test/civl/large-samples/GC.bpl @@ -301,7 +301,7 @@ preserves call Yield_Iso(); preserves call Yield_Lock(); requires {:layer 95, 96, 99} tid->i == i; { - assert {:layer 100} mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]); + call {:layer 100} Assert(mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x])); call WriteBarrier(tid, i, y); call Yield_Iso() | Yield_WriteField(tid, x, y); call WriteFieldRaw(tid, x, f, y) | Yield_Lock(); @@ -1936,7 +1936,8 @@ refines AtomicLockAcquire; preserves call Yield_Lock(); { var status:bool; - assert {:layer 95} tid->i != 0; + + call {:layer 95} Assert(tid->i != 0); while (true) invariant {:yields} true; invariant call Yield_Lock(); diff --git a/Test/civl/large-samples/cache-coherence.bpl b/Test/civl/large-samples/cache-coherence.bpl index 7a04b6019..accb3ca57 100644 --- a/Test/civl/large-samples/cache-coherence.bpl +++ b/Test/civl/large-samples/cache-coherence.bpl @@ -357,7 +357,7 @@ refines atomic action {:layer 2} _ { call Set_Put(cachePermissions, drp); } { - assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma)))); + call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma))))); call cache_evict_resp#0(i, ma); call {:layer 1} Set_Put(cachePermissions, drp); } @@ -397,7 +397,7 @@ refines left action {:layer 2} _ { call Set_Put(cachePermissions, drp); } { - assert {:layer 1} Set_Contains(drp, One(CachePermission(i, Hash(ma)))); + call {:layer 1} Assert(Set_Contains(drp, One(CachePermission(i, Hash(ma))))); call cache_read_resp#0(i, ma, v, s); call {:layer 1} Set_Put(cachePermissions, drp); } @@ -722,7 +722,7 @@ refines left action {:layer 2} _ { call Set_Put(dirPermissions, dp); } { - assert {:layer 1} dp == WholeDirPermission(ma); + call {:layer 1} Assert(dp == WholeDirPermission(ma)); call dir_req_end#0(ma, dirState); call {:layer 1} Set_Put(dirPermissions, dp); } diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl index 4ba4edd03..93a20a0a2 100644 --- a/Test/civl/large-samples/shared-vector.bpl +++ b/Test/civl/large-samples/shared-vector.bpl @@ -157,8 +157,8 @@ preserves call Yield(loc_iv); return; } - assert {:layer 2} Map_Contains(IntArrayPool, One(loc_iv)); - assert {:layer 2} (var vec := Map_At(IntArrayPool, One(loc_iv)); Vec_Contains(vec, i) && Vec_Contains(vec, j)); + call {:layer 2} Assert(Map_Contains(IntArrayPool, One(loc_iv))); + call {:layer 2} Assert((var vec := Map_At(IntArrayPool, One(loc_iv)); Vec_Contains(vec, i) && Vec_Contains(vec, j))); // deadlock avoidance if (i < j) { diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index fa7ba7af2..299d11801 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -178,7 +178,7 @@ refines left action {:layer 2} _ { status[r] := Proposed(v); } { - assert {:layer 1} voteInfo[r] == MapConst(false); + call {:layer 1} Assert(voteInfo[r] == MapConst(false)); call {:layer 1} status := Copy(status[r := Proposed(v)]); } @@ -296,7 +296,7 @@ refines left action {:layer 2} _ { status[r] := Decided(v); } { - assert {:layer 1} status[r] == Proposed(v); + call {:layer 1} Assert(status[r] == Proposed(v)); call {:layer 1} status := Copy(status[r := Decided(v)]); } @@ -363,8 +363,8 @@ requires call YieldInv(); { var voteResponse: VoteResponse; - assert {:layer 1} IsActive(status[r], v); - assert {:layer 1} !voteInfo[r][n]; + call {:layer 1} Assert(IsActive(status[r], v)); + call {:layer 1} Assert(!voteInfo[r][n]); call voteResponse := VoteUpdate(r, n, v); call SendVoteResponse(r, voteResponse); if (voteResponse is VoteAccept) { diff --git a/Test/civl/regression-tests/Pure.bpl b/Test/civl/regression-tests/Pure.bpl new file mode 100644 index 000000000..a45262d04 --- /dev/null +++ b/Test/civl/regression-tests/Pure.bpl @@ -0,0 +1,34 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +pure procedure A(a: int) returns (b: int); +requires false; +ensures b == a; + +yield procedure {:layer 1} X1(a: int) returns ({:layer 1} b: int) +refines atomic action {:layer 2} _ { b := a; } +{ + call {:layer 1} b := A(a); +} + +yield procedure {:layer 2} X2(a: int) returns ({:layer 1} b: int) +{ + call {:layer 1} b := A(a); +} + +pure action B(x:int) +{ + assert x >= 0; +} + +yield procedure {:layer 1} Y1(x:int) +refines atomic action {:layer 2} _ { assert x == 0; } +{ + call {:layer 1} B(x); +} + +yield procedure {:layer 2} Y2(x:int) +{ + call {:layer 1} B(x); +} + diff --git a/Test/civl/regression-tests/Pure.bpl.expect b/Test/civl/regression-tests/Pure.bpl.expect new file mode 100644 index 000000000..6f8224924 --- /dev/null +++ b/Test/civl/regression-tests/Pure.bpl.expect @@ -0,0 +1,13 @@ +Pure.bpl(11,5): Error: a precondition for this call could not be proved +Pure.bpl(5,1): Related location: this is the precondition that could not be proved +Execution trace: + Pure.bpl(11,5): anon0 +Pure.bpl(16,5): Error: a precondition for this call could not be proved +Pure.bpl(5,1): Related location: this is the precondition that could not be proved +Execution trace: + Pure.bpl(16,5): anon0 +Pure.bpl(21,3): Error: this gate of B could not be proved +Execution trace: + Pure.bpl(32,3): anon0 + +Boogie program verifier finished with 7 verified, 3 errors diff --git a/Test/civl/regression-tests/Pure2.bpl b/Test/civl/regression-tests/Pure2.bpl deleted file mode 100644 index e15c921ae..000000000 --- a/Test/civl/regression-tests/Pure2.bpl +++ /dev/null @@ -1,20 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -var {:layer 1,1} g:int; - -pure action P(x:int) -{ - assert x >= 0; -} - -yield procedure {:layer 1} X(x:int) -{ - call {:layer 1} P(x); -} - -yield procedure {:layer 1} Y(x:int) -{ - assert {:layer 1} x == 0; - call {:layer 1} P(x); -} diff --git a/Test/civl/regression-tests/Pure2.bpl.expect b/Test/civl/regression-tests/Pure2.bpl.expect deleted file mode 100644 index 498d2d4f6..000000000 --- a/Test/civl/regression-tests/Pure2.bpl.expect +++ /dev/null @@ -1,8 +0,0 @@ -Pure2.bpl(8,3): Error: this gate of P could not be proved -Execution trace: - Pure2.bpl(13,3): anon0 -Pure2.bpl(18,3): Error: this assertion could not be proved -Execution trace: - Pure2.bpl(18,3): anon0 - -Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/civl/regression-tests/anonymous-action.bpl b/Test/civl/regression-tests/anonymous-action.bpl index df33a221f..ef442ef48 100644 --- a/Test/civl/regression-tests/anonymous-action.bpl +++ b/Test/civl/regression-tests/anonymous-action.bpl @@ -18,11 +18,5 @@ refines both action {:layer 2} _ { yield procedure {:layer 0} C(i: int) returns (j: int); refines both action {:layer 1} AC { - call Incr(); -} - -action {:layer 1} Incr() -modifies x; -{ x := x + 1; -} \ No newline at end of file +} diff --git a/Test/civl/regression-tests/chris5.bpl b/Test/civl/regression-tests/chris5.bpl index 8cdac2caf..fa96e3728 100644 --- a/Test/civl/regression-tests/chris5.bpl +++ b/Test/civl/regression-tests/chris5.bpl @@ -1,12 +1,9 @@ -// RUN: %parallel-boogie /trustRefinement "%s" > "%t" +// RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" -// flag /trustRefinement avoids duplicate error messages since the inlined assert in P -// is checked during both invariant checking and refinement checking at layer 1 - var {:layer 1,1} g:int; -pure procedure {:inline 1} P(x:int) +pure action P(x:int) { assert x == 0; } diff --git a/Test/civl/regression-tests/chris5.bpl.expect b/Test/civl/regression-tests/chris5.bpl.expect index 3559e0ac9..92f59e8e7 100644 --- a/Test/civl/regression-tests/chris5.bpl.expect +++ b/Test/civl/regression-tests/chris5.bpl.expect @@ -1,6 +1,5 @@ -chris5.bpl(11,3): Error: this assertion could not be proved +chris5.bpl(8,3): Error: this gate of P could not be proved Execution trace: - chris5.bpl(16,3): anon0 - chris5.bpl(11,3): inline$P$0$anon0 + chris5.bpl(13,3): anon0 -Boogie program verifier finished with 0 verified, 1 error +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/civl/regression-tests/ghost.bpl b/Test/civl/regression-tests/ghost.bpl index 6404130fa..bbca1319f 100644 --- a/Test/civl/regression-tests/ghost.bpl +++ b/Test/civl/regression-tests/ghost.bpl @@ -9,7 +9,7 @@ modifies x; yield procedure {:layer 0} Incr(); refines AtomicIncr; -pure procedure {:inline 1} ghost(y: int) returns (z: int) +pure action ghost(y: int) returns (z: int) { z := y + 1; } diff --git a/Test/civl/regression-tests/issue-1005.bpl.expect b/Test/civl/regression-tests/issue-1005.bpl.expect index 8012fbc41..192505590 100644 --- a/Test/civl/regression-tests/issue-1005.bpl.expect +++ b/Test/civl/regression-tests/issue-1005.bpl.expect @@ -1,2 +1,2 @@ -issue-1005.bpl(14,10): Error: async call must be synchronized in mover procedure +issue-1005.bpl(14,10): Error: async call must be synchronized 1 type checking errors detected in issue-1005.bpl diff --git a/Test/civl/samples/ABD.bpl b/Test/civl/samples/ABD.bpl index fdc613dfe..9815afd6c 100644 --- a/Test/civl/samples/ABD.bpl +++ b/Test/civl/samples/ABD.bpl @@ -396,7 +396,7 @@ preserves call TimeStampQuorum(); assert {:layer 2} (exists q: ReplicaSet:: IsQuorum(q) && IsSubset(q, tsq)); } -pure procedure {:inline 1} CalculateQuorum(replica_ts: [ReplicaId]TimeStamp, ts: TimeStamp) returns (w: ReplicaSet) +pure action CalculateQuorum(replica_ts: [ReplicaId]TimeStamp, ts: TimeStamp) returns (w: ReplicaSet) { // calculate the set of all replica ids whose timestamp is at least ts w := (lambda rid: ReplicaId:: IsReplica(rid) && le(ts, replica_ts[rid])); diff --git a/Test/civl/samples/MutexOverFutex.bpl b/Test/civl/samples/MutexOverFutex.bpl index fe2b3dcd4..f44d02ed3 100644 --- a/Test/civl/samples/MutexOverFutex.bpl +++ b/Test/civl/samples/MutexOverFutex.bpl @@ -66,7 +66,7 @@ preserves call YieldInv(); preserves call YieldWait(tid); { var oldValue: int; - assert {:layer 1} mutex == Some(tid->val); + call {:layer 1} Assert(mutex == Some(tid->val)); call oldValue := FetchSub(1); if (oldValue == 1) { call {:layer 1} mutex := Copy(None()); diff --git a/Test/civl/samples/StoreBuffer.bpl b/Test/civl/samples/StoreBuffer.bpl index cce0a0f9a..d0b993545 100644 --- a/Test/civl/samples/StoreBuffer.bpl +++ b/Test/civl/samples/StoreBuffer.bpl @@ -75,8 +75,7 @@ requires {:layer 1} mutatorOrGcTid(tid->val); preserves call YieldLock(); preserves call YieldStoreBufferLockAddrAbsent(tid); { - assert {:layer 1} mutatorOrGcTid(tid->val); - assert {:layer 1} lock == tid->val; + call {:layer 1} Assert(lock == tid->val); call LockZero(tid->val); call YieldLock() | YieldStoreBufferLockAddrPresent(tid); call FlushStoreBufferEntryForLock(tid->val); @@ -114,9 +113,8 @@ refines AtomicSetCollectorPhase; requires {:layer 1} mutatorOrGcTid(tid->val); preserves call YieldLock(); { - assert {:layer 1} mutatorOrGcTid(tid->val); - assert {:layer 1} lock == tid->val; - assert {:layer 1} collectorPhase == collectorPhaseDelayed; + call {:layer 1} Assert(lock == tid->val); + call {:layer 1} Assert(collectorPhase == collectorPhaseDelayed); call PrimitiveSetCollectorPhase(tid->val, phase); } diff --git a/Test/civl/samples/array-insert.bpl b/Test/civl/samples/array-insert.bpl index 0fb21c791..4784c059a 100644 --- a/Test/civl/samples/array-insert.bpl +++ b/Test/civl/samples/array-insert.bpl @@ -47,6 +47,7 @@ requires {:layer 1} tid->val != nil; var c:int; // value read from count var {:layer 1} _A:[int]int; + call {:layer 1} Assert(0 <= count); call {:layer 1} _A := Copy(A); call acquire(tid); @@ -76,7 +77,7 @@ requires {:layer 1} tid->val != nil; call write_count(tid, c+1); // let's see if we can prove that A is still sorted - assert {:layer 1} sorted(A, count); + call {:layer 1} Assert(sorted(A, count)); call release(tid); } diff --git a/Test/civl/samples/tds.bpl b/Test/civl/samples/tds.bpl index b5284ae6d..2ce416c77 100644 --- a/Test/civl/samples/tds.bpl +++ b/Test/civl/samples/tds.bpl @@ -61,6 +61,7 @@ refines AtomicMain; var tids': Set (One int); var tid: One int; + call {:layer 1} Assert((forall i: int :: 0 <= i && i < n <==> Set_Contains(tids, One(i)))); i := 0; tids' := tids; call {:layer 1} snapshot := Copy(status);