From 07ae2d8f0584a5a7d0f02a451cbcb564276e0013 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 24 Oct 2024 19:06:49 +0200 Subject: [PATCH] Enable marking if commands as {:allow_split} or not (#970) ### Changes - Introduce the attribute `{:allow_split}` that can be placed on `IfCmd`. When using `{:isolate "paths"}` only, branches with `{:allow_split}` will trigger splitting of the VC. ### Testing - Updated existing tests so they exercise the presence and absence of `{:allow_split}` - Added a test that combines `{:vcs_split_on_every_assert}` and explicit returns. --- .../YieldingProcInstrumentation.cs | 8 +- Source/Core/AST/Absy.cs | 2 +- Source/Core/AST/Commands/AbsyCmd.cs | 23 +- Source/Core/AST/Commands/CallCmd.cs | 2 +- .../{GotoBoogie => Commands}/ChangeScope.cs | 0 Source/Core/AST/GotoBoogie/Block.cs | 18 +- Source/Core/AST/GotoBoogie/GotoCmd.cs | 17 +- .../AST/GotoBoogie/TransferCmdContracts.cs | 18 ++ Source/Core/AST/QKeyValue.cs | 4 +- .../BigBlocksResolutionContext.cs | 195 ++++++------- Source/Core/AST/StructuredBoogie/IfCmd.cs | 8 +- Source/Core/AST/StructuredBoogie/StmtList.cs | 3 +- .../AST/StructuredBoogie/StmtListBuilder.cs | 17 +- Source/Core/Analysis/BlockCoalescer.cs | 17 +- Source/Core/BoogiePL.atg | 14 +- Source/Core/Generic/ListExtensions.cs | 6 + Source/Core/Parser.cs | 20 +- Source/Core/VariableDependenceAnalyser.cs | 198 +++++++------- Source/Directory.Build.props | 2 +- Source/ExecutionEngine/CommandLineOptions.cs | 8 + Source/Graph/Graph.cs | 76 ++++-- .../ExecutionEngineTests/RandomSeedTest.cs | 2 +- Source/VCGeneration/BlockTransformations.cs | 44 ++- Source/VCGeneration/Splits/BlockRewriter.cs | 156 +++++++---- .../Splits/FocusAttributeHandler.cs | 37 +-- .../IsolateAttributeOnAssertsHandler.cs | 18 +- .../Splits/IsolateAttributeOnJumpsHandler.cs | 50 ++-- .../VCGeneration/Splits/ManualSplitFinder.cs | 11 +- Source/VCGeneration/Splits/PathToken.cs | 16 +- .../Splits/SplitAttributeHandler.cs | 20 +- .../Transformations/DesugarReturns.cs | 2 +- .../VerificationConditionGenerator.cs | 31 ++- Test/implementationDivision/focus/focus.bpl | 2 +- .../focus/focus.bpl.expect | 115 ++++++++ .../isolateAssertion/isolateAssertion.bpl | 18 +- .../isolateAssertion.bpl.expect | 256 ++++++++++++++---- .../isolateJump/isolateContinue.bpl | 22 ++ .../isolateJump/isolateContinue.bpl.expect | 49 ++++ .../isolateJump/isolateJump.bpl | 18 +- .../isolateJump/isolateJump.bpl.expect | 125 ++++++--- ...solateJumpAndSplitOnEveryAssert.bpl.expect | 24 -- .../split/AssumeFalseSplit.bpl.expect | 2 +- .../split/Split.bpl.expect | 2 +- Test/inline/Elevator.bpl.expect | 4 +- isa.ppl | 137 ++++++++++ isolateJump.ppl | 113 ++++++++ 46 files changed, 1373 insertions(+), 557 deletions(-) rename Source/Core/AST/{GotoBoogie => Commands}/ChangeScope.cs (100%) create mode 100644 Source/Core/AST/GotoBoogie/TransferCmdContracts.cs create mode 100644 Test/implementationDivision/isolateJump/isolateContinue.bpl create mode 100644 Test/implementationDivision/isolateJump/isolateContinue.bpl.expect create mode 100644 isa.ppl create mode 100644 isolateJump.ppl diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 8fc55130e..1cc43b459 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -541,9 +541,7 @@ private void DesugarConcurrency(Implementation impl, List preconditions) impl.Blocks.Add(unchangedCheckerBlock); impl.Blocks.Add(returnCheckerBlock); impl.Blocks.Add(returnBlock); - foreach (var block in implRefinementCheckingBlocks) { - impl.Blocks.Add(block); - } + impl.Blocks.AddRange(implRefinementCheckingBlocks); impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions)); } @@ -600,9 +598,7 @@ private void SplitBlocks(Implementation impl) b.TransferCmd = currTransferCmd; } - foreach (var newBlock in newBlocks) { - impl.Blocks.Add(newBlock); - } + impl.Blocks.AddRange(newBlocks); } private Block CreateNoninterferenceCheckerBlock() diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index b9e1e36db..df0984032 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -2490,7 +2490,7 @@ public String ErrorMessage public bool CanAlwaysAssume () { - return Free && this.Attributes.FindBoolAttribute("always_assume"); + return Free && Attributes.FindBoolAttribute("always_assume"); } public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv) diff --git a/Source/Core/AST/Commands/AbsyCmd.cs b/Source/Core/AST/Commands/AbsyCmd.cs index 0beaa357b..b2a2c4c45 100644 --- a/Source/Core/AST/Commands/AbsyCmd.cs +++ b/Source/Core/AST/Commands/AbsyCmd.cs @@ -3,12 +3,9 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics.Contracts; -using Set = Microsoft.Boogie.GSet; namespace Microsoft.Boogie { - //--------------------------------------------------------------------- - // Commands [ContractClassFor(typeof(Cmd))] public abstract class CmdContracts : Cmd { @@ -2088,8 +2085,7 @@ public override Absy StdDispatch(StandardVisitor visitor) public class ReturnExprCmd : ReturnCmd { - public Expr /*!*/ - Expr; + public Expr /*!*/ Expr; [ContractInvariantMethod] void ObjectInvariant() @@ -2214,21 +2210,4 @@ public override Absy StdDispatch(StandardVisitor visitor) return visitor.VisitHavocCmd(this); } } - - //--------------------------------------------------------------------- - // Transfer commands - - [ContractClassFor(typeof(TransferCmd))] - public abstract class TransferCmdContracts : TransferCmd - { - public TransferCmdContracts() : base(null) - { - } - - public override void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - throw new NotImplementedException(); - } - } } diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs index 0f0ed662c..4bcc06358 100644 --- a/Source/Core/AST/Commands/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. if (callId is not null) { - (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, + a.CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresAssumed(callId, id)); } diff --git a/Source/Core/AST/GotoBoogie/ChangeScope.cs b/Source/Core/AST/Commands/ChangeScope.cs similarity index 100% rename from Source/Core/AST/GotoBoogie/ChangeScope.cs rename to Source/Core/AST/Commands/ChangeScope.cs diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs index 7ec347060..f217dd79f 100644 --- a/Source/Core/AST/GotoBoogie/Block.cs +++ b/Source/Core/AST/GotoBoogie/Block.cs @@ -7,11 +7,12 @@ namespace Microsoft.Boogie; public sealed class Block : Absy { - public string /*!*/ Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal + + public string Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal - [Rep] - [ElementsPeer] - public List /*!*/ Cmds; + [Rep] + [ElementsPeer] + public List Cmds { get; set; } public IEnumerable Exits() { @@ -23,8 +24,7 @@ public IEnumerable Exits() } [Rep] //PM: needed to verify Traverse.Visit - public TransferCmd - TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) + public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) public byte[] Checksum; @@ -164,10 +164,10 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - foreach (Cmd /*!*/ c in Cmds) + foreach (var /*!*/ cmd in Cmds) { - Contract.Assert(c != null); - c.Typecheck(tc); + Contract.Assert(cmd != null); + cmd.Typecheck(tc); } Contract.Assume(this.TransferCmd != null); diff --git a/Source/Core/AST/GotoBoogie/GotoCmd.cs b/Source/Core/AST/GotoBoogie/GotoCmd.cs index acfefc7ae..7a1ef75dc 100644 --- a/Source/Core/AST/GotoBoogie/GotoCmd.cs +++ b/Source/Core/AST/GotoBoogie/GotoCmd.cs @@ -5,7 +5,7 @@ namespace Microsoft.Boogie; -public class GotoCmd : TransferCmd +public class GotoCmd : TransferCmd, ICarriesAttributes { [Rep] public List LabelNames; [Rep] public List LabelTargets; @@ -43,20 +43,20 @@ public GotoCmd(IToken /*!*/ tok, List /*!*/ labels, List /*!*/ bl this.LabelTargets = blocks; } - public GotoCmd(IToken /*!*/ tok, List /*!*/ blockSeq) + public GotoCmd(IToken /*!*/ tok, List /*!*/ blocks) : base(tok) { //requires (blockSeq[i] != null ==> blockSeq[i].Label != null); Contract.Requires(tok != null); - Contract.Requires(blockSeq != null); - List labelSeq = new List(); - for (int i = 0; i < blockSeq.Count; i++) + Contract.Requires(blocks != null); + var labels = new List(); + foreach (var block in blocks) { - labelSeq.Add(cce.NonNull(blockSeq[i]).Label); + labels.Add(block.Label); } - this.LabelNames = labelSeq; - this.LabelTargets = blockSeq; + this.LabelNames = labels; + this.LabelTargets = blocks; } public void RemoveTarget(Block b) { @@ -91,6 +91,7 @@ public override void Emit(TokenTextWriter stream, int level) //Contract.Requires(stream != null); Contract.Assume(this.LabelNames != null); stream.Write(this, level, "goto "); + Attributes?.Emit(stream); if (stream.Options.PrintWithUniqueASTIds) { if (LabelTargets == null) diff --git a/Source/Core/AST/GotoBoogie/TransferCmdContracts.cs b/Source/Core/AST/GotoBoogie/TransferCmdContracts.cs new file mode 100644 index 000000000..fbb7da6e0 --- /dev/null +++ b/Source/Core/AST/GotoBoogie/TransferCmdContracts.cs @@ -0,0 +1,18 @@ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +[ContractClassFor(typeof(TransferCmd))] +public abstract class TransferCmdContracts : TransferCmd +{ + public TransferCmdContracts() : base(null) + { + } + + public override void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + throw new NotImplementedException(); + } +} \ No newline at end of file diff --git a/Source/Core/AST/QKeyValue.cs b/Source/Core/AST/QKeyValue.cs index 5693a4e3e..0d1d0f977 100644 --- a/Source/Core/AST/QKeyValue.cs +++ b/Source/Core/AST/QKeyValue.cs @@ -48,14 +48,14 @@ void ObjectInvariant() Contract.Invariant(cce.NonNullElements(this._params)); } - public QKeyValue(IToken tok, string key, IList /*!*/ parameters, QKeyValue next) + public QKeyValue(IToken tok, string key, IList /*!*/ parameters = null, QKeyValue next = null) : base(tok) { Contract.Requires(key != null); Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(parameters)); Key = key; - this._params = new List(parameters); + this._params = parameters == null ? new List() : new List(parameters); Next = next; } diff --git a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs index 1172696f5..e2e3dc53c 100644 --- a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs @@ -13,14 +13,13 @@ class BigBlocksResolutionContext [Peer] List blocks; - string /*!*/ - prefix = "anon"; + string /*!*/ prefix = "anon"; int anon = 0; - int FreshAnon() + string FreshPrefix() { - return anon++; + return prefix + anon++; } private readonly HashSet allLabels = new(); @@ -271,10 +270,9 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent } // recurse - else if (bigBlock.ec is WhileCmd) + else if (bigBlock.ec is WhileCmd whileCmd) { - WhileCmd wcmd = (WhileCmd) bigBlock.ec; - CheckLegalLabels(wcmd.Body, stmtList, bigBlock); + CheckLegalLabels(whileCmd.Body, stmtList, bigBlock); } else { @@ -290,29 +288,25 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent } } - void NameAnonymousBlocks(StmtList stmtList) + private void NameAnonymousBlocks(StmtList stmtList) { Contract.Requires(stmtList != null); foreach (var bigBlock in stmtList.BigBlocks) { - if (bigBlock.LabelName == null) - { - bigBlock.LabelName = prefix + FreshAnon(); - } + bigBlock.LabelName ??= FreshPrefix(); - if (bigBlock.ec is WhileCmd) + if (bigBlock.ec is WhileCmd whileCmd) { - WhileCmd wcmd = (WhileCmd) bigBlock.ec; - NameAnonymousBlocks(wcmd.Body); + NameAnonymousBlocks(whileCmd.Body); } else { - for (IfCmd ifcmd = bigBlock.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf) + for (IfCmd ifCmd = bigBlock.ec as IfCmd; ifCmd != null; ifCmd = ifCmd.ElseIf) { - NameAnonymousBlocks(ifcmd.Thn); - if (ifcmd.ElseBlock != null) + NameAnonymousBlocks(ifCmd.Thn); + if (ifCmd.ElseBlock != null) { - NameAnonymousBlocks(ifcmd.ElseBlock); + NameAnonymousBlocks(ifCmd.ElseBlock); } } } @@ -324,7 +318,7 @@ private static void AssignSuccessors(StmtList stmtList, BigBlock next) Contract.Requires(stmtList != null); for (int i = stmtList.BigBlocks.Count; 0 <= --i;) { - BigBlock current = stmtList.BigBlocks[i]; + var current = stmtList.BigBlocks[i]; current.SuccessorBigBlock = next; if (current.ec is WhileCmd whileCmd) @@ -333,12 +327,13 @@ private static void AssignSuccessors(StmtList stmtList, BigBlock next) } else { - for (IfCmd ifcmd = current.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf) + for (IfCmd ifCmd = current.ec as IfCmd; ifCmd != null; ifCmd = ifCmd.ElseIf) { - AssignSuccessors(ifcmd.Thn, next); - if (ifcmd.ElseBlock != null) + //next. + AssignSuccessors(ifCmd.Thn, next); + if (ifCmd.ElseBlock != null) { - AssignSuccessors(ifcmd.ElseBlock, next); + AssignSuccessors(ifCmd.ElseBlock, next); } } } @@ -349,7 +344,7 @@ private static void AssignSuccessors(StmtList stmtList, BigBlock next) // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; // otherwise, it is null. - void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) + private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { Contract.Requires(stmtList != null); Contract.Requires(blocks != null); @@ -377,10 +372,11 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { // this BigBlock has the very same components as a Block Contract.Assert(bigBlock.ec == null); - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc); blocks.Add(block); } - else { + else + { switch (bigBlock.ec) { case null: @@ -389,171 +385,182 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); } else { trCmd = GotoSuccessor(stmtList.EndCurly, bigBlock); } - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd); blocks.Add(block); break; } case BreakCmd breakCmd: { - BreakCmd bcmd = breakCmd; - Contract.Assert(bcmd.BreakEnclosure != null); - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(breakCmd.tok, bcmd.BreakEnclosure)); + Contract.Assert(breakCmd.BreakEnclosure != null); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(breakCmd.tok, breakCmd.BreakEnclosure)); blocks.Add(block); break; } case WhileCmd whileCmd: { - WhileCmd wcmd = whileCmd; - var a = FreshAnon(); - string loopHeadLabel = prefix + a + "_LoopHead"; - string /*!*/ - loopBodyLabel = prefix + a + "_LoopBody"; - string loopDoneLabel = prefix + a + "_LoopDone"; - - List ssBody = new List(); - List ssDone = new List(); - if (wcmd.Guard != null) + var freshPrefix = FreshPrefix(); + string loopHeadLabel = freshPrefix + "_LoopHead"; + string loopBodyLabel = freshPrefix + "_LoopBody"; + string loopDoneLabel = freshPrefix + "_LoopDone"; + + var ssBody = new List(); + var ssDone = new List(); + if (whileCmd.Guard != null) { - var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(whileCmd.tok, whileCmd.Guard) + { + Attributes = new QKeyValue(whileCmd.tok, "partition", new List(), null) + }; ssBody.Add(ac); - ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); + ac = new AssumeCmd(whileCmd.tok, Expr.Not(whileCmd.Guard)) + { + Attributes = new QKeyValue(whileCmd.tok, "partition", new List(), null) + }; ssDone.Add(ac); } // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + bool bodyGuardTakenCareOf = whileCmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); // ... goto LoopHead; - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, - new GotoCmd(wcmd.tok, new List {loopHeadLabel})); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, + new GotoCmd(whileCmd.tok, new List {loopHeadLabel})); blocks.Add(block); // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; List ssHead = new List(); - foreach (CallCmd yield in wcmd.Yields) + foreach (CallCmd yield in whileCmd.Yields) { ssHead.Add(yield); } - foreach (PredicateCmd inv in wcmd.Invariants) + foreach (PredicateCmd inv in whileCmd.Invariants) { ssHead.Add(inv); } - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); + block = new Block(whileCmd.tok, loopHeadLabel, ssHead, + new GotoCmd(whileCmd.tok, new List {loopDoneLabel, loopBodyLabel})); blocks.Add(block); if (!bodyGuardTakenCareOf) { // LoopBody: assume guard; goto firstLoopBlock; - block = new Block(wcmd.tok, loopBodyLabel, ssBody, - new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); + block = new Block(whileCmd.tok, loopBodyLabel, ssBody, + new GotoCmd(whileCmd.tok, new List {whileCmd.Body.BigBlocks[0].LabelName})); blocks.Add(block); } // recurse to create the blocks for the loop body - CreateBlocks(wcmd.Body, loopHeadLabel); + CreateBlocks(whileCmd.Body, loopHeadLabel); // LoopDone: assume !guard; goto loopSuccessor; TransferCmd trCmd; if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(whileCmd.tok, new List {runOffTheEndLabel}); } else { - trCmd = GotoSuccessor(wcmd.tok, bigBlock); + trCmd = GotoSuccessor(whileCmd.tok, bigBlock); } - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); + block = new Block(whileCmd.tok, loopDoneLabel, ssDone, trCmd); blocks.Add(block); break; } - default: + case IfCmd ifCmd: { - IfCmd ifcmd = (IfCmd) bigBlock.ec; string predLabel = bigBlock.LabelName; - List predCmds = theSimpleCmds; + var predCmds = theSimpleCmds; - for (; ifcmd != null; ifcmd = ifcmd.ElseIf) + var jumpBlockToken = bigBlock.tok; + for (; ifCmd != null; ifCmd = ifCmd.ElseIf) { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; + var freshPrefix = FreshPrefix(); + string thenLabel = freshPrefix + "_Then"; Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; + string elseLabel = freshPrefix + "_Else"; Contract.Assert(elseLabel != null); - List ssThen = new List(); - List ssElse = new List(); - if (ifcmd.Guard != null) + var ssThen = new List(); + var ssElse = new List(); + if (ifCmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(ifCmd.tok, ifCmd.Guard) + { + Attributes = new QKeyValue(ifCmd.tok, "partition", new List(), null) + }; ssThen.Add(ac); - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + ac = new AssumeCmd(ifCmd.tok, Expr.Not(ifCmd.Guard)) + { + Attributes = new QKeyValue(ifCmd.tok, "partition", new List(), null) + }; ssElse.Add(ac); } // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock - bool thenGuardTakenCareOf = ifcmd.Thn.PrefixFirstBlock(ssThen, ref thenLabel); + bool thenGuardTakenCareOf = ifCmd.Thn.PrefixFirstBlock(ssThen, ref thenLabel); bool elseGuardTakenCareOf = false; - if (ifcmd.ElseBlock != null) + if (ifCmd.ElseBlock != null) { - elseGuardTakenCareOf = ifcmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + elseGuardTakenCareOf = ifCmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel); } // ... goto Then, Else; - var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + var jump = new GotoCmd(jumpBlockToken, new List {thenLabel, elseLabel}) + { + Attributes = ifCmd.Attributes + }; + var jumpBlock = new Block(jumpBlockToken, predLabel, predCmds, jump); blocks.Add(jumpBlock); if (!thenGuardTakenCareOf) { // Then: assume guard; goto firstThenBlock; - var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, - new GotoCmd(ifcmd.tok, new List {ifcmd.Thn.BigBlocks[0].LabelName})); + var thenJumpBlock = new Block(ifCmd.tok, thenLabel, ssThen, + new GotoCmd(ifCmd.tok, new List {ifCmd.Thn.BigBlocks[0].LabelName})); blocks.Add(thenJumpBlock); } // recurse to create the blocks for the then branch - CreateBlocks(ifcmd.Thn, remainingBigBlocks == 0 ? runOffTheEndLabel : null); + CreateBlocks(ifCmd.Thn, remainingBigBlocks == 0 ? runOffTheEndLabel : null); - if (ifcmd.ElseBlock != null) + if (ifCmd.ElseBlock != null) { - Contract.Assert(ifcmd.ElseIf == null); + Contract.Assert(ifCmd.ElseIf == null); if (!elseGuardTakenCareOf) { // Else: assume !guard; goto firstElseBlock; - var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.ElseBlock.BigBlocks[0].LabelName})); + var elseJumpBlock = new Block(ifCmd.tok, elseLabel, ssElse, + new GotoCmd(ifCmd.tok, new List {ifCmd.ElseBlock.BigBlocks[0].LabelName})); blocks.Add(elseJumpBlock); } // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.ElseBlock, remainingBigBlocks == 0 ? runOffTheEndLabel : null); + CreateBlocks(ifCmd.ElseBlock, remainingBigBlocks == 0 ? runOffTheEndLabel : null); } - else if (ifcmd.ElseIf != null) + else if (ifCmd.ElseIf != null) { // this is an "else if" + jumpBlockToken = ifCmd.ElseIf.tok; predLabel = elseLabel; predCmds = new List(); - if (ifcmd.Guard != null) + if (ifCmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(ifCmd.tok, Expr.Not(ifCmd.Guard)) + { + Attributes = new QKeyValue(ifCmd.tok, "partition", new List(), null) + }; predCmds.Add(ac); } } @@ -565,14 +572,14 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(ifCmd.tok, new List {runOffTheEndLabel}); } else { - trCmd = GotoSuccessor(ifcmd.tok, bigBlock); + trCmd = GotoSuccessor(ifCmd.tok, bigBlock); } - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + var block = new Block(ifCmd.tok, elseLabel, ssElse, trCmd); blocks.Add(block); } } @@ -584,7 +591,7 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) } } - TransferCmd GotoSuccessor(IToken tok, BigBlock b) + private static TransferCmd GotoSuccessor(IToken tok, BigBlock b) { Contract.Requires(b != null); Contract.Requires(tok != null); diff --git a/Source/Core/AST/StructuredBoogie/IfCmd.cs b/Source/Core/AST/StructuredBoogie/IfCmd.cs index ed2dff9e3..a08dd9501 100644 --- a/Source/Core/AST/StructuredBoogie/IfCmd.cs +++ b/Source/Core/AST/StructuredBoogie/IfCmd.cs @@ -4,6 +4,7 @@ namespace Microsoft.Boogie; public class IfCmd : StructuredCmd { + public QKeyValue Attributes; public Expr Guard; private StmtList /*!*/ thn; @@ -53,7 +54,8 @@ void ObjectInvariant() Contract.Invariant(this.elseIf == null || this.elseBlock == null); } - public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) + public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock, + QKeyValue attributes = null) : base(tok) { Contract.Requires(tok != null); @@ -63,13 +65,13 @@ public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, Stm this.thn = thn; this.elseIf = elseIf; this.elseBlock = elseBlock; + Attributes = attributes; } public override void Emit(TokenTextWriter stream, int level) { stream.Write(level, "if ("); - IfCmd /*!*/ - ifcmd = this; + var /*!*/ ifcmd = this; while (true) { if (ifcmd.Guard == null) diff --git a/Source/Core/AST/StructuredBoogie/StmtList.cs b/Source/Core/AST/StructuredBoogie/StmtList.cs index 51407e1c7..159972001 100644 --- a/Source/Core/AST/StructuredBoogie/StmtList.cs +++ b/Source/Core/AST/StructuredBoogie/StmtList.cs @@ -20,8 +20,7 @@ public IList /*!*/ BigBlocks public List PrefixCommands; - public readonly IToken /*!*/ - EndCurly; + public readonly IToken /*!*/ EndCurly; public StmtList ParentContext; public BigBlock ParentBigBlock; diff --git a/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs b/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs index dd7b67666..2ca373f71 100644 --- a/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs +++ b/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; namespace Microsoft.Boogie; @@ -21,7 +22,7 @@ void ObjectInvariant() Contract.Invariant(cce.NonNullElements(bigBlocks)); } - void Dump(StructuredCmd scmd, TransferCmd tcmd) + void Dump(IToken token, StructuredCmd scmd, TransferCmd tcmd) { Contract.Requires(scmd == null || tcmd == null); Contract.Ensures(label == null && simpleCmds == null); @@ -36,7 +37,7 @@ void Dump(StructuredCmd scmd, TransferCmd tcmd) simpleCmds = new List(); } - bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd)); + bigBlocks.Add(new BigBlock(token, label, simpleCmds, scmd, tcmd)); label = null; simpleCmds = null; } @@ -50,11 +51,11 @@ public StmtList Collect(IToken endCurlyBrace) { Contract.Requires(endCurlyBrace != null); Contract.Ensures(Contract.Result() != null); - Dump(null, null); + Dump(endCurlyBrace, null, null); if (bigBlocks.Count == 0) { simpleCmds = new List(); // the StmtList constructor doesn't like an empty list of BigBlock's - Dump(null, null); + Dump(endCurlyBrace, null, null); } return new StmtList(bigBlocks, endCurlyBrace); @@ -74,19 +75,19 @@ public void Add(Cmd cmd) public void Add(StructuredCmd scmd) { Contract.Requires(scmd != null); - Dump(scmd, null); + Dump(scmd.tok, scmd, null); } public void Add(TransferCmd tcmd) { Contract.Requires(tcmd != null); - Dump(null, tcmd); + Dump(tcmd.tok, null, tcmd); } - public void AddLabelCmd(string label) + public void AddLabelCmd(IToken token, string label) { Contract.Requires(label != null); - Dump(null, null); + Dump(token, null, null); this.label = label; } diff --git a/Source/Core/Analysis/BlockCoalescer.cs b/Source/Core/Analysis/BlockCoalescer.cs index 82ba4a099..d492e00b7 100644 --- a/Source/Core/Analysis/BlockCoalescer.cs +++ b/Source/Core/Analysis/BlockCoalescer.cs @@ -79,6 +79,12 @@ public override Implementation VisitImplementation(Implementation impl) return impl; } + public static void CoalesceInPlace(IList blocks) { + var coalesced = CoalesceFromRootBlock(blocks); + blocks.Clear(); + blocks.AddRange(coalesced); + } + public static IList CoalesceFromRootBlock(IList blocks) { if (!blocks.Any()) @@ -134,8 +140,17 @@ public static IList CoalesceFromRootBlock(IList blocks) continue; } - block.Cmds.AddRange(successor.Cmds); + // Previously this was block.Cmds.AddRange, + // command lists are reused between blocks + // so that was buggy. Maybe Block.Cmds should be made immutable + block.Cmds = block.Cmds.Concat(successor.Cmds).ToList(); + var originalTransferToken = block.TransferCmd.tok; block.TransferCmd = successor.TransferCmd; + if (!block.TransferCmd.tok.IsValid) { + block.TransferCmd = (TransferCmd)block.TransferCmd.Clone(); + block.TransferCmd.tok = originalTransferToken; + } + if (!block.tok.IsValid && successor.tok.IsValid) { block.tok = successor.tok; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index fe5b791c2..348ac2580 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1072,10 +1072,13 @@ TransferCmd QKeyValue kv = null; .) ( "goto" (. y = t; .) + { Attribute } Idents (. foreach(IToken/*!*/ s in xs){ Contract.Assert(s != null); ss.Add(s.val); } - tc = new GotoCmd(y, ss); + tc = new GotoCmd(y, ss) { + Attributes = kv + }; .) | "return" { Attribute } @@ -1099,8 +1102,10 @@ IfCmd StmtList/*!*/ thn; IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; + QKeyValue kv = null; .) "if" (. x = t; .) + { Attribute } Guard "{" StmtList [ "else" @@ -1109,7 +1114,7 @@ IfCmd StmtList (. elseOption = els; .) ) ] - (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); .) + (. ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption, kv); .) . WhileCmd @@ -1742,10 +1747,13 @@ SpecBlock .) } ( "goto" (. y = t; .) + { Attribute } Idents (. foreach(IToken/*!*/ s in xs){ Contract.Assert(s != null); ss.Add(s.val); } - b = new Block(x,x.val,cs,new GotoCmd(y,ss)); + b = new Block(x,x.val,cs,new GotoCmd(y,ss) { + Attributes = kv + }); .) | "return" { Attribute } diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs index 6825839b8..e0e5679ee 100644 --- a/Source/Core/Generic/ListExtensions.cs +++ b/Source/Core/Generic/ListExtensions.cs @@ -5,6 +5,12 @@ namespace Microsoft.Boogie; public static class ListExtensions { + public static void AddRange(this IList list, IEnumerable newValues) { + foreach (var value in newValues) { + list.Add(value); + } + } + public static IReadOnlyList Reversed(this IReadOnlyList list) { return new ReversedReadOnlyList(list); } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 86678cf34..703fa7b8b 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1580,11 +1580,16 @@ void TransferCmd(out TransferCmd/*!*/ tc) { if (la.kind == 55) { Get(); y = t; + while (la.kind == 26) { + Attribute(ref kv); + } Idents(out xs); foreach(IToken/*!*/ s in xs){ Contract.Assert(s != null); ss.Add(s.val); } - tc = new GotoCmd(y, ss); + tc = new GotoCmd(y, ss) { + Attributes = kv + }; } else if (la.kind == 56) { Get(); @@ -1602,9 +1607,13 @@ void IfCmd(out IfCmd/*!*/ ifcmd) { StmtList/*!*/ thn; IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; + QKeyValue kv = null; Expect(57); x = t; + while (la.kind == 26) { + Attribute(ref kv); + } Guard(out guard); Expect(26); StmtList(out thn); @@ -1619,7 +1628,7 @@ void IfCmd(out IfCmd/*!*/ ifcmd) { elseOption = els; } else SynErr(150); } - ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); + ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption, kv); } void WhileCmd(out WhileCmd wcmd) { @@ -2619,11 +2628,16 @@ void SpecBlock(out Block/*!*/ b) { if (la.kind == 55) { Get(); y = t; + while (la.kind == 26) { + Attribute(ref kv); + } Idents(out xs); foreach(IToken/*!*/ s in xs){ Contract.Assert(s != null); ss.Add(s.val); } - b = new Block(x,x.val,cs,new GotoCmd(y,ss)); + b = new Block(x,x.val,cs,new GotoCmd(y,ss) { + Attributes = kv + }); } else if (la.kind == 56) { Get(); diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 064b4a6db..6b9fdd5c4 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -137,8 +137,8 @@ public class VariableDependenceAnalyser : IVariableDependenceAnalyser private CoreOptions options; private Graph dependsOnNonTransitive; private Program prog; - private Dictionary> BlockToControllingBlocks; - private Dictionary> ControllingBlockToVariables; + private Dictionary> blockToControllingBlocks; + private Dictionary> controllingBlockToVariables; public VariableDependenceAnalyser(Program prog, CoreOptions options) { @@ -151,30 +151,30 @@ public VariableDependenceAnalyser(Program prog, CoreOptions options) private void Initialise() { foreach (var descriptor in - prog.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)).Select(Variable => Variable.Name) - .Select(Name => new GlobalDescriptor(Name))) + prog.Variables.Where(item => VariableRelevantToAnalysis(item, null)).Select(variable => variable.Name) + .Select(name => new GlobalDescriptor(name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } - foreach (var Proc in prog.NonInlinedProcedures()) + foreach (var proc in prog.NonInlinedProcedures()) { List parameters = new List(); - parameters.AddRange(Proc.InParams); - parameters.AddRange(Proc.OutParams); + parameters.AddRange(proc.InParams); + parameters.AddRange(proc.OutParams); foreach (var descriptor in - parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) + parameters.Select(variable => variable.Name).Select(name => new LocalDescriptor(proc.Name, name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } } - foreach (var Impl in prog.NonInlinedImplementations()) + foreach (var impl in prog.NonInlinedImplementations()) { List locals = new List(); - locals.AddRange(Impl.LocVars); + locals.AddRange(impl.LocVars); foreach (var descriptor in - locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) + locals.Select(variable => variable.Name).Select(name => new LocalDescriptor(impl.Name, name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } @@ -279,29 +279,29 @@ public void Analyse() options.OutputWriter.WriteLine("Variable dependence analysis: Computing control dependence info"); } - BlockToControllingBlocks = ComputeGlobalControlDependences(); + blockToControllingBlocks = ComputeGlobalControlDependences(); if (options.Trace) { options.OutputWriter.WriteLine("Variable dependence analysis: Computing control dependence variables"); } - ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks); - foreach (var Impl in prog.NonInlinedImplementations()) + controllingBlockToVariables = ComputeControllingVariables(blockToControllingBlocks); + foreach (var impl in prog.NonInlinedImplementations()) { if (options.Trace) { - options.OutputWriter.WriteLine("Variable dependence analysis: Analysing " + Impl.Name); + options.OutputWriter.WriteLine("Variable dependence analysis: Analysing " + impl.Name); } - Analyse(Impl); + Analyse(impl); } } - private void Analyse(Implementation Impl) + private void Analyse(Implementation impl) { - string proc = Impl.Name; - foreach (Block b in Impl.Blocks) + string proc = impl.Name; + foreach (Block b in impl.Blocks) { Analyse(proc, b); } @@ -349,7 +349,7 @@ private void HandleCall(string proc, Block b, CallCmd call) private void HandleAssign(string proc, Block b, AssignCmd assign) { foreach (var assignPair in assign.Lhss.Zip(assign.Rhss).Where( - Item => VariableRelevantToAnalysis(Item.Item1.DeepAssignedVariable, proc))) + item => VariableRelevantToAnalysis(item.Item1.DeepAssignedVariable, proc))) { VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable); AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc), @@ -362,24 +362,24 @@ private void HandleAssign(string proc, Block b, AssignCmd assign) private void AddControlDependences(Block b, VariableDescriptor v, string reason, IToken tok) { - if (!BlockToControllingBlocks.ContainsKey(b)) + if (!blockToControllingBlocks.ContainsKey(b)) { return; } - foreach (var controller in BlockToControllingBlocks[b]) + foreach (var controller in blockToControllingBlocks[b]) { - AddDependences(v, ControllingBlockToVariables[controller], + AddDependences(v, controllingBlockToVariables[controller], reason + " controlling block at (" + controller.tok.line + ":" + controller.tok.col + ")", tok); } } private IEnumerable GetReferencedVariables(Absy node, string proc) { - var VarCollector = new VariableCollector(); - VarCollector.Visit(node); - return VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)) - .Select(Item => MakeDescriptor(proc, Item)); + var varCollector = new VariableCollector(); + varCollector.Visit(node); + return varCollector.usedVars.Where(item => VariableRelevantToAnalysis(item, proc)) + .Select(item => MakeDescriptor(proc, item)); } void AddDependences(VariableDescriptor v, IEnumerable vs, string reason, IToken tok) @@ -397,14 +397,14 @@ void AddDependences(VariableDescriptor v, IEnumerable vs, st } private Dictionary> ComputeControllingVariables( - Dictionary> GlobalCtrlDep) + Dictionary> globalCtrlDep) { - Dictionary> result = new Dictionary>(); - foreach (var Impl in prog.NonInlinedImplementations()) + var result = new Dictionary>(); + foreach (var impl in prog.NonInlinedImplementations()) { - foreach (var b in Impl.Blocks) + foreach (var b in impl.Blocks) { - result[b] = GetControlDependencyVariables(Impl.Name, b); + result[b] = GetControlDependencyVariables(impl.Name, b); } } @@ -427,10 +427,10 @@ private HashSet GetControlDependencyVariables(string proc, B AssumeCmd a = c as AssumeCmd; if (a != null && a.Attributes.FindBoolAttribute("partition")) { - var VarCollector = new VariableCollector(); - VarCollector.VisitExpr(a.Expr); - result.UnionWith(VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)) - .Select(Item => MakeDescriptor(proc, Item))); + var varCollector = new VariableCollector(); + varCollector.VisitExpr(a.Expr); + result.UnionWith(varCollector.usedVars.Where(item => VariableRelevantToAnalysis(item, proc)) + .Select(item => MakeDescriptor(proc, item))); } else { @@ -443,21 +443,21 @@ private HashSet GetControlDependencyVariables(string proc, B return result; } - private HashSet IgnoredVariables = null; + private HashSet ignoredVariables; public bool Ignoring(Variable v, string proc) { - if (IgnoredVariables == null) + if (ignoredVariables == null) { MakeIgnoreList(); } - if (proc != null && IgnoredVariables.Contains(new LocalDescriptor(proc, v.Name))) + if (proc != null && ignoredVariables.Contains(new LocalDescriptor(proc, v.Name))) { return true; } - if (IgnoredVariables.Contains(new GlobalDescriptor(v.Name))) + if (ignoredVariables.Contains(new GlobalDescriptor(v.Name))) { return true; } @@ -472,7 +472,7 @@ public bool VariableRelevantToAnalysis(Variable v, string proc) private void MakeIgnoreList() { - IgnoredVariables = new HashSet(); + ignoredVariables = new HashSet(); if (options.VariableDependenceIgnore == null) { return; @@ -498,12 +498,12 @@ private void MakeIgnoreList() if (tokens.Count() == 1) { - IgnoredVariables.Add(new GlobalDescriptor(tokens[0])); + ignoredVariables.Add(new GlobalDescriptor(tokens[0])); continue; } Debug.Assert(tokens.Count() == 2); - IgnoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); + ignoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); } } catch (System.IO.IOException e) @@ -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); } @@ -580,23 +580,23 @@ private Dictionary> ComputeGlobalControlDependences() return result; } - private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee) + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation directCallee) { - return ComputeIndirectCallees(callGraph, DirectCallee, new HashSet()); + return ComputeIndirectCallees(callGraph, directCallee, new HashSet()); } - private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee, + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation directCallee, HashSet seen) { - if (seen.Contains(DirectCallee)) + if (seen.Contains(directCallee)) { return new HashSet(); } HashSet result = new HashSet(); - result.Add(DirectCallee); - seen.Add(DirectCallee); - foreach (var succ in callGraph.Successors(DirectCallee)) + result.Add(directCallee); + seen.Add(directCallee); + foreach (var succ in callGraph.Successors(directCallee)) { result.UnionWith(ComputeIndirectCallees(callGraph, succ, seen)); } @@ -607,11 +607,11 @@ private HashSet ComputeIndirectCallees(Graph cal private HashSet GetControllingBlocks(Block b, Dictionary> ctrlDep) { HashSet result = new HashSet(); - foreach (var KeyValue in ctrlDep) + foreach (var keyValue in ctrlDep) { - if (KeyValue.Value.Contains(b)) + if (keyValue.Value.Contains(b)) { - result.Add(KeyValue.Key); + result.Add(keyValue.Key); } } @@ -620,11 +620,11 @@ private HashSet GetControllingBlocks(Block b, Dictionary Item is LocalDescriptor).Select( - Item => (LocalDescriptor) Item).Where(Item => Item.Proc.Equals(proc) && - Item.Name.Equals(v.Name)); - if (MatchingLocals.Count() > 0) + var matchingLocals = dependsOnNonTransitive.Nodes.Where(item => item is LocalDescriptor).Select( + item => (LocalDescriptor) item).Where(item => item.Proc.Equals(proc) && + item.Name.Equals(v.Name)); + if (matchingLocals.Count() > 0) { - Debug.Assert(MatchingLocals.Count() == 1); - return MatchingLocals.ToArray()[0]; + Debug.Assert(matchingLocals.Count() == 1); + return matchingLocals.ToArray()[0]; } // It must be a global with same name as v - return dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor && - Item.Name.Equals(v.Name)).ToArray()[0]; + return dependsOnNonTransitive.Nodes.Where(item => item is GlobalDescriptor && + item.Name.Equals(v.Name)).ToArray()[0]; } - private Dictionary, HashSet> DependsOnCache = + private Dictionary, HashSet> dependsOnCache = new Dictionary, HashSet>(); - private Graph> DependsOnSCCsDAG; - private Dictionary> VariableDescriptorToSCC; + private Graph> dependsOnScCsDag; + private Dictionary> variableDescriptorToScc; public HashSet DependsOn(VariableDescriptor v) { - if (DependsOnSCCsDAG == null) + if (dependsOnScCsDag == null) { if (options.Trace) { @@ -665,33 +665,33 @@ public HashSet DependsOn(VariableDescriptor v) Adjacency next = new Adjacency(dependsOnNonTransitive.Successors); Adjacency prev = new Adjacency(dependsOnNonTransitive.Predecessors); - StronglyConnectedComponents DependsOnSCCs = + StronglyConnectedComponents dependsOnScCs = new StronglyConnectedComponents( dependsOnNonTransitive.Nodes, next, prev); - DependsOnSCCs.Compute(); + dependsOnScCs.Compute(); - VariableDescriptorToSCC = new Dictionary>(); - foreach (var scc in DependsOnSCCs) + variableDescriptorToScc = new Dictionary>(); + foreach (var scc in dependsOnScCs) { foreach (var s in scc) { - VariableDescriptorToSCC[s] = scc; + variableDescriptorToScc[s] = scc; } } - DependsOnSCCsDAG = new Graph>(); + dependsOnScCsDag = new Graph>(); foreach (var edge in dependsOnNonTransitive.Edges) { - if (VariableDescriptorToSCC[edge.Item1] != VariableDescriptorToSCC[edge.Item2]) + if (variableDescriptorToScc[edge.Item1] != variableDescriptorToScc[edge.Item2]) { - DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[edge.Item1], VariableDescriptorToSCC[edge.Item2]); + dependsOnScCsDag.AddEdge(variableDescriptorToScc[edge.Item1], variableDescriptorToScc[edge.Item2]); } } SCC dummy = new SCC(); foreach (var n in dependsOnNonTransitive.Nodes) { - DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[n], dummy); + dependsOnScCsDag.AddEdge(variableDescriptorToScc[n], dummy); } if (options.Trace) @@ -700,27 +700,27 @@ public HashSet DependsOn(VariableDescriptor v) } } - return DependsOn(VariableDescriptorToSCC[v]); + return DependsOn(variableDescriptorToScc[v]); } - public HashSet DependsOn(SCC vSCC) + public HashSet DependsOn(SCC vScc) { - if (!DependsOnCache.ContainsKey(vSCC)) + if (!dependsOnCache.ContainsKey(vScc)) { HashSet result = new HashSet(); - if (vSCC.Count() > 0) + if (vScc.Count() > 0) { - result.UnionWith(vSCC); - foreach (var wSCC in DependsOnSCCsDAG.Successors(vSCC)) + result.UnionWith(vScc); + foreach (var wScc in dependsOnScCsDag.Successors(vScc)) { - result.UnionWith(DependsOn(wSCC)); + result.UnionWith(DependsOn(wScc)); } } - DependsOnCache[vSCC] = result; + dependsOnCache[vScc] = result; } - return DependsOnCache[vSCC]; + return dependsOnCache[vScc]; } public void Dump() @@ -731,34 +731,34 @@ public void Dump() options.OutputWriter.WriteLine("Global variables"); options.OutputWriter.WriteLine("================"); - foreach (var GlobalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor)) + foreach (var globalEntry in dependsOnNonTransitive.Nodes.Where(item => item is GlobalDescriptor)) { - dump(GlobalEntry); + Dump(globalEntry); } foreach (var proc in Procedures()) { options.OutputWriter.WriteLine("Variables of " + proc); options.OutputWriter.WriteLine("====================="); - foreach (var LocalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor - && ((LocalDescriptor) Item).Proc.Equals( + foreach (var localEntry in dependsOnNonTransitive.Nodes.Where(item => item is LocalDescriptor + && ((LocalDescriptor) item).Proc.Equals( proc))) { - dump(LocalEntry); + Dump(localEntry); } } } - private void dump(VariableDescriptor vd) + private void Dump(VariableDescriptor vd) { options.OutputWriter.Write(vd + " <- {"); bool first = true; - var SortedDependents = DependsOn(vd).ToList(); - SortedDependents.Sort(); - foreach (var Descriptor in SortedDependents) + var sortedDependents = DependsOn(vd).ToList(); + sortedDependents.Sort(); + foreach (var descriptor in sortedDependents) { - options.OutputWriter.Write((first ? "" : ",") + "\n " + Descriptor); + options.OutputWriter.Write((first ? "" : ",") + "\n " + descriptor); if (first) { first = false; @@ -771,8 +771,8 @@ private void dump(VariableDescriptor vd) private HashSet Procedures() { - return new HashSet(dependsOnNonTransitive.Nodes.Where(Item => - Item is LocalDescriptor).Select(Item => ((LocalDescriptor) Item).Proc)); + return new HashSet(dependsOnNonTransitive.Nodes.Where(item => + item is LocalDescriptor).Select(item => ((LocalDescriptor) item).Proc)); } } diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index b36443f38..c8f378583 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.4 + 3.4.0 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 764ea17a4..a6f5bfd60 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -1667,6 +1667,14 @@ that makes all verification conditions valid. Without option {:subsumption n} Overrides the /subsumption command-line setting for this assertion. + {:isolate} + Places this assertion into a separate VC, where all other assertions are assumptions. + In the remaining VC, this assertion becomes an assumption + + {:isolate ""paths""} + Similar to the above, except a separate VC is created for each control flow path that leads to the marked assertion. + However, only goto commands that are annotated with {:allow_split} cause additional VCs to be created. + {:focus} Splits verification into two problems. First problem deletes all paths that do not have the focus block. Second problem considers the paths diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 2af21485a..689e7cf82 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -67,7 +67,7 @@ public class DomRelation private int sourceNum; // (number for) root of the graph private readonly Node source; // root of the graph private readonly Graph graph; - private Dictionary> immediateDominatorMap; + private Dictionary> immediateDominateesMap; [NotDelayed] internal DomRelation(Graph g, Node source) @@ -79,12 +79,12 @@ internal DomRelation(Graph g, Node source) NewComputeDominators(); } - public Dictionary> ImmediateDominatorMap + public Dictionary> ImmediateDominateesMap { get { - Contract.Assume(immediateDominatorMap != null); - return immediateDominatorMap; + Contract.Assume(immediateDominateesMap != null); + return immediateDominateesMap; } } @@ -298,26 +298,25 @@ private void NewComputeDominators() #region Populate the Immediate Dominator Map - int sourceNum = nodeToPostOrderNumber[source]; - immediateDominatorMap = new Dictionary>(); + immediateDominateesMap = new Dictionary>(); for (int i = 1; i <= n; i++) { Node node = postOrderNumberToNode[i]; - Node idomNode = postOrderNumberToNode[nodeNumberToImmediateDominator[i]]; + Node immediateDominator = postOrderNumberToNode[nodeNumberToImmediateDominator[i]]; if (i == sourceNum && nodeNumberToImmediateDominator[i] == sourceNum) { continue; } - if (immediateDominatorMap.ContainsKey(idomNode)) + if (immediateDominateesMap.ContainsKey(immediateDominator)) { - immediateDominatorMap[idomNode].Add(node); + immediateDominateesMap[immediateDominator].Add(node); } else { - List l = new List(); + var l = new List(); l.Add(node); - immediateDominatorMap.Add(idomNode, l); + immediateDominateesMap.Add(immediateDominator, l); } } @@ -347,12 +346,11 @@ private static int Intersect(int b1, int b2, int[] doms) private void PostOrderVisit(Node /*!*/ n, HashSet visited, ref int currentNumber) { Contract.Requires(n != null); - if (visited.Contains(n)) + if (!visited.Add(n)) { return; } - visited.Add(n); foreach (Node /*!*/ child in graph.Successors(n)) { Contract.Assert(child != null); @@ -415,13 +413,43 @@ public Node LeastCommonAncestor(Node n1, Node n2) int lca = Intersect(num1, num2, nodeNumberToImmediateDominator); return postOrderNumberToNode[lca]; } + + public Node GetImmediateDominator(Node node) + { + return postOrderNumberToNode[nodeNumberToImmediateDominator[nodeToPostOrderNumber[node]]]; + } + + public ISet GetNodesUntilImmediateDominatorForDag(Node node) + { + var dominator = GetImmediateDominator(node); + + var result = new HashSet(); + var toVisit = new Stack(graph.Predecessors(node)); + while (toVisit.Any()) + { + var current = toVisit.Pop(); + if (Equals(current, dominator)) + { + continue; + } + + result.Add(current); + + foreach (var predecessor in graph.Predecessors(current)) + { + toVisit.Push(predecessor); + } + } + + return result; + } } public class Graph { private HashSet> edges; private HashSet nodes; - private Node source; + public Node Source { get; set; } private bool reducible; private HashSet headers; private Dictionary> backEdgeNodes; @@ -509,7 +537,7 @@ public void AddSource(Node /*!*/ x) // BUGBUG: This generates bad code in the compiler //ns += new Set{x}; nodes.Add(x); - source = x; + Source = x; } public void AddEdge(Node /*!*/ source, Node /*!*/ dest) @@ -613,10 +641,10 @@ public List SuccessorsAsList(Node n) { get { - Contract.Assert(source != null); + Contract.Assert(Source != null); if (dominatorMap == null) { - dominatorMap = new DomRelation(this, source); + dominatorMap = new DomRelation(this, Source); } return dominatorMap; @@ -682,7 +710,7 @@ public Dictionary ImmediateDominator() immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => indexPerNode[e])); } - immediateDominator.Remove(source); + immediateDominator.Remove(Source); return immediateDominator; } @@ -690,13 +718,13 @@ public Dictionary> ImmediateDominatorMap { get { - Contract.Assert(source != null); + Contract.Assert(Source != null); if (dominatorMap == null) { - dominatorMap = new DomRelation(this, source); + dominatorMap = new DomRelation(this, Source); } - return dominatorMap.ImmediateDominatorMap; + return dominatorMap.ImmediateDominateesMap; } } @@ -1101,7 +1129,7 @@ public HashSet SplitCandidates public void ComputeLoops() { - ReducibleResult r = ComputeReducible(this, source); + ReducibleResult r = ComputeReducible(this, Source); reducible = r.reducible; headers = r.headers; backEdgeNodes = r.backEdgeNodes; @@ -1154,7 +1182,7 @@ public string ToDot(Func NodeLabel = null, Func Node return s.ToString(); } - public ISet ComputeReachability(Node start, bool forward = true) + public HashSet ComputeReachability(Node start, bool forward = true) { var todo = new Stack(); var visited = new HashSet(); @@ -1179,7 +1207,7 @@ public ISet ComputeReachability(Node start, bool forward = true) public ICollection Reachable() { - return ComputeReachability(source); + return ComputeReachability(Source); } } // end: class Graph diff --git a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs index 94505c1c9..0a3787750 100644 --- a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs @@ -74,6 +74,6 @@ public async Task SomeVariablesAreRenamed() options.RandomSeed = randomSeed; options.NormalizeNames = false; var randomOptionsLogs = await GetProverLogs.GetProverLogForProgram(options, program); - Assert.IsTrue(randomOptionsLogs.Contains("random2084218992")); + Assert.IsTrue(randomOptionsLogs.Contains("random506996257")); } } \ No newline at end of file diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs index 561113331..40298b460 100644 --- a/Source/VCGeneration/BlockTransformations.cs +++ b/Source/VCGeneration/BlockTransformations.cs @@ -12,7 +12,7 @@ namespace VCGeneration; public static class BlockTransformations { - public static void Optimize(List blocks) { + public static void Optimize(IList blocks) { foreach (var block in blocks) { // make blocks ending in assume false leaves of the CFG-DAG @@ -20,11 +20,8 @@ public static void Optimize(List blocks) { } DeleteBlocksNotLeadingToAssertions(blocks); - DeleteUselessBlocks(blocks); - - var coalesced = BlockCoalescer.CoalesceFromRootBlock(blocks); - blocks.Clear(); - blocks.AddRange(coalesced); + DeleteStraightLineBlocksWithoutCommands(blocks); + BlockCoalescer.CoalesceInPlace(blocks); } private static void StopControlFlowAtAssumeFalse(Block block) @@ -49,7 +46,7 @@ private static void StopControlFlowAtAssumeFalse(Block block) private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; } - public static void DeleteBlocksNotLeadingToAssertions(List blocks) + public static void DeleteBlocksNotLeadingToAssertions(IList blocks) { var todo = new Stack(); var peeked = new HashSet(); @@ -99,10 +96,10 @@ private static bool ContainsAssert(Block b) public static bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd { Expr: not LiteralExpr { asBool: true } }; } - private static void DeleteUselessBlocks(IList blocks) { + public static void DeleteStraightLineBlocksWithoutCommands(IList blocks) { var toVisit = new HashSet(blocks); var removed = new HashSet(); - while(toVisit.Count > 0) { + while(toVisit.Count > 0 && blocks.Count > 1) { var block = toVisit.First(); toVisit.Remove(block); if (removed.Contains(block)) { @@ -112,12 +109,31 @@ private static void DeleteUselessBlocks(IList blocks) { continue; } - var isBranchingBlock = block.TransferCmd is GotoCmd gotoCmd1 && gotoCmd1.LabelTargets.Count > 1 && - block.Predecessors.Count != 1; - if (isBranchingBlock) { + var hasMultipleOuts = block.TransferCmd is GotoCmd gotoCmd && gotoCmd.LabelTargets.Count > 1; + var hasMultipleInsOrIsSource = block.Predecessors.Count != 1; + var hasMultipleInsAndOuts = hasMultipleOuts && hasMultipleInsOrIsSource; + if (hasMultipleInsAndOuts) { continue; } + if (!hasMultipleOuts && block.TransferCmd is GotoCmd gotoCmd2) { + // Attempt to transfer token forward + var successor = gotoCmd2.LabelTargets.FirstOrDefault(); + if (successor != null && !successor.tok.IsValid && block.tok.IsValid) { + successor.tok = block.tok; + successor.Label = block.Label; + } + } + + if (!hasMultipleInsOrIsSource) { + // Attempt to transfer token backward + var predecessor = block.Predecessors.First(); + if (!predecessor.tok.IsValid && block.tok.IsValid) { + predecessor.tok = block.tok; + predecessor.Label = block.Label; // TODO should update targetLabels + } + } + removed.Add(block); blocks.Remove(block); @@ -127,17 +143,21 @@ private static void DeleteUselessBlocks(IList blocks) { var intoCmd = (GotoCmd)predecessor.TransferCmd; intoCmd.RemoveTarget(block); if (noSuccessors) { + // The predecessor might now have become eligible for deletion toVisit.Add(predecessor); } } if (block.TransferCmd is not GotoCmd outGoto) { + // No successors means no added targets to our predecessors + // And no updates to successors continue; } foreach (var outBlock in outGoto.LabelTargets) { outBlock.Predecessors.Remove(block); if (noPredecessors) { + // The successor might now have become eligible for deletion toVisit.Add(outBlock); } } diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs index 717accf65..404dd4605 100644 --- a/Source/VCGeneration/Splits/BlockRewriter.cs +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -10,6 +10,9 @@ namespace VCGeneration.Splits; public class BlockRewriter { + private const string AllowPathIsolation = "allow_path_isolation"; + public static readonly QKeyValue AllowSplitQ = new(Token.NoToken, AllowPathIsolation); + private readonly Dictionary assumedAssertions = new(); private readonly IReadOnlyList reversedBlocks; public List OrderedBlocks { get; } @@ -35,67 +38,111 @@ public Cmd TransformAssertCmd(Cmd cmd) { return cmd; } - public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IReadOnlySet? blocksToInclude, - IToken origin) { - var blockToVisit = new Stack>(); - var newToOldBlocks = new Dictionary(); - var newLastBlock = Block.ShallowClone(lastBlock); - newLastBlock.Predecessors = lastBlock.Predecessors; - blockToVisit.Push(ImmutableStack.Create(newLastBlock)); - newToOldBlocks[newLastBlock] = lastBlock; - - while (blockToVisit.Any()) { - var path = blockToVisit.Pop(); - var firstBlock = path.Peek(); - IEnumerable predecessors = firstBlock.Predecessors; - if (blocksToInclude != null) { - predecessors = predecessors.Where(blocksToInclude.Contains); - } - var hadPredecessors = false; - foreach (var oldPrevious in predecessors) { - hadPredecessors = true; - var newPrevious = Block.ShallowClone(oldPrevious); - newPrevious.Predecessors = oldPrevious.Predecessors; - newPrevious.Cmds = oldPrevious.Cmds.Select(TransformAssertCmd).ToList(); - - newToOldBlocks[newPrevious] = oldPrevious; - if (newPrevious.TransferCmd is GotoCmd gotoCmd) { - newPrevious.TransferCmd = - new GotoCmd(gotoCmd.tok, new List { firstBlock.Label }, new List { - firstBlock - }); - } + /// + /// Each {:allow_isolate_paths} goto creates a new VC for each jump target + /// + public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IReadOnlySet blocksToInclude, IImplementationPartOrigin origin) + { + // By default, we process the foci in a top-down fashion, i.e., in the topological order. + // If the user sets the RelaxFocus flag, we use the reverse (topological) order. + var splitCommands = GetSplitCommands(blocksToInclude); + if (!splitCommands.Any()) { + return new List { CreateSplit(origin, OrderedBlocks) }; + } + + var result = new List(); - blockToVisit.Push(path.Push(newPrevious)); + AddSplitsFromIndex(ImmutableStack.Empty, 0, blocksToInclude); + return result; + + void AddSplitsFromIndex(ImmutableStack choices, int gotoIndex, IReadOnlySet blocksToIncludeForChoices) { + + if (!blocksToIncludeForChoices.Any()) { + return; + } + + var allFocusBlocksHaveBeenProcessed = gotoIndex == splitCommands.Count; + if (allFocusBlocksHaveBeenProcessed) { + + // freeBlocks consist of the predecessors of the relevant foci. + // Their assertions turn into assumes and any splits inside them are disabled. + var newBlocks = ComputeNewBlocks(blocksToIncludeForChoices, + (oldBlock, newBlock) => { + newBlock.Cmds = oldBlock == lastBlock ? oldBlock.Cmds : oldBlock.Cmds.Select(TransformAssertCmd).ToList(); + if (oldBlock == lastBlock) { + newBlock.TransferCmd = new ReturnCmd(origin); + } + }); + result.Add(CreateSplit(new PathOrigin(origin, choices.OrderBy(b => b.pos).ToList(), "paths"), newBlocks)); + } else { + var splitGoto = splitCommands[gotoIndex]; + if (!blocksToIncludeForChoices.Contains(splitGoto.Block)) + { + AddSplitsFromIndex(choices, gotoIndex + 1, blocksToIncludeForChoices); + } else { + var includedTargetBlocks = splitGoto.Goto.LabelTargets.Where(blocksToIncludeForChoices.Contains).ToList(); + + var remainingBlocks = blocksToIncludeForChoices.Where( + blk => Dag.DominatorMap.DominatedBy(splitGoto.Block, blk)).ToHashSet(); + AddSplitsFromIndex(choices, gotoIndex + 1, remainingBlocks); + + var addChoice = /*remainingBlocks.Any() ||*/ includedTargetBlocks.Count > 1; + var ancestors = Dag.ComputeReachability(splitGoto.Block, false); + foreach (var targetBlock in includedTargetBlocks) { + var descendants = Dag.ComputeReachability(targetBlock, true); + + // Recursive call that does focus the block + // Contains all the ancestors, the focus block, and the descendants. + var newChoices = addChoice ? choices.Push(targetBlock.tok) : choices; + AddSplitsFromIndex(newChoices, gotoIndex + 1, + ancestors.Union(descendants).Intersect(blocksToIncludeForChoices).ToHashSet()); + } + } } + } + } - if (!hadPredecessors) { - var filteredDag = blocksToInclude == null - ? Dag - : Program.GraphFromBlocksSubset(OrderedBlocks, blocksToInclude); - var nonDominatedBranches = path.Where(b => - !filteredDag.DominatorMap.DominatedBy(lastBlock, newToOldBlocks[b])).ToList(); - var singletonBlock = Block.ShallowClone(firstBlock); - singletonBlock.TransferCmd = new ReturnCmd(origin); - singletonBlock.Cmds = path.SelectMany(b => b.Cmds).ToList(); - yield return CreateSplit(new PathOrigin(origin, nonDominatedBranches), new List { singletonBlock }); + + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + public static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, IReadOnlySet subgraph) + { + var dominatorsPerBlock = new Dictionary>(); + foreach (var block in topologicallySortedBlocks.Where(subgraph.Contains)) + { + var dominatorsForBlock = new HashSet(); + var predecessors = block.Predecessors.Where(subgraph.Contains).ToList(); + if (predecessors.Count != 0) + { + dominatorsForBlock.UnionWith(dominatorsPerBlock[predecessors[0]]); + predecessors.ForEach(blk => dominatorsForBlock.IntersectWith(dominatorsPerBlock[blk])); } + dominatorsForBlock.Add(block); + dominatorsPerBlock[block] = dominatorsForBlock; } + return subgraph.Where(blk => dominatorsPerBlock[blk].Contains(focusBlock)).ToHashSet(); + } + + private static List<(Block Block, GotoCmd Goto)> GetSplitCommands(IEnumerable blocks) { + return blocks. + Where(t => t.TransferCmd is GotoCmd gotoCmd && gotoCmd.Attributes.FindBoolAttribute(AllowPathIsolation)). + Select(block => (block, (GotoCmd)block.TransferCmd)).ToList(); } - public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( - ISet blocksToInclude, + public List ComputeNewBlocks( + IReadOnlySet blocksToInclude, ISet freeAssumeBlocks) { - return ComputeNewBlocks(blocksToInclude, block => - freeAssumeBlocks.Contains(block) - ? block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(Options, c)).ToList() - : block.Cmds); + return ComputeNewBlocks(blocksToInclude, (oldBlock, newBlock) => { + newBlock.Cmds = freeAssumeBlocks.Contains(oldBlock) + ? oldBlock.Cmds.Select(c => CommandTransformations.AssertIntoAssume(Options, c)).ToList() + : oldBlock.Cmds; + }); } - public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( - ISet? blocksToInclude, - Func> getCommands) + public List ComputeNewBlocks( + IReadOnlySet? blocksToInclude, + Action updateNewBlock) { var newBlocks = new List(); var oldToNewBlockMap = new Dictionary(reversedBlocks.Count); @@ -110,10 +157,6 @@ public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IRead var newBlock = Block.ShallowClone(block); newBlocks.Add(newBlock); oldToNewBlockMap[block] = newBlock; - // freeBlocks consist of the predecessors of the relevant foci. - // Their assertions turn into assumes and any splits inside them are disabled. - newBlock.Cmds = getCommands(block); - if (block.TransferCmd is GotoCmd gtc) { var targets = blocksToInclude == null ? gtc.LabelTargets : gtc.LabelTargets.Where(blocksToInclude.Contains).ToList(); @@ -121,11 +164,14 @@ public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IRead targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), targets.Select(blk => oldToNewBlockMap[blk]).ToList()); } + updateNewBlock(block, newBlock); } newBlocks.Reverse(); BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); - return (newBlocks, oldToNewBlockMap); + + BlockCoalescer.CoalesceInPlace(newBlocks); + return newBlocks; } diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs index 9ed2eca04..85d69efa5 100644 --- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs +++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs @@ -8,7 +8,6 @@ using Block = Microsoft.Boogie.Block; using Cmd = Microsoft.Boogie.Cmd; using PredicateCmd = Microsoft.Boogie.PredicateCmd; -using QKeyValue = Microsoft.Boogie.QKeyValue; namespace VCGeneration; @@ -46,15 +45,19 @@ public static List GetParts(VCGenOptions options, ImplementationRun focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block).ToHashSet()); var result = new List(); - AddSplitsFromIndex(ImmutableStack.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet.Empty); + AddSplitsFromIndex(ImmutableStack.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet.Empty); return result; - void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet blocksToInclude, ISet freeAssumeBlocks) { + void AddSplitsFromIndex(ImmutableStack path, int focusIndex, IReadOnlySet blocksToInclude, ISet freeAssumeBlocks) { var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count; if (allFocusBlocksHaveBeenProcessed) { - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks); + + // freeBlocks consist of the predecessors of the relevant foci. + // Their assertions turn into assumes and any splits inside them are disabled. + var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks); IImplementationPartOrigin token = path.Any() - ? new PathOrigin(run.Implementation.tok, path.ToList()) // TODO fix + ? new PathOrigin(new ImplementationRootOrigin(run.Implementation), + path.OrderBy(t => t.pos).ToList(), "focus") : new ImplementationRootOrigin(run.Implementation); result.Add(rewriter.CreateSplit(token, newBlocks)); } else { @@ -66,7 +69,7 @@ void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet } else { - var dominatedBlocks = DominatedBlocks(rewriter.OrderedBlocks, focusBlock, blocksToInclude); + var dominatedBlocks = BlockRewriter.DominatedBlocks(rewriter.OrderedBlocks, focusBlock, blocksToInclude); // Recursive call that does NOT focus the block // Contains all blocks except the ones dominated by the focus block AddSplitsFromIndex(path, focusIndex + 1, @@ -76,33 +79,13 @@ void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet // Recursive call that does focus the block // Contains all the ancestors, the focus block, and the descendants. - AddSplitsFromIndex(path.Push(focusBlock), focusIndex + 1, + AddSplitsFromIndex(path.Push(nextToken), focusIndex + 1, ancestors.Union(descendants).Intersect(blocksToInclude).ToHashSet(), ancestors.Union(freeAssumeBlocks).ToHashSet()); } } } } - - // finds all the blocks dominated by focusBlock in the subgraph - // which only contains vertices of subgraph. - private static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, ISet subgraph) - { - var dominatorsPerBlock = new Dictionary>(); - foreach (var block in topologicallySortedBlocks.Where(subgraph.Contains)) - { - var dominatorsForBlock = new HashSet(); - var predecessors = block.Predecessors.Where(subgraph.Contains).ToList(); - if (predecessors.Count != 0) - { - dominatorsForBlock.UnionWith(dominatorsPerBlock[predecessors[0]]); - predecessors.ForEach(blk => dominatorsForBlock.IntersectWith(dominatorsPerBlock[blk])); - } - dominatorsForBlock.Add(block); - dominatorsPerBlock[block] = dominatorsForBlock; - } - return subgraph.Where(blk => dominatorsPerBlock[blk].Contains(focusBlock)).ToHashSet(); - } private static List<(Block Block, IToken Token)> GetFocusBlocks(List blocks) { return blocks. diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs index 137b678d6..9cd8bd66f 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -1,7 +1,6 @@ #nullable enable using System; using System.Collections.Generic; -using System.Collections.Immutable; using System.Linq; using Microsoft.Boogie; using VC; @@ -35,7 +34,8 @@ public static (List IsolatedParts, ManualSplit Remainder) GetParts( isolatedAssertions.Add(assert); if (isolateAttribute != null && isolateAttribute.Params.OfType().Any(p => Equals(p, "paths"))) { - results.AddRange(rewriter.GetSplitsForIsolatedPaths(block, null, assert.tok).Select(p => { + var origin = new IsolatedAssertionOrigin(new ImplementationRootOrigin(partToDivide.Implementation), assert); + results.AddRange(rewriter.GetSplitsForIsolatedPaths(block, rewriter.OrderedBlocks.ToHashSet(), origin).Select(p => { var newAssertBlock = p.Blocks.Last(); newAssertBlock.Cmds = GetCommandsForBlockWithAssert(newAssertBlock, assert); return p; @@ -49,8 +49,9 @@ public static (List IsolatedParts, ManualSplit Remainder) GetParts( if (!results.Any()) { return (results,partToDivide); } - - return (results,GetSplitWithoutIsolatedAssertions()); + + var remainder = GetSplitWithoutIsolatedAssertions(); + return (results,remainder); ManualSplit GetSplitForIsolatedAssertion(Block blockWithAssert, AssertCmd assertCmd) { var blocksToKeep = rewriter.Dag.ComputeReachability(blockWithAssert, false); @@ -60,9 +61,8 @@ List GetCommands(Block oldBlock) => ? GetCommandsForBlockWithAssert(oldBlock, assertCmd) : oldBlock.Cmds.Select(rewriter.TransformAssertCmd).ToList(); - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToKeep, GetCommands); - var origin = new IsolatedAssertionOrigin(partToDivide.Token, assertCmd); - return rewriter.CreateSplit(origin, newBlocks); + var newBlocks = rewriter.ComputeNewBlocks(blocksToKeep, (oldBlock, newBlock) => newBlock.Cmds = GetCommands(oldBlock)); + return rewriter.CreateSplit(new IsolatedAssertionOrigin(partToDivide.Token, assertCmd), newBlocks); } List GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert) @@ -84,8 +84,7 @@ ManualSplit GetSplitWithoutIsolatedAssertions() { return rewriter.CreateSplit(partToDivide.Token, partToDivide.Blocks); } - var (newBlocks, _) = rewriter.ComputeNewBlocks(null, GetCommands); - + var newBlocks = rewriter.ComputeNewBlocks(null, (oldBlock, newBlock) => newBlock.Cmds = GetCommands(oldBlock)); return rewriter.CreateSplit(partToDivide.Token, newBlocks); List GetCommands(Block block) => block.Cmds.Select(cmd => @@ -104,4 +103,5 @@ public IsolatedAssertionOrigin(IImplementationPartOrigin origin, AssertCmd isola } public string ShortName => $"{Origin.ShortName}/assert@{IsolatedAssert.Line}"; + public string KindName => "assertion"; } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index 368cb9621..a11a9f3c0 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -24,40 +24,51 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; partToDivide.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); - var isolatedBlocks = new HashSet(); + var isolatedBlockJumps = new HashSet(); foreach (var block in partToDivide.Blocks) { if (block.TransferCmd is not GotoCmd gotoCmd) { continue; } - var isTypeOfAssert = gotoCmd.tok is GotoFromReturn; + var gotoFromReturn = gotoCmd.tok as GotoFromReturn; var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate"); + var isTypeOfAssert = gotoFromReturn != null && gotoFromReturn.Origin.tok is Token; var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); if (!isolate) { continue; } - isolatedBlocks.Add(block); + isolatedBlockJumps.Add(block); var ancestors = dag.ComputeReachability(block, false); var descendants = dag.ComputeReachability(block, true); var blocksToInclude = ancestors.Union(descendants).ToHashSet(); - var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin; - var returnWasFromOriginalSource = originalReturn.tok is not Token; - if (returnWasFromOriginalSource) { - continue; - } + var originalJump = gotoFromReturn?.Origin ?? (TransferCmd)gotoCmd; if (isolateAttribute != null && isolateAttribute.Params.OfType().Any(p => Equals(p, "paths"))) { // These conditions hold if the goto was originally a return Debug.Assert(gotoCmd.LabelTargets.Count == 1); Debug.Assert(gotoCmd.LabelTargets[0].TransferCmd is not GotoCmd); - var origin = new ReturnOrigin(originalReturn); + var origin = new JumpOrigin(originalJump); results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, origin)); } else { - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, ancestors.ToHashSet()); - results.Add(rewriter.CreateSplit(new ReturnOrigin(originalReturn), newBlocks)); + var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, (oldBlock, newBlock) => { + if (ancestors.Contains(oldBlock)) { + newBlock.Cmds = oldBlock.Cmds.Select(c => CommandTransformations.AssertIntoAssume(rewriter.Options, c)) + .ToList(); + } else { + newBlock.Cmds = oldBlock.Cmds; + if (newBlock.TransferCmd is ReturnCmd && gotoFromReturn != null) { + /* + I'm not sure why this is necessary. + Possibly two block are coalesced which deletes the goto with the GotoFromReturn + */ + newBlock.TransferCmd = gotoFromReturn.Origin; + } + } + }); + results.Add(rewriter.CreateSplit(new JumpOrigin(originalJump), newBlocks)); } } @@ -68,13 +79,11 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen return (results, GetPartWithoutIsolatedReturns()); ManualSplit GetPartWithoutIsolatedReturns() { - var (newBlocks, mapping) = rewriter.ComputeNewBlocks(blocks.ToHashSet(), new HashSet()); - foreach (var (oldBlock, newBlock) in mapping) { - if (isolatedBlocks.Contains(oldBlock)) { + var newBlocks = rewriter.ComputeNewBlocks(blocks.ToHashSet(), (oldBlock, newBlock) => { + if (isolatedBlockJumps.Contains(oldBlock)) { newBlock.TransferCmd = new ReturnCmd(Token.NoToken); } - } - BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); + }); return rewriter.CreateSplit(new ImplementationRootOrigin(partToDivide.Implementation), newBlocks); } @@ -82,12 +91,13 @@ ManualSplit GetPartWithoutIsolatedReturns() { } -public class ReturnOrigin : TokenWrapper, IImplementationPartOrigin { - public ReturnCmd IsolatedReturn { get; } +public class JumpOrigin : TokenWrapper, IImplementationPartOrigin { + public TransferCmd IsolatedReturn { get; } - public ReturnOrigin(ReturnCmd isolatedReturn) : base(isolatedReturn.tok) { + public JumpOrigin(TransferCmd isolatedReturn) : base(isolatedReturn.tok) { this.IsolatedReturn = isolatedReturn; } - public string ShortName => $"/return@{IsolatedReturn.Line}"; + public string ShortName => $"/{KindName}@{IsolatedReturn.Line}"; + public string KindName => IsolatedReturn is ReturnCmd ? "return" : "goto"; } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs index 651ebdc44..a2706da9e 100644 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -16,16 +16,22 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart); var result = focussedParts.SelectMany(focussedPart => { + foreach(var block in focussedPart.Blocks) + { + block.Predecessors.Clear(); + } + Implementation.ComputePredecessorsForBlocks(focussedPart.Blocks); var (isolatedJumps, withoutIsolatedJumps) = IsolateAttributeOnJumpsHandler.GetParts(options, focussedPart, createPart); - return new[] { withoutIsolatedJumps }.Concat(isolatedJumps).SelectMany(isolatedJumpSplit => + var resultForFocusPart = new[] { withoutIsolatedJumps }.Concat(isolatedJumps).SelectMany(isolatedJumpSplit => { var (isolatedAssertions, withoutIsolatedAssertions) = IsolateAttributeOnAssertsHandler.GetParts(options, isolatedJumpSplit, createPart); var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); return isolatedAssertions.Concat(splitParts); - }); + }).ToList(); + return resultForFocusPart; }).Where(s => s.Asserts.Any()).ToList(); if (result.Any()) @@ -39,4 +45,5 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa public interface IImplementationPartOrigin : IToken { string ShortName { get; } + string KindName { get; } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/PathToken.cs b/Source/VCGeneration/Splits/PathToken.cs index b0dabe1cd..a8ce48964 100644 --- a/Source/VCGeneration/Splits/PathToken.cs +++ b/Source/VCGeneration/Splits/PathToken.cs @@ -9,13 +9,18 @@ namespace VCGeneration; public class PathOrigin : TokenWrapper, IImplementationPartOrigin { + private readonly string kindName; - public PathOrigin(IToken inner, List branches) : base(inner) { - Branches = branches; + public PathOrigin(IImplementationPartOrigin inner, List branchTokens, string kindName) : base(inner) { + this.kindName = kindName; + Inner = inner; + BranchTokens = branchTokens; } - - public List Branches { get; } - public string ShortName => $"/assert@{line}[{string.Join(",", Branches.Select(b => b.tok.line))}]"; + + public new IImplementationPartOrigin Inner { get; } + public List BranchTokens { get; } + public string ShortName => $"{Inner.ShortName}/{kindName}[{string.Join(",", BranchTokens.Select(b => b.line))}]"; + public string KindName => "path"; } class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin { @@ -24,4 +29,5 @@ public ImplementationRootOrigin(Implementation implementation) : base(implementa } public string ShortName => ""; + public string KindName => "root"; } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs index a71952000..0b6fccacf 100644 --- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs +++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs @@ -63,9 +63,10 @@ public static List GetParts(ManualSplit partToSplit) { ManualSplit CreateVc(IImplementationPartOrigin token, List blocks) { return new ManualSplit(partToSplit.Options, () => { - BlockTransformations.Optimize(blocks); - return blocks; - }, partToSplit.parent, partToSplit.Run, token); + BlockTransformations.Optimize(blocks); + return blocks; + }, + partToSplit.parent, partToSplit.Run, token); } } @@ -131,7 +132,7 @@ private static bool ShouldSplitHere(Cmd c) { return null; } - return createVc(new SplitOrigin(split?.tok ?? partToSplit.Token), newBlocks); + return createVc(split == null ? partToSplit.Token : new SplitOrigin(partToSplit.Token, split.tok), newBlocks); List GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock) { @@ -208,9 +209,14 @@ private static void AddJumpsToNewBlocks(Dictionary oldToNewBlockMa } class SplitOrigin : TokenWrapper, IImplementationPartOrigin { - public SplitOrigin(IToken inner) : base(inner) - { + public new IImplementationPartOrigin Inner { get; } + public IToken Tok { get; } + + public SplitOrigin(IImplementationPartOrigin inner, IToken tok) : base(tok) { + Inner = inner; + Tok = tok; } - public string ShortName => $"/split@{line}"; + public string ShortName => $"{Inner.ShortName}/split@{line}"; + public string KindName => "split"; } \ No newline at end of file diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs index 90ab89089..a0974a7d4 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -26,7 +26,7 @@ public static Block GenerateUnifiedExit(Implementation impl) if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - var unifiedExit = new Block(Token.NoToken, unifiedExitLabel, new List(), + var unifiedExit = new Block(Token.NoToken, unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); Contract.Assert(unifiedExit != null); foreach (var block in impl.Blocks) { diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index c0463d88f..cef701469 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -11,6 +11,7 @@ using System.Threading; using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; +using VCGeneration; using VCGeneration.Transformations; namespace VC @@ -571,11 +572,11 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, if (newCounterexample is ReturnCounterexample returnExample) { - foreach (var b in returnExample.Trace) + foreach (var block in returnExample.Trace) { - Contract.Assert(b != null); - Contract.Assume(b.TransferCmd != null); - if (b.TransferCmd.tok is GotoFromReturn gotoFromReturn) { + Contract.Assert(block != null); + Contract.Assume(block.TransferCmd != null); + if (block.TransferCmd.tok is GotoFromReturn gotoFromReturn) { returnExample.FailingReturn = gotoFromReturn.Origin; } } @@ -762,9 +763,10 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) if (Options.RemoveEmptyBlocks) { #region Get rid of empty blocks - { RemoveEmptyBlocks(impl.Blocks); + // var copy = impl.Blocks.ToList(); + // BlockTransformations.DeleteStraightLineBlocksWithoutCommands(impl.Blocks); impl.PruneUnreachableBlocks(Options); } @@ -1646,6 +1648,7 @@ static void RemoveEmptyBlocks(IList blocks) // generate renameInfoForStartBlock GotoCmd gtc = curr.TransferCmd as GotoCmd; + renameInfo[curr] = null; if (gtc == null || gtc.LabelTargets == null || gtc.LabelTargets.Count == 0) { @@ -1696,19 +1699,23 @@ static void RemoveEmptyBlocks(IList blocks) { continue; } + + if (gtc is { Attributes: not null }) { + keep.Add(curr); + } - foreach (Block s in gtc.LabelTargets) + foreach (Block successor in gtc.LabelTargets) { - if (!visited.Contains(s)) + if (!visited.Contains(successor)) { - visited.Add(s); - stack.Push(s); + visited.Add(successor); + stack.Push(successor); } - else if (grey.Contains(s) && !postorder.Contains(s)) + else if (grey.Contains(successor) && !postorder.Contains(successor)) { // s is a loop head - keep.Add(s); - } + keep.Add(successor); + } } } } diff --git a/Test/implementationDivision/focus/focus.bpl b/Test/implementationDivision/focus/focus.bpl index 735a57d47..432235c4c 100644 --- a/Test/implementationDivision/focus/focus.bpl +++ b/Test/implementationDivision/focus/focus.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie /printSplit:%t /errorTrace:0 "%s" > "%t" +// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" procedure Ex() returns (y: int) diff --git a/Test/implementationDivision/focus/focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect index 2c28a1a35..8bb01ee29 100644 --- a/Test/implementationDivision/focus/focus.bpl.expect +++ b/Test/implementationDivision/focus/focus.bpl.expect @@ -1,3 +1,118 @@ +implementation Ex() returns (y: int) +{ + + anon0: + assert 5 + 0 == 5; + assert 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} 0 >= x#AT#0; + assume y#AT#2 == y#AT#0; + assert y#AT#2 >= 0; + return; +} + + +implementation Ex/focus[16]/split@15() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assert {:split_here} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 16; + assert {:focus} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} 3 <= x#AT#1; + assert 2 < 2; + goto ; +} + + +implementation Ex/focus[16,25]() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 16; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} 3 <= x#AT#1; + assume 2 < 2; + assert {:focus} (x#AT#1 + y#AT#1) * (x#AT#1 + y#AT#1) == 25; + assert x#AT#1 + y#AT#1 == 5; + assert x#AT#1 * x#AT#1 <= 25; + assume false; + assume y#AT#2 == y#AT#1; + return; +} + + +implementation Ex/focus[16,20]() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 16; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} x#AT#1 < 3; + assert 2 < 2; + assert {:focus} y#AT#1 * y#AT#1 > 4; + goto ; +} + + +implementation Ex/focus[16,20,25]() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 16; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} x#AT#1 < 3; + assume 2 < 2; + assume y#AT#1 * y#AT#1 > 4; + assert {:focus} (x#AT#1 + y#AT#1) * (x#AT#1 + y#AT#1) == 25; + assert x#AT#1 + y#AT#1 == 5; + assert x#AT#1 * x#AT#1 <= 25; + assume false; + assume y#AT#2 == y#AT#1; + return; +} + + focus.bpl(15,5): Error: this assertion could not be proved +implementation focusInconsistency/focus[38](x: int) returns (y: int) +{ + + anon0: + assume {:where i} false && true; + assume {:partition} 0 >= x; + assume {:focus} true; + assert false; + return; +} + + Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl index 59cd30f93..797bb2ecf 100644 --- a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl @@ -5,13 +5,13 @@ procedure IsolateAssertion(x: int, y: int) { var z: int; z := 0; - if (x > 0) { + if {:allow_path_isolation} (x > 0) { z := z + 1; } else { z := z + 2; } - if (y > 0) { + if {:allow_path_isolation} (y > 0) { z := z + 3; } else { z := z + 4; @@ -25,13 +25,23 @@ procedure IsolatePathsAssertion(x: int, y: int) { var z: int; z := 0; - if (x > 0) { + if {:allow_path_isolation} (x > 0) { z := z + 1; - } else { + } + else if {:allow_path_isolation} (x > 1) { z := z + 2; + } + else { + z := z + 1; } if (y > 0) { + z := z + 0; + } else { + z := z + 0; + } + + if {:allow_path_isolation} (y > 0) { z := z + 3; } else { z := z + 4; diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect index 27589907d..c17e44842 100644 --- a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect @@ -8,12 +8,15 @@ implementation IsolateAssertion/assert@20(x: int, y: int) assume {:partition} x > 0; assume z#AT#0 == 0 + 1; assume z#AT#2 == z#AT#0; - goto anon8_Then, anon8_Else; + goto anon3; anon7_Else: assume {:partition} 0 >= x; assume z#AT#1 == 0 + 2; assume z#AT#2 == z#AT#1; + goto anon3; + + anon3: goto anon8_Then, anon8_Else; anon8_Then: @@ -45,12 +48,15 @@ implementation IsolateAssertion(x: int, y: int) assume {:partition} x > 0; assume z#AT#0 == 0 + 1; assume z#AT#2 == z#AT#0; - goto anon8_Then, anon8_Else; + goto anon3; anon7_Else: assume {:partition} 0 >= x; assume z#AT#1 == 0 + 2; assume z#AT#2 == z#AT#1; + goto anon3; + + anon3: goto anon8_Then, anon8_Else; anon8_Then: @@ -75,66 +81,192 @@ implementation IsolateAssertion(x: int, y: int) isolateAssertion.bpl(20,3): Error: this assertion could not be proved isolateAssertion.bpl(21,3): Error: this assertion could not be proved -implementation IsolatePathsAssertion/assert@40[29,35](x: int, y: int) +implementation IsolatePathsAssertion/assert@50/paths[29,45](x: int, y: int) { anon0: assume {:partition} x > 0; assume z#AT#0 == 0 + 1; - assume z#AT#2 == z#AT#0; + assume z#AT#3 == z#AT#0; + goto anon13_Then, anon13_Else; + + anon13_Then: assume {:partition} y > 0; - assume z#AT#3 == z#AT#2 + 3; - assume z#AT#5 == z#AT#3; - assume z#AT#5 > 1; - assert {:isolate "paths"} z#AT#5 > 5; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: + assume {:partition} 0 >= y; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} y > 0; + assume z#AT#7 == z#AT#6 + 3; + assume z#AT#9 == z#AT#7; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; + return; +} + + +implementation IsolatePathsAssertion/assert@50/paths[29,47](x: int, y: int) +{ + + anon0: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#3 == z#AT#0; + goto anon13_Then, anon13_Else; + + anon13_Then: + assume {:partition} y > 0; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: + assume {:partition} 0 >= y; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} 0 >= y; + assume z#AT#8 == z#AT#6 + 4; + assume z#AT#9 == z#AT#8; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; return; } -implementation IsolatePathsAssertion/assert@40[31,35](x: int, y: int) +implementation IsolatePathsAssertion/assert@50/paths[31,32,45](x: int, y: int) { anon0: assume {:partition} 0 >= x; + assume {:partition} x > 1; assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; + assume z#AT#3 == z#AT#1; + goto anon13_Then, anon13_Else; + + anon13_Then: assume {:partition} y > 0; - assume z#AT#3 == z#AT#2 + 3; - assume z#AT#5 == z#AT#3; - assume z#AT#5 > 1; - assert {:isolate "paths"} z#AT#5 > 5; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: + assume {:partition} 0 >= y; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} y > 0; + assume z#AT#7 == z#AT#6 + 3; + assume z#AT#9 == z#AT#7; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; return; } -implementation IsolatePathsAssertion/assert@40[29,37](x: int, y: int) +implementation IsolatePathsAssertion/assert@50/paths[31,32,47](x: int, y: int) { anon0: - assume {:partition} x > 0; - assume z#AT#0 == 0 + 1; - assume z#AT#2 == z#AT#0; + assume {:partition} 0 >= x; + assume {:partition} x > 1; + assume z#AT#1 == 0 + 2; + assume z#AT#3 == z#AT#1; + goto anon13_Then, anon13_Else; + + anon13_Then: + assume {:partition} y > 0; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: assume {:partition} 0 >= y; - assume z#AT#4 == z#AT#2 + 4; - assume z#AT#5 == z#AT#4; - assume z#AT#5 > 1; - assert {:isolate "paths"} z#AT#5 > 5; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} 0 >= y; + assume z#AT#8 == z#AT#6 + 4; + assume z#AT#9 == z#AT#8; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; return; } -implementation IsolatePathsAssertion/assert@40[31,37](x: int, y: int) +implementation IsolatePathsAssertion/assert@50/paths[31,35,45](x: int, y: int) { anon0: assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; + assume {:partition} 1 >= x; + assume z#AT#2 == 0 + 1; + assume z#AT#3 == z#AT#2; + goto anon13_Then, anon13_Else; + + anon13_Then: + assume {:partition} y > 0; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: assume {:partition} 0 >= y; - assume z#AT#4 == z#AT#2 + 4; - assume z#AT#5 == z#AT#4; - assume z#AT#5 > 1; - assert {:isolate "paths"} z#AT#5 > 5; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} y > 0; + assume z#AT#7 == z#AT#6 + 3; + assume z#AT#9 == z#AT#7; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; + return; +} + + +implementation IsolatePathsAssertion/assert@50/paths[31,35,47](x: int, y: int) +{ + + anon0: + assume {:partition} 0 >= x; + assume {:partition} 1 >= x; + assume z#AT#2 == 0 + 1; + assume z#AT#3 == z#AT#2; + goto anon13_Then, anon13_Else; + + anon13_Then: + assume {:partition} y > 0; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon13_Else: + assume {:partition} 0 >= y; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + assume {:partition} 0 >= y; + assume z#AT#8 == z#AT#6 + 4; + assume z#AT#9 == z#AT#8; + assume z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; return; } @@ -143,41 +275,65 @@ implementation IsolatePathsAssertion(x: int, y: int) { anon0: - goto anon7_Then, anon7_Else; + goto anon11_Then, anon11_Else; - anon7_Then: + anon11_Then: assume {:partition} x > 0; assume z#AT#0 == 0 + 1; - assume z#AT#2 == z#AT#0; - goto anon8_Then, anon8_Else; + assume z#AT#3 == z#AT#0; + goto anon13_Then, anon13_Else; - anon7_Else: + anon11_Else: assume {:partition} 0 >= x; + goto anon12_Then, anon12_Else; + + anon12_Then: + assume {:partition} x > 1; assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - goto anon8_Then, anon8_Else; + assume z#AT#3 == z#AT#1; + goto anon13_Then, anon13_Else; - anon8_Then: + anon12_Else: + assume {:partition} 1 >= x; + assume z#AT#2 == 0 + 1; + assume z#AT#3 == z#AT#2; + goto anon13_Then, anon13_Else; + + anon13_Then: assume {:partition} y > 0; - assume z#AT#3 == z#AT#2 + 3; - assume z#AT#5 == z#AT#3; - goto anon6; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; - anon8_Else: + anon13_Else: assume {:partition} 0 >= y; - assume z#AT#4 == z#AT#2 + 4; - assume z#AT#5 == z#AT#4; - goto anon6; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; - anon6: - assert z#AT#5 > 1; - assume z#AT#5 > 5; - assert z#AT#5 > 6; + anon7: + goto anon14_Then, anon14_Else; + + anon14_Then: + assume {:partition} y > 0; + assume z#AT#7 == z#AT#6 + 3; + assume z#AT#9 == z#AT#7; + goto anon10; + + anon14_Else: + assume {:partition} 0 >= y; + assume z#AT#8 == z#AT#6 + 4; + assume z#AT#9 == z#AT#8; + goto anon10; + + anon10: + assert z#AT#9 > 1; + assume z#AT#9 > 5; + assert z#AT#9 > 6; return; } -isolateAssertion.bpl(40,3): Error: this assertion could not be proved -isolateAssertion.bpl(41,3): Error: this assertion could not be proved +isolateAssertion.bpl(50,3): Error: this assertion could not be proved Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/implementationDivision/isolateJump/isolateContinue.bpl b/Test/implementationDivision/isolateJump/isolateContinue.bpl new file mode 100644 index 000000000..3a524564b --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateContinue.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure IsolateContinue(x: int) returns (r: int) + requires x >= 10; + ensures r >= 10; +{ + var i: int; + i := x; + r := 0; + while(i > 0) + invariant r >= 10 - i; + { + i := i - 1; + if (i == 3) { + r := r + 2; + goto {:isolate} Continue; + } + r := r + 1; + Continue: + } +} \ No newline at end of file diff --git a/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect new file mode 100644 index 000000000..564b013b1 --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateContinue.bpl.expect @@ -0,0 +1,49 @@ +implementation IsolateContinue(x: int) returns (r: int) +{ + + anon0: + assume x >= 10; + assert 0 >= 10 - x; + assume r#AT#0 >= 10 - i#AT#0; + goto anon4_LoopDone, anon4_LoopBody; + + anon4_LoopDone: + assume {:partition} 0 >= i#AT#0; + assume r#AT#4 == r#AT#0; + assert r#AT#4 >= 10; + return; + + anon4_LoopBody: + assume {:partition} i#AT#0 > 0; + assume i#AT#1 == i#AT#0 - 1; + assume {:partition} i#AT#1 != 3; + assume r#AT#2 == r#AT#0 + 1; + assume r#AT#3 == r#AT#2; + assert r#AT#3 >= 10 - i#AT#1; + assume false; + assume r#AT#4 == r#AT#3; + return; +} + + +implementation IsolateContinue/goto@17(x: int) returns (r: int) +{ + + anon0: + assume x >= 10; + assume 0 >= 10 - x; + assume r#AT#0 >= 10 - i#AT#0; + assume {:partition} i#AT#0 > 0; + assume i#AT#1 == i#AT#0 - 1; + assume {:partition} i#AT#1 == 3; + assume r#AT#1 == r#AT#0 + 2; + assume r#AT#3 == r#AT#1; + assert r#AT#3 >= 10 - i#AT#1; + assume false; + assume r#AT#4 == r#AT#3; + return; +} + + + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl b/Test/implementationDivision/isolateJump/isolateJump.bpl index d40ee651c..4b9999980 100644 --- a/Test/implementationDivision/isolateJump/isolateJump.bpl +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl @@ -23,16 +23,26 @@ procedure IsolateReturnPaths(x: int, y: int) returns (r: int) ensures r > 4; { r := 0; - if (x > 0) { + if {:allow_path_isolation} (x > 0) { r := r + 1; - } else { + } + else if {:allow_path_isolation} (x > 1) { r := r + 2; + } + else { + r := r + 3; } - if (y > 0) { + if (x + y > 0) { + r := 0; + } else { + r := 0; + } + + if {:allow_path_isolation} (y > 0) { r := r + 3; return {:isolate "paths"}; } - r := r + 4; + r := r + 6; } \ No newline at end of file diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect index 9c32be2a1..f83e90f0d 100644 --- a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect @@ -20,9 +20,6 @@ implementation IsolateReturn(x: int, y: int) returns (r: int) assume {:partition} 0 >= y; assume r#AT#4 == r#AT#2 + 4; assume r#AT#5 == r#AT#4; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assert r#AT#5 > 4; return; } @@ -50,9 +47,6 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int) assume {:partition} y > 0; assume r#AT#3 == r#AT#2 + 3; assume r#AT#5 == r#AT#3; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assert r#AT#5 > 4; return; } @@ -64,63 +58,130 @@ implementation IsolateReturnPaths(x: int, y: int) returns (r: int) { anon0: - goto anon6_Then, anon6_Else; + goto anon10_Then, anon10_Else; - anon6_Then: + anon10_Then: assume {:partition} x > 0; assume r#AT#0 == 0 + 1; - assume r#AT#2 == r#AT#0; - goto anon7_Else; + goto anon12_Then, anon12_Else; - anon6_Else: + anon10_Else: assume {:partition} 0 >= x; + goto anon11_Then, anon11_Else; + + anon11_Then: + assume {:partition} x > 1; assume r#AT#1 == 0 + 2; - assume r#AT#2 == r#AT#1; - goto anon7_Else; + goto anon12_Then, anon12_Else; - anon7_Else: - assume {:partition} 0 >= y; - assume r#AT#4 == r#AT#2 + 4; - assume r#AT#5 == r#AT#4; - goto GeneratedUnifiedExit; + anon11_Else: + assume {:partition} 1 >= x; + assume r#AT#2 == 0 + 3; + goto anon12_Then, anon12_Else; - GeneratedUnifiedExit: - assert r#AT#5 > 4; + anon12_Then: + assume {:partition} x + y > 0; + assume r#AT#3 == 0; + goto anon7; + + anon12_Else: + assume {:partition} 0 >= x + y; + assume r#AT#3 == 0; + goto anon7; + + anon7: + assume {:partition} 0 >= y; + assume r#AT#5 == r#AT#3 + 6; + assume r#AT#6 == r#AT#5; + assert r#AT#6 > 4; return; } -implementation IsolateReturnPaths/assert@34[27](x: int, y: int) returns (r: int) +implementation IsolateReturnPaths/return@44/paths[27](x: int, y: int) returns (r: int) { anon0: assume {:partition} x > 0; assume r#AT#0 == 0 + 1; - assume r#AT#2 == r#AT#0; + goto anon12_Then, anon12_Else; + + anon12_Then: + assume {:partition} x + y > 0; + assume r#AT#3 == 0; + goto anon7; + + anon12_Else: + assume {:partition} 0 >= x + y; + assume r#AT#3 == 0; + goto anon7; + + anon7: assume {:partition} y > 0; - assume r#AT#3 == r#AT#2 + 3; - assume r#AT#5 == r#AT#3; - assert r#AT#5 > 4; + assume r#AT#4 == r#AT#3 + 3; + assume r#AT#6 == r#AT#4; + assert r#AT#6 > 4; return; } -implementation IsolateReturnPaths/assert@34[29](x: int, y: int) returns (r: int) +implementation IsolateReturnPaths/return@44/paths[29,30](x: int, y: int) returns (r: int) { anon0: assume {:partition} 0 >= x; + assume {:partition} x > 1; assume r#AT#1 == 0 + 2; - assume r#AT#2 == r#AT#1; + goto anon12_Then, anon12_Else; + + anon12_Then: + assume {:partition} x + y > 0; + assume r#AT#3 == 0; + goto anon7; + + anon12_Else: + assume {:partition} 0 >= x + y; + assume r#AT#3 == 0; + goto anon7; + + anon7: assume {:partition} y > 0; - assume r#AT#3 == r#AT#2 + 3; - assume r#AT#5 == r#AT#3; - assert r#AT#5 > 4; + assume r#AT#4 == r#AT#3 + 3; + assume r#AT#6 == r#AT#4; + assert r#AT#6 > 4; + return; +} + + +implementation IsolateReturnPaths/return@44/paths[29,33](x: int, y: int) returns (r: int) +{ + + anon0: + assume {:partition} 0 >= x; + assume {:partition} 1 >= x; + assume r#AT#2 == 0 + 3; + goto anon12_Then, anon12_Else; + + anon12_Then: + assume {:partition} x + y > 0; + assume r#AT#3 == 0; + goto anon7; + + anon12_Else: + assume {:partition} 0 >= x + y; + assume r#AT#3 == 0; + goto anon7; + + anon7: + assume {:partition} y > 0; + assume r#AT#4 == r#AT#3 + 3; + assume r#AT#6 == r#AT#4; + assert r#AT#6 > 4; return; } -isolateJump.bpl(34,29): Error: a postcondition could not be proved on this return path +isolateJump.bpl(44,29): Error: a postcondition could not be proved on this return path isolateJump.bpl(23,3): Related location: this is the postcondition that could not be proved -Boogie program verifier finished with 0 verified, 2 errors +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect index a48405e1e..bb4ef01e6 100644 --- a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect +++ b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect @@ -26,14 +26,8 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16( { anon0: - goto anon3_Else; - - anon3_Else: assume {:partition} 0 >= x; assume r#AT#0 == 20; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assert r#AT#0 > 1; return; } @@ -43,14 +37,8 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17( { anon0: - goto anon3_Else; - - anon3_Else: assume {:partition} 0 >= x; assume r#AT#0 == 20; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assume r#AT#0 > 1; assert r#AT#0 < 10; return; @@ -61,14 +49,8 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16( { anon0: - goto anon3_Then; - - anon3_Then: assume {:partition} x > 0; assume r#AT#0 == 1; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assert r#AT#0 > 1; return; } @@ -78,14 +60,8 @@ implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@17( { anon0: - goto anon3_Then; - - anon3_Then: assume {:partition} x > 0; assume r#AT#0 == 1; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: assume r#AT#0 > 1; assert r#AT#0 < 10; return; diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect index 29725f4eb..3e453dc52 100644 --- a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect +++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect @@ -1,4 +1,4 @@ -implementation Foo/split@4() +implementation Foo() { anon3_Then: diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect index 9f213b896..0765bcc8f 100644 --- a/Test/implementationDivision/split/Split.bpl.expect +++ b/Test/implementationDivision/split/Split.bpl.expect @@ -1,4 +1,4 @@ -implementation Foo/split@4() returns (y: int) +implementation Foo() returns (y: int) { anon0: diff --git a/Test/inline/Elevator.bpl.expect b/Test/inline/Elevator.bpl.expect index 414a20f32..35323e3e9 100644 --- a/Test/inline/Elevator.bpl.expect +++ b/Test/inline/Elevator.bpl.expect @@ -17,8 +17,8 @@ Execution trace: Elevator.bpl(18,3): anon0$1 Elevator.bpl(19,3): anon10_LoopHead Elevator.bpl(22,5): anon10_LoopBody - Elevator.bpl(22,5): anon11_Else - Elevator.bpl(22,5): anon12_Else + Elevator.bpl(24,12): anon11_Else + Elevator.bpl(26,12): anon12_Else Elevator.bpl(27,7): anon13_Then Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0 diff --git a/isa.ppl b/isa.ppl new file mode 100644 index 000000000..389bb6c72 --- /dev/null +++ b/isa.ppl @@ -0,0 +1,137 @@ + +procedure IsolateAssertion(x: int, y: int); + + + +implementation IsolateAssertion(x: int, y: int) +{ + var z: int; + var z#AT#0: int; + var z#AT#1: int; + var z#AT#2: int; + var z#AT#3: int; + var z#AT#4: int; + var z#AT#5: int; + + + anon0: + goto anon7_Then, anon7_Else; + + anon7_Then: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + goto anon3; + + anon7_Else: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + goto anon3; + + anon3: + goto anon8_Then, anon8_Else; + + anon8_Then: + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + goto anon6; + + anon8_Else: + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + goto anon6; + + anon6: + assert z#AT#5 > 1; + assume z#AT#5 > 5; + assert z#AT#5 > 6; + return; +} + + + +procedure IsolatePathsAssertion(x: int, y: int); + + + +implementation IsolatePathsAssertion(x: int, y: int) +{ + var z: int; + var z#AT#0: int; + var z#AT#1: int; + var z#AT#2: int; + var z#AT#3: int; + var z#AT#4: int; + var z#AT#5: int; + var z#AT#6: int; + var z#AT#7: int; + var z#AT#8: int; + var z#AT#9: int; + + + PreconditionGeneratedEntry: + goto anon0; + + anon0: + goto anon11_Then, anon11_Else; + + anon11_Else: + assume {:partition} 0 >= x; + goto anon12_Then, anon12_Else; + + anon12_Else: + assume {:partition} 1 >= x; + assume z#AT#2 == 0 + 1; + assume z#AT#3 == z#AT#2; + goto anon13_Then, anon13_Else; + + anon13_Else: + assume {:partition} 0 >= y; + assume z#AT#5 == z#AT#3 + 0; + assume z#AT#6 == z#AT#5; + goto anon7; + + anon7: + goto anon14_Then, anon14_Else; + + anon14_Else: + assume {:partition} 0 >= y; + assume z#AT#8 == z#AT#6 + 4; + assume z#AT#9 == z#AT#8; + goto anon10; + + anon10: + assert z#AT#9 > 1; + assert {:isolate "paths"} z#AT#9 > 5; + assert z#AT#9 > 6; + return; + + anon14_Then: + assume {:partition} y > 0; + assume z#AT#7 == z#AT#6 + 3; + assume z#AT#9 == z#AT#7; + goto anon10; + + anon13_Then: + assume {:partition} y > 0; + assume z#AT#4 == z#AT#3 + 0; + assume z#AT#6 == z#AT#4; + goto anon7; + + anon12_Then: + assume {:partition} x > 1; + assume z#AT#1 == 0 + 2; + assume z#AT#3 == z#AT#1; + goto anon13_Then, anon13_Else; + + anon11_Then: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#3 == z#AT#0; + goto anon13_Then, anon13_Else; +} + + diff --git a/isolateJump.ppl b/isolateJump.ppl new file mode 100644 index 000000000..b5d97d3ff --- /dev/null +++ b/isolateJump.ppl @@ -0,0 +1,113 @@ + +procedure IsolateReturn(x: int, y: int) returns (r: int); + ensures r > 4; + + + +implementation IsolateReturn(x: int, y: int) returns (r: int) +{ + var r#AT#0: int; + var r#AT#1: int; + var r#AT#2: int; + var r#AT#3: int; + var r#AT#4: int; + var r#AT#5: int; + + + anon0: + goto anon6_Then, anon6_Else; + + anon6_Then: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + assume r#AT#2 == r#AT#0; + goto anon7_Then; + + anon6_Else: + assume {:partition} 0 >= x; + assume r#AT#1 == 0 + 2; + assume r#AT#2 == r#AT#1; + goto anon7_Then; + + anon7_Then: + assume {:partition} y > 0; + assume r#AT#3 == r#AT#2 + 3; + assume r#AT#5 == r#AT#3; + assert r#AT#5 > 4; + return; +} + + + +procedure IsolateReturnPaths(x: int, y: int) returns (r: int); + ensures r > 4; + + + +implementation IsolateReturnPaths(x: int, y: int) returns (r: int) +{ + var r#AT#0: int; + var r#AT#1: int; + var r#AT#2: int; + var r#AT#3: int; + var r#AT#4: int; + var r#AT#5: int; + var r#AT#6: int; + + + PreconditionGeneratedEntry: + goto anon0; + + anon0: + goto anon10_Then, anon10_Else; + + anon10_Else: + assume {:partition} 0 >= x; + goto anon11_Then, anon11_Else; + + anon11_Else: + assume {:partition} 1 >= x; + assume r#AT#2 == 0 + 3; + goto anon12_Then, anon12_Else; + + anon12_Else: + assume {:partition} 0 >= x + y; + assume r#AT#3 == 0; + goto anon7; + + anon7: + goto anon13_Then, anon13_Else; + + anon13_Else: + assume {:partition} 0 >= y; + assume r#AT#5 == r#AT#3 + 6; + assume r#AT#6 == r#AT#5; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#6 > 4; + return; + + anon13_Then: + assume {:partition} y > 0; + assume r#AT#4 == r#AT#3 + 3; + assume r#AT#6 == r#AT#4; + goto GeneratedUnifiedExit; + + anon12_Then: + assume {:partition} x + y > 0; + assume r#AT#3 == 0; + goto anon7; + + anon11_Then: + assume {:partition} x > 1; + assume r#AT#1 == 0 + 2; + goto anon12_Then, anon12_Else; + + anon10_Then: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + goto anon12_Then, anon12_Else; +} + +