diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomCheck.cs | 63 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomedLoopUnrolling.cs | 78 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomedStrategy.cs | 207 | ||||
| -rw-r--r-- | Source/VCGeneration/HasseDiagram.cs | 57 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 45 |
6 files changed, 340 insertions, 118 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index e68c1b71..4bc845dd 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -110,6 +110,7 @@ namespace Microsoft.Boogie { public string PrintFile = null;
public int PrintUnstructured = 0;
public int DoomStrategy = -1;
+ public bool DoomRestartTP = false;
public bool PrintDesugarings = false;
public string SimplifyLogFilePath = null;
public string/*!*/ LogPrefix = "";
@@ -1069,6 +1070,13 @@ namespace Microsoft.Boogie { case "/DoomStrategy":
ps.GetNumericArgument(ref DoomStrategy);
break;
+ case "-DoomRestartTP":
+ case "/DoomRestartTP":
+ if (ps.ConfirmArgumentCount(0))
+ {
+ DoomRestartTP = true;
+ }
+ break;
case "-extractLoops":
case "/extractLoops":
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 7d84422a..9e1b2b1c 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -4,11 +4,6 @@ //
//-----------------------------------------------------------------------------
-/*
- Todo:
- - Inject Pre- and Postcondition
-*/
-
using System;
using System.Collections;
using System.Collections.Generic;
@@ -72,7 +67,7 @@ void ObjectInvariant() }
//Console.WriteLine("TPQuery k={0}, l={1}, |Sp|={2}", k, l, finalreachvars.Count);
- VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO);
+ VCExpr vc21 = m_Checker.VCExprGen.Integer(BigNum.ZERO); // Ask: is the necessary or can we use the same instance term in two inequalities?
VCExpr vc22 = m_Checker.VCExprGen.Integer(BigNum.ZERO);
foreach (KeyValuePair<Expr, int> kvp in finalreachvars)
@@ -82,11 +77,14 @@ void ObjectInvariant() 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)))
- );
+ VCExpr post = m_Checker.VCExprGen.Gt(m_Checker.VCExprGen.Integer(BigNum.FromInt(l)), vc21);
+ if (k != -1)
+ {
+ post = m_Checker.VCExprGen.Or(
+ post, m_Checker.VCExprGen.Gt(vc22, m_Checker.VCExprGen.Integer(BigNum.FromInt(k)))
+ );
+ }
vc = (m_Checker.VCExprGen.Or(vc, (post) ));
}
@@ -178,40 +176,38 @@ void ObjectInvariant() 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);
+ if (CommandLineOptions.Clo.DoomStrategy!=-1) 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);
-
+ {
+ if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover specialK Strategy");
+ m_Order = new PathCoverStrategyK(passive_impl, unifiedExit, uncheckable);
break;
}
case 1:
{
- Console.WriteLine("Path Cover Strategy");
+ if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("Path Cover L Strategy");
m_Order = new PathCoverStrategy(passive_impl, unifiedExit, uncheckable);
break;
}
case 2:
{
- Console.WriteLine("hasse strategy");
+ if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse strategy");
m_Order = new HierachyStrategy(passive_impl, unifiedExit, uncheckable);
break;
}
case 3:
{
- Console.WriteLine("hasse+ce strategy");
+ if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("hasse+ce strategy");
m_Order = new HierachyCEStrategy(passive_impl, unifiedExit, uncheckable);
break;
}
case 4:
{
- Console.WriteLine("no strategy");
+ if (CommandLineOptions.Clo.DoomStrategy != -1) Console.WriteLine("no strategy");
m_Order = new NoStrategy(passive_impl, unifiedExit, uncheckable);
break;
}
@@ -226,10 +222,24 @@ void ObjectInvariant() Contract.Assert( l2a!=null);
Label2Absy = l2a;
- m_Evc.Initialize(vce);
+ m_Evc.Initialize(vce);
}
- public static VCExpr __tmpHack;
+
+ public void RespawnChecker(Implementation passive_impl, Checker check)
+ {
+ Contract.Requires(check != null);
+ m_Check = check;
+ 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(l2a != null);
+ Label2Absy = l2a;
+
+ m_Evc.Initialize(vce);
+ }
/* - Set b to the next block that needs to be checked.
- Returns false and set b to null if all blocks are checked.
@@ -239,7 +249,9 @@ void ObjectInvariant() {
return m_Order.GetNextBlock(out lb);
}
-
+
+ public Stopwatch DEBUG_ProverTime = new Stopwatch();
+
/* - 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.
@@ -247,12 +259,17 @@ void ObjectInvariant() public bool CheckLabel(List<Variable> lv,Dictionary<Expr, int> finalreachvars, out ProverInterface.Outcome outcome) {
Contract.Requires(lv != null);
outcome = ProverInterface.Outcome.Undetermined;
+ DEBUG_ProverTime.Reset();
+ DEBUG_ProverTime.Start();
if (m_Evc.CheckReachvar(lv,finalreachvars,m_Order.MaxBlocks,m_Order.MinBlocks,m_Order.HACK_NewCheck, out outcome) ) {
+ DEBUG_ProverTime.Stop();
if (!m_Order.SetCurrentResult(lv, outcome, m_ErrHandler)) {
outcome = ProverInterface.Outcome.Undetermined;
}
return true;
} else {
+ DEBUG_ProverTime.Stop();
+ Console.WriteLine(outcome);
m_Order.SetCurrentResult(lv, ProverInterface.Outcome.Undetermined, m_ErrHandler);
return false;
}
diff --git a/Source/VCGeneration/DoomedLoopUnrolling.cs b/Source/VCGeneration/DoomedLoopUnrolling.cs index 1e42a535..9d58d227 100644 --- a/Source/VCGeneration/DoomedLoopUnrolling.cs +++ b/Source/VCGeneration/DoomedLoopUnrolling.cs @@ -320,8 +320,13 @@ namespace VC 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);
+
+
+ m_DetectCutPoints(GraphMap[blocks[0]]);
+
+ //m_DetectCutPoints(GraphMap[blocks[0]], null, new List<GraphNode>());
+ Graphloops = m_CollectLoops(GraphMap[blocks[0]], null);
+
}
public List<Block> ToImplementation(out List<Block> uncheckables)
@@ -379,13 +384,14 @@ namespace VC 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;
+ Console.WriteLine("Normal RootNode {0}", gn.Label.Label);
return;
}
else
@@ -400,10 +406,70 @@ namespace VC }
}
+*/
+
+
+ private void m_DetectCutPoints(GraphNode gn)
+ {
+ List<GraphNode> todo = new List<GraphNode>();
+ List<GraphNode> done = new List<GraphNode>();
+ todo.Add(gn);
+
+ GraphNode current = null;
+ todo[0].Index = 0;
+
+ while (todo.Count > 0)
+ {
+ current = todo[0];
+ todo.Remove(current);
+
+ bool ready = true;
+ foreach (GraphNode p in current.Pre)
+ {
+ if (!done.Contains(p) )
+ {
+ _loopbacktracking.Clear();
+ if (!m_isLoop(current, p, todo, done))
+ {
+ todo.Add(current);
+ ready = false;
+ break;
+ }
+ else
+ {
+ if (!current.LoopingPred.Contains(p)) current.LoopingPred.Add(p);
+ current.IsCutpoint = true;
+ }
+ }
+ }
+ if (!ready) continue;
+ done.Add(current);
+ foreach (GraphNode s in current.Suc)
+ {
+ if (!todo.Contains(s) && !done.Contains(s)) todo.Add(s);
+ }
+ }
+
+ }
+
+ List<GraphNode> _loopbacktracking = new List<GraphNode>();
+ private bool m_isLoop(GraphNode loophead, GraphNode gn, List<GraphNode> l1, List<GraphNode> l2)
+ {
+ if (loophead == gn) return true;
+ if (l1.Contains(gn) || l2.Contains(gn) || _loopbacktracking.Contains(gn)) return false;
+ _loopbacktracking.Add(gn);
+ foreach (GraphNode p in gn.Pre)
+ {
+ if (m_isLoop(loophead, p, l1, l2)) return true;
+ }
+ return false;
+ }
private List<Loop> m_CollectLoops(GraphNode gn, Loop lastLoop)
{
List<Loop> ret = new List<Loop>();
+ if (gn.Visited) return ret;
+ gn.Visited = true;
List<GraphNode> loopingSucs = new List<GraphNode>();
if (gn.IsCutpoint)
{
@@ -416,11 +482,12 @@ namespace VC loopingSucs = l.LoopNodes;
lastLoop = l;
ret.Add(lastLoop);
- }
+ }
foreach (GraphNode suc in gn.Suc)
{
if (!loopingSucs.Contains(suc)) ret.AddRange(m_CollectLoops(suc, lastLoop));
}
+ //Debugger.Break();
return ret;
}
}
@@ -429,6 +496,9 @@ namespace VC #region GraphNodeStructure
internal class GraphNode
{
+ public int Index = -1; // Used for scc detection
+ public int LowLink = -1; // Used for scc detection
+
public GraphNode(Block b)
{
Label = b; IsCutpoint = false;
diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/VCGeneration/DoomedStrategy.cs index 74ac0657..18de31c7 100644 --- a/Source/VCGeneration/DoomedStrategy.cs +++ b/Source/VCGeneration/DoomedStrategy.cs @@ -37,35 +37,35 @@ namespace VC protected BlockHierachy m_BlockH = null;
protected int m_MaxBranchingDepth = 0;
- protected int m_MaxMinElemPerPath = 0;
+ protected int m_MaxK = 0;
+
+ protected Stopwatch sw = new Stopwatch();
// 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/*!*/>/*!*/>();
+ private List<Block> __DEBUG_minelements = new 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;
+
+ //foreach (BlockHierachyNode bhn in m_BlockH.Leaves)
+ //{
+ // if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]);
+ //}
+ //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);
+
- 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);
+ Console.WriteLine("MaBranchingDepth {0} MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK);
+
+ Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0);
}
MaxBlocks = imp.Blocks.Count;
@@ -74,7 +74,6 @@ namespace VC __DEBUG_BlocksTotal = imp.Blocks.Count;
}
-
public int MaxBlocks, MinBlocks;
public bool HACK_NewCheck;
@@ -116,14 +115,9 @@ namespace VC 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;
+ if (__DEBUG_minelements.Contains(b)) leavespp++;
plen++;
- if (gc != null)
+ if (gc != null && gc.labelTargets.Length>0)
{
if (gc.labelTargets.Length > 1) branchingdepth++;
m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth;
@@ -136,11 +130,12 @@ namespace VC {
__pathLength.Add(plen);
__leavespp.Add(leavespp);
+ m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp;
}
-
}
+
}
#endregion
@@ -206,6 +201,7 @@ namespace VC override public bool GetNextBlock(out List<Block> lb)
{
+ sw.Start();
if (m_Current < m_Blocks.Count)
{
lb = new List<Block>();
@@ -230,6 +226,10 @@ namespace VC {
m_doomedBlocks.Add(m_Blocks[m_Current - 1]);
}
+ if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks);
+ sw.Stop();
+ sw.Reset();
+
return true;
}
}
@@ -299,7 +299,7 @@ namespace VC }
#endregion
- #region Path Cover Optimization
+ #region Path Cover Optimization with L
internal class PathCoverStrategy : DoomDetectionStrategy
{
List<Block> m_Uncheckedlocks = new List<Block>();
@@ -312,26 +312,113 @@ namespace VC 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;
+ m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);
+ MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);
+ MaxBlocks = -1;
+ }
+
+ override public bool GetNextBlock(out List<Block> lb)
+ {
+ sw.Start();
+
+ 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);
+
+ return true;
+ }
+
+ override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)
+ {
+ this.__DEBUG_BlocksChecked++;
+ // Valid means infeasible...
+ int oldl = MinBlocks;
+ int oldsize = m_Uncheckedlocks.Count;
+
+
+ if (outcome == ProverInterface.Outcome.Valid)
+ {
+ this.__DEBUG_InfeasibleTraces++;
+ if (MinBlocks == 1)
+ {
+ m_NoMoreMoves = true;
+ }
+ else
+ {
+ MinBlocks = 1;
+ }
+ }
+ else if (outcome == ProverInterface.Outcome.Invalid)
+ {
+ this.__DEBUG_TracesChecked++;
+
+ List<Block> errortrace = m_GetErrorTraceFromCE(cb);
+ foreach (Block b in errortrace)
+ {
+ if (m_Uncheckedlocks.Contains(b))
+ {
+ m_Uncheckedlocks.Remove(b);
+ }
+ }
+ cb.TraceNodes.Clear();
+ m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);
+ if (m_MaxK < 1)
+ {
+ m_NoMoreMoves = true; m_Uncheckedlocks.Clear();
+ }
+ MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);
+ //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK;
+
+ }
+ else
+ {
+ m_NoMoreMoves = true; m_Uncheckedlocks.Clear();
+ }
+ if (__DEBUGOUT)
+ Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);
+ sw.Stop();
+ sw.Reset();
+ return true;
}
- public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach, bool test_alternativeK)
+
+ }
+ #endregion
+
+ #region Path Cover Optimization with K
+ internal class PathCoverStrategyK : 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 PathCoverStrategyK(Implementation imp, Block unifiedexit, List<Block> unreach)
: base(imp, unifiedexit, unreach)
{
m_Ignore = unreach;
@@ -339,20 +426,16 @@ namespace VC 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]);
}
- }
+ }
+
+ m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);
+
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;
@@ -365,33 +448,13 @@ namespace VC {
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;
- }
-
+ //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks);
}
override public bool GetNextBlock(out List<Block> lb)
{
+ sw.Start();
+
lb = new List<Block>();
if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)
@@ -405,17 +468,20 @@ namespace VC }
lb.AddRange(m_Uncheckedlocks);
- MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks;
- MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0);
+ 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...
+ int oldk = MaxBlocks;
+ int oldl = MinBlocks;
+ int oldsize = m_Uncheckedlocks.Count;
+
if (outcome == ProverInterface.Outcome.Valid)
{
this.__DEBUG_InfeasibleTraces++;
@@ -431,7 +497,7 @@ namespace VC 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)
{
@@ -441,11 +507,18 @@ namespace VC }
}
cb.TraceNodes.Clear();
+
+ int k = m_BlockH.GetMaxK(m_Uncheckedlocks);
+ MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k;
}
else
{
m_NoMoreMoves = true; m_Uncheckedlocks.Clear();
}
+ if (__DEBUGOUT)
+ Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);
+ sw.Stop();
+ sw.Reset();
return true;
}
diff --git a/Source/VCGeneration/HasseDiagram.cs b/Source/VCGeneration/HasseDiagram.cs index 144d70e5..db777336 100644 --- a/Source/VCGeneration/HasseDiagram.cs +++ b/Source/VCGeneration/HasseDiagram.cs @@ -144,8 +144,11 @@ namespace VC readonly public Dictionary<Block, List<Block>> PostDominators = new Dictionary<Block, List<Block>>();
readonly public List<BlockHierachyNode> Leaves = new List<BlockHierachyNode>();
+ private Implementation m_Impl;
+
public BlockHierachy(Implementation impl, Block unifiedExit)
{
+ m_Impl = impl;
List<Block> blocks = impl.Blocks;
List<BlockHierachyNode> tmp_hnodes = new List<BlockHierachyNode>();
Dictionary<Block, List<Block>> unavoidable = new Dictionary<Block, List<Block>>();
@@ -182,6 +185,60 @@ namespace VC Leaves = hd.Leaves;
}
+ public int GetMaxK(List<Block> blocks)
+ {
+ m_GetMaxK(blocks);
+ return (m_MaxK>0) ? m_MaxK : 1;
+ }
+
+ private int m_MaxK = 0;
+ private void m_GetMaxK(List<Block> blocks)
+ {
+ m_MaxK = 0;
+ Dictionary<Block, int> kstore = new Dictionary<Block, int>();
+ List<Block> todo = new List<Block>();
+ List<Block> done = new List<Block>();
+ todo.Add(m_Impl.Blocks[0]);
+ kstore[m_Impl.Blocks[0]] = 0;
+ int localmax;
+ Block current = null;
+ while (todo.Count > 0)
+ {
+ current = todo[0];
+ todo.Remove(current);
+ bool ready = true;
+ localmax = 0;
+ if (current.Predecessors!=null) {
+ foreach (Block p in current.Predecessors)
+ {
+ if (!done.Contains(p))
+ {
+ ready = false; break;
+ }
+ else localmax = (localmax > kstore[p]) ? localmax : kstore[p];
+ }
+ }
+ if (!ready)
+ {
+ todo.Add(current); continue;
+ }
+ done.Add(current);
+ kstore[current] = (blocks.Contains(current)) ? localmax +1 : localmax;
+
+ m_MaxK = (kstore[current] > m_MaxK) ? kstore[current] : m_MaxK;
+
+ GotoCmd gc = current.TransferCmd as GotoCmd;
+ if (gc != null)
+ {
+ foreach (Block s in gc.labelTargets)
+ {
+ if (!todo.Contains(s)) todo.Add(s);
+ }
+ }
+ }
+
+ }
+
public List<Block> GetOtherDoomedBlocks(List<Block> doomedblocks)
{
List<Block> alsoDoomed = new List<Block>();
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 805eb84f..f7c77412 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -122,21 +122,17 @@ namespace VC { //Contract.Requires(callback != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Stopwatch watch = new Stopwatch();
-
Console.WriteLine();
Console.WriteLine("Checking function {0}", impl.Name);
callback.OnProgress("doomdetector", 0, 0, 0);
- watch.Reset();
- watch.Start();
+ bool restartTP = CommandLineOptions.Clo.DoomRestartTP ;
- //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));
Transform4DoomedCheck(impl, program);
-
- //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
+ //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
Checker checker = FindCheckerFor(impl, 1000);
Contract.Assert(checker != null);
@@ -149,10 +145,7 @@ namespace VC { ProverInterface.Outcome outcome;
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
- watch.Stop();
- watch.Reset();
-
- System.TimeSpan ts = watch.Elapsed;
+ System.TimeSpan ts = new TimeSpan();
if (_print_time) Console.WriteLine("Total number of blocks {0}", impl.Blocks.Count);
@@ -189,15 +182,18 @@ namespace VC { _totalchecks++;
- 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());
- watch.Reset();
+ ts += dc.DEBUG_ProverTime.Elapsed;
+
+ if (restartTP)
+ {
+ checker.Close();
+ checker = FindCheckerFor(impl, 1000);
+ dc.RespawnChecker(impl, checker);
+ dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
+ }
}
checker.Close();
@@ -720,7 +716,7 @@ namespace VC { impl.PruneUnreachableBlocks();
AddBlocksBetween(impl.Blocks);
ClearPredecessors(impl.Blocks);
- ComputePredecessors(impl.Blocks);
+ ComputePredecessors(impl.Blocks);
GraphAnalyzer ga = new GraphAnalyzer(impl.Blocks);
LoopRemover lr = new LoopRemover(ga);
@@ -758,15 +754,16 @@ namespace VC { m_BlockReachabilityMap = new Dictionary<Block, Variable>();
CmdSeq cs = GenerateReachabilityPredicates(impl);
-
- foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
- {
- test.Cmds.AddRange(cs);
- }
-
+
+ //foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
+ //{
+ // test.Cmds.AddRange(cs);
+ //}
+
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
|