diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index ac48c1164..49ee3003c 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars) public static class BlockHelper { + public static readonly IToken /*!*/ ReportedNoToken = new Token(); + public static Block Block(string label, List cmds) { - return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd); + return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd); } public static Block Block(string label, List cmds, List gotoTargets) { - return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); + return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); } } diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index a14a846be..965241a98 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -40,8 +40,6 @@ public List FindLayers() } return layers.Distinct().OrderBy(l => l).ToList(); } - - } public static class QKeyValueExtensions { diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs index 5f7a1bb1f..27a0dd156 100644 --- a/Source/Core/Token.cs +++ b/Source/Core/Token.cs @@ -33,8 +33,7 @@ public string /*!*/ public Token next; // ML 2005-03-11 Tokens are kept in linked list - public static readonly IToken /*!*/ - NoToken = new Token(); + public static readonly IToken /*!*/ NoToken = new Token(); public Token() { diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index ad6f33558..6b9fdd5c4 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -548,7 +548,7 @@ private Dictionary> ComputeGlobalControlDependences() var indirectCallees = ComputeIndirectCallees(callGraph, directCallee); foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl])) { - foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(item => item)) + foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(item => item)) { globalCtrlDep[control].Add(c); } diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index d68939fad..2965b7047 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.5 + 3.3.0 net6.0 false Boogie diff --git a/Source/VCGeneration/Counterexample/Counterexample.cs b/Source/VCGeneration/Counterexample/Counterexample.cs index 6f7997e68..15d4cab2b 100644 --- a/Source/VCGeneration/Counterexample/Counterexample.cs +++ b/Source/VCGeneration/Counterexample/Counterexample.cs @@ -124,8 +124,6 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) } else { // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) { continue; } diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs index aea41c34b..edeec0497 100644 --- a/Source/VCGeneration/Splits/BlockRewriter.cs +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -167,4 +167,10 @@ public List ComputeNewBlocks( BlockCoalescer.CoalesceInPlace(newBlocks); return newBlocks; } + + + public static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) + { + return splitOnEveryAssert || isolateAttribute != null; + } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs index 5e834f41b..ec865264c 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -28,7 +28,7 @@ public static (List IsolatedParts, ManualSplit Remainder) GetParts( foreach (var assert in block.Cmds.OfType()) { var attributes = assert.Attributes; var isolateAttribute = QKeyValue.FindAttribute(attributes, p => p.Key == "isolate"); - if (!ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { + if (!BlockRewriter.ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { continue; } @@ -90,18 +90,6 @@ List GetCommands(Block block) => block.Cmds.Select(cmd => isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList(); } } - - private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) { - if (splitOnEveryAssert) { - if (isolateAttribute == null) { - return true; - } - - return !isolateAttribute.Params.OfType().Any(p => Equals(p, "none")); - } - - return isolateAttribute != null; - } } diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index bed4d3ce8..5b6ab5f49 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -33,7 +33,7 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var isTypeOfAssert = gotoCmd.tok is GotoFromReturn; var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate"); - var isolate = ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); + var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); if (!isolate) { continue; } @@ -62,7 +62,6 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen return (results, GetPartWithoutIsolatedReturns()); ManualSplit GetPartWithoutIsolatedReturns() { - // TODO this needs an extra test. In case the isolated jump is followed by something it dominates var newBlocks = rewriter.ComputeNewBlocks(blocks.ToHashSet(), (oldBlock, newBlock) => { if (isolatedBlockJumps.Contains(oldBlock)) { newBlock.TransferCmd = new ReturnCmd(Token.NoToken); @@ -72,18 +71,6 @@ ManualSplit GetPartWithoutIsolatedReturns() { newBlocks); } } - - private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) { - if (splitOnEveryAssert) { - if (isolateAttribute == null) { - return true; - } - - return !isolateAttribute.Params.OfType().Any(p => Equals(p, "none")); - } - - return isolateAttribute != null; - } } diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs index 7e4a13425..1d12f7f53 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -98,7 +98,7 @@ private void PrintSplit() { Thread.Sleep(100); } - var prefix = (this is ManualSplit manualSplit) ? manualSplit.Token.ShortName : ""; + var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : ""; var name = Implementation.Name + prefix; using var writer = printToConsole ? new TokenTextWriter("", Options.OutputWriter, false, Options.PrettyPrint, Options) diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index eee6a5843..8d79243ed 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -1352,22 +1352,22 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". /// - public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt, + public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, Block implEntryBlock) { - Contract.Requires(assrt != null); + Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; - if (assrt is AssertRequiresCmd assertRequiresCmd) + if (assert is AssertRequiresCmd assertRequiresCmd) { cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, assertRequiresCmd, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun, assertRequiresCmd.Checksum); } - else if (assrt is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample) + else if (assert is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample) { // The first three parameters of ReturnCounterexample are: List trace, List augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures. // We have the "aa" version of failingEnsures, namely aa.Ensures. The first and third parameters take more work to reconstruct. @@ -1451,7 +1451,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options } else { - cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context, + cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assert, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun); } diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect index 08c401b27..1a747e1d9 100644 --- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect +++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect @@ -1,4 +1,5 @@ intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed Execution trace: + (0,0): init Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect index 383a2cd10..44ada71cb 100644 --- a/Test/civl/regression-tests/left-mover.bpl.expect +++ b/Test/civl/regression-tests/left-mover.bpl.expect @@ -10,5 +10,6 @@ Execution trace: left-mover.bpl(6,24): inline$inc$0$Return left-mover.bpl(26,24): Error: Cooperation check for block failed Execution trace: + (0,0): init Boogie program verifier finished with 3 verified, 3 errors diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect index be24ba16a..9ed2f19b1 100644 --- a/Test/civl/regression-tests/non-interference-1.bpl.expect +++ b/Test/civl/regression-tests/non-interference-1.bpl.expect @@ -2,5 +2,6 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-1.bpl(7,3): anon0 non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/regression-tests/non-interference-2.bpl.expect b/Test/civl/regression-tests/non-interference-2.bpl.expect index 4bbae5629..c1176c36d 100644 --- a/Test/civl/regression-tests/non-interference-2.bpl.expect +++ b/Test/civl/regression-tests/non-interference-2.bpl.expect @@ -2,8 +2,10 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(7,3): anon0 non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(34,3): anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect index 55715916a..b97bf307f 100644 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect +++ b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect @@ -1,5 +1,6 @@ pa-noninterference-check.bpl(26,1): Error: Non-interference check failed Execution trace: + (0,0): init pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0 pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect index 0bc33ffe1..4b52e2854 100644 --- a/Test/civl/regression-tests/parallel1.bpl.expect +++ b/Test/civl/regression-tests/parallel1.bpl.expect @@ -2,5 +2,6 @@ parallel1.bpl(25,1): Error: Non-interference check failed Execution trace: parallel1.bpl(7,3): anon0 parallel1.bpl(12,5): inline$AtomicIncr$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/regression-tests/parallel6.bpl.expect b/Test/civl/regression-tests/parallel6.bpl.expect index 9a6a6e2be..0ff7beb24 100644 --- a/Test/civl/regression-tests/parallel6.bpl.expect +++ b/Test/civl/regression-tests/parallel6.bpl.expect @@ -7,5 +7,6 @@ Execution trace: parallel6.bpl(11,5): anon0_0 parallel6.bpl(30,7): inline$atomic_incr$2$anon0 parallel6.bpl(30,7): inline$atomic_incr$3$anon0 + (0,0): Civl_ReturnChecker Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect index 5e0a35e06..86c6fbf94 100644 --- a/Test/civl/regression-tests/pending-async-1.bpl.expect +++ b/Test/civl/regression-tests/pending-async-1.bpl.expect @@ -5,6 +5,7 @@ Execution trace: pending-async-1.bpl(51,3): anon0$1 pending-async-1.bpl(11,9): inline$B$1$anon0 pending-async-1.bpl(51,3): anon0$2 + (0,0): Civl_ReturnChecker pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized Execution trace: pending-async-1.bpl(67,3): anon0 diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect index d6951c016..29a3c680e 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect +++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect @@ -1,5 +1,6 @@ pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed Execution trace: + (0,0): init pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0 pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return diff --git a/Test/civl/regression-tests/refinement.bpl.expect b/Test/civl/regression-tests/refinement.bpl.expect index 7203ec2a4..4974958b5 100644 --- a/Test/civl/regression-tests/refinement.bpl.expect +++ b/Test/civl/regression-tests/refinement.bpl.expect @@ -5,11 +5,13 @@ Execution trace: refinement.bpl(10,3): anon0$1 refinement.bpl(10,3): anon0_0 refinement.bpl(58,5): inline$INCR$1$anon0 + (0,0): Civl_ReturnChecker refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action Execution trace: refinement.bpl(18,3): anon0 refinement.bpl(64,5): inline$DECR$0$anon0 refinement.bpl(18,3): anon0$1 + (0,0): Civl_RefinementChecker refinement.bpl(15,28): Error: 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(18,3): anon0 @@ -17,9 +19,11 @@ Execution trace: refinement.bpl(18,3): anon0$1 refinement.bpl(18,3): anon0_0 refinement.bpl(58,5): inline$INCR$0$anon0 + (0,0): Civl_ReturnChecker refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement.bpl(41,1): anon0 + (0,0): Civl_ReturnChecker refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement.bpl(46,3): anon0 @@ -28,5 +32,6 @@ Execution trace: refinement.bpl(46,3): anon0_0 refinement.bpl(48,3): anon2_LoopHead refinement.bpl(58,5): inline$INCR$1$anon0 + (0,0): Civl_UnchangedChecker Boogie program verifier finished with 3 verified, 5 errors diff --git a/Test/civl/regression-tests/refinement2.bpl.expect b/Test/civl/regression-tests/refinement2.bpl.expect index 24cb32f73..3005f0993 100644 --- a/Test/civl/regression-tests/refinement2.bpl.expect +++ b/Test/civl/regression-tests/refinement2.bpl.expect @@ -1,11 +1,15 @@ refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement2.bpl(16,5): anon0 + (0,0): Civl_call_refinement_4 refinement2.bpl(27,28): inline$atomic_nop$0$Return + (0,0): Civl_ReturnChecker refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement2.bpl(16,5): anon0 + (0,0): Civl_call_refinement_3 refinement2.bpl(22,7): inline$atomic_incr$0$anon0 refinement2.bpl(19,28): inline$atomic_incr$0$Return + (0,0): Civl_UnchangedChecker Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect index 8bab02145..093836a59 100644 --- a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect +++ b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect @@ -2,5 +2,6 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed Execution trace: yield-invariant-fails.bpl(11,5): anon0 yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L Boogie program verifier finished with 0 verified, 1 error