From 8e4eecb48dd8092e4dab59d9716907332d457802 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 7 Oct 2024 18:08:40 +0200 Subject: [PATCH] Extracted refactorings from https://github.com/boogie-org/boogie/pull/960 (#961) Extracted classes into separate files, corrected variable names, and moved some methods to extension classes --- Source/Core/AST/Absy.cs | 12 +- Source/Core/AST/AbsyQuant.cs | 274 ---- Source/Core/AST/{ => Commands}/AbsyCmd.cs | 1397 +---------------- Source/Core/AST/{ => Commands}/CallCmd.cs | 4 +- .../Core/AST/{ => Commands}/HideRevealCmd.cs | 0 Source/Core/AST/{ => GotoBoogie}/Block.cs | 20 +- .../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 | 16 +- Source/Core/AST/Implementation.cs | 2 +- Source/Core/AST/Program.cs | 6 +- 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 | 6 +- Source/Core/CivlAttributes.cs | 2 +- Source/Core/FunctionDependencyChecker.cs | 16 +- Source/Core/Inline.cs | 2 +- Source/Core/Parser.cs | 6 +- Source/Core/ResolutionContext.cs | 4 +- Source/Core/VariableDependenceAnalyser.cs | 2 +- Source/ExecutionEngine/ExecutionEngine.cs | 2 +- .../Houdini/AnnotationDependenceAnalyser.cs | 8 +- Source/Houdini/Houdini.cs | 2 +- Source/VCGeneration/ConditionGeneration.cs | 12 +- .../VCGeneration/Prune/DependencyEvaluator.cs | 2 +- Source/VCGeneration/Prune/Pruner.cs | 2 +- Source/VCGeneration/SmokeTester.cs | 2 +- .../Splits/FocusAttributeHandler.cs | 2 +- .../Splits/SplitAttributeHandler.cs | 2 +- .../VerificationConditionGenerator.cs | 18 +- Source/VCGeneration/Wlp.cs | 4 +- 43 files changed, 1806 insertions(+), 1752 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 (91%) 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 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 97b66daf7..0beaa357b 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/Commands/AbsyCmd.cs @@ -7,1187 +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++; - } - - 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); - } - } - } - - [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))] @@ -1225,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; @@ -1693,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 @@ -3398,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 @@ -3441,187 +2231,4 @@ public override void Emit(TokenTextWriter stream, int level) throw new NotImplementedException(); } } - - 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); - } - } - - 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); - } - } } 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 f20360987..0f0ed662c 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/Commands/CallCmd.cs @@ -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); 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 91% rename from Source/Core/AST/Block.cs rename to Source/Core/AST/GotoBoogie/Block.cs index 4cb78df21..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,18 +114,18 @@ void ObjectInvariant() { Contract.Invariant(this.label != null); Contract.Invariant(this.cmds != null); - Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); + Contract.Invariant(cce.NonNullElements(this.liveVarsBefore, true)); } public bool IsLive(Variable v) { Contract.Requires(v != null); - if (liveVarsBefore == null) + if (LiveVarsBefore == null) { return true; } - return liveVarsBefore.Contains(v); + return LiveVarsBefore.Contains(v); } public static Block ShallowClone(Block block) { @@ -147,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 1f9bbf412..b20edeaad 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -39,22 +39,20 @@ 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 destination, IToken tok, ICarriesAttributes src) { diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs index 7a6c565ac..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; diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 82ec6e4ba..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); } 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 eecb93c6b..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); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index ad5250f33..8c6e77732 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/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/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 cc67d930f..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); 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/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 46df39226..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); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 7cc6abc0c..f206c6612 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; 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/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8188ebb07..13ee3a18a 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -764,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. @@ -1037,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() @@ -1062,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)) @@ -1210,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); @@ -1238,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) @@ -1273,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()); 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/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs index b9d327250..812d80407 100644 --- a/Source/VCGeneration/Splits/FocusAttributeHandler.cs +++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs @@ -111,6 +111,6 @@ private static HashSet DominatedBlocks(List topologicallySortedBlo } private static bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); + return c is PredicateCmd p && p.Attributes.FindBoolAttribute("focus"); } } \ No newline at end of file diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs index 4e145da9d..8adb35a41 100644 --- a/Source/VCGeneration/Splits/SplitAttributeHandler.cs +++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs @@ -74,7 +74,7 @@ private static bool ShouldSplitHere(Cmd c) { return false; } - return QKeyValue.FindBoolAttribute(predicateCmd.Attributes, "split_here"); + return predicateCmd.Attributes.FindBoolAttribute("split_here"); } private static Dictionary GetMapFromBlockStartToSplit(List blocks, Dictionary> splitsPerBlock) { diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index 9187d39c8..8c41526b2 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -326,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); @@ -699,7 +699,7 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) 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))); @@ -752,7 +752,7 @@ public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) 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); } @@ -922,13 +922,13 @@ static HashSet JoinVariableSets(HashSet c0, HashSet variables) @@ -985,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) @@ -994,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; @@ -1047,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; } 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) {