diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs index cce5e03a4..fba0e2473 100644 --- a/Source/Concurrency/RefinementInstrumentation.cs +++ b/Source/Concurrency/RefinementInstrumentation.cs @@ -27,12 +27,7 @@ public virtual List CreateReturnAssertCmds() return new List(); } - public virtual List CreateUnchangedGlobalsAssertCmds() - { - return new List(); - } - - public virtual List CreateUnchangedOutputsAssertCmds() + public virtual List CreateUnchangedAssertCmds() { return new List(); } @@ -59,6 +54,7 @@ class ActionRefinementInstrumentation : RefinementInstrumentation private Expr gate; private Expr transitionRelation; private IToken tok; + private int layerNum; private Dictionary transitionRelationCache; @@ -72,7 +68,7 @@ public ActionRefinementInstrumentation( this.tok = impl.tok; this.oldGlobalMap = new Dictionary(); ActionProc actionProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc] as ActionProc; - int layerNum = actionProc.upperLayer; + this.layerNum = actionProc.upperLayer; foreach (Variable v in civlTypeChecker.GlobalVariables) { var layerRange = civlTypeChecker.GlobalVariableLayerRange(v); @@ -173,14 +169,14 @@ public override List CreateAssertCmds() var skipOrTransitionRelationAssertCmd = CmdHelper.AssertCmd( tok, Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), transitionRelation)), - "Transition invariant violated in initial state"); + $"A yield-to-yield fragment modifies layer-{layerNum + 1} state in a way that does not match the refined atomic action"); CivlUtil.ResolveAndTypecheck(skipOrTransitionRelationAssertCmd); // assert pc ==> g_old == g && o_old == o; AssertCmd skipAssertCmd = CmdHelper.AssertCmd( tok, Expr.Imp(Expr.Ident(pc), Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs())), - "Transition invariant violated in final state"); + $"A yield-to-yield fragment modifies layer-{layerNum + 1} state subsequent to a yield-to-yield fragment that already modified layer-{layerNum + 1} state"); CivlUtil.ResolveAndTypecheck(skipAssertCmd); return new List {skipOrTransitionRelationAssertCmd, skipAssertCmd}; @@ -191,29 +187,26 @@ public override List CreateReturnAssertCmds() AssertCmd assertCmd = CmdHelper.AssertCmd( tok, Expr.Ident(ok), - "Failed to execute atomic action before procedure return"); + "On some path no yield-to-yield fragment matched the refined atomic action"); return new List {assertCmd}; } - public override List CreateUnchangedGlobalsAssertCmds() + public override List CreateUnchangedAssertCmds() { - AssertCmd skipAssertCmd = CmdHelper.AssertCmd( + AssertCmd globalsAssertCmd = CmdHelper.AssertCmd( tok, Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value)))), - "Globals must not be modified"); - CivlUtil.ResolveAndTypecheck(skipAssertCmd); - return new List {skipAssertCmd}; - } + $"A yield-to-yield fragment illegally modifies layer-{layerNum + 1} globals"); + CivlUtil.ResolveAndTypecheck(globalsAssertCmd); - public override List CreateUnchangedOutputsAssertCmds() - { // assert pc ==> o_old == o; - AssertCmd skipAssertCmd = CmdHelper.AssertCmd( + AssertCmd outputsAssertCmd = CmdHelper.AssertCmd( tok, Expr.Imp(Expr.Ident(pc), OldEqualityExprForOutputs()), - "Outputs must not be modified"); - CivlUtil.ResolveAndTypecheck(skipAssertCmd); - return new List {skipAssertCmd}; + $"A yield-to-yield fragment illegally modifies layer-{layerNum + 1} outputs"); + CivlUtil.ResolveAndTypecheck(outputsAssertCmd); + + return new List {globalsAssertCmd, outputsAssertCmd}; } public override List CreateUpdatesToRefinementVars(bool isMarkedCall) @@ -224,7 +217,7 @@ public override List CreateUpdatesToRefinementVars(bool isMarkedCall) { // assert !pc; // pc, ok := true, true; - cmds.Add(CmdHelper.AssertCmd(tok, Expr.Not(Expr.Ident(pc)), "Visible state changed before marked call")); + cmds.Add(CmdHelper.AssertCmd(tok, Expr.Not(Expr.Ident(pc)), $"Layer-{layerNum + 1} state modified before marked call")); var pcOkUpdateRHS = new List {Expr.True, Expr.True}; cmds.Add(CmdHelper.AssignCmd(pcOkUpdateLHS, pcOkUpdateRHS)); } diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 1357b1004..ed9760580 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -412,7 +412,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) { var noninterferenceCheckerBlock = CreateNoninterferenceCheckerBlock(); var refinementCheckerBlock = CreateRefinementCheckerBlock(); - var refinementCheckerForYieldingLoopsBlock = CreateRefinementCheckerBlockForYieldingLoops(); + var unchangedCheckerBlock = CreateUnchangedCheckerBlock(); var returnCheckerBlock = CreateReturnCheckerBlock(); var returnBlock = BlockHelper.Block(civlTypeChecker.AddNamePrefix("UnifiedReturn"), new List()); SplitBlocks(impl); @@ -428,7 +428,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) AddEdge(gotoCmd, noninterferenceCheckerBlock); if (blocksInYieldingLoops.Contains(pred)) { - AddEdge(gotoCmd, refinementCheckerForYieldingLoopsBlock); + AddEdge(gotoCmd, unchangedCheckerBlock); } else { @@ -479,7 +479,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) FixUpImplRefinementCheckingBlock(targetBlock, IsCallMarked(callCmd) ? returnCheckerBlock - : refinementCheckerForYieldingLoopsBlock); + : unchangedCheckerBlock); targetBlocks.Add(targetBlock); implRefinementCheckingBlocks.Add(targetBlock); } @@ -496,7 +496,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) AddEdge(gotoCmd, noninterferenceCheckerBlock); AddEdge(gotoCmd, blocksInYieldingLoops.Contains(b) - ? refinementCheckerForYieldingLoopsBlock + ? unchangedCheckerBlock : refinementCheckerBlock); } } @@ -526,7 +526,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) impl.Blocks.Add(noninterferenceCheckerBlock); impl.Blocks.Add(refinementCheckerBlock); - impl.Blocks.Add(refinementCheckerForYieldingLoopsBlock); + impl.Blocks.Add(unchangedCheckerBlock); impl.Blocks.Add(returnCheckerBlock); impl.Blocks.Add(returnBlock); impl.Blocks.AddRange(implRefinementCheckingBlocks); @@ -614,13 +614,12 @@ private Block CreateRefinementCheckerBlock() return BlockHelper.Block(civlTypeChecker.AddNamePrefix("RefinementChecker"), newCmds); } - private Block CreateRefinementCheckerBlockForYieldingLoops() + private Block CreateUnchangedCheckerBlock() { var newCmds = new List(); - newCmds.AddRange(refinementInstrumentation.CreateUnchangedGlobalsAssertCmds()); - newCmds.AddRange(refinementInstrumentation.CreateUnchangedOutputsAssertCmds()); + newCmds.AddRange(refinementInstrumentation.CreateUnchangedAssertCmds()); newCmds.Add(CmdHelper.AssumeCmd(Expr.False)); - return BlockHelper.Block(civlTypeChecker.AddNamePrefix("RefinementCheckerForYieldingLoops"), newCmds); + return BlockHelper.Block(civlTypeChecker.AddNamePrefix("UnchangedChecker"), newCmds); } private Block CreateReturnCheckerBlock() diff --git a/Test/civl/parallel6.bpl.expect b/Test/civl/parallel6.bpl.expect index 1fad3e5e2..3a8aa067d 100644 --- a/Test/civl/parallel6.bpl.expect +++ b/Test/civl/parallel6.bpl.expect @@ -1,4 +1,4 @@ -parallel6.bpl(8,64): Error BP5001: Transition invariant violated in final state +parallel6.bpl(8,64): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state Execution trace: parallel6.bpl(10,5): anon0 parallel6.bpl(28,7): inline$atomic_incr$0$anon0 diff --git a/Test/civl/pending-async-1.bpl.expect b/Test/civl/pending-async-1.bpl.expect index 79a11096c..d54550c9d 100644 --- a/Test/civl/pending-async-1.bpl.expect +++ b/Test/civl/pending-async-1.bpl.expect @@ -1,4 +1,4 @@ -pending-async-1.bpl(48,49): Error BP5001: Failed to execute atomic action before procedure return +pending-async-1.bpl(48,49): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: pending-async-1.bpl(50,3): anon0 pending-async-1.bpl(16,7): inline$B$0$anon0 diff --git a/Test/civl/r2.bpl.expect b/Test/civl/r2.bpl.expect index 0bf8e9fad..0eb435d3e 100644 --- a/Test/civl/r2.bpl.expect +++ b/Test/civl/r2.bpl.expect @@ -1,15 +1,15 @@ -r2.bpl(10,57): Error BP5001: Failed to execute atomic action before procedure return +r2.bpl(10,57): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: r2.bpl(11,5): anon0 (0,0): Civl_call_refinement_4 r2.bpl(21,34): inline$atomic_nop$0$Return (0,0): Civl_ReturnChecker -r2.bpl(10,57): Error BP5001: Globals must not be modified +r2.bpl(10,57): Error BP5001: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: r2.bpl(11,5): anon0 (0,0): Civl_call_refinement_3 r2.bpl(17,7): inline$atomic_incr$0$anon0 r2.bpl(14,34): inline$atomic_incr$0$Return - (0,0): Civl_RefinementCheckerForYieldingLoops + (0,0): Civl_UnchangedChecker Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/civl/refinement.bpl b/Test/civl/refinement.bpl index 1d581495c..7a811aa2d 100644 --- a/Test/civl/refinement.bpl +++ b/Test/civl/refinement.bpl @@ -7,15 +7,14 @@ procedure {:yields}{:layer 1}{:refines "INCR"} p () { call incr(); // Refined action INCR occurred yield; - call incr(); // State changed again - // Error: Transition invariant in final state violated + call incr(); // Error: State changed again } procedure {:yields}{:layer 1}{:refines "INCR"} q () { - call decr(); // State changed, but not according to INCR - yield; // Error: Transition invariant in initial state violated - call incr(); + call decr(); // Error: State changed, but not according to INCR + yield; + call incr(); // Error: State changed again } procedure {:yields}{:layer 1}{:refines "INCR"} r () @@ -33,7 +32,18 @@ procedure {:yields}{:layer 1}{:refines "INCR"} r () procedure {:yields}{:layer 1}{:refines "INCR"} s () { - // Error: Failed to execute atomic action before procedure return + // Error: Refined action INCR never occurs +} + +procedure {:yields}{:layer 1}{:refines "INCR"} t () +{ + call incr(); + yield; + while (*) + invariant {:layer 1}{:yields} true; + { + call incr(); // Error: State change inside yielding loop + } } procedure {:both} {:layer 1,2} INCR () diff --git a/Test/civl/refinement.bpl.expect b/Test/civl/refinement.bpl.expect index 15aa930eb..8f964fcc2 100644 --- a/Test/civl/refinement.bpl.expect +++ b/Test/civl/refinement.bpl.expect @@ -1,25 +1,33 @@ -refinement.bpl(6,48): Error BP5001: Transition invariant violated in final state +refinement.bpl(6,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state Execution trace: refinement.bpl(8,3): anon0 - refinement.bpl(42,5): inline$INCR$0$anon0 + refinement.bpl(52,5): inline$INCR$0$anon0 refinement.bpl(8,3): anon0_0 - refinement.bpl(42,5): inline$INCR$1$anon0 + refinement.bpl(52,5): inline$INCR$1$anon0 (0,0): Civl_ReturnChecker -refinement.bpl(14,48): Error BP5001: Transition invariant violated in initial state +refinement.bpl(13,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action Execution trace: - refinement.bpl(16,3): anon0 - refinement.bpl(48,5): inline$DECR$0$anon0 + refinement.bpl(15,3): anon0 + refinement.bpl(58,5): inline$DECR$0$anon0 (0,0): Civl_RefinementChecker -refinement.bpl(14,48): Error BP5001: Transition invariant violated in final state +refinement.bpl(13,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state Execution trace: - refinement.bpl(16,3): anon0 - refinement.bpl(48,5): inline$DECR$0$anon0 - refinement.bpl(16,3): anon0_0 - refinement.bpl(42,5): inline$INCR$0$anon0 + refinement.bpl(15,3): anon0 + refinement.bpl(58,5): inline$DECR$0$anon0 + refinement.bpl(15,3): anon0_0 + refinement.bpl(52,5): inline$INCR$0$anon0 (0,0): Civl_ReturnChecker -refinement.bpl(34,48): Error BP5001: Failed to execute atomic action before procedure return +refinement.bpl(33,48): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: - refinement.bpl(37,1): anon0 + refinement.bpl(36,1): anon0 (0,0): Civl_ReturnChecker +refinement.bpl(38,48): Error BP5001: A yield-to-yield fragment illegally modifies layer-2 globals +Execution trace: + refinement.bpl(40,3): anon0 + refinement.bpl(52,5): inline$INCR$0$anon0 + refinement.bpl(40,3): anon0_0 + refinement.bpl(42,3): anon2_LoopHead + refinement.bpl(52,5): inline$INCR$1$anon0 + (0,0): Civl_UnchangedChecker -Boogie program verifier finished with 3 verified, 4 errors +Boogie program verifier finished with 3 verified, 5 errors