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/Predication/BlockPredicator.cs | 26 +++++++++++++------------- Source/Predication/SmartBlockPredicator.cs | 18 +++++++++--------- Source/Predication/UniformityAnalyser.cs | 2 +- 3 files changed, 23 insertions(+), 23 deletions(-) (limited to 'Source/Predication') diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index c655175a..771d403b 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -61,7 +61,7 @@ public class BlockPredicator { } } - void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) { + void PredicateCmd(List cmdSeq, Cmd cmd) { if (cmd is AssignCmd) { var aCmd = (AssignCmd)cmd; cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss, @@ -125,7 +125,7 @@ public class BlockPredicator { } else if (cmd is StateCmd) { var sCmd = (StateCmd)cmd; - var newCmdSeq = new CmdSeq(); + var newCmdSeq = new List(); foreach (Cmd c in sCmd.Cmds) PredicateCmd(newCmdSeq, c); sCmd.Cmds = newCmdSeq; @@ -136,7 +136,7 @@ public class BlockPredicator { } } - void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) { + void PredicateTransferCmd(List cmdSeq, TransferCmd cmd) { if (cmd is GotoCmd) { var gCmd = (GotoCmd)cmd; var targets = new List( @@ -161,7 +161,7 @@ public class BlockPredicator { aCmd.Expr))); } b.Cmds = - new CmdSeq(b.Cmds.Cast().Skip(assumes.Count()).ToArray()); + new List(b.Cmds.Cast().Skip(assumes.Count()).ToArray()); } } } @@ -201,9 +201,9 @@ public class BlockPredicator { Block entryBlock = new Block(); entryBlock.Label = "entry"; - entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, + entryBlock.Cmds = new List { Cmd.SimpleAssign(Token.NoToken, cur, CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1], - returnBlockId))); + returnBlockId)) }; newBlocks.Add(entryBlock); var prevBlock = entryBlock; @@ -213,9 +213,9 @@ public class BlockPredicator { newBlocks.Add(backedgeBlock); backedgeBlock.Label = n.Item1.Label + ".backedge"; - backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, + backedgeBlock.Cmds = new List { new AssumeCmd(Token.NoToken, Expr.Eq(cur, blockIds[n.Item1]), - new QKeyValue(Token.NoToken, "backedge", new List(), null))); + new QKeyValue(Token.NoToken, "backedge", new List(), null)) }; backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(n.Item1)); @@ -223,8 +223,8 @@ public class BlockPredicator { newBlocks.Add(tailBlock); tailBlock.Label = n.Item1.Label + ".tail"; - tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, - Expr.Neq(cur, blockIds[n.Item1]))); + tailBlock.Cmds = new List { new AssumeCmd(Token.NoToken, + Expr.Neq(cur, blockIds[n.Item1])) }; prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(backedgeBlock, tailBlock)); @@ -232,7 +232,7 @@ public class BlockPredicator { } else { var runBlock = n.Item1; var oldCmdSeq = runBlock.Cmds; - runBlock.Cmds = new CmdSeq(); + runBlock.Cmds = new List(); newBlocks.Add(runBlock); prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(runBlock)); @@ -267,13 +267,13 @@ public class BlockPredicator { } } - private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { + private void AddUniformCandidateInvariant(List cs, Block header) { cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur, CreateIfFPThenElse(blockIds[header], returnBlockId)), "uniform loop")); } - private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) { + private void AddNonUniformCandidateInvariant(List cs, Block header) { var loopNodes = new HashSet(); foreach (var b in blockGraph.BackEdgeNodes(header)) loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 28005186..94b47f5e 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -72,7 +72,7 @@ public class SmartBlockPredicator { } } - void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) { + void PredicateCmd(Expr p, List cmdSeq, Cmd cmd) { if (cmd is CallCmd) { var cCmd = (CallCmd)cmd; Debug.Assert(useProcedurePredicates(cCmd.Proc)); @@ -125,7 +125,7 @@ public class SmartBlockPredicator { // skip } else if (cmd is StateCmd) { var sCmd = (StateCmd)cmd; - var newCmdSeq = new CmdSeq(); + var newCmdSeq = new List(); foreach (Cmd c in sCmd.Cmds) PredicateCmd(p, newCmdSeq, c); sCmd.Cmds = newCmdSeq; @@ -137,7 +137,7 @@ public class SmartBlockPredicator { // hasPredicatedRegion is true iff the block or its targets are predicated // (i.e. we enter, stay within or exit a predicated region). - void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) { + void PredicateTransferCmd(Expr p, Block src, List cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) { hasPredicatedRegion = predMap.ContainsKey(src); if (cmd is GotoCmd) { @@ -347,7 +347,7 @@ public class SmartBlockPredicator { if (parts.Count() > 0) { pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And); block.Cmds = - new CmdSeq(block.Cmds.Cast().Skip(parts.Count()).ToArray()); + new List(block.Cmds.Cast().Skip(parts.Count()).ToArray()); } else { continue; } @@ -386,8 +386,8 @@ public class SmartBlockPredicator { newBlocks.Add(backedgeBlock); backedgeBlock.Label = n.Item1.Label + ".backedge"; - backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr, - new QKeyValue(Token.NoToken, "backedge", new List(), null))); + backedgeBlock.Cmds = new List { new AssumeCmd(Token.NoToken, pExpr, + new QKeyValue(Token.NoToken, "backedge", new List(), null)) }; backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(n.Item1)); @@ -395,8 +395,8 @@ public class SmartBlockPredicator { newBlocks.Add(tailBlock); tailBlock.Label = n.Item1.Label + ".tail"; - tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, - Expr.Not(pExpr))); + tailBlock.Cmds = new List { new AssumeCmd(Token.NoToken, + Expr.Not(pExpr)) }; if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) { uni.AddNonUniform(impl.Name, backedgeBlock); @@ -427,7 +427,7 @@ public class SmartBlockPredicator { var firstBlock = block; var oldCmdSeq = block.Cmds; - block.Cmds = new CmdSeq(); + block.Cmds = new List(); newBlocks.Add(block); if (prevBlock != null) { prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block)); diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index a6287db5..3c8f4cd9 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -292,7 +292,7 @@ namespace Microsoft.Boogie return null; } - private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform) + private bool Analyse(Implementation impl, List cmdSeq, bool ControlFlowIsUniform) { foreach (Cmd c in cmdSeq) { -- cgit v1.2.3