From f01b081986124cf10e95d00d0c3aa2173becb9a9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Oct 2024 15:10:30 +0200 Subject: [PATCH 1/4] Revert "Revert isolation (#966)" This reverts commit 09093a2d2c02fa9b9f6936258fdec6b0eb2e5a58. --- Source/Concurrency/CivlUtil.cs | 6 +- Source/Core/AST/Absy.cs | 12 +- Source/Core/AST/AbsyQuant.cs | 274 ---- Source/Core/AST/{ => Commands}/AbsyCmd.cs | 1394 +---------------- Source/Core/AST/{ => Commands}/CallCmd.cs | 8 +- .../Core/AST/{ => Commands}/HideRevealCmd.cs | 0 Source/Core/AST/{ => GotoBoogie}/Block.cs | 26 +- .../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 + 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/{ => Generic}/Util.cs | 0 Source/Core/Inline.cs | 2 +- Source/Core/Parser.cs | 21 +- Source/Core/ResolutionContext.cs | 4 +- Source/Core/Token.cs | 3 +- 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 +- Source/VCGeneration/ConditionGeneration.cs | 25 +- .../AssertCounterexample.cs | 11 +- .../CallCounterexample.cs | 10 +- .../CalleeCounterexampleInfo.cs | 0 .../Counterexample.cs | 17 +- .../CounterexampleComparer.cs | 0 .../ReturnCounterexample.cs | 10 +- .../TraceLocation.cs | 0 .../{ => Counterexample}/VerifierCallback.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 +- Source/VCGeneration/SmokeTester.cs | 2 +- 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 + Source/VCGeneration/{ => Splits}/Split.cs | 42 +- .../{ => Splits}/SplitAndVerifyWorker.cs | 6 +- .../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 +- Source/VCGeneration/Wlp.cs | 4 +- Test/aitest0/Issue25.bpl | 8 +- Test/aitest0/Issue25.bpl.expect | 8 +- Test/commandline/SplitOnEveryAssert.bpl | 2 +- .../focus/focus.bpl} | 0 .../focus/focus.bpl.expect} | 2 +- .../isolateAssertion/isolateAssertion.bpl | 42 + .../isolateAssertion.bpl.expect | 183 +++ .../isolateJump/isolateJump.bpl | 38 + .../isolateJump/isolateJump.bpl.expect | 126 ++ .../split}/AssumeFalseSplit.bpl | 5 +- .../split/AssumeFalseSplit.bpl.expect | 36 + .../split}/Split.bpl | 6 +- .../split/Split.bpl.expect | 112 ++ Test/pruning/MonomorphicSplit.bpl | 2 +- .../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 - Test/test0/Split/Split.bpl.expect | 5 - Test/test0/SplitOnEveryAssert.bpl | 2 +- Test/test2/Structured.bpl.expect | 1 - 106 files changed, 3437 insertions(+), 2577 deletions(-) rename Source/Core/AST/{ => Commands}/AbsyCmd.cs (60%) rename Source/Core/AST/{ => Commands}/CallCmd.cs (99%) rename Source/Core/AST/{ => Commands}/HideRevealCmd.cs (100%) rename Source/Core/AST/{ => GotoBoogie}/Block.cs (88%) rename Source/Core/AST/{ => GotoBoogie}/ChangeScope.cs (100%) create mode 100644 Source/Core/AST/GotoBoogie/GotoCmd.cs create mode 100644 Source/Core/AST/GotoBoogie/ReturnCmd.cs create mode 100644 Source/Core/AST/GotoBoogie/TransferCmd.cs create mode 100644 Source/Core/AST/QKeyValue.cs create mode 100644 Source/Core/AST/QKeyValueExtensions.cs create mode 100644 Source/Core/AST/StructuredBoogie/BigBlock.cs create mode 100644 Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs create mode 100644 Source/Core/AST/StructuredBoogie/BreakCmd.cs create mode 100644 Source/Core/AST/StructuredBoogie/IfCmd.cs create mode 100644 Source/Core/AST/StructuredBoogie/StmtList.cs create mode 100644 Source/Core/AST/StructuredBoogie/StmtListBuilder.cs create mode 100644 Source/Core/AST/StructuredBoogie/StructuredCmd.cs create mode 100644 Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs create mode 100644 Source/Core/AST/StructuredBoogie/WhileCmd.cs create mode 100644 Source/Core/Generic/ListExtensions.cs rename Source/Core/{ => Generic}/Util.cs (100%) rename Source/VCGeneration/{ => Counterexample}/AssertCounterexample.cs (82%) rename Source/VCGeneration/{Counterexamples => Counterexample}/CallCounterexample.cs (86%) rename Source/VCGeneration/{Counterexamples => Counterexample}/CalleeCounterexampleInfo.cs (100%) rename Source/VCGeneration/{Counterexamples => Counterexample}/Counterexample.cs (97%) rename Source/VCGeneration/{Counterexamples => Counterexample}/CounterexampleComparer.cs (100%) rename Source/VCGeneration/{ => Counterexample}/ReturnCounterexample.cs (85%) rename Source/VCGeneration/{Counterexamples => Counterexample}/TraceLocation.cs (100%) rename Source/VCGeneration/{ => Counterexample}/VerifierCallback.cs (100%) delete mode 100644 Source/VCGeneration/FocusAttribute.cs delete mode 100644 Source/VCGeneration/ManualSplitFinder.cs create mode 100644 Source/VCGeneration/Splits/BlockRewriter.cs create mode 100644 Source/VCGeneration/Splits/FocusAttributeHandler.cs create mode 100644 Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs create mode 100644 Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs create mode 100644 Source/VCGeneration/Splits/ManualSplitFinder.cs create mode 100644 Source/VCGeneration/Splits/PathToken.cs rename Source/VCGeneration/{ => Splits}/Split.cs (96%) rename Source/VCGeneration/{ => Splits}/SplitAndVerifyWorker.cs (97%) create mode 100644 Source/VCGeneration/Splits/SplitAttributeHandler.cs create mode 100644 Source/VCGeneration/Splits/TokenWrapper.cs rename Test/{pruning/Focus.bpl => implementationDivision/focus/focus.bpl} (100%) rename Test/{pruning/Focus.bpl.expect => implementationDivision/focus/focus.bpl.expect} (50%) create mode 100644 Test/implementationDivision/isolateAssertion/isolateAssertion.bpl create mode 100644 Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect create mode 100644 Test/implementationDivision/isolateJump/isolateJump.bpl create mode 100644 Test/implementationDivision/isolateJump/isolateJump.bpl.expect rename Test/{test0/AssumeFalseSplit => implementationDivision/split}/AssumeFalseSplit.bpl (50%) create mode 100644 Test/implementationDivision/split/AssumeFalseSplit.bpl.expect rename Test/{test0/Split => implementationDivision/split}/Split.bpl (64%) create mode 100644 Test/implementationDivision/split/Split.bpl.expect delete mode 100644 Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect delete mode 100644 Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect delete mode 100644 Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect delete mode 100644 Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect delete mode 100644 Test/test0/Split/Foo.split.0.bpl.expect delete mode 100644 Test/test0/Split/Foo.split.1.bpl.expect delete mode 100644 Test/test0/Split/Foo.split.2.bpl.expect delete mode 100644 Test/test0/Split/Foo.split.3.bpl.expect delete mode 100644 Test/test0/Split/Foo.split.4.bpl.expect delete mode 100644 Test/test0/Split/Split.bpl.expect diff --git a/Source/Concurrency/CivlUtil.cs b/Source/Concurrency/CivlUtil.cs index ac48c1164..49ee3003c 100644 --- a/Source/Concurrency/CivlUtil.cs +++ b/Source/Concurrency/CivlUtil.cs @@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars) public static class BlockHelper { + public static readonly IToken /*!*/ ReportedNoToken = new Token(); + public static Block Block(string label, List cmds) { - return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd); + return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd); } public static Block Block(string label, List cmds, List gotoTargets) { - return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); + return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets)); } } diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index d8f53dbca..c109aacbb 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 (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null) + if (Attributes.FindBoolAttribute("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 (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool) + if (Attributes.FindBoolAttribute("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 && !QKeyValue.FindBoolAttribute(Attributes, "inline")) + if (Body != null && !Attributes.FindBoolAttribute("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 && !QKeyValue.FindBoolAttribute(Attributes, "define")) + if (DefinitionBody != null && !Attributes.FindBoolAttribute("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 && QKeyValue.FindBoolAttribute(Attributes, "always_assume"); + return Free && Attributes.FindBoolAttribute("always_assume"); } @@ -2490,7 +2490,7 @@ public String ErrorMessage public bool CanAlwaysAssume () { - return Free && QKeyValue.FindBoolAttribute(this.Attributes, "always_assume"); + return Free && this.Attributes.FindBoolAttribute("always_assume"); } public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv) diff --git a/Source/Core/AST/AbsyQuant.cs b/Source/Core/AST/AbsyQuant.cs index 301a3bf70..185fa32e9 100644 --- a/Source/Core/AST/AbsyQuant.cs +++ b/Source/Core/AST/AbsyQuant.cs @@ -330,280 +330,6 @@ 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/AbsyCmd.cs b/Source/Core/AST/Commands/AbsyCmd.cs similarity index 60% rename from Source/Core/AST/AbsyCmd.cs rename to Source/Core/AST/Commands/AbsyCmd.cs index a6400e232..0beaa357b 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/Commands/AbsyCmd.cs @@ -7,1188 +7,6 @@ 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))] @@ -1226,7 +44,7 @@ public static void ComputeChecksums(CoreOptions options, Cmd cmd, Implementation } if (cmd is AssumeCmd assumeCmd - && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization")) + && assumeCmd.Attributes.FindBoolAttribute("assumption_variable_initialization")) { // Ignore assumption variable initializations. assumeCmd.Checksum = currentChecksum; @@ -1694,7 +512,7 @@ public override void Resolve(ResolutionContext rc) continue; } var decl = lhs.AssignedVariable.Decl; - if (lhs.AssignedVariable.Decl != null && QKeyValue.FindBoolAttribute(decl.Attributes, "assumption")) + if (lhs.AssignedVariable.Decl != null && decl.Attributes.FindBoolAttribute("assumption")) { var rhs = Rhss[i] as NAryExpr; if (rhs == null @@ -3399,35 +2217,6 @@ 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 @@ -3442,183 +2231,4 @@ 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/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs similarity index 99% rename from Source/Core/AST/CallCmd.cs rename to Source/Core/AST/Commands/CallCmd.cs index e35541b6d..0f0ed662c 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. if (callId is not null) { - a.CopyIdWithModificationsFrom(tok, req, + (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresAssumed(callId, id)); } @@ -1052,12 +1052,12 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #region stratified inlining support - if (QKeyValue.FindBoolAttribute(e.Attributes, "si_fcall")) + if (e.Attributes.FindBoolAttribute("si_fcall")) { assume.Attributes = Attributes; } - if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate")) + if (e.Attributes.FindBoolAttribute("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.CopyIdWithModificationsFrom(tok, e, + (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, id => new TrackedCallEnsures(callId, id)); } diff --git a/Source/Core/AST/HideRevealCmd.cs b/Source/Core/AST/Commands/HideRevealCmd.cs similarity index 100% rename from Source/Core/AST/HideRevealCmd.cs rename to Source/Core/AST/Commands/HideRevealCmd.cs diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs similarity index 88% rename from Source/Core/AST/Block.cs rename to Source/Core/AST/GotoBoogie/Block.cs index c6ac50740..0bc535bdb 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/GotoBoogie/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,21 +114,25 @@ 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 Block(IToken tok) + public static Block ShallowClone(Block block) { + return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); + } + + public Block(IToken tok, TransferCmd cmd) : this(tok, "", new List(), new ReturnCmd(tok)) { } @@ -143,7 +147,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/ChangeScope.cs b/Source/Core/AST/GotoBoogie/ChangeScope.cs similarity index 100% rename from Source/Core/AST/ChangeScope.cs rename to Source/Core/AST/GotoBoogie/ChangeScope.cs diff --git a/Source/Core/AST/GotoBoogie/GotoCmd.cs b/Source/Core/AST/GotoBoogie/GotoCmd.cs new file mode 100644 index 000000000..9b7aa5340 --- /dev/null +++ b/Source/Core/AST/GotoBoogie/GotoCmd.cs @@ -0,0 +1,159 @@ +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 new file mode 100644 index 000000000..9f60df66b --- /dev/null +++ b/Source/Core/AST/GotoBoogie/ReturnCmd.cs @@ -0,0 +1,33 @@ +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 new file mode 100644 index 000000000..933ccdc91 --- /dev/null +++ b/Source/Core/AST/GotoBoogie/TransferCmd.cs @@ -0,0 +1,33 @@ +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/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index a24485f89..b20edeaad 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 string FindStringAttribute(string name) + public static string FindStringAttribute(this ICarriesAttributes destination, string name) { - return QKeyValue.FindStringAttribute(Attributes, name); + return QKeyValue.FindStringAttribute(destination.Attributes, name); } - public void AddStringAttribute(IToken tok, string name, string parameter) + public static void AddStringAttribute(this ICarriesAttributes destination, IToken tok, string name, string parameter) { - Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); + destination.Attributes = new QKeyValue(tok, name, new List() {parameter}, destination.Attributes); } - -} - -public static class CarriesAttributesExtensions -{ - public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src) + + public static void CopyIdFrom(this ICarriesAttributes destination, IToken tok, ICarriesAttributes src) { var id = src.FindStringAttribute("id"); if (id is not null) { - dest.AddStringAttribute(tok, "id", id); + destination.AddStringAttribute(tok, "id", id); } } - public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func modifier) + public static void CopyIdWithModificationsFrom(this ICarriesAttributes destination, IToken tok, + ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { - dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel); + destination.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 6d6d2415c..d1b497dfb 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 !QKeyValue.FindBoolAttribute(Attributes, "entrypoint"); + return !Attributes.FindBoolAttribute("entrypoint"); } return false; @@ -462,19 +462,19 @@ void BlocksWriters(TokenTextWriter stream) { } public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable blocks, - bool showLocals) { + bool showLocals, string nameSuffix = "") { EmitImplementation(stream, level, writer => { foreach (var block in blocks) { block.Emit(writer, level + 1); } - }, showLocals); + }, showLocals, nameSuffix); } - public void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals) + private void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals, string nameSuffix = "") { stream.Write(this, level, "implementation "); EmitAttributes(stream); - stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(Name) + nameSuffix); EmitSignature(stream, false); stream.WriteLine(); diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 45011b574..810b73232 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 => !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))) + foreach (var d in TopLevelDeclarations.Where(d => !d.Attributes.FindBoolAttribute("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 (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) + if (!d.Attributes.FindBoolAttribute("ignore")) { d.Resolve(rc); } @@ -110,7 +110,7 @@ private void ResolveTypes(ResolutionContext rc) foreach (var d in TopLevelDeclarations.OfType()) { Contract.Assert(d != null); - if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) + if (!d.Attributes.FindBoolAttribute("ignore")) { synonymDecls.Add(d); } @@ -498,7 +498,7 @@ public static Graph BuildCallGraph(CoreOptions options, Program return callGraph; } - public static Graph GraphFromBlocks(List blocks, bool forward = true) + public static Graph GraphFromBlocksSubset(IReadOnlyList blocks, IReadOnlySet subset = null, bool forward = true) { var result = new Graph(); if (!blocks.Any()) @@ -506,6 +506,9 @@ public static Graph GraphFromBlocks(List blocks, bool forward = tr 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); @@ -514,7 +517,7 @@ void AddEdge(Block a, Block b) { } } - result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph + result.AddSource(blocks[0]); foreach (var block in blocks) { if (block.TransferCmd is GotoCmd gtc) @@ -525,6 +528,10 @@ 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 new file mode 100644 index 000000000..5693a4e3e --- /dev/null +++ b/Source/Core/AST/QKeyValue.cs @@ -0,0 +1,269 @@ +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 new file mode 100644 index 000000000..4949875e3 --- /dev/null +++ b/Source/Core/AST/QKeyValueExtensions.cs @@ -0,0 +1,16 @@ +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 new file mode 100644 index 000000000..0fbe65e52 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/BigBlock.cs @@ -0,0 +1,124 @@ +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 new file mode 100644 index 000000000..b53bc3606 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs @@ -0,0 +1,591 @@ +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 new file mode 100644 index 000000000..3ea89b616 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/BreakCmd.cs @@ -0,0 +1,28 @@ +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 new file mode 100644 index 000000000..5f29f407d --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/IfCmd.cs @@ -0,0 +1,108 @@ +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 new file mode 100644 index 000000000..51407e1c7 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/StmtList.cs @@ -0,0 +1,134 @@ +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 new file mode 100644 index 000000000..dd7b67666 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/StmtListBuilder.cs @@ -0,0 +1,98 @@ +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 new file mode 100644 index 000000000..f95ef14db --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/StructuredCmd.cs @@ -0,0 +1,38 @@ +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 new file mode 100644 index 000000000..b363253d5 --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/StructuredCmdContracts.cs @@ -0,0 +1,18 @@ +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 new file mode 100644 index 000000000..135bd43ae --- /dev/null +++ b/Source/Core/AST/StructuredBoogie/WhileCmd.cs @@ -0,0 +1,74 @@ +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 bcdbbf517..8b5e95ac5 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 && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && + if (expr.Decl != null && !(expr.Decl.Attributes.FindBoolAttribute("assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { liveSet.Remove(expr.Decl); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index b850527c2..e020af43f 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 (QKeyValue.FindBoolAttribute(kv, "inline")) { - if (QKeyValue.FindBoolAttribute(kv, "define")) + if (kv.FindBoolAttribute("inline")) { + if (kv.FindBoolAttribute("define")) SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; - } else if (QKeyValue.FindBoolAttribute(kv, "define")) { + } else if (kv.FindBoolAttribute("define")) { if (func.TypeParameters.Count > 0) SemErr("function with :define attribute has to be monomorphic"); func.DefinitionBody = func.CreateFunctionDefinition(definition); @@ -1032,6 +1032,7 @@ 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){ @@ -1039,7 +1040,9 @@ TransferCmd ss.Add(s.val); } tc = new GotoCmd(y, ss); .) - | "return" (. tc = new ReturnCmd(t); .) + | "return" + { Attribute } + (. tc = new ReturnCmd(t) { Attributes = kv }; .) ) ";" . @@ -1688,6 +1691,7 @@ SpecBlock List/*!*/ xs; List ss = new List(); b = dummyBlock; + QKeyValue kv = null; Expr/*!*/ e; .) Ident ":" @@ -1706,8 +1710,13 @@ SpecBlock ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); .) - | "return" Expression - (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) + | "return" + { Attribute } + Expression + (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { + Attributes = kv + }); + .) ) ";" . diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 42b25efab..3e3ff4bc5 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 QKeyValue.FindBoolAttribute(obj.Attributes, name); + return obj.Attributes.FindBoolAttribute(name); } public static bool RemoveAttributes(ICarriesAttributes obj, Func cond) diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index d0d472ff5..b7ab2e965 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -10,6 +10,8 @@ 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 a3a958fd9..fce5eb802 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 (QKeyValue.FindBoolAttribute(function.Attributes, "inline") && - QKeyValue.FindBoolAttribute(function.Attributes, "define")) + if (function.Attributes.FindBoolAttribute("inline") && + function.Attributes.FindBoolAttribute("define")) { checkingContext.Error(function.tok, "A function may not have both :inline and :define attributes"); } - if (QKeyValue.FindBoolAttribute(function.Attributes, "inline") && + if (function.Attributes.FindBoolAttribute("inline") && function.Body == null) { checkingContext.Error(function.tok, "Function with :inline attribute must have a body"); } - if (QKeyValue.FindBoolAttribute(function.Attributes, "define") && + if (function.Attributes.FindBoolAttribute("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 (QKeyValue.FindBoolAttribute(node.Attributes, "inline")) + if (node.Attributes.FindBoolAttribute("inline")) { this.enclosingFunction = node; base.Visit(node.Body); this.enclosingFunction = null; } - else if (QKeyValue.FindBoolAttribute(node.Attributes, "define")) + else if (node.Attributes.FindBoolAttribute("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 (QKeyValue.FindBoolAttribute(functionCall.Func.Attributes, "inline") || - QKeyValue.FindBoolAttribute(functionCall.Func.Attributes, "define")) + if (functionCall.Func.Attributes.FindBoolAttribute("inline") || + functionCall.Func.Attributes.FindBoolAttribute("define")) { functionDependencyGraph.AddEdge(enclosingFunction, functionCall.Func); } diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs new file mode 100644 index 000000000..6825839b8 --- /dev/null +++ b/Source/Core/Generic/ListExtensions.cs @@ -0,0 +1,31 @@ +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/Util.cs b/Source/Core/Generic/Util.cs similarity index 100% rename from Source/Core/Util.cs rename to Source/Core/Generic/Util.cs diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 3162cddbe..d67732fa2 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 (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) + if (ens.Attributes.FindBoolAttribute("InlineAssume")) { return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition)); } diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ff6ecb84f..68966a376 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 (QKeyValue.FindBoolAttribute(kv, "inline")) { - if (QKeyValue.FindBoolAttribute(kv, "define")) + if (kv.FindBoolAttribute("inline")) { + if (kv.FindBoolAttribute("define")) SemErr("function cannot have both :inline and :define attributes"); func.Body = definition; - } else if (QKeyValue.FindBoolAttribute(kv, "define")) { + } else if (kv.FindBoolAttribute("define")) { if (func.TypeParameters.Count > 0) SemErr("function with :define attribute has to be monomorphic"); func.DefinitionBody = func.CreateFunctionDefinition(definition); @@ -1536,6 +1536,7 @@ 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(); @@ -1548,7 +1549,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) { } else if (la.kind == 56) { Get(); - tc = new ReturnCmd(t); + while (la.kind == 26) { + Attribute(ref kv); + } + tc = new ReturnCmd(t) { Attributes = kv }; } else SynErr(148); Expect(10); } @@ -2558,6 +2562,7 @@ void SpecBlock(out Block/*!*/ b) { List/*!*/ xs; List ss = new List(); b = dummyBlock; + QKeyValue kv = null; Expr/*!*/ e; Ident(out x); @@ -2583,8 +2588,14 @@ 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)); + b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { + Attributes = kv + }); + } else SynErr(174); Expect(10); } diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 47fe6bd57..ee240bde7 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 (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) + if (a.Attributes.FindBoolAttribute("extern")) { ignore = a; keep = b; } - else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) + else if (b.Attributes.FindBoolAttribute("extern")) { ignore = b; keep = a; diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs index 5f7a1bb1f..27a0dd156 100644 --- a/Source/Core/Token.cs +++ b/Source/Core/Token.cs @@ -33,8 +33,7 @@ public string /*!*/ public Token next; // ML 2005-03-11 Tokens are kept in linked list - public static readonly IToken /*!*/ - NoToken = new Token(); + public static readonly IToken /*!*/ NoToken = new Token(); public Token() { diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 2e0ae6c67..064b4a6db 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 && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) + if (a != null && a.Attributes.FindBoolAttribute("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)); + localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok, new ReturnCmd(prog.tok))); foreach (var keyValue in localCtrlDeps[impl]) { globalCtrlDep.Add(keyValue.Key, keyValue.Value); } } - var callGraph = Program.BuildCallGraph(options, prog); + Graph 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,17 +562,18 @@ private Dictionary> ComputeGlobalControlDependences() // Finally reverse the dependences - var result = new Dictionary>(); - foreach (var keyValue in globalCtrlDep) + Dictionary> 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 112c6c481..ec349a347 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.3 + 3.3.2 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 171797990..764ea17a4 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 _, out _); + callback, out _, out _); } } diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs index ecb6b4220..183a7028c 100644 --- a/Source/ExecutionEngine/ConsolePrinter.cs +++ b/Source/ExecutionEngine/ConsolePrinter.cs @@ -177,8 +177,9 @@ public virtual void ReportBplError(IToken tok, string message, bool error, TextW message = $"{category}: {message}"; } - var s = tok != null - ? $"{ExecutionEngine.GetFileNameForConsole(Options, tok.filename)}({tok.line},{tok.col}): {message}" + var s = tok != null + ? string.Format("{0}({1},{2}): {3}", 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 0d6fa1bbc..72002036b 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 => QKeyValue.FindBoolAttribute(f.Attributes, "define"))) + else if (program.TopLevelDeclarations.OfType().Any(f => f.Attributes.FindBoolAttribute("define"))) { Options.OutputWriter.WriteLine("Functions with :define attribute only supported with monomorphic encoding"); return PipelineOutcome.FatalError; @@ -736,16 +736,15 @@ 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.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList(); + var splits = ManualSplitFinder.GetParts(Options, run, + (token, blocks) => new ManualSplit(Options, () => blocks, vcGenerator, run, token)).ToList(); for (var index = 0; index < splits.Count; index++) { var split = splits[index]; split.SplitIndex = index; @@ -1310,6 +1309,8 @@ 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 f7e4806df..baf7c48a1 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -22,7 +22,6 @@ 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 43dda6925..50f3fd8e5 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, Split.GotoCmdOrigins, + var split = new ManualSplit(Split.Options, () => Split.Blocks, 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 2738566dd..2af21485a 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 currentDominatorNum = nodeNumberToImmediateDominator[domineeNum]; + int currentDominator = nodeNumberToImmediateDominator[domineeNum]; while (true) { - if (currentDominatorNum == dominatorNum) + if (currentDominator == dominatorNum) { return true; } - if (currentDominatorNum == sourceNum) + if (currentDominator == sourceNum) { return false; } - path?.Add(postOrderNumberToNode[currentDominatorNum]); + path?.Add(postOrderNumberToNode[currentDominator]); - currentDominatorNum = nodeNumberToImmediateDominator[currentDominatorNum]; + currentDominator = nodeNumberToImmediateDominator[currentDominator]; } } @@ -623,35 +623,55 @@ 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> DominatorsFast() + /// + /// 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() { - var topoSorted = TopologicalSort().ToList(); - var dominators = new Dictionary>(); - topoSorted.ForEach(u => dominators[u] = topoSorted.ToHashSet()); - foreach (var node in topoSorted) + var dominatorsPerNode = new Dictionary>(); + foreach (var node in TopologicalSort()) { - 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])); + 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); } - s.Add(node); - dominators[node] = s; } - return dominators; + + if (result == null) { + return new HashSet(); + } + + return result; } - // 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() { - List topoSorted = TopologicalSort().ToList(); - Dictionary> dominators = DominatorsFast(); + var topoSorted = TopologicalSort().ToList(); + var indexPerNode = new Dictionary(); + for (int index = 0; index < topoSorted.Count; index++) { + indexPerNode[topoSorted[index]] = index; + } + var dominators = AcyclicDominators(); var immediateDominator = new Dictionary(); foreach (var node in Nodes) { @@ -659,9 +679,10 @@ public Dictionary ImmediateDominator() { dominators[node].Remove(node); } - immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => topoSorted.IndexOf(e))); + immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => indexPerNode[e])); } - immediateDominator[source] = source; + + immediateDominator.Remove(source); return immediateDominator; } @@ -686,7 +707,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(); @@ -1133,7 +1154,7 @@ public string ToDot(Func NodeLabel = null, Func Node return s.ToString(); } - public ICollection ComputeReachability(Node start, bool forward = true) + public ISet 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 e88ca2fb9..0ad80927d 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) && QKeyValue.FindBoolAttribute(p.Attributes, "originated_from_invariant")) + else if ((p is AssertCmd) && p.Attributes.FindBoolAttribute("originated_from_invariant")) { var tag = GetTagFromNonCandidateAttributes(p.Attributes); if (tag != null) @@ -467,7 +467,7 @@ private IEnumerable GetNonCandidateAnnotations() continue; } - if (!QKeyValue.FindBoolAttribute(Assertion.Attributes, "originated_from_invariant")) + if (!Assertion.Attributes.FindBoolAttribute("originated_from_invariant")) { continue; } @@ -528,7 +528,7 @@ private IEnumerable GetNonCandidateAnnotations() private IEnumerable GetCandidates() { return prog.Variables.Where(Item => - QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); + Item.Attributes.FindBoolAttribute("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 (QKeyValue.FindBoolAttribute(a.Attributes, "originated_from_invariant")) + else if (a.Attributes.FindBoolAttribute("originated_from_invariant")) { string tag = GetTagFromNonCandidateAttributes(a.Attributes); if (tag == null) diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 4efc13c77..2afaddbf4 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 => QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); + Item => Item.Attributes.FindBoolAttribute("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 ee24e7bfa..a787a8a65 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); - var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo); + 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, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector, + handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, 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 6c39f1ec0..85d1f41a1 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -98,7 +98,8 @@ procedure Procedure(y: int) var engine = ExecutionEngine.CreateWithoutSharedCache(options); var tasks = await engine.GetVerificationTasks(program); - // The first split is empty. Maybe it can be optimized away + // The implicit return at the end gets a separate VC. + // 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 fb0087cd8..94505c1c9 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 true; + ensures 1 == 1; { }"; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 2e7f91060..13ee3a18a 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( - new Token(-17, -4), blockLabel, startCmds, + Token.NoToken, 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.CopyIdFrom(req.tok, req); + (c as ICarriesAttributes).CopyIdFrom(req.tok, req); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -450,8 +450,6 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr options.PrintDesugarings = oldPrintDesugaringSetting; } - - public static void ResetPredecessors(List blocks) { Contract.Requires(blocks != null); @@ -766,7 +764,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. @@ -881,8 +879,7 @@ 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 @@ -1040,7 +1037,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing } } else if (pc is AssumeCmd - && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot") + && pc.Attributes.FindBoolAttribute("precondition_previous_snapshot") && pc.SugaredCmdChecksum != null) { if (!relevantDoomedAssumpVars.Any() @@ -1065,7 +1062,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing dropCmd = true; } } - else if (pc is AssumeCmd && QKeyValue.FindBoolAttribute(pc.Attributes, "assumption_variable_initialization")) + else if (pc is AssumeCmd && pc.Attributes.FindBoolAttribute("assumption_variable_initialization")) { var identExpr = pc.Expr as IdentifierExpr; if (identExpr != null && identExpr.Decl != null && !incarnationMap.ContainsKey(identExpr.Decl)) @@ -1200,7 +1197,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.CopyIdFrom(assign.tok, assign); + (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); passiveCmds.Add(assumeCmd); } @@ -1213,7 +1210,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing { var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr; if (identExpr != null && identExpr.Decl != null && - QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && + identExpr.Decl.Attributes.FindBoolAttribute("assumption") && incarnationMap.TryGetValue(identExpr.Decl, out var incarnation)) { TraceCachingAction(traceWriter, assign, CachingAction.AssumeNegationOfAssumptionVariable); @@ -1241,7 +1238,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 => - !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))) + !(v.Decl.Attributes.FindBoolAttribute("assumption") && v.Decl.Name.StartsWith("a##cached##"))) .ToList(); // First, compute the new incarnations foreach (IdentifierExpr ie in havocVars) @@ -1276,7 +1273,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing // assume v_post ==> v_pre; foreach (IdentifierExpr ie in havocVars) { - if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption")) + if (ie.Decl.Attributes.FindBoolAttribute("assumption")) { var preInc = (Expr) (preHavocIncarnationMap[ie.Decl].Clone()); var postInc = (Expr) (incarnationMap[ie.Decl].Clone()); @@ -1394,7 +1391,7 @@ public Block CreateBlockBetween(int predIndex, Block succ) bs.Add(succ); Block newBlock = new Block( - new Token(-17, -4), + Token.NoToken, newBlockLabel, new List(), new GotoCmd(Token.NoToken, ls, bs) diff --git a/Source/VCGeneration/AssertCounterexample.cs b/Source/VCGeneration/Counterexample/AssertCounterexample.cs similarity index 82% rename from Source/VCGeneration/AssertCounterexample.cs rename to Source/VCGeneration/Counterexample/AssertCounterexample.cs index e43d6fecd..522b55cd0 100644 --- a/Source/VCGeneration/AssertCounterexample.cs +++ b/Source/VCGeneration/Counterexample/AssertCounterexample.cs @@ -6,23 +6,19 @@ 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) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssert) { Contract.Requires(trace != null); Contract.Requires(failingAssert != null); Contract.Requires(context != null); - this.FailingAssert = failingAssert; } protected override Cmd ModelFailingCommand => FailingAssert; @@ -32,10 +28,7 @@ public override int GetLocation() return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; } - public override byte[] Checksum - { - get { return FailingAssert.Checksum; } - } + public override byte[] Checksum => FailingAssert.Checksum; public override Counterexample Clone() { diff --git a/Source/VCGeneration/Counterexamples/CallCounterexample.cs b/Source/VCGeneration/Counterexample/CallCounterexample.cs similarity index 86% rename from Source/VCGeneration/Counterexamples/CallCounterexample.cs rename to Source/VCGeneration/Counterexample/CallCounterexample.cs index e98ce17b3..199df0c15 100644 --- a/Source/VCGeneration/Counterexamples/CallCounterexample.cs +++ b/Source/VCGeneration/Counterexample/CallCounterexample.cs @@ -6,9 +6,8 @@ namespace Microsoft.Boogie; public class CallCounterexample : Counterexample { - public CallCmd FailingCall; - public Requires FailingRequires; - public AssertRequiresCmd FailingFailingAssert; + public readonly CallCmd FailingCall; + public readonly Requires FailingRequires; [ContractInvariantMethod] void ObjectInvariant() @@ -20,7 +19,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) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertRequires) { var failingRequires = failingAssertRequires.Requires; var failingCall = failingAssertRequires.Call; @@ -31,7 +30,6 @@ 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; } @@ -52,7 +50,7 @@ public override byte[] Checksum public override Counterexample Clone() { - var ret = new CallCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, Model, MvInfo, Context, ProofRun, Checksum); + var ret = new CallCounterexample(Options, Trace, AugmentedTrace, (AssertRequiresCmd)FailingAssert, Model, MvInfo, Context, ProofRun, Checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs b/Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs rename to Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs diff --git a/Source/VCGeneration/Counterexamples/Counterexample.cs b/Source/VCGeneration/Counterexample/Counterexample.cs similarity index 97% rename from Source/VCGeneration/Counterexamples/Counterexample.cs rename to Source/VCGeneration/Counterexample/Counterexample.cs index da9cdca9c..15d4cab2b 100644 --- a/Source/VCGeneration/Counterexamples/Counterexample.cs +++ b/Source/VCGeneration/Counterexample/Counterexample.cs @@ -25,6 +25,7 @@ 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; @@ -35,7 +36,7 @@ void ObjectInvariant() public Dictionary CalleeCounterexamples; internal Counterexample(VCGenOptions options, List trace, List augmentedTrace, Model model, - VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) + VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, AssertCmd failingAssert) { Contract.Requires(trace != null); Contract.Requires(context != null); @@ -45,6 +46,7 @@ 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) @@ -112,7 +114,7 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { int numBlock = -1; string ind = new string(' ', indent); - foreach (var block in Trace) + foreach (Block block in Trace) { Contract.Assert(block != null); numBlock++; @@ -120,13 +122,9 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { tw.WriteLine("{0}", ind); } - else - { + else { // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user - if (Options.ErrorTrace == 1 && block.tok.line == -17 && block.tok.col == -4) - { + if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) { continue; } @@ -137,8 +135,7 @@ 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/Counterexamples/CounterexampleComparer.cs b/Source/VCGeneration/Counterexample/CounterexampleComparer.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/CounterexampleComparer.cs rename to Source/VCGeneration/Counterexample/CounterexampleComparer.cs diff --git a/Source/VCGeneration/ReturnCounterexample.cs b/Source/VCGeneration/Counterexample/ReturnCounterexample.cs similarity index 85% rename from Source/VCGeneration/ReturnCounterexample.cs rename to Source/VCGeneration/Counterexample/ReturnCounterexample.cs index 526ee4959..98092c946 100644 --- a/Source/VCGeneration/ReturnCounterexample.cs +++ b/Source/VCGeneration/Counterexample/ReturnCounterexample.cs @@ -7,8 +7,7 @@ namespace Microsoft.Boogie; public class ReturnCounterexample : Counterexample { public TransferCmd FailingReturn; - public Ensures FailingEnsures; - public AssertEnsuresCmd FailingFailingAssert; + public readonly Ensures FailingEnsures; [ContractInvariantMethod] void ObjectInvariant() @@ -21,7 +20,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) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertEnsures) { var failingEnsures = failingAssertEnsures.Ensures; Contract.Requires(trace != null); @@ -31,7 +30,6 @@ public ReturnCounterexample(VCGenOptions options, List trace, List /// Returns the checksum of the corresponding assertion. @@ -51,7 +49,7 @@ public override int GetLocation() public override Counterexample Clone() { - var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); + var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, (AssertEnsuresCmd)FailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/Counterexamples/TraceLocation.cs b/Source/VCGeneration/Counterexample/TraceLocation.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/TraceLocation.cs rename to Source/VCGeneration/Counterexample/TraceLocation.cs diff --git a/Source/VCGeneration/VerifierCallback.cs b/Source/VCGeneration/Counterexample/VerifierCallback.cs similarity index 100% rename from Source/VCGeneration/VerifierCallback.cs rename to Source/VCGeneration/Counterexample/VerifierCallback.cs diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs deleted file mode 100644 index 2da576e11..000000000 --- a/Source/VCGeneration/FocusAttribute.cs +++ /dev/null @@ -1,147 +0,0 @@ -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 a8fa2bc30..e0f40524b 100644 --- a/Source/VCGeneration/LoopExtractor.cs +++ b/Source/VCGeneration/LoopExtractor.cs @@ -313,10 +313,7 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G continue; } - Block newBlock = new Block(block.tok) - { - Label = block.Label - }; + var newBlock = Block.ShallowClone(block); if (headRecursion && block == header) { CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone(); @@ -334,11 +331,8 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G blockMap[block] = newBlock; if (newBlocksCreated.TryGetValue(block, out var original)) { - var newBlock2 = new Block(original.tok) - { - Label = original.Label, - Cmds = Substituter.Apply(subst, original.Cmds) - }; + var newBlock2 = Block.ShallowClone(original); + newBlock2.Cmds = Substituter.Apply(subst, original.Cmds); blockMap[original] = newBlock2; } @@ -350,22 +344,18 @@ 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 = 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 + 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 if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd)) { auxNewBlock.Cmds.Add(assignCmd); diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs index 09927d3c1..5b47299b7 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 IToken Token { get; } + public IImplementationPartOrigin Token { get; } public ManualSplit(VCGenOptions options, Func> blocks, - Dictionary gotoCmdOrigins, - VerificationConditionGenerator par, + VerificationConditionGenerator parent, ImplementationRun run, - IToken token, int? randomSeed = null) - : base(options, blocks, gotoCmdOrigins, par, run, randomSeed) + IImplementationPartOrigin origin, int? randomSeed = null) + : base(options, blocks, parent, run, randomSeed) { - Token = token; + Token = origin; } } \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs deleted file mode 100644 index ffc6806d2..000000000 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ /dev/null @@ -1,216 +0,0 @@ -#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 85da548a6..8999f8e65 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 (QKeyValue.FindBoolAttribute(declaration.Attributes, "include_dep")) { + if (declaration.Attributes.FindBoolAttribute("include_dep")) { incomingSets.Add(new[] { newIncoming }); } } diff --git a/Source/VCGeneration/Prune/Pruner.cs b/Source/VCGeneration/Prune/Pruner.cs index 165eb5239..39d479405 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 => QKeyValue.FindBoolAttribute(d.Attributes, "keep")); + var keepRoots = program.TopLevelDeclarations.Where(d => d.Attributes.FindBoolAttribute("keep")); var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies, blocksVisitor.Outgoing.Concat(keepRoots).ToHashSet(), TraverseDeclaration).ToHashSet(); return program.TopLevelDeclarations.Where(d => diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 3f49e5207..350567ebb 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 && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable")) + if (assrt != null && assrt.Attributes.FindBoolAttribute("PossiblyUnreachable")) { return false; } diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs new file mode 100644 index 000000000..dc93dab28 --- /dev/null +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -0,0 +1,136 @@ +#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 new file mode 100644 index 000000000..812d80407 --- /dev/null +++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs @@ -0,0 +1,116 @@ +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 new file mode 100644 index 000000000..1d90a36e0 --- /dev/null +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -0,0 +1,106 @@ +#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 new file mode 100644 index 000000000..5f7c1de04 --- /dev/null +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -0,0 +1,87 @@ +#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 new file mode 100644 index 000000000..b1b8e676b --- /dev/null +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -0,0 +1,33 @@ +#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 new file mode 100644 index 000000000..b0dabe1cd --- /dev/null +++ b/Source/VCGeneration/Splits/PathToken.cs @@ -0,0 +1,27 @@ +#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/Split.cs b/Source/VCGeneration/Splits/Split.cs similarity index 96% rename from Source/VCGeneration/Split.cs rename to Source/VCGeneration/Splits/Split.cs index 3eac0cb51..d34affb12 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -10,6 +10,7 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; using System.Threading.Tasks; +using VCGeneration; namespace VC { @@ -55,8 +56,6 @@ public IReadOnlyList PrunedDeclarations { int assertionCount; double assertionCost; // without multiplication by paths - public Dictionary GotoCmdOrigins { get; } - public readonly VerificationConditionGenerator /*!*/ parent; @@ -76,14 +75,11 @@ public readonly VerificationConditionGenerator /*!*/ public VerificationConditionGenerator.ErrorReporter reporter; public Split(VCGenOptions options, Func> /*!*/ getBlocks, - Dictionary /*!*/ gotoCmdOrigins, - VerificationConditionGenerator /*!*/ par, ImplementationRun run, int? randomSeed = null) + VerificationConditionGenerator /*!*/ parent, ImplementationRun run, int? randomSeed = null) { - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(par != null); + Contract.Requires(parent != null); this.getBlocks = getBlocks; - this.GotoCmdOrigins = gotoCmdOrigins; - parent = par; + this.parent = parent; this.Run = run; this.Options = options; Interlocked.Increment(ref currentId); @@ -91,17 +87,26 @@ public Split(VCGenOptions options, Func> /*!*/ getBlocks, RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0; randomGen = new Random(RandomSeed); } - - public void PrintSplit() { + + private void PrintSplit() { if (Options.PrintSplitFile == null) { return; } + + var printToConsole = Options.PrintSplitFile == "-"; + if (printToConsole) { + Thread.Sleep(100); + } - using var writer = new TokenTextWriter( - $"{Options.PrintSplitFile}-{Util.EscapeFilename(Implementation.Name)}-{SplitIndex}.spl", false, - Options.PrettyPrint, Options); + 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); - Implementation.EmitImplementation(writer, 0, Blocks, false); + Implementation.EmitImplementation(writer, 0, Blocks, false, prefix); PrintSplitDeclarations(writer); } @@ -654,7 +659,6 @@ 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); @@ -664,10 +668,6 @@ 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, newGotoCmdOrigins, parent, Run); + return new Split(Options, () => newBlocks, 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, GotoCmdOrigins, absyIds, + reporter = new VerificationConditionGenerator.ErrorReporter(Options, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs similarity index 97% rename from Source/VCGeneration/SplitAndVerifyWorker.cs rename to Source/VCGeneration/Splits/SplitAndVerifyWorker.cs index a42723458..57f3bfb33 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs @@ -39,8 +39,7 @@ public SplitAndVerifyWorker( Program program, VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, - ImplementationRun run, - Dictionary gotoCmdOrigins, + ImplementationRun run, VerifierCallback callback, ModelViewInfo mvInfo, VcOutcome vcOutcome) @@ -66,7 +65,8 @@ public SplitAndVerifyWorker( ResetPredecessors(Implementation.Blocks); - ManualSplits = ManualSplitFinder.FocusAndSplit(program, options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); + ManualSplits = ManualSplitFinder.GetParts(options, run, + (token, blocks) => new ManualSplit(options, () => blocks, verificationConditionGenerator, run, token)).ToList(); if (ManualSplits.Count == 1 && maxSplits > 1) { diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs new file mode 100644 index 000000000..8adb35a41 --- /dev/null +++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs @@ -0,0 +1,216 @@ +#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 new file mode 100644 index 000000000..d7ea8427d --- /dev/null +++ b/Source/VCGeneration/Splits/TokenWrapper.cs @@ -0,0 +1,48 @@ +#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 4362273a6..90ab89089 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -1,84 +1,70 @@ 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, out Dictionary gotoCmdOrigins) - { - Contract.Requires(impl != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Ensures(Contract.Result() != null); - - gotoCmdOrigins = new(); - Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); - Block exitBlock = null; + public static Block GenerateUnifiedExit(Implementation impl) + { + Contract.Requires(impl != null); + Contract.Ensures(Contract.Result() != null); - #region Create a unified exit block, if there's more than one + Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); + Block exitBlock = null; - { - 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); - } - } + int returnBlocks = 0; + foreach (var block in impl.Blocks.Where(block => block.TransferCmd is ReturnCmd)) + { + exitBlock = block; + returnBlocks++; + } - exitBlock = unifiedExit; - impl.Blocks.Add(unifiedExit); + 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; } - Contract.Assert(exitBlock != null); + 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); } - return exitBlock; - #endregion + exitBlock = unifiedExit; + impl.Blocks.Add(unifiedExit); } - - /// - /// 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) + + 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) { 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); @@ -89,7 +75,7 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun debugWriter.WriteLine("Effective postcondition:"); } - Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); + var formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); // (free and checked) ensures clauses foreach (Ensures ens in impl.Proc.Ensures) @@ -98,18 +84,18 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun if (!ens.Free) { - 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; + var ensuresCopy = (Ensures) cce.NonNull(ens.Clone()); + ensuresCopy.Condition = Substituter.Apply(formalProcImplSubst, ens.Condition); + AssertEnsuresCmd assert = new AssertEnsuresCmd(ensuresCopy) { + ErrorDataEnhanced = ensuresCopy.ErrorDataEnhanced + }; // Copy any {:id ...} from the postcondition to the assumption, so // we can track it while analyzing verification coverage. - c.CopyIdFrom(ens.tok, ens); - unifiedExitBlock.Cmds.Add(c); + assert.CopyIdFrom(ens.tok, ens); + unifiedExitBlock.Cmds.Add(assert); if (debugWriter != null) { - c.Emit(debugWriter, 1); + assert.Emit(debugWriter, 1); } } else if (ens.CanAlwaysAssume()) @@ -128,4 +114,12 @@ 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 731f7a1e5..f9233af03 100644 --- a/Source/VCGeneration/Transformations/RemoveBackEdges.cs +++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs @@ -9,7 +9,7 @@ namespace VCGeneration.Transformations; public class RemoveBackEdges { - private VerificationConditionGenerator generator; + private readonly 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(new Token(-17, -4), "0", new List(), + new Block(Token.NoToken, "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ConditionGeneration.ResetPredecessors(impl.Blocks); @@ -206,14 +206,7 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary GotoCmdOrigins { get; set; } public ModelViewInfo ModelViewInfo { get; set; } } @@ -114,7 +113,7 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(traceWriter, codeExpr.Blocks, + 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); @@ -327,7 +326,7 @@ void ExpandAsserts(Implementation impl) attr = ae.Ensures.Attributes; } - if (QKeyValue.FindExprAttribute(attr, "expand") != null || QKeyValue.FindBoolAttribute(attr, "expand")) + if (QKeyValue.FindExprAttribute(attr, "expand") != null || attr.FindBoolAttribute("expand")) { int depth = QKeyValue.FindIntAttribute(attr, "expand", 100); Func fe = e => Expr.Or(a.Expr, e); @@ -380,7 +379,7 @@ public override async Task VerifyImplementation(ImplementationRun run callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0); - PrepareImplementation(run, callback, out var smokeTester, out var dataGotoCmdOrigins, out var dataModelViewInfo); + PrepareImplementation(run, callback, out var smokeTester, out var dataModelViewInfo); VcOutcome vcOutcome = VcOutcome.Correct; @@ -400,15 +399,14 @@ 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], - dataGotoCmdOrigins); + var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0]); callback.OnCounterexample(cex, null); } } } } - var worker = new SplitAndVerifyWorker(program, Options, this, run, dataGotoCmdOrigins, callback, + var worker = new SplitAndVerifyWorker(program, Options, this, run, callback, dataModelViewInfo, vcOutcome); vcOutcome = await worker.WorkUntilDone(cancellationToken); @@ -427,7 +425,6 @@ 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)!; @@ -447,7 +444,7 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba if (!data.Passified) { data.Passified = true; - data.GotoCmdOrigins = gotoCmdOrigins = PassifyImpl(run, out modelViewInfo); + PassifyImpl(run, out modelViewInfo); data.ModelViewInfo = modelViewInfo; ExpandAsserts(run.Implementation); @@ -466,7 +463,6 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba else { modelViewInfo = data.ModelViewInfo; - gotoCmdOrigins = data.GotoCmdOrigins; } } @@ -475,7 +471,6 @@ public class ErrorReporter : ProverInterface.ErrorHandler { private ProofRun split; private new VCGenOptions options; - Dictionary gotoCmdOrigins; ControlFlowIdMap absyIds; @@ -491,7 +486,6 @@ 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); @@ -510,7 +504,6 @@ public override void AddCoveredElement(TrackedNodeComponent elt) } public ErrorReporter(VCGenOptions options, - Dictionary /*!*/ gotoCmdOrigins, ControlFlowIdMap /*!*/ absyIds, List /*!*/ blocks, Dictionary> debugInfos, @@ -519,13 +512,11 @@ 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; @@ -568,7 +559,7 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, Contract.Assert(traceNodes.Contains(entryBlock)); trace.Add(entryBlock); - Counterexample newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, + var newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, debugInfos, context, split, new Dictionary()); if (newCounterexample == null) @@ -580,15 +571,12 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, if (newCounterexample is ReturnCounterexample returnExample) { - foreach (var block in returnExample.Trace) + foreach (var b in returnExample.Trace) { - Contract.Assert(block != null); - Contract.Assume(block.TransferCmd != null); - var cmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); - if (cmd != null) - { - returnExample.FailingReturn = cmd; - break; + Contract.Assert(b != null); + Contract.Assume(b.TransferCmd != null); + if (b.TransferCmd.tok is GotoFromReturn gotoFromReturn) { + returnExample.FailingReturn = gotoFromReturn.Origin; } } } @@ -660,14 +648,14 @@ public void DesugarCalls(Implementation impl) } } - public Dictionary PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) + public void 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, out var gotoCmdOrigins); + var exitBlock = DesugarReturns.GenerateUnifiedExit(impl); #region Debug Tracing @@ -706,12 +694,12 @@ public Dictionary PassifyImpl(ImplementationRun run, out if (lvar.TypedIdent.WhereExpr != null) { var exp = Expr.Binary(lvar.tok, BinaryOperator.Opcode.And, lvar.TypedIdent.WhereExpr, - LiteralExpr.Literal(true)); + Expr.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 (QKeyValue.FindBoolAttribute(lvar.Attributes, "assumption")) + else if (lvar.Attributes.FindBoolAttribute("assumption")) { cc.Add(new AssumeCmd(lvar.tok, idExp, new QKeyValue(lvar.tok, "assumption_variable_initialization", new List(), null))); @@ -722,7 +710,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out InjectPreconditions(Options, run, cc); // append postconditions, starting in exitBlock and continuing into other blocks, if needed - DesugarReturns.InjectPostConditions(Options, run, exitBlock, gotoCmdOrigins); + DesugarReturns.InjectPostConditions(Options, run, exitBlock); } #endregion @@ -764,7 +752,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out modelViewInfo = new ModelViewInfo(program, impl); Convert2PassiveCmd(run, modelViewInfo); - if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation")) + if (impl.Attributes.FindBoolAttribute("may_unverified_instrumentation")) { InstrumentWithMayUnverifiedConditions(impl, exitBlock); } @@ -796,8 +784,6 @@ public Dictionary PassifyImpl(ImplementationRun run, out #endregion Peep-hole optimizations HandleSelectiveChecking(impl); - - return gotoCmdOrigins; } #region Simplified May-Unverified Analysis and Instrumentation @@ -936,13 +922,13 @@ static HashSet JoinVariableSets(HashSet c0, HashSet variables) @@ -999,8 +985,8 @@ static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet private void HandleSelectiveChecking(Implementation impl) { - if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") || - QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "selective_checking")) + if (impl.Attributes.FindBoolAttribute("selective_checking") || + impl.Proc.Attributes.FindBoolAttribute("selective_checking")) { var startPoints = new List(); foreach (var b in impl.Blocks) @@ -1008,7 +994,7 @@ private void HandleSelectiveChecking(Implementation impl) foreach (Cmd c in b.Cmds) { var p = c as PredicateCmd; - if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) + if (p != null && p.Attributes.FindBoolAttribute("start_checking_here")) { startPoints.Add(b); break; @@ -1061,7 +1047,7 @@ private void HandleSelectiveChecking(Implementation impl) foreach (Cmd c in b.Cmds) { var p = c as PredicateCmd; - if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) + if (p != null && p.Attributes.FindBoolAttribute("start_checking_here")) { copyMode = true; } @@ -1367,12 +1353,11 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, - Block implEntryBlock, Dictionary gotoCmdOrigins) + Block implEntryBlock) { Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); - Contract.Requires(gotoCmdOrigins != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; @@ -1445,7 +1430,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options { Contract.Assert(block != null); Contract.Assume(block.TransferCmd != null); - returnCmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); + returnCmd = block.TransferCmd.tok is GotoFromReturn gotoFromReturn ? gotoFromReturn.Origin : null; if (returnCmd != null) { break; diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index 15e3a2cdb..d5b130748 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -28,17 +28,9 @@ public void ComputePerAssertOutcomes(out Dictionary pe if (Outcome == SolverOutcome.Valid) { perAssertOutcome = Asserts.ToDictionary(cmd => cmd, _ => SolverOutcome.Valid); } else { - 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; - } + foreach (var counterExample in CounterExamples) + { + var underlyingAssert = counterExample.FailingAssert; // We ensure that the underlyingAssert is among the original asserts if (!Asserts.Contains(underlyingAssert)) { diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 84090f10a..7857e5142 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 = QKeyValue.FindBoolAttribute(ac.Attributes, "try"); + var isTry = ac.Attributes.FindBoolAttribute("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 = QKeyValue.FindBoolAttribute(ac.Attributes, "soft"); + var soft = ac.Attributes.FindBoolAttribute("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 28481b41e..7f04782a6 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 de1be84d4..650e46069 100644 --- a/Test/aitest0/Issue25.bpl.expect +++ b/Test/aitest0/Issue25.bpl.expect @@ -1,8 +1,8 @@ -Issue25.bpl(12,1): Error: a postcondition could not be proved on this return path +Issue25.bpl(12,3): 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,3): anon0 - Issue25.bpl(12,1): anon2_LoopHead - Issue25.bpl(12,1): anon2_LoopDone + Issue25.bpl(11,5): anon0 + Issue25.bpl(12,3): anon2_LoopHead + Issue25.bpl(12,3): anon2_LoopDone Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl index 2e3878802..50425d6e9 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/pruning/Focus.bpl b/Test/implementationDivision/focus/focus.bpl similarity index 100% rename from Test/pruning/Focus.bpl rename to Test/implementationDivision/focus/focus.bpl diff --git a/Test/pruning/Focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect similarity index 50% rename from Test/pruning/Focus.bpl.expect rename to Test/implementationDivision/focus/focus.bpl.expect index 71c2b6338..2c28a1a35 100644 --- a/Test/pruning/Focus.bpl.expect +++ b/Test/implementationDivision/focus/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/implementationDivision/isolateAssertion/isolateAssertion.bpl b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl new file mode 100644 index 000000000..59cd30f93 --- /dev/null +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl @@ -0,0 +1,42 @@ +// 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 new file mode 100644 index 000000000..27589907d --- /dev/null +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect @@ -0,0 +1,183 @@ +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 new file mode 100644 index 000000000..d40ee651c --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl @@ -0,0 +1,38 @@ +// 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 new file mode 100644 index 000000000..3c47dc663 --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect @@ -0,0 +1,126 @@ +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/test0/AssumeFalseSplit/AssumeFalseSplit.bpl b/Test/implementationDivision/split/AssumeFalseSplit.bpl similarity index 50% rename from Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl rename to Test/implementationDivision/split/AssumeFalseSplit.bpl index 148216280..92c6bb87f 100644 --- a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl +++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl @@ -1,8 +1,5 @@ -// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" +// RUN: %boogie /printSplit:- "%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/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect new file mode 100644 index 000000000..29725f4eb --- /dev/null +++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect @@ -0,0 +1,36 @@ +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/test0/Split/Split.bpl b/Test/implementationDivision/split/Split.bpl similarity index 64% rename from Test/test0/Split/Split.bpl rename to Test/implementationDivision/split/Split.bpl index e99d76351..4c7fdaf45 100644 --- a/Test/test0/Split/Split.bpl +++ b/Test/implementationDivision/split/Split.bpl @@ -1,9 +1,5 @@ -// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" +// RUN: %boogie /printSplit:- "%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/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect new file mode 100644 index 000000000..9f213b896 --- /dev/null +++ b/Test/implementationDivision/split/Split.bpl.expect @@ -0,0 +1,112 @@ +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/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 15351bb11..1fccbd8bf 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--1.spl" +// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.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/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -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 deleted file mode 100644 index c8727ad27..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index 29ba05d16..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index 838d5aebd..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index 79578bccc..000000000 --- a/Test/test0/Split/Foo.split.0.bpl.expect +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index 37297e028..000000000 --- a/Test/test0/Split/Foo.split.1.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -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 deleted file mode 100644 index 7f28a2ebf..000000000 --- a/Test/test0/Split/Foo.split.2.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -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 deleted file mode 100644 index eb031aa38..000000000 --- a/Test/test0/Split/Foo.split.3.bpl.expect +++ /dev/null @@ -1,35 +0,0 @@ -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 deleted file mode 100644 index 83b9850a7..000000000 --- a/Test/test0/Split/Foo.split.4.bpl.expect +++ /dev/null @@ -1,31 +0,0 @@ -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/test0/Split/Split.bpl.expect b/Test/test0/Split/Split.bpl.expect deleted file mode 100644 index 67f8e9921..000000000 --- a/Test/test0/Split/Split.bpl.expect +++ /dev/null @@ -1,5 +0,0 @@ -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 c883fb50c..e459892fd 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 a349c0d87..22c885b42 100644 --- a/Test/test2/Structured.bpl.expect +++ b/Test/test2/Structured.bpl.expect @@ -22,6 +22,5 @@ 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 From 160b0f7af0e1a8cb7b59391eae995afc6dfa9d57 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Oct 2024 15:23:18 +0200 Subject: [PATCH 2/4] Fix problems with isolate each assertion and isolating jumps --- Source/Core/AST/GotoBoogie/ImplicitJump.cs | 10 ++ .../BigBlocksResolutionContext.cs | 5 +- .../Splits => Core/Generic}/TokenWrapper.cs | 0 Source/Directory.Build.props | 2 +- .../IsolateAttributeOnAssertsHandler.cs | 17 +-- .../Splits/IsolateAttributeOnJumpsHandler.cs | 7 +- .../VCGeneration/Splits/ManualSplitFinder.cs | 27 +++-- .../isolateJumpAndSplitOnEveryAssert.bpl | 27 +++++ ...solateJumpAndSplitOnEveryAssert.bpl.expect | 100 ++++++++++++++++++ 9 files changed, 174 insertions(+), 21 deletions(-) create mode 100644 Source/Core/AST/GotoBoogie/ImplicitJump.cs rename Source/{VCGeneration/Splits => Core/Generic}/TokenWrapper.cs (100%) create mode 100644 Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl create mode 100644 Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect diff --git a/Source/Core/AST/GotoBoogie/ImplicitJump.cs b/Source/Core/AST/GotoBoogie/ImplicitJump.cs new file mode 100644 index 000000000..655f847c0 --- /dev/null +++ b/Source/Core/AST/GotoBoogie/ImplicitJump.cs @@ -0,0 +1,10 @@ +#nullable enable +using Microsoft.Boogie; + +namespace VCGeneration; + +public class ImplicitJump : TokenWrapper { + public ImplicitJump(IToken inner) : base(inner) + { + } +} \ No newline at end of file diff --git a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs index b53bc3606..a6974fc07 100644 --- a/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using VCGeneration; namespace Microsoft.Boogie; @@ -581,11 +582,11 @@ TransferCmd GotoSuccessor(IToken tok, BigBlock b) Contract.Ensures(Contract.Result() != null); if (b.successorBigBlock != null) { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + return new GotoCmd(new ImplicitJump(tok), new List {b.successorBigBlock.LabelName}); } else { - return new ReturnCmd(tok); + return new ReturnCmd(new ImplicitJump(tok)); } } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/TokenWrapper.cs b/Source/Core/Generic/TokenWrapper.cs similarity index 100% rename from Source/VCGeneration/Splits/TokenWrapper.cs rename to Source/Core/Generic/TokenWrapper.cs diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index ec349a347..b36443f38 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.3.2 + 3.3.4 net6.0 false Boogie diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs index 1d90a36e0..f08ee284f 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -61,7 +61,8 @@ List GetCommands(Block oldBlock) => : oldBlock.Cmds.Select(rewriter.TransformAssertCmd).ToList(); var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToKeep, GetCommands); - return rewriter.CreateSplit(new IsolatedAssertionOrigin(assertCmd), newBlocks); + var origin = new IsolatedAssertionOrigin(partToDivide.Token, assertCmd); + return rewriter.CreateSplit(origin, newBlocks); } List GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert) @@ -79,14 +80,13 @@ List GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert) } ManualSplit GetSplitWithoutIsolatedAssertions() { - var origin = new ImplementationRootOrigin(partToDivide.Implementation); if (!isolatedAssertions.Any()) { - return rewriter.CreateSplit(origin, partToDivide.Blocks); + return rewriter.CreateSplit(partToDivide.Token, partToDivide.Blocks); } - var (newBlocks, mapping) = rewriter.ComputeNewBlocks(null, GetCommands); + var (newBlocks, _) = rewriter.ComputeNewBlocks(null, GetCommands); - return rewriter.CreateSplit(origin, newBlocks); + return rewriter.CreateSplit(partToDivide.Token, newBlocks); List GetCommands(Block block) => block.Cmds.Select(cmd => isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList(); @@ -94,13 +94,14 @@ List GetCommands(Block block) => block.Cmds.Select(cmd => } } - public class IsolatedAssertionOrigin : TokenWrapper, IImplementationPartOrigin { + public IImplementationPartOrigin Origin { get; } public AssertCmd IsolatedAssert { get; } - public IsolatedAssertionOrigin(AssertCmd isolatedAssert) : base(isolatedAssert.tok) { + public IsolatedAssertionOrigin(IImplementationPartOrigin origin, AssertCmd isolatedAssert) : base(isolatedAssert.tok) { + Origin = origin; this.IsolatedAssert = isolatedAssert; } - public string ShortName => $"/assert@{IsolatedAssert.Line}"; + public string ShortName => $"{Origin.ShortName}/assert@{IsolatedAssert.Line}"; } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index 5f7c1de04..1b38445e6 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -44,11 +44,16 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var blocksToInclude = ancestors.Union(descendants).ToHashSet(); var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin; + if (originalReturn.tok is ImplicitJump) { + continue; + } + 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)); + var origin = new ReturnOrigin(originalReturn); + results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, origin)); } else { var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, ancestors.ToHashSet()); results.Add(rewriter.CreateSplit(new ReturnOrigin(originalReturn), newBlocks)); diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs index b1b8e676b..934a2aa40 100644 --- a/Source/VCGeneration/Splits/ManualSplitFinder.cs +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -14,17 +14,26 @@ public static IEnumerable GetParts(VCGenOptions options, Implementa Func, ManualSplit> createPart) { var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart); - var result = focussedParts.SelectMany(focussedPart => { + 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; + return new[] { withoutIsolatedJumps }.Concat(isolatedJumps).SelectMany(isolatedJumpSplit => + { + var (isolatedAssertions, withoutIsolatedAssertions) = + IsolateAttributeOnAssertsHandler.GetParts(options, isolatedJumpSplit, createPart); + + var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); + return isolatedAssertions.Concat(splitParts); + }); + }).Where(s => s.Asserts.Any()).ToList(); + + if (result.Any()) + { + return result; + } + + return focussedParts.Take(1); } } diff --git a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl new file mode 100644 index 000000000..f6ea9ab53 --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure {:vcs_split_on_every_assert} MergeAtEnd(x: int) returns (r: int) + ensures r > 1; +{ + if (x > 0) { + r := 1; + } + else { + r := 2; + } +} + +procedure {:vcs_split_on_every_assert} MultipleEnsures(x: int) returns (r: int) + ensures r > 1; + ensures r < 10; +{ + if (x > 0) { + r := 1; + return; + } + else { + r := 20; + return; + } +} \ No newline at end of file diff --git a/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect new file mode 100644 index 000000000..a48405e1e --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect @@ -0,0 +1,100 @@ +implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns (r: int) +{ + + anon0: + goto anon3_Then, anon3_Else; + + anon3_Then: + assume {:partition} x > 0; + assume r#AT#0 == 1; + goto GeneratedUnifiedExit; + + anon3_Else: + assume {:partition} 0 >= x; + assume r#AT#0 == 2; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#0 > 1; + return; +} + + +isolateJumpAndSplitOnEveryAssert.bpl(9,3): Error: a postcondition could not be proved on this return path +isolateJumpAndSplitOnEveryAssert.bpl(5,3): Related location: this is the postcondition that could not be proved +implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(x: int) returns (r: int) +{ + + anon0: + goto anon3_Else; + + anon3_Else: + assume {:partition} 0 >= x; + assume r#AT#0 == 20; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#0 > 1; + return; +} + + +implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(x: int) returns (r: int) +{ + + anon0: + goto anon3_Else; + + anon3_Else: + assume {:partition} 0 >= x; + assume r#AT#0 == 20; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assume r#AT#0 > 1; + assert r#AT#0 < 10; + return; +} + + +implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(x: int) returns (r: int) +{ + + anon0: + goto anon3_Then; + + anon3_Then: + assume {:partition} x > 0; + assume r#AT#0 == 1; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#0 > 1; + return; +} + + +implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@17(x: int) returns (r: int) +{ + + anon0: + goto anon3_Then; + + anon3_Then: + assume {:partition} x > 0; + assume r#AT#0 == 1; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assume r#AT#0 > 1; + assert r#AT#0 < 10; + return; +} + + +isolateJumpAndSplitOnEveryAssert.bpl(21,5): Error: a postcondition could not be proved on this return path +isolateJumpAndSplitOnEveryAssert.bpl(16,3): Related location: this is the postcondition that could not be proved +isolateJumpAndSplitOnEveryAssert.bpl(25,5): Error: a postcondition could not be proved on this return path +isolateJumpAndSplitOnEveryAssert.bpl(17,3): Related location: this is the postcondition that could not be proved + +Boogie program verifier finished with 0 verified, 3 errors From f27d1ebd940c438990b9aa59e5507138d460ed7e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Oct 2024 16:49:02 +0200 Subject: [PATCH 3/4] Update expect file --- Test/commandline/SplitOnEveryAssert.bpl | 2 +- .../isolateJump/isolateJump.bpl.expect | 66 +++++++++---------- Test/test0/SplitOnEveryAssert.bpl | 2 +- 3 files changed, 35 insertions(+), 35 deletions(-) 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/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect index 3c47dc663..9c32be2a1 100644 --- a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect @@ -1,3 +1,33 @@ +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; +} + + implementation IsolateReturn/return@16(x: int, y: int) returns (r: int) { @@ -28,7 +58,9 @@ implementation IsolateReturn/return@16(x: int, y: int) returns (r: int) } -implementation IsolateReturn(x: int, y: int) returns (r: int) +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(x: int, y: int) returns (r: int) { anon0: @@ -58,8 +90,6 @@ implementation IsolateReturn(x: int, y: int) returns (r: int) } -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) { @@ -90,36 +120,6 @@ implementation IsolateReturnPaths/assert@34[29](x: int, y: int) returns (r: int) } -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 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.* From 4cbed7f436bb3932acd351d3cebbfae2d5b02c8a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 21 Oct 2024 18:09:17 +0200 Subject: [PATCH 4/4] Refactoring to make code more robust --- Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs index 1b38445e6..9a26ea973 100644 --- a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -44,7 +44,8 @@ public static (List Isolated, ManualSplit Remainder) GetParts(VCGen var blocksToInclude = ancestors.Union(descendants).ToHashSet(); var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin; - if (originalReturn.tok is ImplicitJump) { + var returnWasFromOriginalSource = originalReturn.tok is not Token; + if (returnWasFromOriginalSource) { continue; }