summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-02-20 09:43:34 +0000
committerGravatar rustanleino <unknown>2010-02-20 09:43:34 +0000
commitbf3c95c9b96553159b0d121881179feff7853e5d (patch)
tree8a7dd8a411fbc3954fb0891638c184f899f80902
parente516262abbc3276777a222481757cd74dab1d497 (diff)
Boogie:
* Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
Diffstat
-rw-r--r--Source/Core/Absy.ssc145
-rw-r--r--Source/Core/AbsyCmd.ssc2
-rw-r--r--Source/Core/AbsyExpr.ssc229
-rw-r--r--Source/Core/CommandLineOptions.ssc137
-rw-r--r--Source/Core/DeadVarElim.ssc4
-rw-r--r--Source/Core/StandardVisitor.ssc8
-rw-r--r--Source/VCExpr/Boogie2VCExpr.ssc9
-rw-r--r--Source/VCGeneration/ConditionGeneration.ssc191
-rw-r--r--Source/VCGeneration/VC.ssc110
-rw-r--r--Source/VCGeneration/VCDoomed.ssc719
-rw-r--r--Test/aitest0/runtest.bat2
-rw-r--r--Test/aitest1/runtest.bat2
-rw-r--r--Test/aitest9/answer3
-rw-r--r--Test/dafny0/Answer3
-rw-r--r--Test/inline/Answer16
-rw-r--r--Test/inline/runtest.bat7
-rw-r--r--Test/livevars/Answer15
-rw-r--r--Test/smoke/Answer4
-rw-r--r--Test/test2/Answer20
-rw-r--r--Test/test2/ContractEvaluationOrder.bpl34
-rw-r--r--Test/test2/Structured.bpl2
-rw-r--r--Test/test2/runtest.bat2
22 files changed, 723 insertions, 941 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
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index 15f36ab0..a4c12d8d 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -3,4 +3,4 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-%BGEXE% %* -infer:c -printInstrumented -noVerify constants.bpl
+%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl
diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat
index f2a4d3e5..3b2c382c 100644
--- a/Test/aitest1/runtest.bat
+++ b/Test/aitest1/runtest.bat
@@ -7,7 +7,7 @@ for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl
Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl
Linear7.bpl Linear8.bpl Linear9.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% %* -infer:p -printInstrumented -noVerify %%f
+ %BGEXE% %* -infer:p -instrumentInfer:e -printInstrumented -noVerify %%f
)
for %%f in (Bound.bpl) do (
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
index d6bba688..27e18ca4 100644
--- a/Test/aitest9/answer
+++ b/Test/aitest9/answer
@@ -13,11 +13,8 @@ TestIntervals.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
TestIntervals.bpl(5,5): anon0
TestIntervals.bpl(6,3): anon9_LoopHead
- TestIntervals.bpl(6,3): anon9_LoopDone
TestIntervals.bpl(12,14): anon10_Then
- TestIntervals.bpl(13,3): anon4
TestIntervals.bpl(13,14): anon11_Then
- TestIntervals.bpl(14,3): anon6
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 107cab0b..540bcb4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -87,17 +87,14 @@ Execution trace:
(0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
- (0,0): anon0
(0,0): anon10_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
- (0,0): anon0
(0,0): anon10_Else
(0,0): anon3
(0,0): anon11_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
- (0,0): anon0
(0,0): anon10_Then
(0,0): anon3
(0,0): anon11_Then
diff --git a/Test/inline/Answer b/Test/inline/Answer
index 934b45ba..12cb5960 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1443,13 +1443,8 @@ Boogie program verifier finished with 5 verified, 0 errors
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
test5.bpl(34,10): anon0
- test5.bpl(25,23): inline$P$0$Entry
test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(25,23): inline$P$0$Return
- test5.bpl(34,10): anon0$1
- test5.bpl(25,23): inline$P$1$Entry
test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(25,23): inline$P$1$Return
test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
@@ -1477,6 +1472,17 @@ Boogie program verifier finished with 1 verified, 1 error
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Elevator.bpl(15,3): anon0
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(24,7): anon13_Then$1
+
+Boogie program verifier finished with 1 verified, 1 error
+-------------------- Elevator.bpl with empty blocks --------------------
+Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Elevator.bpl(15,3): anon0
Elevator.bpl(68,23): inline$Initialize$0$Entry
Elevator.bpl(71,13): inline$Initialize$0$anon0
Elevator.bpl(68,23): inline$Initialize$0$Return
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 335c857d..179509f8 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -18,6 +18,13 @@ for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
%BGEXE% %* %%f
)
+REM Peephole optimizations are so good that Elevator seems worthwhile
+REM to include twice among these inline tests
+for %%f in (Elevator.bpl) do (
+ echo -------------------- %%f with empty blocks --------------------
+ %BGEXE% /removeEmptyBlocks:0 %* %%f
+)
+
echo -------------------- expansion2.bpl --------------------
%BGEXE% %* /proverLog:expansion2.sx expansion2.bpl
%SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx
diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index aaaee494..1a0327f6 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -51,6 +51,7 @@ Execution trace:
bla1.bpl(1654,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1
+ bla1.bpl(1676,3): inline$storm_IoCompleteRequest$0$label_1#1
bla1.bpl(1734,3): anon14_Then#1
bla1.bpl(1739,3): anon7#1
bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1
@@ -144,6 +145,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(1872,3): inline$storm_KeAcquireSpinLock$0$anon7#2
daytona_bug2_ioctl_example_2.bpl(1883,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
daytona_bug2_ioctl_example_2.bpl(1888,3): inline$storm_KeAcquireSpinLock$0$anon9#2
+ daytona_bug2_ioctl_example_2.bpl(1892,3): inline$storm_KeAcquireSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(1909,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
daytona_bug2_ioctl_example_2.bpl(1920,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
@@ -155,6 +157,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2039,3): inline$storm_IoSetCancelRoutine$0$anon8#2
daytona_bug2_ioctl_example_2.bpl(2050,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2055,3): inline$storm_IoSetCancelRoutine$0$anon10#2
+ daytona_bug2_ioctl_example_2.bpl(2062,3): inline$storm_IoSetCancelRoutine$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2
daytona_bug2_ioctl_example_2.bpl(2075,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
daytona_bug2_ioctl_example_2.bpl(2200,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
@@ -170,6 +173,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2337,3): inline$storm_IoSetCancelRoutine$1$anon8#2
daytona_bug2_ioctl_example_2.bpl(2348,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
daytona_bug2_ioctl_example_2.bpl(2353,3): inline$storm_IoSetCancelRoutine$1$anon10#2
+ daytona_bug2_ioctl_example_2.bpl(2361,3): inline$storm_IoSetCancelRoutine$1$label_1#2
daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2
daytona_bug2_ioctl_example_2.bpl(2375,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
daytona_bug2_ioctl_example_2.bpl(2385,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
@@ -185,6 +189,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2599,3): inline$storm_KeReleaseSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(2610,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(2615,3): inline$storm_KeReleaseSpinLock$0$anon7#2
+ daytona_bug2_ioctl_example_2.bpl(2619,3): inline$storm_KeReleaseSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
daytona_bug2_ioctl_example_2.bpl(2858,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51#2
@@ -194,10 +199,12 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(2951,3): inline$storm_IoCompleteRequest$2$anon6_Else#2
daytona_bug2_ioctl_example_2.bpl(2959,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
daytona_bug2_ioctl_example_2.bpl(2969,3): inline$storm_IoCompleteRequest$2$anon2#2
+ daytona_bug2_ioctl_example_2.bpl(2973,3): inline$storm_IoCompleteRequest$2$label_1#2
daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#2
daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
daytona_bug2_ioctl_example_2.bpl(3000,3): inline$I8xCompleteSysButtonIrp$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
+ daytona_bug2_ioctl_example_2.bpl(3013,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2
daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3169,3): inline$I8xKeyboardGetSysButtonEvent$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2
@@ -222,6 +229,7 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(3931,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3942,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(3947,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
+ daytona_bug2_ioctl_example_2.bpl(3951,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2
daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2
daytona_bug2_ioctl_example_2.bpl(3964,3): inline$storm_IoCancelIrp$0$anon30_Else#2
daytona_bug2_ioctl_example_2.bpl(3982,3): inline$storm_IoCancelIrp$0$label_16_true#2
@@ -293,6 +301,7 @@ Execution trace:
stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1
stack_overflow.bpl(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
+ stack_overflow.bpl(78233,3): inline$storm_IoSetCompletionRoutine$0$label_1#1
stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1
stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
@@ -330,11 +339,13 @@ Execution trace:
stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
stack_overflow.bpl(87671,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
stack_overflow.bpl(87685,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
+ stack_overflow.bpl(87692,3): inline$BDLDevicePowerIoCompletion$3$label_83#1
stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
stack_overflow.bpl(87702,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1
stack_overflow.bpl(87713,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1
stack_overflow.bpl(87738,3): inline$storm_IoCompleteRequest$7$label_6_false#1
stack_overflow.bpl(87777,3): inline$storm_IoCompleteRequest$7$label_7#1
+ stack_overflow.bpl(87782,3): inline$storm_IoCompleteRequest$7$label_1#1
stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#1
stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
@@ -344,13 +355,16 @@ Execution trace:
stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
stack_overflow.bpl(87953,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
stack_overflow.bpl(87967,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
+ stack_overflow.bpl(87974,3): inline$BDLDevicePowerIoCompletion$3$label_122#1
stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1
stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1
stack_overflow.bpl(88146,3): inline$CallCompletionRoutine$3$label_20_icall_return#1
stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1
+ stack_overflow.bpl(88169,3): inline$CallCompletionRoutine$3$label_1#1
stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1
stack_overflow.bpl(88190,3): inline$storm_IoCallDriver$1$anon15_Else#1
stack_overflow.bpl(88218,3): inline$storm_IoCallDriver$1$label_36#1
+ stack_overflow.bpl(88222,3): inline$storm_IoCallDriver$1$label_1#1
stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#1
stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1
stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1
@@ -373,6 +387,7 @@ Execution trace:
stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1
stack_overflow.bpl(89292,3): inline$BDLPnPStart$0$anon46_Else#1
stack_overflow.bpl(89306,3): inline$BDLPnPStart$0$label_101_true#1
+ stack_overflow.bpl(89313,3): inline$BDLPnPStart$0$label_102#1
stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#1
stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1
stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1
diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index 5fb6fe62..de255422 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -6,15 +6,11 @@ implementation b(x: int)
anon0:
- assume true;
- assume true;
goto anon3_Then;
anon3_Then:
- assume true;
assume x < 0;
y := 1;
- assume 1 <= y && y <= 1;
assert false;
return;
}
diff --git a/Test/test2/Answer b/Test/test2/Answer
index ef808373..8abc36c9 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -34,6 +34,7 @@ Execution trace:
Passification.bpl(165,3): Error BP5001: This assertion might not hold.
Execution trace:
Passification.bpl(158,1): L0
+ Passification.bpl(161,1): L1
Passification.bpl(164,1): L2
Boogie program verifier finished with 7 verified, 4 errors
@@ -213,14 +214,16 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar
Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement.
Structured.bpl(243,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Structured.bpl(245,3): anon0
+ Structured.bpl(244,5): anon0
Structured.bpl(246,5): anon6_LoopBody
Structured.bpl(247,7): anon7_LoopBody
+ Structured.bpl(248,11): anon8_Then
Structured.bpl(252,5): anon4
Structured.bpl(252,14): anon9_Then
Structured.bpl(303,3): Error BP5001: This assertion might not hold.
Execution trace:
Structured.bpl(299,5): anon0
+ Structured.bpl(300,3): anon3_Else
Structured.bpl(303,3): anon2
Structured.bpl(311,7): Error BP5001: This assertion might not hold.
Execution trace:
@@ -378,3 +381,18 @@ Execution trace:
CallForall.bpl(124,3): anon0
Boogie program verifier finished with 10 verified, 8 errors
+
+-------------------- ContractEvaluationOrder.bpl --------------------
+ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.
+ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(7,5): anon0
+ContractEvaluationOrder.bpl(15,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(12,5): anon0
+ContractEvaluationOrder.bpl(24,3): Error BP5002: A precondition for this call might not hold.
+ContractEvaluationOrder.bpl(30,3): Related location: This is the precondition that might not hold.
+Execution trace:
+ ContractEvaluationOrder.bpl(23,5): anon0
+
+Boogie program verifier finished with 1 verified, 3 errors
diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
new file mode 100644
index 00000000..3eab4bda
--- /dev/null
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -0,0 +1,34 @@
+procedure P() returns (x, y: int)
+ ensures x == y; // ensured by the body
+ ensures x == 0; // error: not ensured by the body
+ ensures y == 0; // follows from the previous two ensures clauses (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+{
+ x := y;
+}
+
+procedure Q() returns (x, y: int)
+{
+ x := y;
+
+ assert x == y; // ensured by the body
+ assert x == 0; // error: not ensured by the body
+ assert y == 0; // follows from the previous two asserts (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+}
+
+procedure R()
+{
+ var a, b: int;
+ a := b;
+ call S(a, b);
+}
+
+procedure S(x, y: int)
+ // In the call from R:
+ requires x == y; // ensured by the body of R
+ requires x == 0; // error: not ensured by the body of R
+ requires y == 0; // follows from the previous two requires clauses (provided they are
+ // indeed evaluated in this order, which they are supposed to be)
+{
+}
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index ce97b145..69ea2576 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -241,7 +241,7 @@ procedure RunOffEnd2() returns (x: int)
procedure RunOffEnd3() returns (x: int)
ensures x == 9;
-{
+{ x := 9;
while (true) {
while (true) {
if (*) {
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index f472741c..dbe5b726 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
echo -------------------- sk_hack.bpl --------------------
%BGEXE% %* /noinfer /bv:z sk_hack.bpl
-for %%f in (CallForall.bpl) do (
+for %%f in (CallForall.bpl ContractEvaluationOrder.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* %%f
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 10:03:04 +0000