diff options
| -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 | ||||
| -rw-r--r-- | Test/aitest0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/aitest1/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/aitest9/answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/inline/Answer | 16 | ||||
| -rw-r--r-- | Test/inline/runtest.bat | 7 | ||||
| -rw-r--r-- | Test/livevars/Answer | 15 | ||||
| -rw-r--r-- | Test/smoke/Answer | 4 | ||||
| -rw-r--r-- | Test/test2/Answer | 20 | ||||
| -rw-r--r-- | Test/test2/ContractEvaluationOrder.bpl | 34 | ||||
| -rw-r--r-- | Test/test2/Structured.bpl | 2 | ||||
| -rw-r--r-- | Test/test2/runtest.bat | 2 |
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
|