From 09093a2d2c02fa9b9f6936258fdec6b0eb2e5a58 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 15 Oct 2024 10:54:20 +0200 Subject: [PATCH] Revert isolation (#966) --- Source/Concurrency/CivlUtil.cs | 6 +- Source/Core/AST/Absy.cs | 12 +- Source/Core/AST/{Commands => }/AbsyCmd.cs | 1394 ++++++++++++++++- Source/Core/AST/AbsyQuant.cs | 274 ++++ Source/Core/AST/{GotoBoogie => }/Block.cs | 26 +- Source/Core/AST/{Commands => }/CallCmd.cs | 8 +- .../Core/AST/{GotoBoogie => }/ChangeScope.cs | 0 Source/Core/AST/GotoBoogie/GotoCmd.cs | 159 -- Source/Core/AST/GotoBoogie/ReturnCmd.cs | 33 - Source/Core/AST/GotoBoogie/TransferCmd.cs | 33 - .../Core/AST/{Commands => }/HideRevealCmd.cs | 0 Source/Core/AST/ICarriesAttributes.cs | 26 +- Source/Core/AST/Implementation.cs | 10 +- Source/Core/AST/Program.cs | 17 +- Source/Core/AST/QKeyValue.cs | 269 ---- Source/Core/AST/QKeyValueExtensions.cs | 16 - Source/Core/AST/StructuredBoogie/BigBlock.cs | 124 -- .../BigBlocksResolutionContext.cs | 591 ------- Source/Core/AST/StructuredBoogie/BreakCmd.cs | 28 - Source/Core/AST/StructuredBoogie/IfCmd.cs | 108 -- Source/Core/AST/StructuredBoogie/StmtList.cs | 134 -- .../AST/StructuredBoogie/StmtListBuilder.cs | 98 -- .../AST/StructuredBoogie/StructuredCmd.cs | 38 - .../StructuredCmdContracts.cs | 18 - Source/Core/AST/StructuredBoogie/WhileCmd.cs | 74 - .../LiveVariableAnalysis.cs | 10 +- Source/Core/BoogiePL.atg | 21 +- Source/Core/CivlAttributes.cs | 2 +- Source/Core/CoreOptions.cs | 2 - Source/Core/FunctionDependencyChecker.cs | 16 +- Source/Core/Generic/ListExtensions.cs | 31 - Source/Core/Inline.cs | 2 +- Source/Core/Parser.cs | 21 +- Source/Core/ResolutionContext.cs | 4 +- Source/Core/Token.cs | 3 +- Source/Core/{Generic => }/Util.cs | 0 Source/Core/VariableDependenceAnalyser.cs | 17 +- Source/Directory.Build.props | 2 +- Source/ExecutionEngine/CommandLineOptions.cs | 2 +- Source/ExecutionEngine/ConsolePrinter.cs | 5 +- Source/ExecutionEngine/ExecutionEngine.cs | 9 +- .../ExecutionEngine/ExecutionEngineOptions.cs | 1 + Source/ExecutionEngine/VerificationTask.cs | 2 +- Source/Graph/Graph.cs | 81 +- .../Houdini/AnnotationDependenceAnalyser.cs | 8 +- Source/Houdini/Houdini.cs | 2 +- Source/Houdini/HoudiniSession.cs | 4 +- .../ExecutionEngineTest.cs | 3 +- .../ExecutionEngineTests/RandomSeedTest.cs | 2 +- .../AssertCounterexample.cs | 11 +- Source/VCGeneration/ConditionGeneration.cs | 25 +- .../CallCounterexample.cs | 10 +- .../CalleeCounterexampleInfo.cs | 0 .../Counterexample.cs | 17 +- .../CounterexampleComparer.cs | 0 .../TraceLocation.cs | 0 Source/VCGeneration/FocusAttribute.cs | 147 ++ Source/VCGeneration/LoopExtractor.cs | 34 +- Source/VCGeneration/ManualSplit.cs | 12 +- Source/VCGeneration/ManualSplitFinder.cs | 216 +++ .../VCGeneration/Prune/DependencyEvaluator.cs | 2 +- Source/VCGeneration/Prune/Pruner.cs | 2 +- .../ReturnCounterexample.cs | 10 +- Source/VCGeneration/SmokeTester.cs | 2 +- Source/VCGeneration/{Splits => }/Split.cs | 42 +- .../{Splits => }/SplitAndVerifyWorker.cs | 6 +- Source/VCGeneration/Splits/BlockRewriter.cs | 136 -- .../Splits/FocusAttributeHandler.cs | 116 -- .../IsolateAttributeOnAssertsHandler.cs | 106 -- .../Splits/IsolateAttributeOnJumpsHandler.cs | 87 - .../VCGeneration/Splits/ManualSplitFinder.cs | 33 - Source/VCGeneration/Splits/PathToken.cs | 27 - .../Splits/SplitAttributeHandler.cs | 216 --- Source/VCGeneration/Splits/TokenWrapper.cs | 48 - .../Transformations/DesugarReturns.cs | 132 +- .../Transformations/RemoveBackEdges.cs | 13 +- .../VerificationConditionGenerator.cs | 67 +- Source/VCGeneration/VerificationRunResult.cs | 14 +- .../{Counterexample => }/VerifierCallback.cs | 0 Source/VCGeneration/Wlp.cs | 4 +- Test/aitest0/Issue25.bpl | 8 +- Test/aitest0/Issue25.bpl.expect | 8 +- Test/commandline/SplitOnEveryAssert.bpl | 2 +- .../isolateAssertion/isolateAssertion.bpl | 42 - .../isolateAssertion.bpl.expect | 183 --- .../isolateJump/isolateJump.bpl | 38 - .../isolateJump/isolateJump.bpl.expect | 126 -- .../split/AssumeFalseSplit.bpl.expect | 36 - .../split/Split.bpl.expect | 112 -- .../focus/focus.bpl => pruning/Focus.bpl} | 0 .../Focus.bpl.expect} | 2 +- Test/pruning/MonomorphicSplit.bpl | 2 +- .../AssumeFalseSplit}/AssumeFalseSplit.bpl | 5 +- .../AssumeFalseSplit.bpl.expect | 2 + .../AssumeFalseSplit/Foo.split.0.bpl.expect | 10 + .../AssumeFalseSplit/Foo.split.1.bpl.expect | 12 + .../AssumeFalseSplit/Foo.split.2.bpl.expect | 12 + Test/test0/Split/Foo.split.0.bpl.expect | 15 + Test/test0/Split/Foo.split.1.bpl.expect | 19 + Test/test0/Split/Foo.split.2.bpl.expect | 19 + Test/test0/Split/Foo.split.3.bpl.expect | 35 + Test/test0/Split/Foo.split.4.bpl.expect | 31 + .../split => test0/Split}/Split.bpl | 6 +- Test/test0/Split/Split.bpl.expect | 5 + Test/test0/SplitOnEveryAssert.bpl | 2 +- Test/test2/Structured.bpl.expect | 1 + 106 files changed, 2577 insertions(+), 3437 deletions(-) rename Source/Core/AST/{Commands => }/AbsyCmd.cs (60%) rename Source/Core/AST/{GotoBoogie => }/Block.cs (88%) rename Source/Core/AST/{Commands => }/CallCmd.cs (99%) rename Source/Core/AST/{GotoBoogie => }/ChangeScope.cs (100%) delete mode 100644 Source/Core/AST/GotoBoogie/GotoCmd.cs delete mode 100644 Source/Core/AST/GotoBoogie/ReturnCmd.cs delete mode 100644 Source/Core/AST/GotoBoogie/TransferCmd.cs rename Source/Core/AST/{Commands => }/HideRevealCmd.cs (100%) delete mode 100644 Source/Core/AST/QKeyValue.cs delete mode 100644 Source/Core/AST/QKeyValueExtensions.cs delete mode 100644 Source/Core/AST/StructuredBoogie/BigBlock.cs delete mode 100644 Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs delete mode 100644 Source/Core/AST/StructuredBoogie/BreakCmd.cs delete mode 100644 Source/Core/AST/StructuredBoogie/IfCmd.cs delete mode 100644 Source/Core/AST/StructuredBoogie/StmtList.cs delete mode 100644 Source/Core/AST/StructuredBoogie/StmtListBuilder.cs delete mode 100644 Source/Core/AST/StructuredBoogie/StructuredCmd.cs delete mode 100644 Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs delete mode 100644 Source/Core/AST/StructuredBoogie/WhileCmd.cs delete mode 100644 Source/Core/Generic/ListExtensions.cs rename Source/Core/{Generic => }/Util.cs (100%) rename Source/VCGeneration/{Counterexample => }/AssertCounterexample.cs (82%) rename Source/VCGeneration/{Counterexample => Counterexamples}/CallCounterexample.cs (86%) rename Source/VCGeneration/{Counterexample => Counterexamples}/CalleeCounterexampleInfo.cs (100%) rename Source/VCGeneration/{Counterexample => Counterexamples}/Counterexample.cs (97%) rename Source/VCGeneration/{Counterexample => Counterexamples}/CounterexampleComparer.cs (100%) rename Source/VCGeneration/{Counterexample => Counterexamples}/TraceLocation.cs (100%) create mode 100644 Source/VCGeneration/FocusAttribute.cs create mode 100644 Source/VCGeneration/ManualSplitFinder.cs rename Source/VCGeneration/{Counterexample => }/ReturnCounterexample.cs (85%) rename Source/VCGeneration/{Splits => }/Split.cs (96%) rename Source/VCGeneration/{Splits => }/SplitAndVerifyWorker.cs (97%) delete mode 100644 Source/VCGeneration/Splits/BlockRewriter.cs delete mode 100644 Source/VCGeneration/Splits/FocusAttributeHandler.cs delete mode 100644 Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs delete mode 100644 Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs delete mode 100644 Source/VCGeneration/Splits/ManualSplitFinder.cs delete mode 100644 Source/VCGeneration/Splits/PathToken.cs delete mode 100644 Source/VCGeneration/Splits/SplitAttributeHandler.cs delete mode 100644 Source/VCGeneration/Splits/TokenWrapper.cs rename Source/VCGeneration/{Counterexample => }/VerifierCallback.cs (100%) delete mode 100644 Test/implementationDivision/isolateAssertion/isolateAssertion.bpl delete mode 100644 Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect delete mode 100644 Test/implementationDivision/isolateJump/isolateJump.bpl delete mode 100644 Test/implementationDivision/isolateJump/isolateJump.bpl.expect delete mode 100644 Test/implementationDivision/split/AssumeFalseSplit.bpl.expect delete mode 100644 Test/implementationDivision/split/Split.bpl.expect rename Test/{implementationDivision/focus/focus.bpl => pruning/Focus.bpl} (100%) rename Test/{implementationDivision/focus/focus.bpl.expect => pruning/Focus.bpl.expect} (50%) rename Test/{implementationDivision/split => test0/AssumeFalseSplit}/AssumeFalseSplit.bpl (50%) create mode 100644 Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect create mode 100644 Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect create mode 100644 Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect create mode 100644 Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect create mode 100644 Test/test0/Split/Foo.split.0.bpl.expect create mode 100644 Test/test0/Split/Foo.split.1.bpl.expect create mode 100644 Test/test0/Split/Foo.split.2.bpl.expect create mode 100644 Test/test0/Split/Foo.split.3.bpl.expect create mode 100644 Test/test0/Split/Foo.split.4.bpl.expect rename Test/{implementationDivision/split => test0/Split}/Split.bpl (64%) create mode 100644 Test/test0/Split/Split.bpl.expect diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index 49ee3003c..ac48c1164 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -307,16 +307,14 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars) public static class BlockHelper { - public static readonly IToken /*!*/ ReportedNoToken = new Token(); - public static Block Block(string label, List cmds) { - return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd); + return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd); } public static Block Block(string label, List cmds, List gotoTargets) { - return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); + return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); } } diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index c109aacbb..d8f53dbca 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -1300,7 +1300,7 @@ public override void Resolve(ResolutionContext rc) public void ResolveWhere(ResolutionContext rc) { - if (Attributes.FindBoolAttribute("assumption") && this.TypedIdent.WhereExpr != null) + if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null) { rc.Error(tok, "assumption variable may not be declared with a where clause"); } @@ -1315,7 +1315,7 @@ public override void Typecheck(TypecheckingContext tc) { (this as ICarriesAttributes).TypecheckAttributes(tc); this.TypedIdent.Typecheck(tc); - if (Attributes.FindBoolAttribute("assumption") && !this.TypedIdent.Type.IsBool) + if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool) { tc.Error(tok, "assumption variable must be of type 'bool'"); } @@ -2059,7 +2059,7 @@ public override void Emit(TokenTextWriter stream, int level) stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function "); EmitAttributes(stream); - if (Body != null && !Attributes.FindBoolAttribute("inline")) + if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline")) { Contract.Assert(DefinitionBody == null); // Boogie inlines any function whose .Body field is non-null. The parser populates the .Body field @@ -2069,7 +2069,7 @@ public override void Emit(TokenTextWriter stream, int level) stream.Write("{:inline} "); } - if (DefinitionBody != null && !Attributes.FindBoolAttribute("define")) + if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define")) { // Boogie defines any function whose .DefinitionBody field is non-null. The parser populates the .DefinitionBody field // if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then @@ -2350,7 +2350,7 @@ public String ErrorMessage public bool CanAlwaysAssume() { - return Free && Attributes.FindBoolAttribute("always_assume"); + return Free && QKeyValue.FindBoolAttribute(Attributes, "always_assume"); } @@ -2490,7 +2490,7 @@ public String ErrorMessage public bool CanAlwaysAssume () { - return Free && this.Attributes.FindBoolAttribute("always_assume"); + return Free && QKeyValue.FindBoolAttribute(this.Attributes, "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/AbsyCmd.cs similarity index 60% rename from Source/Core/AST/Commands/AbsyCmd.cs rename to Source/Core/AST/AbsyCmd.cs index 0beaa357b..a6400e232 100644 --- a/Source/Core/AST/Commands/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -7,6 +7,1188 @@ namespace Microsoft.Boogie { + //--------------------------------------------------------------------- + // BigBlock + public class BigBlock + { + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(tok != null); + Contract.Invariant(Anonymous || this.labelName != null); + Contract.Invariant(this._ec == null || this._tc == null); + Contract.Invariant(this._simpleCmds != null); + } + + public readonly IToken /*!*/ + tok; + + public readonly bool Anonymous; + + private string labelName; + + public string LabelName + { + get + { + Contract.Ensures(Anonymous || Contract.Result() != null); + return this.labelName; + } + set + { + Contract.Requires(Anonymous || value != null); + this.labelName = value; + } + } + + [Rep] private List /*!*/ _simpleCmds; + + /// + /// These come before the structured command + /// + public List /*!*/ simpleCmds + { + get + { + Contract.Ensures(Contract.Result>() != null); + return this._simpleCmds; + } + set + { + Contract.Requires(value != null); + this._simpleCmds = value; + } + } + + private StructuredCmd _ec; + + public StructuredCmd ec + { + get { return this._ec; } + set + { + Contract.Requires(value == null || this.tc == null); + this._ec = value; + } + } + + private TransferCmd _tc; + + public TransferCmd tc + { + get { return this._tc; } + set + { + Contract.Requires(value == null || this.ec == null); + this._tc = value; + } + } + + public BigBlock + successorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized) + + public BigBlock(IToken tok, string labelName, [Captured] List simpleCmds, StructuredCmd ec, TransferCmd tc) + { + Contract.Requires(simpleCmds != null); + Contract.Requires(tok != null); + Contract.Requires(ec == null || tc == null); + this.tok = tok; + this.Anonymous = labelName == null; + this.labelName = labelName; + this._simpleCmds = simpleCmds; + this._ec = ec; + this._tc = tc; + } + + public void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + if (!Anonymous) + { + stream.WriteLine(level, "{0}:", + stream.Options.PrintWithUniqueASTIds + ? String.Format("h{0}^^{1}", this.GetHashCode(), this.LabelName) + : this.LabelName); + } + + foreach (Cmd /*!*/ c in this.simpleCmds) + { + Contract.Assert(c != null); + c.Emit(stream, level + 1); + } + + if (this.ec != null) + { + this.ec.Emit(stream, level + 1); + } + else if (this.tc != null) + { + this.tc.Emit(stream, level + 1); + } + } + } + + public class StmtList + { + [Rep] private readonly List /*!*/ bigBlocks; + + public IList /*!*/ BigBlocks + { + get + { + Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(Contract.Result>().IsReadOnly); + return this.bigBlocks.AsReadOnly(); + } + } + + public List PrefixCommands; + + public readonly IToken /*!*/ + EndCurly; + + public StmtList ParentContext; + public BigBlock ParentBigBlock; + + private readonly HashSet /*!*/ + labels = new HashSet(); + + public void AddLabel(string label) + { + labels.Add(label); + } + + public IEnumerable /*!*/ Labels + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result /*!*/>())); + return this.labels.AsEnumerable(); + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(EndCurly != null); + Contract.Invariant(cce.NonNullElements(this.bigBlocks)); + Contract.Invariant(cce.NonNullElements(this.labels)); + } + + public StmtList(IList /*!*/ bigblocks, IToken endCurly) + { + Contract.Requires(endCurly != null); + Contract.Requires(cce.NonNullElements(bigblocks)); + Contract.Requires(bigblocks.Count > 0); + this.bigBlocks = new List(bigblocks); + this.EndCurly = endCurly; + } + + // prints the list of statements, not the surrounding curly braces + public void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + bool needSeperator = false; + foreach (BigBlock b in BigBlocks) + { + Contract.Assert(b != null); + Contract.Assume(cce.IsPeerConsistent(b)); + if (needSeperator) + { + stream.WriteLine(); + } + + b.Emit(stream, level); + needSeperator = true; + } + } + + /// + /// Tries to insert the commands "prefixCmds" at the beginning of the first block + /// of the StmtList, and returns "true" iff it succeeded. + /// In the event of success, the "suggestedLabel" returns as the name of the + /// block inside StmtList where "prefixCmds" were inserted. This name may be the + /// same as the one passed in, in case this StmtList has no preference as to what + /// to call its first block. In the event of failure, "suggestedLabel" is returned + /// as its input value. + /// Note, to be conservative (that is, ignoring the possible optimization that this + /// method enables), this method can do nothing and return false. + /// + public bool PrefixFirstBlock([Captured] List prefixCmds, ref string suggestedLabel) + { + Contract.Requires(suggestedLabel != null); + Contract.Requires(prefixCmds != null); + Contract.Ensures(Contract.Result() || + cce.Owner.None(prefixCmds)); // "prefixCmds" is captured only on success + Contract.Assume(PrefixCommands == null); // prefix has not been used + + BigBlock bb0 = BigBlocks[0]; + if (prefixCmds.Count == 0) + { + // This is always a success, since there is nothing to insert. Now, decide + // which name to use for the first block. + if (bb0.Anonymous) + { + bb0.LabelName = suggestedLabel; + } + else + { + Contract.Assert(bb0.LabelName != null); + suggestedLabel = bb0.LabelName; + } + + return true; + } + else + { + // There really is something to insert. We can do this inline only if the first + // block is anonymous (which implies there is no branch to it from within the block). + if (bb0.Anonymous) + { + PrefixCommands = prefixCmds; + bb0.LabelName = suggestedLabel; + return true; + } + else + { + return false; + } + } + } + } + + /// + /// The AST for Boogie structured commands was designed to support backward compatibility with + /// the Boogie unstructured commands. This has made the structured commands hard to construct. + /// The StmtListBuilder class makes it easier to build structured commands. + /// + public class StmtListBuilder + { + readonly List /*!*/ bigBlocks = new(); + + string label; + List simpleCmds; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(bigBlocks)); + } + + void Dump(StructuredCmd scmd, TransferCmd tcmd) + { + Contract.Requires(scmd == null || tcmd == null); + Contract.Ensures(label == null && simpleCmds == null); + if (label == null && simpleCmds == null && scmd == null && tcmd == null) + { + // nothing to do + } + else + { + if (simpleCmds == null) + { + simpleCmds = new List(); + } + + bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd)); + label = null; + simpleCmds = null; + } + } + + /// + /// Collects the StmtList built so far and returns it. The StmtListBuilder should no longer + /// be used once this method has been invoked. + /// + public StmtList Collect(IToken endCurlyBrace) + { + Contract.Requires(endCurlyBrace != null); + Contract.Ensures(Contract.Result() != null); + Dump(null, null); + if (bigBlocks.Count == 0) + { + simpleCmds = new List(); // the StmtList constructor doesn't like an empty list of BigBlock's + Dump(null, null); + } + + return new StmtList(bigBlocks, endCurlyBrace); + } + + public void Add(Cmd cmd) + { + Contract.Requires(cmd != null); + if (simpleCmds == null) + { + simpleCmds = new List(); + } + + simpleCmds.Add(cmd); + } + + public void Add(StructuredCmd scmd) + { + Contract.Requires(scmd != null); + Dump(scmd, null); + } + + public void Add(TransferCmd tcmd) + { + Contract.Requires(tcmd != null); + Dump(null, tcmd); + } + + public void AddLabelCmd(string label) + { + Contract.Requires(label != null); + Dump(null, null); + this.label = label; + } + + public void AddLocalVariable(string name) + { + Contract.Requires(name != null); + // TODO + } + } + + class BigBlocksResolutionContext + { + StmtList /*!*/ + stmtList; + + [Peer] List blocks; + + string /*!*/ + prefix = "anon"; + + int anon = 0; + + int FreshAnon() + { + return anon++; + } + + HashSet allLabels = new HashSet(); + + Errors /*!*/ + errorHandler; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(stmtList != null); + Contract.Invariant(cce.NonNullElements(blocks, true)); + Contract.Invariant(prefix != null); + Contract.Invariant(cce.NonNullElements(allLabels, true)); + Contract.Invariant(errorHandler != null); + } + + private void ComputeAllLabels(StmtList stmts) + { + if (stmts == null) + { + return; + } + + foreach (BigBlock bb in stmts.BigBlocks) + { + if (bb.LabelName != null) + { + allLabels.Add(bb.LabelName); + } + + ComputeAllLabels(bb.ec); + } + } + + private void ComputeAllLabels(StructuredCmd cmd) + { + if (cmd == null) + { + return; + } + + if (cmd is IfCmd) + { + IfCmd ifCmd = (IfCmd) cmd; + ComputeAllLabels(ifCmd.thn); + ComputeAllLabels(ifCmd.elseIf); + ComputeAllLabels(ifCmd.elseBlock); + } + else if (cmd is WhileCmd) + { + WhileCmd whileCmd = (WhileCmd) cmd; + ComputeAllLabels(whileCmd.Body); + } + } + + public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) + { + Contract.Requires(errorHandler != null); + Contract.Requires(stmtList != null); + this.stmtList = stmtList; + // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. + // This transformation creates a suitable jump target for break statements inside the nested while loop. + InjectEmptyBigBlockInsideWhileLoopBody(stmtList); + this.errorHandler = errorHandler; + ComputeAllLabels(stmtList); + } + + public List /*!*/ Blocks + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (blocks == null) + { + blocks = new List(); + + int startErrorCount = this.errorHandler.count; + // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. + // Also, determine a good value for "prefix". + CheckLegalLabels(stmtList, null, null); + + // fill in names of anonymous blocks + NameAnonymousBlocks(stmtList); + + // determine successor blocks + RecordSuccessors(stmtList, null); + + if (this.errorHandler.count == startErrorCount) + { + // generate blocks from the big blocks + CreateBlocks(stmtList, null); + } + } + + return blocks; + } + } + + void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) + { + foreach (var bb in stmtList.BigBlocks) + { + InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); + } + } + + void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) + { + if (structuredCmd is WhileCmd whileCmd) + { + InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); + if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) + { + var newBigBlocks = new List(whileCmd.Body.BigBlocks); + newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); + whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); + } + } + else if (structuredCmd is IfCmd ifCmd) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); + if (ifCmd.elseBlock != null) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); + } + + if (ifCmd.elseIf != null) + { + InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); + } + } + } + + void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) + { + Contract.Requires(stmtList != null); + Contract.Requires((parentContext == null) == (parentBigBlock == null)); + Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet + //modifies stmtList.*; + Contract.Ensures(stmtList.ParentContext == parentContext); + stmtList.ParentContext = parentContext; + stmtList.ParentBigBlock = parentBigBlock; + + // record the labels declared in this StmtList + foreach (BigBlock b in stmtList.BigBlocks) + { + if (b.LabelName != null) + { + string n = b.LabelName; + if (n.StartsWith(prefix)) + { + if (prefix.Length < n.Length && n[prefix.Length] == '0') + { + prefix += "1"; + } + else + { + prefix += "0"; + } + } + + stmtList.AddLabel(b.LabelName); + } + } + + // check that labels in this and nested StmtList's are legal + foreach (BigBlock b in stmtList.BigBlocks) + { + // goto's must reference blocks in enclosing blocks + if (b.tc is GotoCmd) + { + GotoCmd g = (GotoCmd) b.tc; + foreach (string /*!*/ lbl in cce.NonNull(g.LabelNames)) + { + Contract.Assert(lbl != null); + /* + bool found = false; + for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) { + if (sl.Labels.Contains(lbl)) { + found = true; + break; + } + } + if (!found) { + this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); + } + */ + if (!allLabels.Contains(lbl)) + { + this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); + } + } + } + + // break labels must refer to an enclosing while statement + else if (b.ec is BreakCmd) + { + BreakCmd bcmd = (BreakCmd) b.ec; + Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet + bool found = false; + for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) + { + cce.LoopInvariant(sl != null); + BigBlock bb = sl.ParentBigBlock; + + if (bcmd.Label == null) + { + // a label-less break statement breaks out of the innermost enclosing while statement + if (bb.ec is WhileCmd) + { + bcmd.BreakEnclosure = bb; + found = true; + break; + } + } + else if (bcmd.Label == bb.LabelName) + { + // a break statement with a label can break out of both if statements and while statements + if (bb.simpleCmds.Count == 0) + { + // this is a good target: the label refers to the if/while statement + bcmd.BreakEnclosure = bb; + } + else + { + // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement + this.errorHandler.SemErr(bcmd.tok, + "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + } + + found = true; // don't look any further, since we've found a matching label + break; + } + } + + if (!found) + { + if (bcmd.Label == null) + { + this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); + } + else + { + this.errorHandler.SemErr(bcmd.tok, + "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); + } + } + } + + // recurse + else if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + CheckLegalLabels(wcmd.Body, stmtList, b); + } + else + { + for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + CheckLegalLabels(ifcmd.thn, stmtList, b); + if (ifcmd.elseBlock != null) + { + CheckLegalLabels(ifcmd.elseBlock, stmtList, b); + } + } + } + } + } + + void NameAnonymousBlocks(StmtList stmtList) + { + Contract.Requires(stmtList != null); + foreach (BigBlock b in stmtList.BigBlocks) + { + if (b.LabelName == null) + { + b.LabelName = prefix + FreshAnon(); + } + + if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + NameAnonymousBlocks(wcmd.Body); + } + else + { + for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + NameAnonymousBlocks(ifcmd.thn); + if (ifcmd.elseBlock != null) + { + NameAnonymousBlocks(ifcmd.elseBlock); + } + } + } + } + } + + void RecordSuccessors(StmtList stmtList, BigBlock successor) + { + Contract.Requires(stmtList != null); + for (int i = stmtList.BigBlocks.Count; 0 <= --i;) + { + BigBlock big = stmtList.BigBlocks[i]; + big.successorBigBlock = successor; + + if (big.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) big.ec; + RecordSuccessors(wcmd.Body, big); + } + else + { + for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) + { + RecordSuccessors(ifcmd.thn, successor); + if (ifcmd.elseBlock != null) + { + RecordSuccessors(ifcmd.elseBlock, successor); + } + } + } + + successor = big; + } + } + + // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; + // otherwise, it is null. + void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) + { + Contract.Requires(stmtList != null); + Contract.Requires(blocks != null); + List cmdPrefixToApply = stmtList.PrefixCommands; + + int n = stmtList.BigBlocks.Count; + foreach (BigBlock b in stmtList.BigBlocks) + { + n--; + Contract.Assert(b.LabelName != null); + List theSimpleCmds; + if (cmdPrefixToApply == null) + { + theSimpleCmds = b.simpleCmds; + } + else + { + theSimpleCmds = new List(); + theSimpleCmds.AddRange(cmdPrefixToApply); + theSimpleCmds.AddRange(b.simpleCmds); + cmdPrefixToApply = null; // now, we've used 'em up + } + + if (b.tc != null) + { + // this BigBlock has the very same components as a Block + Contract.Assert(b.ec == null); + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); + blocks.Add(block); + } + else if (b.ec == null) + { + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(stmtList.EndCurly, b); + } + + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); + blocks.Add(block); + } + else if (b.ec is BreakCmd) + { + BreakCmd bcmd = (BreakCmd) b.ec; + Contract.Assert(bcmd.BreakEnclosure != null); + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); + blocks.Add(block); + } + else if (b.ec is WhileCmd) + { + WhileCmd wcmd = (WhileCmd) b.ec; + 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 ac = new AssumeCmd(wcmd.tok, wcmd.Guard); + ac.Attributes = new QKeyValue(wcmd.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); + ssDone.Add(ac); + } + + // Try to squeeze in ssBody into the first block of wcmd.Body + bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + + // ... goto LoopHead; + Block block = new Block(b.tok, b.LabelName, theSimpleCmds, + new GotoCmd(wcmd.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) + { + ssHead.Add(yield); + } + foreach (PredicateCmd inv in wcmd.Invariants) + { + ssHead.Add(inv); + } + + block = new Block(wcmd.tok, loopHeadLabel, ssHead, + new GotoCmd(wcmd.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})); + blocks.Add(block); + } + + // recurse to create the blocks for the loop body + CreateBlocks(wcmd.Body, loopHeadLabel); + + // LoopDone: assume !guard; goto loopSuccessor; + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(wcmd.tok, b); + } + + block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); + blocks.Add(block); + } + else + { + IfCmd ifcmd = (IfCmd) b.ec; + string predLabel = b.LabelName; + List predCmds = theSimpleCmds; + + for (; ifcmd != null; ifcmd = ifcmd.elseIf) + { + var a = FreshAnon(); + string thenLabel = prefix + a + "_Then"; + Contract.Assert(thenLabel != null); + string elseLabel = prefix + a + "_Else"; + Contract.Assert(elseLabel != null); + + List ssThen = new List(); + List 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); + ssThen.Add(ac); + + ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.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 elseGuardTakenCareOf = false; + if (ifcmd.elseBlock != null) + { + elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + } + + // ... goto Then, Else; + var jumpBlock = new Block(b.tok, predLabel, predCmds, + new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + 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})); + blocks.Add(thenJumpBlock); + } + + // recurse to create the blocks for the then branch + CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); + + if (ifcmd.elseBlock != 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})); + blocks.Add(elseJumpBlock); + } + + // recurse to create the blocks for the else branch + CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); + } + else if (ifcmd.elseIf != null) + { + // this is an "else if" + predLabel = elseLabel; + predCmds = new List(); + if (ifcmd.Guard != null) + { + var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); + ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + predCmds.Add(ac); + } + } + else + { + // no else alternative is specified, so else branch is just "skip" + // Else: assume !guard; goto ifSuccessor; + TransferCmd trCmd; + if (n == 0 && runOffTheEndLabel != null) + { + // goto the given label instead of the textual successor block + trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(ifcmd.tok, b); + } + + var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + blocks.Add(block); + } + } + } + } + } + + TransferCmd GotoSuccessor(IToken tok, BigBlock b) + { + Contract.Requires(b != null); + Contract.Requires(tok != null); + Contract.Ensures(Contract.Result() != null); + if (b.successorBigBlock != null) + { + return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + } + else + { + return new ReturnCmd(tok); + } + } + } + + [ContractClass(typeof(StructuredCmdContracts))] + public abstract class StructuredCmd + { + private IToken /*!*/ + _tok; + + public IToken /*!*/ tok + { + get + { + Contract.Ensures(Contract.Result() != null); + return this._tok; + } + set + { + Contract.Requires(value != null); + this._tok = value; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this._tok != null); + } + + public StructuredCmd(IToken tok) + { + Contract.Requires(tok != null); + this._tok = tok; + } + + public abstract void Emit(TokenTextWriter /*!*/ stream, int level); + } + + [ContractClassFor(typeof(StructuredCmd))] + public abstract class StructuredCmdContracts : StructuredCmd + { + public override void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + throw new NotImplementedException(); + } + + public StructuredCmdContracts() : base(null) + { + } + } + + public class IfCmd : StructuredCmd + { + public Expr Guard; + + private StmtList /*!*/ + _thn; + + public StmtList /*!*/ thn + { + get + { + Contract.Ensures(Contract.Result() != null); + return this._thn; + } + set + { + Contract.Requires(value != null); + this._thn = value; + } + } + + private IfCmd _elseIf; + + public IfCmd elseIf + { + get { return this._elseIf; } + set + { + Contract.Requires(value == null || this.elseBlock == null); + this._elseIf = value; + } + } + + private StmtList _elseBlock; + + public StmtList elseBlock + { + get { return this._elseBlock; } + set + { + Contract.Requires(value == null || this.elseIf == null); + this._elseBlock = value; + } + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(this._thn != null); + Contract.Invariant(this._elseIf == null || this._elseBlock == null); + } + + public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) + : base(tok) + { + Contract.Requires(tok != null); + Contract.Requires(thn != null); + Contract.Requires(elseIf == null || elseBlock == null); + this.Guard = guard; + this._thn = thn; + this._elseIf = elseIf; + this._elseBlock = elseBlock; + } + + public override void Emit(TokenTextWriter stream, int level) + { + stream.Write(level, "if ("); + IfCmd /*!*/ + ifcmd = this; + while (true) + { + if (ifcmd.Guard == null) + { + stream.Write("*"); + } + else + { + ifcmd.Guard.Emit(stream); + } + + stream.WriteLine(")"); + + stream.WriteLine(level, "{"); + ifcmd.thn.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + + if (ifcmd.elseIf != null) + { + stream.Write(level, "else if ("); + ifcmd = ifcmd.elseIf; + continue; + } + else if (ifcmd.elseBlock != null) + { + stream.WriteLine(level, "else"); + stream.WriteLine(level, "{"); + ifcmd.elseBlock.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + } + + break; + } + } + } + + public class WhileCmd : StructuredCmd + { + [Peer] public Expr Guard; + + public List Invariants; + + public List Yields; + + public StmtList Body; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Body != null); + Contract.Invariant(cce.NonNullElements(Invariants)); + } + + public WhileCmd(IToken tok, [Captured] Expr guard, List invariants, List yields, StmtList body) + : base(tok) + { + Contract.Requires(cce.NonNullElements(invariants)); + Contract.Requires(body != null); + Contract.Requires(tok != null); + this.Guard = guard; + this.Invariants = invariants; + this.Yields = yields; + this.Body = body; + } + + public override void Emit(TokenTextWriter stream, int level) + { + stream.Write(level, "while ("); + if (Guard == null) + { + stream.Write("*"); + } + else + { + Guard.Emit(stream); + } + + stream.WriteLine(")"); + + foreach (var yield in Yields) + { + stream.Write(level + 1, "invariant"); + yield.Emit(stream, level + 1); + } + foreach (var inv in Invariants) + { + if (inv is AssumeCmd) + { + stream.Write(level + 1, "free invariant "); + } + else + { + stream.Write(level + 1, "invariant "); + } + + Cmd.EmitAttributes(stream, inv.Attributes); + inv.Expr.Emit(stream); + stream.WriteLine(";"); + } + + stream.WriteLine(level, "{"); + Body.Emit(stream, level + 1); + stream.WriteLine(level, "}"); + } + } + + public class BreakCmd : StructuredCmd + { + public string Label; + public BigBlock BreakEnclosure; + + public BreakCmd(IToken tok, string label) + : base(tok) + { + Contract.Requires(tok != null); + this.Label = label; + } + + public override void Emit(TokenTextWriter stream, int level) + { + if (Label == null) + { + stream.WriteLine(level, "break;"); + } + else + { + stream.WriteLine(level, "break {0};", Label); + } + } + } + + //--------------------------------------------------------------------- + // Block + //--------------------------------------------------------------------- // Commands [ContractClassFor(typeof(Cmd))] @@ -44,7 +1226,7 @@ public static void ComputeChecksums(CoreOptions options, Cmd cmd, Implementation } if (cmd is AssumeCmd assumeCmd - && assumeCmd.Attributes.FindBoolAttribute("assumption_variable_initialization")) + && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization")) { // Ignore assumption variable initializations. assumeCmd.Checksum = currentChecksum; @@ -512,7 +1694,7 @@ public override void Resolve(ResolutionContext rc) continue; } var decl = lhs.AssignedVariable.Decl; - if (lhs.AssignedVariable.Decl != null && decl.Attributes.FindBoolAttribute("assumption")) + if (lhs.AssignedVariable.Decl != null && QKeyValue.FindBoolAttribute(decl.Attributes, "assumption")) { var rhs = Rhss[i] as NAryExpr; if (rhs == null @@ -2217,6 +3399,35 @@ public override Absy StdDispatch(StandardVisitor visitor) //--------------------------------------------------------------------- // Transfer commands + [ContractClass(typeof(TransferCmdContracts))] + public abstract class TransferCmd : Absy + { + public ProofObligationDescription Description { get; set; } = new PostconditionDescription(); + + internal TransferCmd(IToken /*!*/ tok) + : base(tok) + { + Contract.Requires(tok != null); + } + + public abstract void Emit(TokenTextWriter /*!*/ stream, int level); + + public override void Typecheck(TypecheckingContext tc) + { + //Contract.Requires(tc != null); + // nothing to typecheck + } + + public override string ToString() + { + Contract.Ensures(Contract.Result() != null); + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using TokenTextWriter stream = new TokenTextWriter("", buffer, false, false, PrintOptions.Default); + this.Emit(stream, 0); + + return buffer.ToString(); + } + } [ContractClassFor(typeof(TransferCmd))] public abstract class TransferCmdContracts : TransferCmd @@ -2231,4 +3442,183 @@ public override void Emit(TokenTextWriter stream, int level) throw new NotImplementedException(); } } + + public class ReturnCmd : TransferCmd + { + public ReturnCmd(IToken /*!*/ tok) + : base(tok) + { + Contract.Requires(tok != null); + } + + public override void Emit(TokenTextWriter stream, int level) + { + //Contract.Requires(stream != null); + stream.WriteLine(this, level, "return;"); + } + + public override void Resolve(ResolutionContext rc) + { + //Contract.Requires(rc != null); + // nothing to resolve + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitReturnCmd(this); + } + } + + public class GotoCmd : TransferCmd + { + [Rep] public List LabelNames; + [Rep] public List LabelTargets; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(LabelNames == null || LabelTargets == null || LabelNames.Count == LabelTargets.Count); + } + + [NotDelayed] + public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq) + : base(tok) + { + Contract.Requires(tok != null); + Contract.Requires(labelSeq != null); + this.LabelNames = labelSeq; + } + + public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq, List /*!*/ blockSeq) + : base(tok) + { + Contract.Requires(tok != null); + Contract.Requires(labelSeq != null); + Contract.Requires(blockSeq != null); + Debug.Assert(labelSeq.Count == blockSeq.Count); + for (int i = 0; i < labelSeq.Count; i++) + { + Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label)); + } + + this.LabelNames = labelSeq; + this.LabelTargets = blockSeq; + } + + public GotoCmd(IToken /*!*/ tok, List /*!*/ blockSeq) + : 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++) + { + labelSeq.Add(cce.NonNull(blockSeq[i]).Label); + } + + this.LabelNames = labelSeq; + this.LabelTargets = blockSeq; + } + + public void RemoveTarget(Block b) { + LabelNames.Remove(b.Label); + LabelTargets.Remove(b); + } + + public void AddTarget(Block b) + { + Contract.Requires(b != null); + Contract.Requires(b.Label != null); + Contract.Requires(this.LabelTargets != null); + Contract.Requires(this.LabelNames != null); + this.LabelTargets.Add(b); + this.LabelNames.Add(b.Label); + } + + public void AddTargets(IEnumerable blocks) + { + Contract.Requires(blocks != null); + Contract.Requires(cce.NonNullElements(blocks)); + Contract.Requires(this.LabelTargets != null); + Contract.Requires(this.LabelNames != null); + foreach (var block in blocks) + { + AddTarget(block); + } + } + + public override void Emit(TokenTextWriter stream, int level) + { + //Contract.Requires(stream != null); + Contract.Assume(this.LabelNames != null); + stream.Write(this, level, "goto "); + if (stream.Options.PrintWithUniqueASTIds) + { + if (LabelTargets == null) + { + string sep = ""; + foreach (string name in LabelNames) + { + stream.Write("{0}{1}^^{2}", sep, "NoDecl", name); + sep = ", "; + } + } + else + { + string sep = ""; + foreach (Block /*!*/ b in LabelTargets) + { + Contract.Assert(b != null); + stream.Write("{0}h{1}^^{2}", sep, b.GetHashCode(), b.Label); + sep = ", "; + } + } + } + else + { + LabelNames.Emit(stream); + } + + stream.WriteLine(";"); + } + + public override void Resolve(ResolutionContext rc) + { + //Contract.Requires(rc != null); + Contract.Ensures(LabelTargets != null); + if (LabelTargets != null) + { + // already resolved + return; + } + + Contract.Assume(this.LabelNames != null); + LabelTargets = new List(); + foreach (string /*!*/ lbl in LabelNames) + { + Contract.Assert(lbl != null); + Block b = rc.LookUpBlock(lbl); + if (b == null) + { + rc.Error(this, "goto to unknown block: {0}", lbl); + } + else + { + LabelTargets.Add(b); + } + } + + Debug.Assert(rc.ErrorCount > 0 || LabelTargets.Count == LabelNames.Count); + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitGotoCmd(this); + } + } } diff --git a/Source/Core/AST/AbsyQuant.cs b/Source/Core/AST/AbsyQuant.cs index 185fa32e9..301a3bf70 100644 --- a/Source/Core/AST/AbsyQuant.cs +++ b/Source/Core/AST/AbsyQuant.cs @@ -330,6 +330,280 @@ protected List GetUnmentionedTypeParameters() } } + public class QKeyValue : Absy + { + public readonly string /*!*/ + Key; + + private readonly List /*!*/ + _params; // each element is either a string or an Expr + + public void AddParam(object p) + { + Contract.Requires(p != null); + this._params.Add(p); + } + + public void AddParams(IEnumerable ps) + { + Contract.Requires(cce.NonNullElements(ps)); + this._params.AddRange(ps); + } + + public void ClearParams() + { + this._params.Clear(); + } + + public IList Params + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Contract.Result>().IsReadOnly); + return this._params.AsReadOnly(); + } + } + + public QKeyValue Next; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(Key != null); + Contract.Invariant(cce.NonNullElements(this._params)); + } + + public QKeyValue(IToken tok, string key, IList /*!*/ parameters, QKeyValue next) + : base(tok) + { + Contract.Requires(key != null); + Contract.Requires(tok != null); + Contract.Requires(cce.NonNullElements(parameters)); + Key = key; + this._params = new List(parameters); + Next = next; + } + + public void Emit(TokenTextWriter stream) + { + Contract.Requires(stream != null); + stream.Write("{:"); + stream.Write(Key); + string sep = " "; + foreach (object p in Params) + { + stream.Write(sep); + sep = ", "; + if (p is string) + { + stream.Write("\""); + stream.Write((string) p); + stream.Write("\""); + } + else + { + ((Expr) p).Emit(stream); + } + } + + stream.Write("}"); + } + + public override void Resolve(ResolutionContext rc) + { + //Contract.Requires(rc != null); + + if ((Key == "minimize" || Key == "maximize") && Params.Count != 1) + { + rc.Error(this, "attributes :minimize and :maximize accept only one argument"); + } + + if (Key == "verified_under" && Params.Count != 1) + { + rc.Error(this, "attribute :verified_under accepts only one argument"); + } + + if (Key == CivlAttributes.LAYER) + { + foreach (var o in Params) + { + if (o is LiteralExpr l && l.isBigNum) + { + var n = l.asBigNum; + if (n.IsNegative) + { + rc.Error(this, "layer must be non-negative"); + } + else if (!n.InInt32) + { + rc.Error(this, "layer is too large (max value is Int32.MaxValue)"); + } + } + else + { + rc.Error(this, "layer must be a non-negative integer"); + } + } + } + + foreach (object p in Params) + { + if (p is Expr) + { + var oldCtxtState = rc.StateMode; + if (oldCtxtState == ResolutionContext.State.Single) + { + rc.StateMode = ResolutionContext.State.Two; + } + + ((Expr) p).Resolve(rc); + if (oldCtxtState != rc.StateMode) + { + rc.StateMode = oldCtxtState; + } + } + } + } + + public override void Typecheck(TypecheckingContext tc) + { + //Contract.Requires(tc != null); + foreach (object p in Params) + { + var expr = p as Expr; + if (expr != null) + { + expr.Typecheck(tc); + } + + if ((Key == "minimize" || Key == "maximize") + && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv))) + { + tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv"); + break; + } + + if (Key == "verified_under" && (expr == null || !expr.Type.IsBool)) + { + tc.Error(this, "attribute :verified_under accepts only one argument of type bool"); + break; + } + } + } + + public void AddLast(QKeyValue other) + { + Contract.Requires(other != null); + QKeyValue current = this; + while (current.Next != null) + { + current = current.Next; + } + + current.Next = other; + } + + public static QKeyValue FindAttribute(QKeyValue kv, Func property) + { + for (; kv != null; kv = kv.Next) + { + if (property(kv)) + { + return kv; + } + } + return null; + } + + // Look for {:name string} in list of attributes. + [Pure] + public static string FindStringAttribute(QKeyValue kv, string name) + { + Contract.Requires(name != null); + kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is string); + if (kv != null) + { + Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is string); + return (string) kv.Params[0]; + } + return null; + } + + // Look for {:name expr} in list of attributes. + public static Expr FindExprAttribute(QKeyValue kv, string name) + { + Contract.Requires(name != null); + kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is Expr); + if (kv != null) + { + Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is Expr); + return (Expr) kv.Params[0]; + } + return null; + } + + // Return 'true' if {:name true} or {:name} is an attribute in 'kv' + public static bool FindBoolAttribute(QKeyValue kv, string name) + { + Contract.Requires(name != null); + kv = FindAttribute(kv, qkv => qkv.Key == name && (qkv.Params.Count == 0 || + (qkv.Params.Count == 1 && qkv.Params[0] is LiteralExpr && + ((LiteralExpr) qkv.Params[0]).IsTrue))); + return kv != null; + } + + public static int FindIntAttribute(QKeyValue kv, string name, int defl) + { + Contract.Requires(name != null); + Expr e = FindExprAttribute(kv, name); + LiteralExpr l = e as LiteralExpr; + if (l != null && l.isBigNum) + { + return l.asBigNum.ToIntSafe; + } + + return defl; + } + + public override Absy Clone() + { + List newParams = new List(); + foreach (object o in Params) + { + newParams.Add(o); + } + + return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue) Next.Clone()); + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + return visitor.VisitQKeyValue(this); + } + + public override bool Equals(object obj) + { + var other = obj as QKeyValue; + if (other == null) + { + return false; + } + else + { + return Key == other.Key && object.Equals(Params, other.Params) && + (Next == null + ? other.Next == null + : object.Equals(Next, other.Next)); + } + } + + public override int GetHashCode() + { + throw new NotImplementedException(); + } + } + public class Trigger : Absy { public readonly bool Pos; diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/Block.cs similarity index 88% rename from Source/Core/AST/GotoBoogie/Block.cs rename to Source/Core/AST/Block.cs index 0bc535bdb..c6ac50740 100644 --- a/Source/Core/AST/GotoBoogie/Block.cs +++ b/Source/Core/AST/Block.cs @@ -79,20 +79,20 @@ public int // This field is used during passification to null-out entries in block2Incarnation dictionary early public int succCount; - private HashSet liveVarsBefore; + private HashSet _liveVarsBefore; - public IEnumerable LiveVarsBefore + public IEnumerable liveVarsBefore { get { Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); - if (this.liveVarsBefore == null) + if (this._liveVarsBefore == null) { return null; } else { - return this.liveVarsBefore.AsEnumerable(); + return this._liveVarsBefore.AsEnumerable(); } } set @@ -100,11 +100,11 @@ public IEnumerable LiveVarsBefore Contract.Requires(cce.NonNullElements(value, true)); if (value == null) { - this.liveVarsBefore = null; + this._liveVarsBefore = null; } else { - this.liveVarsBefore = new HashSet(value); + this._liveVarsBefore = new HashSet(value); } } } @@ -114,25 +114,21 @@ void ObjectInvariant() { Contract.Invariant(this.label != null); Contract.Invariant(this.cmds != null); - Contract.Invariant(cce.NonNullElements(this.liveVarsBefore, true)); + Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); } public bool IsLive(Variable v) { Contract.Requires(v != null); - if (LiveVarsBefore == null) + if (liveVarsBefore == null) { return true; } - return LiveVarsBefore.Contains(v); + return liveVarsBefore.Contains(v); } - public static Block ShallowClone(Block block) { - return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); - } - - public Block(IToken tok, TransferCmd cmd) + public Block(IToken tok) : this(tok, "", new List(), new ReturnCmd(tok)) { } @@ -147,7 +143,7 @@ public Block(IToken tok, string /*!*/ label, List /*!*/ cmds, TransferCmd t this.cmds = cmds; this.TransferCmd = transferCmd; this.Predecessors = new List(); - this.liveVarsBefore = null; + this._liveVarsBefore = null; this.TraversingStatus = VisitState.ToVisit; this.iterations = 0; } diff --git a/Source/Core/AST/Commands/CallCmd.cs b/Source/Core/AST/CallCmd.cs similarity index 99% rename from Source/Core/AST/Commands/CallCmd.cs rename to Source/Core/AST/CallCmd.cs index 0f0ed662c..e35541b6d 100644 --- a/Source/Core/AST/Commands/CallCmd.cs +++ b/Source/Core/AST/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)); } @@ -1052,12 +1052,12 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #region stratified inlining support - if (e.Attributes.FindBoolAttribute("si_fcall")) + if (QKeyValue.FindBoolAttribute(e.Attributes, "si_fcall")) { assume.Attributes = Attributes; } - if (e.Attributes.FindBoolAttribute("candidate")) + if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate")) { assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List(), assume.Attributes); assume.Attributes.AddParam(this.callee); @@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion if (callId is not null) { - (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, + assume.CopyIdWithModificationsFrom(tok, e, id => new TrackedCallEnsures(callId, id)); } diff --git a/Source/Core/AST/GotoBoogie/ChangeScope.cs b/Source/Core/AST/ChangeScope.cs similarity index 100% rename from Source/Core/AST/GotoBoogie/ChangeScope.cs rename to Source/Core/AST/ChangeScope.cs diff --git a/Source/Core/AST/GotoBoogie/GotoCmd.cs b/Source/Core/AST/GotoBoogie/GotoCmd.cs deleted file mode 100644 index 9b7aa5340..000000000 --- a/Source/Core/AST/GotoBoogie/GotoCmd.cs +++ /dev/null @@ -1,159 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class GotoCmd : TransferCmd -{ - [Rep] public List LabelNames; - [Rep] public List LabelTargets; - - public QKeyValue Attributes { get; set; } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(LabelNames == null || LabelTargets == null || LabelNames.Count == LabelTargets.Count); - } - - [NotDelayed] - public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(labelSeq != null); - this.LabelNames = labelSeq; - } - - public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq, List /*!*/ blockSeq) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(labelSeq != null); - Contract.Requires(blockSeq != null); - Debug.Assert(labelSeq.Count == blockSeq.Count); - for (int i = 0; i < labelSeq.Count; i++) - { - Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label)); - } - - this.LabelNames = labelSeq; - this.LabelTargets = blockSeq; - } - - public GotoCmd(IToken /*!*/ tok, List /*!*/ blockSeq) - : 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++) - { - labelSeq.Add(cce.NonNull(blockSeq[i]).Label); - } - - this.LabelNames = labelSeq; - this.LabelTargets = blockSeq; - } - - public void RemoveTarget(Block b) { - LabelNames.Remove(b.Label); - LabelTargets.Remove(b); - } - - public void AddTarget(Block b) - { - Contract.Requires(b != null); - Contract.Requires(b.Label != null); - Contract.Requires(this.LabelTargets != null); - Contract.Requires(this.LabelNames != null); - this.LabelTargets.Add(b); - this.LabelNames.Add(b.Label); - } - - public void AddTargets(IEnumerable blocks) - { - Contract.Requires(blocks != null); - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Requires(this.LabelTargets != null); - Contract.Requires(this.LabelNames != null); - foreach (var block in blocks) - { - AddTarget(block); - } - } - - public override void Emit(TokenTextWriter stream, int level) - { - //Contract.Requires(stream != null); - Contract.Assume(this.LabelNames != null); - stream.Write(this, level, "goto "); - if (stream.Options.PrintWithUniqueASTIds) - { - if (LabelTargets == null) - { - string sep = ""; - foreach (string name in LabelNames) - { - stream.Write("{0}{1}^^{2}", sep, "NoDecl", name); - sep = ", "; - } - } - else - { - string sep = ""; - foreach (Block /*!*/ b in LabelTargets) - { - Contract.Assert(b != null); - stream.Write("{0}h{1}^^{2}", sep, b.GetHashCode(), b.Label); - sep = ", "; - } - } - } - else - { - LabelNames.Emit(stream); - } - - stream.WriteLine(";"); - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - Contract.Ensures(LabelTargets != null); - if (LabelTargets != null) - { - // already resolved - return; - } - - Contract.Assume(this.LabelNames != null); - LabelTargets = new List(); - foreach (string /*!*/ lbl in LabelNames) - { - Contract.Assert(lbl != null); - Block b = rc.LookUpBlock(lbl); - if (b == null) - { - rc.Error(this, "goto to unknown block: {0}", lbl); - } - else - { - LabelTargets.Add(b); - } - } - - Debug.Assert(rc.ErrorCount > 0 || LabelTargets.Count == LabelNames.Count); - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitGotoCmd(this); - } -} \ No newline at end of file diff --git a/Source/Core/AST/GotoBoogie/ReturnCmd.cs b/Source/Core/AST/GotoBoogie/ReturnCmd.cs deleted file mode 100644 index 9f60df66b..000000000 --- a/Source/Core/AST/GotoBoogie/ReturnCmd.cs +++ /dev/null @@ -1,33 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class ReturnCmd : TransferCmd -{ - public QKeyValue Attributes { get; set; } - - public ReturnCmd(IToken /*!*/ tok) - : base(tok) - { - Contract.Requires(tok != null); - } - - public override void Emit(TokenTextWriter stream, int level) - { - //Contract.Requires(stream != null); - stream.WriteLine(this, level, "return;"); - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - // nothing to resolve - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitReturnCmd(this); - } -} \ No newline at end of file diff --git a/Source/Core/AST/GotoBoogie/TransferCmd.cs b/Source/Core/AST/GotoBoogie/TransferCmd.cs deleted file mode 100644 index 933ccdc91..000000000 --- a/Source/Core/AST/GotoBoogie/TransferCmd.cs +++ /dev/null @@ -1,33 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -[ContractClass(typeof(TransferCmdContracts))] -public abstract class TransferCmd : Absy -{ - public ProofObligationDescription Description { get; set; } = new PostconditionDescription(); - - internal TransferCmd(IToken /*!*/ tok) - : base(tok) - { - Contract.Requires(tok != null); - } - - public abstract void Emit(TokenTextWriter /*!*/ stream, int level); - - public override void Typecheck(TypecheckingContext tc) - { - //Contract.Requires(tc != null); - // nothing to typecheck - } - - public override string ToString() - { - Contract.Ensures(Contract.Result() != null); - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using TokenTextWriter stream = new TokenTextWriter("", buffer, false, false, PrintOptions.Default); - this.Emit(stream, 0); - - return buffer.ToString(); - } -} \ No newline at end of file diff --git a/Source/Core/AST/Commands/HideRevealCmd.cs b/Source/Core/AST/HideRevealCmd.cs similarity index 100% rename from Source/Core/AST/Commands/HideRevealCmd.cs rename to Source/Core/AST/HideRevealCmd.cs diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index b20edeaad..a24485f89 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -39,35 +39,35 @@ public List FindLayers() } return layers.Distinct().OrderBy(l => l).ToList(); } -} -public static class CarriesAttributesExtensions { - // Look for {:name string} in list of attributes. - public static string FindStringAttribute(this ICarriesAttributes destination, string name) + public string FindStringAttribute(string name) { - return QKeyValue.FindStringAttribute(destination.Attributes, name); + return QKeyValue.FindStringAttribute(Attributes, name); } - public static void AddStringAttribute(this ICarriesAttributes destination, IToken tok, string name, string parameter) + public void AddStringAttribute(IToken tok, string name, string parameter) { - destination.Attributes = new QKeyValue(tok, name, new List() {parameter}, destination.Attributes); + Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); } - - public static void CopyIdFrom(this ICarriesAttributes destination, IToken tok, ICarriesAttributes src) + +} + +public static class CarriesAttributesExtensions +{ + public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src) { var id = src.FindStringAttribute("id"); if (id is not null) { - destination.AddStringAttribute(tok, "id", id); + dest.AddStringAttribute(tok, "id", id); } } - public static void CopyIdWithModificationsFrom(this ICarriesAttributes destination, IToken tok, - ICarriesAttributes src, Func modifier) + public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { - destination.AddStringAttribute(tok, "id", modifier(id).SolverLabel); + dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel); } } } \ No newline at end of file diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs index d1b497dfb..6d6d2415c 100644 --- a/Source/Core/AST/Implementation.cs +++ b/Source/Core/AST/Implementation.cs @@ -151,7 +151,7 @@ public bool IsSkipVerification(CoreOptions options) } if (options.StratifiedInlining > 0) { - return !Attributes.FindBoolAttribute("entrypoint"); + return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint"); } return false; @@ -462,19 +462,19 @@ void BlocksWriters(TokenTextWriter stream) { } public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable blocks, - bool showLocals, string nameSuffix = "") { + bool showLocals) { EmitImplementation(stream, level, writer => { foreach (var block in blocks) { block.Emit(writer, level + 1); } - }, showLocals, nameSuffix); + }, showLocals); } - private void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals, string nameSuffix = "") + public void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals) { stream.Write(this, level, "implementation "); EmitAttributes(stream); - stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(Name) + nameSuffix); + stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); EmitSignature(stream, false); stream.WriteLine(); diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 810b73232..45011b574 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -63,7 +63,7 @@ public override void Resolve(ResolutionContext rc) ResolveTypes(rc); var prunedTopLevelDeclarations = new List(); - foreach (var d in TopLevelDeclarations.Where(d => !d.Attributes.FindBoolAttribute("ignore"))) + foreach (var d in TopLevelDeclarations.Where(d => !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))) { // resolve all the declarations that have not been resolved yet if (!(d is TypeCtorDecl || d is TypeSynonymDecl)) @@ -98,7 +98,7 @@ private void ResolveTypes(ResolutionContext rc) // first resolve type constructors foreach (var d in TopLevelDeclarations.OfType()) { - if (!d.Attributes.FindBoolAttribute("ignore")) + if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) { d.Resolve(rc); } @@ -110,7 +110,7 @@ private void ResolveTypes(ResolutionContext rc) foreach (var d in TopLevelDeclarations.OfType()) { Contract.Assert(d != null); - if (!d.Attributes.FindBoolAttribute("ignore")) + if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) { synonymDecls.Add(d); } @@ -498,7 +498,7 @@ public static Graph BuildCallGraph(CoreOptions options, Program return callGraph; } - public static Graph GraphFromBlocksSubset(IReadOnlyList blocks, IReadOnlySet subset = null, bool forward = true) + public static Graph GraphFromBlocks(List blocks, bool forward = true) { var result = new Graph(); if (!blocks.Any()) @@ -506,9 +506,6 @@ public static Graph GraphFromBlocksSubset(IReadOnlyList blocks, IR return result; } void AddEdge(Block a, Block b) { - if (subset != null && (!subset.Contains(a) || !subset.Contains(b))) { - return; - } Contract.Assert(a != null && b != null); if (forward) { result.AddEdge(a, b); @@ -517,7 +514,7 @@ void AddEdge(Block a, Block b) { } } - result.AddSource(blocks[0]); + result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph foreach (var block in blocks) { if (block.TransferCmd is GotoCmd gtc) @@ -528,10 +525,6 @@ void AddEdge(Block a, Block b) { } return result; } - - public static Graph GraphFromBlocks(IReadOnlyList blocks, bool forward = true) { - return GraphFromBlocksSubset(blocks, null, forward); - } public static Graph /*!*/ GraphFromImpl(Implementation impl, bool forward = true) { diff --git a/Source/Core/AST/QKeyValue.cs b/Source/Core/AST/QKeyValue.cs deleted file mode 100644 index 5693a4e3e..000000000 --- a/Source/Core/AST/QKeyValue.cs +++ /dev/null @@ -1,269 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class QKeyValue : Absy -{ - public readonly string /*!*/ - Key; - - private readonly List /*!*/ - _params; // each element is either a string or an Expr - - public void AddParam(object p) - { - Contract.Requires(p != null); - this._params.Add(p); - } - - public void AddParams(IEnumerable ps) - { - Contract.Requires(cce.NonNullElements(ps)); - this._params.AddRange(ps); - } - - public void ClearParams() - { - this._params.Clear(); - } - - public IList Params - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Contract.Ensures(Contract.Result>().IsReadOnly); - return this._params.AsReadOnly(); - } - } - - public QKeyValue Next; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Key != null); - Contract.Invariant(cce.NonNullElements(this._params)); - } - - public QKeyValue(IToken tok, string key, IList /*!*/ parameters, QKeyValue next) - : base(tok) - { - Contract.Requires(key != null); - Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(parameters)); - Key = key; - this._params = new List(parameters); - Next = next; - } - - public void Emit(TokenTextWriter stream) - { - Contract.Requires(stream != null); - stream.Write("{:"); - stream.Write(Key); - string sep = " "; - foreach (object p in Params) - { - stream.Write(sep); - sep = ", "; - if (p is string) - { - stream.Write("\""); - stream.Write((string) p); - stream.Write("\""); - } - else - { - ((Expr) p).Emit(stream); - } - } - - stream.Write("}"); - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - - if ((Key == "minimize" || Key == "maximize") && Params.Count != 1) - { - rc.Error(this, "attributes :minimize and :maximize accept only one argument"); - } - - if (Key == "verified_under" && Params.Count != 1) - { - rc.Error(this, "attribute :verified_under accepts only one argument"); - } - - if (Key == CivlAttributes.LAYER) - { - foreach (var o in Params) - { - if (o is LiteralExpr l && l.isBigNum) - { - var n = l.asBigNum; - if (n.IsNegative) - { - rc.Error(this, "layer must be non-negative"); - } - else if (!n.InInt32) - { - rc.Error(this, "layer is too large (max value is Int32.MaxValue)"); - } - } - else - { - rc.Error(this, "layer must be a non-negative integer"); - } - } - } - - foreach (object p in Params) - { - if (p is Expr) - { - var oldCtxtState = rc.StateMode; - if (oldCtxtState == ResolutionContext.State.Single) - { - rc.StateMode = ResolutionContext.State.Two; - } - - ((Expr) p).Resolve(rc); - if (oldCtxtState != rc.StateMode) - { - rc.StateMode = oldCtxtState; - } - } - } - } - - public override void Typecheck(TypecheckingContext tc) - { - //Contract.Requires(tc != null); - foreach (object p in Params) - { - var expr = p as Expr; - if (expr != null) - { - expr.Typecheck(tc); - } - - if ((Key == "minimize" || Key == "maximize") - && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv))) - { - tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv"); - break; - } - - if (Key == "verified_under" && (expr == null || !expr.Type.IsBool)) - { - tc.Error(this, "attribute :verified_under accepts only one argument of type bool"); - break; - } - } - } - - public void AddLast(QKeyValue other) - { - Contract.Requires(other != null); - QKeyValue current = this; - while (current.Next != null) - { - current = current.Next; - } - - current.Next = other; - } - - public static QKeyValue FindAttribute(QKeyValue kv, Func property) - { - for (; kv != null; kv = kv.Next) - { - if (property(kv)) - { - return kv; - } - } - return null; - } - - // Look for {:name string} in list of attributes. - [Pure] - public static string FindStringAttribute(QKeyValue kv, string name) - { - Contract.Requires(name != null); - kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is string); - if (kv != null) - { - Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is string); - return (string) kv.Params[0]; - } - return null; - } - - // Look for {:name expr} in list of attributes. - public static Expr FindExprAttribute(QKeyValue kv, string name) - { - Contract.Requires(name != null); - kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is Expr); - if (kv != null) - { - Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is Expr); - return (Expr) kv.Params[0]; - } - return null; - } - - public static int FindIntAttribute(QKeyValue kv, string name, int defl) - { - Contract.Requires(name != null); - Expr e = FindExprAttribute(kv, name); - LiteralExpr l = e as LiteralExpr; - if (l != null && l.isBigNum) - { - return l.asBigNum.ToIntSafe; - } - - return defl; - } - - public override Absy Clone() - { - List newParams = new List(); - foreach (object o in Params) - { - newParams.Add(o); - } - - return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue) Next.Clone()); - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - return visitor.VisitQKeyValue(this); - } - - public override bool Equals(object obj) - { - var other = obj as QKeyValue; - if (other == null) - { - return false; - } - else - { - return Key == other.Key && object.Equals(Params, other.Params) && - (Next == null - ? other.Next == null - : object.Equals(Next, other.Next)); - } - } - - public override int GetHashCode() - { - throw new NotImplementedException(); - } -} \ No newline at end of file diff --git a/Source/Core/AST/QKeyValueExtensions.cs b/Source/Core/AST/QKeyValueExtensions.cs deleted file mode 100644 index 4949875e3..000000000 --- a/Source/Core/AST/QKeyValueExtensions.cs +++ /dev/null @@ -1,16 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public static class QKeyValueExtensions { - - // Return 'true' if {:name true} or {:name} is an attribute in 'kv' - public static bool FindBoolAttribute(this QKeyValue kv, string name) - { - Contract.Requires(name != null); - kv = QKeyValue.FindAttribute(kv, qkv => qkv.Key == name && (qkv.Params.Count == 0 || - (qkv.Params.Count == 1 && qkv.Params[0] is LiteralExpr && - ((LiteralExpr) qkv.Params[0]).IsTrue))); - return kv != null; - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/BigBlock.cs b/Source/Core/AST/StructuredBoogie/BigBlock.cs deleted file mode 100644 index 0fbe65e52..000000000 --- a/Source/Core/AST/StructuredBoogie/BigBlock.cs +++ /dev/null @@ -1,124 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class BigBlock -{ - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(tok != null); - Contract.Invariant(Anonymous || this.labelName != null); - Contract.Invariant(this._ec == null || this._tc == null); - Contract.Invariant(this._simpleCmds != null); - } - - public readonly IToken /*!*/ - tok; - - public readonly bool Anonymous; - - private string labelName; - - public string LabelName - { - get - { - Contract.Ensures(Anonymous || Contract.Result() != null); - return this.labelName; - } - set - { - Contract.Requires(Anonymous || value != null); - this.labelName = value; - } - } - - [Rep] private List /*!*/ _simpleCmds; - - /// - /// These come before the structured command - /// - public List /*!*/ simpleCmds - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this._simpleCmds; - } - set - { - Contract.Requires(value != null); - this._simpleCmds = value; - } - } - - private StructuredCmd _ec; - - public StructuredCmd ec - { - get { return this._ec; } - set - { - Contract.Requires(value == null || this.tc == null); - this._ec = value; - } - } - - private TransferCmd _tc; - - public TransferCmd tc - { - get { return this._tc; } - set - { - Contract.Requires(value == null || this.ec == null); - this._tc = value; - } - } - - public BigBlock - successorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized) - - public BigBlock(IToken tok, string labelName, [Captured] List simpleCmds, StructuredCmd ec, TransferCmd tc) - { - Contract.Requires(simpleCmds != null); - Contract.Requires(tok != null); - Contract.Requires(ec == null || tc == null); - this.tok = tok; - this.Anonymous = labelName == null; - this.labelName = labelName; - this._simpleCmds = simpleCmds; - this._ec = ec; - this._tc = tc; - } - - public void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - if (!Anonymous) - { - stream.WriteLine(level, "{0}:", - stream.Options.PrintWithUniqueASTIds - ? String.Format("h{0}^^{1}", this.GetHashCode(), this.LabelName) - : this.LabelName); - } - - foreach (Cmd /*!*/ c in this.simpleCmds) - { - Contract.Assert(c != null); - c.Emit(stream, level + 1); - } - - if (this.ec != null) - { - this.ec.Emit(stream, level + 1); - } - else if (this.tc != null) - { - this.tc.Emit(stream, level + 1); - } - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs deleted file mode 100644 index b53bc3606..000000000 --- a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs +++ /dev/null @@ -1,591 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Linq; - -namespace Microsoft.Boogie; - -class BigBlocksResolutionContext -{ - StmtList /*!*/ - stmtList; - - [Peer] List blocks; - - string /*!*/ - prefix = "anon"; - - int anon = 0; - - int FreshAnon() - { - return anon++; - } - - private readonly HashSet allLabels = new(); - - private readonly Errors /*!*/ errorHandler; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(stmtList != null); - Contract.Invariant(cce.NonNullElements(blocks, true)); - Contract.Invariant(prefix != null); - Contract.Invariant(cce.NonNullElements(allLabels, true)); - Contract.Invariant(errorHandler != null); - } - - private void ComputeAllLabels(StmtList stmts) - { - if (stmts == null) - { - return; - } - - foreach (BigBlock bb in stmts.BigBlocks) - { - if (bb.LabelName != null) - { - allLabels.Add(bb.LabelName); - } - - ComputeAllLabels(bb.ec); - } - } - - private void ComputeAllLabels(StructuredCmd cmd) - { - if (cmd == null) - { - return; - } - - if (cmd is IfCmd) - { - IfCmd ifCmd = (IfCmd) cmd; - ComputeAllLabels(ifCmd.thn); - ComputeAllLabels(ifCmd.elseIf); - ComputeAllLabels(ifCmd.elseBlock); - } - else if (cmd is WhileCmd) - { - WhileCmd whileCmd = (WhileCmd) cmd; - ComputeAllLabels(whileCmd.Body); - } - } - - public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) - { - Contract.Requires(errorHandler != null); - Contract.Requires(stmtList != null); - this.stmtList = stmtList; - // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. - // This transformation creates a suitable jump target for break statements inside the nested while loop. - InjectEmptyBigBlockInsideWhileLoopBody(stmtList); - this.errorHandler = errorHandler; - ComputeAllLabels(stmtList); - } - - public List /*!*/ Blocks - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (blocks == null) - { - blocks = new List(); - - int startErrorCount = this.errorHandler.count; - // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. - // Also, determine a good value for "prefix". - CheckLegalLabels(stmtList, null, null); - - // fill in names of anonymous blocks - NameAnonymousBlocks(stmtList); - - // determine successor blocks - RecordSuccessors(stmtList, null); - - if (this.errorHandler.count == startErrorCount) - { - // generate blocks from the big blocks - CreateBlocks(stmtList, null); - } - } - - return blocks; - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) - { - foreach (var bb in stmtList.BigBlocks) - { - InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) - { - if (structuredCmd is WhileCmd whileCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); - if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) - { - var newBigBlocks = new List(whileCmd.Body.BigBlocks); - newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); - whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); - } - } - else if (structuredCmd is IfCmd ifCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); - if (ifCmd.elseBlock != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); - } - - if (ifCmd.elseIf != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); - } - } - } - - void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) - { - Contract.Requires(stmtList != null); - Contract.Requires((parentContext == null) == (parentBigBlock == null)); - Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet - //modifies stmtList.*; - Contract.Ensures(stmtList.ParentContext == parentContext); - stmtList.ParentContext = parentContext; - stmtList.ParentBigBlock = parentBigBlock; - - // record the labels declared in this StmtList - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName != null) - { - string n = b.LabelName; - if (n.StartsWith(prefix)) - { - if (prefix.Length < n.Length && n[prefix.Length] == '0') - { - prefix += "1"; - } - else - { - prefix += "0"; - } - } - - stmtList.AddLabel(b.LabelName); - } - } - - // check that labels in this and nested StmtList's are legal - foreach (BigBlock b in stmtList.BigBlocks) - { - // goto's must reference blocks in enclosing blocks - if (b.tc is GotoCmd) - { - GotoCmd g = (GotoCmd) b.tc; - foreach (string /*!*/ lbl in cce.NonNull(g.LabelNames)) - { - Contract.Assert(lbl != null); - /* - bool found = false; - for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) { - if (sl.Labels.Contains(lbl)) { - found = true; - break; - } - } - if (!found) { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); - } - */ - if (!allLabels.Contains(lbl)) - { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); - } - } - } - - // break labels must refer to an enclosing while statement - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet - bool found = false; - for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) - { - cce.LoopInvariant(sl != null); - BigBlock bb = sl.ParentBigBlock; - - if (bcmd.Label == null) - { - // a label-less break statement breaks out of the innermost enclosing while statement - if (bb.ec is WhileCmd) - { - bcmd.BreakEnclosure = bb; - found = true; - break; - } - } - else if (bcmd.Label == bb.LabelName) - { - // a break statement with a label can break out of both if statements and while statements - if (bb.simpleCmds.Count == 0) - { - // this is a good target: the label refers to the if/while statement - bcmd.BreakEnclosure = bb; - } - else - { - // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - - found = true; // don't look any further, since we've found a matching label - break; - } - } - - if (!found) - { - if (bcmd.Label == null) - { - this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); - } - else - { - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - } - } - - // recurse - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - CheckLegalLabels(wcmd.Body, stmtList, b); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - CheckLegalLabels(ifcmd.thn, stmtList, b); - if (ifcmd.elseBlock != null) - { - CheckLegalLabels(ifcmd.elseBlock, stmtList, b); - } - } - } - } - } - - void NameAnonymousBlocks(StmtList stmtList) - { - Contract.Requires(stmtList != null); - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName == null) - { - b.LabelName = prefix + FreshAnon(); - } - - if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - NameAnonymousBlocks(wcmd.Body); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - NameAnonymousBlocks(ifcmd.thn); - if (ifcmd.elseBlock != null) - { - NameAnonymousBlocks(ifcmd.elseBlock); - } - } - } - } - } - - void RecordSuccessors(StmtList stmtList, BigBlock successor) - { - Contract.Requires(stmtList != null); - for (int i = stmtList.BigBlocks.Count; 0 <= --i;) - { - BigBlock big = stmtList.BigBlocks[i]; - big.successorBigBlock = successor; - - if (big.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) big.ec; - RecordSuccessors(wcmd.Body, big); - } - else - { - for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - RecordSuccessors(ifcmd.thn, successor); - if (ifcmd.elseBlock != null) - { - RecordSuccessors(ifcmd.elseBlock, successor); - } - } - } - - successor = big; - } - } - - // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; - // otherwise, it is null. - void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) - { - Contract.Requires(stmtList != null); - Contract.Requires(blocks != null); - List cmdPrefixToApply = stmtList.PrefixCommands; - - int n = stmtList.BigBlocks.Count; - foreach (BigBlock b in stmtList.BigBlocks) - { - n--; - Contract.Assert(b.LabelName != null); - List theSimpleCmds; - if (cmdPrefixToApply == null) - { - theSimpleCmds = b.simpleCmds; - } - else - { - theSimpleCmds = new List(); - theSimpleCmds.AddRange(cmdPrefixToApply); - theSimpleCmds.AddRange(b.simpleCmds); - cmdPrefixToApply = null; // now, we've used 'em up - } - - if (b.tc != null) - { - // this BigBlock has the very same components as a Block - Contract.Assert(b.ec == null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); - blocks.Add(block); - } - else if (b.ec == null) - { - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(stmtList.EndCurly, b); - } - - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); - blocks.Add(block); - } - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure != null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); - blocks.Add(block); - } - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - 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 ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.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); - ssDone.Add(ac); - } - - // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); - - // ... goto LoopHead; - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, - new GotoCmd(wcmd.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) - { - ssHead.Add(yield); - } - foreach (PredicateCmd inv in wcmd.Invariants) - { - ssHead.Add(inv); - } - - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.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})); - blocks.Add(block); - } - - // recurse to create the blocks for the loop body - CreateBlocks(wcmd.Body, loopHeadLabel); - - // LoopDone: assume !guard; goto loopSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(wcmd.tok, b); - } - - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); - blocks.Add(block); - } - else - { - IfCmd ifcmd = (IfCmd) b.ec; - string predLabel = b.LabelName; - List predCmds = theSimpleCmds; - - for (; ifcmd != null; ifcmd = ifcmd.elseIf) - { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; - Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; - Contract.Assert(elseLabel != null); - - List ssThen = new List(); - List 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); - ssThen.Add(ac); - - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.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 elseGuardTakenCareOf = false; - if (ifcmd.elseBlock != null) - { - elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); - } - - // ... goto Then, Else; - var jumpBlock = new Block(b.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); - 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})); - blocks.Add(thenJumpBlock); - } - - // recurse to create the blocks for the then branch - CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); - - if (ifcmd.elseBlock != 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})); - blocks.Add(elseJumpBlock); - } - - // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); - } - else if (ifcmd.elseIf != null) - { - // this is an "else if" - predLabel = elseLabel; - predCmds = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - predCmds.Add(ac); - } - } - else - { - // no else alternative is specified, so else branch is just "skip" - // Else: assume !guard; goto ifSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(ifcmd.tok, b); - } - - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); - blocks.Add(block); - } - } - } - } - } - - TransferCmd GotoSuccessor(IToken tok, BigBlock b) - { - Contract.Requires(b != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - if (b.successorBigBlock != null) - { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); - } - else - { - return new ReturnCmd(tok); - } - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/BreakCmd.cs b/Source/Core/AST/StructuredBoogie/BreakCmd.cs deleted file mode 100644 index 3ea89b616..000000000 --- a/Source/Core/AST/StructuredBoogie/BreakCmd.cs +++ /dev/null @@ -1,28 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class BreakCmd : StructuredCmd -{ - public string Label; - public BigBlock BreakEnclosure; - - public BreakCmd(IToken tok, string label) - : base(tok) - { - Contract.Requires(tok != null); - this.Label = label; - } - - public override void Emit(TokenTextWriter stream, int level) - { - if (Label == null) - { - stream.WriteLine(level, "break;"); - } - else - { - stream.WriteLine(level, "break {0};", Label); - } - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/IfCmd.cs b/Source/Core/AST/StructuredBoogie/IfCmd.cs deleted file mode 100644 index 5f29f407d..000000000 --- a/Source/Core/AST/StructuredBoogie/IfCmd.cs +++ /dev/null @@ -1,108 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class IfCmd : StructuredCmd -{ - public Expr Guard; - - private StmtList /*!*/ - _thn; - - public StmtList /*!*/ thn - { - get - { - Contract.Ensures(Contract.Result() != null); - return this._thn; - } - set - { - Contract.Requires(value != null); - this._thn = value; - } - } - - private IfCmd _elseIf; - - public IfCmd elseIf - { - get { return this._elseIf; } - set - { - Contract.Requires(value == null || this.elseBlock == null); - this._elseIf = value; - } - } - - private StmtList _elseBlock; - - public StmtList elseBlock - { - get { return this._elseBlock; } - set - { - Contract.Requires(value == null || this.elseIf == null); - this._elseBlock = value; - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this._thn != null); - Contract.Invariant(this._elseIf == null || this._elseBlock == null); - } - - public IfCmd(IToken /*!*/ tok, Expr guard, StmtList /*!*/ thn, IfCmd elseIf, StmtList elseBlock) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(thn != null); - Contract.Requires(elseIf == null || elseBlock == null); - this.Guard = guard; - this._thn = thn; - this._elseIf = elseIf; - this._elseBlock = elseBlock; - } - - public override void Emit(TokenTextWriter stream, int level) - { - stream.Write(level, "if ("); - IfCmd /*!*/ - ifcmd = this; - while (true) - { - if (ifcmd.Guard == null) - { - stream.Write("*"); - } - else - { - ifcmd.Guard.Emit(stream); - } - - stream.WriteLine(")"); - - stream.WriteLine(level, "{"); - ifcmd.thn.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - - if (ifcmd.elseIf != null) - { - stream.Write(level, "else if ("); - ifcmd = ifcmd.elseIf; - continue; - } - else if (ifcmd.elseBlock != null) - { - stream.WriteLine(level, "else"); - stream.WriteLine(level, "{"); - ifcmd.elseBlock.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - } - - break; - } - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/StmtList.cs b/Source/Core/AST/StructuredBoogie/StmtList.cs deleted file mode 100644 index 51407e1c7..000000000 --- a/Source/Core/AST/StructuredBoogie/StmtList.cs +++ /dev/null @@ -1,134 +0,0 @@ -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Linq; - -namespace Microsoft.Boogie; - -public class StmtList -{ - [Rep] private readonly List /*!*/ bigBlocks; - - public IList /*!*/ BigBlocks - { - get - { - Contract.Ensures(Contract.Result>() != null); - Contract.Ensures(Contract.Result>().IsReadOnly); - return this.bigBlocks.AsReadOnly(); - } - } - - public List PrefixCommands; - - public readonly IToken /*!*/ - EndCurly; - - public StmtList ParentContext; - public BigBlock ParentBigBlock; - - private readonly HashSet /*!*/ - labels = new HashSet(); - - public void AddLabel(string label) - { - labels.Add(label); - } - - public IEnumerable /*!*/ Labels - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result /*!*/>())); - return this.labels.AsEnumerable(); - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(EndCurly != null); - Contract.Invariant(cce.NonNullElements(this.bigBlocks)); - Contract.Invariant(cce.NonNullElements(this.labels)); - } - - public StmtList(IList /*!*/ bigblocks, IToken endCurly) - { - Contract.Requires(endCurly != null); - Contract.Requires(cce.NonNullElements(bigblocks)); - Contract.Requires(bigblocks.Count > 0); - this.bigBlocks = new List(bigblocks); - this.EndCurly = endCurly; - } - - // prints the list of statements, not the surrounding curly braces - public void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - bool needSeperator = false; - foreach (BigBlock b in BigBlocks) - { - Contract.Assert(b != null); - Contract.Assume(cce.IsPeerConsistent(b)); - if (needSeperator) - { - stream.WriteLine(); - } - - b.Emit(stream, level); - needSeperator = true; - } - } - - /// - /// Tries to insert the commands "prefixCmds" at the beginning of the first block - /// of the StmtList, and returns "true" iff it succeeded. - /// In the event of success, the "suggestedLabel" returns as the name of the - /// block inside StmtList where "prefixCmds" were inserted. This name may be the - /// same as the one passed in, in case this StmtList has no preference as to what - /// to call its first block. In the event of failure, "suggestedLabel" is returned - /// as its input value. - /// Note, to be conservative (that is, ignoring the possible optimization that this - /// method enables), this method can do nothing and return false. - /// - public bool PrefixFirstBlock([Captured] List prefixCmds, ref string suggestedLabel) - { - Contract.Requires(suggestedLabel != null); - Contract.Requires(prefixCmds != null); - Contract.Ensures(Contract.Result() || - cce.Owner.None(prefixCmds)); // "prefixCmds" is captured only on success - Contract.Assume(PrefixCommands == null); // prefix has not been used - - BigBlock bb0 = BigBlocks[0]; - if (prefixCmds.Count == 0) - { - // This is always a success, since there is nothing to insert. Now, decide - // which name to use for the first block. - if (bb0.Anonymous) - { - bb0.LabelName = suggestedLabel; - } - else - { - Contract.Assert(bb0.LabelName != null); - suggestedLabel = bb0.LabelName; - } - - return true; - } - else - { - // There really is something to insert. We can do this inline only if the first - // block is anonymous (which implies there is no branch to it from within the block). - if (bb0.Anonymous) - { - PrefixCommands = prefixCmds; - bb0.LabelName = suggestedLabel; - return true; - } - else - { - return false; - } - } - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs b/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs deleted file mode 100644 index dd7b67666..000000000 --- a/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs +++ /dev/null @@ -1,98 +0,0 @@ -using System.Collections.Generic; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -/// -/// The AST for Boogie structured commands was designed to support backward compatibility with -/// the Boogie unstructured commands. This has made the structured commands hard to construct. -/// The StmtListBuilder class makes it easier to build structured commands. -/// -public class StmtListBuilder -{ - readonly List /*!*/ bigBlocks = new(); - - string label; - List simpleCmds; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(bigBlocks)); - } - - void Dump(StructuredCmd scmd, TransferCmd tcmd) - { - Contract.Requires(scmd == null || tcmd == null); - Contract.Ensures(label == null && simpleCmds == null); - if (label == null && simpleCmds == null && scmd == null && tcmd == null) - { - // nothing to do - } - else - { - if (simpleCmds == null) - { - simpleCmds = new List(); - } - - bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd)); - label = null; - simpleCmds = null; - } - } - - /// - /// Collects the StmtList built so far and returns it. The StmtListBuilder should no longer - /// be used once this method has been invoked. - /// - public StmtList Collect(IToken endCurlyBrace) - { - Contract.Requires(endCurlyBrace != null); - Contract.Ensures(Contract.Result() != null); - Dump(null, null); - if (bigBlocks.Count == 0) - { - simpleCmds = new List(); // the StmtList constructor doesn't like an empty list of BigBlock's - Dump(null, null); - } - - return new StmtList(bigBlocks, endCurlyBrace); - } - - public void Add(Cmd cmd) - { - Contract.Requires(cmd != null); - if (simpleCmds == null) - { - simpleCmds = new List(); - } - - simpleCmds.Add(cmd); - } - - public void Add(StructuredCmd scmd) - { - Contract.Requires(scmd != null); - Dump(scmd, null); - } - - public void Add(TransferCmd tcmd) - { - Contract.Requires(tcmd != null); - Dump(null, tcmd); - } - - public void AddLabelCmd(string label) - { - Contract.Requires(label != null); - Dump(null, null); - this.label = label; - } - - public void AddLocalVariable(string name) - { - Contract.Requires(name != null); - // TODO - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/StructuredCmd.cs b/Source/Core/AST/StructuredBoogie/StructuredCmd.cs deleted file mode 100644 index f95ef14db..000000000 --- a/Source/Core/AST/StructuredBoogie/StructuredCmd.cs +++ /dev/null @@ -1,38 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -[ContractClass(typeof(StructuredCmdContracts))] -public abstract class StructuredCmd -{ - private IToken /*!*/ - _tok; - - public IToken /*!*/ tok - { - get - { - Contract.Ensures(Contract.Result() != null); - return this._tok; - } - set - { - Contract.Requires(value != null); - this._tok = value; - } - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(this._tok != null); - } - - public StructuredCmd(IToken tok) - { - Contract.Requires(tok != null); - this._tok = tok; - } - - public abstract void Emit(TokenTextWriter /*!*/ stream, int level); -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs b/Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs deleted file mode 100644 index b363253d5..000000000 --- a/Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs +++ /dev/null @@ -1,18 +0,0 @@ -using System; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -[ContractClassFor(typeof(StructuredCmd))] -public abstract class StructuredCmdContracts : StructuredCmd -{ - public override void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - throw new NotImplementedException(); - } - - public StructuredCmdContracts() : base(null) - { - } -} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/WhileCmd.cs b/Source/Core/AST/StructuredBoogie/WhileCmd.cs deleted file mode 100644 index 135bd43ae..000000000 --- a/Source/Core/AST/StructuredBoogie/WhileCmd.cs +++ /dev/null @@ -1,74 +0,0 @@ -using System.Collections.Generic; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie; - -public class WhileCmd : StructuredCmd -{ - [Peer] public Expr Guard; - - public List Invariants; - - public List Yields; - - public StmtList Body; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(Body != null); - Contract.Invariant(cce.NonNullElements(Invariants)); - } - - public WhileCmd(IToken tok, [Captured] Expr guard, List invariants, List yields, StmtList body) - : base(tok) - { - Contract.Requires(cce.NonNullElements(invariants)); - Contract.Requires(body != null); - Contract.Requires(tok != null); - this.Guard = guard; - this.Invariants = invariants; - this.Yields = yields; - this.Body = body; - } - - public override void Emit(TokenTextWriter stream, int level) - { - stream.Write(level, "while ("); - if (Guard == null) - { - stream.Write("*"); - } - else - { - Guard.Emit(stream); - } - - stream.WriteLine(")"); - - foreach (var yield in Yields) - { - stream.Write(level + 1, "invariant"); - yield.Emit(stream, level + 1); - } - foreach (var inv in Invariants) - { - if (inv is AssumeCmd) - { - stream.Write(level + 1, "free invariant "); - } - else - { - stream.Write(level + 1, "invariant "); - } - - Cmd.EmitAttributes(stream, inv.Attributes); - inv.Expr.Emit(stream); - stream.WriteLine(";"); - } - - stream.WriteLine(level, "{"); - Body.Emit(stream, level + 1); - stream.WriteLine(level, "}"); - } -} \ No newline at end of file diff --git a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs index 8b5e95ac5..bcdbbf517 100644 --- a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs +++ b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs @@ -20,7 +20,7 @@ public static void ClearLiveVariables(Implementation impl) foreach (Block /*!*/ block in impl.Blocks) { Contract.Assert(block != null); - block.LiveVarsBefore = null; + block.liveVarsBefore = null; } } @@ -59,8 +59,8 @@ public void ComputeLiveVariables(Implementation impl) foreach (Block /*!*/ succ in gotoCmd.LabelTargets) { Contract.Assert(succ != null); - Contract.Assert(succ.LiveVarsBefore != null); - liveVarsAfter.UnionWith(succ.LiveVarsBefore); + Contract.Assert(succ.liveVarsBefore != null); + liveVarsAfter.UnionWith(succ.liveVarsBefore); } } } @@ -84,7 +84,7 @@ public void ComputeLiveVariables(Implementation impl) Propagate(cmds[i], liveVarsAfter); } - block.LiveVarsBefore = liveVarsAfter; + block.liveVarsBefore = liveVarsAfter; } } @@ -141,7 +141,7 @@ public void Propagate(Cmd cmd, HashSet /*!*/ liveSet) foreach (IdentifierExpr /*!*/ expr in havocCmd.Vars) { Contract.Assert(expr != null); - if (expr.Decl != null && !(expr.Decl.Attributes.FindBoolAttribute("assumption") && + if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { liveSet.Remove(expr.Decl); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index e020af43f..b850527c2 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -529,11 +529,11 @@ Function<.out List/*!*/ ds.> } if (definition != null) { // generate either an axiom or a function body - if (kv.FindBoolAttribute("inline")) { - if (kv.FindBoolAttribute("define")) + if (QKeyValue.FindBoolAttribute(kv, "inline")) { + if (QKeyValue.FindBoolAttribute(kv, "define")) SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; - } else if (kv.FindBoolAttribute("define")) { + } else if (QKeyValue.FindBoolAttribute(kv, "define")) { if (func.TypeParameters.Count > 0) SemErr("function with :define attribute has to be monomorphic"); func.DefinitionBody = func.CreateFunctionDefinition(definition); @@ -1032,7 +1032,6 @@ TransferCmd = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; List ss = new List(); - QKeyValue kv = null; .) ( "goto" (. y = t; .) Idents (. foreach(IToken/*!*/ s in xs){ @@ -1040,9 +1039,7 @@ TransferCmd ss.Add(s.val); } tc = new GotoCmd(y, ss); .) - | "return" - { Attribute } - (. tc = new ReturnCmd(t) { Attributes = kv }; .) + | "return" (. tc = new ReturnCmd(t); .) ) ";" . @@ -1691,7 +1688,6 @@ SpecBlock List/*!*/ xs; List ss = new List(); b = dummyBlock; - QKeyValue kv = null; Expr/*!*/ e; .) Ident ":" @@ -1710,13 +1706,8 @@ SpecBlock ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); .) - | "return" - { Attribute } - Expression - (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { - Attributes = kv - }); - .) + | "return" Expression + (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) ) ";" . diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 3e3ff4bc5..42b25efab 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -127,7 +127,7 @@ public static List FindAllAttributes(this ICarriesAttributes obj, str public static bool HasAttribute(this ICarriesAttributes obj, string name) { - return obj.Attributes.FindBoolAttribute(name); + return QKeyValue.FindBoolAttribute(obj.Attributes, name); } public static bool RemoveAttributes(ICarriesAttributes obj, Func cond) diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index b7ab2e965..d0d472ff5 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -10,8 +10,6 @@ namespace Microsoft.Boogie public interface CoreOptions : PrintOptions { public TextWriter OutputWriter { get; } - bool UseBaseNameForFileName { get; } - public enum TypeEncoding { Predicates, diff --git a/Source/Core/FunctionDependencyChecker.cs b/Source/Core/FunctionDependencyChecker.cs index fce5eb802..a3a958fd9 100644 --- a/Source/Core/FunctionDependencyChecker.cs +++ b/Source/Core/FunctionDependencyChecker.cs @@ -16,17 +16,17 @@ public static bool Check(Program program) { checkingContext.Error(function.tok, "Parameter to :inline attribute on a function must be Boolean"); } - if (function.Attributes.FindBoolAttribute("inline") && - function.Attributes.FindBoolAttribute("define")) + if (QKeyValue.FindBoolAttribute(function.Attributes, "inline") && + QKeyValue.FindBoolAttribute(function.Attributes, "define")) { checkingContext.Error(function.tok, "A function may not have both :inline and :define attributes"); } - if (function.Attributes.FindBoolAttribute("inline") && + if (QKeyValue.FindBoolAttribute(function.Attributes, "inline") && function.Body == null) { checkingContext.Error(function.tok, "Function with :inline attribute must have a body"); } - if (function.Attributes.FindBoolAttribute("define") && + if (QKeyValue.FindBoolAttribute(function.Attributes, "define") && function.DefinitionBody == null) { checkingContext.Error(function.tok, "Function with :define attribute must have a body"); @@ -84,13 +84,13 @@ private FunctionDependencyChecker() public override Function VisitFunction(Function node) { - if (node.Attributes.FindBoolAttribute("inline")) + if (QKeyValue.FindBoolAttribute(node.Attributes, "inline")) { this.enclosingFunction = node; base.Visit(node.Body); this.enclosingFunction = null; } - else if (node.Attributes.FindBoolAttribute("define")) + else if (QKeyValue.FindBoolAttribute(node.Attributes, "define")) { this.enclosingFunction = node; base.Visit(node.DefinitionBody.Args[1]); @@ -103,8 +103,8 @@ public override Expr VisitNAryExpr(NAryExpr node) { if (node.Fun is FunctionCall functionCall) { - if (functionCall.Func.Attributes.FindBoolAttribute("inline") || - functionCall.Func.Attributes.FindBoolAttribute("define")) + if (QKeyValue.FindBoolAttribute(functionCall.Func.Attributes, "inline") || + QKeyValue.FindBoolAttribute(functionCall.Func.Attributes, "define")) { functionDependencyGraph.AddEdge(enclosingFunction, functionCall.Func); } diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs deleted file mode 100644 index 6825839b8..000000000 --- a/Source/Core/Generic/ListExtensions.cs +++ /dev/null @@ -1,31 +0,0 @@ -using System.Collections; -using System.Collections.Generic; -using System.Linq; - -namespace Microsoft.Boogie; - -public static class ListExtensions { - public static IReadOnlyList Reversed(this IReadOnlyList list) { - return new ReversedReadOnlyList(list); - } -} - -class ReversedReadOnlyList : IReadOnlyList { - private readonly IReadOnlyList inner; - - public ReversedReadOnlyList(IReadOnlyList inner) { - this.inner = inner; - } - - public IEnumerator GetEnumerator() { - return Enumerable.Range(0, inner.Count).Select(index => this[index]).GetEnumerator(); - } - - IEnumerator IEnumerable.GetEnumerator() { - return GetEnumerator(); - } - - public int Count => inner.Count; - - public T this[int index] => inner[^(index + 1)]; -} \ No newline at end of file diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index d67732fa2..3162cddbe 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -580,7 +580,7 @@ private Cmd InlinedRequires(CallCmd callCmd, Requires req) private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) { - if (ens.Attributes.FindBoolAttribute("InlineAssume")) + if (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) { return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition)); } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 68966a376..ff6ecb84f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -501,11 +501,11 @@ void Function(out List/*!*/ ds) { } if (definition != null) { // generate either an axiom or a function body - if (kv.FindBoolAttribute("inline")) { - if (kv.FindBoolAttribute("define")) + if (QKeyValue.FindBoolAttribute(kv, "inline")) { + if (QKeyValue.FindBoolAttribute(kv, "define")) SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; - } else if (kv.FindBoolAttribute("define")) { + } else if (QKeyValue.FindBoolAttribute(kv, "define")) { if (func.TypeParameters.Count > 0) SemErr("function with :define attribute has to be monomorphic"); func.DefinitionBody = func.CreateFunctionDefinition(definition); @@ -1536,7 +1536,6 @@ void TransferCmd(out TransferCmd/*!*/ tc) { Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; List ss = new List(); - QKeyValue kv = null; if (la.kind == 55) { Get(); @@ -1549,10 +1548,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) { } else if (la.kind == 56) { Get(); - while (la.kind == 26) { - Attribute(ref kv); - } - tc = new ReturnCmd(t) { Attributes = kv }; + tc = new ReturnCmd(t); } else SynErr(148); Expect(10); } @@ -2562,7 +2558,6 @@ void SpecBlock(out Block/*!*/ b) { List/*!*/ xs; List ss = new List(); b = dummyBlock; - QKeyValue kv = null; Expr/*!*/ e; Ident(out x); @@ -2588,14 +2583,8 @@ void SpecBlock(out Block/*!*/ b) { } else if (la.kind == 56) { Get(); - while (la.kind == 26) { - Attribute(ref kv); - } Expression(out e); - b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { - Attributes = kv - }); - + b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); } else SynErr(174); Expect(10); } diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index ee240bde7..47fe6bd57 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -560,12 +560,12 @@ T SelectNonExtern(T a, T b) where T : Declaration Contract.Result() == b); T ignore, keep; - if (a.Attributes.FindBoolAttribute("extern")) + if (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) { ignore = a; keep = b; } - else if (b.Attributes.FindBoolAttribute("extern")) + else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) { ignore = b; keep = a; diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs index 27a0dd156..5f7a1bb1f 100644 --- a/Source/Core/Token.cs +++ b/Source/Core/Token.cs @@ -33,7 +33,8 @@ public string /*!*/ public Token next; // ML 2005-03-11 Tokens are kept in linked list - public static readonly IToken /*!*/ NoToken = new Token(); + public static readonly IToken /*!*/ + NoToken = new Token(); public Token() { diff --git a/Source/Core/Generic/Util.cs b/Source/Core/Util.cs similarity index 100% rename from Source/Core/Generic/Util.cs rename to Source/Core/Util.cs diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 064b4a6db..2e0ae6c67 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -425,7 +425,7 @@ private HashSet GetControlDependencyVariables(string proc, B foreach (Cmd c in succ.Cmds) { AssumeCmd a = c as AssumeCmd; - if (a != null && a.Attributes.FindBoolAttribute("partition")) + if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) { var VarCollector = new VariableCollector(); VarCollector.VisitExpr(a.Expr); @@ -523,14 +523,14 @@ private Dictionary> ComputeGlobalControlDependences() foreach (var impl in prog.NonInlinedImplementations()) { var blockGraph = prog.ProcessLoops(options, impl); - localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok, new ReturnCmd(prog.tok))); + localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok)); foreach (var keyValue in localCtrlDeps[impl]) { globalCtrlDep.Add(keyValue.Key, keyValue.Value); } } - Graph callGraph = Program.BuildCallGraph(options, prog); + var callGraph = Program.BuildCallGraph(options, prog); // Add inter-procedural control dependence nodes based on calls foreach (var impl in prog.NonInlinedImplementations()) @@ -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); } @@ -562,18 +562,17 @@ private Dictionary> ComputeGlobalControlDependences() // Finally reverse the dependences - Dictionary> result = new Dictionary>(); - - foreach (var KeyValue in globalCtrlDep) + var result = new Dictionary>(); + foreach (var keyValue in globalCtrlDep) { - foreach (var v in KeyValue.Value) + foreach (var v in keyValue.Value) { if (!result.ContainsKey(v)) { result[v] = new HashSet(); } - result[v].Add(KeyValue.Key); + result[v].Add(keyValue.Key); } } diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index ec349a347..112c6c481 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.2 + 3.3.3 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 764ea17a4..171797990 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -105,7 +105,7 @@ static void PassifyAllImplementations(ExecutionEngineOptions options, ProcessedP foreach(var implementation in processedProgram.Program.Implementations) { vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter), - callback, out _, out _); + callback, out _, out _, out _); } } diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs index 183a7028c..ecb6b4220 100644 --- a/Source/ExecutionEngine/ConsolePrinter.cs +++ b/Source/ExecutionEngine/ConsolePrinter.cs @@ -177,9 +177,8 @@ public virtual void ReportBplError(IToken tok, string message, bool error, TextW message = $"{category}: {message}"; } - var s = tok != null - ? string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(Options, tok.filename), tok.line, - tok.col, message) + var s = tok != null + ? $"{ExecutionEngine.GetFileNameForConsole(Options, tok.filename)}({tok.line},{tok.col}): {message}" : message; if (error) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 72002036b..0d6fa1bbc 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -436,7 +436,7 @@ public PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, Options.OutputWriter.WriteLine("Datatypes only supported with monomorphic encoding"); return PipelineOutcome.FatalError; } - else if (program.TopLevelDeclarations.OfType().Any(f => f.Attributes.FindBoolAttribute("define"))) + else if (program.TopLevelDeclarations.OfType().Any(f => QKeyValue.FindBoolAttribute(f.Attributes, "define"))) { Options.OutputWriter.WriteLine("Functions with :define attribute only supported with monomorphic encoding"); return PipelineOutcome.FatalError; @@ -736,15 +736,16 @@ public async Task> GetVerificationTasks(Program { var writer = TextWriter.Null; var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool); + var run = new ImplementationRun(implementation, writer); var collector = new VerificationResultCollector(Options); vcGenerator.PrepareImplementation(run, collector, out _, + out var gotoCmdOrigins, out var modelViewInfo); ConditionGeneration.ResetPredecessors(run.Implementation.Blocks); - var splits = ManualSplitFinder.GetParts(Options, run, - (token, blocks) => new ManualSplit(Options, () => blocks, vcGenerator, run, token)).ToList(); + var splits = ManualSplitFinder.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList(); for (var index = 0; index < splits.Count; index++) { var split = splits[index]; split.SplitIndex = index; @@ -1309,8 +1310,6 @@ public void ProcessErrors(OutputPrinter printer, return; } - // When an assertion fails on multiple paths, only show an error for one of them. - errors = errors.DistinctBy(e => e.FailingAssert).ToList(); errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { diff --git a/Source/ExecutionEngine/ExecutionEngineOptions.cs b/Source/ExecutionEngine/ExecutionEngineOptions.cs index baf7c48a1..f7e4806df 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -22,6 +22,7 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions ShowEnvironment ShowEnv { get; } string Version { get; } string Environment { get; } + bool UseBaseNameForFileName { get; } HashSet Libraries { get; set; } bool NoResolve { get; } bool NoTypecheck { get; } diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 50f3fd8e5..43dda6925 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -44,7 +44,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra public IVerificationTask FromSeed(int newSeed) { - var split = new ManualSplit(Split.Options, () => Split.Blocks, + var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.GotoCmdOrigins, Split.parent, Split.Run, Split.Token, newSeed); split.SplitIndex = Split.SplitIndex; return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo); diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 2af21485a..2738566dd 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -99,22 +99,22 @@ public bool DominatedBy(Node dominee, Node dominator, List path = null) return true; } - int currentDominator = nodeNumberToImmediateDominator[domineeNum]; + int currentDominatorNum = nodeNumberToImmediateDominator[domineeNum]; while (true) { - if (currentDominator == dominatorNum) + if (currentDominatorNum == dominatorNum) { return true; } - if (currentDominator == sourceNum) + if (currentDominatorNum == sourceNum) { return false; } - path?.Add(postOrderNumberToNode[currentDominator]); + path?.Add(postOrderNumberToNode[currentDominatorNum]); - currentDominator = nodeNumberToImmediateDominator[currentDominator]; + currentDominatorNum = nodeNumberToImmediateDominator[currentDominatorNum]; } } @@ -623,55 +623,35 @@ public List SuccessorsAsList(Node n) } } - /// - /// This method gives a simpler way to compute dominators but it assmumes the graph is a DAG. - /// With acyclicty we can compute all dominators by traversing the graph (once) in topological order - /// (using the property: A vertex's dominator set is unaffected by vertices that come later). - /// The method does not check the graph for the DAG property. That risk is on the caller. - /// - public Dictionary> AcyclicDominators() + // This method gives a simpler way to compute dominators but it assmumes the graph is a DAG. + // With acyclicty we can compute all dominators by traversing the graph (once) in topological order + // (using the property: A vertex's dominator set is unaffected by vertices that come later). + // The method does not check the graph for the DAG property. That risk is on the caller. + public Dictionary> DominatorsFast() { - var dominatorsPerNode = new Dictionary>(); - foreach (var node in TopologicalSort()) + var topoSorted = TopologicalSort().ToList(); + var dominators = new Dictionary>(); + topoSorted.ForEach(u => dominators[u] = topoSorted.ToHashSet()); + foreach (var node in topoSorted) { - var predecessors = Predecessors(node); - var dominatorsForNode = Intersection(predecessors.Select(p => dominatorsPerNode[p])); - dominatorsForNode.Add(node); - dominatorsPerNode[node] = dominatorsForNode; - } - return dominatorsPerNode; - } - - public static HashSet Intersection(IEnumerable> sets) { - var first = true; - HashSet result = null; - foreach (var set in sets) { - if (first) { - result = set.ToHashSet(); - first = false; - } else { - result!.IntersectWith(set); + var s = new HashSet(); + var predecessors = Predecessors(node).ToList(); + if (predecessors.Count != 0) + { + s.UnionWith(dominators[predecessors.First()]); + predecessors.ForEach(v => s.IntersectWith(dominators[v])); } + s.Add(node); + dominators[node] = s; } - - if (result == null) { - return new HashSet(); - } - - return result; + return dominators; } - /// - /// Use this method only for DAGs because it uses DominatorsFast() for computing dominators - /// + // Use this method only for DAGs because it uses DominatorsFast() for computing dominators public Dictionary ImmediateDominator() { - var topoSorted = TopologicalSort().ToList(); - var indexPerNode = new Dictionary(); - for (int index = 0; index < topoSorted.Count; index++) { - indexPerNode[topoSorted[index]] = index; - } - var dominators = AcyclicDominators(); + List topoSorted = TopologicalSort().ToList(); + Dictionary> dominators = DominatorsFast(); var immediateDominator = new Dictionary(); foreach (var node in Nodes) { @@ -679,10 +659,9 @@ public Dictionary ImmediateDominator() { dominators[node].Remove(node); } - immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => indexPerNode[e])); + immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => topoSorted.IndexOf(e))); } - - immediateDominator.Remove(source); + immediateDominator[source] = source; return immediateDominator; } @@ -707,7 +686,7 @@ public List ImmediatelyDominatedBy(Node /*!*/ n) return dominees ?? new List(); } - public List TopologicalSort(bool reversed = false) + public List TopologicalSort(bool reversed = false) { TarjanTopSort(out var acyclic, out var sortedList, reversed); return acyclic ? sortedList : new List(); @@ -1154,7 +1133,7 @@ public string ToDot(Func NodeLabel = null, Func Node return s.ToString(); } - public ISet ComputeReachability(Node start, bool forward = true) + public ICollection ComputeReachability(Node start, bool forward = true) { var todo = new Stack(); var visited = new HashSet(); diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs index 0ad80927d..e88ca2fb9 100644 --- a/Source/Houdini/AnnotationDependenceAnalyser.cs +++ b/Source/Houdini/AnnotationDependenceAnalyser.cs @@ -232,7 +232,7 @@ private IEnumerable AnnotationInstances() { yield return new AnnotationInstance(c, impl.Name, p.Expr); } - else if ((p is AssertCmd) && p.Attributes.FindBoolAttribute("originated_from_invariant")) + else if ((p is AssertCmd) && QKeyValue.FindBoolAttribute(p.Attributes, "originated_from_invariant")) { var tag = GetTagFromNonCandidateAttributes(p.Attributes); if (tag != null) @@ -467,7 +467,7 @@ private IEnumerable GetNonCandidateAnnotations() continue; } - if (!Assertion.Attributes.FindBoolAttribute("originated_from_invariant")) + if (!QKeyValue.FindBoolAttribute(Assertion.Attributes, "originated_from_invariant")) { continue; } @@ -528,7 +528,7 @@ private IEnumerable GetNonCandidateAnnotations() private IEnumerable GetCandidates() { return prog.Variables.Where(Item => - Item.Attributes.FindBoolAttribute("existential")).Select(Item => Item.Name); + QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); } @@ -611,7 +611,7 @@ public StagedHoudiniPlan ApplyStages() newCmds.Add(new AssumeCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr, Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c), a.Attributes)); } - else if (a.Attributes.FindBoolAttribute("originated_from_invariant")) + else if (QKeyValue.FindBoolAttribute(a.Attributes, "originated_from_invariant")) { string tag = GetTagFromNonCandidateAttributes(a.Attributes); if (tag == null) diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 2afaddbf4..4efc13c77 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1617,7 +1617,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead public static void ApplyAssignment(Program prog, HoudiniOutcome outcome) { var Candidates = prog.TopLevelDeclarations.OfType().Where( - Item => Item.Attributes.FindBoolAttribute("existential")).Select(Item => Item.Name); + Item => QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); // Treat all assertions // TODO: do we need to also consider assumptions? diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index a787a8a65..ee24e7bfa 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -168,7 +168,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); new RemoveBackEdges(vcgen).ConvertCfg2Dag(run, taskID: taskId); - vcgen.PassifyImpl(run, out var mvInfo); + var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo); ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out var ecollector); this.houdiniAssertConstants = ecollector.houdiniAssertConstants; @@ -196,7 +196,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); proverInterface.DefineMacro(macro, conjecture); conjecture = exprGen.Function(macro); - handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, absyIds, impl.Blocks, impl.debugInfos, collector, + handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector, mvInfo, proverInterface.Context, program, this); } diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 85d1f41a1..6c39f1ec0 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -98,8 +98,7 @@ procedure Procedure(y: int) var engine = ExecutionEngine.CreateWithoutSharedCache(options); var tasks = await engine.GetVerificationTasks(program); - // The implicit return at the end gets a separate VC. - // first split is empty. Maybe it can be optimized away + // The first split is empty. Maybe it can be optimized away Assert.AreEqual(4, tasks.Count); var outcomes = new List { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid }; diff --git a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs index 94505c1c9..fb0087cd8 100644 --- a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs @@ -17,7 +17,7 @@ public class RandomSeedTest axiom N <= 3; procedure nEquals3() - ensures 1 == 1; + ensures true; { }"; diff --git a/Source/VCGeneration/Counterexample/AssertCounterexample.cs b/Source/VCGeneration/AssertCounterexample.cs similarity index 82% rename from Source/VCGeneration/Counterexample/AssertCounterexample.cs rename to Source/VCGeneration/AssertCounterexample.cs index 522b55cd0..e43d6fecd 100644 --- a/Source/VCGeneration/Counterexample/AssertCounterexample.cs +++ b/Source/VCGeneration/AssertCounterexample.cs @@ -6,19 +6,23 @@ namespace Microsoft.Boogie; public class AssertCounterexample : Counterexample { + [Peer] public AssertCmd FailingAssert; + [ContractInvariantMethod] void ObjectInvariant() { + Contract.Invariant(FailingAssert != null); } public AssertCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssert) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) { Contract.Requires(trace != null); Contract.Requires(failingAssert != null); Contract.Requires(context != null); + this.FailingAssert = failingAssert; } protected override Cmd ModelFailingCommand => FailingAssert; @@ -28,7 +32,10 @@ public override int GetLocation() return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; } - public override byte[] Checksum => FailingAssert.Checksum; + public override byte[] Checksum + { + get { return FailingAssert.Checksum; } + } public override Counterexample Clone() { diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 13ee3a18a..2e7f91060 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -222,7 +222,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu Block origStartBlock = impl.Blocks[0]; Block insertionPoint = new Block( - Token.NoToken, blockLabel, startCmds, + new Token(-17, -4), blockLabel, startCmds, new GotoCmd(impl.tok, new List {origStartBlock.Label}, new List {origStartBlock})); impl.Blocks.Insert(0, insertionPoint); // make insertionPoint the start block @@ -236,7 +236,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu AssumeCmd c = new AssumeCmd(req.tok, e, CivlAttributes.ApplySubstitutionToPoolHints(formalProcImplSubst, req.Attributes)); // Copy any {:id ...} from the precondition to the assumption, so // we can track it while analyzing verification coverage. - (c as ICarriesAttributes).CopyIdFrom(req.tok, req); + c.CopyIdFrom(req.tok, req); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -450,6 +450,8 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr options.PrintDesugarings = oldPrintDesugaringSetting; } + + public static void ResetPredecessors(List blocks) { Contract.Requires(blocks != null); @@ -764,7 +766,7 @@ protected Dictionary ConvertBlocks2PassiveCmd(TextWriter traceWr Dictionary incarnationMap = ComputeIncarnationMap(b, block2Incarnation); // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out. - b.LiveVarsBefore = null; + b.liveVarsBefore = null; // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, // all its successors have been passified. Consequently, its entry in block2Incarnation can be removed. @@ -879,7 +881,8 @@ private void AddDebugInfo(Cmd c, Dictionary incarnationMap, List { foreach (var param in current.Params) { - if (param is IdentifierExpr identifierExpr) { + if (param is IdentifierExpr identifierExpr) + { debugExprs.Add(incarnationMap.GetValueOrDefault(identifierExpr.Decl, identifierExpr)); } else @@ -1037,7 +1040,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing } } else if (pc is AssumeCmd - && pc.Attributes.FindBoolAttribute("precondition_previous_snapshot") + && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") && pc.SugaredCmdChecksum != null) { if (!relevantDoomedAssumpVars.Any() @@ -1062,7 +1065,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing dropCmd = true; } } - else if (pc is AssumeCmd && pc.Attributes.FindBoolAttribute("assumption_variable_initialization")) + else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization")) { var identExpr = pc.Expr as IdentifierExpr; if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl)) @@ -1197,7 +1200,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing var assumeCmd = new AssumeCmd(c.tok, assumption); // Copy any {:id ...} from the assignment to the assumption, so // we can track it while analyzing verification coverage. - (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); + assumeCmd.CopyIdFrom(assign.tok, assign); passiveCmds.Add(assumeCmd); } @@ -1210,7 +1213,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing { var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr; if (identExpr != null && identExpr.Decl != null && - identExpr.Decl.Attributes.FindBoolAttribute("assumption") && + QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out var incarnation)) { TraceCachingAction(traceWriter, assign, CachingAction.AssumeNegationOfAssumptionVariable); @@ -1238,7 +1241,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map. List havocVars = hc.Vars.Where(v => - !(v.Decl.Attributes.FindBoolAttribute("assumption") && v.Decl.Name.StartsWith("a##cached##"))) + !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))) .ToList(); // First, compute the new incarnations foreach (IdentifierExpr ie in havocVars) @@ -1273,7 +1276,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing // assume v_post ==> v_pre; foreach (IdentifierExpr ie in havocVars) { - if (ie.Decl.Attributes.FindBoolAttribute("assumption")) + if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption")) { var preInc = (Expr) (preHavocIncarnationMap[ie.Decl].Clone()); var postInc = (Expr) (incarnationMap[ie.Decl].Clone()); @@ -1391,7 +1394,7 @@ public Block CreateBlockBetween(int predIndex, Block succ) bs.Add(succ); Block newBlock = new Block( - Token.NoToken, + new Token(-17, -4), newBlockLabel, new List(), new GotoCmd(Token.NoToken, ls, bs) diff --git a/Source/VCGeneration/Counterexample/CallCounterexample.cs b/Source/VCGeneration/Counterexamples/CallCounterexample.cs similarity index 86% rename from Source/VCGeneration/Counterexample/CallCounterexample.cs rename to Source/VCGeneration/Counterexamples/CallCounterexample.cs index 199df0c15..e98ce17b3 100644 --- a/Source/VCGeneration/Counterexample/CallCounterexample.cs +++ b/Source/VCGeneration/Counterexamples/CallCounterexample.cs @@ -6,8 +6,9 @@ namespace Microsoft.Boogie; public class CallCounterexample : Counterexample { - public readonly CallCmd FailingCall; - public readonly Requires FailingRequires; + public CallCmd FailingCall; + public Requires FailingRequires; + public AssertRequiresCmd FailingFailingAssert; [ContractInvariantMethod] void ObjectInvariant() @@ -19,7 +20,7 @@ void ObjectInvariant() public CallCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertRequiresCmd failingAssertRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum = null) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertRequires) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) { var failingRequires = failingAssertRequires.Requires; var failingCall = failingAssertRequires.Call; @@ -30,6 +31,7 @@ public CallCounterexample(VCGenOptions options, List trace, List Contract.Requires(failingRequires != null); this.FailingCall = failingCall; this.FailingRequires = failingRequires; + this.FailingFailingAssert = failingAssertRequires; this.checksum = checksum; this.SugaredCmdChecksum = failingCall.Checksum; } @@ -50,7 +52,7 @@ public override byte[] Checksum public override Counterexample Clone() { - var ret = new CallCounterexample(Options, Trace, AugmentedTrace, (AssertRequiresCmd)FailingAssert, Model, MvInfo, Context, ProofRun, Checksum); + var ret = new CallCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, Model, MvInfo, Context, ProofRun, Checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs b/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs similarity index 100% rename from Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs rename to Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs diff --git a/Source/VCGeneration/Counterexample/Counterexample.cs b/Source/VCGeneration/Counterexamples/Counterexample.cs similarity index 97% rename from Source/VCGeneration/Counterexample/Counterexample.cs rename to Source/VCGeneration/Counterexamples/Counterexample.cs index 15d4cab2b..da9cdca9c 100644 --- a/Source/VCGeneration/Counterexample/Counterexample.cs +++ b/Source/VCGeneration/Counterexamples/Counterexample.cs @@ -25,7 +25,6 @@ void ObjectInvariant() protected readonly VCGenOptions Options; [Peer] public List Trace; public readonly List AugmentedTrace; - public AssertCmd FailingAssert { get; } public Model Model { get; } public readonly ModelViewInfo MvInfo; public readonly ProverContext Context; @@ -36,7 +35,7 @@ void ObjectInvariant() public Dictionary CalleeCounterexamples; internal Counterexample(VCGenOptions options, List trace, List augmentedTrace, Model model, - VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, AssertCmd failingAssert) + VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) { Contract.Requires(trace != null); Contract.Requires(context != null); @@ -46,7 +45,6 @@ internal Counterexample(VCGenOptions options, List trace, List au this.MvInfo = mvInfo; this.Context = context; this.ProofRun = proofRun; - this.FailingAssert = failingAssert; this.CalleeCounterexamples = new Dictionary(); // the call to instance method GetModelValue in the following code requires the fields Model and Context to be initialized if (augmentedTrace != null) @@ -114,7 +112,7 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { int numBlock = -1; string ind = new string(' ', indent); - foreach (Block block in Trace) + foreach (var block in Trace) { Contract.Assert(block != null); numBlock++; @@ -122,9 +120,13 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { tw.WriteLine("{0}", ind); } - else { + else + { // for ErrorTrace == 1 restrict the output; - if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) { + // do not print tokens with -17:-4 as their location because they have been + // introduced in the translation and do not give any useful feedback to the user + if (Options.ErrorTrace == 1 && block.tok.line == -17 && block.tok.col == -4) + { continue; } @@ -135,7 +137,8 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) for (int numInstr = 0; numInstr < block.Cmds.Count; numInstr++) { var loc = new TraceLocation(numBlock, numInstr); - if (!CalleeCounterexamples.ContainsKey(loc)) { + if (!CalleeCounterexamples.ContainsKey(loc)) + { continue; } diff --git a/Source/VCGeneration/Counterexample/CounterexampleComparer.cs b/Source/VCGeneration/Counterexamples/CounterexampleComparer.cs similarity index 100% rename from Source/VCGeneration/Counterexample/CounterexampleComparer.cs rename to Source/VCGeneration/Counterexamples/CounterexampleComparer.cs diff --git a/Source/VCGeneration/Counterexample/TraceLocation.cs b/Source/VCGeneration/Counterexamples/TraceLocation.cs similarity index 100% rename from Source/VCGeneration/Counterexample/TraceLocation.cs rename to Source/VCGeneration/Counterexamples/TraceLocation.cs diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs new file mode 100644 index 000000000..2da576e11 --- /dev/null +++ b/Source/VCGeneration/FocusAttribute.cs @@ -0,0 +1,147 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; +using Block = Microsoft.Boogie.Block; +using Cmd = Microsoft.Boogie.Cmd; +using PredicateCmd = Microsoft.Boogie.PredicateCmd; +using QKeyValue = Microsoft.Boogie.QKeyValue; +using ReturnCmd = Microsoft.Boogie.ReturnCmd; +using TransferCmd = Microsoft.Boogie.TransferCmd; +using VCGenOptions = Microsoft.Boogie.VCGenOptions; + +namespace VCGeneration; + +public static class FocusAttribute +{ + + public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) + { + var impl = run.Implementation; + var dag = Program.GraphFromImpl(impl); + var topologicallySortedBlocks = dag.TopologicalSort().ToList(); + // 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 focusBlocks = GetFocusBlocks(topologicallySortedBlocks); + if (par.CheckerPool.Options.RelaxFocus) { + focusBlocks.Reverse(); + } + if (!focusBlocks.Any()) { + return new List { new(options, () => impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) }; + } + + var ancestorsPerBlock = new Dictionary>(); + var descendantsPerBlock = new Dictionary>(); + focusBlocks.ForEach(fb => ancestorsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, false).ToHashSet()); + focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, true).ToHashSet()); + var result = new List(); + var duplicator = new Duplicator(); + + FocusRec(run.Implementation.tok, 0, impl.Blocks, new List()); + return result; + + void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList blocksToInclude, IReadOnlyList freeAssumeBlocks) + { + if (focusIndex == focusBlocks.Count) + { + // it is important for l to be consistent with reverse topological order. + var sortedBlocks = dag.TopologicalSort().Where(blocksToInclude.Contains).Reverse(); + // assert that the root block, impl.Blocks[0], is in l + var newBlocks = new List(); + var oldToNewBlockMap = new Dictionary(blocksToInclude.Count()); + foreach (var block in sortedBlocks) + { + var newBlock = (Block)duplicator.Visit(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. + if(freeAssumeBlocks.Contains(block)) + { + newBlock.Cmds = block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(DisableSplits).ToList(); + } + if (block.TransferCmd is GotoCmd gtc) + { + var targets = gtc.LabelTargets.Where(blocksToInclude.Contains).ToList(); + newBlock.TransferCmd = new GotoCmd(gtc.tok, + targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), + targets.Select(blk => oldToNewBlockMap[blk]).ToList()); + } + } + newBlocks.Reverse(); + Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); + result.Add(new ManualSplit(options, () => + { + BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); + return newBlocks; + }, gotoCmdOrigins, par, run, focusToken)); + } + else if (!blocksToInclude.Contains(focusBlocks[focusIndex].Block) || freeAssumeBlocks.Contains(focusBlocks[focusIndex].Block)) + { + FocusRec(focusBlocks[focusIndex].Token, focusIndex + 1, blocksToInclude, freeAssumeBlocks); + } + else + { + var (block, nextToken) = focusBlocks[focusIndex]; // assert b in blocks + var dominatedBlocks = DominatedBlocks(topologicallySortedBlocks, block, blocksToInclude); + // the first part takes all blocks except the ones dominated by the focus block + FocusRec(nextToken, focusIndex + 1, blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToList(), freeAssumeBlocks); + var ancestors = ancestorsPerBlock[block]; + ancestors.Remove(block); + var descendants = descendantsPerBlock[block]; + // the other part takes all the ancestors, the focus block, and the descendants. + FocusRec(nextToken, focusIndex + 1, + ancestors.Union(descendants).Intersect(blocksToInclude).ToList(), + ancestors.Union(freeAssumeBlocks).ToList()); + } + } + } + + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + private static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, IEnumerable subgraph) + { + var dominators = new Dictionary>(); + foreach (var b in topologicallySortedBlocks.Where(subgraph.Contains)) + { + var s = new HashSet(); + var pred = b.Predecessors.Where(subgraph.Contains).ToList(); + if (pred.Count != 0) + { + s.UnionWith(dominators[pred[0]]); + pred.ForEach(blk => s.IntersectWith(dominators[blk])); + } + s.Add(b); + dominators[b] = s; + } + return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); + } + + private static Cmd DisableSplits(Cmd command) + { + if (command is not PredicateCmd pc) + { + return command; + } + + for (var kv = pc.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "split") + { + kv.AddParam(new LiteralExpr(Token.NoToken, false)); + } + } + return command; + } + + private static List<(Block Block, IToken Token)> GetFocusBlocks(List blocks) { + return blocks. + Select(block => (Block: block, FocusCommand: block.Cmds.FirstOrDefault(IsFocusCmd)?.tok)). + Where(t => t.FocusCommand != null).ToList(); + } + + private static bool IsFocusCmd(Cmd c) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); + } +} \ No newline at end of file diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs index e0f40524b..a8fa2bc30 100644 --- a/Source/VCGeneration/LoopExtractor.cs +++ b/Source/VCGeneration/LoopExtractor.cs @@ -313,7 +313,10 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G continue; } - var newBlock = Block.ShallowClone(block); + Block newBlock = new Block(block.tok) + { + Label = block.Label + }; if (headRecursion && block == header) { CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone(); @@ -331,8 +334,11 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G blockMap[block] = newBlock; if (newBlocksCreated.TryGetValue(block, out var original)) { - var newBlock2 = Block.ShallowClone(original); - newBlock2.Cmds = Substituter.Apply(subst, original.Cmds); + var newBlock2 = new Block(original.tok) + { + Label = original.Label, + Cmds = Substituter.Apply(subst, original.Cmds) + }; blockMap[original] = newBlock2; } @@ -344,18 +350,22 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G auxGotoCmd.LabelTargets != null && auxGotoCmd.LabelTargets.Count >= 1); //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode var loopNodes = GetBlocksInAllNaturalLoops(options, header, g); //var loopNodes = g.NaturalLoops(header, source); - foreach (var bl in auxGotoCmd.LabelTargets) { - if (!g.Nodes.Contains(bl) || // newly created blocks are not present in NaturalLoop(header, xx, g) - loopNodes.Contains(bl)) { + foreach (var bl in auxGotoCmd.LabelTargets) + { + if (!g.Nodes.Contains(bl) || //newly created blocks are not present in NaturalLoop(header, xx, g) + loopNodes.Contains(bl)) + { continue; } - var auxNewBlock = Block.ShallowClone(bl); - // these blocks may have read/write locals that are not present in naturalLoops - // we need to capture these variables - auxNewBlock.Cmds = Substituter.Apply(subst, bl.Cmds); - - // add restoration code for such blocks + var auxNewBlock = new Block(bl.tok) + { + Label = bl.Label, + //these blocks may have read/write locals that are not present in naturalLoops + //we need to capture these variables + Cmds = Substituter.Apply(subst, bl.Cmds) + }; + //add restoration code for such blocks if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd)) { auxNewBlock.Cmds.Add(assignCmd); diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs index 5b47299b7..09927d3c1 100644 --- a/Source/VCGeneration/ManualSplit.cs +++ b/Source/VCGeneration/ManualSplit.cs @@ -1,22 +1,22 @@ using System; using System.Collections.Generic; using Microsoft.Boogie; -using VCGeneration; namespace VC; public class ManualSplit : Split { - public IImplementationPartOrigin Token { get; } + public IToken Token { get; } public ManualSplit(VCGenOptions options, Func> blocks, - VerificationConditionGenerator parent, + Dictionary gotoCmdOrigins, + VerificationConditionGenerator par, ImplementationRun run, - IImplementationPartOrigin origin, int? randomSeed = null) - : base(options, blocks, parent, run, randomSeed) + IToken token, int? randomSeed = null) + : base(options, blocks, gotoCmdOrigins, par, run, randomSeed) { - Token = origin; + Token = token; } } \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs new file mode 100644 index 000000000..ffc6806d2 --- /dev/null +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -0,0 +1,216 @@ +#nullable enable +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +public static class ManualSplitFinder { + public static IEnumerable FocusAndSplit(Program program, VCGenOptions options, ImplementationRun run, + Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { + var focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); + return focussedImpl.SelectMany(s => FindManualSplits(program, s)); + } + + private static List FindManualSplits(Program program, ManualSplit initialSplit) { + Contract.Requires(initialSplit.Implementation != null); + Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); + + var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert; + initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + + var splitPoints = new Dictionary>(); + foreach (var block in initialSplit.Blocks) { + foreach (Cmd command in block.Cmds) { + if (ShouldSplitHere(command, splitOnEveryAssert)) { + splitPoints.GetOrCreate(block, () => new List()).Add(command.tok); + } + } + } + var splits = new List(); + if (!splitPoints.Any()) { + splits.Add(initialSplit); + } else { + Block entryPoint = initialSplit.Blocks[0]; + var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints); + var entryBlockHasSplit = splitPoints.ContainsKey(entryPoint); + var firstSplitBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, + -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert); + if (firstSplitBlocks != null) + { + splits.Add(new ManualSplit(initialSplit.Options, () => { + BlockTransformations.Optimize(firstSplitBlocks); + return firstSplitBlocks; + }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token)); + } + foreach (var block in initialSplit.Blocks) { + var tokens = splitPoints.GetValueOrDefault(block); + if (tokens == null) { + continue; + } + + for (int i = 0; i < tokens.Count; i++) { + var token = tokens[i]; + bool lastSplitInBlock = i == tokens.Count - 1; + var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, block, lastSplitInBlock, splitOnEveryAssert); + if (newBlocks != null) + { + splits.Add(new ManualSplit(initialSplit.Options, + () => { + BlockTransformations.Optimize(newBlocks); + return newBlocks; + }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); + } + } + } + } + return splits; + } + + private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") + || c is AssertCmd && splitOnEveryAssert; + } + + // Verify b with the last split in blockAssignments[b] + private static Dictionary PickBlocksToVerify(List blocks, Dictionary> splitPoints) { + var todo = new Stack(); + var blockAssignments = new Dictionary(); + var immediateDominator = Program.GraphFromBlocks(blocks).ImmediateDominator(); + todo.Push(blocks[0]); + while (todo.Count > 0) { + var currentBlock = todo.Pop(); + if (blockAssignments.Keys.Contains(currentBlock)) { + continue; + } + + if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. + { + blockAssignments[currentBlock] = currentBlock; + } else if (splitPoints.ContainsKey(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split + { + blockAssignments[currentBlock] = immediateDominator[currentBlock]; + } else { + Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock])); + blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]]; + } + if (currentBlock.TransferCmd is GotoCmd exit) { + exit.LabelTargets.ForEach(blk => todo.Push(blk)); + } + } + return blockAssignments; + } + + private static List SplitOnAssert(VCGenOptions options, List oldBlocks, AssertCmd assertToKeep) { + var oldToNewBlockMap = new Dictionary(oldBlocks.Count); + + var newBlocks = new List(oldBlocks.Count); + foreach (var oldBlock in oldBlocks) { + var newBlock = new Block(oldBlock.tok) { + Label = oldBlock.Label, + Cmds = oldBlock.Cmds.Select(cmd => + cmd != assertToKeep ? CommandTransformations.AssertIntoAssume(options, cmd) : cmd).ToList() + }; + oldToNewBlockMap[oldBlock] = newBlock; + newBlocks.Add(newBlock); + } + + AddBlockJumps(oldBlocks, oldToNewBlockMap); + return newBlocks; + } + private static List? DoPreAssignedManualSplit(VCGenOptions options, List blocks, + Dictionary blockAssignments, int splitNumberWithinBlock, + Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { + var newBlocks = new List(blocks.Count); // Copies of the original blocks + //var duplicator = new Duplicator(); + var assertionCount = 0; + var oldToNewBlockMap = new Dictionary(blocks.Count); // Maps original blocks to their new copies in newBlocks + foreach (var currentBlock in blocks) { + var newBlock = new Block(currentBlock.tok) + { + Label = currentBlock.Label + }; + + oldToNewBlockMap[currentBlock] = newBlock; + newBlocks.Add(newBlock); + if (currentBlock == containingBlock) + { + newBlock.Cmds = GetCommandsForBlockWithSplit(currentBlock); + } else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) + { + newBlock.Cmds = GetCommandsForBlockImmediatelyDominatedBySplit(currentBlock); + } else { + newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); + } + } + + if (assertionCount == 0) + { + return null; + } + + // Patch the edges between the new blocks + AddBlockJumps(blocks, oldToNewBlockMap); + return newBlocks; + + List GetCommandsForBlockWithSplit(Block currentBlock) + { + var newCmds = new List(); + var splitCount = -1; + var verify = splitCount == splitNumberWithinBlock; + foreach (Cmd command in currentBlock.Cmds) { + if (ShouldSplitHere(command, splitOnEveryAssert)) { + splitCount++; + verify = splitCount == splitNumberWithinBlock; + } + + if (verify && BlockTransformations.IsNonTrivialAssert(command)) + { + assertionCount++; + } + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); + } + + return newCmds; + } + + List GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock) + { + var verify = true; + var newCmds = new List(); + foreach (var command in currentBlock.Cmds) { + verify = !ShouldSplitHere(command, splitOnEveryAssert) && verify; + if (verify && BlockTransformations.IsNonTrivialAssert(command)) + { + assertionCount++; + } + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); + } + + return newCmds; + } + } + + private static void AddBlockJumps(List oldBlocks, Dictionary oldToNewBlockMap) + { + foreach (var oldBlock in oldBlocks) { + var newBlock = oldToNewBlockMap[oldBlock]; + if (oldBlock.TransferCmd is ReturnCmd returnCmd) { + ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok; + continue; + } + + var gotoCmd = (GotoCmd)oldBlock.TransferCmd; + var newLabelTargets = new List(gotoCmd.LabelTargets.Count()); + var newLabelNames = new List(gotoCmd.LabelTargets.Count()); + foreach (var target in gotoCmd.LabelTargets) { + newLabelTargets.Add(oldToNewBlockMap[target]); + newLabelNames.Add(oldToNewBlockMap[target].Label); + } + + oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); + } + } +} \ No newline at end of file diff --git a/Source/VCGeneration/Prune/DependencyEvaluator.cs b/Source/VCGeneration/Prune/DependencyEvaluator.cs index 8999f8e65..85da548a6 100644 --- a/Source/VCGeneration/Prune/DependencyEvaluator.cs +++ b/Source/VCGeneration/Prune/DependencyEvaluator.cs @@ -26,7 +26,7 @@ public class DependencyEvaluator : ReadOnlyVisitor protected void AddIncoming(Declaration newIncoming) { - if (declaration.Attributes.FindBoolAttribute("include_dep")) { + if (QKeyValue.FindBoolAttribute(declaration.Attributes, "include_dep")) { incomingSets.Add(new[] { newIncoming }); } } diff --git a/Source/VCGeneration/Prune/Pruner.cs b/Source/VCGeneration/Prune/Pruner.cs index 39d479405..165eb5239 100644 --- a/Source/VCGeneration/Prune/Pruner.cs +++ b/Source/VCGeneration/Prune/Pruner.cs @@ -71,7 +71,7 @@ public static IEnumerable GetLiveDeclarations(VCGenOptions options, blocksVisitor.Visit(block); } - var keepRoots = program.TopLevelDeclarations.Where(d => d.Attributes.FindBoolAttribute("keep")); + var keepRoots = program.TopLevelDeclarations.Where(d => QKeyValue.FindBoolAttribute(d.Attributes, "keep")); var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, blocksVisitor.Outgoing.Concat(keepRoots).ToHashSet(), TraverseDeclaration).ToHashSet(); return program.TopLevelDeclarations.Where(d => diff --git a/Source/VCGeneration/Counterexample/ReturnCounterexample.cs b/Source/VCGeneration/ReturnCounterexample.cs similarity index 85% rename from Source/VCGeneration/Counterexample/ReturnCounterexample.cs rename to Source/VCGeneration/ReturnCounterexample.cs index 98092c946..526ee4959 100644 --- a/Source/VCGeneration/Counterexample/ReturnCounterexample.cs +++ b/Source/VCGeneration/ReturnCounterexample.cs @@ -7,7 +7,8 @@ namespace Microsoft.Boogie; public class ReturnCounterexample : Counterexample { public TransferCmd FailingReturn; - public readonly Ensures FailingEnsures; + public Ensures FailingEnsures; + public AssertEnsuresCmd FailingFailingAssert; [ContractInvariantMethod] void ObjectInvariant() @@ -20,7 +21,7 @@ void ObjectInvariant() public ReturnCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertEnsuresCmd failingAssertEnsures, TransferCmd failingReturn, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertEnsures) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) { var failingEnsures = failingAssertEnsures.Ensures; Contract.Requires(trace != null); @@ -30,6 +31,7 @@ public ReturnCounterexample(VCGenOptions options, List trace, List /// Returns the checksum of the corresponding assertion. @@ -49,7 +51,7 @@ public override int GetLocation() public override Counterexample Clone() { - var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, (AssertEnsuresCmd)FailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); + var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 350567ebb..3f49e5207 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -242,7 +242,7 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s foreach (Cmd cmd in seq) { AssertCmd assrt = cmd as AssertCmd; - if (assrt != null && assrt.Attributes.FindBoolAttribute("PossiblyUnreachable")) + if (assrt != null && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable")) { return false; } diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Split.cs similarity index 96% rename from Source/VCGeneration/Splits/Split.cs rename to Source/VCGeneration/Split.cs index d34affb12..3eac0cb51 100644 --- a/Source/VCGeneration/Splits/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -10,7 +10,6 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; using System.Threading.Tasks; -using VCGeneration; namespace VC { @@ -56,6 +55,8 @@ public IReadOnlyList PrunedDeclarations { int assertionCount; double assertionCost; // without multiplication by paths + public Dictionary GotoCmdOrigins { get; } + public readonly VerificationConditionGenerator /*!*/ parent; @@ -75,11 +76,14 @@ public readonly VerificationConditionGenerator /*!*/ public VerificationConditionGenerator.ErrorReporter reporter; public Split(VCGenOptions options, Func> /*!*/ getBlocks, - VerificationConditionGenerator /*!*/ parent, ImplementationRun run, int? randomSeed = null) + Dictionary /*!*/ gotoCmdOrigins, + VerificationConditionGenerator /*!*/ par, ImplementationRun run, int? randomSeed = null) { - Contract.Requires(parent != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Requires(par != null); this.getBlocks = getBlocks; - this.parent = parent; + this.GotoCmdOrigins = gotoCmdOrigins; + parent = par; this.Run = run; this.Options = options; Interlocked.Increment(ref currentId); @@ -87,26 +91,17 @@ public Split(VCGenOptions options, Func> /*!*/ getBlocks, RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0; randomGen = new Random(RandomSeed); } - - private void PrintSplit() { + + public void PrintSplit() { if (Options.PrintSplitFile == null) { return; } - - var printToConsole = Options.PrintSplitFile == "-"; - if (printToConsole) { - Thread.Sleep(100); - } - var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : ""; - var name = Implementation.Name + prefix; - using var writer = printToConsole - ? new TokenTextWriter("", Options.OutputWriter, false, Options.PrettyPrint, Options) - : new TokenTextWriter( - $"{Options.PrintSplitFile}-{Util.EscapeFilename(name)}.spl", false, - Options.PrettyPrint, Options); + using var writer = new TokenTextWriter( + $"{Options.PrintSplitFile}-{Util.EscapeFilename(Implementation.Name)}-{SplitIndex}.spl", false, + Options.PrettyPrint, Options); - Implementation.EmitImplementation(writer, 0, Blocks, false, prefix); + Implementation.EmitImplementation(writer, 0, Blocks, false); PrintSplitDeclarations(writer); } @@ -659,6 +654,7 @@ private Split DoSplit() copies.Clear(); CloneBlock(Blocks[0]); var newBlocks = new List(); + var newGotoCmdOrigins = new Dictionary(); foreach (var block in Blocks) { Contract.Assert(block != null); @@ -668,6 +664,10 @@ private Split DoSplit() } newBlocks.Add(cce.NonNull(tmp)); + if (GotoCmdOrigins.TryGetValue(block.TransferCmd, out var origin)) + { + newGotoCmdOrigins[tmp.TransferCmd] = origin; + } foreach (var predecessor in block.Predecessors) { @@ -679,7 +679,7 @@ private Split DoSplit() } } - return new Split(Options, () => newBlocks, parent, Run); + return new Split(Options, () => newBlocks, newGotoCmdOrigins, parent, Run); } private Split SplitAt(int idx) @@ -951,7 +951,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VerificationConditionGenerator.ErrorReporter(Options, absyIds, + reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } diff --git a/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs similarity index 97% rename from Source/VCGeneration/Splits/SplitAndVerifyWorker.cs rename to Source/VCGeneration/SplitAndVerifyWorker.cs index 57f3bfb33..a42723458 100644 --- a/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -39,7 +39,8 @@ public SplitAndVerifyWorker( Program program, VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, - ImplementationRun run, + ImplementationRun run, + Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, VcOutcome vcOutcome) @@ -65,8 +66,7 @@ public SplitAndVerifyWorker( ResetPredecessors(Implementation.Blocks); - ManualSplits = ManualSplitFinder.GetParts(options, run, - (token, blocks) => new ManualSplit(options, () => blocks, verificationConditionGenerator, run, token)).ToList(); + ManualSplits = ManualSplitFinder.FocusAndSplit(program, options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); if (ManualSplits.Count == 1 && maxSplits > 1) { diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs deleted file mode 100644 index dc93dab28..000000000 --- a/Source/VCGeneration/Splits/BlockRewriter.cs +++ /dev/null @@ -1,136 +0,0 @@ -#nullable enable -using System; -using System.Collections.Generic; -using System.Collections.Immutable; -using System.Linq; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; -using VC; - -namespace VCGeneration.Splits; - -public class BlockRewriter { - private readonly Dictionary assumedAssertions = new(); - private readonly IReadOnlyList reversedBlocks; - public List OrderedBlocks { get; } - public VCGenOptions Options { get; } - public Graph Dag { get; } - public Func, ManualSplit> CreateSplit { get; } - - public BlockRewriter(VCGenOptions options, List blocks, - Func, ManualSplit> createSplit) { - this.Options = options; - CreateSplit = createSplit; - Dag = Program.GraphFromBlocks(blocks); - OrderedBlocks = Dag.TopologicalSort(); - reversedBlocks = OrderedBlocks.Reversed(); - } - - public Cmd TransformAssertCmd(Cmd cmd) { - if (cmd is AssertCmd assertCmd) { - return assumedAssertions.GetOrCreate(assertCmd, - () => VerificationConditionGenerator.AssertTurnedIntoAssume(Options, assertCmd)); - } - - 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 - }); - } - - blockToVisit.Push(path.Push(newPrevious)); - } - - 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 }); - } - } - } - - public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( - ISet blocksToInclude, - ISet freeAssumeBlocks) { - return ComputeNewBlocks(blocksToInclude, block => - freeAssumeBlocks.Contains(block) - ? block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(Options, c)).ToList() - : block.Cmds); - } - - public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( - ISet? blocksToInclude, - Func> getCommands) - { - var newBlocks = new List(); - var oldToNewBlockMap = new Dictionary(reversedBlocks.Count); - - // Traverse backwards to allow settings the jumps to the new blocks - foreach (var block in reversedBlocks) - { - if (blocksToInclude != null && !blocksToInclude.Contains(block)) { - continue; - } - - 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(); - newBlock.TransferCmd = new GotoCmd(gtc.tok, - targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), - targets.Select(blk => oldToNewBlockMap[blk]).ToList()); - } - } - newBlocks.Reverse(); - - BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); - return (newBlocks, oldToNewBlockMap); - } - - - public static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) - { - return splitOnEveryAssert || isolateAttribute != null; - } -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs deleted file mode 100644 index 812d80407..000000000 --- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs +++ /dev/null @@ -1,116 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Collections.Immutable; -using System.Linq; -using Microsoft.Boogie; -using VC; -using VCGeneration.Splits; -using Block = Microsoft.Boogie.Block; -using Cmd = Microsoft.Boogie.Cmd; -using PredicateCmd = Microsoft.Boogie.PredicateCmd; -using QKeyValue = Microsoft.Boogie.QKeyValue; - -namespace VCGeneration; - -public class FocusAttributeHandler { - - /// - /// Each focus block creates two options. - /// We recurse twice for each focus, leading to potentially 2^N splits - /// - public static List GetParts(VCGenOptions options, ImplementationRun run, - Func, ManualSplit> createPart) - { - var rewriter = new BlockRewriter(options, run.Implementation.Blocks, createPart); - - var implementation = run.Implementation; - var dag = rewriter.Dag; - - // 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 focusBlocks = GetFocusBlocks(rewriter.OrderedBlocks); - if (rewriter.Options.RelaxFocus) { - focusBlocks.Reverse(); - } - if (!focusBlocks.Any()) { - return new List { rewriter.CreateSplit(new ImplementationRootOrigin(run.Implementation), implementation.Blocks) }; - } - - var ancestorsPerBlock = new Dictionary>(); - var descendantsPerBlock = new Dictionary>(); - focusBlocks.ForEach(fb => { - var reachables = dag.ComputeReachability(fb.Block, false).ToHashSet(); - reachables.Remove(fb.Block); - ancestorsPerBlock[fb.Block] = reachables; - }); - focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block).ToHashSet()); - var result = new List(); - - AddSplitsFromIndex(ImmutableStack.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet.Empty); - return result; - - void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet blocksToInclude, ISet freeAssumeBlocks) { - var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count; - if (allFocusBlocksHaveBeenProcessed) { - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks); - IImplementationPartOrigin token = path.Any() - ? new PathOrigin(run.Implementation.tok, path.ToList()) // TODO fix - : new ImplementationRootOrigin(run.Implementation); - result.Add(rewriter.CreateSplit(token, newBlocks)); - } else { - var (focusBlock, nextToken) = focusBlocks[focusIndex]; // assert b in blocks - if (!blocksToInclude.Contains(focusBlock) || freeAssumeBlocks.Contains(focusBlock)) - { - // This focus block can not be reached in our current path, so we ignore it by continuing - AddSplitsFromIndex(path, focusIndex + 1, blocksToInclude, freeAssumeBlocks); - } - else - { - var dominatedBlocks = 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, - blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToHashSet(), freeAssumeBlocks); - var ancestors = ancestorsPerBlock[focusBlock]; - var descendants = descendantsPerBlock[focusBlock]; - - // Recursive call that does focus the block - // Contains all the ancestors, the focus block, and the descendants. - AddSplitsFromIndex(path.Push(focusBlock), 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. - Select(block => (Block: block, FocusCommand: block.Cmds.FirstOrDefault(IsFocusCmd)?.tok)). - Where(t => t.FocusCommand != null).ToList(); - } - - private static bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && p.Attributes.FindBoolAttribute("focus"); - } -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs deleted file mode 100644 index 1d90a36e0..000000000 --- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs +++ /dev/null @@ -1,106 +0,0 @@ -#nullable enable -using System; -using System.Collections.Generic; -using System.Collections.Immutable; -using System.Linq; -using Microsoft.Boogie; -using VC; -using VCGeneration.Splits; - -namespace VCGeneration; - -class IsolateAttributeOnAssertsHandler { - - public static (List IsolatedParts, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, - Func, ManualSplit> createPart) { - var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); - - var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; - partToDivide.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); - - var isolatedAssertions = new HashSet(); - var results = new List(); - - foreach (var b in partToDivide.Blocks) { - b.Predecessors.Clear(); - } - Implementation.ComputePredecessorsForBlocks(partToDivide.Blocks); - foreach (var block in partToDivide.Blocks) { - foreach (var assert in block.Cmds.OfType()) { - var attributes = assert.Attributes; - var isolateAttribute = QKeyValue.FindAttribute(attributes, p => p.Key == "isolate"); - if (!BlockRewriter.ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { - continue; - } - - 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 newAssertBlock = p.Blocks.Last(); - newAssertBlock.Cmds = GetCommandsForBlockWithAssert(newAssertBlock, assert); - return p; - })); - } else { - results.Add(GetSplitForIsolatedAssertion(block, assert)); - } - } - } - - if (!results.Any()) { - return (results,partToDivide); - } - - return (results,GetSplitWithoutIsolatedAssertions()); - - ManualSplit GetSplitForIsolatedAssertion(Block blockWithAssert, AssertCmd assertCmd) { - var blocksToKeep = rewriter.Dag.ComputeReachability(blockWithAssert, false); - - List GetCommands(Block oldBlock) => - oldBlock == blockWithAssert - ? GetCommandsForBlockWithAssert(oldBlock, assertCmd) - : oldBlock.Cmds.Select(rewriter.TransformAssertCmd).ToList(); - - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToKeep, GetCommands); - return rewriter.CreateSplit(new IsolatedAssertionOrigin(assertCmd), newBlocks); - } - - List GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert) - { - var result = new List(); - foreach (var command in currentBlock.Cmds) { - if (assert == command) { - result.Add(command); - break; - } - result.Add(rewriter.TransformAssertCmd(command)); - } - - return result; - } - - ManualSplit GetSplitWithoutIsolatedAssertions() { - var origin = new ImplementationRootOrigin(partToDivide.Implementation); - if (!isolatedAssertions.Any()) { - return rewriter.CreateSplit(origin, partToDivide.Blocks); - } - - var (newBlocks, mapping) = rewriter.ComputeNewBlocks(null, GetCommands); - - return rewriter.CreateSplit(origin, newBlocks); - - List GetCommands(Block block) => block.Cmds.Select(cmd => - isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList(); - } - } -} - - -public class IsolatedAssertionOrigin : TokenWrapper, IImplementationPartOrigin { - public AssertCmd IsolatedAssert { get; } - - public IsolatedAssertionOrigin(AssertCmd isolatedAssert) : base(isolatedAssert.tok) { - this.IsolatedAssert = isolatedAssert; - } - - public string ShortName => $"/assert@{IsolatedAssert.Line}"; -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs deleted file mode 100644 index 5f7c1de04..000000000 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ /dev/null @@ -1,87 +0,0 @@ -#nullable enable -using System; -using System.Collections.Generic; -using System.Collections.Immutable; -using System.Diagnostics; -using System.Linq; -using Microsoft.Boogie; -using VC; -using VCGeneration.Splits; -using VCGeneration.Transformations; - -namespace VCGeneration; - -class IsolateAttributeOnJumpsHandler { - public static (List Isolated, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, - Func, ManualSplit> createPart) { - - var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); - - var results = new List(); - var blocks = partToDivide.Blocks; - var dag = Program.GraphFromBlocks(blocks); - - var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; - partToDivide.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); - - var isolatedBlocks = new HashSet(); - - foreach (var block in partToDivide.Blocks) { - if (block.TransferCmd is not GotoCmd gotoCmd) { - continue; - } - - var isTypeOfAssert = gotoCmd.tok is GotoFromReturn; - var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate"); - var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); - if (!isolate) { - continue; - } - - isolatedBlocks.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; - 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); - results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, originalReturn.tok)); - } else { - var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, ancestors.ToHashSet()); - results.Add(rewriter.CreateSplit(new ReturnOrigin(originalReturn), newBlocks)); - } - } - - if (!results.Any()) { - return (results,partToDivide); - } - - return (results, GetPartWithoutIsolatedReturns()); - - ManualSplit GetPartWithoutIsolatedReturns() { - var (newBlocks, mapping) = rewriter.ComputeNewBlocks(blocks.ToHashSet(), new HashSet()); - foreach (var (oldBlock, newBlock) in mapping) { - if (isolatedBlocks.Contains(oldBlock)) { - newBlock.TransferCmd = new ReturnCmd(Token.NoToken); - } - } - BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); - return rewriter.CreateSplit(new ImplementationRootOrigin(partToDivide.Implementation), - newBlocks); - } - } -} - - -public class ReturnOrigin : TokenWrapper, IImplementationPartOrigin { - public ReturnCmd IsolatedReturn { get; } - - public ReturnOrigin(ReturnCmd isolatedReturn) : base(isolatedReturn.tok) { - this.IsolatedReturn = isolatedReturn; - } - - public string ShortName => $"/return@{IsolatedReturn.Line}"; -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs deleted file mode 100644 index b1b8e676b..000000000 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ /dev/null @@ -1,33 +0,0 @@ -#nullable enable -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Boogie; -using VC; - -namespace VCGeneration; - - -public static class ManualSplitFinder { - - public static IEnumerable GetParts(VCGenOptions options, ImplementationRun run, - Func, ManualSplit> createPart) { - - var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart); - var result = focussedParts.SelectMany(focussedPart => { - var (isolatedJumps, withoutIsolatedJumps) = - IsolateAttributeOnJumpsHandler.GetParts(options, focussedPart, createPart); - var (isolatedAssertions, withoutIsolatedAssertions) = - IsolateAttributeOnAssertsHandler.GetParts(options, withoutIsolatedJumps, createPart); - - var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); - var splits = isolatedJumps.Concat(isolatedAssertions).Concat(splitParts).Where(s => s.Asserts.Any()).ToList(); - return splits.Any() ? splits : new List { focussedPart }; - }); - return result; - } -} - -public interface IImplementationPartOrigin : IToken { - string ShortName { get; } -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/PathToken.cs b/Source/VCGeneration/Splits/PathToken.cs deleted file mode 100644 index b0dabe1cd..000000000 --- a/Source/VCGeneration/Splits/PathToken.cs +++ /dev/null @@ -1,27 +0,0 @@ -#nullable enable -using System.Collections.Generic; -using System.Collections.Immutable; -using System.IO; -using System.Linq; -using Microsoft.Boogie; -using Microsoft.Boogie.GraphUtil; - -namespace VCGeneration; - -public class PathOrigin : TokenWrapper, IImplementationPartOrigin { - - public PathOrigin(IToken inner, List branches) : base(inner) { - Branches = branches; - } - - public List Branches { get; } - public string ShortName => $"/assert@{line}[{string.Join(",", Branches.Select(b => b.tok.line))}]"; -} - -class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin { - public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok) - { - } - - public string ShortName => ""; -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs deleted file mode 100644 index 8adb35a41..000000000 --- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs +++ /dev/null @@ -1,216 +0,0 @@ -#nullable enable -using System; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Linq; -using Microsoft.Boogie; -using VC; - -namespace VCGeneration; - -class SplitAttributeHandler { - - public static List GetParts(ManualSplit partToSplit) { - var splitsPerBlock = new Dictionary>(); - var splits = new HashSet(); - foreach (var block in partToSplit.Blocks) { - var splitsForThisBlock = new List(); - foreach (var command in block.Cmds) { - if (!ShouldSplitHere(command)) { - continue; - } - - splits.Add(command); - splitsForThisBlock.Add(command); - } - - if (splitsForThisBlock.Any()) { - splitsPerBlock[block] = splitsForThisBlock; - } - } - - if (!splits.Any()) { - return new List { partToSplit }; - } - - var vcs = new List(); - var entryPoint = partToSplit.Blocks[0]; - var blockStartToSplit = GetMapFromBlockStartToSplit(partToSplit.Blocks, splitsPerBlock); - - var beforeSplitsVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, blockStartToSplit, - entryPoint, splits, null); - if (beforeSplitsVc != null) - { - vcs.Add(beforeSplitsVc); - } - foreach (var block in partToSplit.Blocks) { - var splitsForBlock = splitsPerBlock.GetValueOrDefault(block); - if (splitsForBlock == null) { - continue; - } - - foreach (var split in splitsForBlock) - { - var splitVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, - blockStartToSplit, block, splits, split); - if (splitVc != null) - { - vcs.Add(splitVc); - } - } - } - return vcs; - - ManualSplit CreateVc(IImplementationPartOrigin token, List blocks) { - return new ManualSplit(partToSplit.Options, () => { - BlockTransformations.Optimize(blocks); - return blocks; - }, partToSplit.parent, partToSplit.Run, token); - } - } - - private static bool ShouldSplitHere(Cmd c) { - if (c is not PredicateCmd predicateCmd) { - return false; - } - - return predicateCmd.Attributes.FindBoolAttribute("split_here"); - } - - private static Dictionary GetMapFromBlockStartToSplit(List blocks, Dictionary> splitsPerBlock) { - var todo = new Stack(); - var blockAssignments = new Dictionary(); - var immediateDominators = Program.GraphFromBlocks(blocks).ImmediateDominator(); - todo.Push(blocks[0]); - while (todo.Count > 0) { - var currentBlock = todo.Pop(); - if (blockAssignments.Keys.Contains(currentBlock)) { - continue; - } - - if (!immediateDominators.TryGetValue(currentBlock, out var immediateDominator)) - { - blockAssignments[currentBlock] = null; - } - else if (splitsPerBlock.TryGetValue(immediateDominator, out var splitsForDominator)) // if the currentBlock's dominator has a split then it will be associated with that split - { - blockAssignments[currentBlock] = splitsForDominator.Last(); - } - else { - Contract.Assert(blockAssignments.Keys.Contains(immediateDominator)); - blockAssignments[currentBlock] = blockAssignments[immediateDominator]; - } - - if (currentBlock.TransferCmd is GotoCmd gotoCmd) { - gotoCmd.LabelTargets.ForEach(block => todo.Push(block)); - } - } - return blockAssignments; - } - - private static ManualSplit? GetImplementationPartAfterSplit(Func, ManualSplit> createVc, - ManualSplit partToSplit, - Dictionary blockStartToSplit, Block blockWithSplit, - HashSet splits, Cmd? split) - { - var assertionCount = 0; - - var newBlocks = UpdateBlocks(partToSplit.Blocks, currentBlock => { - if (currentBlock == blockWithSplit) { - return GetCommandsForBlockWithSplit(currentBlock); - } - - if (blockStartToSplit[currentBlock] == split) { - return GetCommandsForBlockImmediatelyDominatedBySplit(currentBlock); - } - - return currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(partToSplit.Options, x)).ToList(); - }); - - if (assertionCount == 0) { - return null; - } - - return createVc(new SplitOrigin(split?.tok ?? partToSplit.Token), newBlocks); - - List GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock) - { - var verify = true; - var newCmds = new List(); - foreach (var command in currentBlock.Cmds) { - verify &= !splits.Contains(command); - if (verify && BlockTransformations.IsNonTrivialAssert(command)) - { - assertionCount++; - } - newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(partToSplit.Options, command)); - } - - return newCmds; - } - - List GetCommandsForBlockWithSplit(Block currentBlock) - { - var newCmds = new List(); - var verify = false; - foreach (var command in currentBlock.Cmds) { - if (splits.Contains(command)) { - verify = command == split; - } - - if (verify && BlockTransformations.IsNonTrivialAssert(command)) - { - assertionCount++; - } - newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(partToSplit.Options, command)); - } - - return newCmds; - } - } - - private static List UpdateBlocks(IReadOnlyList blocks, - Func> getCommands) - { - var newBlocks = new List(blocks.Count); - var oldToNewBlockMap = new Dictionary(newBlocks.Count); - foreach (var currentBlock in blocks) { - var newBlock = Block.ShallowClone(currentBlock); - - oldToNewBlockMap[currentBlock] = newBlock; - newBlocks.Add(newBlock); - newBlock.Cmds = getCommands(currentBlock); - } - - AddJumpsToNewBlocks(oldToNewBlockMap); - return newBlocks; - } - - private static void AddJumpsToNewBlocks(Dictionary oldToNewBlockMap) - { - foreach (var (oldBlock, newBlock) in oldToNewBlockMap) { - if (oldBlock.TransferCmd is ReturnCmd returnCmd) { - ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok; - continue; - } - - var gotoCmd = (GotoCmd)oldBlock.TransferCmd; - var newLabelTargets = new List(gotoCmd.LabelTargets.Count); - var newLabelNames = new List(gotoCmd.LabelTargets.Count); - foreach (var target in gotoCmd.LabelTargets) { - newLabelTargets.Add(oldToNewBlockMap[target]); - newLabelNames.Add(oldToNewBlockMap[target].Label); - } - - oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); - } - } -} - -class SplitOrigin : TokenWrapper, IImplementationPartOrigin { - public SplitOrigin(IToken inner) : base(inner) - { - } - - public string ShortName => $"/split@{line}"; -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/TokenWrapper.cs b/Source/VCGeneration/Splits/TokenWrapper.cs deleted file mode 100644 index d7ea8427d..000000000 --- a/Source/VCGeneration/Splits/TokenWrapper.cs +++ /dev/null @@ -1,48 +0,0 @@ -#nullable enable -using Microsoft.Boogie; - -namespace VCGeneration; - -public class TokenWrapper : IToken { - public IToken Inner { get; } - - public TokenWrapper(IToken inner) { - this.Inner = inner; - } - - public int CompareTo(IToken? other) { - return Inner.CompareTo(other); - } - - public int kind { - get => Inner.kind; - set => Inner.kind = value; - } - - public string filename { - get => Inner.filename; - set => Inner.filename = value; - } - - public int pos { - get => Inner.pos; - set => Inner.pos = value; - } - - public int col { - get => Inner.col; - set => Inner.col = value; - } - - public int line { - get => Inner.line; - set => Inner.line = value; - } - - public string val { - get => Inner.val; - set => Inner.val = value; - } - - public bool IsValid => Inner.IsValid; -} \ No newline at end of file diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs index 90ab89089..4362273a6 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -1,70 +1,84 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; -using System.Linq; using Microsoft.Boogie; using VC; namespace VCGeneration.Transformations; public static class DesugarReturns { - public static Block GenerateUnifiedExit(Implementation impl) - { - Contract.Requires(impl != null); - Contract.Ensures(Contract.Result() != null); + public static Block GenerateUnifiedExit(Implementation impl, out Dictionary gotoCmdOrigins) + { + Contract.Requires(impl != null); + Contract.Requires(gotoCmdOrigins != null); + Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); - Block exitBlock = null; + gotoCmdOrigins = new(); + Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); + Block exitBlock = null; - int returnBlocks = 0; - foreach (var block in impl.Blocks.Where(block => block.TransferCmd is ReturnCmd)) - { - exitBlock = block; - returnBlocks++; - } + #region Create a unified exit block, if there's more than one - if (returnBlocks > 1) - { - string unifiedExitLabel = "GeneratedUnifiedExit"; - 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) { - if (block.TransferCmd is not ReturnCmd returnCmd) { - continue; + { + int returnBlocks = 0; + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd) + { + exitBlock = b; + returnBlocks++; + } + } + + if (returnBlocks > 1) + { + string unifiedExitLabel = "GeneratedUnifiedExit"; + var unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), + new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); + Contract.Assert(unifiedExit != null); + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd returnCmd) + { + List labels = new List(); + labels.Add(unifiedExitLabel); + List bs = new List(); + bs.Add(unifiedExit); + GotoCmd go = new GotoCmd(returnCmd.tok, labels, bs); + gotoCmdOrigins[go] = returnCmd; + b.TransferCmd = go; + unifiedExit.Predecessors.Add(b); + } + } + + exitBlock = unifiedExit; + impl.Blocks.Add(unifiedExit); } - var gotoLabels = new List { unifiedExitLabel }; - var gotoTargets = new List { unifiedExit }; - var gotoCmd = new GotoCmd(new GotoFromReturn(returnCmd), gotoLabels, gotoTargets) { - Attributes = returnCmd.Attributes - }; - block.TransferCmd = gotoCmd; - unifiedExit.Predecessors.Add(block); + Contract.Assert(exitBlock != null); } + return exitBlock; - exitBlock = unifiedExit; - impl.Blocks.Add(unifiedExit); + #endregion } - - Contract.Assert(exitBlock != null); - return exitBlock; - } - - /// - /// Modifies an implementation by inserting all postconditions - /// as assert statements at the end of the implementation - /// Returns the possibly-new unified exit block of the implementation - /// - /// The unified exit block that has - /// already been constructed for the implementation (and so - /// is already an element of impl.Blocks) - /// - public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock) + + /// + /// Modifies an implementation by inserting all postconditions + /// as assert statements at the end of the implementation + /// Returns the possibly-new unified exit block of the implementation + /// + /// + /// The unified exit block that has + /// already been constructed for the implementation (and so + /// is already an element of impl.Blocks) + /// + public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, + Dictionary gotoCmdOrigins) { var impl = run.Implementation; Contract.Requires(impl != null); Contract.Requires(unifiedExitBlock != null); + Contract.Requires(gotoCmdOrigins != null); Contract.Requires(impl.Proc != null); Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); @@ -75,7 +89,7 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun debugWriter.WriteLine("Effective postcondition:"); } - var formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); + Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); // (free and checked) ensures clauses foreach (Ensures ens in impl.Proc.Ensures) @@ -84,18 +98,18 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun if (!ens.Free) { - var ensuresCopy = (Ensures) cce.NonNull(ens.Clone()); - ensuresCopy.Condition = Substituter.Apply(formalProcImplSubst, ens.Condition); - AssertEnsuresCmd assert = new AssertEnsuresCmd(ensuresCopy) { - ErrorDataEnhanced = ensuresCopy.ErrorDataEnhanced - }; + Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); + Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); + ensCopy.Condition = e; + AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); + c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; // Copy any {:id ...} from the postcondition to the assumption, so // we can track it while analyzing verification coverage. - assert.CopyIdFrom(ens.tok, ens); - unifiedExitBlock.Cmds.Add(assert); + c.CopyIdFrom(ens.tok, ens); + unifiedExitBlock.Cmds.Add(c); if (debugWriter != null) { - assert.Emit(debugWriter, 1); + c.Emit(debugWriter, 1); } } else if (ens.CanAlwaysAssume()) @@ -114,12 +128,4 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun debugWriter.WriteLine(); } } -} - -class GotoFromReturn : TokenWrapper { - public ReturnCmd Origin { get; } - - public GotoFromReturn(ReturnCmd origin) : base(origin.tok) { - this.Origin = origin; - } } \ No newline at end of file diff --git a/Source/VCGeneration/Transformations/RemoveBackEdges.cs b/Source/VCGeneration/Transformations/RemoveBackEdges.cs index f9233af03..731f7a1e5 100644 --- a/Source/VCGeneration/Transformations/RemoveBackEdges.cs +++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs @@ -9,7 +9,7 @@ namespace VCGeneration.Transformations; public class RemoveBackEdges { - private readonly VerificationConditionGenerator generator; + private VerificationConditionGenerator generator; public RemoveBackEdges(VerificationConditionGenerator generator) { this.generator = generator; @@ -48,7 +48,7 @@ public void ConvertCfg2Dag(ImplementationRun run, Dictionary> // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges // below assumes that the start node has no predecessor) impl.Blocks.Insert(0, - new Block(Token.NoToken, "0", new List(), + new Block(new Token(-17, -4), "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ConditionGeneration.ResetPredecessors(impl.Blocks); @@ -206,7 +206,14 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary GotoCmdOrigins { get; set; } public ModelViewInfo ModelViewInfo { get; set; } } @@ -113,7 +114,7 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(traceWriter, codeExpr.Blocks, new List(), new ModelViewInfo(codeExpr), debugInfos); VCExpr startCorrect = vcgen.LetVC(codeExpr.Blocks, null, absyIds, ctx, out var ac, isPositiveContext); VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect); @@ -326,7 +327,7 @@ void ExpandAsserts(Implementation impl) attr = ae.Ensures.Attributes; } - if (QKeyValue.FindExprAttribute(attr, "expand") != null || attr.FindBoolAttribute("expand")) + if (QKeyValue.FindExprAttribute(attr, "expand") != null || QKeyValue.FindBoolAttribute(attr, "expand")) { int depth = QKeyValue.FindIntAttribute(attr, "expand", 100); Func fe = e => Expr.Or(a.Expr, e); @@ -379,7 +380,7 @@ public override async Task VerifyImplementation(ImplementationRun run callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0); - PrepareImplementation(run, callback, out var smokeTester, out var dataModelViewInfo); + PrepareImplementation(run, callback, out var smokeTester, out var dataGotoCmdOrigins, out var dataModelViewInfo); VcOutcome vcOutcome = VcOutcome.Correct; @@ -399,14 +400,15 @@ public override async Task VerifyImplementation(ImplementationRun run else { // If possible, we use the old counterexample, but with the location information of "a" - var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0]); + var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0], + dataGotoCmdOrigins); callback.OnCounterexample(cex, null); } } } } - var worker = new SplitAndVerifyWorker(program, Options, this, run, callback, + var worker = new SplitAndVerifyWorker(program, Options, this, run, dataGotoCmdOrigins, callback, dataModelViewInfo, vcOutcome); vcOutcome = await worker.WorkUntilDone(cancellationToken); @@ -425,6 +427,7 @@ public override async Task VerifyImplementation(ImplementationRun run public void PrepareImplementation(ImplementationRun run, VerifierCallback callback, out SmokeTester smokeTester, + out Dictionary gotoCmdOrigins, out ModelViewInfo modelViewInfo) { var data = implementationData.GetOrCreateValue(run.Implementation)!; @@ -444,7 +447,7 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba if (!data.Passified) { data.Passified = true; - PassifyImpl(run, out modelViewInfo); + data.GotoCmdOrigins = gotoCmdOrigins = PassifyImpl(run, out modelViewInfo); data.ModelViewInfo = modelViewInfo; ExpandAsserts(run.Implementation); @@ -463,6 +466,7 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba else { modelViewInfo = data.ModelViewInfo; + gotoCmdOrigins = data.GotoCmdOrigins; } } @@ -471,6 +475,7 @@ public class ErrorReporter : ProverInterface.ErrorHandler { private ProofRun split; private new VCGenOptions options; + Dictionary gotoCmdOrigins; ControlFlowIdMap absyIds; @@ -486,6 +491,7 @@ public class ErrorReporter : ProverInterface.ErrorHandler [ContractInvariantMethod] void ObjectInvariant() { + Contract.Invariant(gotoCmdOrigins != null); Contract.Invariant(absyIds != null); Contract.Invariant(cce.NonNullElements(blocks)); Contract.Invariant(callback != null); @@ -504,6 +510,7 @@ public override void AddCoveredElement(TrackedNodeComponent elt) } public ErrorReporter(VCGenOptions options, + Dictionary /*!*/ gotoCmdOrigins, ControlFlowIdMap /*!*/ absyIds, List /*!*/ blocks, Dictionary> debugInfos, @@ -512,11 +519,13 @@ public ErrorReporter(VCGenOptions options, ProverContext /*!*/ context, Program /*!*/ program, ProofRun split) : base(options) { + Contract.Requires(gotoCmdOrigins != null); Contract.Requires(absyIds != null); Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(callback != null); Contract.Requires(context != null); Contract.Requires(program != null); + this.gotoCmdOrigins = gotoCmdOrigins; this.absyIds = absyIds; this.blocks = blocks; this.debugInfos = debugInfos; @@ -559,7 +568,7 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, Contract.Assert(traceNodes.Contains(entryBlock)); trace.Add(entryBlock); - var newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, + Counterexample newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, debugInfos, context, split, new Dictionary()); if (newCounterexample == null) @@ -571,12 +580,15 @@ 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) { - returnExample.FailingReturn = gotoFromReturn.Origin; + Contract.Assert(block != null); + Contract.Assume(block.TransferCmd != null); + var cmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); + if (cmd != null) + { + returnExample.FailingReturn = cmd; + break; } } } @@ -648,14 +660,14 @@ public void DesugarCalls(Implementation impl) } } - public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) + public Dictionary PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) { Contract.Requires(run != null); Contract.Requires(program != null); Contract.Ensures(Contract.Result>() != null); var impl = run.Implementation; - var exitBlock = DesugarReturns.GenerateUnifiedExit(impl); + var exitBlock = DesugarReturns.GenerateUnifiedExit(impl, out var gotoCmdOrigins); #region Debug Tracing @@ -694,12 +706,12 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) if (lvar.TypedIdent.WhereExpr != null) { var exp = Expr.Binary(lvar.tok, BinaryOperator.Opcode.And, lvar.TypedIdent.WhereExpr, - Expr.Literal(true)); + LiteralExpr.Literal(true)); Cmd c = new AssumeCmd(lvar.tok, exp, new QKeyValue(lvar.tok, "where", new List(new object[] { idExp }), null)); cc.Add(c); } - else if (lvar.Attributes.FindBoolAttribute("assumption")) + else if (QKeyValue.FindBoolAttribute(lvar.Attributes, "assumption")) { cc.Add(new AssumeCmd(lvar.tok, idExp, new QKeyValue(lvar.tok, "assumption_variable_initialization", new List(), null))); @@ -710,7 +722,7 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) InjectPreconditions(Options, run, cc); // append postconditions, starting in exitBlock and continuing into other blocks, if needed - DesugarReturns.InjectPostConditions(Options, run, exitBlock); + DesugarReturns.InjectPostConditions(Options, run, exitBlock, gotoCmdOrigins); } #endregion @@ -752,7 +764,7 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) modelViewInfo = new ModelViewInfo(program, impl); Convert2PassiveCmd(run, modelViewInfo); - if (impl.Attributes.FindBoolAttribute("may_unverified_instrumentation")) + if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation")) { InstrumentWithMayUnverifiedConditions(impl, exitBlock); } @@ -784,6 +796,8 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) #endregion Peep-hole optimizations HandleSelectiveChecking(impl); + + return gotoCmdOrigins; } #region Simplified May-Unverified Analysis and Instrumentation @@ -922,13 +936,13 @@ static HashSet JoinVariableSets(HashSet c0, HashSet variables) @@ -985,8 +999,8 @@ static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet private void HandleSelectiveChecking(Implementation impl) { - if (impl.Attributes.FindBoolAttribute("selective_checking") || - impl.Proc.Attributes.FindBoolAttribute("selective_checking")) + if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") || + QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "selective_checking")) { var startPoints = new List(); foreach (var b in impl.Blocks) @@ -994,7 +1008,7 @@ private void HandleSelectiveChecking(Implementation impl) foreach (Cmd c in b.Cmds) { var p = c as PredicateCmd; - if (p != null && p.Attributes.FindBoolAttribute("start_checking_here")) + if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) { startPoints.Add(b); break; @@ -1047,7 +1061,7 @@ private void HandleSelectiveChecking(Implementation impl) foreach (Cmd c in b.Cmds) { var p = c as PredicateCmd; - if (p != null && p.Attributes.FindBoolAttribute("start_checking_here")) + if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) { copyMode = true; } @@ -1353,11 +1367,12 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, - Block implEntryBlock) + Block implEntryBlock, Dictionary gotoCmdOrigins) { Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); + Contract.Requires(gotoCmdOrigins != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; @@ -1430,7 +1445,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options { Contract.Assert(block != null); Contract.Assume(block.TransferCmd != null); - returnCmd = block.TransferCmd.tok is GotoFromReturn gotoFromReturn ? gotoFromReturn.Origin : null; + returnCmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); if (returnCmd != null) { break; diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index d5b130748..15e3a2cdb 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -28,9 +28,17 @@ public void ComputePerAssertOutcomes(out Dictionary pe if (Outcome == SolverOutcome.Valid) { perAssertOutcome = Asserts.ToDictionary(cmd => cmd, _ => SolverOutcome.Valid); } else { - foreach (var counterExample in CounterExamples) - { - var underlyingAssert = counterExample.FailingAssert; + foreach (var counterExample in CounterExamples) { + AssertCmd underlyingAssert; + if (counterExample is AssertCounterexample assertCounterexample) { + underlyingAssert = assertCounterexample.FailingAssert; + } else if (counterExample is CallCounterexample callCounterexample) { + underlyingAssert = callCounterexample.FailingFailingAssert; + } else if (counterExample is ReturnCounterexample returnCounterexample) { + underlyingAssert = returnCounterexample.FailingFailingAssert; + } else { + continue; + } // We ensure that the underlyingAssert is among the original asserts if (!Asserts.Contains(underlyingAssert)) { diff --git a/Source/VCGeneration/Counterexample/VerifierCallback.cs b/Source/VCGeneration/VerifierCallback.cs similarity index 100% rename from Source/VCGeneration/Counterexample/VerifierCallback.cs rename to Source/VCGeneration/VerifierCallback.cs diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 7857e5142..84090f10a 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -212,12 +212,12 @@ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) var assumeId = QKeyValue.FindStringAttribute(ac.Attributes, "id"); if (assumeId != null && ctxt.Options.TrackVerificationCoverage) { - var isTry = ac.Attributes.FindBoolAttribute("try"); + var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, isTry ? VCExprVarKind.Try : VCExprVarKind.Assume); expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr)); } - var soft = ac.Attributes.FindBoolAttribute("soft"); + var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); var softWeight = QKeyValue.FindIntAttribute(ac.Attributes, "soft", 0); if ((soft || 0 < softWeight) && assumeId != null) { diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl index 7f04782a6..28481b41e 100644 --- a/Test/aitest0/Issue25.bpl +++ b/Test/aitest0/Issue25.bpl @@ -7,8 +7,8 @@ axiom 0 <= N; procedure vacuous_post() ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25). { - var x: int; - x := -N; - while (x != x) { - } +var x: int; +x := -N; +while (x != x) { +} } diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect index 650e46069..de1be84d4 100644 --- a/Test/aitest0/Issue25.bpl.expect +++ b/Test/aitest0/Issue25.bpl.expect @@ -1,8 +1,8 @@ -Issue25.bpl(12,3): Error: a postcondition could not be proved on this return path +Issue25.bpl(12,1): Error: a postcondition could not be proved on this return path Issue25.bpl(8,1): Related location: this is the postcondition that could not be proved Execution trace: - Issue25.bpl(11,5): anon0 - Issue25.bpl(12,3): anon2_LoopHead - Issue25.bpl(12,3): anon2_LoopDone + Issue25.bpl(11,3): anon0 + Issue25.bpl(12,1): anon2_LoopHead + Issue25.bpl(12,1): anon2_LoopDone Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl index 50425d6e9..2e3878802 100644 --- a/Test/commandline/SplitOnEveryAssert.bpl +++ b/Test/commandline/SplitOnEveryAssert.bpl @@ -6,8 +6,8 @@ // CHECK: checking split 1/11 .* // CHECK: checking split 2/11 .* // CHECK: checking split 3/11 .* +// CHECK: --> split #3 done, \[.* s\] Invalid // CHECK: checking split 4/11 .* -// CHECK: --> split #4 done, \[.* s\] Invalid // CHECK: checking split 5/11 .* // CHECK: checking split 6/11 .* // CHECK: checking split 7/11 .* diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl deleted file mode 100644 index 59cd30f93..000000000 --- a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl +++ /dev/null @@ -1,42 +0,0 @@ -// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -procedure IsolateAssertion(x: int, y: int) -{ - var z: int; - z := 0; - if (x > 0) { - z := z + 1; - } else { - z := z + 2; - } - - if (y > 0) { - z := z + 3; - } else { - z := z + 4; - } - assert z > 1; - assert {:isolate} z > 5; - assert z > 6; -} - -procedure IsolatePathsAssertion(x: int, y: int) -{ - var z: int; - z := 0; - if (x > 0) { - z := z + 1; - } else { - z := z + 2; - } - - if (y > 0) { - z := z + 3; - } else { - z := z + 4; - } - assert z > 1; - assert {:isolate "paths"} z > 5; // fails on three out of four paths - assert z > 6; -} \ No newline at end of file diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect deleted file mode 100644 index 27589907d..000000000 --- a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect +++ /dev/null @@ -1,183 +0,0 @@ -implementation IsolateAssertion/assert@20(x: int, y: 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 anon8_Then, anon8_Else; - - anon7_Else: - assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - 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: - assume z#AT#5 > 1; - assert {:isolate} z#AT#5 > 5; - return; -} - - -implementation IsolateAssertion(x: int, y: 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 anon8_Then, anon8_Else; - - anon7_Else: - assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - 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; -} - - -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) -{ - - anon0: - assume {:partition} x > 0; - assume z#AT#0 == 0 + 1; - assume z#AT#2 == z#AT#0; - 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; - return; -} - - -implementation IsolatePathsAssertion/assert@40[31,35](x: int, y: int) -{ - - anon0: - assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - 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; - return; -} - - -implementation IsolatePathsAssertion/assert@40[29,37](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 >= 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; - return; -} - - -implementation IsolatePathsAssertion/assert@40[31,37](x: int, y: int) -{ - - anon0: - assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - 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; - return; -} - - -implementation IsolatePathsAssertion(x: int, y: 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 anon8_Then, anon8_Else; - - anon7_Else: - assume {:partition} 0 >= x; - assume z#AT#1 == 0 + 2; - assume z#AT#2 == z#AT#1; - 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; -} - - -isolateAssertion.bpl(40,3): Error: this assertion could not be proved -isolateAssertion.bpl(41,3): Error: this assertion could not be proved - -Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl b/Test/implementationDivision/isolateJump/isolateJump.bpl deleted file mode 100644 index d40ee651c..000000000 --- a/Test/implementationDivision/isolateJump/isolateJump.bpl +++ /dev/null @@ -1,38 +0,0 @@ -// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -procedure IsolateReturn(x: int, y: int) returns (r: int) - ensures r > 4; -{ - r := 0; - if (x > 0) { - r := r + 1; - } else { - r := r + 2; - } - - if (y > 0) { - r := r + 3; - return {:isolate}; - } - - r := r + 4; -} - -procedure IsolateReturnPaths(x: int, y: int) returns (r: int) - ensures r > 4; -{ - r := 0; - if (x > 0) { - r := r + 1; - } else { - r := r + 2; - } - - if (y > 0) { - r := r + 3; - return {:isolate "paths"}; - } - - r := r + 4; -} \ No newline at end of file diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect deleted file mode 100644 index 3c47dc663..000000000 --- a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect +++ /dev/null @@ -1,126 +0,0 @@ -implementation IsolateReturn/return@16(x: int, y: int) returns (r: 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; - goto GeneratedUnifiedExit; - - GeneratedUnifiedExit: - assert r#AT#5 > 4; - return; -} - - -implementation IsolateReturn(x: int, y: int) returns (r: 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_Else; - - anon6_Else: - assume {:partition} 0 >= x; - assume r#AT#1 == 0 + 2; - assume r#AT#2 == r#AT#1; - goto anon7_Else; - - anon7_Else: - 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; -} - - -isolateJump.bpl(16,21): Error: a postcondition could not be proved on this return path -isolateJump.bpl(5,3): Related location: this is the postcondition that could not be proved -implementation IsolateReturnPaths/assert@34[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; - 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; -} - - -implementation IsolateReturnPaths/assert@34[29](x: int, y: int) returns (r: int) -{ - - anon0: - assume {:partition} 0 >= x; - assume r#AT#1 == 0 + 2; - assume r#AT#2 == r#AT#1; - 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; -} - - -implementation IsolateReturnPaths(x: int, y: int) returns (r: 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_Else; - - anon6_Else: - assume {:partition} 0 >= x; - assume r#AT#1 == 0 + 2; - assume r#AT#2 == r#AT#1; - goto anon7_Else; - - anon7_Else: - 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; -} - - -isolateJump.bpl(34,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 diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect deleted file mode 100644 index 29725f4eb..000000000 --- a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect +++ /dev/null @@ -1,36 +0,0 @@ -implementation Foo/split@4() -{ - - anon3_Then: - assert 2 == 1 + 1; - assume false; - return; -} - - -implementation Foo/split@11() -{ - - anon3_Else: - assume 2 == 1 + 1; - assert {:split_here} 2 == 2; - assume 3 == 2 + 1; - assume 1 == 1; - goto ; -} - - -implementation Foo/split@12() -{ - - anon3_Else: - assume 2 == 1 + 1; - assume 2 == 2; - assert {:split_here} 3 == 2 + 1; - assert 1 == 1; - goto ; -} - - - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect deleted file mode 100644 index 9f213b896..000000000 --- a/Test/implementationDivision/split/Split.bpl.expect +++ /dev/null @@ -1,112 +0,0 @@ -implementation Foo/split@4() 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 Foo/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) > 25; - assume y#AT#1 == y#AT#0 + 1; - assume {:partition} x#AT#1 < 3; - assert 2 < 2; - assume y#AT#1 * y#AT#1 > 4; - goto ; -} - - -implementation Foo/split@22() 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) > 25; - assume y#AT#1 == y#AT#0 + 1; - assume {:partition} 3 <= x#AT#1; - assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; - assert 2 < 2; - goto ; -} - - -implementation Foo/split@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) > 25; - assume y#AT#1 == y#AT#0 + 1; - goto anon6_Then, anon6_Else; - - anon6_Else: - assume {:partition} 3 <= x#AT#1; - assume y#AT#1 * y#AT#1 * y#AT#1 < 8; - assume 2 < 2; - goto anon4; - - anon4: - assert {:split_here} (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; - return; - - anon6_Then: - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assume y#AT#1 * y#AT#1 > 4; - goto anon4; -} - - -implementation Foo/split@19() 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) > 25; - assume y#AT#1 == y#AT#0 + 1; - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assert {:split_here} y#AT#1 * y#AT#1 > 4; - goto ; -} - - -Split.bpl(15,5): Error: this assertion could not be proved -Execution trace: - Split.bpl(8,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/implementationDivision/focus/focus.bpl b/Test/pruning/Focus.bpl similarity index 100% rename from Test/implementationDivision/focus/focus.bpl rename to Test/pruning/Focus.bpl diff --git a/Test/implementationDivision/focus/focus.bpl.expect b/Test/pruning/Focus.bpl.expect similarity index 50% rename from Test/implementationDivision/focus/focus.bpl.expect rename to Test/pruning/Focus.bpl.expect index 2c28a1a35..71c2b6338 100644 --- a/Test/implementationDivision/focus/focus.bpl.expect +++ b/Test/pruning/Focus.bpl.expect @@ -1,3 +1,3 @@ -focus.bpl(15,5): Error: this assertion could not be proved +Focus.bpl(15,5): Error: this assertion could not be proved Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 1fccbd8bf..15351bb11 100644 --- a/Test/pruning/MonomorphicSplit.bpl +++ b/Test/pruning/MonomorphicSplit.bpl @@ -1,5 +1,5 @@ // RUN: %parallel-boogie /prune:1 /errorTrace:0 /printSplit:"%t" /printSplitDeclarations "%s" > "%t" -// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.spl" +// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit--1.spl" // The following checks are a bit simplistic, but this is // on purpose to reduce brittleness. We assume there would now be two uses clauses diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl similarity index 50% rename from Test/implementationDivision/split/AssumeFalseSplit.bpl rename to Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl index 92c6bb87f..148216280 100644 --- a/Test/implementationDivision/split/AssumeFalseSplit.bpl +++ b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl @@ -1,5 +1,8 @@ -// RUN: %boogie /printSplit:- "%s" > "%t" +// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" // RUN: %diff "%s.expect" "%t" +// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl +// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl +// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl procedure Foo() { diff --git a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect new file mode 100644 index 000000000..37fad75c9 --- /dev/null +++ b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect new file mode 100644 index 000000000..c8727ad27 --- /dev/null +++ b/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect @@ -0,0 +1,10 @@ +implementation Foo() +{ + + anon3_Then: + assert 2 == 1 + 1; + assume false; + return; +} + + diff --git a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect new file mode 100644 index 000000000..29ba05d16 --- /dev/null +++ b/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect @@ -0,0 +1,12 @@ +implementation Foo() +{ + + anon3_Else: + assume 2 == 1 + 1; + assert {:split_here} 2 == 2; + assume 3 == 2 + 1; + assume 1 == 1; + goto ; +} + + diff --git a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect new file mode 100644 index 000000000..838d5aebd --- /dev/null +++ b/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect @@ -0,0 +1,12 @@ +implementation Foo() +{ + + anon3_Else: + assume 2 == 1 + 1; + assume 2 == 2; + assert {:split_here} 3 == 2 + 1; + assert 1 == 1; + goto ; +} + + diff --git a/Test/test0/Split/Foo.split.0.bpl.expect b/Test/test0/Split/Foo.split.0.bpl.expect new file mode 100644 index 000000000..79578bccc --- /dev/null +++ b/Test/test0/Split/Foo.split.0.bpl.expect @@ -0,0 +1,15 @@ +implementation Foo() 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; +} + + diff --git a/Test/test0/Split/Foo.split.1.bpl.expect b/Test/test0/Split/Foo.split.1.bpl.expect new file mode 100644 index 000000000..37297e028 --- /dev/null +++ b/Test/test0/Split/Foo.split.1.bpl.expect @@ -0,0 +1,19 @@ +implementation Foo() 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) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} x#AT#1 < 3; + assert 2 < 2; + assume y#AT#1 * y#AT#1 > 4; + goto ; +} + + diff --git a/Test/test0/Split/Foo.split.2.bpl.expect b/Test/test0/Split/Foo.split.2.bpl.expect new file mode 100644 index 000000000..7f28a2ebf --- /dev/null +++ b/Test/test0/Split/Foo.split.2.bpl.expect @@ -0,0 +1,19 @@ +implementation Foo() 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) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} 3 <= x#AT#1; + assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; + assert 2 < 2; + goto ; +} + + diff --git a/Test/test0/Split/Foo.split.3.bpl.expect b/Test/test0/Split/Foo.split.3.bpl.expect new file mode 100644 index 000000000..eb031aa38 --- /dev/null +++ b/Test/test0/Split/Foo.split.3.bpl.expect @@ -0,0 +1,35 @@ +implementation Foo() 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) > 25; + assume y#AT#1 == y#AT#0 + 1; + goto anon6_Then, anon6_Else; + + anon6_Else: + assume {:partition} 3 <= x#AT#1; + assume y#AT#1 * y#AT#1 * y#AT#1 < 8; + assume 2 < 2; + goto anon4; + + anon4: + assert {:split_here} (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; + return; + + anon6_Then: + assume {:partition} x#AT#1 < 3; + assume 2 < 2; + assume y#AT#1 * y#AT#1 > 4; + goto anon4; +} + + diff --git a/Test/test0/Split/Foo.split.4.bpl.expect b/Test/test0/Split/Foo.split.4.bpl.expect new file mode 100644 index 000000000..83b9850a7 --- /dev/null +++ b/Test/test0/Split/Foo.split.4.bpl.expect @@ -0,0 +1,31 @@ +implementation Foo() returns (y: int) +{ + + PreconditionGeneratedEntry: + goto anon0; + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + goto anon5_LoopHead; + + anon5_LoopHead: + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + goto anon5_LoopBody; + + anon5_LoopBody: + 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) > 25; + assume y#AT#1 == y#AT#0 + 1; + goto anon6_Then; + + anon6_Then: + assume {:partition} x#AT#1 < 3; + assume 2 < 2; + assert {:split_here} y#AT#1 * y#AT#1 > 4; + goto ; +} + + diff --git a/Test/implementationDivision/split/Split.bpl b/Test/test0/Split/Split.bpl similarity index 64% rename from Test/implementationDivision/split/Split.bpl rename to Test/test0/Split/Split.bpl index 4c7fdaf45..e99d76351 100644 --- a/Test/implementationDivision/split/Split.bpl +++ b/Test/test0/Split/Split.bpl @@ -1,5 +1,9 @@ -// RUN: %boogie /printSplit:- "%s" > "%t" +// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" // RUN: %diff "%s.expect" "%t" +// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl +// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl +// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl +// RUN: %diff %S/Foo.split.3.bpl.expect %t-Foo-3.spl procedure Foo() returns (y: int) ensures y >= 0; diff --git a/Test/test0/Split/Split.bpl.expect b/Test/test0/Split/Split.bpl.expect new file mode 100644 index 000000000..67f8e9921 --- /dev/null +++ b/Test/test0/Split/Split.bpl.expect @@ -0,0 +1,5 @@ +Split.bpl(19,5): Error: this assertion could not be proved +Execution trace: + Split.bpl(12,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl index e459892fd..c883fb50c 100644 --- a/Test/test0/SplitOnEveryAssert.bpl +++ b/Test/test0/SplitOnEveryAssert.bpl @@ -6,8 +6,8 @@ // CHECK: checking split 1/11.* // CHECK: checking split 2/11.* // CHECK: checking split 3/11.* +// CHECK: --> split #3 done, \[.* s\] Invalid // CHECK: checking split 4/11.* -// CHECK: --> split #4 done, \[.* s\] Invalid // CHECK: checking split 5/11.* // CHECK: checking split 6/11.* // CHECK: checking split 7/11.* diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect index 22c885b42..a349c0d87 100644 --- a/Test/test2/Structured.bpl.expect +++ b/Test/test2/Structured.bpl.expect @@ -22,5 +22,6 @@ Execution trace: Structured.bpl(355,3): anon4_LoopHead Structured.bpl(358,7): anon4_LoopBody Structured.bpl(361,7): anon5_LoopBody + (0,0): anon3 Boogie program verifier finished with 16 verified, 4 errors