From 39d097578051fdee43bca8d17cb568b99a7be50e Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 22:17:36 +0100 Subject: CmdSeq: farewell --- Source/Core/Absy.cs | 27 +++++--------- Source/Core/AbsyCmd.cs | 48 ++++++++++++------------- Source/Core/BoogiePL.atg | 16 ++++----- Source/Core/DeadVarElim.cs | 6 ++-- Source/Core/Duplicator.cs | 4 +-- Source/Core/Inline.cs | 22 ++++++------ Source/Core/InterProceduralReachabilityGraph.cs | 10 +++--- Source/Core/LinearSets.cs | 6 ++-- Source/Core/LoopUnroll.cs | 16 ++++----- Source/Core/OwickiGries.cs | 42 +++++++++++----------- Source/Core/Parser.cs | 16 ++++----- Source/Core/StandardVisitor.cs | 4 +-- 12 files changed, 103 insertions(+), 114 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8654af37..8d68102a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -604,19 +604,19 @@ namespace Microsoft.Boogie { } } - CmdSeq cmdSeq; + List cmdSeq; if (headRecursion) - cmdSeq = new CmdSeq(); + cmdSeq = new List(); else { CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone(); addUniqueCallAttr(si_unique_loc, callCmd); si_unique_loc++; - cmdSeq = new CmdSeq(callCmd); + cmdSeq = new List { callCmd }; } Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy", - new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken)); + new List{ new AssumeCmd(Token.NoToken, Expr.False) }, new ReturnCmd(Token.NoToken)); Block/*!*/ block2 = new Block(Token.NoToken, block1.Label, cmdSeq, new ReturnCmd(Token.NoToken)); impl.Blocks.Add(block1); @@ -639,7 +639,7 @@ namespace Microsoft.Boogie { blockMap[block1] = block2; } List/*!*/ blocks = new List(); - Block exit = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken)); + Block exit = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); GotoCmd cmd = new GotoCmd(Token.NoToken, new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label), new BlockSeq(blockMap[header], exit)); @@ -650,7 +650,7 @@ namespace Microsoft.Boogie { new BlockSeq(blockMap[header])); Block entry; - CmdSeq initCmds = new CmdSeq(); + List initCmds = new List(); if (loopHeaderToAssignCmd.ContainsKey(header)) { AssignCmd assignCmd = loopHeaderToAssignCmd[header]; initCmds.Add(assignCmd); @@ -700,7 +700,7 @@ namespace Microsoft.Boogie { string lastIterBlockName = header.Label + "_last"; Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd); newBlocksCreated[header] = lastIterBlock; - header.Cmds = new CmdSeq(loopHeaderToCallCmd1[header]); + header.Cmds = new List { loopHeaderToCallCmd1[header] }; header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock)); impl.Blocks.Add(lastIterBlock); blockMap[origHeader] = blockMap[header]; @@ -821,7 +821,7 @@ namespace Microsoft.Boogie { gotoCmd.labelTargets.Remove(splitCandidate); CodeCopier codeCopier = new CodeCopier(new Hashtable(), new Hashtable()); - CmdSeq newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds); + List newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds); TransferCmd newTransferCmd; GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd; if (splitGotoCmd == null) { @@ -3234,17 +3234,6 @@ namespace Microsoft.Boogie { } } - public sealed class CmdSeq : List { - public CmdSeq(params Cmd[]/*!*/ args) - : base(args) { - Contract.Requires(args != null); - } - public CmdSeq(CmdSeq/*!*/ cmdSeq) - : base(cmdSeq) { - Contract.Requires(cmdSeq != null); - } - } - public sealed class ExprSeq : List { public ExprSeq(params Expr[]/*!*/ args) : base(args) { diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index ace4e7b6..a11d53a2 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -34,13 +34,13 @@ namespace Microsoft.Boogie { public readonly bool Anonymous; [Rep] - public CmdSeq/*!*/ simpleCmds; + public List/*!*/ simpleCmds; public StructuredCmd ec; public TransferCmd tc; public BigBlock successorBigBlock; // null if successor is end of procedure body (or if field has not yet been initialized) - public BigBlock(IToken tok, string labelName, [Captured] CmdSeq simpleCmds, StructuredCmd ec, TransferCmd tc) { + 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); @@ -75,7 +75,7 @@ namespace Microsoft.Boogie { public class StmtList { [Rep] public readonly List/*!*/ BigBlocks; - public CmdSeq PrefixCommands; + public List PrefixCommands; public readonly IToken/*!*/ EndCurly; public StmtList ParentContext; public BigBlock ParentBigBlock; @@ -122,7 +122,7 @@ namespace Microsoft.Boogie { /// 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] CmdSeq prefixCmds, ref string suggestedLabel) { + 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 @@ -162,7 +162,7 @@ namespace Microsoft.Boogie { public class StmtListBuilder { List/*!*/ bigBlocks = new List(); string label; - CmdSeq simpleCmds; + List simpleCmds; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(bigBlocks)); @@ -175,7 +175,7 @@ namespace Microsoft.Boogie { // nothing to do } else { if (simpleCmds == null) { - simpleCmds = new CmdSeq(); + simpleCmds = new List(); } bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd)); label = null; @@ -192,7 +192,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); Dump(null, null); if (bigBlocks.Count == 0) { - simpleCmds = new CmdSeq(); // the StmtList constructor doesn't like an empty list of BigBlock's + simpleCmds = new List(); // the StmtList constructor doesn't like an empty list of BigBlock's Dump(null, null); } return new StmtList(bigBlocks, endCurlyBrace); @@ -201,7 +201,7 @@ namespace Microsoft.Boogie { public void Add(Cmd cmd) { Contract.Requires(cmd != null); if (simpleCmds == null) { - simpleCmds = new CmdSeq(); + simpleCmds = new List(); } simpleCmds.Add(cmd); } @@ -453,17 +453,17 @@ namespace Microsoft.Boogie { void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) { Contract.Requires(stmtList != null); Contract.Requires(blocks != null); - CmdSeq cmdPrefixToApply = stmtList.PrefixCommands; + List cmdPrefixToApply = stmtList.PrefixCommands; int n = stmtList.BigBlocks.Count; foreach (BigBlock b in stmtList.BigBlocks) { n--; Contract.Assert(b.LabelName != null); - CmdSeq theSimpleCmds; + List theSimpleCmds; if (cmdPrefixToApply == null) { theSimpleCmds = b.simpleCmds; } else { - theSimpleCmds = new CmdSeq(); + theSimpleCmds = new List(); theSimpleCmds.AddRange(cmdPrefixToApply); theSimpleCmds.AddRange(b.simpleCmds); cmdPrefixToApply = null; // now, we've used 'em up @@ -499,8 +499,8 @@ namespace Microsoft.Boogie { string loopDoneLabel = prefix + anon + "_LoopDone"; anon++; - CmdSeq ssBody = new CmdSeq(); - CmdSeq ssDone = new CmdSeq(); + 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); @@ -519,7 +519,7 @@ namespace Microsoft.Boogie { blocks.Add(block); // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody; - CmdSeq ssHead = new CmdSeq(); + List ssHead = new List(); foreach (PredicateCmd inv in wcmd.Invariants) { ssHead.Add(inv); } @@ -549,7 +549,7 @@ namespace Microsoft.Boogie { } else { IfCmd ifcmd = (IfCmd)b.ec; string predLabel = b.LabelName; - CmdSeq predCmds = theSimpleCmds; + List predCmds = theSimpleCmds; for (; ifcmd != null; ifcmd = ifcmd.elseIf) { string thenLabel = prefix + anon + "_Then"; @@ -558,8 +558,8 @@ namespace Microsoft.Boogie { Contract.Assert(elseLabel != null); anon++; - CmdSeq ssThen = new CmdSeq(); - CmdSeq ssElse = new CmdSeq(); + 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); @@ -605,7 +605,7 @@ namespace Microsoft.Boogie { } else if (ifcmd.elseIf != null) { // this is an "else if" predLabel = elseLabel; - predCmds = new CmdSeq(); + 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); @@ -796,7 +796,7 @@ namespace Microsoft.Boogie { public 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 [Rep] [ElementsPeer] - public CmdSeq/*!*/ Cmds; + public List/*!*/ Cmds; [Rep] //PM: needed to verify Traverse.Visit public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures) @@ -837,11 +837,11 @@ namespace Microsoft.Boogie { } public Block() - : this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken)) { + : this(Token.NoToken, "", new List(), new ReturnCmd(Token.NoToken)) { } - public Block(IToken tok, string/*!*/ label, CmdSeq/*!*/ cmds, TransferCmd transferCmd) + public Block(IToken tok, string/*!*/ label, List/*!*/ cmds, TransferCmd transferCmd) : base(tok) { Contract.Requires(label != null); Contract.Requires(cmds != null); @@ -1536,9 +1536,9 @@ namespace Microsoft.Boogie { } public /*readonly, except for the StandardVisitor*/ List/*!*/ Locals; - public /*readonly, except for the StandardVisitor*/ CmdSeq/*!*/ Cmds; + public /*readonly, except for the StandardVisitor*/ List/*!*/ Cmds; - public StateCmd(IToken tok, List/*!*/ locals, CmdSeq/*!*/ cmds) + public StateCmd(IToken tok, List/*!*/ locals, List/*!*/ cmds) : base(tok) { Contract.Requires(locals != null); Contract.Requires(cmds != null); @@ -2033,7 +2033,7 @@ namespace Microsoft.Boogie { protected override Cmd ComputeDesugaring() { Contract.Ensures(Contract.Result() != null); - CmdSeq newBlockBody = new CmdSeq(); + List newBlockBody = new List(); Dictionary substMap = new Dictionary(); Dictionary substMapOld = new Dictionary(); Dictionary substMapBound = new Dictionary(); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 4b20e4a7..a8a03567 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -84,7 +84,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) Pgm = new Program(); dummyExpr = new LiteralExpr(Token.NoToken, false); dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr); - dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken)); + dummyBlock = new Block(Token.NoToken, "dummyBlock", new List(), new ReturnCmd(Token.NoToken)); dummyType = new BasicType(Token.NoToken, SimpleType.Bool); dummyExprSeq = new ExprSeq (); dummyTransferCmd = new ReturnCmd(Token.NoToken); @@ -681,7 +681,7 @@ StmtList = (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List bigblocks = new List(); /* built-up state for the current BigBlock: */ IToken startToken = null; string currentLabel = null; - CmdSeq cs = null; /* invariant: startToken != null ==> cs != null */ + List cs = null; /* invariant: startToken != null ==> cs != null */ /* temporary variables: */ IToken label; Cmd c; BigBlock b; StructuredCmd ec = null; StructuredCmd/*!*/ ecn; @@ -693,7 +693,7 @@ StmtList (. if (c != null) { // LabelOrCmd read a Cmd Contract.Assert(label == null); - if (startToken == null) { startToken = c.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = c.tok; cs = new List(); } Contract.Assert(cs != null); cs.Add(c); } else { @@ -708,13 +708,13 @@ StmtList } startToken = label; currentLabel = label.val; - cs = new CmdSeq(); + cs = new List(); } .) | StructuredCmd (. ec = ecn; - if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = ec.tok; cs = new List(); } Contract.Assert(cs != null); b = new BigBlock(startToken, currentLabel, cs, ec, null); bigblocks.Add(b); @@ -723,7 +723,7 @@ StmtList | TransferCmd (. tc = tcn; - if (startToken == null) { startToken = tc.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = tc.tok; cs = new List(); } Contract.Assert(cs != null); b = new BigBlock(startToken, currentLabel, cs, null, tc); bigblocks.Add(b); @@ -735,7 +735,7 @@ StmtList "}" (. IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { - startToken = t; cs = new CmdSeq(); + startToken = t; cs = new List(); } if (startToken != null) { Contract.Assert(cs != null); @@ -1314,7 +1314,7 @@ CodeExpression<.out List/*!*/ locals, out List/*!*/ blocks SpecBlock = (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y; Cmd c; IToken label; - CmdSeq cs = new CmdSeq(); + List cs = new List(); List/*!*/ xs; StringSeq ss = new StringSeq(); b = dummyBlock; diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 62dfa03f..356ff272 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -388,7 +388,7 @@ namespace Microsoft.Boogie { } } - CmdSeq cmds = block.Cmds; + List cmds = block.Cmds; int len = cmds.Count; for (int i = len - 1; i >= 0; i--) { if (cmds[i] is CallCmd) { @@ -469,7 +469,7 @@ namespace Microsoft.Boogie { Propagate(sugCmd.Desugaring, liveSet); } else if (cmd is StateCmd) { StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd); - CmdSeq/*!*/ cmds = cce.NonNull(stCmd.Cmds); + List/*!*/ cmds = cce.NonNull(stCmd.Cmds); int len = cmds.Count; for (int i = len - 1; i >= 0; i--) { Propagate(cmds[i], liveSet); @@ -1461,7 +1461,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; } else if (cmd is StateCmd) { StateCmd/*!*/ stCmd = (StateCmd)cmd; Contract.Assert(stCmd != null); - CmdSeq/*!*/ cmds = stCmd.Cmds; + List/*!*/ cmds = stCmd.Cmds; Contract.Assert(cmds != null); int len = cmds.Count; ret = GenKillWeight.one(); diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 019711e7..e59dd27e 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -118,9 +118,9 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return base.VisitChoice((Choice)node.Clone()); } - public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) { + public override List VisitCmdSeq(List cmdSeq) { //Contract.Requires(cmdSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); return base.VisitCmdSeq(cmdSeq); } public override Constant VisitConstant(Constant node) { diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 07c44bac..0d412fbc 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -220,8 +220,8 @@ namespace Microsoft.Boogie { foreach (Block block in blocks) { TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd); - CmdSeq cmds = block.Cmds; - CmdSeq newCmds = new CmdSeq(); + List cmds = block.Cmds; + List newCmds = new List(); Block newBlock; string label = block.Label; int lblCount = 0; @@ -296,7 +296,7 @@ namespace Microsoft.Boogie { newBlocks.AddRange(inlinedBlocks); lblCount = nextlblCount; - newCmds = new CmdSeq(); + newCmds = new List(); } else if (inline == 0) { inlinedSomething = true; if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) { @@ -413,8 +413,8 @@ namespace Microsoft.Boogie { } } - private CmdSeq RemoveAsserts(CmdSeq cmds) { - CmdSeq newCmdSeq = new CmdSeq(); + private List RemoveAsserts(List cmds) { + List newCmdSeq = new List(); for (int i = 0; i < cmds.Count; i++) { Cmd cmd = cmds[i]; if (cmd is AssertCmd) continue; @@ -442,7 +442,7 @@ namespace Microsoft.Boogie { List/*!*/ inlinedBlocks = new List(); // create in block - CmdSeq inCmds = new CmdSeq(); + List inCmds = new List(); // assign in parameters for (int i = 0; i < impl.InParams.Count; ++i) { @@ -516,7 +516,7 @@ namespace Microsoft.Boogie { // inject the blocks of the implementation Block intBlock; foreach (Block block in implBlocks) { - CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds); + List copyCmds = codeCopier.CopyCmdSeq(block.Cmds); if (0 <= inlineDepth) { copyCmds = RemoveAsserts(copyCmds); } @@ -526,7 +526,7 @@ namespace Microsoft.Boogie { } // create out block - CmdSeq outCmds = new CmdSeq(); + List outCmds = new List(); // inject ensures for (int i = 0; i < proc.Ensures.Count; i++) { @@ -603,10 +603,10 @@ namespace Microsoft.Boogie { public CodeCopier() { } - public CmdSeq CopyCmdSeq(CmdSeq cmds) { + public List CopyCmdSeq(List cmds) { Contract.Requires(cmds != null); - Contract.Ensures(Contract.Result() != null); - CmdSeq newCmds = new CmdSeq(); + Contract.Ensures(Contract.Result>() != null); + List newCmds = new List(); foreach (Cmd/*!*/ cmd in cmds) { Contract.Assert(cmd != null); newCmds.Add(CopyCmd(cmd)); diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs index e103c628..eb34065f 100644 --- a/Source/Core/InterProceduralReachabilityGraph.cs +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -122,7 +122,7 @@ namespace Microsoft.Boogie { if (!newProcedureEntryNodes.ContainsKey(proc.Name)) { - Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq())); + Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List(), new GotoCmd(Token.NoToken, new BlockSeq())); nodes.Add(newBlock); newProcedureEntryNodes[proc.Name] = newBlock; newProcedureExitNodes[proc.Name] = newBlock; @@ -137,7 +137,7 @@ namespace Microsoft.Boogie foreach (var impl in prog.TopLevelDeclarations.OfType()) { string exitLabel = "__" + impl.Name + "_newExit"; - Block newExit = new Block(Token.NoToken, exitLabel, new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq())); + Block newExit = new Block(Token.NoToken, exitLabel, new List(), new GotoCmd(Token.NoToken, new BlockSeq())); nodes.Add(newExit); newProcedureExitNodes[impl.Name] = newExit; foreach (Block b in impl.Blocks) @@ -150,7 +150,7 @@ namespace Microsoft.Boogie Block newBlock; if (prev == null) { - newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new CmdSeq(cmds.ToArray()), null); + newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new List(cmds.ToArray()), null); nodes.Add(newBlock); originalToNew[b] = newBlock; if (impl.Blocks[0] == b) @@ -161,7 +161,7 @@ namespace Microsoft.Boogie else { string label = "__" + impl.Name + "_" + b.Label + "_call_" + i; - newBlock = new Block(b.tok, label, new CmdSeq(cmds.ToArray()), null); + newBlock = new Block(b.tok, label, new List(cmds.ToArray()), null); nodes.Add(newBlock); originalToNew[newBlock] = newBlock; prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { label }, new BlockSeq { newBlock }); @@ -190,7 +190,7 @@ namespace Microsoft.Boogie #endregion } - private List> PartitionCmds(CmdSeq cmds) { + private List> PartitionCmds(List cmds) { List> result = new List>(); List current = new List(); result.Add(current); diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 957718fa..00caea52 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -365,7 +365,7 @@ namespace Microsoft.Boogie return base.VisitCallCmd(node); } - private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary domainNameToInputVar) + private void AddDisjointnessExpr(List newCmds, Absy absy, Dictionary domainNameToInputVar) { Dictionary> domainNameToScope = new Dictionary>(); foreach (var domainName in linearDomains.Keys) @@ -412,7 +412,7 @@ namespace Microsoft.Boogie foreach (Block b in impl.Blocks) { - CmdSeq newCmds = new CmdSeq(); + List newCmds = new List(); for (int i = 0; i < b.Cmds.Count; i++) { Cmd cmd = b.Cmds[i]; @@ -478,7 +478,7 @@ namespace Microsoft.Boogie { foreach (Block header in g.Headers) { - CmdSeq newCmds = new CmdSeq(); + List newCmds = new List(); AddDisjointnessExpr(newCmds, header, domainNameToInputVar); newCmds.AddRange(header.Cmds); header.Cmds = newCmds; diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index 249e4249..a67f23f7 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -70,7 +70,7 @@ namespace Microsoft.Boogie { class GraphNode { public readonly Block/*!*/ Block; - public readonly CmdSeq/*!*/ Body; + public readonly List/*!*/ Body; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Block != null); @@ -94,16 +94,16 @@ namespace Microsoft.Boogie { [Rep] public readonly List/*!*/ Predecessors = new List(); - GraphNode(Block b, CmdSeq body) { + GraphNode(Block b, List body) { Contract.Requires(body != null); Contract.Requires(b != null); this.Block = b; this.Body = body; } - static CmdSeq GetOptimizedBody(CmdSeq cmds) { + static List GetOptimizedBody(List cmds) { Contract.Requires(cmds != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); int n = 0; foreach (Cmd c in cmds) { n++; @@ -114,7 +114,7 @@ namespace Microsoft.Boogie { for (int i = 0; i < n; i++) { s[i] = cmds[i]; } - return new CmdSeq(s); + return new List(s); } } return cmds; @@ -140,7 +140,7 @@ namespace Microsoft.Boogie { } } else { - CmdSeq body = GetOptimizedBody(b.Cmds); + List body = GetOptimizedBody(b.Cmds); g = new GraphNode(b, body); gd.Add(b, g); if (from != null) { @@ -224,13 +224,13 @@ namespace Microsoft.Boogie { Contract.Assert(nw != null); } else { - CmdSeq body; + List body; TransferCmd tcmd; Contract.Assert(orig.TransferCmd != null); if (next == null && node.IsCutPoint) { // as the body, use the assert/assume commands that make up the loop invariant - body = new CmdSeq(); + body = new List(); foreach (Cmd/*!*/ c in node.Body) { Contract.Assert(c != null); if (c is PredicateCmd || c is CommentCmd) { diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index cbaff3ef..1d0eb0fd 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -180,7 +180,7 @@ namespace Microsoft.Boogie yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); } - private void AddCallToYieldProc(CmdSeq newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + private void AddCallToYieldProc(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) { ExprSeq exprSeq = new ExprSeq(); foreach (string domainName in linearTypechecker.linearDomains.Keys) @@ -213,7 +213,7 @@ namespace Microsoft.Boogie return domainNameToExpr; } - private void AddUpdatesToOldGlobalVars(CmdSeq newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) + private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) { List lhss = new List(); List rhss = new List(); @@ -233,7 +233,7 @@ namespace Microsoft.Boogie } } - private void DesugarYield(YieldCmd yieldCmd, CmdSeq cmds, CmdSeq newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) + private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) { AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); @@ -317,7 +317,7 @@ namespace Microsoft.Boogie return proc; } - private void CreateYieldCheckerImpl(DeclWithFormals decl, List yields, Dictionary map) + private void CreateYieldCheckerImpl(DeclWithFormals decl, List> yields, Dictionary map) { if (yields.Count == 0) return; @@ -373,15 +373,15 @@ namespace Microsoft.Boogie List yieldCheckerBlocks = new List(); StringSeq labels = new StringSeq(); BlockSeq labelTargets = new BlockSeq(); - Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken)); + Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); labels.Add(yieldCheckerBlock.Label); labelTargets.Add(yieldCheckerBlock); yieldCheckerBlocks.Add(yieldCheckerBlock); int yieldCount = 0; - foreach (CmdSeq cs in yields) + foreach (List cs in yields) { var linearDomains = linearTypechecker.linearDomains; - CmdSeq newCmds = new CmdSeq(); + List newCmds = new List(); foreach (Cmd cmd in cs) { PredicateCmd predCmd = (PredicateCmd)cmd; @@ -402,7 +402,7 @@ namespace Microsoft.Boogie labelTargets.Add(yieldCheckerBlock); yieldCheckerBlocks.Add(yieldCheckerBlock); } - yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets))); + yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets))); // Create the yield checker procedure var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name); @@ -452,12 +452,12 @@ namespace Microsoft.Boogie } // Collect the yield predicates and desugar yields - List yields = new List(); - CmdSeq cmds = new CmdSeq(); + List> yields = new List>(); + List cmds = new List(); foreach (Block b in impl.Blocks) { YieldCmd yieldCmd = null; - CmdSeq newCmds = new CmdSeq(); + List newCmds = new List(); for (int i = 0; i < b.Cmds.Count; i++) { Cmd cmd = b.Cmds[i]; @@ -475,7 +475,7 @@ namespace Microsoft.Boogie if (cmds.Count > 0) { yields.Add(cmds); - cmds = new CmdSeq(); + cmds = new List(); } yieldCmd = null; } @@ -538,7 +538,7 @@ namespace Microsoft.Boogie if (cmds.Count > 0) { yields.Add(cmds); - cmds = new CmdSeq(); + cmds = new List(); } } if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart)) @@ -565,7 +565,7 @@ namespace Microsoft.Boogie AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); } - CmdSeq newCmds = new CmdSeq(); + List newCmds = new List(); foreach (string domainName in linearTypechecker.linearDomains.Keys) { newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); @@ -611,7 +611,7 @@ namespace Microsoft.Boogie } if (lhss.Count > 0) { - Block initBlock = new Block(Token.NoToken, "og_init", new CmdSeq(new AssignCmd(Token.NoToken, lhss, rhss)), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))); + Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))); impl.Blocks.Insert(0, initBlock); } } @@ -637,8 +637,8 @@ namespace Microsoft.Boogie } // Collect the yield predicates and desugar yields - List yields = new List(); - CmdSeq cmds = new CmdSeq(); + List> yields = new List>(); + List cmds = new List(); if (proc.Requires.Count > 0) { Dictionary> domainNameToScope = new Dictionary>(); @@ -676,7 +676,7 @@ namespace Microsoft.Boogie } } yields.Add(cmds); - cmds = new CmdSeq(); + cmds = new List(); } if (info.inParallelCall && proc.Ensures.Count > 0) { @@ -715,7 +715,7 @@ namespace Microsoft.Boogie } } yields.Add(cmds); - cmds = new CmdSeq(); + cmds = new List(); } CreateYieldCheckerImpl(proc, yields, new Dictionary()); } @@ -752,14 +752,14 @@ namespace Microsoft.Boogie CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); callCmd.Proc = proc; string label = string.Format("L_{0}", labelCount++); - Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken)); + Block block = new Block(Token.NoToken, label, new List { callCmd }, new ReturnCmd(Token.NoToken)); labelTargets.Add(label); blockTargets.Add(block); blocks.Add(block); } transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); } - blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd)); + blocks.Insert(0, new Block(Token.NoToken, "enter", new List(), transferCmd)); var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new List(), new List(), blocks); yieldImpl.Proc = yieldProc; diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index b0ce346a..bcdd01d8 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -104,7 +104,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) Pgm = new Program(); dummyExpr = new LiteralExpr(Token.NoToken, false); dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr); - dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken)); + dummyBlock = new Block(Token.NoToken, "dummyBlock", new List(), new ReturnCmd(Token.NoToken)); dummyType = new BasicType(Token.NoToken, SimpleType.Bool); dummyExprSeq = new ExprSeq (); dummyTransferCmd = new ReturnCmd(Token.NoToken); @@ -924,7 +924,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List bigblocks = new List(); /* built-up state for the current BigBlock: */ IToken startToken = null; string currentLabel = null; - CmdSeq cs = null; /* invariant: startToken != null ==> cs != null */ + List cs = null; /* invariant: startToken != null ==> cs != null */ /* temporary variables: */ IToken label; Cmd c; BigBlock b; StructuredCmd ec = null; StructuredCmd/*!*/ ecn; @@ -936,7 +936,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { if (c != null) { // LabelOrCmd read a Cmd Contract.Assert(label == null); - if (startToken == null) { startToken = c.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = c.tok; cs = new List(); } Contract.Assert(cs != null); cs.Add(c); } else { @@ -951,13 +951,13 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } startToken = label; currentLabel = label.val; - cs = new CmdSeq(); + cs = new List(); } } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { StructuredCmd(out ecn); ec = ecn; - if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = ec.tok; cs = new List(); } Contract.Assert(cs != null); b = new BigBlock(startToken, currentLabel, cs, ec, null); bigblocks.Add(b); @@ -966,7 +966,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else { TransferCmd(out tcn); tc = tcn; - if (startToken == null) { startToken = tc.tok; cs = new CmdSeq(); } + if (startToken == null) { startToken = tc.tok; cs = new List(); } Contract.Assert(cs != null); b = new BigBlock(startToken, currentLabel, cs, null, tc); bigblocks.Add(b); @@ -977,7 +977,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Expect(28); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { - startToken = t; cs = new CmdSeq(); + startToken = t; cs = new List(); } if (startToken != null) { Contract.Assert(cs != null); @@ -1924,7 +1924,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { void SpecBlock(out Block/*!*/ b) { Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y; Cmd c; IToken label; - CmdSeq cs = new CmdSeq(); + List cs = new List(); List/*!*/ xs; StringSeq ss = new StringSeq(); b = dummyBlock; diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 8f5cf64b..987eadb8 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -168,9 +168,9 @@ namespace Microsoft.Boogie { node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i])); return node; } - public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) { + public virtual List VisitCmdSeq(List cmdSeq) { Contract.Requires(cmdSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); for (int i = 0, n = cmdSeq.Count; i < n; i++) cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor return cmdSeq; -- cgit v1.2.3