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/DoomCheck.cs | |
| parent | b7829c73906c7ddbc01e7e076aa430f349ae9698 (diff) | |
new algorithm for dead code detection (vc:doomed)
Diffstat (limited to 'Source/VCGeneration/DoomCheck.cs')
| -rw-r--r-- | Source/VCGeneration/DoomCheck.cs | 824 |
1 files changed, 137 insertions, 687 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
-
-
+
}
+
}
|