diff options
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Core/Absy.ssc | 145 | ||||
-rw-r--r-- | Source/Core/AbsyCmd.ssc | 2 | ||||
-rw-r--r-- | Source/Core/AbsyExpr.ssc | 229 | ||||
-rw-r--r-- | Source/Core/CommandLineOptions.ssc | 137 | ||||
-rw-r--r-- | Source/Core/DeadVarElim.ssc | 4 | ||||
-rw-r--r-- | Source/Core/StandardVisitor.ssc | 8 | ||||
-rw-r--r-- | Source/VCExpr/Boogie2VCExpr.ssc | 9 | ||||
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 191 | ||||
-rw-r--r-- | Source/VCGeneration/VC.ssc | 110 | ||||
-rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 719 |
10 files changed, 633 insertions, 921 deletions
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index 35175881..d6d7bbc5 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -279,16 +279,6 @@ namespace Microsoft.Boogie }
/// <summary>
- /// Instrument the "widen" blocks with a statement in the form of "assume J", where J is a loop predicate "variable"
- /// </summary>
- public void InstrumentWithLoopInvariantPredicates()
- {
- foreach (Declaration d in this.TopLevelDeclarations) {
- d.InstrumentWithLoopInvariantPredicates();
- }
- }
-
- /// <summary>
/// Reset the abstract stated computed before
/// </summary>
public void ResetAbstractInterpretationState()
@@ -440,11 +430,6 @@ namespace Microsoft.Boogie public virtual void InstrumentWithInvariants () {}
/// <summary>
- /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks
- /// </summary>
- public virtual void InstrumentWithLoopInvariantPredicates() { /* by default it does nothing */ }
-
- /// <summary>
/// Reset the abstract stated computed before
/// </summary>
public virtual void ResetAbstractInterpretationState() { /* does nothing */ }
@@ -1993,56 +1978,39 @@ namespace Microsoft.Boogie {
if (b.Lattice != null)
{
- CmdSeq newCommands = new CmdSeq();
-
assert b.PreInvariant != null; /* If the pre-abstract state is null, then something is wrong */
-
- Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
- newCommands.Add(cmd);
- newCommands.AddRange(b.Cmds);
-
assert b.PostInvariant != null; /* If the post-state is null, then something is wrong */
- // if(b.Cmds.Length > 0) // If it is not an empty block
- // {
- inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);
- cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
- newCommands.Add(cmd);
- // }
-
- b.Cmds = newCommands;
- }
- }
- }
-
- /// <summary>
- /// Insert a statement "assume J", for an opportune J - loop invariant predicate - in the "widen" blocks
- /// </summary>
- override public void InstrumentWithLoopInvariantPredicates()
- {
- foreach(Block b in this.Blocks)
- {
- if(b.widenBlock) { // if it is the head of a loop
- CmdSeq newCommands = new CmdSeq();
-
- Block! entryBlock = b;
-
- ICollection<Block!> connectedComponents = this.GetConnectedComponents(b); // Get the connected components from this block
-
- // Duplicate the connected components.
- // Note that as we duplicate all the nodes, in particular we have also to keep track of the *copy* of the entry node.
- // This is the reason why we pass entryBlockByReference
- ICollection<Block!> dupConnectedComponents = duplicate((!) connectedComponents, ref entryBlock);
-
- Expr loopInvariantPredicate = new LoopPredicate(entryBlock, dupConnectedComponents); // Create a new predicate J_{b.Label}
-
- PredicateCmd cmd = new AssumeCmd(Token.NoToken, loopInvariantPredicate);
-
- newCommands.Add(cmd);
- newCommands.AddRange(b.Cmds);
-
- b.Cmds = newCommands;
+ bool instrumentEntry;
+ bool instrumentExit;
+ switch (CommandLineOptions.Clo.InstrumentInfer) {
+ case CommandLineOptions.InstrumentationPlaces.Everywhere:
+ instrumentEntry = true;
+ instrumentExit = true;
+ break;
+ case CommandLineOptions.InstrumentationPlaces.LoopHeaders:
+ instrumentEntry = b.widenBlock;
+ instrumentExit = false;
+ break;
+ default:
+ assert false; // unexpected InstrumentationPlaces value
+ }
+
+ if (instrumentEntry || instrumentExit) {
+ CmdSeq newCommands = new CmdSeq();
+ if (instrumentEntry) {
+ Expr inv = (Expr) b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ newCommands.Add(cmd);
+ }
+ newCommands.AddRange(b.Cmds);
+ if (instrumentExit) {
+ Expr inv = (Expr) b.Lattice.ToPredicate(b.PostInvariant);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken,inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ newCommands.Add(cmd);
+ }
+ b.Cmds = newCommands;
+ }
}
}
}
@@ -2074,8 +2042,6 @@ namespace Microsoft.Boogie }
assert false; // if we are here, it means that the block is not in one of the components. This is an error.
-
- return null; // unreachable code, just to please the compiler
}
/// <summary>
@@ -2164,57 +2130,6 @@ namespace Microsoft.Boogie this.BlockPredecessorsComputed = true;
}
- /// <summary>
- /// Make a deep copy of the set of blocks in the input.
- /// The input must NOT contain two copies of the same block
- /// </summary>
- private ICollection<Block!>! duplicate(ICollection<Block!>! blocks, ref Block! head)
- {
- Dictionary<Block!, Block!> transMap = new Dictionary<Block!, Block!>(); // A map from the old block to a fresh one
-
- foreach(Block! block in blocks) // Create fresh copies for the blocks
- {
- Block! freshBlock = new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); // Construct a copy of the block
- freshBlock.widenBlock = block.widenBlock;
- freshBlock.Predecessors = new BlockSeq();
- transMap.Add(block, freshBlock); // Add a link block -> freshblock
- }
-
- foreach(Block! block in blocks) // Update the references
- {
- Block! freshBlock = transMap[block];
-
- GotoCmd gotoCmd = freshBlock.TransferCmd as GotoCmd;
- if(gotoCmd != null)
- {
- StringSeq! targetNames = new StringSeq();
- BlockSeq! targetBlocks = new BlockSeq();
-
- foreach(Block! next in (!) gotoCmd.labelTargets)
- {
- if(blocks.Contains(next))
- {
- assert transMap[next] != null;
- targetNames.Add(next.Label);
- targetBlocks.Add(transMap[next]);
- }
- }
-
- GotoCmd freshGotoCmd = new GotoCmd(gotoCmd.tok, targetNames, targetBlocks);
- freshBlock.TransferCmd = freshGotoCmd;
- }
- else
- {
- assert freshBlock.TransferCmd is ReturnCmd; // Do nothing as we do not need to update a returnCmd.
- // However, as we want to make the code robust, we check that it is a ReturnCmd
- }
- }
-
- head = transMap[head];
-
- return transMap.Values;
- }
-
public void PruneUnreachableBlocks() {
ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ ();
List<Block!> reachableBlocks = new List<Block!>();
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index 926724cb..41a62515 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -672,7 +672,7 @@ namespace Microsoft.Boogie // Block
public sealed class Block : Absy
{
- public readonly string! Label;
+ 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;
[Rep] //PM: needed to verify Traverse.Visit
public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index baf12310..eaf4e640 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -836,8 +836,6 @@ namespace Microsoft.Boogie T Visit(FunctionCall! functionCall);
- T Visit(LoopPredicateName! loopPredicateName);
-
T Visit(MapSelect! mapSelect);
T Visit(MapStore! mapStore);
@@ -1572,171 +1570,6 @@ namespace Microsoft.Boogie }
- /// <summary>
- /// A subclass of FunctionCall that stands for a zero-argument function call, used as a loop invariant placeholder
- /// </summary>
- public class LoopPredicateName : FunctionCall
- {
- private Block! block; // The block the predicate refers to
- public Block! Block
- {
- get
- {
- return block;
- }
- }
-
- private string! blockName; // The name of the block
- private ICollection<Block!>! component;
- public ICollection<Block!>! Component
- {
- get
- {
- return this.component;
- }
- }
-
- public string! Name
- {
- get
- {
- return "J_" + this.blockName;
- }
- }
-
- invariant block.Label == blockName; // Note that we ask for object equality of strings...
-
- private Hashtable /* Var -> Incarnations */ preHavocIncarnationMap;
- public Hashtable PreHavocIncarnationMap
- {
- get
- {
- return this.preHavocIncarnationMap;
- }
- }
-
- private Hashtable /* Var -> Incarnations */ postHavocIncarnationMap;
- public Hashtable PostHavocIncarnationMap
- {
- get
- {
- return this.postHavocIncarnationMap;
- }
- }
-
-
- // Those below are the inverse maps of the maps between variables and incarnations
- private Hashtable /* String -> Var */ preHavocIncarnationInverseMap;
- private Hashtable /* String -> Var */ postHavocIncarnationInverseMap;
-
- public Hashtable PreHavocInverseMap
- {
- get
- {
- if(this.preHavocIncarnationInverseMap == null)
- {
- this.preHavocIncarnationInverseMap = new Hashtable();
- assert this.preHavocIncarnationMap != null; // If we get at this point, then something is wrong with the program
- foreach(object! key in (!) (this.preHavocIncarnationMap).Keys)
- {
- object! val = (!) this.preHavocIncarnationMap[key];
- if(!this.preHavocIncarnationInverseMap.ContainsKey(val.ToString()))
- this.preHavocIncarnationInverseMap.Add(val.ToString(), key);
- }
- }
- return this.preHavocIncarnationInverseMap;
- }
- }
-
- public Hashtable PostHavocInverseMap
- {
- get
- {
- if(this.postHavocIncarnationInverseMap == null)
- {
- this.postHavocIncarnationInverseMap = new Hashtable();
- assert this.postHavocIncarnationMap != null; // If it is null, something is wrong before...
- foreach(object! key in (!) (this.postHavocIncarnationMap).Keys)
- {
- object! val = (!) this.postHavocIncarnationMap[key];
- if(!this.postHavocIncarnationInverseMap.ContainsKey(val.ToString()))
- this.postHavocIncarnationInverseMap.Add(val.ToString(), key);
- }
- }
- return this.postHavocIncarnationInverseMap;
- }
- }
-
- /// <summary>
- /// Create a new LoopPredicate
- /// </summary>
- public LoopPredicateName(Block! block, ICollection<Block!>! component)
- : base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool))
- {
- this.block = block;
- this.blockName = block.Label;
- this.component = component;
- // base(new IdentifierExpr(Token.NoToken, "J_"+ block.Label, Type.Bool));
- }
-
- public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post)
- {
- assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null;
-
- this.preHavocIncarnationMap = pre;
- this.postHavocIncarnationMap = post;
- }
-
- /// <summary>
- /// Writes down the loop predicate and the incarnations map before and after the havoc statements
- /// </summary>
- public override void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
- string! pre, post;
-
- if(this.postHavocIncarnationMap != null && this.preHavocIncarnationMap != null)
- {
- pre = "pre: [ " + hashtableToString(this.preHavocIncarnationMap) +" ]";
- post = "post: [ " + hashtableToString(this.postHavocIncarnationMap) +" ]";
- }
- else
- {
- pre = post = "[]";
- }
-
- stream.Write("J_" + this.blockName);
- stream.Write("(");
- stream.Write(pre + ", " + post);
- stream.Write(")");
- }
-
- public override Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- return Type.Bool;
- }
-
- public override int ArgumentCount { get { return 0; } }
-
- private string! hashtableToString(Hashtable! map)
- {
- string! outVal = "";
-
- foreach (object! key in map.Keys)
- {
- object val = map[key];
- outVal += key + " -> " + val + ",";
- }
-
- return outVal;
- }
-
- public override T Dispatch<T>(IAppliableVisitor<T>! visitor) {
- return visitor.Visit(this);
- }
-
- }
-
public class NAryExpr : Expr, AI.IFunApp
{
[Additive] [Peer]
@@ -1870,68 +1703,6 @@ namespace Microsoft.Boogie }
}
- /// <summary>
- /// An instance of LoopPredicate stands for a loop invariant predicate
- /// </summary>
- public class LoopPredicate : NAryExpr
- {
- private static ExprSeq! emptyArgs = new ExprSeq(new Expr[0]); // Share the emptylist of arguments among several instances
-
- invariant loopPredicateName == Fun; // loopPredicateName is just a way of subtyping Fun...
- LoopPredicateName! loopPredicateName;
-
- Hashtable /* Var -> Expr */ preHavocIncarnationMap;
- Hashtable /* Var -> Expr */ postHavocIncarnationMap;
-
- private Block! block; // The block the predicate refers to
- private string! BlockName; // Name of the widen block the predicate refers to
- private ICollection<Block!> component; // The component the block belongs to
-
- /// <summary>
- /// Create a predicate (standing for a loop invariant). The parameter are the name of the block and the (strong) connect components the block belongs to
- /// </summary>
- public LoopPredicate(Block! block, ICollection<Block!>! component)
- {
- this.block = block;
- this.BlockName = block.Label;
- this.component = component;
-
- LoopPredicateName! tmp; // to please the compiler we introde a temp variable
- this.loopPredicateName = tmp = new LoopPredicateName(block, component);
- base(Token.NoToken, tmp, emptyArgs); // due to locally computed data
- }
-
- public void SetPreAndPostHavocIncarnationMaps(Hashtable pre, Hashtable post)
- {
- assert this.preHavocIncarnationMap == null && this.postHavocIncarnationMap == null; // The method must be called just once
-
- this.preHavocIncarnationMap = pre;
- this.postHavocIncarnationMap = post;
- this.loopPredicateName.SetPreAndPostHavocIncarnationMaps(pre, post);
- }
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is LoopPredicate)) return false;
-
- LoopPredicate pred = (LoopPredicate) obj;
- return this.BlockName.Equals(pred.BlockName);
- }
-
- [Pure]
- public override int GetHashCode()
- {
- return this.BlockName.GetHashCode();
- }
-
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
- return visitor.VisitLoopPredicate(this);
- }
- }
-
public class MapSelect : IAppliable, AI.IFunctionSymbol {
public readonly int Arity;
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index da8ee0fe..1d16b569 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -75,6 +75,8 @@ namespace Microsoft.Boogie public string! LogPrefix = "";
public bool PrintInstrumented = false;
public bool InstrumentWithAsserts = false;
+ public enum InstrumentationPlaces { LoopHeaders, Everywhere }
+ public InstrumentationPlaces InstrumentInfer = InstrumentationPlaces.LoopHeaders;
public bool PrintWithUniqueASTIds = false;
private string XmlSinkFilename = null;
[Peer] public XmlSink XmlSink = null;
@@ -604,48 +606,46 @@ namespace Microsoft.Boogie break;
case "-proverWarnings":
- case "/proverWarnings":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/proverWarnings": {
+ int pw = 0;
+ if (ps.GetNumericArgument(ref pw, 3)) {
+ switch (pw) {
+ case 0:
PrintProverWarnings = ProverWarnings.None;
break;
- case "1":
+ case 1:
PrintProverWarnings = ProverWarnings.Stdout;
break;
- case "2":
+ case 2:
PrintProverWarnings = ProverWarnings.Stderr;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-env":
- case "/env":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/env": {
+ int e = 0;
+ if (ps.GetNumericArgument(ref e, 3)) {
+ switch (e) {
+ case 0:
ShowEnv = ShowEnvironment.Never;
break;
- case "1":
+ case 1:
ShowEnv = ShowEnvironment.DuringPrint;
break;
- case "2":
+ case 2:
ShowEnv = ShowEnvironment.Always;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-loopUnroll":
case "/loopUnroll":
@@ -805,64 +805,52 @@ namespace Microsoft.Boogie break;
case "-subsumption":
- case "/subsumption":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
+ case "/subsumption": {
+ int s = 0;
+ if (ps.GetNumericArgument(ref s, 3)) {
+ switch (s) {
+ case 0:
UseSubsumption = SubsumptionOption.Never;
break;
- case "1":
+ case 1:
UseSubsumption = SubsumptionOption.NotForQuantifiers;
break;
- case "2":
+ case 2:
UseSubsumption = SubsumptionOption.Always;
break;
default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
+ assert false; // postcondition of GetNumericArgument guarantees that we don't get here
}
}
break;
+ }
case "-liveVariableAnalysis":
- case "/liveVariableAnalysis":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
- LiveVariableAnalysis = false;
- break;
- case "1":
- LiveVariableAnalysis = true;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
+ case "/liveVariableAnalysis": {
+ int lva = 0;
+ if (ps.GetNumericArgument(ref lva, 2)) {
+ LiveVariableAnalysis = lva == 1;
}
break;
+ }
+
+ case "-removeEmptyBlocks":
+ case "/removeEmptyBlocks": {
+ int reb = 0;
+ if (ps.GetNumericArgument(ref reb, 2)) {
+ RemoveEmptyBlocks = reb == 1;
+ }
+ break;
+ }
case "-coalesceBlocks":
- case "/coalesceBlocks":
- if (ps.ConfirmArgumentCount(1))
- {
- switch (args[ps.i])
- {
- case "0":
- CoalesceBlocks = false;
- break;
- case "1":
- CoalesceBlocks = true;
- break;
- default:
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- break;
- }
+ case "/coalesceBlocks": {
+ int cb = 0;
+ if (ps.GetNumericArgument(ref cb, 2)) {
+ CoalesceBlocks = cb == 1;
}
break;
+ }
case "/DoomDebug":
vcVariety = VCVariety.Doomed;
@@ -983,7 +971,25 @@ namespace Microsoft.Boogie }
}
break;
-
+
+ case "-instrumentInfer":
+ case "/instrumentInfer":
+ if (ps.ConfirmArgumentCount(1)) {
+ switch (args[ps.i])
+ {
+ case "e":
+ InstrumentInfer = InstrumentationPlaces.Everywhere;
+ break;
+ case "h":
+ InstrumentInfer = InstrumentationPlaces.LoopHeaders;
+ break;
+ default:
+ ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
+ break;
+ }
+ }
+ break;
+
case "-vcBrackets":
case "/vcBrackets":
ps.GetNumericArgument(ref BracketIdsInVC, 2);
@@ -1163,7 +1169,6 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||
ps.CheckBooleanFlag("overlookTypeErrors", ref OverlookBoogieTypeErrors) ||
ps.CheckBooleanFlag("noVerify", ref Verify, false) ||
- ps.CheckBooleanFlag("noRemoveEmptyBlocks", ref RemoveEmptyBlocks, false) ||
ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||
ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) ||
ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||
@@ -1840,7 +1845,6 @@ namespace Microsoft.Boogie p = polyhedra for linear inequalities
s = debug statistics
0..9 = number of iterations before applying a widen (default=0)
- /loopInvOnDemand : Infer loop invariants on demand
/noinfer : turn off the default inference, and overrides the /infer
switch on its left
/checkInfer : instrument inferred invariants as asserts to be checked by
@@ -1849,6 +1853,10 @@ namespace Microsoft.Boogie supported)
/contractInfer : perform procedure contract inference
/logInfer : print debug output during inference
+ /instrumentInfer : h - instrument inferred invariants only at beginning of
+ loop headers (default)
+ e - instrument inferred invariants at beginning and end
+ of every block
/printInstrumented : print Boogie program after it has been
instrumented with invariants
/Houdini[:<flags>] : perform procedure Houdini
@@ -1869,7 +1877,8 @@ namespace Microsoft.Boogie /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis
1 = perform live variable analysis (default)
/noVerify : skip VC generation and invocation of the theorem prover
- /noRemoveEmptyBlocks : do not remove empty blocks during VC generation
+ /removeEmptyBlocks:<c> : 0 - do not remove empty blocks during VC generation
+ 1 - remove empty blocks (default)
/coalesceBlocks:<c> : 0 = do not coalesce blocks
1 = coalesce blocks (default)
/vc:<variety> : n = nested block (default for non-/prover:z3),
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index 506739bf..0686212e 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -197,8 +197,10 @@ namespace Microsoft.Boogie b.Cmds.Add(cmd);
}
b.TransferCmd = succ.TransferCmd;
- if (!b.tok.IsValid && succ.tok.IsValid)
+ if (!b.tok.IsValid && succ.tok.IsValid) {
b.tok = succ.tok;
+ b.Label = succ.Label;
+ }
removedBlocks.Add(succ);
dfsStack.Push(b);
visitedBlocks.Remove(b);
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index c6b50b24..6e50f6db 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -319,14 +319,6 @@ namespace Microsoft.Boogie return node;
}
- /// <summary>
- /// Just invoke VisitNAryExpr
- /// </summary>
- public virtual Expr! VisitLoopPredicate(LoopPredicate! node)
- {
- return this.VisitNAryExpr(node);
- }
-
public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
{
node.Map = (AssignLhs!)this.Visit(node.Map);
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc index 4698f541..08554344 100644 --- a/Source/VCExpr/Boogie2VCExpr.ssc +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -288,11 +288,6 @@ namespace Microsoft.Boogie.VCExprAST return node;
}
- public override Expr! VisitLoopPredicate(LoopPredicate! node)
- {
- return this.VisitNAryExpr(node);
- }
-
private VCExpr! TranslateNAryExpr(NAryExpr! node) {
int n = node.Args.Length;
List<VCExpr!>! vcs = new List<VCExpr!> (n);
@@ -721,10 +716,6 @@ namespace Microsoft.Boogie.VCExprAST return TranslateFunctionCall(functionCall, this.args, this.typeArgs);
}
- public VCExpr! Visit(LoopPredicateName! loopPredicateName) {
- return Gen.Variable(loopPredicateName.Name, Type.Bool); // We generate a variable. Intuition: it is a second order variable
- }
-
public VCExpr! Visit(MapSelect! mapSelect) {
return Gen.Select(this.args, this.typeArgs);
}
diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc index 922ee68d..7d71f166 100644 --- a/Source/VCGeneration/ConditionGeneration.ssc +++ b/Source/VCGeneration/ConditionGeneration.ssc @@ -251,11 +251,13 @@ namespace VC /// <summary>
- /// Modifies an implementation by inserting all preconditions
- /// as assume statements at the beginning of the implementation
+ /// Modifies an implementation by prepending it with startCmds and then, as assume
+ /// statements, all preconditions. Insert new blocks as needed, and adjust impl.Blocks[0]
+ /// accordingly to make it the new implementation entry block.
/// </summary>
/// <param name="impl"></param>
- protected static void InjectPreconditions(Implementation! impl)
+ /// <param name="startCmds"></param>
+ protected static void InjectPreconditions(Implementation! impl, [Captured] CmdSeq! startCmds)
requires impl.Proc != null;
{
TokenTextWriter debugWriter = null;
@@ -265,68 +267,65 @@ namespace VC }
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ string LabelPrefix = "PreconditionGeneratedEntry";
+ int k = 0;
- Block! originalEntryPoint = (!) impl.Blocks[0];
- Block! currentEntryPoint = (!) impl.Blocks[0];
- CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" preconditions
+ Block origStartBlock = impl.Blocks[0];
+ Block insertionPoint = new Block(
+ new Token(-17, -4), LabelPrefix + k, startCmds,
+ new GotoCmd(Token.NoToken, new StringSeq(origStartBlock.Label), new BlockSeq(origStartBlock)));
+ k++;
+ impl.Blocks[0] = insertionPoint; // make insertionPoint the start block
+ impl.Blocks.Add(origStartBlock); // and put the previous start block at the end of the list
// (free and checked) requires clauses
- for (int i = impl.Proc.Requires.Length-1; 0 <= i; i--){
-
- // need to process the preconditions from bottom up, because
- // for any that are BlockExprs, we need to thread them on
- // to the top of the implementation
-
- Requires req = impl.Proc.Requires[i];
- Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);
- BlockExpr be = req.Condition as BlockExpr;
- if (be != null){
- if (currentClump.Length > 0){
- AddAsPrefix(currentEntryPoint, currentClump);
- currentClump = new CmdSeq();
- }
- ThreadInBlockExpr(impl,currentEntryPoint, be,false,debugWriter);
- currentEntryPoint = (!)be.Blocks[0];
- }else{
- Cmd! c = new AssumeCmd(req.tok, e);
- currentClump.Add(c);
+ foreach (Requires! req in impl.Proc.Requires)
+ // invariant: insertionPoint.TransferCmd is "goto origStartBlock;", but origStartBlock.Predecessors has not yet been updated
+ {
+ Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
+ BlockExpr be = e as BlockExpr;
+ if (be == null) {
+ // This is the normal case, where the precondition is an ordinary expression
+ Cmd c = new AssumeCmd(req.tok, e);
+ insertionPoint.Cmds.Add(c);
if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ } else {
+ // This is a BlockExpr, so append all of its blocks (changing return expressions
+ // to assume statements), make the insertion-point block goto the head block of the
+ // BlockExpr, and create a new empty block as the current insertion point.
+ // Here goes: First, create the new block, which will become the new insertion
+ // point and which will serve as a target for the BlockExpr. Move the goto's from
+ // the current insertion point to this new block.
+ Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
+ k++;
+ // Second, append the BlockExpr blocks to the implementation's blocks
+ ThreadInBlockExpr(impl, nextIP, be, false, debugWriter);
+ // Third, make the old insertion-point block goto the entry block of the BlockExpr
+ Block beEntry = (!)be.Blocks[0];
+ insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));
+ beEntry.Predecessors.Add(insertionPoint);
+ // Fourth, update the insertion point
+ insertionPoint = nextIP;
}
-
}
+ origStartBlock.Predecessors.Add(insertionPoint);
- if (currentClump.Length > 0){
- AddAsPrefix(currentEntryPoint, currentClump);
- }
-
- if (currentEntryPoint != originalEntryPoint){
- string EntryLabel = "PreconditionGeneratedEntry";
- Block! newEntry = new Block(new Token(-17, -4),EntryLabel,new CmdSeq(),
- new GotoCmd(Token.NoToken,
- new StringSeq(currentEntryPoint.Label),
- new BlockSeq(currentEntryPoint)));
- currentEntryPoint.Predecessors.Add(newEntry);
- List<Block!> newBody = new List<Block!>();
- newBody.Add(newEntry);
- newBody.AddRange(impl.Blocks);
- impl.Blocks = newBody;
- }
-
if (debugWriter != null) { debugWriter.WriteLine(); }
-
- return;
}
/// <summary>
/// Modifies an implementation by inserting all postconditions
/// as assert statements at the end of the implementation
+ /// Returns the possibly-new unified exit block of the implementation
/// </summary>
/// <param name="impl"></param>
/// <param name="unifiedExitblock">The unified exit block that has
/// already been constructed for the implementation (and so
/// is already an element of impl.Blocks)
/// </param>
- protected static void InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)
+ protected static Block! InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)
requires impl.Proc != null;
+ requires unifiedExitBlock.TransferCmd is ReturnCmd;
+ ensures result.TransferCmd is ReturnCmd;
{
TokenTextWriter debugWriter = null;
if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
@@ -334,58 +333,49 @@ namespace VC debugWriter.WriteLine("Effective postcondition:");
}
- string ExitLabel = "ReallyLastGeneratedExit";
- Block! newExit = new Block(new Token(-17, -4),ExitLabel,new CmdSeq(),new ReturnCmd(Token.NoToken));
- impl.Blocks.Add(newExit);
- Block! currentEntryPoint = newExit;
- CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" postconditions
-
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ Block insertionPoint = unifiedExitBlock;
+ string LabelPrefix = "ReallyLastGeneratedExit";
+ int k = 0;
// (free and checked) ensures clauses
- for (int i = impl.Proc.Ensures.Length-1; 0 <= i; i--){
-
- // need to process the postconditions from bottom up, because
- // for any that are BlockExprs, we need to thread them on
- // to the top of the implementation
-
- Ensures ens = (impl.Proc).Ensures[i];
- if (!ens.Free) { // free ensures aren't needed for verifying the implementation
- Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);
+ foreach (Ensures! ens in impl.Proc.Ensures)
+ invariant insertionPoint.TransferCmd is ReturnCmd;
+ {
+ if (!ens.Free) { // skip free ensures clauses
+ Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
BlockExpr be = ens.Condition as BlockExpr;
- if (be != null){
- if (currentClump.Length > 0){
- AddAsPrefix(currentEntryPoint, currentClump);
- currentClump = new CmdSeq();
- }
- ThreadInBlockExpr(impl,currentEntryPoint,be,true,debugWriter);
- currentEntryPoint = (!)be.Blocks[0];
- }else{
- Ensures! ensCopy = (Ensures!) ens.Clone();
+ if (be == null) {
+ // This is the normal case, where the postcondition is an ordinary expression
+ Ensures ensCopy = (Ensures!) ens.Clone();
ensCopy.Condition = e;
- Cmd! c = new AssertEnsuresCmd(ensCopy);
- ((AssertEnsuresCmd) c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
- currentClump.Add(c);
+ AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy);
+ c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;
+ insertionPoint.Cmds.Add(c);
if (debugWriter != null) { c.Emit(debugWriter, 1); }
+ } else {
+ // This is a BlockExpr, so append all of its blocks (changing return expressions
+ // to assert statements), insert a goto to its head block from the current insertion
+ // point, and create a new empty block as the current insertion point.
+ // Here goes: First, create the new block, which will become the new insertion
+ // point and which will serve as a target for the BlockExpr. Steal the TransferCmd
+ // from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.
+ Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
+ k++;
+ // Second, append the BlockExpr blocks to the implementation's blocks
+ ThreadInBlockExpr(impl, nextIP, be, true, debugWriter);
+ // Third, make the old insertion-point block goto the entry block of the BlockExpr
+ Block beEntry = (!)be.Blocks[0];
+ insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));
+ beEntry.Predecessors.Add(insertionPoint);
+ // Fourth, update the insertion point
+ insertionPoint = nextIP;
}
}
-
- }
-
- if (currentClump.Length > 0){
- AddAsPrefix(currentEntryPoint, currentClump);
}
- GotoCmd gtc = new GotoCmd(Token.NoToken,
- new StringSeq(currentEntryPoint.Label),
- new BlockSeq(currentEntryPoint));
- gotoCmdOrigins[gtc] = unifiedExitBlock.TransferCmd;
- unifiedExitBlock.TransferCmd = gtc;
- currentEntryPoint.Predecessors.Add(unifiedExitBlock);
-
if (debugWriter != null) { debugWriter.WriteLine(); }
-
- return;
+ return insertionPoint;
}
@@ -558,6 +548,7 @@ namespace VC protected Block! GenerateUnifiedExit(Implementation! impl, Hashtable! gotoCmdOrigins)
+ ensures result.TransferCmd is ReturnCmd;
{
Block/*?*/ exitBlock = null;
#region Create a unified exit block, if there's more than one
@@ -659,7 +650,7 @@ namespace VC -1;
Variable v = new Incarnation(x,currentIncarnationNumber + 1);
variable2SequenceNumber[x] = currentIncarnationNumber + 1;
- Debug.Assert(current_impl != null, "The field current_impl wasn't set.");
+ assert current_impl != null; // otherwise, the field current_impl wasn't set
current_impl.LocVars.Add(v);
incarnationOriginMap.Add((Incarnation) v, a);
return v;
@@ -691,7 +682,7 @@ namespace VC Set /*Variable*/ fixUps = new Set /*Variable*/ ();
foreach (Block! pred in b.Predecessors)
{
- Debug.Assert(block2Incarnation.Contains(pred), "Passive Transformation found a block whose predecessors have not been processed yet.");
+ assert block2Incarnation.Contains(pred); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet
Hashtable /*Variable -> Expr*/ predMap = (Hashtable! /*Variable -> Expr*/) block2Incarnation[pred];
if (incarnationMap == null)
{
@@ -818,7 +809,7 @@ namespace VC }
}
IEnumerable! sortedNodes = dag.TopologicalSort();
- //Debug.Assert( sortedNodes != null, "Topological Sort returned null." );
+ // assume sortedNodes != null;
#endregion
// Create substitution for old expressions
@@ -835,7 +826,7 @@ namespace VC Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();
foreach (Block! b in sortedNodes )
{
- Debug.Assert( !block2Incarnation.Contains(b) );
+ assert !block2Incarnation.Contains(b);
Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);
#region Each block's map needs to be available to successor blocks
@@ -869,17 +860,10 @@ namespace VC #region assert/assume P |--> assert/assume P[x := in(x)], out := in
if ( c is PredicateCmd )
{
- Debug.Assert( c is AssertCmd || c is AssumeCmd, "Internal Error: Found a PredicateCmd h is not an assert or an assume." );
+ assert c is AssertCmd || c is AssumeCmd; // otherwise, unexpected PredicateCmd type
PredicateCmd! pc = (PredicateCmd) c.Clone();
- if(pc is AssumeCmd && pc.Expr is LoopPredicate // Check if the PredicateCmd is in the form of "assume J", with J loop invariant predicate
- && this.preHavocIncarnationMap != null) // Furthermore, the command just before was a (list of) havoc statements
- {
- LoopPredicate! lp = (LoopPredicate!) pc.Expr;
- lp.SetPreAndPostHavocIncarnationMaps(this.preHavocIncarnationMap, (Hashtable /*Variable -> Expr*/!) incarnationMap.Clone());
- }
-
Expr! copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
if (pc is AssertCmd) {
((AssertCmd) pc).OrigExpr = pc.Expr;
@@ -1086,16 +1070,21 @@ namespace VC protected void AddBlocksBetween(Implementation! impl)
{
- #region Introduce empty blocks before all blocks with more than one predecessor
+ #region Introduce empty blocks between join points and their multi-successor predecessors
List<Block!> tweens = new List<Block!>();
foreach ( Block b in impl.Blocks )
{
int nPreds = b.Predecessors.Length;
if ( nPreds > 1 )
{
+ // b is a join point (i.e., it has more than one predecessor)
for (int i = 0; i < nPreds; i++ )
{
- tweens.Add(CreateBlockBetween(i, b));
+ GotoCmd gotocmd = (GotoCmd!)((!)b.Predecessors[i]).TransferCmd;
+ if (gotocmd.labelNames != null && gotocmd.labelNames.Length > 1)
+ {
+ tweens.Add(CreateBlockBetween(i, b));
+ }
}
}
}
diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc index cdc6dde2..7f890826 100644 --- a/Source/VCGeneration/VC.ssc +++ b/Source/VCGeneration/VC.ssc @@ -1575,10 +1575,10 @@ namespace VC {
Block! pred = (!)header.Predecessors[predIndex];
- // Create a block between header and pred for the predicate commands if header has more than one successor
- // or if pred is a back edge node
- GotoCmd gotocmd = pred.TransferCmd as GotoCmd;
- if ((backEdgeNodes.ContainsKey(pred)) || (gotocmd != null && gotocmd.labelNames != null && gotocmd.labelNames.Length > 1))
+ // Create a block between header and pred for the predicate commands if pred has more than one successor
+ GotoCmd gotocmd = (GotoCmd!)pred.TransferCmd;
+ assert gotocmd.labelNames != null; // if "pred" is really a predecessor, it may be a GotoCmd with at least one label
+ if (gotocmd.labelNames.Length > 1)
{
Block! newBlock = CreateBlockBetween(predIndex, header);
impl.Blocks.Add(newBlock);
@@ -1691,7 +1691,7 @@ namespace VC protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)
{
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
- Block/*?*/ exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
+ Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
@@ -1722,16 +1722,11 @@ namespace VC }
}
- InjectPreconditions(impl);
- //cc.AddRange(GetPre(impl));
+ // add cc and the preconditions to new blocks preceding impl.Blocks[0]
+ InjectPreconditions(impl, cc);
- Block! entryBlock = (!) impl.Blocks[0];
- cc.AddRange(entryBlock.Cmds);
- entryBlock.Cmds = cc;
-
- InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
- //CmdSeq! post = GetPost(impl);
- //exitBlock.Cmds.AddRange(post);
+ // append postconditions, starting in exitBlock and continuing into other blocks, if needed
+ exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
}
#endregion
@@ -1748,21 +1743,21 @@ namespace VC #region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
- Console.WriteLine("after adding empty blocks before all blocks with more than one predecessor");
+ Console.WriteLine("after adding empty blocks as needed to catch join assumptions");
EmitImpl(impl, true);
}
#endregion
if (CommandLineOptions.Clo.LiveVariableAnalysis) {
- Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
- }
-
+ Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
+ }
+
Convert2PassiveCmd(impl);
if (CommandLineOptions.Clo.LiveVariableAnalysis) {
- Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
- }
-
+ Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
+ }
+
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
@@ -2867,49 +2862,110 @@ namespace VC static BlockSeq! RemoveEmptyBlocks(Block! b)
{
assert b.TraversingStatus == Block.VisitState.ToVisit;
- BlockSeq retVal = removeEmptyBlocksWorker(b, true);
+ Block renameInfo;
+ BlockSeq retVal = removeEmptyBlocksWorker(b, true, out renameInfo);
+ if (renameInfo != null && !b.tok.IsValid) {
+ bool onlyAssumes = true;
+ foreach (Cmd c in b.Cmds) {
+ if (!(c is AssumeCmd)) {
+ onlyAssumes = false;
+ break;
+ }
+ }
+ if (onlyAssumes) {
+ b.tok = renameInfo.tok;
+ b.Label = renameInfo.Label;
+ }
+ }
return retVal;
}
- private static BlockSeq! removeEmptyBlocksWorker(Block! b, bool startNode)
+ /// <summary>
+ /// For every not-yet-visited block n reachable from b, change n's successors to skip empty nodes.
+ /// Return the *set* of blocks reachable from b without passing through a nonempty block.
+ /// The target of any backedge is counted as a nonempty block.
+ /// If renameInfoForStartBlock is non-null, it denotes an empty block with location information, and that
+ /// information would be appropriate to display
+ /// </summary>
+ private static BlockSeq! removeEmptyBlocksWorker(Block! b, bool startNode, out Block renameInfoForStartBlock)
+ ensures renameInfoForStartBlock != null ==> renameInfoForStartBlock.tok.IsValid;
+ // ensures: b in result ==> renameInfoForStartBlock == null;
{
+ renameInfoForStartBlock = null;
BlockSeq bs = new BlockSeq();
GotoCmd gtc = b.TransferCmd as GotoCmd;
// b has no successors
if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Length == 0)
- {
+ {
if (b.Cmds.Length != 0){ // only empty blocks are removed...
bs.Add(b);
+ } else if (b.tok.IsValid) {
+ renameInfoForStartBlock = b;
}
return bs;
}
- else if(b.TraversingStatus == Block.VisitState.ToVisit) // if b has some successors and we have not seen it so far...
+ else if (b.TraversingStatus == Block.VisitState.ToVisit) // if b has some successors and we have not seen it so far...
{
b.TraversingStatus = Block.VisitState.BeingVisited;
+ // Before recursing down to successors, make a sobering observation:
+ // If b has no commands and is not the start node, then it will see
+ // extinction (because it will not be included in the "return setOfSuccessors"
+ // statement below). In that case, if b has a location, then the location
+ // information would be lost. Hence, make an attempt to save the location
+ // by pushing the location onto b's successor. This can be done if (0) b has
+ // exactly one successor, (1) that successor has no location of its own, and
+ // (2) that successor has no other predecessors.
+ if (b.Cmds.Length == 0 && !startNode) {
+ // b is about to become extinct; try to save its name and location, if possible
+ if (b.tok.IsValid && gtc.labelTargets.Length == 1) {
+ Block succ = (!)gtc.labelTargets[0];
+ if (!succ.tok.IsValid && succ.Predecessors.Length == 1) {
+ succ.tok = b.tok;
+ succ.Label = b.Label;
+ }
+ }
+ }
+
// recursively call this method on each successor
// merge result into a *set* of blocks
Dictionary<Block,bool> mergedSuccessors = new Dictionary<Block,bool>();
+ int m = 0; // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null
foreach (Block! dest in gtc.labelTargets){
- BlockSeq! ys = removeEmptyBlocksWorker(dest, false);
+ Block renameInfo;
+ BlockSeq! ys = removeEmptyBlocksWorker(dest, false, out renameInfo);
+ if (m == 0) {
+ renameInfoForStartBlock = renameInfo;
+ } else if (renameInfoForStartBlock != renameInfo) {
+ renameInfoForStartBlock = null;
+ }
foreach (Block successor in ys){
if (!mergedSuccessors.ContainsKey(successor))
mergedSuccessors.Add(successor,true);
}
+ m++;
}
b.TraversingStatus = Block.VisitState.AlreadyVisited;
BlockSeq setOfSuccessors = new BlockSeq();
foreach (Block d in mergedSuccessors.Keys)
setOfSuccessors.Add(d);
- if (b.Cmds.Length == 0 && !startNode)
+ if (b.Cmds.Length == 0 && !startNode) {
+ // b is about to become extinct
+ if (b.tok.IsValid) {
+ renameInfoForStartBlock = b;
+ }
return setOfSuccessors;
+ }
// otherwise, update the list of successors of b to be the blocks in setOfSuccessors
gtc.labelTargets = setOfSuccessors;
gtc.labelNames = new StringSeq();
foreach (Block! d in setOfSuccessors)
gtc.labelNames.Add(d.Label);
+ if (!startNode) {
+ renameInfoForStartBlock = null;
+ }
return new BlockSeq(b);
}
else // b has some successors, but we are already visiting it, or we have already visited it...
diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index f1487fad..f3720e7f 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -634,13 +634,13 @@ namespace VC out Dictionary<Block!, Block!> copiedblocks)
{
Block! start = impl.Blocks[0];
- Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();
- Set/*Block*/! beingVisited = new Set/*Block*/();
- GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);
+ Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();
+ Set/*Block*/! beingVisited = new Set/*Block*/();
+ GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);
DCProgramTransformer pt = new DCProgramTransformer(checkableBlocks);
- pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");
- pt.Blocks.Reverse();
+ pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");
+ pt.Blocks.Reverse();
copiedblocks = pt.m_copyMap;
return pt.Blocks;
}
@@ -655,262 +655,262 @@ namespace VC #region Loop Unrolling Methods
- private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
- {
- Block newb;
- if (visited.TryGetValue(node, out newb))
- {
- assert newb!=null;
- return newb;
- } else
- {
- if (node.IsCutPoint)
- {
- // compute the loop body and the blocks leaving the loop
-
- List<GraphNode!>! loopNodes = new List<GraphNode!>();
- GatherLoopBodyNodes(node, node, loopNodes);
+ private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
+ {
+ Block newb;
+ if (visited.TryGetValue(node, out newb))
+ {
+ assert newb!=null;
+ return newb;
+ } else
+ {
+ if (node.IsCutPoint)
+ {
+ // compute the loop body and the blocks leaving the loop
+
+ List<GraphNode!>! loopNodes = new List<GraphNode!>();
+ GatherLoopBodyNodes(node, node, loopNodes);
- List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);
-
- // Continue Unrolling after the current loop
- Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();
- foreach (GraphNode! g in exitNodes)
- {
- Block b = LoopUnrolling(g, visited, unrollable, prefix);
- _visited.Add(g,b);
- }
- newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);
- visited.Add(node,newb);
- } else
- {
- BlockSeq! newSuccs = new BlockSeq();
- foreach(GraphNode! g in node.Succecessors)
- {
- newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
- }
- newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);
+
+ // Continue Unrolling after the current loop
+ Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();
+ foreach (GraphNode! g in exitNodes)
+ {
+ Block b = LoopUnrolling(g, visited, unrollable, prefix);
+ _visited.Add(g,b);
+ }
+ newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);
+ visited.Add(node,newb);
+ } else
+ {
+ BlockSeq! newSuccs = new BlockSeq();
+ foreach(GraphNode! g in node.Succecessors)
+ {
+ newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
+ }
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
Block b;
- if (m_copyMap.TryGetValue(node.Block, out b) ) {
- assert b!=null;
- m_copyMap.Add(newb, b);
- } else {
- m_copyMap.Add(newb, node.Block);
- }
-
-
- assert newb!=null; assert newb.TransferCmd!=null;
- if (newSuccs.Length == 0)
- newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
- else
- newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
-
- visited.Add(node, newb);
- Blocks.Add(newb);
- if (unrollable)
- {
- m_checkableBlocks.Add(newb);
- }
- }
- }
- assert newb!=null;
- //newb.checkable = unrollable;
- return newb;
- }
+ if (m_copyMap.TryGetValue(node.Block, out b) ) {
+ assert b!=null;
+ m_copyMap.Add(newb, b);
+ } else {
+ m_copyMap.Add(newb, node.Block);
+ }
+
+
+ assert newb!=null; assert newb.TransferCmd!=null;
+ if (newSuccs.Length == 0)
+ newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
+ else
+ newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
+
+ visited.Add(node, newb);
+ Blocks.Add(newb);
+ if (unrollable)
+ {
+ m_checkableBlocks.Add(newb);
+ }
+ }
+ }
+ assert newb!=null;
+ //newb.checkable = unrollable;
+ return newb;
+ }
- private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited,
- List<GraphNode!>! loopNodes, bool unrollable, String! prefix)
- {
- if (unrollable)
- {
- Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);
- Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);
- Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);
+ private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited,
+ List<GraphNode!>! loopNodes, bool unrollable, String! prefix)
+ {
+ if (unrollable)
+ {
+ Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);
+ Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);
+ Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);
- Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");
-
- Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");
- AddHavocCmd(last,loopNodes);
-
- // You might use true for the unrollable flag as well.
- Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");
- AddHavocCmd(arb,loopNodes);
-
-
- BlockSeq! succ = new BlockSeq();
- succ.Add(last); succ.Add(arb);
- assert arb.TransferCmd!=null;
- Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));
- Blocks.Add(tmp);
- m_checkableBlocks.Add(tmp);
+ Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");
+
+ Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");
+ AddHavocCmd(last,loopNodes);
+
+ // You might use true for the unrollable flag as well.
+ Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");
+ AddHavocCmd(arb,loopNodes);
+
+
+ BlockSeq! succ = new BlockSeq();
+ succ.Add(last); succ.Add(arb);
+ assert arb.TransferCmd!=null;
+ Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));
+ Blocks.Add(tmp);
+ m_checkableBlocks.Add(tmp);
// check if arb is already a copy of something else
// if not then write to m_copyMap that tmp is a copy
// of arb
- Block b = null;
- if (m_copyMap.TryGetValue(arb,out b) ) {
- assert b!=null;
- m_copyMap.Add(tmp, b);
- } else {
- m_copyMap.Add(tmp, arb);
- }
+ Block b = null;
+ if (m_copyMap.TryGetValue(arb,out b) ) {
+ assert b!=null;
+ m_copyMap.Add(tmp, b);
+ } else {
+ m_copyMap.Add(tmp, arb);
+ }
- Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");
-
- return first;
+ Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");
+
+ return first;
- } else
- {
- Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);
- Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");
- Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);
- AddHavocCmd(ret, loopNodes);
- return ret;
- }
- }
-
- private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
- {
- visited.Add(node, nextIter);
- Block newb,b;
- BlockSeq! newSuccs = new BlockSeq();
- foreach(GraphNode! g in node.Succecessors)
- {
- newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
- }
- newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
- if (m_copyMap.TryGetValue(node.Block, out b) ) {
- assert b!=null;
- m_copyMap.Add(newb, b);
- } else {
- m_copyMap.Add(newb, node.Block);
- }
-
- assert newb!=null; assert newb.TransferCmd!=null;
- if (newSuccs.Length == 0)
- newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
- else
- newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
-
- Blocks.Add(newb);
- if (unrollable) m_checkableBlocks.Add(newb);
- return newb;
- }
+ } else
+ {
+ Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);
+ Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");
+ Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);
+ AddHavocCmd(ret, loopNodes);
+ return ret;
+ }
+ }
+
+ private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)
+ {
+ visited.Add(node, nextIter);
+ Block newb,b;
+ BlockSeq! newSuccs = new BlockSeq();
+ foreach(GraphNode! g in node.Succecessors)
+ {
+ newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );
+ }
+ newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);
+ if (m_copyMap.TryGetValue(node.Block, out b) ) {
+ assert b!=null;
+ m_copyMap.Add(newb, b);
+ } else {
+ m_copyMap.Add(newb, node.Block);
+ }
+
+ assert newb!=null; assert newb.TransferCmd!=null;
+ if (newSuccs.Length == 0)
+ newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
+ else
+ newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
+
+ Blocks.Add(newb);
+ if (unrollable) m_checkableBlocks.Add(newb);
+ return newb;
+ }
- private Block! AbstractIteration(GraphNode! node, String! prefix)
- {
- CmdSeq body = new CmdSeq();
- foreach (Cmd! c in node.Body)
- {
- if (c is PredicateCmd || c is CommentCmd)
- body.Add(c );
- else
- break;
- }
- body.Add(new AssumeCmd(node.Block.tok, Expr.False) );
- TransferCmd! tcmd = new ReturnCmd(node.Block.tok);
- Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);
- Blocks.Add(b);
+ private Block! AbstractIteration(GraphNode! node, String! prefix)
+ {
+ CmdSeq body = new CmdSeq();
+ foreach (Cmd! c in node.Body)
+ {
+ if (c is PredicateCmd || c is CommentCmd)
+ body.Add(c );
+ else
+ break;
+ }
+ body.Add(new AssumeCmd(node.Block.tok, Expr.False) );
+ TransferCmd! tcmd = new ReturnCmd(node.Block.tok);
+ Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);
+ Blocks.Add(b);
Block tmp;
- if (m_copyMap.TryGetValue(node.Block, out tmp) ) {
- assert tmp!=null;
- m_copyMap.Add(b, tmp);
- } else {
- m_copyMap.Add(b, node.Block);
- }
-
- return b;
- }
+ if (m_copyMap.TryGetValue(node.Block, out tmp) ) {
+ assert tmp!=null;
+ m_copyMap.Add(b, tmp);
+ } else {
+ m_copyMap.Add(b, node.Block);
+ }
+
+ return b;
+ }
- private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes,
- Dictionary<GraphNode, Block!>! visited, String! prefix)
- {
- BlockSeq! newSucc = new BlockSeq();
- Block! orig = cutPoint.Block;
-
- // detect the block after the loop
- // FixMe: What happens when using break commands?
- foreach (GraphNode! g in cutPoint.Succecessors)
- {
- if (!loopNodes.Contains(g))
- {
- Block b;
- if (visited.TryGetValue(g,out b) )
- newSucc.Add(b);
- }
- }
- TransferCmd tcmd;
- assert orig.TransferCmd!=null;
- if (newSucc.Length==0)
- tcmd = new ReturnCmd(orig.TransferCmd.tok);
- else
- tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);
- // FixMe: Genertate IToken for counterexample creation
- Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);
- Blocks.Add(newb);
- m_checkableBlocks.Add(newb);
- return newb;
- }
+ private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes,
+ Dictionary<GraphNode, Block!>! visited, String! prefix)
+ {
+ BlockSeq! newSucc = new BlockSeq();
+ Block! orig = cutPoint.Block;
+
+ // detect the block after the loop
+ // FixMe: What happens when using break commands?
+ foreach (GraphNode! g in cutPoint.Succecessors)
+ {
+ if (!loopNodes.Contains(g))
+ {
+ Block b;
+ if (visited.TryGetValue(g,out b) )
+ newSucc.Add(b);
+ }
+ }
+ TransferCmd tcmd;
+ assert orig.TransferCmd!=null;
+ if (newSucc.Length==0)
+ tcmd = new ReturnCmd(orig.TransferCmd.tok);
+ else
+ tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);
+ // FixMe: Genertate IToken for counterexample creation
+ Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);
+ Blocks.Add(newb);
+ m_checkableBlocks.Add(newb);
+ return newb;
+ }
- private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)
- {
- loopNodes.Add(current);
- if (false) System.Diagnostics.Debugger.Break();
- foreach (GraphNode! g in current.Predecessors)
- {
- if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;
- GatherLoopBodyNodes(g, cutPoint, loopNodes);
- }
- }
-
- private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)
- {
- List<GraphNode!>! exitnodes = new List<GraphNode!>();
-
- foreach (GraphNode! g in loopNodes)
- {
- foreach (GraphNode! s in g.Succecessors)
- {
- if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);
- }
- }
- return exitnodes;
- }
-
- private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)
- {
- List<Block!>! loopBlocks = new List<Block!>();
- foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);
- HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);
- CmdSeq! body = new CmdSeq();
- body.Add(hcmd);
- body.AddRange(b.Cmds);
- b.Cmds = body;
- }
+ private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)
+ {
+ loopNodes.Add(current);
+ if (false) System.Diagnostics.Debugger.Break();
+ foreach (GraphNode! g in current.Predecessors)
+ {
+ if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;
+ GatherLoopBodyNodes(g, cutPoint, loopNodes);
+ }
+ }
+
+ private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)
+ {
+ List<GraphNode!>! exitnodes = new List<GraphNode!>();
+
+ foreach (GraphNode! g in loopNodes)
+ {
+ foreach (GraphNode! s in g.Succecessors)
+ {
+ if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);
+ }
+ }
+ return exitnodes;
+ }
+
+ private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)
+ {
+ List<Block!>! loopBlocks = new List<Block!>();
+ foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);
+ HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);
+ CmdSeq! body = new CmdSeq();
+ body.Add(hcmd);
+ body.AddRange(b.Cmds);
+ b.Cmds = body;
+ }
- private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)
- {
- VariableSeq varsToHavoc = new VariableSeq();
- foreach ( Block! b in bl )
- {
- foreach ( Cmd! c in b.Cmds )
- {
- c.AddAssignedVariables(varsToHavoc);
- }
- }
- IdentifierExprSeq havocExprs = new IdentifierExprSeq();
- foreach ( Variable! v in varsToHavoc )
- {
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- if(!havocExprs.Has(ie))
- havocExprs.Add(ie);
- }
- // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
- // the source location for this later on
- return new HavocCmd(tok,havocExprs);
- }
-
+ private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)
+ {
+ VariableSeq varsToHavoc = new VariableSeq();
+ foreach ( Block! b in bl )
+ {
+ foreach ( Cmd! c in b.Cmds )
+ {
+ c.AddAssignedVariables(varsToHavoc);
+ }
+ }
+ IdentifierExprSeq havocExprs = new IdentifierExprSeq();
+ foreach ( Variable! v in varsToHavoc )
+ {
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ if(!havocExprs.Has(ie))
+ havocExprs.Add(ie);
+ }
+ // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
+ // the source location for this later on
+ return new HavocCmd(tok,havocExprs);
+ }
+
#endregion
@@ -1009,7 +1009,7 @@ namespace VC assume gcmd.labelTargets != null;
foreach (Block! succ in gcmd.labelTargets)
{
- g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );
+ g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );
}
}
beingVisited.Remove(b);
@@ -1020,148 +1020,135 @@ namespace VC }
}
- #endregion
+ #endregion
#endregion
#region Program Passification
private void GenerateReachVars(Implementation! impl)
{
- Hashtable gotoCmdOrigins = new Hashtable();
- Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
- AddBlocksBetween(impl);
-
+ Hashtable gotoCmdOrigins = new Hashtable();
+ Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
+ AddBlocksBetween(impl);
+
#region Insert pre- and post-conditions and where clauses as assume and assert statements
{
- CmdSeq cc = new CmdSeq();
- // where clauses of global variables
- foreach (Declaration d in program.TopLevelDeclarations) {
- GlobalVariable gvar = d as GlobalVariable;
- if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
- Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
- cc.Add(c);
+ CmdSeq cc = new CmdSeq();
+ // where clauses of global variables
+ foreach (Declaration d in program.TopLevelDeclarations) {
+ GlobalVariable gvar = d as GlobalVariable;
+ if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
+ Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
+ cc.Add(c);
+ }
}
- }
- // where clauses of in- and out-parameters
- cc.AddRange( GetParamWhereClauses(impl));
- // where clauses of local variables
- foreach (Variable! lvar in impl.LocVars) {
- if (lvar.TypedIdent.WhereExpr != null) {
- Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);
- cc.Add(c);
+ // where clauses of in- and out-parameters
+ cc.AddRange( GetParamWhereClauses(impl));
+ // where clauses of local variables
+ foreach (Variable! lvar in impl.LocVars) {
+ if (lvar.TypedIdent.WhereExpr != null) {
+ Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);
+ cc.Add(c);
+ }
}
- }
- InjectPreconditions(impl);
- //cc.AddRange(GetPre(impl));
+ // add cc and the preconditions to new blocks preceding impl.Blocks[0]
+ InjectPreconditions(impl, cc);
- Block! entryBlock = (!) impl.Blocks[0];
- cc.AddRange(entryBlock.Cmds);
- entryBlock.Cmds = cc;
-
- InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
- //CmdSeq! post = GetPost(impl);
- //exitBlock.Cmds.AddRange(post);
- }
- // Check If a new Unified Exit has been generated
- GotoCmd gc = exitBlock.TransferCmd as GotoCmd;
- if (gc!=null) {
- assert gc.labelTargets !=null;
- assert gc.labelTargets.Length==1;
- assert gc.labelTargets[0]!=null;
- exitBlock = (!)gc.labelTargets[0];
+ // append postconditions, starting in exitBlock and continuing into other blocks, if needed
+ exitBlock = InjectPostConditions(impl,exitBlock,gotoCmdOrigins);
}
- #endregion
- GenerateReachabilityPredicates(impl, exitBlock);
+ #endregion
+ GenerateReachabilityPredicates(impl, exitBlock);
}
private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl)
- {
- current_impl = impl;
- Convert2PassiveCmd(impl);
- impl = current_impl;
- return new Hashtable();
- }
+ {
+ current_impl = impl;
+ Convert2PassiveCmd(impl);
+ impl = current_impl;
+ return new Hashtable();
+ }
- /// <summary>
- /// Add additional variable to allow checking as described in the paper
- /// "It's doomed; we can prove it"
- /// </summary>
- private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)
- {
- ExprSeq! es = new ExprSeq();
- Cmd eblockcond = null;
-
- foreach (Block! b in impl.Blocks)
- {
- //if (b.Predecessors.Length==0) continue;
- //if (b.Cmds.Length == 0 ) continue;
+ /// <summary>
+ /// Add additional variable to allow checking as described in the paper
+ /// "It's doomed; we can prove it"
+ /// </summary>
+ private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)
+ {
+ ExprSeq! es = new ExprSeq();
+ Cmd eblockcond = null;
+
+ foreach (Block! b in impl.Blocks)
+ {
+ //if (b.Predecessors.Length==0) continue;
+ //if (b.Cmds.Length == 0 ) continue;
- Variable v_ = new LocalVariable(Token.NoToken,
- new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );
-
- impl.LocVars.Add(v_);
-
- m_BlockReachabilityMap[b] = v_;
-
- IdentifierExpr! lhs = new IdentifierExpr(b.tok, v_);
-
- es.Add( new IdentifierExpr(b.tok, v_) );
-
- List<AssignLhs!>! lhsl = new List<AssignLhs!>();
- lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );
- List<Expr!>! rhsl = new List<Expr!>();
- rhsl.Add(Expr.True);
-
- if (b!=exitBlock)
- {
- CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
- cs.AddRange(b.Cmds);
- b.Cmds = cs;
- } else
- {
- eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);
- }
-
- //checkBlocks.Add(new CheckableBlock(v_,b));
- }
- if (es.Length==0) return;
+ Variable v_ = new LocalVariable(Token.NoToken,
+ new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );
+
+ impl.LocVars.Add(v_);
+
+ m_BlockReachabilityMap[b] = v_;
+
+ IdentifierExpr! lhs = new IdentifierExpr(b.tok, v_);
+
+ es.Add( new IdentifierExpr(b.tok, v_) );
+
+ List<AssignLhs!>! lhsl = new List<AssignLhs!>();
+ lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );
+ List<Expr!>! rhsl = new List<Expr!>();
+ rhsl.Add(Expr.True);
+
+ if (b!=exitBlock)
+ {
+ CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
+ cs.AddRange(b.Cmds);
+ b.Cmds = cs;
+ } else
+ {
+ eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);
+ }
+
+ //checkBlocks.Add(new CheckableBlock(v_,b));
+ }
+ if (es.Length==0) return;
- Expr aexp = null;
+ Expr aexp = null;
- if (es.Length==1)
- {
- aexp = es[0];
- } else if (es.Length==2)
- {
- aexp = Expr.Binary(Token.NoToken,
- BinaryOperator.Opcode.And,
- (!)es[0],
- (!)es[1]);
- } else
- {
- aexp = Expr.True;
- foreach (Expr e_ in es)
- {
- aexp = Expr.Binary(Token.NoToken,
- BinaryOperator.Opcode.And,
- (!)e_, aexp);
- }
- }
- assert (aexp!=null);
- assert (eblockcond!=null);
-
- AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);
-
- assert(exitBlock!=null);
+ if (es.Length==1)
+ {
+ aexp = es[0];
+ } else if (es.Length==2)
+ {
+ aexp = Expr.Binary(Token.NoToken,
+ BinaryOperator.Opcode.And,
+ (!)es[0],
+ (!)es[1]);
+ } else
+ {
+ aexp = Expr.True;
+ foreach (Expr e_ in es)
+ {
+ aexp = Expr.Binary(Token.NoToken,
+ BinaryOperator.Opcode.And,
+ (!)e_, aexp);
+ }
+ }
+ assert (aexp!=null);
+ assert (eblockcond!=null);
+
+ AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);
+
+ assert(exitBlock!=null);
- CmdSeq cseq = new CmdSeq(eblockcond);
- cseq.AddRange(exitBlock.Cmds);
- cseq.Add(ac);
-
- exitBlock.Cmds = cseq;
- }
+ CmdSeq cseq = new CmdSeq(eblockcond);
+ cseq.AddRange(exitBlock.Cmds);
+ cseq.Add(ac);
+
+ exitBlock.Cmds = cseq;
+ }
#endregion
|