From 54535419ce28d0fb1126f757468a3f58dc13489b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:12:41 +0200 Subject: [PATCH 1/8] Extract Source/Core/AST/BigBlocksResolutionContext.cs into a separate file, and IfCmd as well --- Source/Concurrency/LinearTypeChecker.cs | 10 +- Source/Core/AST/AbsyCmd.cs | 693 +----------------- Source/Core/AST/BigBlocksResolutionContext.cs | 599 +++++++++++++++ Source/Core/AST/IfCmd.cs | 106 +++ 4 files changed, 711 insertions(+), 697 deletions(-) create mode 100644 Source/Core/AST/BigBlocksResolutionContext.cs create mode 100644 Source/Core/AST/IfCmd.cs diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 2e3fb6aa8..848c82dfe 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -773,14 +773,14 @@ void ProcessIfCmd(IfCmd ifCmd) { checkingContext.Error(ifCmd.tok, "access to linear store not allowed"); } - stmtLists.Push(ifCmd.thn); - if (ifCmd.elseIf != null) + stmtLists.Push(ifCmd.Thn); + if (ifCmd.ElseIf != null) { - ProcessIfCmd(ifCmd.elseIf); + ProcessIfCmd(ifCmd.ElseIf); } - else if (ifCmd.elseBlock != null) + else if (ifCmd.ElseBlock != null) { - stmtLists.Push(ifCmd.elseBlock); + stmtLists.Push(ifCmd.ElseBlock); } } ProcessIfCmd(ifCmd); diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index a6400e232..5a4d6d493 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -350,593 +350,7 @@ public void AddLocalVariable(string name) // TODO } } - - class BigBlocksResolutionContext - { - StmtList /*!*/ - stmtList; - - [Peer] List blocks; - - string /*!*/ - prefix = "anon"; - - int anon = 0; - - int FreshAnon() - { - return anon++; - } - - HashSet allLabels = new HashSet(); - - Errors /*!*/ - errorHandler; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(stmtList != null); - Contract.Invariant(cce.NonNullElements(blocks, true)); - Contract.Invariant(prefix != null); - Contract.Invariant(cce.NonNullElements(allLabels, true)); - Contract.Invariant(errorHandler != null); - } - - private void ComputeAllLabels(StmtList stmts) - { - if (stmts == null) - { - return; - } - - foreach (BigBlock bb in stmts.BigBlocks) - { - if (bb.LabelName != null) - { - allLabels.Add(bb.LabelName); - } - - ComputeAllLabels(bb.ec); - } - } - - private void ComputeAllLabels(StructuredCmd cmd) - { - if (cmd == null) - { - return; - } - - if (cmd is IfCmd) - { - IfCmd ifCmd = (IfCmd) cmd; - ComputeAllLabels(ifCmd.thn); - ComputeAllLabels(ifCmd.elseIf); - ComputeAllLabels(ifCmd.elseBlock); - } - else if (cmd is WhileCmd) - { - WhileCmd whileCmd = (WhileCmd) cmd; - ComputeAllLabels(whileCmd.Body); - } - } - - public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler) - { - Contract.Requires(errorHandler != null); - Contract.Requires(stmtList != null); - this.stmtList = stmtList; - // Inject an empty big block at the end of the body of a while loop if its current end is another while loop. - // This transformation creates a suitable jump target for break statements inside the nested while loop. - InjectEmptyBigBlockInsideWhileLoopBody(stmtList); - this.errorHandler = errorHandler; - ComputeAllLabels(stmtList); - } - - public List /*!*/ Blocks - { - get - { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (blocks == null) - { - blocks = new List(); - - int startErrorCount = this.errorHandler.count; - // Check that all goto statements go to a label in allLabels, and no break statement to a non-enclosing loop. - // Also, determine a good value for "prefix". - CheckLegalLabels(stmtList, null, null); - - // fill in names of anonymous blocks - NameAnonymousBlocks(stmtList); - - // determine successor blocks - RecordSuccessors(stmtList, null); - - if (this.errorHandler.count == startErrorCount) - { - // generate blocks from the big blocks - CreateBlocks(stmtList, null); - } - } - - return blocks; - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StmtList stmtList) - { - foreach (var bb in stmtList.BigBlocks) - { - InjectEmptyBigBlockInsideWhileLoopBody(bb.ec); - } - } - - void InjectEmptyBigBlockInsideWhileLoopBody(StructuredCmd structuredCmd) - { - if (structuredCmd is WhileCmd whileCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(whileCmd.Body); - if (whileCmd.Body.BigBlocks.Count > 0 && whileCmd.Body.BigBlocks.Last().ec is WhileCmd) - { - var newBigBlocks = new List(whileCmd.Body.BigBlocks); - newBigBlocks.Add(new BigBlock(Token.NoToken, null, new List(), null, null)); - whileCmd.Body = new StmtList(newBigBlocks, whileCmd.Body.EndCurly); - } - } - else if (structuredCmd is IfCmd ifCmd) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.thn); - if (ifCmd.elseBlock != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseBlock); - } - - if (ifCmd.elseIf != null) - { - InjectEmptyBigBlockInsideWhileLoopBody(ifCmd.elseIf); - } - } - } - - void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parentBigBlock) - { - Contract.Requires(stmtList != null); - Contract.Requires((parentContext == null) == (parentBigBlock == null)); - Contract.Requires(stmtList.ParentContext == null); // it hasn't been set yet - //modifies stmtList.*; - Contract.Ensures(stmtList.ParentContext == parentContext); - stmtList.ParentContext = parentContext; - stmtList.ParentBigBlock = parentBigBlock; - - // record the labels declared in this StmtList - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName != null) - { - string n = b.LabelName; - if (n.StartsWith(prefix)) - { - if (prefix.Length < n.Length && n[prefix.Length] == '0') - { - prefix += "1"; - } - else - { - prefix += "0"; - } - } - - stmtList.AddLabel(b.LabelName); - } - } - - // check that labels in this and nested StmtList's are legal - foreach (BigBlock b in stmtList.BigBlocks) - { - // goto's must reference blocks in enclosing blocks - if (b.tc is GotoCmd) - { - GotoCmd g = (GotoCmd) b.tc; - foreach (string /*!*/ lbl in cce.NonNull(g.LabelNames)) - { - Contract.Assert(lbl != null); - /* - bool found = false; - for (StmtList sl = stmtList; sl != null; sl = sl.ParentContext) { - if (sl.Labels.Contains(lbl)) { - found = true; - break; - } - } - if (!found) { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined or out of reach"); - } - */ - if (!allLabels.Contains(lbl)) - { - this.errorHandler.SemErr(g.tok, "Error: goto label '" + lbl + "' is undefined"); - } - } - } - - // break labels must refer to an enclosing while statement - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure == null); // it hasn't been initialized yet - bool found = false; - for (StmtList sl = stmtList; sl.ParentBigBlock != null; sl = sl.ParentContext) - { - cce.LoopInvariant(sl != null); - BigBlock bb = sl.ParentBigBlock; - - if (bcmd.Label == null) - { - // a label-less break statement breaks out of the innermost enclosing while statement - if (bb.ec is WhileCmd) - { - bcmd.BreakEnclosure = bb; - found = true; - break; - } - } - else if (bcmd.Label == bb.LabelName) - { - // a break statement with a label can break out of both if statements and while statements - if (bb.simpleCmds.Count == 0) - { - // this is a good target: the label refers to the if/while statement - bcmd.BreakEnclosure = bb; - } - else - { - // the label of bb refers to the first statement of bb, which in which case is a simple statement, not an if/while statement - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - - found = true; // don't look any further, since we've found a matching label - break; - } - } - - if (!found) - { - if (bcmd.Label == null) - { - this.errorHandler.SemErr(bcmd.tok, "Error: break statement is not inside a loop"); - } - else - { - this.errorHandler.SemErr(bcmd.tok, - "Error: break label '" + bcmd.Label + "' must designate an enclosing statement"); - } - } - } - - // recurse - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - CheckLegalLabels(wcmd.Body, stmtList, b); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - CheckLegalLabels(ifcmd.thn, stmtList, b); - if (ifcmd.elseBlock != null) - { - CheckLegalLabels(ifcmd.elseBlock, stmtList, b); - } - } - } - } - } - - void NameAnonymousBlocks(StmtList stmtList) - { - Contract.Requires(stmtList != null); - foreach (BigBlock b in stmtList.BigBlocks) - { - if (b.LabelName == null) - { - b.LabelName = prefix + FreshAnon(); - } - - if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - NameAnonymousBlocks(wcmd.Body); - } - else - { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - NameAnonymousBlocks(ifcmd.thn); - if (ifcmd.elseBlock != null) - { - NameAnonymousBlocks(ifcmd.elseBlock); - } - } - } - } - } - - void RecordSuccessors(StmtList stmtList, BigBlock successor) - { - Contract.Requires(stmtList != null); - for (int i = stmtList.BigBlocks.Count; 0 <= --i;) - { - BigBlock big = stmtList.BigBlocks[i]; - big.successorBigBlock = successor; - - if (big.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) big.ec; - RecordSuccessors(wcmd.Body, big); - } - else - { - for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) - { - RecordSuccessors(ifcmd.thn, successor); - if (ifcmd.elseBlock != null) - { - RecordSuccessors(ifcmd.elseBlock, successor); - } - } - } - - successor = big; - } - } - - // If the enclosing context is a loop, then "runOffTheEndLabel" is the loop head label; - // otherwise, it is null. - void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) - { - Contract.Requires(stmtList != null); - Contract.Requires(blocks != null); - List cmdPrefixToApply = stmtList.PrefixCommands; - - int n = stmtList.BigBlocks.Count; - foreach (BigBlock b in stmtList.BigBlocks) - { - n--; - Contract.Assert(b.LabelName != null); - List theSimpleCmds; - if (cmdPrefixToApply == null) - { - theSimpleCmds = b.simpleCmds; - } - else - { - theSimpleCmds = new List(); - theSimpleCmds.AddRange(cmdPrefixToApply); - theSimpleCmds.AddRange(b.simpleCmds); - cmdPrefixToApply = null; // now, we've used 'em up - } - - if (b.tc != null) - { - // this BigBlock has the very same components as a Block - Contract.Assert(b.ec == null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, b.tc); - blocks.Add(block); - } - else if (b.ec == null) - { - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(stmtList.EndCurly, b); - } - - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, trCmd); - blocks.Add(block); - } - else if (b.ec is BreakCmd) - { - BreakCmd bcmd = (BreakCmd) b.ec; - Contract.Assert(bcmd.BreakEnclosure != null); - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, GotoSuccessor(b.ec.tok, bcmd.BreakEnclosure)); - blocks.Add(block); - } - else if (b.ec is WhileCmd) - { - WhileCmd wcmd = (WhileCmd) b.ec; - var a = FreshAnon(); - string loopHeadLabel = prefix + a + "_LoopHead"; - string /*!*/ - loopBodyLabel = prefix + a + "_LoopBody"; - string loopDoneLabel = prefix + a + "_LoopDone"; - - List ssBody = new List(); - List ssDone = new List(); - if (wcmd.Guard != null) - { - var ac = new AssumeCmd(wcmd.tok, wcmd.Guard); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssBody.Add(ac); - - ac = new AssumeCmd(wcmd.tok, Expr.Not(wcmd.Guard)); - ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List(), null); - ssDone.Add(ac); - } - - // Try to squeeze in ssBody into the first block of wcmd.Body - bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); - - // ... goto LoopHead; - Block block = new Block(b.tok, b.LabelName, theSimpleCmds, - new GotoCmd(wcmd.tok, new List {loopHeadLabel})); - blocks.Add(block); - - // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; - List ssHead = new List(); - foreach (CallCmd yield in wcmd.Yields) - { - ssHead.Add(yield); - } - foreach (PredicateCmd inv in wcmd.Invariants) - { - ssHead.Add(inv); - } - - block = new Block(wcmd.tok, loopHeadLabel, ssHead, - new GotoCmd(wcmd.tok, new List {loopDoneLabel, loopBodyLabel})); - blocks.Add(block); - - if (!bodyGuardTakenCareOf) - { - // LoopBody: assume guard; goto firstLoopBlock; - block = new Block(wcmd.tok, loopBodyLabel, ssBody, - new GotoCmd(wcmd.tok, new List {wcmd.Body.BigBlocks[0].LabelName})); - blocks.Add(block); - } - - // recurse to create the blocks for the loop body - CreateBlocks(wcmd.Body, loopHeadLabel); - - // LoopDone: assume !guard; goto loopSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(wcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(wcmd.tok, b); - } - - block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd); - blocks.Add(block); - } - else - { - IfCmd ifcmd = (IfCmd) b.ec; - string predLabel = b.LabelName; - List predCmds = theSimpleCmds; - - for (; ifcmd != null; ifcmd = ifcmd.elseIf) - { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; - Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; - Contract.Assert(elseLabel != null); - - List ssThen = new List(); - List ssElse = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssThen.Add(ac); - - ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - ssElse.Add(ac); - } - - // Try to squeeze in ssThen/ssElse into the first block of ifcmd.thn/ifcmd.elseBlock - bool thenGuardTakenCareOf = ifcmd.thn.PrefixFirstBlock(ssThen, ref thenLabel); - bool elseGuardTakenCareOf = false; - if (ifcmd.elseBlock != null) - { - elseGuardTakenCareOf = ifcmd.elseBlock.PrefixFirstBlock(ssElse, ref elseLabel); - } - - // ... goto Then, Else; - var jumpBlock = new Block(b.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); - blocks.Add(jumpBlock); - - if (!thenGuardTakenCareOf) - { - // Then: assume guard; goto firstThenBlock; - var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen, - new GotoCmd(ifcmd.tok, new List {ifcmd.thn.BigBlocks[0].LabelName})); - blocks.Add(thenJumpBlock); - } - - // recurse to create the blocks for the then branch - CreateBlocks(ifcmd.thn, n == 0 ? runOffTheEndLabel : null); - - if (ifcmd.elseBlock != null) - { - Contract.Assert(ifcmd.elseIf == null); - if (!elseGuardTakenCareOf) - { - // Else: assume !guard; goto firstElseBlock; - var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.elseBlock.BigBlocks[0].LabelName})); - blocks.Add(elseJumpBlock); - } - - // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.elseBlock, n == 0 ? runOffTheEndLabel : null); - } - else if (ifcmd.elseIf != null) - { - // this is an "else if" - predLabel = elseLabel; - predCmds = new List(); - if (ifcmd.Guard != null) - { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); - predCmds.Add(ac); - } - } - else - { - // no else alternative is specified, so else branch is just "skip" - // Else: assume !guard; goto ifSuccessor; - TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) - { - // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); - } - else - { - trCmd = GotoSuccessor(ifcmd.tok, b); - } - - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); - blocks.Add(block); - } - } - } - } - } - - TransferCmd GotoSuccessor(IToken tok, BigBlock b) - { - Contract.Requires(b != null); - Contract.Requires(tok != null); - Contract.Ensures(Contract.Result() != null); - if (b.successorBigBlock != null) - { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); - } - else - { - return new ReturnCmd(tok); - } - } - } - + [ContractClass(typeof(StructuredCmdContracts))] public abstract class StructuredCmd { @@ -986,111 +400,6 @@ 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; diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs new file mode 100644 index 000000000..4e66238e2 --- /dev/null +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -0,0 +1,599 @@ +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. + private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) + { + Contract.Requires(stmtList != null); + Contract.Requires(blocks != null); + List cmdPrefixToApply = stmtList.PrefixCommands; + + int n = stmtList.BigBlocks.Count; + foreach (var bigBlock in stmtList.BigBlocks) + { + n--; + Contract.Assert(bigBlock.LabelName != null); + List theSimpleCmds; + if (cmdPrefixToApply == null) + { + theSimpleCmds = bigBlock.simpleCmds; + } + else + { + theSimpleCmds = new List(); + theSimpleCmds.AddRange(cmdPrefixToApply); + theSimpleCmds.AddRange(bigBlock.simpleCmds); + cmdPrefixToApply = null; // now, we've used 'em up + } + + if (bigBlock.tc != null) + { + // this BigBlock has the very same components as a Block + Contract.Assert(bigBlock.ec == null); + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc); + blocks.Add(block); + } + else + { + switch (bigBlock.ec) + { + case 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, bigBlock); + } + + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd); + blocks.Add(block); + break; + } + case BreakCmd ec: + { + Contract.Assert(ec.BreakEnclosure != null); + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(ec.tok, ec.BreakEnclosure)); + blocks.Add(block); + break; + } + case WhileCmd 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 (ec.Guard != null) + { + var ac = new AssumeCmd(ec.tok, ec.Guard); + ac.Attributes = new QKeyValue(ec.tok, "partition", new List(), null); + ssBody.Add(ac); + + ac = new AssumeCmd(ec.tok, Expr.Not(ec.Guard)); + ac.Attributes = new QKeyValue(ec.tok, "partition", new List(), null); + ssDone.Add(ac); + } + + // Try to squeeze in ssBody into the first block of wcmd.Body + bool bodyGuardTakenCareOf = ec.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); + + // ... goto LoopHead; + Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, + new GotoCmd(ec.tok, new List {loopHeadLabel})); + blocks.Add(block); + + // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; + List ssHead = new List(); + foreach (CallCmd yield in ec.Yields) + { + ssHead.Add(yield); + } + foreach (PredicateCmd inv in ec.Invariants) + { + ssHead.Add(inv); + } + + block = new Block(ec.tok, loopHeadLabel, ssHead, + new GotoCmd(ec.tok, new List {loopDoneLabel, loopBodyLabel})); + blocks.Add(block); + + if (!bodyGuardTakenCareOf) + { + // LoopBody: assume guard; goto firstLoopBlock; + block = new Block(ec.tok, loopBodyLabel, ssBody, + new GotoCmd(ec.tok, new List {ec.Body.BigBlocks[0].LabelName})); + blocks.Add(block); + } + + // recurse to create the blocks for the loop body + CreateBlocks(ec.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(ec.tok, new List {runOffTheEndLabel}); + } + else + { + trCmd = GotoSuccessor(ec.tok, bigBlock); + } + + block = new Block(ec.tok, loopDoneLabel, ssDone, trCmd); + blocks.Add(block); + break; + } + case IfCmd ifcmd: + { + string predLabel = bigBlock.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(bigBlock.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, bigBlock); + } + + var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + blocks.Add(block); + } + } + + break; + } + } + } + } + } + + 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/IfCmd.cs b/Source/Core/AST/IfCmd.cs new file mode 100644 index 000000000..dfbe74009 --- /dev/null +++ b/Source/Core/AST/IfCmd.cs @@ -0,0 +1,106 @@ +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 ("); + var /*!*/ 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 From eff7523afc87bb19a0cd6a5747bfc875be237e53 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:14:29 +0200 Subject: [PATCH 2/8] Change FreshAnon into FreshPrefix --- Source/Core/AST/BigBlocksResolutionContext.cs | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 4e66238e2..62ba00f92 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -12,14 +12,13 @@ class BigBlocksResolutionContext [Peer] List blocks; - string /*!*/ - prefix = "anon"; + string /*!*/ prefix = "anon"; int anon = 0; - int FreshAnon() + string FreshPrefix() { - return anon++; + return prefix + anon++; } private readonly HashSet allLabels = new(); @@ -296,7 +295,7 @@ void NameAnonymousBlocks(StmtList stmtList) { if (b.LabelName == null) { - b.LabelName = prefix + FreshAnon(); + b.LabelName = FreshPrefix(); } if (b.ec is WhileCmd) @@ -410,11 +409,11 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) } case WhileCmd ec: { - var a = FreshAnon(); - string loopHeadLabel = prefix + a + "_LoopHead"; + var freshPrefix = FreshPrefix(); + string loopHeadLabel = freshPrefix + "_LoopHead"; string /*!*/ - loopBodyLabel = prefix + a + "_LoopBody"; - string loopDoneLabel = prefix + a + "_LoopDone"; + loopBodyLabel = freshPrefix + "_LoopBody"; + string loopDoneLabel = freshPrefix + "_LoopDone"; List ssBody = new List(); List ssDone = new List(); @@ -486,10 +485,10 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) for (; ifcmd != null; ifcmd = ifcmd.ElseIf) { - var a = FreshAnon(); - string thenLabel = prefix + a + "_Then"; + var freshPrefix = FreshPrefix(); + string thenLabel = freshPrefix + "_Then"; Contract.Assert(thenLabel != null); - string elseLabel = prefix + a + "_Else"; + string elseLabel = freshPrefix + "_Else"; Contract.Assert(elseLabel != null); List ssThen = new List(); From fff02b87c0b3d88b1980dafb2b568ebd012406af Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:21:09 +0200 Subject: [PATCH 3/8] Automated refactoring --- .../YieldingProcInstrumentation.cs | 96 ++++++++++--------- Source/Core/AST/BigBlocksResolutionContext.cs | 6 +- Source/Core/AST/Block.cs | 25 ++--- .../ExecutionEngineTest.cs | 2 +- Source/VCGeneration/Split.cs | 2 +- 5 files changed, 63 insertions(+), 68 deletions(-) diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 71a3623f4..424958a81 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -474,65 +474,73 @@ private void DesugarConcurrency(Implementation impl, List preconditions) // add jumps to noninterferenceChecker, returnChecker, and refinementChecker blocks var implRefinementCheckingBlocks = new List(); - foreach (var b in impl.Blocks) + foreach (var block in impl.Blocks) { - if (b.TransferCmd is GotoCmd gotoCmd) + if (block.TransferCmd is not GotoCmd gotoCmd) + { + block.TransferCmd = new GotoCmd(block.TransferCmd.tok, + new List { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock }); + } + else { var targetBlocks = new List(); var addEdge = false; foreach (var nextBlock in gotoCmd.LabelTargets) { - if (nextBlock.cmds.Count > 0) + if (nextBlock.Cmds.Count <= 0) + { + continue; + } + + var cmd = nextBlock.Cmds[0]; + if (cmd is not ParCallCmd parCallCmd) { - var cmd = nextBlock.cmds[0]; - if (cmd is ParCallCmd parCallCmd) + continue; + } + + foreach (var callCmd in parCallCmd.CallCmds) + { + if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock)) { - foreach (var callCmd in parCallCmd.CallCmds) - { - if (refinementBlocks.ContainsKey(callCmd)) - { - var targetBlock = refinementBlocks[callCmd]; - FixUpImplRefinementCheckingBlock(targetBlock, - CivlAttributes.IsCallMarked(callCmd) - ? returnCheckerBlock - : unchangedCheckerBlock); - targetBlocks.Add(targetBlock); - implRefinementCheckingBlocks.Add(targetBlock); - } - } - addEdge = true; + continue; } + + FixUpImplRefinementCheckingBlock(targetBlock, + CivlAttributes.IsCallMarked(callCmd) + ? returnCheckerBlock + : unchangedCheckerBlock); + targetBlocks.Add(targetBlock); + implRefinementCheckingBlocks.Add(targetBlock); } + + addEdge = true; } gotoCmd.AddTargets(targetBlocks); - if (addEdge) + if (!addEdge) { - AddEdge(gotoCmd, noninterferenceCheckerBlock); - if (blocksInYieldingLoops.Contains(b)) - { - AddEdge(gotoCmd, unchangedCheckerBlock); - } - else - { - b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds()); - AddEdge(gotoCmd, refinementCheckerBlock); - } + continue; + } + + AddEdge(gotoCmd, noninterferenceCheckerBlock); + if (blocksInYieldingLoops.Contains(block)) + { + AddEdge(gotoCmd, unchangedCheckerBlock); + } + else + { + block.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds()); + AddEdge(gotoCmd, refinementCheckerBlock); } - } - else - { - b.TransferCmd = new GotoCmd(b.TransferCmd.tok, - new List {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock}); } } // desugar ParCallCmd foreach (Block b in impl.Blocks) { - if (b.cmds.Count > 0) + if (b.Cmds.Count > 0) { - var cmd = b.cmds[0]; + var cmd = b.Cmds[0]; if (cmd is ParCallCmd) { DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b)); @@ -578,11 +586,11 @@ private void SplitBlocks(Implementation impl) { var currTransferCmd = b.TransferCmd; int labelCount = 0; - int lastSplitIndex = b.cmds.Count; - for (int i = b.cmds.Count - 1; i >= 0; i--) + int lastSplitIndex = b.Cmds.Count; + for (int i = b.Cmds.Count - 1; i >= 0; i--) { var split = false; - var cmd = b.cmds[i]; + var cmd = b.Cmds[i]; if (cmd is ParCallCmd) { split = true; @@ -590,7 +598,7 @@ private void SplitBlocks(Implementation impl) if (split) { - var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i), + var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i), currTransferCmd); newBlocks.Add(newBlock); currTransferCmd = new GotoCmd(b.tok, new List {newBlock}); @@ -598,7 +606,7 @@ private void SplitBlocks(Implementation impl) } } - b.cmds = b.cmds.GetRange(0, lastSplitIndex); + b.Cmds = b.Cmds.GetRange(0, lastSplitIndex); b.TransferCmd = currTransferCmd; } @@ -714,8 +722,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop) newCmds.AddRange(CreateUpdatesToOldGlobalVars()); newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars()); newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd)); - newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1)); - block.cmds = newCmds; + newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1)); + block.Cmds = newCmds; } private Formal ParCallDesugarFormal(Variable v, int count, bool incoming) diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 62ba00f92..9e6b846b8 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -491,8 +491,8 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) string elseLabel = freshPrefix + "_Else"; Contract.Assert(elseLabel != null); - List ssThen = new List(); - List ssElse = new List(); + var ssThen = new List(); + var ssElse = new List(); if (ifcmd.Guard != null) { var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); @@ -514,7 +514,7 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) // ... goto Then, Else; var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); blocks.Add(jumpBlock); if (!thenGuardTakenCareOf) diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs index c6ac50740..075dfa2f5 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/Block.cs @@ -23,21 +23,9 @@ public string /*!*/ Label } } - [Rep] [ElementsPeer] public List /*!*/ cmds; - - public List /*!*/ Cmds - { - get - { - Contract.Ensures(Contract.Result>() != null); - return this.cmds; - } - set - { - Contract.Requires(value != null); - this.cmds = value; - } - } + [field: Rep] + [field: ElementsPeer] + public List Cmds { get; set; } public IEnumerable Exits() { @@ -70,8 +58,7 @@ public enum VisitState public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run public bool widenBlock; - public int - iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not + public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not // VC generation and SCC computation public List /*!*/ Predecessors; @@ -113,7 +100,7 @@ public IEnumerable liveVarsBefore void ObjectInvariant() { Contract.Invariant(this.label != null); - Contract.Invariant(this.cmds != null); + Contract.Invariant(this.Cmds != null); Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); } @@ -140,7 +127,7 @@ public Block(IToken tok, string /*!*/ label, List /*!*/ cmds, TransferCmd t Contract.Requires(cmds != null); Contract.Requires(tok != null); this.label = label; - this.cmds = cmds; + this.Cmds = cmds; this.TransferCmd = transferCmd; this.Predecessors = new List(); this._liveVarsBefore = null; diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 6c39f1ec0..7415571ea 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -251,7 +251,7 @@ public async Task LoopInvariantDescriptions() Parser.Parse(programString, "fakeFilename", out var program1); foreach (var block in program1.Implementations.First().Blocks) { - foreach (var cmd in block.cmds) { + foreach (var cmd in block.Cmds) { if (cmd is AssertCmd assertCmd) { assertCmd.Description = new FakeDescription(); } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index fc5ff9473..aa22d0779 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -25,7 +25,7 @@ public class Split : ProofRun public List Blocks => blocks ??= getBlocks(); readonly List bigBlocks = new(); - public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); + public List Asserts => Blocks.SelectMany(block => block.Cmds.OfType()).ToList(); public IReadOnlyList prunedDeclarations; public IReadOnlyList PrunedDeclarations { From d9722c3bbefc4d80bdb2a23bb6590d3b26250126 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:25:46 +0200 Subject: [PATCH 4/8] Automated refactoring --- .../AbstractInterpretation/NativeLattice.cs | 14 +- Source/AbstractInterpretation/Traverse.cs | 4 +- Source/Core/AST/Block.cs | 73 +++---- .../LiveVariableAnalysis.cs | 8 +- Source/Core/VariableDependenceAnalyser.cs | 198 +++++++++--------- Source/VCGeneration/ConditionGeneration.cs | 10 +- 6 files changed, 148 insertions(+), 159 deletions(-) diff --git a/Source/AbstractInterpretation/NativeLattice.cs b/Source/AbstractInterpretation/NativeLattice.cs index 2efc1f0bf..8b63e17f7 100644 --- a/Source/AbstractInterpretation/NativeLattice.cs +++ b/Source/AbstractInterpretation/NativeLattice.cs @@ -195,7 +195,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El int n = 0; foreach (var block in impl.Blocks) { - block.aiId = n; + block.AiId = n; // Note: The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null. // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition: // n == 0 || block.widenBlock @@ -219,7 +219,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El { var workItem = workItems.Dequeue(); var b = workItem.Item1; - var id = b.aiId; + var id = b.AiId; var e = workItem.Item2; if (pre[id] == null) { @@ -230,7 +230,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El // no change continue; } - else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id]) + else if (b.WidenBlock && options.Ai.StepsBeforeWidening <= iterations[id]) { e = lattice.Widen(pre[id], e); pre[id] = e; @@ -275,8 +275,8 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice. foreach (var b in impl.Blocks) { - var element = pre[b.aiId]; - if (element != null && (b.widenBlock || options.InstrumentInfer == + var element = pre[b.AiId]; + if (element != null && (b.WidenBlock || options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere)) { List newCommands = new List(); @@ -294,9 +294,9 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice. newCommands.Add(cmd); newCommands.AddRange(b.Cmds); - if (post != null && post[b.aiId] != null) + if (post != null && post[b.AiId] != null) { - inv = post[b.aiId].ToExpr(options); + inv = post[b.AiId].ToExpr(options); kv = new QKeyValue(Token.NoToken, "inferred", new List(), null); if (options.InstrumentWithAsserts) { diff --git a/Source/AbstractInterpretation/Traverse.cs b/Source/AbstractInterpretation/Traverse.cs index 1a1315c51..69a6d361f 100644 --- a/Source/AbstractInterpretation/Traverse.cs +++ b/Source/AbstractInterpretation/Traverse.cs @@ -54,7 +54,7 @@ static void Visit(Block b) { cce.BeginExpose(b); // we got here through a back-edge - b.widenBlock = true; + b.WidenBlock = true; cce.EndExpose(); } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) @@ -111,7 +111,7 @@ static void Visit(Block b) /// public static List ComputeLoopBodyFrom(Block block) { - Contract.Requires(block.widenBlock); + Contract.Requires(block.WidenBlock); Contract.Requires(block != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs index 075dfa2f5..bfebf90fc 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/Block.cs @@ -7,21 +7,7 @@ namespace Microsoft.Boogie; public sealed class Block : Absy { - private string /*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal - - public string /*!*/ Label - { - get - { - Contract.Ensures(Contract.Result() != null); - return this.label; - } - set - { - Contract.Requires(value != null); - this.label = value; - } - } + public string Label { get; set; } [field: Rep] [field: ElementsPeer] @@ -37,8 +23,7 @@ public IEnumerable Exits() } [Rep] //PM: needed to verify Traverse.Visit - public TransferCmd - TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) + public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) public byte[] Checksum; @@ -55,31 +40,31 @@ public enum VisitState public VisitState TraversingStatus; - public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run - public bool widenBlock; + public int AiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run + public bool WidenBlock; - public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not + public int Iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not // VC generation and SCC computation public List /*!*/ Predecessors; // This field is used during passification to null-out entries in block2Incarnation dictionary early - public int succCount; + 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 @@ -87,11 +72,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); } } } @@ -99,24 +84,28 @@ public IEnumerable liveVarsBefore [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(this.label != null); + Contract.Invariant(this.Label != null); Contract.Invariant(this.Cmds != null); - Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true)); + Contract.Invariant(cce.NonNullElements(this.liveVarsBefore, true)); } public bool IsLive(Variable v) { Contract.Requires(v != null); - if (liveVarsBefore == null) + if (LiveVarsBefore == null) { return true; } - return liveVarsBefore.Contains(v); + return LiveVarsBefore.Contains(v); } - public Block(IToken tok) - : this(tok, "", new List(), new ReturnCmd(tok)) + public static Block ShallowClone(Block block) { + return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); + } + + public Block(IToken tok, TransferCmd cmd) + : this(tok, "", new List(), cmd) { } @@ -126,13 +115,13 @@ public Block(IToken tok, string /*!*/ label, List /*!*/ cmds, TransferCmd t Contract.Requires(label != null); Contract.Requires(cmds != null); Contract.Requires(tok != null); - this.label = label; + this.Label = label; this.Cmds = cmds; this.TransferCmd = transferCmd; this.Predecessors = new List(); - this._liveVarsBefore = null; + this.liveVarsBefore = null; this.TraversingStatus = VisitState.ToVisit; - this.iterations = 0; + this.Iterations = 0; } public void Emit(TokenTextWriter stream, int level) @@ -146,7 +135,7 @@ public void Emit(TokenTextWriter stream, int level) stream.Options.PrintWithUniqueASTIds ? String.Format("h{0}^^{1}", this.GetHashCode(), this.Label) : this.Label, - this.widenBlock ? " // cut point" : ""); + this.WidenBlock ? " // cut point" : ""); foreach (Cmd /*!*/ c in this.Cmds) { @@ -178,10 +167,10 @@ public override void Resolve(ResolutionContext rc) public override void Typecheck(TypecheckingContext tc) { - foreach (Cmd /*!*/ c in Cmds) + foreach (var /*!*/ cmd in Cmds) { - Contract.Assert(c != null); - c.Typecheck(tc); + Contract.Assert(cmd != null); + cmd.Typecheck(tc); } Contract.Assume(this.TransferCmd != null); @@ -195,14 +184,14 @@ public void ResetAbstractInterpretationState() { // this.currentlyTraversed = false; this.TraversingStatus = VisitState.ToVisit; - this.iterations = 0; + this.Iterations = 0; } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); - return this.Label + (this.widenBlock ? "[w]" : ""); + return this.Label + (this.WidenBlock ? "[w]" : ""); } public override Absy StdDispatch(StandardVisitor visitor) diff --git a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs index bcdbbf517..98fdef014 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; } } diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 2e0ae6c67..3e6fdd2b3 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -137,8 +137,8 @@ public class VariableDependenceAnalyser : IVariableDependenceAnalyser private CoreOptions options; private Graph dependsOnNonTransitive; private Program prog; - private Dictionary> BlockToControllingBlocks; - private Dictionary> ControllingBlockToVariables; + private Dictionary> blockToControllingBlocks; + private Dictionary> controllingBlockToVariables; public VariableDependenceAnalyser(Program prog, CoreOptions options) { @@ -151,30 +151,30 @@ public VariableDependenceAnalyser(Program prog, CoreOptions options) private void Initialise() { foreach (var descriptor in - prog.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)).Select(Variable => Variable.Name) - .Select(Name => new GlobalDescriptor(Name))) + prog.Variables.Where(item => VariableRelevantToAnalysis(item, null)).Select(variable => variable.Name) + .Select(name => new GlobalDescriptor(name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } - foreach (var Proc in prog.NonInlinedProcedures()) + foreach (var proc in prog.NonInlinedProcedures()) { List parameters = new List(); - parameters.AddRange(Proc.InParams); - parameters.AddRange(Proc.OutParams); + parameters.AddRange(proc.InParams); + parameters.AddRange(proc.OutParams); foreach (var descriptor in - parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) + parameters.Select(variable => variable.Name).Select(name => new LocalDescriptor(proc.Name, name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } } - foreach (var Impl in prog.NonInlinedImplementations()) + foreach (var impl in prog.NonInlinedImplementations()) { List locals = new List(); - locals.AddRange(Impl.LocVars); + locals.AddRange(impl.LocVars); foreach (var descriptor in - locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) + locals.Select(variable => variable.Name).Select(name => new LocalDescriptor(impl.Name, name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); } @@ -279,29 +279,29 @@ public void Analyse() options.OutputWriter.WriteLine("Variable dependence analysis: Computing control dependence info"); } - BlockToControllingBlocks = ComputeGlobalControlDependences(); + blockToControllingBlocks = ComputeGlobalControlDependences(); if (options.Trace) { options.OutputWriter.WriteLine("Variable dependence analysis: Computing control dependence variables"); } - ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks); - foreach (var Impl in prog.NonInlinedImplementations()) + controllingBlockToVariables = ComputeControllingVariables(blockToControllingBlocks); + foreach (var impl in prog.NonInlinedImplementations()) { if (options.Trace) { - options.OutputWriter.WriteLine("Variable dependence analysis: Analysing " + Impl.Name); + options.OutputWriter.WriteLine("Variable dependence analysis: Analysing " + impl.Name); } - Analyse(Impl); + Analyse(impl); } } - private void Analyse(Implementation Impl) + private void Analyse(Implementation impl) { - string proc = Impl.Name; - foreach (Block b in Impl.Blocks) + string proc = impl.Name; + foreach (Block b in impl.Blocks) { Analyse(proc, b); } @@ -349,7 +349,7 @@ private void HandleCall(string proc, Block b, CallCmd call) private void HandleAssign(string proc, Block b, AssignCmd assign) { foreach (var assignPair in assign.Lhss.Zip(assign.Rhss).Where( - Item => VariableRelevantToAnalysis(Item.Item1.DeepAssignedVariable, proc))) + item => VariableRelevantToAnalysis(item.Item1.DeepAssignedVariable, proc))) { VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable); AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc), @@ -362,24 +362,24 @@ private void HandleAssign(string proc, Block b, AssignCmd assign) private void AddControlDependences(Block b, VariableDescriptor v, string reason, IToken tok) { - if (!BlockToControllingBlocks.ContainsKey(b)) + if (!blockToControllingBlocks.ContainsKey(b)) { return; } - foreach (var controller in BlockToControllingBlocks[b]) + foreach (var controller in blockToControllingBlocks[b]) { - AddDependences(v, ControllingBlockToVariables[controller], + AddDependences(v, controllingBlockToVariables[controller], reason + " controlling block at (" + controller.tok.line + ":" + controller.tok.col + ")", tok); } } private IEnumerable GetReferencedVariables(Absy node, string proc) { - var VarCollector = new VariableCollector(); - VarCollector.Visit(node); - return VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)) - .Select(Item => MakeDescriptor(proc, Item)); + var varCollector = new VariableCollector(); + varCollector.Visit(node); + return varCollector.usedVars.Where(item => VariableRelevantToAnalysis(item, proc)) + .Select(item => MakeDescriptor(proc, item)); } void AddDependences(VariableDescriptor v, IEnumerable vs, string reason, IToken tok) @@ -397,14 +397,14 @@ void AddDependences(VariableDescriptor v, IEnumerable vs, st } private Dictionary> ComputeControllingVariables( - Dictionary> GlobalCtrlDep) + Dictionary> globalCtrlDep) { - Dictionary> result = new Dictionary>(); - foreach (var Impl in prog.NonInlinedImplementations()) + var result = new Dictionary>(); + foreach (var impl in prog.NonInlinedImplementations()) { - foreach (var b in Impl.Blocks) + foreach (var b in impl.Blocks) { - result[b] = GetControlDependencyVariables(Impl.Name, b); + result[b] = GetControlDependencyVariables(impl.Name, b); } } @@ -427,10 +427,10 @@ private HashSet GetControlDependencyVariables(string proc, B AssumeCmd a = c as AssumeCmd; if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) { - var VarCollector = new VariableCollector(); - VarCollector.VisitExpr(a.Expr); - result.UnionWith(VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)) - .Select(Item => MakeDescriptor(proc, Item))); + var varCollector = new VariableCollector(); + varCollector.VisitExpr(a.Expr); + result.UnionWith(varCollector.usedVars.Where(item => VariableRelevantToAnalysis(item, proc)) + .Select(item => MakeDescriptor(proc, item))); } else { @@ -443,21 +443,21 @@ private HashSet GetControlDependencyVariables(string proc, B return result; } - private HashSet IgnoredVariables = null; + private HashSet ignoredVariables; public bool Ignoring(Variable v, string proc) { - if (IgnoredVariables == null) + if (ignoredVariables == null) { MakeIgnoreList(); } - if (proc != null && IgnoredVariables.Contains(new LocalDescriptor(proc, v.Name))) + if (proc != null && ignoredVariables.Contains(new LocalDescriptor(proc, v.Name))) { return true; } - if (IgnoredVariables.Contains(new GlobalDescriptor(v.Name))) + if (ignoredVariables.Contains(new GlobalDescriptor(v.Name))) { return true; } @@ -472,7 +472,7 @@ public bool VariableRelevantToAnalysis(Variable v, string proc) private void MakeIgnoreList() { - IgnoredVariables = new HashSet(); + ignoredVariables = new HashSet(); if (options.VariableDependenceIgnore == null) { return; @@ -498,12 +498,12 @@ private void MakeIgnoreList() if (tokens.Count() == 1) { - IgnoredVariables.Add(new GlobalDescriptor(tokens[0])); + ignoredVariables.Add(new GlobalDescriptor(tokens[0])); continue; } Debug.Assert(tokens.Count() == 2); - IgnoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); + ignoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); } } catch (System.IO.IOException e) @@ -548,7 +548,7 @@ private Dictionary> ComputeGlobalControlDependences() var indirectCallees = ComputeIndirectCallees(callGraph, directCallee); foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl])) { - foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) + foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(item => item)) { globalCtrlDep[control].Add(c); } @@ -579,23 +579,23 @@ private Dictionary> ComputeGlobalControlDependences() return result; } - private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee) + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation directCallee) { - return ComputeIndirectCallees(callGraph, DirectCallee, new HashSet()); + return ComputeIndirectCallees(callGraph, directCallee, new HashSet()); } - private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee, + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation directCallee, HashSet seen) { - if (seen.Contains(DirectCallee)) + if (seen.Contains(directCallee)) { return new HashSet(); } HashSet result = new HashSet(); - result.Add(DirectCallee); - seen.Add(DirectCallee); - foreach (var succ in callGraph.Successors(DirectCallee)) + result.Add(directCallee); + seen.Add(directCallee); + foreach (var succ in callGraph.Successors(directCallee)) { result.UnionWith(ComputeIndirectCallees(callGraph, succ, seen)); } @@ -606,11 +606,11 @@ private HashSet ComputeIndirectCallees(Graph cal private HashSet GetControllingBlocks(Block b, Dictionary> ctrlDep) { HashSet result = new HashSet(); - foreach (var KeyValue in ctrlDep) + foreach (var keyValue in ctrlDep) { - if (KeyValue.Value.Contains(b)) + if (keyValue.Value.Contains(b)) { - result.Add(KeyValue.Key); + result.Add(keyValue.Key); } } @@ -619,11 +619,11 @@ private HashSet GetControllingBlocks(Block b, Dictionary Item is LocalDescriptor).Select( - Item => (LocalDescriptor) Item).Where(Item => Item.Proc.Equals(proc) && - Item.Name.Equals(v.Name)); - if (MatchingLocals.Count() > 0) + var matchingLocals = dependsOnNonTransitive.Nodes.Where(item => item is LocalDescriptor).Select( + item => (LocalDescriptor) item).Where(item => item.Proc.Equals(proc) && + item.Name.Equals(v.Name)); + if (matchingLocals.Count() > 0) { - Debug.Assert(MatchingLocals.Count() == 1); - return MatchingLocals.ToArray()[0]; + Debug.Assert(matchingLocals.Count() == 1); + return matchingLocals.ToArray()[0]; } // It must be a global with same name as v - return dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor && - Item.Name.Equals(v.Name)).ToArray()[0]; + return dependsOnNonTransitive.Nodes.Where(item => item is GlobalDescriptor && + item.Name.Equals(v.Name)).ToArray()[0]; } - private Dictionary, HashSet> DependsOnCache = + private Dictionary, HashSet> dependsOnCache = new Dictionary, HashSet>(); - private Graph> DependsOnSCCsDAG; - private Dictionary> VariableDescriptorToSCC; + private Graph> dependsOnScCsDag; + private Dictionary> variableDescriptorToScc; public HashSet DependsOn(VariableDescriptor v) { - if (DependsOnSCCsDAG == null) + if (dependsOnScCsDag == null) { if (options.Trace) { @@ -664,33 +664,33 @@ public HashSet DependsOn(VariableDescriptor v) Adjacency next = new Adjacency(dependsOnNonTransitive.Successors); Adjacency prev = new Adjacency(dependsOnNonTransitive.Predecessors); - StronglyConnectedComponents DependsOnSCCs = + StronglyConnectedComponents dependsOnScCs = new StronglyConnectedComponents( dependsOnNonTransitive.Nodes, next, prev); - DependsOnSCCs.Compute(); + dependsOnScCs.Compute(); - VariableDescriptorToSCC = new Dictionary>(); - foreach (var scc in DependsOnSCCs) + variableDescriptorToScc = new Dictionary>(); + foreach (var scc in dependsOnScCs) { foreach (var s in scc) { - VariableDescriptorToSCC[s] = scc; + variableDescriptorToScc[s] = scc; } } - DependsOnSCCsDAG = new Graph>(); + dependsOnScCsDag = new Graph>(); foreach (var edge in dependsOnNonTransitive.Edges) { - if (VariableDescriptorToSCC[edge.Item1] != VariableDescriptorToSCC[edge.Item2]) + if (variableDescriptorToScc[edge.Item1] != variableDescriptorToScc[edge.Item2]) { - DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[edge.Item1], VariableDescriptorToSCC[edge.Item2]); + dependsOnScCsDag.AddEdge(variableDescriptorToScc[edge.Item1], variableDescriptorToScc[edge.Item2]); } } SCC dummy = new SCC(); foreach (var n in dependsOnNonTransitive.Nodes) { - DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[n], dummy); + dependsOnScCsDag.AddEdge(variableDescriptorToScc[n], dummy); } if (options.Trace) @@ -699,27 +699,27 @@ public HashSet DependsOn(VariableDescriptor v) } } - return DependsOn(VariableDescriptorToSCC[v]); + return DependsOn(variableDescriptorToScc[v]); } - public HashSet DependsOn(SCC vSCC) + public HashSet DependsOn(SCC vScc) { - if (!DependsOnCache.ContainsKey(vSCC)) + if (!dependsOnCache.ContainsKey(vScc)) { HashSet result = new HashSet(); - if (vSCC.Count() > 0) + if (vScc.Count() > 0) { - result.UnionWith(vSCC); - foreach (var wSCC in DependsOnSCCsDAG.Successors(vSCC)) + result.UnionWith(vScc); + foreach (var wScc in dependsOnScCsDag.Successors(vScc)) { - result.UnionWith(DependsOn(wSCC)); + result.UnionWith(DependsOn(wScc)); } } - DependsOnCache[vSCC] = result; + dependsOnCache[vScc] = result; } - return DependsOnCache[vSCC]; + return dependsOnCache[vScc]; } public void Dump() @@ -730,34 +730,34 @@ public void Dump() options.OutputWriter.WriteLine("Global variables"); options.OutputWriter.WriteLine("================"); - foreach (var GlobalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor)) + foreach (var globalEntry in dependsOnNonTransitive.Nodes.Where(item => item is GlobalDescriptor)) { - dump(GlobalEntry); + Dump(globalEntry); } foreach (var proc in Procedures()) { options.OutputWriter.WriteLine("Variables of " + proc); options.OutputWriter.WriteLine("====================="); - foreach (var LocalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor - && ((LocalDescriptor) Item).Proc.Equals( + foreach (var localEntry in dependsOnNonTransitive.Nodes.Where(item => item is LocalDescriptor + && ((LocalDescriptor) item).Proc.Equals( proc))) { - dump(LocalEntry); + Dump(localEntry); } } } - private void dump(VariableDescriptor vd) + private void Dump(VariableDescriptor vd) { options.OutputWriter.Write(vd + " <- {"); bool first = true; - var SortedDependents = DependsOn(vd).ToList(); - SortedDependents.Sort(); - foreach (var Descriptor in SortedDependents) + var sortedDependents = DependsOn(vd).ToList(); + sortedDependents.Sort(); + foreach (var descriptor in sortedDependents) { - options.OutputWriter.Write((first ? "" : ",") + "\n " + Descriptor); + options.OutputWriter.Write((first ? "" : ",") + "\n " + descriptor); if (first) { first = false; @@ -770,8 +770,8 @@ private void dump(VariableDescriptor vd) private HashSet Procedures() { - return new HashSet(dependsOnNonTransitive.Nodes.Where(Item => - Item is LocalDescriptor).Select(Item => ((LocalDescriptor) Item).Proc)); + return new HashSet(dependsOnNonTransitive.Nodes.Where(item => + item is LocalDescriptor).Select(item => ((LocalDescriptor) item).Proc)); } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 2e7f91060..3ba97ab5a 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -766,7 +766,7 @@ protected Dictionary ConvertBlocks2PassiveCmd(TextWriter traceWr Dictionary incarnationMap = ComputeIncarnationMap(b, block2Incarnation); // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out. - b.liveVarsBefore = null; + b.LiveVarsBefore = null; // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, // all its successors have been passified. Consequently, its entry in block2Incarnation can be removed. @@ -775,7 +775,7 @@ protected Dictionary ConvertBlocks2PassiveCmd(TextWriter traceWr variableCollectors[b] = mvc; foreach (Block p in b.Predecessors) { - p.succCount--; + p.SuccCount--; if (p.Checksum != null) { // Compute the checksum based on the checksums of the predecessor. The order should not matter. @@ -783,7 +783,7 @@ protected Dictionary ConvertBlocks2PassiveCmd(TextWriter traceWr } mvc.AddUsedVariables(variableCollectors[p].UsedVariables); - if (p.succCount == 0) + if (p.SuccCount == 0) { block2Incarnation.Remove(p); } @@ -794,12 +794,12 @@ protected Dictionary ConvertBlocks2PassiveCmd(TextWriter traceWr GotoCmd gotoCmd = b.TransferCmd as GotoCmd; if (gotoCmd == null) { - b.succCount = 0; + b.SuccCount = 0; } else { // incarnationMap needs to be added only if there is some successor of b - b.succCount = gotoCmd.LabelNames.Count; + b.SuccCount = gotoCmd.LabelNames.Count; block2Incarnation.Add(b, incarnationMap); } From 3e14a66c08118f2840f0c13b9efd55d809019749 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:36:33 +0200 Subject: [PATCH 5/8] Extract classes into separate files --- Source/Core/AST/AbsyCmd.cs | 228 +----------------- Source/Core/AST/{ => Blocks}/Block.cs | 12 +- Source/Core/AST/Blocks/GotoCmd.cs | 159 ++++++++++++ Source/Core/AST/Blocks/ReturnCmd.cs | 33 +++ Source/Core/AST/Blocks/TransferCmd.cs | 33 +++ .../Core/AST/Blocks/TransferCmdContracts.cs | 18 ++ Source/VCGeneration/ManualSplitFinder.cs | 17 -- 7 files changed, 246 insertions(+), 254 deletions(-) rename Source/Core/AST/{ => Blocks}/Block.cs (94%) create mode 100644 Source/Core/AST/Blocks/GotoCmd.cs create mode 100644 Source/Core/AST/Blocks/ReturnCmd.cs create mode 100644 Source/Core/AST/Blocks/TransferCmd.cs create mode 100644 Source/Core/AST/Blocks/TransferCmdContracts.cs diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index 5a4d6d493..f42a4be00 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -2579,8 +2579,7 @@ public override Absy StdDispatch(StandardVisitor visitor) public class ReturnExprCmd : ReturnCmd { - public Expr /*!*/ - Expr; + public Expr /*!*/ Expr; [ContractInvariantMethod] void ObjectInvariant() @@ -2705,229 +2704,4 @@ public override Absy StdDispatch(StandardVisitor visitor) return visitor.VisitHavocCmd(this); } } - - //--------------------------------------------------------------------- - // 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 - { - public TransferCmdContracts() : base(null) - { - } - - public override void Emit(TokenTextWriter stream, int level) - { - Contract.Requires(stream != null); - throw new NotImplementedException(); - } - } - - public class ReturnCmd : TransferCmd - { - public ReturnCmd(IToken /*!*/ tok) - : base(tok) - { - Contract.Requires(tok != null); - } - - public override void Emit(TokenTextWriter stream, int level) - { - //Contract.Requires(stream != null); - stream.WriteLine(this, level, "return;"); - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - // nothing to resolve - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitReturnCmd(this); - } - } - - public class GotoCmd : TransferCmd - { - [Rep] public List LabelNames; - [Rep] public List LabelTargets; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(LabelNames == null || LabelTargets == null || LabelNames.Count == LabelTargets.Count); - } - - [NotDelayed] - public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(labelSeq != null); - this.LabelNames = labelSeq; - } - - public GotoCmd(IToken /*!*/ tok, List /*!*/ labelSeq, List /*!*/ blockSeq) - : base(tok) - { - Contract.Requires(tok != null); - Contract.Requires(labelSeq != null); - Contract.Requires(blockSeq != null); - Debug.Assert(labelSeq.Count == blockSeq.Count); - for (int i = 0; i < labelSeq.Count; i++) - { - Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label)); - } - - this.LabelNames = labelSeq; - this.LabelTargets = blockSeq; - } - - public GotoCmd(IToken /*!*/ tok, List /*!*/ blockSeq) - : base(tok) - { - //requires (blockSeq[i] != null ==> blockSeq[i].Label != null); - Contract.Requires(tok != null); - Contract.Requires(blockSeq != null); - List labelSeq = new List(); - for (int i = 0; i < blockSeq.Count; i++) - { - labelSeq.Add(cce.NonNull(blockSeq[i]).Label); - } - - this.LabelNames = labelSeq; - this.LabelTargets = blockSeq; - } - - public void RemoveTarget(Block b) { - LabelNames.Remove(b.Label); - LabelTargets.Remove(b); - } - - public void AddTarget(Block b) - { - Contract.Requires(b != null); - Contract.Requires(b.Label != null); - Contract.Requires(this.LabelTargets != null); - Contract.Requires(this.LabelNames != null); - this.LabelTargets.Add(b); - this.LabelNames.Add(b.Label); - } - - public void AddTargets(IEnumerable blocks) - { - Contract.Requires(blocks != null); - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Requires(this.LabelTargets != null); - Contract.Requires(this.LabelNames != null); - foreach (var block in blocks) - { - AddTarget(block); - } - } - - public override void Emit(TokenTextWriter stream, int level) - { - //Contract.Requires(stream != null); - Contract.Assume(this.LabelNames != null); - stream.Write(this, level, "goto "); - if (stream.Options.PrintWithUniqueASTIds) - { - if (LabelTargets == null) - { - string sep = ""; - foreach (string name in LabelNames) - { - stream.Write("{0}{1}^^{2}", sep, "NoDecl", name); - sep = ", "; - } - } - else - { - string sep = ""; - foreach (Block /*!*/ b in LabelTargets) - { - Contract.Assert(b != null); - stream.Write("{0}h{1}^^{2}", sep, b.GetHashCode(), b.Label); - sep = ", "; - } - } - } - else - { - LabelNames.Emit(stream); - } - - stream.WriteLine(";"); - } - - public override void Resolve(ResolutionContext rc) - { - //Contract.Requires(rc != null); - Contract.Ensures(LabelTargets != null); - if (LabelTargets != null) - { - // already resolved - return; - } - - Contract.Assume(this.LabelNames != null); - LabelTargets = new List(); - foreach (string /*!*/ lbl in LabelNames) - { - Contract.Assert(lbl != null); - Block b = rc.LookUpBlock(lbl); - if (b == null) - { - rc.Error(this, "goto to unknown block: {0}", lbl); - } - else - { - LabelTargets.Add(b); - } - } - - Debug.Assert(rc.ErrorCount > 0 || LabelTargets.Count == LabelNames.Count); - } - - public override Absy StdDispatch(StandardVisitor visitor) - { - //Contract.Requires(visitor != null); - Contract.Ensures(Contract.Result() != null); - return visitor.VisitGotoCmd(this); - } - } } diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Blocks/Block.cs similarity index 94% rename from Source/Core/AST/Block.cs rename to Source/Core/AST/Blocks/Block.cs index bfebf90fc..89a6c08cd 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/Blocks/Block.cs @@ -27,10 +27,6 @@ public IEnumerable Exits() public byte[] Checksum; - // Abstract interpretation - - // public bool currentlyTraversed; - public enum VisitState { ToVisit, @@ -99,13 +95,9 @@ public bool IsLive(Variable v) return LiveVarsBefore.Contains(v); } - - public static Block ShallowClone(Block block) { - return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); - } - public Block(IToken tok, TransferCmd cmd) - : this(tok, "", new List(), cmd) + public Block(IToken tok) + : this(tok, "", new List(), new ReturnCmd(tok)) { } diff --git a/Source/Core/AST/Blocks/GotoCmd.cs b/Source/Core/AST/Blocks/GotoCmd.cs new file mode 100644 index 000000000..790988969 --- /dev/null +++ b/Source/Core/AST/Blocks/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 /*!*/ blocks) + : base(tok) + { + //requires (blockSeq[i] != null ==> blockSeq[i].Label != null); + Contract.Requires(tok != null); + Contract.Requires(blocks != null); + var labels = new List(); + foreach (var block in blocks) + { + labels.Add(block.Label); + } + + this.LabelNames = labels; + this.LabelTargets = blocks; + } + + 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/Blocks/ReturnCmd.cs b/Source/Core/AST/Blocks/ReturnCmd.cs new file mode 100644 index 000000000..9f60df66b --- /dev/null +++ b/Source/Core/AST/Blocks/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/Blocks/TransferCmd.cs b/Source/Core/AST/Blocks/TransferCmd.cs new file mode 100644 index 000000000..933ccdc91 --- /dev/null +++ b/Source/Core/AST/Blocks/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/Blocks/TransferCmdContracts.cs b/Source/Core/AST/Blocks/TransferCmdContracts.cs new file mode 100644 index 000000000..fbb7da6e0 --- /dev/null +++ b/Source/Core/AST/Blocks/TransferCmdContracts.cs @@ -0,0 +1,18 @@ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie; + +[ContractClassFor(typeof(TransferCmd))] +public abstract class TransferCmdContracts : TransferCmd +{ + public TransferCmdContracts() : base(null) + { + } + + public override void Emit(TokenTextWriter stream, int level) + { + Contract.Requires(stream != null); + throw new NotImplementedException(); + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index ffc6806d2..d6307ed29 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -103,23 +103,6 @@ private static Dictionary PickBlocksToVerify(List blocks, D return blockAssignments; } - private static List SplitOnAssert(VCGenOptions options, List oldBlocks, AssertCmd assertToKeep) { - var oldToNewBlockMap = new Dictionary(oldBlocks.Count); - - var newBlocks = new List(oldBlocks.Count); - foreach (var oldBlock in oldBlocks) { - var newBlock = new Block(oldBlock.tok) { - Label = oldBlock.Label, - Cmds = oldBlock.Cmds.Select(cmd => - cmd != assertToKeep ? CommandTransformations.AssertIntoAssume(options, cmd) : cmd).ToList() - }; - oldToNewBlockMap[oldBlock] = newBlock; - newBlocks.Add(newBlock); - } - - AddBlockJumps(oldBlocks, oldToNewBlockMap); - return newBlocks; - } private static List? DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { From 760c2b06c861ecc47dbd26227b39db48322b9a2e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 10:50:52 +0200 Subject: [PATCH 6/8] Refactoring --- Source/Core/AST/BigBlocksResolutionContext.cs | 107 +++++++++--------- 1 file changed, 56 insertions(+), 51 deletions(-) diff --git a/Source/Core/AST/BigBlocksResolutionContext.cs b/Source/Core/AST/BigBlocksResolutionContext.cs index 9e6b846b8..1dfdcca23 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/BigBlocksResolutionContext.cs @@ -352,12 +352,12 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { Contract.Requires(stmtList != null); Contract.Requires(blocks != null); - List cmdPrefixToApply = stmtList.PrefixCommands; + var cmdPrefixToApply = stmtList.PrefixCommands; - int n = stmtList.BigBlocks.Count; + int remainingBigBlocks = stmtList.BigBlocks.Count; foreach (var bigBlock in stmtList.BigBlocks) { - n--; + remainingBigBlocks--; Contract.Assert(bigBlock.LabelName != null); List theSimpleCmds; if (cmdPrefixToApply == null) @@ -376,7 +376,7 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { // this BigBlock has the very same components as a Block Contract.Assert(bigBlock.ec == null); - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, bigBlock.tc); blocks.Add(block); } else @@ -386,24 +386,24 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) case null: { TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) + if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(stmtList.EndCurly, new List {runOffTheEndLabel}); } else { trCmd = GotoSuccessor(stmtList.EndCurly, bigBlock); } - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, trCmd); blocks.Add(block); break; } case BreakCmd ec: { Contract.Assert(ec.BreakEnclosure != null); - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(ec.tok, ec.BreakEnclosure)); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, GotoSuccessor(ec.tok, ec.BreakEnclosure)); blocks.Add(block); break; } @@ -411,20 +411,23 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { var freshPrefix = FreshPrefix(); string loopHeadLabel = freshPrefix + "_LoopHead"; - string /*!*/ - loopBodyLabel = freshPrefix + "_LoopBody"; + string loopBodyLabel = freshPrefix + "_LoopBody"; string loopDoneLabel = freshPrefix + "_LoopDone"; - List ssBody = new List(); - List ssDone = new List(); + var ssBody = new List(); + var ssDone = new List(); if (ec.Guard != null) { - var ac = new AssumeCmd(ec.tok, ec.Guard); - ac.Attributes = new QKeyValue(ec.tok, "partition", new List(), null); + var ac = new AssumeCmd(ec.tok, ec.Guard) + { + Attributes = new QKeyValue(ec.tok, "partition", new List(), null) + }; ssBody.Add(ac); - ac = new AssumeCmd(ec.tok, Expr.Not(ec.Guard)); - ac.Attributes = new QKeyValue(ec.tok, "partition", new List(), null); + ac = new AssumeCmd(ec.tok, Expr.Not(ec.Guard)) + { + Attributes = new QKeyValue(ec.tok, "partition", new List(), null) + }; ssDone.Add(ac); } @@ -432,8 +435,8 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) bool bodyGuardTakenCareOf = ec.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel); // ... goto LoopHead; - Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, - new GotoCmd(ec.tok, new List {loopHeadLabel})); + var block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, + new GotoCmd(ec.tok, new List {loopHeadLabel})); blocks.Add(block); // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; @@ -448,14 +451,14 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) } block = new Block(ec.tok, loopHeadLabel, ssHead, - new GotoCmd(ec.tok, new List {loopDoneLabel, loopBodyLabel})); + new GotoCmd(ec.tok, new List {loopDoneLabel, loopBodyLabel})); blocks.Add(block); if (!bodyGuardTakenCareOf) { // LoopBody: assume guard; goto firstLoopBlock; block = new Block(ec.tok, loopBodyLabel, ssBody, - new GotoCmd(ec.tok, new List {ec.Body.BigBlocks[0].LabelName})); + new GotoCmd(ec.tok, new List {ec.Body.BigBlocks[0].LabelName})); blocks.Add(block); } @@ -464,10 +467,10 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) // LoopDone: assume !guard; goto loopSuccessor; TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) + if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ec.tok, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(ec.tok, new List {runOffTheEndLabel}); } else { @@ -478,12 +481,12 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) blocks.Add(block); break; } - case IfCmd ifcmd: + case IfCmd ifCmd: { string predLabel = bigBlock.LabelName; - List predCmds = theSimpleCmds; + var predCmds = theSimpleCmds; - for (; ifcmd != null; ifcmd = ifcmd.ElseIf) + for (; ifCmd != null; ifCmd = ifCmd.ElseIf) { var freshPrefix = FreshPrefix(); string thenLabel = freshPrefix + "_Then"; @@ -493,64 +496,66 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) var ssThen = new List(); var ssElse = new List(); - if (ifcmd.Guard != null) + if (ifCmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(ifCmd.tok, ifCmd.Guard); + 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); + 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 thenGuardTakenCareOf = ifCmd.Thn.PrefixFirstBlock(ssThen, ref thenLabel); bool elseGuardTakenCareOf = false; - if (ifcmd.ElseBlock != null) + if (ifCmd.ElseBlock != null) { - elseGuardTakenCareOf = ifcmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel); + elseGuardTakenCareOf = ifCmd.ElseBlock.PrefixFirstBlock(ssElse, ref elseLabel); } // ... goto Then, Else; var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds, - new GotoCmd(ifcmd.tok, new List {thenLabel, elseLabel})); + 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})); + 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); + CreateBlocks(ifCmd.Thn, remainingBigBlocks == 0 ? runOffTheEndLabel : null); - if (ifcmd.ElseBlock != null) + if (ifCmd.ElseBlock != null) { - Contract.Assert(ifcmd.ElseIf == null); + Contract.Assert(ifCmd.ElseIf == null); if (!elseGuardTakenCareOf) { // Else: assume !guard; goto firstElseBlock; - var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse, - new GotoCmd(ifcmd.tok, new List {ifcmd.ElseBlock.BigBlocks[0].LabelName})); + var elseJumpBlock = new Block(ifCmd.tok, elseLabel, ssElse, + new GotoCmd(ifCmd.tok, new List {ifCmd.ElseBlock.BigBlocks[0].LabelName})); blocks.Add(elseJumpBlock); } // recurse to create the blocks for the else branch - CreateBlocks(ifcmd.ElseBlock, n == 0 ? runOffTheEndLabel : null); + CreateBlocks(ifCmd.ElseBlock, remainingBigBlocks == 0 ? runOffTheEndLabel : null); } - else if (ifcmd.ElseIf != null) + else if (ifCmd.ElseIf != null) { // this is an "else if" predLabel = elseLabel; predCmds = new List(); - if (ifcmd.Guard != null) + if (ifCmd.Guard != null) { - var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard)); - ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List(), null); + var ac = new AssumeCmd(ifCmd.tok, Expr.Not(ifCmd.Guard)) + { + Attributes = new QKeyValue(ifCmd.tok, "partition", new List(), null) + }; predCmds.Add(ac); } } @@ -559,17 +564,17 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) // no else alternative is specified, so else branch is just "skip" // Else: assume !guard; goto ifSuccessor; TransferCmd trCmd; - if (n == 0 && runOffTheEndLabel != null) + if (remainingBigBlocks == 0 && runOffTheEndLabel != null) { // goto the given label instead of the textual successor block - trCmd = new GotoCmd(ifcmd.tok, new List {runOffTheEndLabel}); + trCmd = new GotoCmd(ifCmd.tok, new List {runOffTheEndLabel}); } else { - trCmd = GotoSuccessor(ifcmd.tok, bigBlock); + trCmd = GotoSuccessor(ifCmd.tok, bigBlock); } - var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd); + var block = new Block(ifCmd.tok, elseLabel, ssElse, trCmd); blocks.Add(block); } } @@ -588,7 +593,7 @@ TransferCmd GotoSuccessor(IToken tok, BigBlock b) Contract.Ensures(Contract.Result() != null); if (b.successorBigBlock != null) { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); } else { From 5271205f8c4042022dfef329e64b3eb0c051ac47 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 11:00:34 +0200 Subject: [PATCH 7/8] Moves classes into separate files --- Source/Core/AST/{ => Commands}/AbsyCmd.cs | 494 ------------------ Source/Core/AST/{ => Commands}/CallCmd.cs | 0 Source/Core/AST/{ => Commands}/ChangeScope.cs | 0 .../Core/AST/{ => Commands}/HideRevealCmd.cs | 0 Source/Core/AST/HigherBoogie/BigBlock.cs | 123 +++++ .../BigBlocksResolutionContext.cs | 6 +- Source/Core/AST/HigherBoogie/BreakCmd.cs | 28 + Source/Core/AST/{ => HigherBoogie}/IfCmd.cs | 0 Source/Core/AST/HigherBoogie/StmtList.cs | 134 +++++ .../Core/AST/HigherBoogie/StmtListBuilder.cs | 98 ++++ Source/Core/AST/HigherBoogie/StructuredCmd.cs | 38 ++ .../HigherBoogie/StructuredCmdContracts.cs | 18 + Source/Core/AST/HigherBoogie/WhileCmd.cs | 74 +++ .../Core/AST/{Blocks => LowerBoogie}/Block.cs | 0 .../AST/{Blocks => LowerBoogie}/GotoCmd.cs | 0 .../AST/{Blocks => LowerBoogie}/ReturnCmd.cs | 0 .../{Blocks => LowerBoogie}/TransferCmd.cs | 0 .../TransferCmdContracts.cs | 0 18 files changed, 516 insertions(+), 497 deletions(-) rename Source/Core/AST/{ => Commands}/AbsyCmd.cs (82%) rename Source/Core/AST/{ => Commands}/CallCmd.cs (100%) rename Source/Core/AST/{ => Commands}/ChangeScope.cs (100%) rename Source/Core/AST/{ => Commands}/HideRevealCmd.cs (100%) create mode 100644 Source/Core/AST/HigherBoogie/BigBlock.cs rename Source/Core/AST/{ => HigherBoogie}/BigBlocksResolutionContext.cs (99%) create mode 100644 Source/Core/AST/HigherBoogie/BreakCmd.cs rename Source/Core/AST/{ => HigherBoogie}/IfCmd.cs (100%) create mode 100644 Source/Core/AST/HigherBoogie/StmtList.cs create mode 100644 Source/Core/AST/HigherBoogie/StmtListBuilder.cs create mode 100644 Source/Core/AST/HigherBoogie/StructuredCmd.cs create mode 100644 Source/Core/AST/HigherBoogie/StructuredCmdContracts.cs create mode 100644 Source/Core/AST/HigherBoogie/WhileCmd.cs rename Source/Core/AST/{Blocks => LowerBoogie}/Block.cs (100%) rename Source/Core/AST/{Blocks => LowerBoogie}/GotoCmd.cs (100%) rename Source/Core/AST/{Blocks => LowerBoogie}/ReturnCmd.cs (100%) rename Source/Core/AST/{Blocks => LowerBoogie}/TransferCmd.cs (100%) rename Source/Core/AST/{Blocks => LowerBoogie}/TransferCmdContracts.cs (100%) diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/Commands/AbsyCmd.cs similarity index 82% rename from Source/Core/AST/AbsyCmd.cs rename to Source/Core/AST/Commands/AbsyCmd.cs index f42a4be00..e10114c03 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/Commands/AbsyCmd.cs @@ -3,503 +3,9 @@ using System.Collections.Generic; using System.Linq; using System.Diagnostics.Contracts; -using Set = Microsoft.Boogie.GSet; 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 - } - } - - [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 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))] public abstract class CmdContracts : Cmd { diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/Commands/CallCmd.cs similarity index 100% rename from Source/Core/AST/CallCmd.cs rename to Source/Core/AST/Commands/CallCmd.cs diff --git a/Source/Core/AST/ChangeScope.cs b/Source/Core/AST/Commands/ChangeScope.cs similarity index 100% rename from Source/Core/AST/ChangeScope.cs rename to Source/Core/AST/Commands/ChangeScope.cs 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/HigherBoogie/BigBlock.cs b/Source/Core/AST/HigherBoogie/BigBlock.cs new file mode 100644 index 000000000..dc0370a4a --- /dev/null +++ b/Source/Core/AST/HigherBoogie/BigBlock.cs @@ -0,0 +1,123 @@ +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/BigBlocksResolutionContext.cs b/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs similarity index 99% rename from Source/Core/AST/BigBlocksResolutionContext.cs rename to Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs index 1dfdcca23..bbc781606 100644 --- a/Source/Core/AST/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs @@ -323,7 +323,7 @@ void RecordSuccessors(StmtList stmtList, BigBlock successor) for (int i = stmtList.BigBlocks.Count; 0 <= --i;) { BigBlock big = stmtList.BigBlocks[i]; - big.successorBigBlock = successor; + big.SuccessorBigBlock = successor; if (big.ec is WhileCmd) { @@ -591,9 +591,9 @@ TransferCmd GotoSuccessor(IToken tok, BigBlock b) Contract.Requires(b != null); Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); - if (b.successorBigBlock != null) + if (b.SuccessorBigBlock != null) { - return new GotoCmd(tok, new List {b.successorBigBlock.LabelName}); + return new GotoCmd(tok, new List {b.SuccessorBigBlock.LabelName}); } else { diff --git a/Source/Core/AST/HigherBoogie/BreakCmd.cs b/Source/Core/AST/HigherBoogie/BreakCmd.cs new file mode 100644 index 000000000..3ea89b616 --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/IfCmd.cs b/Source/Core/AST/HigherBoogie/IfCmd.cs similarity index 100% rename from Source/Core/AST/IfCmd.cs rename to Source/Core/AST/HigherBoogie/IfCmd.cs diff --git a/Source/Core/AST/HigherBoogie/StmtList.cs b/Source/Core/AST/HigherBoogie/StmtList.cs new file mode 100644 index 000000000..51407e1c7 --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/HigherBoogie/StmtListBuilder.cs b/Source/Core/AST/HigherBoogie/StmtListBuilder.cs new file mode 100644 index 000000000..dd7b67666 --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/HigherBoogie/StructuredCmd.cs b/Source/Core/AST/HigherBoogie/StructuredCmd.cs new file mode 100644 index 000000000..f95ef14db --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/HigherBoogie/StructuredCmdContracts.cs b/Source/Core/AST/HigherBoogie/StructuredCmdContracts.cs new file mode 100644 index 000000000..b363253d5 --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/HigherBoogie/WhileCmd.cs b/Source/Core/AST/HigherBoogie/WhileCmd.cs new file mode 100644 index 000000000..135bd43ae --- /dev/null +++ b/Source/Core/AST/HigherBoogie/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/AST/Blocks/Block.cs b/Source/Core/AST/LowerBoogie/Block.cs similarity index 100% rename from Source/Core/AST/Blocks/Block.cs rename to Source/Core/AST/LowerBoogie/Block.cs diff --git a/Source/Core/AST/Blocks/GotoCmd.cs b/Source/Core/AST/LowerBoogie/GotoCmd.cs similarity index 100% rename from Source/Core/AST/Blocks/GotoCmd.cs rename to Source/Core/AST/LowerBoogie/GotoCmd.cs diff --git a/Source/Core/AST/Blocks/ReturnCmd.cs b/Source/Core/AST/LowerBoogie/ReturnCmd.cs similarity index 100% rename from Source/Core/AST/Blocks/ReturnCmd.cs rename to Source/Core/AST/LowerBoogie/ReturnCmd.cs diff --git a/Source/Core/AST/Blocks/TransferCmd.cs b/Source/Core/AST/LowerBoogie/TransferCmd.cs similarity index 100% rename from Source/Core/AST/Blocks/TransferCmd.cs rename to Source/Core/AST/LowerBoogie/TransferCmd.cs diff --git a/Source/Core/AST/Blocks/TransferCmdContracts.cs b/Source/Core/AST/LowerBoogie/TransferCmdContracts.cs similarity index 100% rename from Source/Core/AST/Blocks/TransferCmdContracts.cs rename to Source/Core/AST/LowerBoogie/TransferCmdContracts.cs From fa0019d7b3422893defbb875538392deea2e3ced Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 4 Oct 2024 12:52:36 +0200 Subject: [PATCH 8/8] Refactoring --- .../BigBlocksResolutionContext.cs | 45 +++++++++---------- 1 file changed, 20 insertions(+), 25 deletions(-) diff --git a/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs b/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs index bbc781606..a2853c336 100644 --- a/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs +++ b/Source/Core/AST/HigherBoogie/BigBlocksResolutionContext.cs @@ -104,7 +104,7 @@ public List /*!*/ Blocks NameAnonymousBlocks(stmtList); // determine successor blocks - RecordSuccessors(stmtList, null); + AssignSuccessors(stmtList, null); if (this.errorHandler.count == startErrorCount) { @@ -288,61 +288,56 @@ void CheckLegalLabels(StmtList stmtList, StmtList parentContext, BigBlock parent } } - void NameAnonymousBlocks(StmtList stmtList) + private void NameAnonymousBlocks(StmtList stmtList) { Contract.Requires(stmtList != null); foreach (BigBlock b in stmtList.BigBlocks) { - if (b.LabelName == null) - { - b.LabelName = FreshPrefix(); - } + b.LabelName ??= FreshPrefix(); - if (b.ec is WhileCmd) + if (b.ec is WhileCmd whileCmd) { - WhileCmd wcmd = (WhileCmd) b.ec; - NameAnonymousBlocks(wcmd.Body); + NameAnonymousBlocks(whileCmd.Body); } else { - for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf) + for (IfCmd ifCmd = b.ec as IfCmd; ifCmd != null; ifCmd = ifCmd.ElseIf) { - NameAnonymousBlocks(ifcmd.Thn); - if (ifcmd.ElseBlock != null) + NameAnonymousBlocks(ifCmd.Thn); + if (ifCmd.ElseBlock != null) { - NameAnonymousBlocks(ifcmd.ElseBlock); + NameAnonymousBlocks(ifCmd.ElseBlock); } } } } } - void RecordSuccessors(StmtList stmtList, BigBlock successor) + private static void AssignSuccessors(StmtList stmtList, BigBlock next) { Contract.Requires(stmtList != null); for (int i = stmtList.BigBlocks.Count; 0 <= --i;) { - BigBlock big = stmtList.BigBlocks[i]; - big.SuccessorBigBlock = successor; + var current = stmtList.BigBlocks[i]; + current.SuccessorBigBlock = next; - if (big.ec is WhileCmd) + if (current.ec is WhileCmd whileCmd) { - WhileCmd wcmd = (WhileCmd) big.ec; - RecordSuccessors(wcmd.Body, big); + AssignSuccessors(whileCmd.Body, current); } else { - for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.ElseIf) + for (IfCmd ifCmd = current.ec as IfCmd; ifCmd != null; ifCmd = ifCmd.ElseIf) { - RecordSuccessors(ifcmd.Thn, successor); - if (ifcmd.ElseBlock != null) + AssignSuccessors(ifCmd.Thn, next); + if (ifCmd.ElseBlock != null) { - RecordSuccessors(ifcmd.ElseBlock, successor); + AssignSuccessors(ifCmd.ElseBlock, next); } } } - successor = big; + next = current; } } @@ -586,7 +581,7 @@ private void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) } } - TransferCmd GotoSuccessor(IToken tok, BigBlock b) + private static TransferCmd GotoSuccessor(IToken tok, BigBlock b) { Contract.Requires(b != null); Contract.Requires(tok != null);