diff options
| author |  schaef <unknown> | 2011-03-15 02:58:31 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2011-03-15 02:58:31 +0000 |
| commit | 3b95e484b2e097534bf150edc87bc1b19b5892bf (patch) | |
| tree | f1ae58dc91efec7599a44d06908d85e83c9be2e4 /Source/VCGeneration | |
| parent | b7829c73906c7ddbc01e7e076aa430f349ae9698 (diff) | |
new algorithm for dead code detection (vc:doomed)
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/DoomCheck.cs | 824 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomErrorHandler.cs | 138 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomedLoopUnrolling.cs | 581 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomedStrategy.cs | 456 | ||||
| -rw-r--r-- | Source/VCGeneration/HasseDiagram.cs | 368 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 21 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 1054 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.csproj | 3 |
8 files changed, 1872 insertions, 1573 deletions
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 03f0af8f..7d84422a 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -54,14 +54,72 @@ void ObjectInvariant() }
- public bool CheckReachvar(Variable reachvar, out ProverInterface.Outcome outcome) {
- Contract.Requires(reachvar != null);
- VCExpr vc = m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(reachvar);
- Contract.Assert(vc != null);
+ public bool CheckReachvar(List<Variable> lv,Dictionary<Expr, int> finalreachvars,
+ int k, int l, bool usenew , out ProverInterface.Outcome outcome) {
+ Contract.Requires(lv != null);
+
+ VCExpr vc = VCExpressionGenerator.False;
+ if (usenew )
+ {
+ foreach (Variable v in lv)
+ {
+
+ vc = m_Checker.VCExprGen.Or(
+ m_Checker.VCExprGen.Neq(
+ m_Checker.VCExprGen.Integer(BigNum.ZERO),
+ m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)),
+ vc);
+ }
+ //Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count);
+
+ VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO);
+ VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO);
+
+ foreach (KeyValuePair<Expr, int> kvp in finalreachvars)
+ {
+
+ vc21 = m_Checker.VCExprGen.Add(vc21, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key));
+ vc22 = m_Checker.VCExprGen.Add(vc22, m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key));
+ }
+
+ VCExpr post = m_Checker.VCExprGen.Or(
+ m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21) ,
+ m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k)))
+ );
+
+ vc = (m_Checker.VCExprGen.Or(vc, (post) ));
+
+ }
+ else
+ {
+
+ foreach (Variable v in lv)
+ {
+
+ vc = m_Checker.VCExprGen.Or(
+ m_Checker.VCExprGen.Eq(
+ m_Checker.VCExprGen.Integer(BigNum.ONE),
+ m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(v)),
+ vc);
+ }
+ Contract.Assert(vc != null);
+
+ // Add the desired outcome of the reachability variables
+ foreach (KeyValuePair<Expr, int> kvp in finalreachvars)
+ {
+ vc = m_Checker.VCExprGen.Or(
+ m_Checker.VCExprGen.Neq(
+ m_Checker.VCExprGen.Integer(BigNum.FromInt(kvp.Value)),
+ m_Checker.TheoremProver.Context.BoogieExprTranslator.Translate(kvp.Key)),
+ vc);
+ }
+
+ }
+
// Todo: Check if vc is trivial true or false
outcome = ProverInterface.Outcome.Undetermined;
Contract.Assert( m_ErrorHandler !=null);
- m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
+ m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
m_Checker.ProverDone.WaitOne();
try {
@@ -69,7 +127,7 @@ void ObjectInvariant() } catch (UnexpectedProverOutputException e)
{
if (CommandLineOptions.Clo.TraceVerify) {
- Console.WriteLine("Prover is unable to check {0}! Reason:", reachvar.Name);
+ Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);
Console.WriteLine(e.ToString());
}
return false;
@@ -81,13 +139,13 @@ void ObjectInvariant() internal class DoomCheck {
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Label2Absy!=null);
- Contract.Invariant(m_Check != null);
- Contract.Invariant(m_Evc != null);
- Contract.Invariant(m_Order != null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(Label2Absy!=null);
+ Contract.Invariant(m_Check != null);
+ Contract.Invariant(m_Evc != null);
+ Contract.Invariant(m_Order != null);
+ }
#region Attributes
public Hashtable Label2Absy;
@@ -104,53 +162,98 @@ void ObjectInvariant() private DoomErrorHandler m_ErrHandler;
private Checker m_Check;
- private InclusionOrder m_Order;
+ private DoomDetectionStrategy m_Order;
private Evc m_Evc;
#endregion
+ public void __DEBUG_PrintStatistics()
+ {
+ Console.WriteLine("Checked/Total: Bl {0} / {1} EQ {2} / {3} {4} Tr {5} {6} / {7}", m_Order.__DEBUG_BlocksChecked, m_Order.__DEBUG_BlocksTotal, m_Order.__DEBUG_EQCChecked, m_Order.__DEBUG_EQCTotal, m_Order.__DEBUG_EQCLeaf, m_Order.__DEBUG_TracesChecked, m_Order.__DEBUG_InfeasibleTraces, m_Order.__DEBUG_TracesTotal);
+ }
+
[NotDelayed]
- public DoomCheck (Implementation passive_impl, Checker check) {
+ public DoomCheck (Implementation passive_impl, Block unifiedExit, Checker check, List<Block> uncheckable) {
Contract.Requires(passive_impl != null);
Contract.Requires(check != null);
- m_Check = check;
- if (!VC.DCGen.UseItAsDebugger ) {
- m_Order = new InclusionOrder(passive_impl.Blocks[0]);
- } else {
- m_Order = new InclusionOrder(cce.NonNull(VC.DCGen.firstNonDebugBlock) );
+ Contract.Requires(uncheckable != null);
+ m_Check = check;
+
+ //@Cristiano: Plug your own optimizer here.
+ int replaceThisByCmdLineOption = CommandLineOptions.Clo.DoomStrategy ;
+ Console.Write("Running experiments using {0} /", replaceThisByCmdLineOption);
+ switch (replaceThisByCmdLineOption)
+ {
+ default:
+ {
+ Console.WriteLine("Path Cover specialK Strategy");
+ m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable, true);
+
+ break;
+ }
+ case 1:
+ {
+ Console.WriteLine("Path Cover Strategy");
+ m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable);
+ break;
+ }
+ case 2:
+ {
+ Console.WriteLine("hasse strategy");
+ m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable);
+
+ break;
+ }
+ case 3:
+ {
+ Console.WriteLine("hasse+ce strategy");
+ m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable);
+ break;
+ }
+ case 4:
+ {
+ Console.WriteLine("no strategy");
+ m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable);
+ break;
+ }
+
}
+
Label2Absy = new Hashtable(); // This is only a dummy
m_Evc = new Evc(check);
Hashtable l2a = null;
VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check);
- Contract.Assert(vce != null);
+ Contract.Assert(vce != null);
Contract.Assert( l2a!=null);
Label2Absy = l2a;
-// vce = check.VCExprGen.Implies(vce, vce);
- m_Evc.Initialize(vce);
+
+ m_Evc.Initialize(vce);
}
+ public static VCExpr __tmpHack;
+
/* - Set b to the next block that needs to be checked.
- Returns false and set b to null if all blocks are checked.
- Has to be alternated with CheckLabel; might crash otherwise
*/
- public bool GetNextBlock(out Block b) {
- return m_Order.GetNextBlock(out b);
+ public bool GetNextBlock(out List<Block> lb)
+ {
+ return m_Order.GetNextBlock(out lb);
}
/* - Checking a label means to ask the prover if |= ( rvar=false -> vc ) holds.
- outcome is set to Outcome.Invalid if the Block denoted by reachvar is doomed.
- returns false if the theorem prover throws an exception, otherwise true.
*/
- public bool CheckLabel(Variable reachvar, out ProverInterface.Outcome outcome) {
- Contract.Requires(reachvar != null);
+ public bool CheckLabel(List<Variable> lv,Dictionary<Expr, int> finalreachvars, out ProverInterface.Outcome outcome) {
+ Contract.Requires(lv != null);
outcome = ProverInterface.Outcome.Undetermined;
- if (m_Evc.CheckReachvar(reachvar, out outcome) ) {
- if (!m_Order.SetCurrentResult(reachvar, outcome, m_ErrHandler)) {
+ if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck, out outcome) ) {
+ if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) {
outcome = ProverInterface.Outcome.Undetermined;
}
return true;
} else {
- m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);
+ m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler);
return false;
}
}
@@ -187,40 +290,9 @@ void ObjectInvariant() VCExpr vc;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Doomed:
-
- if (!VC.DCGen.UseItAsDebugger ) {
- vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context);
- }
- #region _TESTING_NEW_STUFF_
- else {
-
- CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;
- Contract.Assert( VC.DCGen.firstDebugBlock != null);
- VCExpr a = LetVC(VC.DCGen.firstDebugBlock, label2absy, ch.TheoremProver.Context);
- Contract.Assert(a != null);
- CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;
-
-
- VCExpr b = LetVC(cce.NonNull(VC.DCGen.firstNonDebugBlock), label2absy, ch.TheoremProver.Context);
-
- //_tmpUseFreshBVars=false;
- //vc = ch.VCExprGen.Not(ch.VCExprGen.Implies( wp, ch.VCExprGen.Not(vc)));
-
- vc = ch.VCExprGen.Not(ch.VCExprGen.Implies(ch.VCExprGen.Not(a), ch.VCExprGen.Not(b)));
-
-
- /*
- ConsoleColor col = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Green;
- Console.WriteLine(vc.ToString());
- Console.ForegroundColor = col;
- Console.WriteLine(" ... was asked.");
- */
-
- }
- #endregion
-
+ vc = LetVC(cce.NonNull(impl.Blocks[0]), label2absy, ch.TheoremProver.Context);
+
break;
default:
@@ -303,629 +375,7 @@ void ObjectInvariant() #endregion
-
-
- #region Build Inclusion Order to minimize the number of checks
- class InclusionOrder
- {
-
- #region Attributes
- public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();
-
-
- InclusionTree RootNode = new InclusionTree(null);
- InclusionTree currentNode = null;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(DetectedBlock!=null);
- Contract.Invariant(RootNode != null);
-}
-
- #endregion
-
- private void printmap(Dictionary<Block, TraceNode> map)
- {
- foreach(KeyValuePair<Block,TraceNode> kvp in map)
- {
- Console.Write("{0} :", kvp.Key.Label);
- foreach (TraceNode t in kvp.Value.Unavoidables) Console.Write("{0}, ", t.block.Label);
- Console.WriteLine();
- }
- }
-
- [NotDelayed]
- public InclusionOrder(Block rootblock) {Contract.Requires(rootblock != null);
- /*
- We now compute for each block the set of blocks that
- are reached on every execution reaching this block (dominator).
- We first compute it form the start block to the current
- block and second from the Term block to the current one.
- Finally we build the union.
- */
- Dictionary<Block,TraceNode> map2 = new Dictionary<Block,TraceNode>();
- Dictionary<Block,TraceNode> map = new Dictionary<Block,TraceNode>();
-
- Dictionary<Block, List<Block>> unavoidablemap = new Dictionary<Block, List<Block>>();
-
- Block exitblock = BreadthFirst(rootblock, map2);
- Contract.Assert(exitblock != null);
- BreadthFirstBwd(exitblock, map);
-
- foreach (KeyValuePair<Block, TraceNode> kvp in map) {
- Contract.Assert(kvp.Key != null);Contract.Assert(kvp.Value != null);
- List<Block/*!*/>/*!*/ blist = new List<Block/*!*/>();
- foreach (TraceNode tn in kvp.Value.Unavoidables ) {
- if (!blist.Contains(tn.block)) blist.Add(tn.block);
- }
- unavoidablemap.Add(kvp.Key, blist);
- }
-
-
- foreach (KeyValuePair<Block, List<Block>> kvp in unavoidablemap) {
- Contract.Assert(kvp.Key != null);
- Contract.Assert(cce.NonNullElements(kvp.Value));
- TraceNode tn = null;
- if (map2.TryGetValue(kvp.Key, out tn) ) {
- Contract.Assert( tn!=null);
- foreach (TraceNode t0 in tn.Unavoidables) {Contract.Assert(t0 != null);
- if (!kvp.Value.Contains(t0.block))
- kvp.Value.Add(t0.block);
- }
- } else {
- //assert false;
- }
- }
-
- foreach (KeyValuePair<Block, List<Block>> kvp in unavoidablemap) {
- Contract.Assert(kvp.Key != null);
- Contract.Assert(cce.NonNullElements(kvp.Value));
- Insert2Tree(RootNode,kvp);
- }
- InitCurrentNode(RootNode);
- }
-
- void InitCurrentNode(InclusionTree n) {Contract.Requires(n != null);
- if (n.Children.Count>0) {
- InitCurrentNode(n.Children[0]);
- } else {
- currentNode = n;
- }
- }
-
- public bool GetNextBlock(out Block b) {
- if (currentNode!=null && currentNode.EquivBlock.Count>0) {
- b = currentNode.EquivBlock[0];
- return true;
- }
- b = null;
- return false;
- }
-
-
- /*
- Warning: this is a very slow implementation. There should be
- a map from Block to InclusionTree to prevent running through
- the tree over and over again.
- */
- private void MarkUndoomedFromCE(Block b, InclusionTree node)
- {Contract.Requires(b != null);Contract.Requires(node != null);
- if (node.EquivBlock.Contains(b) ) {
- //Console.WriteLine("Block {0} does not need to be checked - appears in CE", b.Label);
- node.HasBeenChecked = true;
- node.IsDoomed = false;
- MarkUndoomedParents(node);
- return;
- } else
- {
- foreach (InclusionTree c in node.Children) {
- Contract.Assert(c != null);
- MarkUndoomedFromCE(b, c);
- }
- }
- }
-
- // Takes the outcome for the current reachvar and marks all blocks
- // the do not need any further checking because they share the same
- // desteny
- // returns false if an explicite assert false was found.
- // Warning: Still slow; we do not need to do this while constructing the error report!
- public bool SetCurrentResult(Variable reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) {Contract.Requires(reachvar != null);
- if (outcome!=ProverInterface.Outcome.Valid) {
- if (currentNode != null) {
- currentNode.IsDoomed = false;
- currentNode.HasBeenChecked = true;
- MarkUndoomedParents(currentNode);
- if (cb != null) {
- //Console.WriteLine("CE contains: ");
- foreach (Block b in cb.TraceNodes)
- {Contract.Assert(b != null);
- //Console.Write("{0}, ", b.Label);
- MarkUndoomedFromCE(b, RootNode);
- }
- //Console.WriteLine();
- } else {
- Console.WriteLine("ErrorHandler is not valid! ------ (DoomCheck)");
- }
-
- currentNode = FindNextNode(currentNode);
- }
- } else {
- if (currentNode != null) {
-
- // Check if there is an assert false in this node or in one of its parents
- // if so do not report anything
-// if (ECContainsAssertFalse(currentNode.EquivBlock)) {
-//
-// ConsoleColor col = Console.ForegroundColor;
-// Console.ForegroundColor = ConsoleColor.Blue;
-// Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");
-// Console.ForegroundColor = col;
-//
-// currentNode.HasBeenChecked = true;
-// currentNode.IsDoomed = false;
-// currentNode = currentNode.Parent;
-// return false;
-// }
-
- List<Block> traceblocks = new List<Block>();
-
- TracedChildern(currentNode, traceblocks);
- TracedParents(currentNode, traceblocks);
-
-// cb.OnWarning("Doomed program points found!");
- if (cb != null) {
- cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
- }
-
- if (currentNode.EquivBlock.Count>0) {
-
- foreach (InclusionTree n in currentNode.Children) {Contract.Assert(n != null);
- if (DetectedBlock.Contains(n.EquivBlock) ) {
- DetectedBlock.Remove(n.EquivBlock);
- }
- }
-
- DetectedBlock.Add(currentNode.EquivBlock);
-
- } else {
- Console.WriteLine("An empty equivalence class has been detected");
- Contract.Assert(false);throw new cce.UnreachableException();
- }
-
- currentNode.IsDoomed = true;
- currentNode.HasBeenChecked = true;
- MarkDoomedChildren(currentNode);
- currentNode = currentNode.Parent;
- if (currentNode!=null) {
- foreach (InclusionTree it in currentNode.Children) {
- Contract.Assert(it != null);
- if (!it.HasBeenChecked) {
- currentNode = DescendToDeepestUnchecked(it);
- break;
- }
- }
- }
- }
- }
- return true;
- }
-
- private InclusionTree DescendToDeepestUnchecked(InclusionTree node)
- {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<InclusionTree>() != null);
-
- foreach (InclusionTree it in node.Children) {Contract.Assert(it != null);
- if (!it.HasBeenChecked) {
- return DescendToDeepestUnchecked(it);
- }
- }
- return node;
- }
-
- private bool ECContainsAssertFalse(List<Block> equiv) {
- Contract.Requires(cce.NonNullElements(equiv));
- foreach (Block b in equiv) {Contract.Assert(b != null);
- if (BlockContainsAssertFalse(b)) return true;
- }
- return false;
- }
-
- private bool BlockContainsAssertFalse(Block b) {Contract.Requires(b != null);
- foreach (Cmd c in b.Cmds) {Contract.Assert(c != null);
- AssertCmd ac = c as AssertCmd;
- if (ac!=null) {
- if (IsFalse(ac.Expr) || QKeyValue.FindBoolAttribute(ac.Attributes, "PossiblyUnreachable") ) {
- return true;
- }
- }
- }
- return false;
- }
-
- // check if e is true, false, !true, !false
- // if so return true and the value of the expression in val
- bool BooleanEval(Expr e, ref bool val)
- {
- Contract.Requires(e != null);
- LiteralExpr lit = e as LiteralExpr;
- NAryExpr call = e as NAryExpr;
-
- if (lit != null && lit.isBool) {
- val = lit.asBool;
- return true;
- } else if (call != null &&
- call.Fun is UnaryOperator &&
- ((UnaryOperator)call.Fun).Op == UnaryOperator.Opcode.Not &&
- BooleanEval(cce.NonNull(call.Args[0]), ref val)) {
- val = !val;
- return true;
- }
- // this is for the 0bv32 != 0bv32 generated by vcc
- else if (call != null &&
- call.Fun is BinaryOperator &&
- ((BinaryOperator)call.Fun).Op == BinaryOperator.Opcode.Neq &&
- call.Args[0] is LiteralExpr &&
- cce.NonNull(call.Args[0]).Equals(call.Args[1]))
- {
- val = false;
- return true;
- }
-
- return false;
- }
-
- bool IsFalse(Expr e)
- {Contract.Requires(e != null);
- bool val = false;
- return BooleanEval(e, ref val) && !val;
- }
-
- private void TracedChildern(InclusionTree node, List<Block/*!*/>/*!*/ blist) {
- Contract.Requires(node != null);
- Contract.Requires(cce.NonNullElements(blist));
- foreach (Block b in node.EquivBlock) {Contract.Assert(b != null);
- if (!blist.Contains(b)) blist.Add(b);
- }
- foreach (InclusionTree n in node.Children) {
- Contract.Assert(n != null);
- TracedChildern(n, blist);
- }
- }
-
- private void TracedParents(InclusionTree node, List<Block> blist) {
- Contract.Requires(node != null);
- Contract.Requires(cce.NonNullElements(blist));
- foreach (Block b in node.EquivBlock) {Contract.Assert(b != null);
- if (!blist.Contains(b)) blist.Add(b);
- }
- if (node.Parent!=null) {
- TracedParents(node.Parent, blist);
- }
- }
-
- InclusionTree FindNextNode(InclusionTree n) {Contract.Requires(n != null);
- Contract.Assert( n!=n.Parent);
- InclusionTree next = n.Parent;
- if (next!=null) {
- foreach (InclusionTree n0 in next.Children) {
- Contract.Assert(n0 != null);
- if (!n0.HasBeenChecked) {
- return DescendToDeepestUnchecked(n0); ;
- }
- }
- return FindNextNode(next);
- }
- return next;
- }
-
- void MarkUndoomedParents(InclusionTree n) {Contract.Requires(n != null);
- if (n.Parent != null) {
- n.Parent.HasBeenChecked = true;
- n.Parent.IsDoomed = false;
- MarkUndoomedParents(n.Parent);
- }
- }
-
- void MarkDoomedChildren(InclusionTree n) {Contract.Requires(n != null);
- foreach (InclusionTree t in n.Children) {
- Contract.Assert(t != null);
- t.IsDoomed = true;
- t.HasBeenChecked = true;
- MarkDoomedChildren(t);
- }
- }
-
- bool Insert2Tree(InclusionTree node, KeyValuePair<Block, List<Block>> kvp) {
- Contract.Requires(node != null);
- Contract.Requires(kvp.Key != null);
- Contract.Requires(cce.NonNullElements(kvp.Value));
- if (IsSubset(node.PathBlocks, kvp.Value) ) {
- if (IsSubset(kvp.Value, node.PathBlocks) ) {
- // The set of unavoidable blocks is equal, so
- // we can put the block in the same node.
- node.EquivBlock.Add(kvp.Key);
- return true;
- } else {
- foreach (InclusionTree n in node.Children) {Contract.Assert(n != null);
- if (Insert2Tree(n,kvp) ) {
- return true;
- }
- }
- // we have not been able to add the block to one of
- // the children, so we have to create a new child.
- InclusionTree it = new InclusionTree(node);
- Contract.Assert(it != null);
- it.EquivBlock.Add(kvp.Key);
- it.PathBlocks.AddRange(kvp.Value);
- node.Children.Add(it);
- return true;
- }
- // If we reached this point, we have to add a new node since
- // our current set of pathnodes is not a subset of anything else
- } else {
- // seems, that we have reached a new leaf.
- }
- return false;
- }
-
- bool IsSubset(List<Block> sub, List<Block> super ) {Contract.Requires(sub!=null);Contract.Requires(cce.NonNullElements(super));
- foreach (Block b in sub) {
- Contract.Assert(b != null);
- if (!super.Contains(b) ) return false;
- }
- return true;
- }
-
- void printtree(InclusionTree n, string indent, int level) {Contract.Requires(n != null);
- Console.Write("{0}Level {1}: Blocks ", indent, level);
- foreach (Block b in n.EquivBlock) {Contract.Assert(b != null);
- Console.Write("{0}, ", b.Label);
- }
- Console.WriteLine();
-
- foreach (InclusionTree t in n.Children) {
- Contract.Assert(t != null);
- printtree(t, indent+" ", level+1);
- }
- }
-
- private class InclusionTree {
- public InclusionTree(InclusionTree p) {
- Parent = p;
- HasBeenChecked=false;
- IsDoomed = false;
- }
-
- public bool HasBeenChecked;
- public bool IsDoomed;
- public InclusionTree Parent;
- public List<Block/*!*/>/*!*/ EquivBlock = new List<Block>();
- public List<Block/*!*/>/*!*/ PathBlocks = new List<Block>();
- public List<InclusionTree/*!*/>/*!*/ Children = new List<InclusionTree>();
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Parent!=null);
- Contract.Invariant(cce.NonNullElements(EquivBlock));
- Contract.Invariant(cce.NonNullElements(PathBlocks));
- Contract.Invariant(cce.NonNullElements(Children));
-}
- }
-
- #region Collect Unavoidable Blocks
- private Block BreadthFirst(Block start, Dictionary<Block, TraceNode> blockmap) {
- Contract.Requires(start != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
- Contract.Ensures(Contract.Result<Block>() != null);
-
- List<Block> JobList = new List<Block>();
- List<Block> DoneList = new List<Block>();
- Block exitblock=null;
- JobList.Add(start);
- Block currentBlock = JobList[0];
- // Travers the Graph Breadth First and collect all
- // predecessors of each node that are reached on any
- // path to this node
- while (JobList.Count>0)
- {
- currentBlock = JobList[0];
- TraceNode tn = new TraceNode(currentBlock);
- Contract.Assert(tn != null);
-
- if (currentBlock.Predecessors.Length>0 ) {
- TraceNode t0 =null;
- Block firstpred = currentBlock.Predecessors[0];
-
- Contract.Assert( firstpred!=null);
- if (blockmap.TryGetValue(firstpred, out t0)) {
- Contract.Assert( t0 !=null);
- tn.Unavoidables.AddRange(t0.Unavoidables);
- }
- }
-
- foreach (Block b0 in currentBlock.Predecessors) {Contract.Assert(b0 != null);
- TraceNode t = null;
- if (blockmap.TryGetValue(b0, out t)) {
- Contract.Assert( t!=null);
- tn.Predecessors.Add(t);
- IntersectUnavoidables(t,tn);
- if (!t.Successors.Contains(tn)) t.Successors.Add(tn);
- blockmap[b0]=t;
- }
- }
- if (!tn.Unavoidables.Contains(tn)) {
- tn.Unavoidables.Add(tn);
- } else
- {
- Contract.Assert(false);throw new cce.UnreachableException();
- }
-
-
- blockmap.Add(currentBlock, tn);
-
- GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
- if (gc!=null) {
- Contract.Assert( gc.labelTargets!=null);
- foreach (Block b0 in gc.labelTargets) {
- Contract.Assert(b0 != null);
- bool notready = false;
- foreach (Block b1 in b0.Predecessors)
- {
- if (!JobList.Contains(b1) && !DoneList.Contains(b1))
- {
- notready = true;
- break;
- }
- }
- if (notready) continue;
- if (!JobList.Contains(b0) && !DoneList.Contains(b0)) {
-
- JobList.Add(b0);
- }
- }
- } else {
- exitblock=currentBlock;
- }
- DoneList.Add(currentBlock);
- JobList.RemoveAt(0);
- }
- Contract.Assert( exitblock!=null);
- return exitblock;
- }
-
- // WARNING: It is only for testing reasons that
- // BreadthFirstBwd and BreadthFirst and separat functions
- // it should be implemented using one function later on.
- private void BreadthFirstBwd(Block start, Dictionary<Block, TraceNode> blockmap) {
- Contract.Requires(start != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
-
- List<Block> JobList = new List<Block>();
- List<Block> DoneList = new List<Block>();
- JobList.Add(start);
- Block currentBlock = JobList[0];
- // Travers the Graph Breadth First and collect all
- // predecessors of each node that are reached on any
- // path to this node
- while (JobList.Count>0)
- {
- currentBlock = JobList[0];
- TraceNode tn = new TraceNode(currentBlock);Contract.Assert(tn != null);
-
- GotoCmd gc = currentBlock.TransferCmd as GotoCmd;
- BlockSeq preds = null;
- if (gc!=null) {
- preds = gc.labelTargets;
- }
-
- if (preds != null ) {
-
- TraceNode t0 =null;
- Block firstpred = preds[0];
-
- Contract.Assert( firstpred!=null);
- if (blockmap.TryGetValue(firstpred, out t0)) {
- Contract.Assert( t0 !=null);
- tn.Unavoidables.AddRange(t0.Unavoidables);
- }
-
-
- foreach (Block b0 in preds) {Contract.Assert(b0 != null);
- TraceNode t = null;
- if (blockmap.TryGetValue(b0, out t)) {
- Contract.Assert( t!=null);
- tn.Successors.Add(t);
- IntersectUnavoidables(t,tn);
- if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);
- blockmap[b0]=t;
- }
- }
- }
- if (!tn.Unavoidables.Contains(tn)) {
- tn.Unavoidables.Add(tn);
- } else
- {
- Contract.Assert(false);throw new cce.UnreachableException();
- }
- blockmap.Add(currentBlock, tn);
-
- if (currentBlock.Predecessors.Length>0) {
- foreach (Block b0 in currentBlock.Predecessors) {
- Contract.Assert(b0 != null);
- GotoCmd gcmd = b0.TransferCmd as GotoCmd;
- if (gcmd != null)
- {
- bool notready = false;
- Contract.Assert(gcmd.labelTargets != null);
- foreach (Block b1 in gcmd.labelTargets)
- {
- Contract.Assert(b1 != null);
- if (!JobList.Contains(b1) && !DoneList.Contains(b1))
- {
- notready = true;
- break;
- }
- }
- if (notready) continue;
- }
- if (!JobList.Contains(b0) && !DoneList.Contains(b0) )
- JobList.Add(b0);
- }
- }
- DoneList.Add(currentBlock);
- JobList.RemoveAt(0);
- }
- }
-
- private void IntersectUnavoidables(TraceNode parent, TraceNode child) {
- Contract.Requires(parent != null);
- Contract.Requires(child != null);
- List<TraceNode/*!*/>/*!*/ ret = new List<TraceNode>();
- List<TraceNode/*!*/>/*!*/ tmp = new List<TraceNode>();
- tmp.AddRange(parent.Unavoidables);
- tmp.AddRange(child.Unavoidables);
-
- foreach (TraceNode tn in tmp) {Contract.Assert(tn != null);
- if (parent.Unavoidables.Contains(tn) && child.Unavoidables.Contains(tn)
- && !ret.Contains(tn) ) {
- ret.Add(tn);
- }
- }
- Contract.Assert( ret.Count <= parent.Unavoidables.Count && ret.Count <= child.Unavoidables.Count);
- child.Unavoidables = ret;
-
- }
-
- #region TraceNode Class
- // We assume that the program is already loopfree, otherwise we will
- // not terminate
- private class TraceNode {
- public List<TraceNode/*!*/>/*!*/ Predecessors = new List<TraceNode>();
- public List<TraceNode/*!*/>/*!*/ Successors = new List<TraceNode>();
- public List<TraceNode/*!*/>/*!*/ Unavoidables = new List<TraceNode>();
- public Block/*!*/ block;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(block != null);
- Contract.Invariant(cce.NonNullElements(Predecessors));
- Contract.Invariant(cce.NonNullElements(Successors));
- Contract.Invariant(cce.NonNullElements(Unavoidables));
- }
-
- public TraceNode(Block b) {
- Contract.Requires(b != null);
- block=b;
- }
-
- }
- #endregion
- #endregion
- }
- #endregion
-
-
+
}
+
}
diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs index 12936c1f..76893b8c 100644 --- a/Source/VCGeneration/DoomErrorHandler.cs +++ b/Source/VCGeneration/DoomErrorHandler.cs @@ -13,106 +13,76 @@ using Microsoft.Boogie.VCExprAST; namespace VC
{
- internal class DoomErrorHandler : ProverInterface.ErrorHandler {
+ internal class DoomErrorHandler : ProverInterface.ErrorHandler
+ {
protected Hashtable label2Absy;
protected VerifierCallback callback;
private List<Block> m_CurrentTrace = new List<Block>();
- public Variable m_Reachvar;
- public List<Block> m_DoomedBlocks, m_TraceBlocks;
-
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(label2Absy!=null);
- Contract.Invariant(callback != null);
- Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
- Contract.Invariant(m_Reachvar != null);
- Contract.Invariant(m_DoomedBlocks != null);
- Contract.Invariant(m_TraceBlocks != null);
-}
-
- public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
- Contract.Requires(label2Absy != null);
- Contract.Requires(callback != null);
- this.label2Absy = label2Absy;
- this.callback = callback;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(label2Absy != null);
+ Contract.Invariant(callback != null);
+ Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
}
-
- public override Absy Label2Absy(string label) {
- //Contract.Requires(label != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- int id = int.Parse(label);
- return cce.NonNull((Absy) label2Absy[id]);
+
+ public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback)
+ {
+ Contract.Requires(label2Absy != null);
+ Contract.Requires(callback != null);
+ this.label2Absy = label2Absy;
+ this.callback = callback;
}
-
- public override void OnProverWarning(string msg) {
- //Contract.Requires(msg != null);
- this.callback.OnWarning(msg);
+
+ public override Absy Label2Absy(string label)
+ {
+ //Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+
+ int id = int.Parse(label);
+ return cce.NonNull((Absy)label2Absy[id]);
}
-
- public void OnDoom(Variable reachvar, List<Block>/*!>!*/ doomedblocks, List<Block>/*!>!*/ traceblocks) {
- Contract.Requires(reachvar != null);
- Contract.Requires(cce.NonNullElements(doomedblocks));
- Contract.Requires(cce.NonNullElements(traceblocks));
- m_Reachvar = reachvar;
- m_DoomedBlocks = doomedblocks;
- m_TraceBlocks = traceblocks;
+
+ public override void OnProverWarning(string msg)
+ {
+ //Contract.Requires(msg != null);
+ this.callback.OnWarning(msg);
}
-
-
-
- public List<Block>/*!>!*/ TraceNodes
+
+
+ public List<Block>/*!>!*/ TraceNodes
{
get
{
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+
return m_CurrentTrace;
}
}
-
- public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
- //Contract.Requires(labels != null);
-
- m_CurrentTrace.Clear();
- //Console.Write("Used Blocks: ");
- List<Block> traceNodes = new List<Block>();
- List<AssertCmd> assertNodes = new List<AssertCmd>();
- foreach (string s in labels) {
- Contract.Assert(s != null);
- Absy node = Label2Absy(s);
- if (node is Block) {
- Block b = (Block)node;
- traceNodes.Add(b);
- //Console.Write("{0}, ", b.Label);
- } else {
- AssertCmd a = (AssertCmd)node;
- assertNodes.Add(a);
- }
- }
- m_CurrentTrace.AddRange(traceNodes);
- //Console.WriteLine();
-// assert assertNodes.Count > 0;
-// assert traceNodes.Count == assertNodes.Count;
-//
-// foreach (AssertCmd a in assertNodes) {
-// // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)
-// foreach (Block b in traceNodes) {
-// if (b.Cmds.Has(a)) {
-// BlockSeq trace = new BlockSeq();
-// trace.Add(b);
-// goto NEXT_ASSERT;
-// }
-// }
-// assert false; // there was no block that contains the assert
-// NEXT_ASSERT: {}
-// }
-
+
+ public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel)
+ {
+ // TODO: it would be better to check which reachability variables are actually set to one!
+ List<Block> traceNodes = new List<Block>();
+ List<AssertCmd> assertNodes = new List<AssertCmd>();
+ foreach (string s in labels)
+ {
+ Contract.Assert(s != null);
+ Absy node = Label2Absy(s);
+ if (node is Block)
+ {
+ Block b = (Block)node;
+ traceNodes.Add(b);
+ //Console.Write("{0}, ", b.Label);
+ }
+ }
+ m_CurrentTrace.AddRange(traceNodes);
+
}
-
+
}
-
+
}
\ No newline at end of file diff --git a/Source/VCGeneration/DoomedLoopUnrolling.cs b/Source/VCGeneration/DoomedLoopUnrolling.cs new file mode 100644 index 00000000..1e42a535 --- /dev/null +++ b/Source/VCGeneration/DoomedLoopUnrolling.cs @@ -0,0 +1,581 @@ +using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+ #region Loop handeling for doomed code detection
+
+ #region Loop Remover
+ internal class LoopRemover
+ {
+ GraphAnalyzer m_GraphAnalyzer;
+
+ public LoopRemover(GraphAnalyzer ga)
+ {
+ m_GraphAnalyzer = ga;
+ }
+
+ private void m_RemoveBackEdge(Loop l)
+ {
+ // first remove the backedges of the nested loops
+ foreach (Loop c in l.NestedLoops) m_RemoveBackEdge(c);
+ //Debugger.Break();
+ GraphNode loopSkip = null;
+ foreach (GraphNode gn in l.Cutpoint.Suc)
+ {
+ if (l.LoopExitNodes.Contains(gn))
+ {
+ loopSkip = gn; break;
+ }
+ }
+ if (loopSkip == null)
+ { // We didn't find a loop exit node. There must be a bug
+ Debugger.Break();
+ }
+ foreach (GraphNode gn in l.Cutpoint.LoopingPred)
+ {
+ List<GraphNode> newsuc = new List<GraphNode>();
+ foreach (GraphNode s in gn.Suc)
+ {
+ if (s == l.Cutpoint) newsuc.Add(loopSkip);
+ else newsuc.Add(s);
+ }
+ gn.Suc = newsuc;
+ }
+ }
+
+ private void m_AbstractLoop(Loop l)
+ {
+ foreach (Loop c in l.NestedLoops) m_AbstractLoop(c);
+ m_HavocLoopBody(l);
+ m_RemoveBackEdge(l);
+ }
+
+ public void AbstractLoopUnrolling()
+ {
+ foreach (Loop l in m_GraphAnalyzer.Graphloops)
+ {
+ m_MarkLoopExitUncheckable(l);
+ m_AbstractLoopUnrolling(l,null, "",true);
+ }
+ }
+
+ private void m_HavocLoopBody(Loop l)
+ {
+ List<Block> loopblocks = new List<Block>();
+ foreach (GraphNode g in l.LoopNodes) loopblocks.Add(g.Label);
+ HavocCmd hcmd = m_ComputHavocCmd(loopblocks, l.Cutpoint.Label.tok);
+
+ //Add Havoc before and after the loop body
+ foreach (GraphNode g in l.Cutpoint.Suc) // before
+ {
+ if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd);
+ }
+ foreach (GraphNode g in l.Cutpoint.Pre) // and after
+ {
+ if (l.LoopNodes.Contains(g)) m_AddHavocCmdToFront(g.Label, hcmd);
+ }
+ }
+
+ private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd)
+ {
+ CmdSeq cs = new CmdSeq();
+ cs.Add(hcmd); cs.AddRange(b.Cmds);
+ b.Cmds = cs;
+ }
+
+ private HavocCmd m_ComputHavocCmd(List<Block> bl, IToken tok)
+ {
+ Contract.Requires(bl != null);
+ Contract.Requires(tok != null);
+ Contract.Ensures(Contract.Result<HavocCmd>() != null);
+
+ VariableSeq varsToHavoc = new VariableSeq();
+ foreach (Block b in bl)
+ {
+ Contract.Assert(b != null);
+ foreach (Cmd c in b.Cmds)
+ {
+ Contract.Assert(c != null);
+ c.AddAssignedVariables(varsToHavoc);
+ }
+ }
+ IdentifierExprSeq havocExprs = new IdentifierExprSeq();
+ foreach (Variable v in varsToHavoc)
+ {
+ Contract.Assert(v != null);
+ 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 void m_AbstractLoopUnrolling(Loop l, Loop parent, string prefix, bool unfold)
+ {
+ //Debugger.Break();
+ if (unfold)
+ {
+
+ Loop first = new Loop(l, m_GraphAnalyzer,prefix+"FI_");
+ Loop last = new Loop(l, m_GraphAnalyzer,prefix+"LA_");
+ Loop abs = new Loop(l, m_GraphAnalyzer, prefix + "AB_");
+ foreach (Loop c in first.NestedLoops) m_AbstractLoopUnrolling(c, first, prefix + "FI_", false);
+ foreach (Loop c in last.NestedLoops) m_AbstractLoopUnrolling(c, last, prefix + "LA_", false);
+ foreach (Loop c in abs.NestedLoops) m_AbstractLoopUnrolling(c, abs, prefix + "AB_", true);
+
+ //Debugger.Break();
+
+ if (parent != null)
+ {
+ foreach (GraphNode gn in l.LoopNodes)
+ {
+ if (parent.LoopNodes.Contains(gn)) parent.LoopNodes.Remove(gn);
+ }
+ foreach (GraphNode gn in abs.LoopNodes)
+ {
+ if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);
+ }
+ foreach (GraphNode gn in first.LoopNodes)
+ {
+ if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);
+ }
+ foreach (GraphNode gn in last.LoopNodes)
+ {
+ if (!parent.LoopNodes.Contains(gn)) parent.LoopNodes.Add(gn);
+ }
+ }
+
+ m_HavocLoopBody(abs);
+ List<GraphNode> backupPre = new List<GraphNode>();
+ backupPre.AddRange(l.Cutpoint.Pre);
+ foreach (GraphNode pre in backupPre)
+ {
+ if (!l.Cutpoint.LoopingPred.Contains(pre))
+ {
+ pre.RemoveEdgeTo(l.Cutpoint);
+ pre.RemoveEdgeTo(abs.Cutpoint);
+ pre.AddEdgeTo(first.Cutpoint);
+ }
+ }
+
+ m_RemoveRegularLoopExit(last);
+ m_RemoveRegularLoopExit(abs);
+
+ m_ReplaceBackEdge(first, abs.Cutpoint);
+ m_ReplaceBackEdge(abs, last.Cutpoint);
+ foreach (GraphNode gn in first.Cutpoint.Suc)
+ {
+ if (!first.LoopNodes.Contains(gn))
+ {
+ m_ReplaceBackEdge(last, gn);
+ break;
+ }
+ }
+
+ // Remove all remaining connections to the original loop
+ foreach (GraphNode gn in l.LoopExitNodes)
+ {
+ List<GraphNode> tmp = new List<GraphNode>();
+ tmp.AddRange(gn.Pre);
+ foreach (GraphNode g in tmp)
+ {
+ if (l.LoopNodes.Contains(g))
+ {
+ //Debugger.Break();
+ g.RemoveEdgeTo(gn);
+ }
+ }
+ }
+ foreach (GraphNode gn in l.LoopNodes)
+ {
+ m_GraphAnalyzer.DeleteGraphNode(gn);
+ }
+ foreach (GraphNode gn in first.LoopNodes)
+ {
+ if (gn != first.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn) )
+ m_GraphAnalyzer.UncheckableNodes.Add(gn);
+ }
+ foreach (GraphNode gn in last.LoopNodes)
+ {
+ if (gn != last.Cutpoint && !m_GraphAnalyzer.UncheckableNodes.Contains(gn))
+ m_GraphAnalyzer.UncheckableNodes.Add(gn);
+ }
+ MakeLoopExitUncheckable(last.LoopExitNodes);
+ }
+ else
+ {
+ foreach (Loop c in l.NestedLoops) m_AbstractLoopUnrolling(c, l, prefix, false);
+ m_AbstractLoop(l);
+ //MakeLoopExitUncheckable(l.LoopExitNodes);
+ }
+ }
+
+ // the loop exit has to be marked uncheckable because otherwise
+ // while(true) would report unreachable code.
+ private void m_MarkLoopExitUncheckable(Loop l)
+ {
+
+ foreach (GraphNode g in l.Cutpoint.Suc)
+ {
+ if (!l.LoopNodes.Contains(g))
+ {
+ foreach (GraphNode g_ in m_MarkLoopExitUncheckable(g, l))
+ {
+ if (!m_GraphAnalyzer.UncheckableNodes.Contains(g_))
+ m_GraphAnalyzer.UncheckableNodes.Add(g_);
+ }
+ }
+ }
+ }
+
+ private List<GraphNode> m_MarkLoopExitUncheckable(GraphNode g, Loop l)
+ {
+ List<GraphNode> ret = new List<GraphNode>();
+
+ if (g.Pre.Count > 1) return ret;
+ ret.Add(g);
+ foreach (GraphNode gn in g.Suc)
+ {
+ ret.AddRange(m_MarkLoopExitUncheckable(gn, l));
+ }
+
+ return ret;
+ }
+
+ // to avoid problems with unreachable code after while(true) {}, try to make the loopexit nodes uncheckable.
+ private void MakeLoopExitUncheckable(List<GraphNode> le)
+ {
+ foreach (GraphNode gn in le)
+ {
+ if (gn.Suc.Count==1) m_GraphAnalyzer.UncheckableNodes.Add(gn);
+ }
+ }
+
+ private void m_RemoveRegularLoopExit(Loop l)
+ {
+ List<GraphNode> lg = new List<GraphNode>();
+ lg.AddRange( l.Cutpoint.Suc );
+ foreach (GraphNode gn in lg)
+ {
+ if (l.LoopExitNodes.Contains(gn))
+ {
+ l.Cutpoint.RemoveEdgeTo(gn);
+ l.LoopExitNodes.Remove(gn);
+ }
+ }
+ }
+
+ private void m_ReplaceBackEdge(Loop l, GraphNode loopSkip)
+ {
+
+ foreach (GraphNode gn in l.Cutpoint.LoopingPred)
+ {
+ List<GraphNode> newsuc = new List<GraphNode>();
+ foreach (GraphNode s in gn.Suc)
+ {
+ if (s == l.Cutpoint) newsuc.Add(loopSkip);
+ else newsuc.Add(s);
+ }
+ gn.Suc = newsuc;
+ }
+ }
+
+
+ }
+ #endregion
+
+ #region Graph Analyzer
+ internal class GraphAnalyzer
+ {
+ public List<GraphNode> UncheckableNodes = new List<GraphNode>();
+
+ public Dictionary<Block, GraphNode> GraphMap = new Dictionary<Block, GraphNode>();
+
+ public List<Loop> Graphloops = null;
+
+ public GraphAnalyzer(List<Block> blocks)
+ {
+ //ExitBlock = dedicatedExitBlock;
+ if (blocks.Count < 1) return;
+ foreach (Block b in blocks) GraphMap[b] = new GraphNode(b);
+ foreach (Block b in blocks)
+ {
+ foreach (Block pre in b.Predecessors) GraphMap[b].Pre.Add(GraphMap[pre]);
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (gc != null)
+ {
+ foreach (Block suc in gc.labelTargets) GraphMap[b].Suc.Add(GraphMap[suc]);
+ }
+ }
+ m_DetectCutPoints(GraphMap[blocks[0]], null, new List<GraphNode>());
+ Graphloops = m_CollectLoops(GraphMap[blocks[0]], null);
+ }
+
+ public List<Block> ToImplementation(out List<Block> uncheckables)
+ {
+ List<Block> blocks = new List<Block>();
+ uncheckables = new List<Block>();
+
+ foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap)
+ {
+ Block b = kvp.Key;
+ if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b);
+ blocks.Add(b);
+ b.Predecessors = new BlockSeq();
+ foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);
+ if (kvp.Value.Suc.Count > 0)
+ {
+ BlockSeq bs = new BlockSeq();
+ foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label);
+ b.TransferCmd = new GotoCmd(b.tok, bs);
+ }
+ else
+ {
+ b.TransferCmd = new ReturnCmd(b.tok);
+ }
+ }
+
+ return blocks;
+ }
+
+ public GraphNode CloneGraphNode(GraphNode gn, string prefix)
+ {
+ CmdSeq cmds = new CmdSeq(gn.Label.Cmds);
+
+ Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd);
+ GraphNode clone = new GraphNode(b);
+ clone.IsCutpoint = gn.IsCutpoint;
+ clone.Suc.AddRange(gn.Suc);
+ clone.Pre.AddRange(gn.Pre);
+ clone.LoopingPred.AddRange(gn.LoopingPred);
+ GraphMap[b] = clone;
+ //if (gn.Label == ExitBlock) ExitBlock = b;
+ return clone;
+ }
+
+ public void DeleteGraphNode(GraphNode gn)
+ {
+ List<Block> affected = new List<Block>();
+
+ foreach (KeyValuePair<Block, GraphNode> kvp in GraphMap)
+ {
+ if (kvp.Value == gn && !affected.Contains(kvp.Key)) affected.Add(kvp.Key);
+ }
+ foreach (Block b in affected)
+ {
+ GraphMap.Remove(b);
+ }
+ }
+
+ private void m_DetectCutPoints(GraphNode gn, GraphNode pred, List<GraphNode> visited )
+ {
+ if (visited.Contains(gn) )
+ {
+ if (pred != null && !gn.LoopingPred.Contains(pred)) gn.LoopingPred.Add(pred);
+ gn.IsCutpoint = true;
+ return;
+ }
+ else
+ {
+ List<GraphNode> visited_ = new List<GraphNode>();
+ visited_.AddRange(visited);
+ visited_.Add(gn);
+ foreach (GraphNode next in gn.Suc)
+ {
+ m_DetectCutPoints(next,gn,visited_);
+ }
+ }
+
+ }
+
+ private List<Loop> m_CollectLoops(GraphNode gn, Loop lastLoop)
+ {
+ List<Loop> ret = new List<Loop>();
+ List<GraphNode> loopingSucs = new List<GraphNode>();
+ if (gn.IsCutpoint)
+ {
+ Loop l = new Loop(gn);
+ if (lastLoop != null)
+ {
+ lastLoop.SucLoops.Add(l);
+ l.PreLoops.Add(lastLoop);
+ }
+ loopingSucs = l.LoopNodes;
+ lastLoop = l;
+ ret.Add(lastLoop);
+ }
+ foreach (GraphNode suc in gn.Suc)
+ {
+ if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop));
+ }
+ return ret;
+ }
+ }
+ #endregion
+
+ #region GraphNodeStructure
+ internal class GraphNode
+ {
+ public GraphNode(Block b)
+ {
+ Label = b; IsCutpoint = false;
+ }
+ public Block Label;
+ public List<GraphNode> Pre = new List<GraphNode>();
+ public List<GraphNode> Suc = new List<GraphNode>();
+ public bool IsCutpoint;
+ public bool Visited = false;
+ public List<GraphNode> LoopingPred = new List<GraphNode>();
+
+ public void AddEdgeTo(GraphNode other)
+ {
+ if (!this.Suc.Contains(other)) this.Suc.Add(other);
+ if (!other.Pre.Contains(this)) other.Pre.Add(this);
+ }
+
+ public void RemoveEdgeTo(GraphNode other)
+ {
+ if (this.Suc.Contains(other)) this.Suc.Remove(other);
+ if (other.Pre.Contains(this)) other.Pre.Remove(this);
+ }
+
+ }
+ #endregion
+
+ #region LoopStructure
+ internal class Loop
+ {
+ public Loop(GraphNode cutpoint)
+ {
+ if (!cutpoint.IsCutpoint)
+ {
+ Debugger.Break();
+ }
+ Cutpoint = cutpoint;
+ LoopNodes.Add(Cutpoint);
+ foreach (GraphNode gn in Cutpoint.LoopingPred)
+ {
+ CollectLoopBody(gn);
+ }
+ CollectLoopExitNodes();
+ }
+
+ // Copy Constructor
+ public Loop(Loop l, GraphAnalyzer ga, string prefix)
+ {
+
+ Dictionary<GraphNode, GraphNode> clonemap = new Dictionary<GraphNode, GraphNode>();
+ GraphNode clonecutpoint = null;
+ foreach (GraphNode gn in l.LoopNodes)
+ {
+ clonemap[gn] = ga.CloneGraphNode(gn, prefix);
+ if (gn == l.Cutpoint) clonecutpoint = clonemap[gn];
+ }
+
+ if (clonecutpoint == null)
+ {
+ Debugger.Break();
+ return;
+ }
+ // Replace the pre and post nodes by the corresponding clone
+ foreach (GraphNode gn in l.LoopNodes)
+ {
+ List<GraphNode> newl = new List<GraphNode>();
+ foreach (GraphNode g in clonemap[gn].Pre)
+ {
+ if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);
+ else newl.Add(g);
+ }
+ clonemap[gn].Pre = newl;
+ newl = new List<GraphNode>();
+ foreach (GraphNode g in clonemap[gn].Suc)
+ {
+ if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);
+ else newl.Add(g);
+ }
+ clonemap[gn].Suc = newl;
+ newl = new List<GraphNode>();
+ foreach (GraphNode g in clonemap[gn].LoopingPred)
+ {
+ if (clonemap.ContainsKey(g)) newl.Add(clonemap[g]);
+ else newl.Add(g);
+ }
+ clonemap[gn].LoopingPred = newl;
+ }
+
+ foreach (GraphNode gn in l.Cutpoint.LoopingPred)
+ {
+ clonecutpoint.LoopingPred.Remove(gn);
+ clonecutpoint.LoopingPred.Add(clonemap[gn]);
+ }
+
+
+
+ SucLoops.AddRange(l.SucLoops);
+ PreLoops.AddRange(l.PreLoops);
+ Cutpoint = clonecutpoint;
+ LoopNodes.Add(Cutpoint);
+ foreach (GraphNode gn in Cutpoint.LoopingPred)
+ {
+ CollectLoopBody(gn);
+ }
+ CollectLoopExitNodes();
+ }
+
+ private void CollectLoopBody(GraphNode gn)
+ {
+ if (gn == Cutpoint) return;
+ if (!LoopNodes.Contains(gn))
+ {
+ if (gn.IsCutpoint) // nested loop found
+ {
+ Loop lo = new Loop(gn);
+ foreach (GraphNode lgn in lo.LoopNodes)
+ {
+ if (!LoopNodes.Contains(lgn)) LoopNodes.Add(lgn);
+ }
+ NestedLoops.Add(lo);
+ }
+ else
+ {
+ LoopNodes.Add(gn);
+ }
+ foreach (GraphNode pre in gn.Pre) if (!gn.LoopingPred.Contains(pre)) CollectLoopBody(pre);
+ }
+ }
+
+ private void CollectLoopExitNodes()
+ {
+ foreach (GraphNode gn in LoopNodes)
+ {
+ foreach (GraphNode gn_ in gn.Suc)
+ {
+ if (!LoopNodes.Contains(gn_) && !LoopExitNodes.Contains(gn_)) LoopExitNodes.Add(gn_);
+ }
+ }
+ }
+
+ public GraphNode Cutpoint;
+ public List<GraphNode> LoopExitNodes = new List<GraphNode>();
+ public List<Loop> NestedLoops = new List<Loop>();
+ public List<Loop> SucLoops = new List<Loop>();
+ public List<Loop> PreLoops = new List<Loop>();
+ public List<GraphNode> LoopNodes = new List<GraphNode>();
+ }
+ #endregion
+
+ #endregion
+}
\ No newline at end of file diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/VCGeneration/DoomedStrategy.cs new file mode 100644 index 00000000..74ac0657 --- /dev/null +++ b/Source/VCGeneration/DoomedStrategy.cs @@ -0,0 +1,456 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+ #region SuperClass for different doomed code detection strategies
+ abstract internal class DoomDetectionStrategy
+ {
+ public int __DEBUG_BlocksChecked = 0;
+ public int __DEBUG_BlocksTotal = 0;
+ public int __DEBUG_InfeasibleTraces = 0;
+ public int __DEBUG_TracesChecked = 0;
+ public int __DEBUG_TracesTotal = 0;
+ public int __DEBUG_EQCTotal = 0;
+ public int __DEBUG_EQCLeaf = 0;
+ public int __DEBUG_EQCChecked = 0;
+
+ //Please use this one to toggle your Debug output
+ protected bool __DEBUGOUT = CommandLineOptions.Clo.DoomStrategy != -1;
+
+ protected Implementation impl;
+ protected BlockHierachy m_BlockH = null;
+
+ protected int m_MaxBranchingDepth = 0;
+ protected int m_MaxMinElemPerPath = 0;
+
+
+ // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to
+ // create an error message
+ public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();
+
+ // There is no default constructor, because these parameters are needed for most subclasses
+ public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
+ {
+ m_BlockH = new BlockHierachy(imp, unifiedexit);
+ __DEBUG_EQCLeaf = m_BlockH.Leaves.Count;
+
+ if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);
+ if (__DEBUGOUT)
+ {
+ Console.WriteLine("MaBranchingDepth {0} MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxMinElemPerPath);
+ double avgplen = 0, avglpp=0;
+ foreach (int i in __pathLength)
+ {
+ avgplen+=i;
+ }
+ foreach (int i in __leavespp)
+ {
+ avglpp += i;
+ }
+ avglpp = (__leavespp.Count > 0) ? avglpp / (double)__leavespp.Count : 1;
+ avgplen = (__pathLength.Count > 0) ? avgplen / (double)__pathLength.Count : 1;
+ Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", avglpp, avgplen);
+ }
+
+ MaxBlocks = imp.Blocks.Count;
+ MinBlocks = imp.Blocks.Count;
+ HACK_NewCheck = false;
+ __DEBUG_BlocksTotal = imp.Blocks.Count;
+ }
+
+
+ public int MaxBlocks, MinBlocks;
+ public bool HACK_NewCheck;
+
+ // This method is called by the prover while it returns true. The prover checks for each
+ // List lb if
+ // |= !lb_1 /\ ... /\ !lb_n => wlp(Program, false)
+ // and passes the result to SetCurrentResult
+ abstract public bool GetNextBlock(out List<Block> passBlock);
+
+ // This method is called to inform about the prover outcome for the previous GetNextBlock call.
+ abstract public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb);
+
+ protected List<Block> m_GetErrorTraceFromCE(DoomErrorHandler cb)
+ {
+ BlockHierachyNode tn=null;
+ List<Block> errortrace = new List<Block>();
+ foreach (Block b in cb.TraceNodes)
+ {
+ if (errortrace.Contains(b)) continue;
+ if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out tn))
+ {
+ foreach (Block b_ in tn.Unavoidable)
+ {
+ if (!errortrace.Contains(b_)) errortrace.Add(b_);
+ }
+ foreach (Block b_ in tn.Content)
+ {
+ if (!errortrace.Contains(b_)) errortrace.Add(b_);
+ }
+ }
+ }
+ return errortrace;
+ }
+
+ private List<int> __pathLength = new List<int>();
+ private List<int> __leavespp = new List<int>();
+ protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen)
+ {
+ if (b.Predecessors.Length > 1) branchingdepth--;
+
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ BlockHierachyNode bhn = null;
+ if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out bhn))
+ {
+ if (m_BlockH.Leaves.Contains(bhn)) leavespp++;
+ }
+ m_MaxMinElemPerPath = (leavespp > m_MaxMinElemPerPath) ? leavespp : m_MaxMinElemPerPath;
+ plen++;
+ if (gc != null)
+ {
+ if (gc.labelTargets.Length > 1) branchingdepth++;
+ m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth;
+ foreach (Block s in gc.labelTargets)
+ {
+ m_GatherInfo(s, branchingdepth, leavespp,plen);
+ }
+ }
+ else
+ {
+ __pathLength.Add(plen);
+ __leavespp.Add(leavespp);
+ }
+
+ }
+
+
+ }
+ #endregion
+
+ #region BruteForce Strategy
+ internal class NoStrategy : DoomDetectionStrategy
+ {
+ private List<Block> m_Blocks = new List<Block>();
+ private int m_Current = 0;
+
+ public NoStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
+ : base(imp, unifiedexit, unreach)
+ {
+ m_Blocks = imp.Blocks;
+ }
+
+ override public bool GetNextBlock(out List<Block> lb)
+ {
+ if (m_Current < m_Blocks.Count)
+ {
+ lb = new List<Block>();
+ lb.Add(m_Blocks[m_Current]);
+ m_Current++;
+ return true;
+ }
+ lb = null;
+ return false;
+ }
+
+ // This method is called to inform about the prover outcome for the previous GetNextBlock call.
+ override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)
+ {
+ this.__DEBUG_BlocksChecked++;
+ // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)
+ if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count)
+ {
+ List<Block> lb = new List<Block>();
+ lb.Add(m_Blocks[m_Current - 1]);
+ DetectedBlock.Add(lb);
+ }
+ return true;
+ }
+ }
+ #endregion
+
+ #region Only check the minimal elements of the Hasse diagram
+ internal class HierachyStrategy : DoomDetectionStrategy
+ {
+ private List<Block> m_Blocks = new List<Block>();
+ private List<Block> m_doomedBlocks = new List<Block>();
+ private int m_Current = 0;
+
+ public HierachyStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
+ : base(imp, unifiedexit, unreach)
+ {
+ foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
+ {
+ if (bhn.Content.Count > 0)
+ {
+ m_Blocks.Add(bhn.Content[0]);
+ }
+ }
+ }
+
+ override public bool GetNextBlock(out List<Block> lb)
+ {
+ if (m_Current < m_Blocks.Count)
+ {
+ lb = new List<Block>();
+ lb.Add(m_Blocks[m_Current]);
+ m_Current++;
+ return true;
+ }
+ else
+ {
+ DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks));
+ }
+ lb = null;
+ return false;
+ }
+
+ // This method is called to inform about the prover outcome for the previous GetNextBlock call.
+ override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)
+ {
+ this.__DEBUG_BlocksChecked++;
+ // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)
+ if (outcome == ProverInterface.Outcome.Valid && m_Current <= m_Blocks.Count)
+ {
+ m_doomedBlocks.Add(m_Blocks[m_Current - 1]);
+ }
+ return true;
+ }
+ }
+ #endregion
+
+ #region Only check the minimal elements of the Hasse diagram and use CEs
+ internal class HierachyCEStrategy : DoomDetectionStrategy
+ {
+ private List<Block> m_Blocks = new List<Block>();
+ private List<Block> m_doomedBlocks = new List<Block>();
+ private Block m_Current = null;
+
+ public HierachyCEStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
+ : base(imp, unifiedexit, unreach)
+ {
+ foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
+ {
+ if (bhn.Content.Count > 0)
+ {
+ m_Blocks.Add(bhn.Content[0]);
+ }
+ }
+ }
+
+ override public bool GetNextBlock(out List<Block> lb)
+ {
+ m_Current = null;
+ if (m_Blocks.Count > 0)
+ {
+ m_Current = m_Blocks[0];
+ m_Blocks.Remove(m_Current);
+ lb = new List<Block>();
+ lb.Add(m_Current);
+ return true;
+ }
+ else
+ {
+ DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_doomedBlocks));
+ }
+ lb = null;
+ return false;
+ }
+
+ // This method is called to inform about the prover outcome for the previous GetNextBlock call.
+ override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)
+ {
+ this.__DEBUG_BlocksChecked++;
+ // outcome==Valid means that there is no feasible execution for the current block/path (i.e., might be doomed)
+ if (outcome == ProverInterface.Outcome.Valid && m_Current != null)
+ {
+ m_doomedBlocks.Add(m_Current);
+ }
+ else if (outcome == ProverInterface.Outcome.Invalid)
+ {
+ List<Block> errortrace = m_GetErrorTraceFromCE(cb);
+ foreach (Block b in errortrace)
+ {
+ if (m_Blocks.Contains(b))
+ {
+ m_Blocks.Remove(b);
+ }
+ }
+ cb.TraceNodes.Clear();
+ }
+ return true;
+ }
+ }
+ #endregion
+
+ #region Path Cover Optimization
+ internal class PathCoverStrategy : DoomDetectionStrategy
+ {
+ List<Block> m_Uncheckedlocks = new List<Block>();
+ List<Block> m_Ignore = new List<Block>();
+
+ Random m_Random = new Random();
+ bool m_NoMoreMoves = false;
+
+ private List<Block> m_foundBlock = new List<Block>();
+
+ public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)
+ : base(imp, unifiedexit, unreach)
+ {
+ m_Ignore = unreach;
+ HACK_NewCheck = true;
+ impl = imp;
+ foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
+ {
+ //foreach (Block b in h.Content)
+ //{
+ // m_Uncheckedlocks.Add(b);
+ //}
+ if (bhn.Content.Count > 0)
+ {
+ m_Uncheckedlocks.Add(bhn.Content[0]);
+ }
+
+ }
+ MaxBlocks = m_Uncheckedlocks.Count;
+ }
+
+ public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach, bool test_alternativeK)
+ : base(imp, unifiedexit, unreach)
+ {
+ m_Ignore = unreach;
+ HACK_NewCheck = true;
+ impl = imp;
+ foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
+ {
+ //foreach (Block b in h.Content)
+ //{
+ // m_Uncheckedlocks.Add(b);
+ //}
+ if (bhn.Content.Count > 0)
+ {
+ m_Uncheckedlocks.Add(bhn.Content[0]);
+ }
+
+ }
+ MaxBlocks = m_Uncheckedlocks.Count;
+ if (test_alternativeK)
+ {
+ m_CountUncheckedPP(impl.Blocks[0], 0);
+ if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0)
+ {
+ MaxBlocks = m_MaxK;
+ }
+ else if (m_MaxK >= m_Uncheckedlocks.Count)
+ {
+ MaxBlocks = m_Uncheckedlocks.Count;
+ }
+ else
+ {
+ MaxBlocks = 1;
+ }
+ Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks);
+ }
+ }
+
+ int m_MaxK = 0;
+
+ private void m_CountUncheckedPP(Block b, int localmax)
+ {
+ if (m_Uncheckedlocks.Contains(b)) localmax++;
+
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (gc != null && gc.labelTargets.Length>0)
+ {
+ foreach (Block s in gc.labelTargets)
+ {
+ m_CountUncheckedPP(s, localmax);
+ }
+ }
+ else
+ {
+ m_MaxK = (localmax > m_MaxK) ? localmax : m_MaxK;
+ }
+
+ }
+
+ override public bool GetNextBlock(out List<Block> lb)
+ {
+ lb = new List<Block>();
+
+ if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)
+ {
+ if (m_Uncheckedlocks.Count > 0)
+ {
+ DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks));
+ }
+
+ return false;
+ }
+
+ lb.AddRange(m_Uncheckedlocks);
+ MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks;
+ MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0);
+
+ return true;
+ }
+
+ override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)
+ {
+ this.__DEBUG_BlocksChecked++;
+ //Console.WriteLine(outcome);
+ // Valid means infeasible...
+ if (outcome == ProverInterface.Outcome.Valid)
+ {
+ this.__DEBUG_InfeasibleTraces++;
+ if (MaxBlocks == 1)
+ {
+ m_NoMoreMoves = true;
+ }
+ else
+ {
+ MaxBlocks /= 2;
+ }
+ }
+ else if (outcome == ProverInterface.Outcome.Invalid)
+ {
+ this.__DEBUG_TracesChecked++;
+ //int oldsize = m_Uncheckedlocks.Count;
+ List<Block> errortrace = m_GetErrorTraceFromCE(cb);
+ foreach (Block b in errortrace)
+ {
+ if (m_Uncheckedlocks.Contains(b))
+ {
+ m_Uncheckedlocks.Remove(b);
+ }
+ }
+ cb.TraceNodes.Clear();
+ }
+ else
+ {
+ m_NoMoreMoves = true; m_Uncheckedlocks.Clear();
+ }
+ return true;
+ }
+
+
+ }
+ #endregion
+
+}
\ No newline at end of file diff --git a/Source/VCGeneration/HasseDiagram.cs b/Source/VCGeneration/HasseDiagram.cs new file mode 100644 index 00000000..144d70e5 --- /dev/null +++ b/Source/VCGeneration/HasseDiagram.cs @@ -0,0 +1,368 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Graphing;
+using AI = Microsoft.AbstractInterpretationFramework;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+ internal class BlockHierachyNode
+ {
+ public List<Block> Unavoidable;
+ public List<Block> Content = new List<Block>();
+ public List<BlockHierachyNode> Parents = new List<BlockHierachyNode>();
+ public List<BlockHierachyNode> Children = new List<BlockHierachyNode>();
+
+ public bool Checked, Doomed, DoubleChecked;
+
+ public BlockHierachyNode(Block current, List<Block> unavoidable)
+ {
+ Checked = false; Doomed = false; DoubleChecked = false;
+ Unavoidable = unavoidable;
+ Content.Add(current);
+ }
+
+ public static bool operator <(BlockHierachyNode left, BlockHierachyNode right)
+ {
+ return Compare(left,right)>0;
+ }
+
+ public static bool operator >(BlockHierachyNode left, BlockHierachyNode right)
+ {
+ return Compare(left, right) < 0;
+ }
+
+ // Compare the unavoidable blocks of two BlockHierachyNodes.
+ // returns 0 if sets have the same size, -1 if l2 has an element
+ // that is not in l1, otherwise the size of the intersection.
+ public static int Compare(BlockHierachyNode l1, BlockHierachyNode l2)
+ {
+ List<Block> tmp = new List<Block>();
+ tmp.AddRange(l2.Unavoidable);
+ foreach (Block b in l1.Unavoidable)
+ {
+ if (tmp.Contains(b)) tmp.Remove(b);
+ else return -1;
+ }
+ return tmp.Count;
+ }
+ }
+
+ internal class HasseDiagram
+ {
+ public readonly List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();
+ public readonly List<BlockHierachyNode> Roots = new List<BlockHierachyNode>();
+
+ public HasseDiagram(List<BlockHierachyNode> nodes)
+ {
+ Dictionary<BlockHierachyNode, List<BlockHierachyNode>> largerElements = new Dictionary<BlockHierachyNode, List<BlockHierachyNode>>();
+ foreach (BlockHierachyNode left in nodes)
+ {
+ largerElements[left] = new List<BlockHierachyNode>();
+ foreach (BlockHierachyNode right in nodes)
+ {
+ if (left != right)
+ {
+ if (left < right)
+ {
+ largerElements[left].Add(right);
+ }
+ }
+ }
+ if (largerElements[left].Count == 0) Leaves.Add(left);
+ }
+
+ List<BlockHierachyNode> done = new List<BlockHierachyNode>();
+ List<BlockHierachyNode> lastround = null;
+
+ //Debugger.Break();
+
+ // Now that we have the leaves, build the Hasse diagram
+ while (done.Count < nodes.Count)
+ {
+ List<BlockHierachyNode> maxelements = new List<BlockHierachyNode>();
+ maxelements.AddRange(nodes);
+ foreach (BlockHierachyNode bhn in nodes)
+ {
+ if (!done.Contains(bhn))
+ {
+ foreach (BlockHierachyNode tmp in largerElements[bhn])
+ {
+ if (maxelements.Contains(tmp)) maxelements.Remove(tmp);
+ }
+ }
+ else
+ {
+ maxelements.Remove(bhn);
+ }
+ }
+
+ done.AddRange(maxelements);
+
+ if (lastround != null)
+ {
+ foreach (BlockHierachyNode tmp in lastround)
+ {
+ foreach (BlockHierachyNode tmp2 in maxelements)
+ {
+ if (largerElements[tmp].Contains(tmp2))
+ {
+ if (!tmp.Children.Contains(tmp2)) tmp.Children.Add(tmp2);
+ if (!tmp2.Parents.Contains(tmp)) tmp2.Parents.Add(tmp);
+ }
+ }
+ }
+ }
+ else
+ {
+ Roots.AddRange(maxelements);
+ }
+ lastround = maxelements;
+ }
+ }
+
+
+ }
+
+ internal class BlockHierachy
+ {
+ public BlockHierachyNode RootNode = null;
+ readonly public Dictionary<Block, BlockHierachyNode> BlockToHierachyMap = new Dictionary<Block, BlockHierachyNode>();
+ readonly public Dictionary<Block, List<Block>> Dominators = new Dictionary<Block, List<Block>>();
+ readonly public Dictionary<Block, List<Block>> PostDominators = new Dictionary<Block, List<Block>>();
+ readonly public List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();
+
+ public BlockHierachy(Implementation impl, Block unifiedExit)
+ {
+ List<Block> blocks = impl.Blocks;
+ List<BlockHierachyNode> tmp_hnodes = new List<BlockHierachyNode>();
+ Dictionary<Block, List<Block>> unavoidable = new Dictionary<Block, List<Block>>();
+
+ BfsTraverser(blocks[0], true, Dominators);
+ BfsTraverser(unifiedExit, false, PostDominators);
+
+ foreach (Block b in blocks)
+ {
+ List<Block> l1 = Dominators[b];
+ List<Block> l2 = PostDominators[b];
+ unavoidable[b] = m_MergeLists(l1, l2);
+
+ BlockHierachyNode bhn = new BlockHierachyNode(b, unavoidable[b]);
+ bool found = false;
+ foreach (KeyValuePair<Block, BlockHierachyNode> kvp in BlockToHierachyMap)
+ {
+ if (BlockHierachyNode.Compare(kvp.Value, bhn) == 0) // using the overloaded compare operator
+ {
+ kvp.Value.Content.AddRange(bhn.Content);
+ BlockToHierachyMap[b] = kvp.Value;
+ found = true;
+ break;
+ }
+ }
+ if (!found)
+ {
+ BlockToHierachyMap[b] = bhn;
+ tmp_hnodes.Add(bhn);
+ }
+ }
+
+ HasseDiagram hd = new HasseDiagram(tmp_hnodes);
+ Leaves = hd.Leaves;
+ }
+
+ public List<Block> GetOtherDoomedBlocks(List<Block> doomedblocks)
+ {
+ List<Block> alsoDoomed = new List<Block>();
+ List<BlockHierachyNode> todo = new List<BlockHierachyNode>();
+ foreach (Block b in doomedblocks)
+ {
+ BlockToHierachyMap[b].Doomed = true;
+ todo.Add(BlockToHierachyMap[b]);
+ }
+
+ while (todo.Count > 0)
+ {
+ BlockHierachyNode current = todo[0];
+ todo.Remove(current);
+ if (!current.Doomed && current.Children.Count > 0)
+ {
+ bool childrenDoomed = true;
+ foreach (BlockHierachyNode c in current.Children)
+ {
+ if (!c.Doomed) { childrenDoomed = false; break; }
+ }
+ if (childrenDoomed) current.Doomed = true;
+ }
+
+ if (current.Doomed)
+ {
+ foreach (BlockHierachyNode p in current.Parents)
+ {
+ if (!todo.Contains(p)) todo.Add(p);
+ }
+ foreach (Block b in current.Content)
+ {
+ if (!alsoDoomed.Contains(b)) alsoDoomed.Add(b);
+ }
+ }
+ }
+
+ return alsoDoomed;
+ }
+
+ public void Impl2Dot(string filename)
+ {
+
+ Contract.Requires(filename != null);
+ List<string> nodes = new List<string>();
+ List<string> edges = new List<string>();
+
+ string nodestyle = "[shape=box];";
+
+ List<BlockHierachyNode> nl = new List<BlockHierachyNode>();
+ foreach (BlockHierachyNode h in BlockToHierachyMap.Values) if (!nl.Contains(h)) nl.Add(h);
+
+
+ foreach (BlockHierachyNode b in nl)
+ {
+ String l1 = "";
+ foreach (Block bl in b.Content) l1 = String.Format("{0}_{1}", l1, bl.Label);
+
+ Contract.Assert(b != null);
+ nodes.Add(string.Format("\"{0}\" {1}", l1, nodestyle));
+ foreach (BlockHierachyNode b_ in b.Children)
+ {
+
+ String l2 = "";
+ foreach (Block bl in b_.Content) l2 = String.Format("{0}_{1}", l2, bl.Label);
+ edges.Add(String.Format("\"{0}\" -> \"{1}\";", l1, l2));
+ }
+
+ }
+
+ using (StreamWriter sw = new StreamWriter(filename))
+ {
+ sw.WriteLine(String.Format("digraph {0} {{", "DISCO"));
+ // foreach (string! s in nodes) {
+ // sw.WriteLine(s);
+ // }
+ foreach (string s in edges)
+ {
+ Contract.Assert(s != null);
+ sw.WriteLine(s);
+ }
+ sw.WriteLine("}}");
+ sw.Close();
+ }
+ }
+
+ private void BfsTraverser(Block current, bool forward, Dictionary<Block, List<Block>> unavoidableBlocks)
+ {
+ List<Block> todo = new List<Block>();
+ List<Block> done = new List<Block>();
+ unavoidableBlocks[current] = new List<Block>();
+ //Debugger.Break();
+ todo.Add(current);
+ while (todo.Count > 0)
+ {
+ current = todo[0];
+ todo.Remove(current);
+ BlockSeq pre = m_Predecessors(current, forward);
+ bool ready = true;
+ if (pre != null)
+ {
+ foreach (Block bpre in pre)
+ {
+ if (!done.Contains(bpre))
+ {
+ ready = false;
+ break;
+ }
+ }
+ }
+ if (!ready)
+ {
+ todo.Add(current);
+ continue;
+ }
+ done.Add(current);
+ unavoidableBlocks[current].Add(current);
+
+ BlockSeq suc = m_Succecessors(current, forward);
+ if (suc == null) continue;
+ foreach (Block bsuc in suc)
+ {
+ if (unavoidableBlocks.ContainsKey(bsuc))
+ {
+ unavoidableBlocks[bsuc] = m_IntersectLists(unavoidableBlocks[bsuc], unavoidableBlocks[current]);
+ }
+ else
+ {
+ todo.Add(bsuc);
+ unavoidableBlocks[bsuc] = new List<Block>();
+ unavoidableBlocks[bsuc].AddRange(unavoidableBlocks[current]);
+ }
+
+ }
+ }
+
+ }
+
+ private List<Block> m_MergeLists(List<Block> lb1, List<Block> lb2)
+ {
+ List<Block> ret = new List<Block>();
+ ret.AddRange(lb1);
+ foreach (Block b in lb2)
+ {
+ if (!ret.Contains(b)) ret.Add(b);
+ }
+ return ret;
+ }
+
+ private List<Block> m_IntersectLists(List<Block> lb1, List<Block> lb2)
+ {
+ List<Block> ret = new List<Block>();
+ ret.AddRange(lb1);
+ foreach (Block b in lb2)
+ {
+ if (!lb1.Contains(b)) ret.Remove(b);
+ }
+ foreach (Block b in lb1)
+ {
+ if (ret.Contains(b) && !lb2.Contains(b)) ret.Remove(b);
+ }
+ return ret;
+ }
+
+ private BlockSeq m_Predecessors(Block b, bool forward)
+ {
+ if (forward) return b.Predecessors;
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (gc != null)
+ {
+ return gc.labelTargets;
+ }
+ return null;
+ }
+
+ private BlockSeq m_Succecessors(Block b, bool forward)
+ {
+ return m_Predecessors(b, !forward);
+ }
+
+
+ }
+
+}
\ No newline at end of file diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 8a9e13ff..f3517d60 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -20,7 +20,7 @@ namespace VC { using Bpl = Microsoft.Boogie;
public class VCGen : ConditionGeneration {
-
+ private const bool _print_time = false;
/// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
@@ -1587,10 +1587,17 @@ namespace VC { Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
- }
-
- callback.OnProgress("VCgen", 0, 0, 0.0);
+ }
+ callback.OnProgress("VCgen", 0, 0, 0.0);
+
+ Stopwatch watch = new Stopwatch();
+ if (_print_time)
+ {
+ Console.WriteLine("Checking function {0}", impl.Name);
+ watch.Reset();
+ watch.Start();
+ }
ConvertCFG2DAG(impl, program);
SmokeTester smoke_tester = null;
@@ -1741,6 +1748,12 @@ namespace VC { callback.OnProgress("done", 0, 0, 1.0);
+ if (_print_time)
+ {
+ watch.Stop();
+ Console.WriteLine("Total time for this method: {0}", watch.Elapsed.ToString());
+ }
+
return outcome;
}
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 950c0158..805eb84f 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -17,7 +17,8 @@ using Microsoft.Basetypes; using Microsoft.Boogie.VCExprAST;
namespace VC {
- public class DCGen : ConditionGeneration {
+ public partial class DCGen : ConditionGeneration {
+ private bool _print_time = CommandLineOptions.Clo.DoomStrategy!=-1;
#region Attributes
static private Dictionary<Block, Variable/*!*/>/*!*/ m_BlockReachabilityMap;
Dictionary<Block/*!*/, Block/*!*/>/*!*/ m_copiedBlocks = new Dictionary<Block/*!*/, Block/*!*/>();
@@ -25,13 +26,12 @@ namespace VC { List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>();
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullDictionaryAndValues(m_BlockReachabilityMap));
- Contract.Invariant(cce.NonNullDictionaryAndValues(m_copiedBlocks));
- Contract.Invariant(cce.NonNullElements(m_doomedCmds));
- Contract.Invariant(cce.NonNullElements(_copiedBlock));
+
}
#endregion
+
+
/// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
@@ -89,200 +89,8 @@ namespace VC { sw.Close();
}
}
-
private const string _copyPrefix = "CPY__";
- private Block CopyImplBlocks(Block b, ref List<Block> blocklist, Block targetBlock, ref Dictionary<Block, Block> alreadySeen) {
- Contract.Requires(b != null);
- Contract.Requires(targetBlock != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(alreadySeen));
- Contract.Requires(blocklist != null);
- Contract.Ensures(Contract.ValueAtReturn(out blocklist) != null);
- Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.ValueAtReturn(out alreadySeen)));
- Contract.Ensures(Contract.Result<Block>() != null);
-
- Block seen;
- if (alreadySeen.TryGetValue(b, out seen)) {
- Contract.Assert(seen != null);
- return seen;
- }
-
- GotoCmd gc = b.TransferCmd as GotoCmd;
- TransferCmd tcmd = null;
- if (gc != null) {
- BlockSeq bseq = new BlockSeq();
- Contract.Assert(gc.labelTargets != null);
- foreach (Block c in gc.labelTargets) {
- Contract.Assert(c != null);
- bseq.Add(CopyImplBlocks(c, ref blocklist, targetBlock, ref alreadySeen));
- }
- tcmd = new GotoCmd(gc.tok, bseq);
- } else {
- // BlockSeq! bseq_ = new BlockSeq();
- // bseq_.Add(targetBlock);
- Contract.Assert(b.TransferCmd != null);
- // tcmd = new GotoCmd(b.TransferCmd.tok, bseq_);
- tcmd = new ReturnCmd(b.TransferCmd.tok);
- }
-
- CodeCopier codeCopier = new CodeCopier();
- CmdSeq cl = new CmdSeq();
- foreach (Cmd _c in b.Cmds) {
- Contract.Assert(_c != null);
- if (!ContainsReachVariable(_c))
- cl.Add(codeCopier.CopyCmd(_c));
- }
-
- Block b_ = new Block(b.tok, b.Label + _copyPrefix, cl, tcmd);
- Contract.Assert(b_ != null);
- blocklist.Add(b_);
-
- alreadySeen[b] = b_;
-
- return b_;
- }
-
- /*
- After adding a copy of the implementation in front of our code
- we remove all the edges leading from the copy to the original code
- */
- private void RemoveArtificialGoto(Block b, Block target) {
- Contract.Requires(b != null);
- Contract.Requires(target != null);
- GotoCmd gc = b.TransferCmd as GotoCmd;
-
- if (gc != null) {
- Contract.Assert(gc.labelTargets != null);
- foreach (Block gt in gc.labelTargets) {
- Contract.Assert(gt != null);
- if (gt == target) {
- Contract.Assert(gc.labelTargets.Length == 1);
- Contract.Assert(gc.labelTargets[0] != null);
- b.TransferCmd = new ReturnCmd(gc.tok);
- return;
- } else {
- RemoveArtificialGoto(gt, target);
- }
- }
-
- }
- }
-
- static public bool UseItAsDebugger = false;
-
- public static Block firstNonDebugBlock = null;
- public static Block firstDebugBlock = null;
-
- private void ModifyImplForDebugging(Implementation impl) {
- Contract.Requires(impl != null);
- //List<Block!> backup_blocks=null;
-
-
- if (UseItAsDebugger) {
- #region Copy the Implementation /////////////////////
-
- ConsoleColor col = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Magenta;
- Console.WriteLine("Warning you are using the Infinite Improbability Drive!");
- Console.ForegroundColor = col;
-
- List<Block/*!*/>/*!*/ blist = new List<Block/*!*/>();
- Dictionary<Block, Block> tmpdict = new Dictionary<Block, Block>();
- CopyImplBlocks(impl.Blocks[0], ref blist, impl.Blocks[0], ref tmpdict);
- blist.Reverse();
- //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);
-
- #endregion ////////////////////////////////////
-
- #region Add implementation copy in front of implementation
- // memorize where the original code starts
- firstNonDebugBlock = impl.Blocks[0];
- firstDebugBlock = blist[0];
- // now add the copied program in front of the original one
- blist.AddRange(impl.Blocks);
- //backup_blocks = new List<Block!>(impl.Blocks);
-
- BlockSeq newbseq = new BlockSeq();
- newbseq.Add(firstNonDebugBlock);
- newbseq.Add(firstDebugBlock);
-
- GotoCmd newtcmd = new GotoCmd(Token.NoToken, newbseq);
- Block newfirst = new Block(Token.NoToken, "MySuperFirstBlock", new CmdSeq(), newtcmd);
-
-
- impl.Blocks = new List<Block>();
- impl.Blocks.Add(newfirst);
- impl.Blocks.AddRange(blist);
-
- //Impl2Dot(impl, String.Format("c:/dot/{0}_copied.dot", impl.Name) );
- #endregion
- }
- }
-
- void RemoveReachVars(Block b) {
- Contract.Requires(b != null);
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc != null) {
- CmdSeq cs = new CmdSeq();
- foreach (Cmd c in b.Cmds) {
- Contract.Assert(c != null);
- if (!ContainsReachVariable(c))
- cs.Add(c);
- }
- b.Cmds = cs;
-
- foreach (Block c in gc.labelTargets) {
- Contract.Assert(c != null);
- if (c.Label != "GeneratedUnifiedExit") {
- RemoveReachVars(c);
- }
- }
- }
- }
-
- void RemoveLastBlock(Block b) {
- Contract.Requires(b != null);
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc == null) {
- //Console.WriteLine("WARNING: Check Node {0}", b.Label);
- return;
- }
- Contract.Assert(gc != null);
- Contract.Assert(gc.labelTargets != null);
- BlockSeq tmp = new BlockSeq();
- foreach (Block c in gc.labelTargets) {
- Contract.Assert(c != null);
- // Warning, we should not search by name!
- if (c.Label != "GeneratedUnifiedExit") {
- tmp.Add(c);
- RemoveLastBlock(c);
- } else {
- c.Predecessors.Remove(b);
- }
- }
- if (tmp.Length == 0) {
- b.TransferCmd = new ReturnCmd(gc.tok);
- } else {
- b.TransferCmd = new GotoCmd(gc.tok, tmp);
- }
- }
-
- void FindCopiedBlocks(Block b) {
- Contract.Requires(b != null);
- _copiedBlock.Add(b);
- GotoCmd gc = b.TransferCmd as GotoCmd;
- if (gc != null) {
- Contract.Assert(gc.labelTargets != null);
- foreach (Block c in gc.labelTargets) {
- Contract.Assert(c != null);
- FindCopiedBlocks(c);
- }
- }
- }
-
- private List<Block> _copiedBlock = new List<Block>();
-
-
/// <summary>
/// Helperfunction to restore the predecessor relations after loop unrolling
/// </summary>
@@ -298,7 +106,9 @@ namespace VC { }
}
- /// <summary>
+ private List<Block> m_UncheckableBlocks = null;
+
+ /// <summary>
/// MSchaef:
/// - remove loops and add reach variables
/// - make it a passive program
@@ -311,170 +121,139 @@ namespace VC { //Contract.Requires(program != null);
//Contract.Requires(callback != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;
+
Stopwatch watch = new Stopwatch();
- if (CommandLineOptions.Clo.TraceVerify) {
- Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
- }
- Console.WriteLine("Checking function {0} for doomed points:", impl.Name);
+ Console.WriteLine();
+ Console.WriteLine("Checking function {0}", impl.Name);
callback.OnProgress("doomdetector", 0, 0, 0);
watch.Reset();
watch.Start();
- #region Transform the Program into loop-free passive form
- variable2SequenceNumber = new Hashtable/*Variable -> int*/();
- incarnationOriginMap = new Dictionary<Incarnation, Absy>();
-
- //List<Block!>! orig_blocks = new List<Block!>(impl.Blocks);
-
-// Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
- impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program);
-
- if (UseItAsDebugger)
- ModifyImplForDebugging(impl);
- // Impl2Dot(impl, String.Format("c:/dot/{0}_lf.dot", impl.Name));
-
- ClearPredecessors(impl.Blocks);
- ComputePredecessors(impl.Blocks);
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
- if (UseItAsDebugger)
- RemoveReachVars(cce.NonNull(firstDebugBlock));
-
- GenerateHelperBlocks(impl);
- m_BlockReachabilityMap = new Dictionary<Block, Variable>();
- AssumeCmd finalAssume = GenerateReachabilityPredicates(impl);
- this.exitBlock.Cmds.Add(finalAssume);
-
- ClearPredecessors(impl.Blocks);
- ComputePredecessors(impl.Blocks);
-
- PassifyProgram(impl, new ModelViewInfo(program, impl));
- #endregion
- //EmitImpl(impl,false);
+ Transform4DoomedCheck(impl, program);
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
- // ---------------------------------------------------------------------------
- if (UseItAsDebugger) {
- Contract.Assert(firstNonDebugBlock != null && firstDebugBlock != null);
- firstNonDebugBlock.Predecessors.Remove(impl.Blocks[0]);
- firstDebugBlock.Predecessors.Remove(impl.Blocks[0]);
- // impl.Blocks.Remove(impl.Blocks[0]); // remove the artificial first block
- RemoveLastBlock(firstDebugBlock); // remove the goto to the unified exit
- _copiedBlock.Clear();
- FindCopiedBlocks(firstDebugBlock);
- }
- // ---------------------------------------------------------------------------
-
- // EmitImpl(impl,false);
-
- //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );
-
- bool __debug = false;
-
- watch.Stop();
- if (__debug)
- Console.WriteLine("Transformation takes: {0}", watch.Elapsed.ToString());
- watch.Reset();
-
+
Checker checker = FindCheckerFor(impl, 1000);
Contract.Assert(checker != null);
+ DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks);
- DoomCheck dc = new DoomCheck(impl, checker);
-
+ //EmitImpl(impl, false);
+
int _totalchecks = 0;
- Block b = null;
+
ProverInterface.Outcome outcome;
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
+ watch.Stop();
+ watch.Reset();
+
System.TimeSpan ts = watch.Elapsed;
+
+ if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count);
- while (dc.GetNextBlock(out b)) {
- Contract.Assert(b != null);
+ List<Block> lb;
+ List<Variable> lv = new List<Variable>();
+
+ while (dc.GetNextBlock(out lb))
+ {
+ Contract.Assert(lb != null);
outcome = ProverInterface.Outcome.Undetermined;
- //Console.WriteLine("Checking block {0} ...",b.Label);
+
Variable v = null;
- if (!m_BlockReachabilityMap.TryGetValue(b, out v)) {
+ lv.Clear();
+
+ foreach (Block b_ in lb)
+ {
+ if (!m_BlockReachabilityMap.TryGetValue(b_, out v))
+ {
+ // This should cause an error
+ continue;
+ }
+ //Console.Write("{0}, ",b_.Label);
+ lv.Add(v);
+ }
+ //Console.WriteLine();
+ Dictionary<Expr, int> finalreachvars = m_GetPostconditionVariables(impl.Blocks,lb);
+ if (lv.Count < 1)
+ {
+ continue;
}
- Contract.Assert(v != null);
+
+ Contract.Assert(lv != null);
_totalchecks++;
- watch.Start();
- if (!dc.CheckLabel(v, out outcome)) {
+ watch.Start();
+ if (!dc.CheckLabel(lv,finalreachvars, out outcome)) {
return Outcome.Inconclusive;
}
watch.Stop();
ts += watch.Elapsed;
- if (__debug)
- Console.WriteLine(" Time for Block {0}: {1} elapsed", b.Label, watch.Elapsed.ToString());
+ //if (__debug)
+ // Console.WriteLine(" Time for Block {0}: {1} elapsed", b.Label, watch.Elapsed.ToString());
watch.Reset();
-
- switch (outcome) {
- case ProverInterface.Outcome.Valid: {
- break;
- }
- case ProverInterface.Outcome.Invalid: {
-
- break;
- }
- default: {
-
- break;
- }
- }
-
}
checker.Close();
- if (__debug)
- Console.WriteLine("Number of Checked Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count);
- if (__debug)
- Console.WriteLine("Total time for this method: {0}", ts.ToString());
-
+ if (_print_time)
+ {
+ Console.WriteLine("Number of Checkes / #Blocks: {0} of {1}", _totalchecks, impl.Blocks.Count);
+ dc.__DEBUG_PrintStatistics();
+ Console.WriteLine("Total time for this method: {0}", ts.ToString());
+ }
#region Try to produce a counter example (brute force)
if (dc.DoomedSequences.Count > 0) {
- ConsoleColor col = Console.ForegroundColor;
- // Console.ForegroundColor = ConsoleColor.Red;
- // Console.WriteLine(" {0} is DOOMED!", impl.Name);
- // foreach (List<Block!> bl in dc.DoomedSequences) {
- // Console.Write("Doomed Blocks: ");
- // foreach (Block! b_ in bl) {
- // Console.Write("{0}, ", b_.Label);
- // }
- // Console.WriteLine();
- // }
- Console.ForegroundColor = col;
-
- int counter = 1;
- foreach (List<Block> bl in dc.DoomedSequences) {
- Contract.Assert(bl != null);
- Console.WriteLine("Doomed program point {0} of {1}", counter++, dc.DoomedSequences.Count);
- dc.ErrorHandler.m_DoomedBlocks = bl;
- foreach (Block b_ in bl) {
- Contract.Assert(b_ != null);
- if (m_BlockReachabilityMap.TryGetValue(b_, out dc.ErrorHandler.m_Reachvar))
- break;
+ int counter = 0;
+ List<Block> _all = new List<Block>();
+ foreach (List<Block> lb_ in dc.DoomedSequences)
+ {
+ foreach (Block b_ in lb_)
+ {
+ if (!_all.Contains(b_) && !m_UncheckableBlocks.Contains(b_))
+ {
+ _all.Add(b_); counter++;
+ if (!_print_time) Console.WriteLine(b_.Label);
+ }
+ }
+ }
+ if (_all.Count > 0)
+ {
+ Console.WriteLine("#Dead Blocks found: {0}: ", counter);
+ return Outcome.Errors;
}
- SearchCounterexample(impl, dc.ErrorHandler, callback);
- }
-
- //SearchCounterexample(impl, dc.ErrorHandler, callback);
- Console.WriteLine("------------------------------ \n\n");
- return Outcome.Errors;
}
#endregion
- //Console.WriteLine("------------------------------ \n\n");
return Outcome.Correct;
}
+ private Dictionary<Expr, int> m_GetPostconditionVariables(List<Block> allblock, List<Block> passBlock)
+ {
+ Dictionary<Expr, int> r = new Dictionary<Expr, int>();
+ foreach (Block b in allblock)
+ {
+ Variable v;
+ if (m_BlockReachabilityMap.TryGetValue(b, out v))
+ {
+ if (passBlock.Contains(b)) r[m_LastReachVarIncarnation[v]] = 1;
+ }
+ else
+ {
+ Console.WriteLine("there is no reachability variable for {0}", b.Label);
+ }
+ }
+ return r;
+ }
+#if false
#region Error message construction
private void SearchCounterexample(Implementation impl, DoomErrorHandler errh, VerifierCallback callback) {
Contract.Requires(impl != null);
@@ -635,7 +414,7 @@ namespace VC { Contract.Requires(reachvar != null);
Contract.Requires(impl != null);
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
+ Contract.Requires(cce.NonNullElements(cmdbackup));
#region Modify implementation
for (int i = startidx; i <= endidx; i++) {
if (_copiedBlock.Contains(impl.Blocks[i]))
@@ -762,7 +541,7 @@ namespace VC { void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,
int startidx, int endidx) {
- Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
+ Contract.Requires(cce.NonNullElements(cmdbackup));
Contract.Requires(impl != null);
for (int i = startidx; i <= endidx; i++) {
CmdSeq cs = null;
@@ -781,10 +560,12 @@ namespace VC { Contract.Requires(callback != null);
Checker checker = FindCheckerFor(impl, 1000);
Contract.Assert(checker != null);
- DoomCheck dc = new DoomCheck(impl, checker);
+ DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks);
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
outcome = ProverInterface.Outcome.Undetermined;
- if (!dc.CheckLabel(reachvar, out outcome)) {
+ List<Variable> rv = new List<Variable>();
+ rv.Add(reachvar);
+ if (!dc.CheckLabel(rv,null, out outcome)) {
checker.Close();
return false;
}
@@ -816,454 +597,11 @@ namespace VC { return false;
}
#endregion
+#endif
- #region Loop Removal
- /// <summary>
- /// This class is accessed only via the static method Convert2Dag
- /// It converts the program into a loopfree one by unrolling the loop threetimes and adding the appropriate havoc
- /// statements. The first and the last unrolling represent the first and last iteration of the loop. The second
- /// unrolling stands for any other iteration.
- /// </summary>
- private class DCProgramTransformer {
- private List<Block> Blocks;
- private List<Block> m_checkableBlocks;
- private Dictionary<Block, Block> m_copyMap = new Dictionary<Block, Block>();
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(Blocks));
- Contract.Invariant(cce.NonNullElements(m_checkableBlocks));
- Contract.Invariant(cce.NonNullDictionaryAndValues(m_copyMap));
- }
-
-
- public static List<Block> Convert2Dag(Implementation impl, Program program) {
- Contract.Requires(impl != null);
- Contract.Requires(program != null);
- Contract.Requires(1 <= impl.Blocks.Count);
-
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-
- Block start = impl.Blocks[0];
- Contract.Assert(start != null);
- 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();
- //pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block>(), true, "");
- pt.AbstractLoopUnrolling(gStart, new Dictionary<GraphNode, Block>(), true, "");
- pt.Blocks.Reverse();
- return pt.Blocks;
- }
-
-
- DCProgramTransformer() {
- Blocks = new List<Block>();
- m_checkableBlocks = new List<Block>();
- }
-
-
- #region Loop Unrolling Methods
-
- private Block AbstractLoopUnrolling(GraphNode node, Dictionary<GraphNode, Block> visited, bool unrollable, String prefix)
- {
- Contract.Requires(node != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(visited));
- Contract.Requires(prefix != null);
- Contract.Ensures(Contract.Result<Block>() != null);
- Block newb;
- if (visited.TryGetValue(node, out newb))
- {
- Contract.Assert(newb != null);
- return newb;
- }
- else
- {
- if (node.IsCutPoint)
- {
- #region Identify the body of the loop and the set of nodes succeeding the loop
- GotoCmd gc = node.Block.TransferCmd as GotoCmd;
- Contract.Assert(gc != null);
- Contract.Assert(gc.labelTargets != null);
-
- List<GraphNode> loopNodes = new List<GraphNode>();
- GatherLoopBodyNodes(node, node, loopNodes);
- List<GraphNode> exitNodes = GatherLoopExitNodes(loopNodes);
-
- GraphNode firstbodynode = null;
- foreach (GraphNode g in node.Succecessors)
- {
- Contract.Assert(g != null);
- if (loopNodes.Contains(g))
- {
- Contract.Assert(firstbodynode == null);
- firstbodynode = g;
- }
- }
- loopNodes.Remove(node); // remove the loophead from the loopbody
-
- #endregion
- #region Continue Unrolling for all nodes after the current loop after the current loop
- Dictionary<GraphNode, Block> _visited = new Dictionary<GraphNode, Block>();
-
- Block exitblock = null;
-
- foreach (GraphNode g in exitNodes)
- {
- Contract.Assert(g != null);
- Block b_ = AbstractLoopUnrolling(g, visited, unrollable, prefix);
- _visited.Add(g, b_);
- if (gc.labelTargets.Has(g.Block))
- {
- Contract.Assert(exitblock == null); // This may only happen once!
- exitblock = b_;
- }
- }
- Contract.Assert(exitblock != null); // This may only happen once!
- _visited.Add(node, node.Block);
- #endregion
- #region Apply the abstract loop unrolling to the body of the loop
- Block abstractloophead = null;
- Block abstractloopexit = exitblock;
-
- if (unrollable)
- {
- Dictionary<GraphNode, Block> visited3 = new Dictionary<GraphNode, Block>(_visited);
- Block iterL = AbstractLoopUnrolling(firstbodynode, visited3, false, prefix + "Las_");
- EliminateLoopingGotos(node, exitblock, visited3, _visited);
- AddHavocCmd(iterL, loopNodes);
- abstractloopexit = iterL;
- }
- else
- {
- // if the loop is not unrolled create a dummy block which havocs the loop targets before leaving the loop
- BlockSeq bseq = new BlockSeq();
- bseq.Add(exitblock);
- GotoCmd gcmd = new GotoCmd(node.Block.tok, bseq);
- abstractloopexit = new Block(exitblock.tok, prefix + "_EXIT_" + exitblock.Label, new CmdSeq(), gcmd);
- //UpdateReachabilityVarMap(abstractloopexit, exitblock);
- AddHavocCmd(abstractloopexit, loopNodes);
- Blocks.Add(abstractloopexit);
- }
- Dictionary<GraphNode, Block> visited2 = new Dictionary<GraphNode, Block>(_visited);
- Block iterA = AbstractLoopUnrolling(firstbodynode, visited2, unrollable, prefix + "Abs_");
- EliminateLoopingGotos(node, abstractloopexit, visited2, _visited);
- AddHavocCmd(iterA, loopNodes);
- abstractloophead = iterA;
- if (unrollable)
- {
- Dictionary<GraphNode, Block> visited1 = new Dictionary<GraphNode, Block>(_visited);
- Block iterF = AbstractLoopUnrolling(firstbodynode, visited1, false, prefix + "Fir_");
- EliminateLoopingGotos(node, iterA, visited1, _visited);
- abstractloophead = iterF;
- }
-
- BlockSeq bs = new BlockSeq();
- foreach (GraphNode g in node.Succecessors)
- {
- if (g != firstbodynode) bs.Add(exitblock);
- else bs.Add(abstractloophead);
- }
- newb = new Block(node.Block.tok, prefix+node.Block.Label, node.Body, new GotoCmd(gc.tok, bs));
- Block b;
- if (m_copyMap.TryGetValue(node.Block, out b))
- {
- Console.WriteLine("Duplicate entry for {0}", b.Label);
- }
- else
- {
- m_copyMap.Add(node.Block, newb);
- }
- #endregion
- }
- else
- {
- #region If it is not a cut point continue with successors and make a copy
- BlockSeq newSuccs = new BlockSeq();
- foreach (GraphNode g in node.Succecessors)
- {
- Contract.Assert(g != null);
- newSuccs.Add(AbstractLoopUnrolling(g, visited, unrollable, prefix));
- }
- newb = new Block(node.Block.tok, prefix+node.Block.Label, node.Body, node.Block.TransferCmd);
- Block b;
- if (m_copyMap.TryGetValue(node.Block, out b))
- {
- Contract.Assert(b != null);
- m_copyMap.Add(newb, b);
- }
- else
- {
- m_copyMap.Add(newb, node.Block);
- }
-
-
- Contract.Assert(newb != null);
- Contract.Assert(newb.TransferCmd != null);
- if (newSuccs.Length == 0)
- newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);
- else
- newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);
-
- //TODO replace this by updating the copied reachability variables!
- if (unrollable)
- {
- m_checkableBlocks.Add(newb);
- }
- #endregion
- }
- visited.Add(node, newb);
- Blocks.Add(newb);
- //UpdateReachabilityVarMap(newb, node.Block);
- }
- Contract.Assert(newb != null);
- return newb;
- }
-
- void UpdateReachabilityVarMap(Block clonedBlock, Block origBlock)
- {
- Variable v = null;
- if (!DCGen.m_BlockReachabilityMap.TryGetValue(origBlock, out v))
- {
- Console.WriteLine("no reachability variable for {0}", origBlock.Label);
- }
- DCGen.m_BlockReachabilityMap.Add(clonedBlock, v);
-
- }
-
- private void EliminateLoopingGotos(GraphNode node, Block nextblock, Dictionary<GraphNode, Block> visited2,
- Dictionary<GraphNode, Block> _visited)
- {
- foreach (KeyValuePair<GraphNode, Block> kvp in visited2)
- {
- if (!_visited.ContainsKey(kvp.Key))
- {
- GotoCmd gc = kvp.Value.TransferCmd as GotoCmd;
- if (gc != null)
- {
- bool change = false;
- BlockSeq bs = new BlockSeq();
- Contract.Assert(gc.labelTargets != null);
- foreach (Block b in gc.labelTargets)
- {
- if (b != node.Block)
- {
- if (!bs.Has(b)) bs.Add(b);
- }
- else
- {
- change = true;
- if (!bs.Has(nextblock)) bs.Add(nextblock);
- }
- }
- if (change) gc.labelTargets = bs;
- }
- }
- }
- }
-
-
- private void GatherLoopBodyNodes(GraphNode current, GraphNode cutPoint, List<GraphNode> loopNodes) {
- Contract.Requires(current != null);
- Contract.Requires(cutPoint != null);
- Contract.Requires(cce.NonNullElements(loopNodes));
- loopNodes.Add(current);
- foreach (GraphNode g in current.Predecessors) {
- Contract.Assert(g != null);
- if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g))
- continue;
- GatherLoopBodyNodes(g, cutPoint, loopNodes);
- }
- }
-
- private List<GraphNode> GatherLoopExitNodes(List<GraphNode> loopNodes) {
- Contract.Requires(cce.NonNullElements(loopNodes));
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<GraphNode>>()));
- List<GraphNode> exitnodes = new List<GraphNode>();
-
- foreach (GraphNode g in loopNodes) {
- Contract.Assert(g != null);
- foreach (GraphNode s in g.Succecessors) {
- Contract.Assert(s != null);
- if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ )
- exitnodes.Add(s);
- }
- }
- return exitnodes;
- }
-
- private void AddHavocCmd(Block b, List<GraphNode> loopNodes) {
- Contract.Requires(b != null);
- Contract.Requires(loopNodes != null);
- List<Block> loopBlocks = new List<Block>();
- foreach (GraphNode g in loopNodes) {
- Contract.Assert(g != null);
- loopBlocks.Add(g.Block);
- }
- HavocCmd hcmd = HavocLoopTargets(loopBlocks, b.tok);
- Contract.Assert(hcmd != null);
- CmdSeq body = new CmdSeq();
- body.Add(hcmd);
- body.AddRange(b.Cmds);
- b.Cmds = body;
- }
-
- private HavocCmd HavocLoopTargets(List<Block> bl, IToken tok) {
- Contract.Requires(bl != null);
- Contract.Requires(tok != null);
- Contract.Ensures(Contract.Result<HavocCmd>() != null);
-
- VariableSeq varsToHavoc = new VariableSeq();
- foreach (Block b in bl) {
- Contract.Assert(b != null);
- foreach (Cmd c in b.Cmds) {
- Contract.Assert(c != null);
- c.AddAssignedVariables(varsToHavoc);
- }
- }
- IdentifierExprSeq havocExprs = new IdentifierExprSeq();
- foreach (Variable v in varsToHavoc) {
- Contract.Assert(v != null);
- 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
-
-
- #region GraphNode
- private class GraphNode {
- public readonly Block Block;
- public readonly CmdSeq Body;
- public bool IsCutPoint; // is set during ComputeGraphInfo
- [Rep]
- public readonly List<GraphNode/*!*/>/*!*/ Predecessors = new List<GraphNode>();
- [Rep]
- public readonly List<GraphNode/*!*/>/*!*/ Succecessors = new List<GraphNode>();
- public GraphNode firstPredecessor;
- public List<GraphNode/*!*/>/*!*/ UnavoidableNodes = new List<GraphNode/*!*/>(); // should be done using a set
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Block != null);
- Contract.Invariant(Body != null);
- Contract.Invariant(cce.NonNullElements(Predecessors));
- Contract.Invariant(cce.NonNullElements(Succecessors));
- Contract.Invariant(cce.NonNullElements(UnavoidableNodes));
- }
-
-
- GraphNode(Block b, CmdSeq body) {
- Contract.Requires(b != null);
- Contract.Requires(body != null);
- Block = b;
- Body = body;
- IsCutPoint = false;
-
- }
-
- static CmdSeq GetOptimizedBody(CmdSeq cmds) {
- Contract.Requires(cmds != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
-
- int n = 0;
- foreach (Cmd c in cmds) {
- n++;
- PredicateCmd pc = c as PredicateCmd;
- if (pc != null && pc.Expr is LiteralExpr && ((LiteralExpr)pc.Expr).IsFalse) {
- // return a sequence consisting of the commands seen so far
- Cmd[] s = new Cmd[n];
- for (int i = 0; i < n; i++) {
- s[i] = cmds[i];
- }
- return new CmdSeq(s);
- }
- }
- return cmds;
- }
-
- private static List<GraphNode> Intersect(List<GraphNode> left, List<GraphNode> right) {
- Contract.Requires(left != null);
- Contract.Requires(right != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<GraphNode>>()));
- List<GraphNode> ret = new List<GraphNode>();
- List<GraphNode> tmp = left;
- tmp.AddRange(right);
- foreach (GraphNode gn in tmp) {
- Contract.Assert(gn != null);
- if (ret.Contains(gn))
- continue;
- if (left.Contains(gn) && right.Contains(gn))
- ret.Add(gn);
- }
- return ret;
- }
-
- public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block, GraphNode> gd, Set /*Block*/ beingVisited) {
- Contract.Requires(b != null);
- Contract.Requires(beingVisited != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(gd));
-
- Contract.Ensures(Contract.Result<GraphNode>() != null);
-
- GraphNode g;
- if (gd.TryGetValue(b, out g)) {
- Contract.Assume(from != null);
- Contract.Assert(g != null);
-
- g.UnavoidableNodes = Intersect(g.UnavoidableNodes, from.UnavoidableNodes);
- if (!g.UnavoidableNodes.Contains(g))
- g.UnavoidableNodes.Add(g);
-
- g.Predecessors.Add(from);
- if (g.firstPredecessor == null)
- g.firstPredecessor = from;
-
- if (beingVisited.Contains(b))
- g.IsCutPoint = true; // it's a cut point
- } else {
- CmdSeq body = GetOptimizedBody(b.Cmds);
- g = new GraphNode(b, body);
- gd.Add(b, g);
- if (from != null) {
- g.Predecessors.Add(from);
- if (from == null)
- g.firstPredecessor = g;
-
- if (g.firstPredecessor == null)
- g.firstPredecessor = from;
-
- }
- if (body != b.Cmds) {
- // the body was optimized -- there is no way through this block
- } else {
- beingVisited.Add(b);
- GotoCmd gcmd = b.TransferCmd as GotoCmd;
- if (gcmd != null) {
- Contract.Assume(gcmd.labelTargets != null);
- foreach (Block succ in gcmd.labelTargets) {
- Contract.Assert(succ != null);
- g.Succecessors.Add(ComputeGraphInfo(g, succ, gd, beingVisited));
- }
- }
- beingVisited.Remove(b);
- }
- }
- return g;
- }
- }
-
- }
- #endregion
-
- #endregion
Block exitBlock;
+
#region Program Passification
private void GenerateHelperBlocks(Implementation impl) {
Contract.Requires(impl != null);
@@ -1308,44 +646,45 @@ namespace VC { private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) {
Contract.Requires(impl != null);
Contract.Requires(mvInfo != null);
+ Contract.Requires(this.exitBlock != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
CurrentLocalVariables = impl.LocVars;
- Convert2PassiveCmd(impl, mvInfo);
- return new Hashtable();
+ return Convert2PassiveCmd(impl, mvInfo);
+ //return new Hashtable();
}
/// <summary>
/// Add additional variable to allow checking as described in the paper
/// "It's doomed; we can prove it"
/// </summary>
- private AssumeCmd GenerateReachabilityPredicates(Implementation impl)
+ private CmdSeq GenerateReachabilityPredicates(Implementation impl)
{
- Contract.Requires(impl != null);
- ExprSeq es = new ExprSeq();
-
+ Contract.Requires(impl != null);
+
foreach (Block b in impl.Blocks)
{
Contract.Assert(b != null);
//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_);
+ new TypedIdent(b.tok, b.Label + reachvarsuffix, new BasicType(SimpleType.Int )));
+ impl.LocVars.Add(v_);
+
m_BlockReachabilityMap[b] = v_;
IdentifierExpr lhs = new IdentifierExpr(b.tok, v_);
Contract.Assert(lhs != null);
- es.Add(new IdentifierExpr(b.tok, v_));
-
+ impl.Proc.Modifies.Add(lhs);
+
List<AssignLhs> lhsl = new List<AssignLhs>();
lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs));
List<Expr> rhsl = new List<Expr>();
- rhsl.Add(Expr.True);
+ rhsl.Add(Expr.Literal(1) );
+
CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
cs.AddRange(b.Cmds);
@@ -1353,40 +692,159 @@ namespace VC { //checkBlocks.Add(new CheckableBlock(v_,b));
}
- if (es.Length == 0)
- return null;
- Expr aexp = null;
+ CmdSeq incReachVars = new CmdSeq();
+ foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)
+ {
+ IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value);
+ impl.Proc.Modifies.Add(lhs);
+ incReachVars.Add(new AssumeCmd(Token.NoToken, Expr.Le(lhs, Expr.Literal(1))));
+ }
+
+ return incReachVars;
+ }
+
+ #endregion
- if (es.Length == 1)
+ #region Compute loop-free approximation
+
+ // this might be redundant, but I didn't find a better place to get this information.
+ private Dictionary<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();
+
+ private void Transform4DoomedCheck(Implementation impl, Program program)
+ {
+ variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ incarnationOriginMap = new Dictionary<Incarnation, Absy>();
+ if (impl.Blocks.Count < 1) return;
+
+ impl.PruneUnreachableBlocks();
+ AddBlocksBetween(impl.Blocks);
+ ClearPredecessors(impl.Blocks);
+ ComputePredecessors(impl.Blocks);
+
+ GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks);
+ LoopRemover lr = new LoopRemover(ga);
+ lr.AbstractLoopUnrolling();
+
+ impl.Blocks = ga.ToImplementation(out m_UncheckableBlocks);
+ ClearPredecessors(impl.Blocks);
+ ComputePredecessors(impl.Blocks);
+
+ // Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks
+ List<Block> oldblocks = new List<Block>();
+ oldblocks.AddRange(impl.Blocks);
+ GenerateHelperBlocks(impl);
+ #region Check for the "BlocksBetween" if all their successors are in m_UncheckableBlocks
+ foreach (Block b in impl.Blocks)
{
- aexp = es[0];
+ if (oldblocks.Contains(b)) continue;
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (gc != null)
+ {
+ bool allsuccUncheckable = true;
+ foreach (Block _b in gc.labelTargets)
+ {
+ if (!m_UncheckableBlocks.Contains(_b))
+ {
+ allsuccUncheckable = false; break;
+ }
+ }
+ if (allsuccUncheckable && !m_UncheckableBlocks.Contains(b)) m_UncheckableBlocks.Add(b);
+ }
}
- else if (es.Length == 2)
+ #endregion
+
+ impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks);
+
+ m_BlockReachabilityMap = new Dictionary<Block, Variable>();
+ CmdSeq cs = GenerateReachabilityPredicates(impl);
+
+ foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
{
- aexp = Expr.Binary(Token.NoToken,
- BinaryOperator.Opcode.And,
- cce.NonNull(es[0]),
- cce.NonNull(es[1]));
+ test.Cmds.AddRange(cs);
}
- else
+
+ ClearPredecessors(impl.Blocks);
+ ComputePredecessors(impl.Blocks);
+ //EmitImpl(impl,false);
+ Hashtable/*Variable->Expr*/ htbl = PassifyProgram(impl, new ModelViewInfo(program, impl));
+
+ // Collect the last incarnation of each reachability variable in the passive program
+ foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)
{
- aexp = Expr.True;
- foreach (Expr e_ in es)
+ if (htbl.ContainsKey(kvp.Value))
{
- aexp = Expr.Binary(Token.NoToken,
- BinaryOperator.Opcode.And,
- cce.NonNull(e_), aexp);
+ m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[kvp.Value];
}
}
- Contract.Assert(aexp != null);
+ }
- AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);
- return ac;
+ List<Block> getTheFFinalBlock(Block b)
+ {
+ List<Block> lb = new List<Block>();
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ if (gc == null) lb.Add(b);
+ else
+ {
+ foreach (Block s in gc.labelTargets)
+ {
+ foreach (Block r in getTheFFinalBlock(s)) if (!lb.Contains(r)) lb.Add(r);
+ }
+ }
+ return lb;
}
- #endregion
+ private List<Block> DeepCopyBlocks(List<Block> lb, List<Block> uncheckables)
+ {
+ List<Block> clones = new List<Block>();
+ List<Block> uncheck_ = new List<Block>();
+ Dictionary<Block, Block> clonemap = new Dictionary<Block, Block>();
+
+ foreach (Block b in lb)
+ {
+ Block clone = CloneBlock(b);
+ clones.Add(clone);
+ clonemap[b] = clone;
+ if (uncheckables.Contains(b)) uncheck_.Add(clone);
+ }
+ uncheckables.Clear();
+ uncheckables.AddRange(uncheck_);
+ // update the successors and predecessors
+ foreach (Block b in lb)
+ {
+ BlockSeq newpreds = new BlockSeq();
+ foreach (Block b_ in b.Predecessors)
+ {
+ newpreds.Add(clonemap[b_]);
+ }
+ clonemap[b].Predecessors = newpreds;
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ ReturnCmd rc = b.TransferCmd as ReturnCmd;
+ if (gc != null)
+ {
+ StringSeq lseq = new StringSeq();
+ BlockSeq bseq = new BlockSeq();
+ foreach (string s in gc.labelNames) lseq.Add(s);
+ foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]);
+ GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq);
+ clonemap[b].TransferCmd = tcmd;
+ }
+ else if (rc != null)
+ {
+ clonemap[b].TransferCmd = new ReturnCmd(rc.tok);
+ }
+ }
+ return clones;
+ }
+
+ private Block CloneBlock(Block b)
+ {
+ Block clone = new Block(b.tok, b.Label, b.Cmds, b.TransferCmd);
+ if (this.exitBlock == b) this.exitBlock = clone;
+ return clone;
+ }
+ #endregion
}
}
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 1d4cc566..ff10acbe 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -148,7 +148,10 @@ <Compile Include="ConditionGeneration.cs" />
<Compile Include="Context.cs" />
<Compile Include="DoomCheck.cs" />
+ <Compile Include="DoomedLoopUnrolling.cs" />
+ <Compile Include="DoomedStrategy.cs" />
<Compile Include="DoomErrorHandler.cs" />
+ <Compile Include="HasseDiagram.cs" />
<Compile Include="OrderingAxioms.cs" />
<Compile Include="StratifiedVC.cs" />
<Compile Include="VC.cs" />
|