From ab87233468809af35868c31e85c3144cfd90731e Mon Sep 17 00:00:00 2001 From: schaef Date: Sun, 27 Mar 2011 11:02:18 +0000 Subject: Minor fixes --- Source/VCGeneration/DoomedStrategy.cs | 207 +++++++++++++++++++++++----------- 1 file changed, 140 insertions(+), 67 deletions(-) (limited to 'Source/VCGeneration/DoomedStrategy.cs') 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/*!*/>/*!*/ DetectedBlock = new List/*!*/>(); + private List __DEBUG_minelements = new List(); + // There is no default constructor, because these parameters are needed for most subclasses public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List 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 lb) { + sw.Start(); if (m_Current < m_Blocks.Count) { lb = new List(); @@ -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 m_Uncheckedlocks = new List(); @@ -312,26 +312,113 @@ namespace VC public PathCoverStrategy(Implementation imp, Block unifiedexit, List 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 lb) + { + sw.Start(); + + lb = new List(); + + 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 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 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 unreach, bool test_alternativeK) + + } + #endregion + + #region Path Cover Optimization with K + internal class PathCoverStrategyK : DoomDetectionStrategy + { + List m_Uncheckedlocks = new List(); + List m_Ignore = new List(); + + Random m_Random = new Random(); + bool m_NoMoreMoves = false; + + private List m_foundBlock = new List(); + + public PathCoverStrategyK(Implementation imp, Block unifiedexit, List 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 lb) { + sw.Start(); + lb = new List(); 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 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 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; } -- cgit v1.2.3