From 831d6e2a0e63eed436f3cd9d67af69b17941f24b Mon Sep 17 00:00:00 2001 From: schaef Date: Tue, 15 Jun 2010 16:51:23 +0000 Subject: Improved error messages for doomed program points. --- Source/VCGeneration/DoomCheck.ssc | 50 ++- Source/VCGeneration/VCDoomed.ssc | 718 ++++++++++++++++++++++---------------- 2 files changed, 443 insertions(+), 325 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc index 70b026e9..b65f7f24 100644 --- a/Source/VCGeneration/DoomCheck.ssc +++ b/Source/VCGeneration/DoomCheck.ssc @@ -44,6 +44,7 @@ namespace VC public void Initialize(VCExpr! evc) { m_Checker.PushVCExpr(evc); } + public bool CheckReachvar(Variable! reachvar, out ProverInterface.Outcome outcome) { VCExpr! vc = m_Checker.TheoremProver.Context.BoogieExprTranslator.LookupVariable(reachvar); @@ -393,18 +394,18 @@ namespace VC // 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; - } +// 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! traceblocks = new List(); @@ -425,10 +426,7 @@ namespace VC } DetectedBlock.Add(currentNode.EquivBlock); - // Todo: Remove all doomed blocks that are found - // in children. - // Maybe one should remove them only if all children - // are doomed, but this does not affect soundness + } else { Console.WriteLine("An empty equivalence class has been detected"); assert false; @@ -438,10 +436,28 @@ namespace VC currentNode.HasBeenChecked = true; MarkDoomedChildren(currentNode); currentNode = currentNode.Parent; + if (currentNode!=null) { + foreach (InclusionTree! it in currentNode.Children) { + if (!it.HasBeenChecked) { + currentNode = DescendToDeepestUnchecked(it); + break; + } + } + } } } return true; - } + } + + private InclusionTree! DescendToDeepestUnchecked(InclusionTree! node) + { + foreach (InclusionTree! it in node.Children) { + if (!it.HasBeenChecked) { + return DescendToDeepestUnchecked(it); + } + } + return node; + } private bool ECContainsAssertFalse(List! equiv) { foreach (Block! b in equiv) { diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index f3720e7f..50307c0b 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -320,9 +320,10 @@ namespace VC //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) ); + bool __debug = false; watch.Stop(); - Console.WriteLine("Transformations takes: {0}", watch.Elapsed.ToString() ); + if (__debug) Console.WriteLine("Transformation takes: {0}", watch.Elapsed.ToString() ); watch.Reset(); Checker! checker = FindCheckerFor(impl, 1000); @@ -332,14 +333,11 @@ namespace VC int _totalchecks = 0; Block b = null; ProverInterface.Outcome outcome; - dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); - bool doomfound = false; - - bool __debug = true; + dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); System.TimeSpan ts = watch.Elapsed; - while (dc.GetNextBlock(out b) && !doomfound) { + while (dc.GetNextBlock(out b) ) { assert b!=null; outcome = ProverInterface.Outcome.Undetermined; //Console.WriteLine("Checking block {0} ...",b.Label); @@ -347,9 +345,7 @@ namespace VC m_BlockReachabilityMap.TryGetValue(b, out v); assert v!=null; _totalchecks++; - - if (__debug) Console.WriteLine("Checking Block {0}", v.Name); - + watch.Start(); if (!dc.CheckLabel(v, out outcome) ) { @@ -357,13 +353,12 @@ namespace VC } watch.Stop(); ts+=watch.Elapsed; - Console.WriteLine(" --- {0} elapsed", 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: { - doomfound=true; break; } case ProverInterface.Outcome.Invalid: { @@ -379,17 +374,34 @@ namespace VC } checker.Close(); - Console.WriteLine("Number of Checked Blocks: {0}", _totalchecks); + 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()); #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); +// Console.ForegroundColor = ConsoleColor.Red; +// Console.WriteLine(" {0} is DOOMED!", impl.Name); +// foreach (List bl in dc.DoomedSequences) { +// Console.Write("Doomed Blocks: "); +// foreach (Block! b_ in bl) { +// Console.Write("{0}, ", b_.Label); +// } +// Console.WriteLine(); +// } Console.ForegroundColor = col; - SearchCounterexample(impl, dc.ErrorHandler, callback); + int counter=1; + foreach (List! bl in dc.DoomedSequences) { + Console.WriteLine("Doomed program point {0} of {1}", counter++, dc.DoomedSequences.Count); + dc.ErrorHandler.m_DoomedBlocks = bl; + foreach (Block! b_ in bl) { + if (m_BlockReachabilityMap.TryGetValue(b_, out dc.ErrorHandler.m_Reachvar) )break; + } + SearchCounterexample(impl, dc.ErrorHandler, callback); + } + + //SearchCounterexample(impl, dc.ErrorHandler, callback); Console.WriteLine("------------------------------ \n\n"); return Outcome.Errors; } @@ -405,41 +417,19 @@ namespace VC private void SearchCounterexample(Implementation! impl, DoomErrorHandler! errh, VerifierCallback! callback) { if (errh.m_Reachvar==null) { assert false; - return; } m_doomedCmds.Clear(); - - assert errh.m_TraceBlocks != null; - assert errh.m_DoomedBlocks !=null; - List! nondoomed = new List(); - foreach (Block! b in errh.m_DoomedBlocks) { - if (!errh.m_TraceBlocks.Contains(b) ) { - nondoomed.Add(b); - } - } - + Dictionary! cmdbackup = new Dictionary(); BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count/2-1); BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count/2,impl.Blocks.Count-1); - - BlockSeq! trace = new BlockSeq(); - foreach (Block! b in cmdbackup.Keys ) { - trace.Add(b); - } - AssertCmd asrt = null; - foreach (Cmd! c in m_doomedCmds) { - AssertCmd ac = c as AssertCmd; - if (ac!=null) { - asrt=ac; - } + + List! causals = CollectCausalStatements(impl.Blocks[0]); + foreach (Cmd! c in causals ) { + GenerateErrorMessage(c, causals); } - if (asrt==null) { - //callback.OnWarning("Sorry, cannot create counterexample"); - } else { - //AssertCounterexample! ace = new AssertCounterexample(trace, asrt); - //callback.OnCounterexample(ace, "Todo: Build a reason"); - } + #region Undo all modifications foreach (KeyValuePair kvp in cmdbackup) { kvp.Key.Cmds = kvp.Value; @@ -447,6 +437,119 @@ namespace VC #endregion } +#region Causal Statement Tree + + private void GenerateErrorMessage(Cmd! causalStatement, List! causals) + { + AssumeCmd uc = causalStatement as AssumeCmd; + AssertCmd ac = causalStatement as AssertCmd; + ConsoleColor col = Console.ForegroundColor; + + // Trivial case. Must be either assume or assert false + if (m_doomedCmds.Count==1) { + Console.WriteLine("Found a trivial error:" ); + if (uc!=null) { + Console.Write("Trivial false assumption: " ); + Console.Write("({0};{1}):", uc.tok.line, uc.tok.col ); + } + if (ac!=null) { + Console.Write("Trivial false assertion: " ); + Console.Write("({0};{1}):", ac.tok.line, ac.tok.col ); + } + causalStatement.Emit(new TokenTextWriter("", Console.Out, false), 0); + } else { + // Safety error + if (ac!=null) { + Console.ForegroundColor = ConsoleColor.Red; + Console.WriteLine("Safety error:"); + Console.ForegroundColor = col; + Console.Write("This assertion is violated: "); + Console.Write("({0};{1}):", ac.tok.line, ac.tok.col ); + ac.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + if (uc!=null) { + bool containsAssert = false; + foreach (Cmd! c in m_doomedCmds) { + if (causals.Contains(c) ) { + continue; + } + AssertCmd asrt = c as AssertCmd; + if (asrt!=null) { + containsAssert=true; + break; + } + } + // Plausibility error + if (containsAssert) { + Console.ForegroundColor = ConsoleColor.Yellow ; + Console.WriteLine("Plausibility error:"); + Console.ForegroundColor = col; + Console.Write("There is no legal exeuction passing: "); + Console.Write("({0};{1})", uc.tok.line, uc.tok.col ); + uc.Emit(new TokenTextWriter("", Console.Out, false), 0); + } else { // Reachability error + Console.ForegroundColor = ConsoleColor.DarkRed ; + Console.WriteLine("Reachability error:"); + Console.ForegroundColor = col; + Console.Write("No execution can reach: "); + Console.Write("({0};{1})", uc.tok.line, uc.tok.col ); + uc.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + + } + + Console.ForegroundColor = ConsoleColor.White; + Console.WriteLine("...on any execution passing through:"); + foreach (Cmd! c in m_doomedCmds) { + if (causals.Contains(c) ) { + continue; + } + Console.ForegroundColor = col; + Console.Write("In ({0};{1}): ", c.tok.line, c.tok.col ); + Console.ForegroundColor = ConsoleColor.DarkYellow ; + c.Emit(new TokenTextWriter("", Console.Out, false), 0); + } + Console.ForegroundColor = col; + Console.WriteLine("--"); + + } + } + + private List! CollectCausalStatements(Block! b) { + Cmd lastCausal=null; + foreach (Cmd! c in b.Cmds) { + AssertCmd ac = c as AssertCmd; + AssumeCmd uc = c as AssumeCmd; + if (ac!=null && !ContainsReachVariable(ac)) { + if (ac.Expr!=Expr.True) { + lastCausal = c; + } + } else if (uc!=null && !ContainsReachVariable(uc)) { + lastCausal = c; + } + } + + List causals = new List(); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc!=null && gc.labelTargets!=null) { + List tmp; + //bool allcausal = true; + foreach (Block! b_ in gc.labelTargets) { + tmp = CollectCausalStatements(b_); + + foreach (Cmd cau in tmp) { + if (!causals.Contains(cau)) causals.Add(cau); + } + } + //if (allcausal) + if (causals.Count>0) return causals; + } + if (lastCausal!=null) causals.Add( lastCausal); + return causals; + } + +#endregion + bool BruteForceCESearch(Variable! reachvar, Implementation! impl, VerifierCallback! callback, Dictionary! cmdbackup, int startidx, int endidx) { #region Modify implementation @@ -486,13 +589,12 @@ namespace VC if (startidx>=endidx) { // Now we found an interesting Block and we have to // search for the interesting statements. - int cmdcount = impl.Blocks[endidx].Cmds.Length-1; + int cmdcount = impl.Blocks[endidx].Cmds.Length; BruteForceCmd(impl.Blocks[endidx],0,cmdcount/2 -1,reachvar, impl, callback); - BruteForceCmd(impl.Blocks[endidx],cmdcount/2,cmdcount,reachvar, impl, callback); + BruteForceCmd(impl.Blocks[endidx],cmdcount/2,cmdcount-1,reachvar, impl, callback); return true; } else { BruteForceCESearch(reachvar,impl, callback, cmdbackup, startidx, mid); - //if (startidx+mid+1>=endidx) mid--; //Hack BruteForceCESearch(reachvar,impl, callback, cmdbackup, mid+1, endidx); return true; } @@ -539,16 +641,16 @@ namespace VC b.Cmds = backup; if (startidx>=endidx) { if (!ContainsReachVariable(b.Cmds[endidx])) { - Console.Write(" Witness ("); - - ConsoleColor col = Console.ForegroundColor; - Console.ForegroundColor = ConsoleColor.White; - Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col ); - Console.ForegroundColor = col; - Console.Write("): "); - Console.ForegroundColor = ConsoleColor.Yellow; - b.Cmds[endidx].Emit(new TokenTextWriter("", Console.Out, false), 0); - Console.ForegroundColor = col; +// Console.Write(" Witness ("); +// +// ConsoleColor col = Console.ForegroundColor; +// Console.ForegroundColor = ConsoleColor.White; +// Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col ); +// Console.ForegroundColor = col; +// Console.Write("): "); +// Console.ForegroundColor = ConsoleColor.Yellow; +// b.Cmds[endidx].Emit(new TokenTextWriter("", Console.Out, false), 0); +// Console.ForegroundColor = col; m_doomedCmds.Add(b.Cmds[endidx]); return true; @@ -634,13 +736,13 @@ namespace VC out Dictionary copiedblocks) { Block! start = impl.Blocks[0]; - Dictionary gd = new Dictionary(); - Set/*Block*/! beingVisited = new Set/*Block*/(); - GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited); + Dictionary gd = new Dictionary(); + Set/*Block*/! beingVisited = new Set/*Block*/(); + GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited); DCProgramTransformer pt = new DCProgramTransformer(checkableBlocks); - pt.LoopUnrolling(gStart, new Dictionary(), true, ""); - pt.Blocks.Reverse(); + pt.LoopUnrolling(gStart, new Dictionary(), true, ""); + pt.Blocks.Reverse(); copiedblocks = pt.m_copyMap; return pt.Blocks; } @@ -655,262 +757,262 @@ namespace VC #region Loop Unrolling Methods - private Block! LoopUnrolling(GraphNode! node, Dictionary! visited, bool unrollable, String! prefix) - { - Block newb; - if (visited.TryGetValue(node, out newb)) - { - assert newb!=null; - return newb; - } else - { - if (node.IsCutPoint) - { - // compute the loop body and the blocks leaving the loop - - List! loopNodes = new List(); - GatherLoopBodyNodes(node, node, loopNodes); + private Block! LoopUnrolling(GraphNode! node, Dictionary! visited, bool unrollable, String! prefix) + { + Block newb; + if (visited.TryGetValue(node, out newb)) + { + assert newb!=null; + return newb; + } else + { + if (node.IsCutPoint) + { + // compute the loop body and the blocks leaving the loop + + List! loopNodes = new List(); + GatherLoopBodyNodes(node, node, loopNodes); - List! exitNodes = GatherLoopExitNodes(loopNodes); - - // Continue Unrolling after the current loop - Dictionary! _visited = new Dictionary(); - foreach (GraphNode! g in exitNodes) - { - Block b = LoopUnrolling(g, visited, unrollable, prefix); - _visited.Add(g,b); - } - newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix); - visited.Add(node,newb); - } else - { - BlockSeq! newSuccs = new BlockSeq(); - foreach(GraphNode! g in node.Succecessors) - { - newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) ); - } - newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); + List! exitNodes = GatherLoopExitNodes(loopNodes); + + // Continue Unrolling after the current loop + Dictionary! _visited = new Dictionary(); + foreach (GraphNode! g in exitNodes) + { + Block b = LoopUnrolling(g, visited, unrollable, prefix); + _visited.Add(g,b); + } + newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix); + visited.Add(node,newb); + } else + { + BlockSeq! newSuccs = new BlockSeq(); + foreach(GraphNode! g in node.Succecessors) + { + newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) ); + } + newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); Block b; - if (m_copyMap.TryGetValue(node.Block, out b) ) { - assert b!=null; - m_copyMap.Add(newb, b); - } else { - m_copyMap.Add(newb, node.Block); - } - - - assert newb!=null; assert newb.TransferCmd!=null; - if (newSuccs.Length == 0) - newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok); - else - newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs); - - visited.Add(node, newb); - Blocks.Add(newb); - if (unrollable) - { - m_checkableBlocks.Add(newb); - } - } - } - assert newb!=null; - //newb.checkable = unrollable; - return newb; - } + if (m_copyMap.TryGetValue(node.Block, out b) ) { + assert b!=null; + m_copyMap.Add(newb, b); + } else { + m_copyMap.Add(newb, node.Block); + } + + + assert newb!=null; assert newb.TransferCmd!=null; + if (newSuccs.Length == 0) + newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok); + else + newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs); + + visited.Add(node, newb); + Blocks.Add(newb); + if (unrollable) + { + m_checkableBlocks.Add(newb); + } + } + } + assert newb!=null; + //newb.checkable = unrollable; + return newb; + } - private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary! visited, - List! loopNodes, bool unrollable, String! prefix) - { - if (unrollable) - { - Dictionary! visited1 = new Dictionary(visited); - Dictionary! visited2 = new Dictionary(visited); - Dictionary! visited3 = new Dictionary(visited); + private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary! visited, + List! loopNodes, bool unrollable, String! prefix) + { + if (unrollable) + { + Dictionary! visited1 = new Dictionary(visited); + Dictionary! visited2 = new Dictionary(visited); + Dictionary! visited3 = new Dictionary(visited); - Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last"); - - Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last"); - AddHavocCmd(last,loopNodes); - - // You might use true for the unrollable flag as well. - Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb"); - AddHavocCmd(arb,loopNodes); - - - BlockSeq! succ = new BlockSeq(); - succ.Add(last); succ.Add(arb); - assert arb.TransferCmd!=null; - Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ)); - Blocks.Add(tmp); - m_checkableBlocks.Add(tmp); + Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last"); + + Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last"); + AddHavocCmd(last,loopNodes); + + // You might use true for the unrollable flag as well. + Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb"); + AddHavocCmd(arb,loopNodes); + + + BlockSeq! succ = new BlockSeq(); + succ.Add(last); succ.Add(arb); + assert arb.TransferCmd!=null; + Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ)); + Blocks.Add(tmp); + m_checkableBlocks.Add(tmp); // check if arb is already a copy of something else // if not then write to m_copyMap that tmp is a copy // of arb - Block b = null; - if (m_copyMap.TryGetValue(arb,out b) ) { - assert b!=null; - m_copyMap.Add(tmp, b); - } else { - m_copyMap.Add(tmp, arb); - } + Block b = null; + if (m_copyMap.TryGetValue(arb,out b) ) { + assert b!=null; + m_copyMap.Add(tmp, b); + } else { + m_copyMap.Add(tmp, arb); + } - Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First"); - - return first; + Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First"); + + return first; - } else - { - Dictionary! visited_ = new Dictionary(visited); - Block! loopend = AbstractIteration(cutPoint, prefix+"#UR"); - Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix); - AddHavocCmd(ret, loopNodes); - return ret; - } - } - - private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary! visited, bool unrollable, String! prefix) - { - visited.Add(node, nextIter); - Block newb,b; - BlockSeq! newSuccs = new BlockSeq(); - foreach(GraphNode! g in node.Succecessors) - { - newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) ); - } - newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); - if (m_copyMap.TryGetValue(node.Block, out b) ) { - assert b!=null; - m_copyMap.Add(newb, b); - } else { - m_copyMap.Add(newb, node.Block); - } - - assert newb!=null; assert newb.TransferCmd!=null; - if (newSuccs.Length == 0) - newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok); - else - newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs); - - Blocks.Add(newb); - if (unrollable) m_checkableBlocks.Add(newb); - return newb; - } + } else + { + Dictionary! visited_ = new Dictionary(visited); + Block! loopend = AbstractIteration(cutPoint, prefix+"#UR"); + Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix); + AddHavocCmd(ret, loopNodes); + return ret; + } + } + + private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary! visited, bool unrollable, String! prefix) + { + visited.Add(node, nextIter); + Block newb,b; + BlockSeq! newSuccs = new BlockSeq(); + foreach(GraphNode! g in node.Succecessors) + { + newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) ); + } + newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); + if (m_copyMap.TryGetValue(node.Block, out b) ) { + assert b!=null; + m_copyMap.Add(newb, b); + } else { + m_copyMap.Add(newb, node.Block); + } + + assert newb!=null; assert newb.TransferCmd!=null; + if (newSuccs.Length == 0) + newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok); + else + newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs); + + Blocks.Add(newb); + if (unrollable) m_checkableBlocks.Add(newb); + return newb; + } - private Block! AbstractIteration(GraphNode! node, String! prefix) - { - CmdSeq body = new CmdSeq(); - foreach (Cmd! c in node.Body) - { - if (c is PredicateCmd || c is CommentCmd) - body.Add(c ); - else - break; - } - body.Add(new AssumeCmd(node.Block.tok, Expr.False) ); - TransferCmd! tcmd = new ReturnCmd(node.Block.tok); - Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd); - Blocks.Add(b); + private Block! AbstractIteration(GraphNode! node, String! prefix) + { + CmdSeq body = new CmdSeq(); + foreach (Cmd! c in node.Body) + { + if (c is PredicateCmd || c is CommentCmd) + body.Add(c ); + else + break; + } + body.Add(new AssumeCmd(node.Block.tok, Expr.False) ); + TransferCmd! tcmd = new ReturnCmd(node.Block.tok); + Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd); + Blocks.Add(b); Block tmp; - if (m_copyMap.TryGetValue(node.Block, out tmp) ) { - assert tmp!=null; - m_copyMap.Add(b, tmp); - } else { - m_copyMap.Add(b, node.Block); - } - - return b; - } + if (m_copyMap.TryGetValue(node.Block, out tmp) ) { + assert tmp!=null; + m_copyMap.Add(b, tmp); + } else { + m_copyMap.Add(b, node.Block); + } + + return b; + } - private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List! loopNodes, - Dictionary! visited, String! prefix) - { - BlockSeq! newSucc = new BlockSeq(); - Block! orig = cutPoint.Block; - - // detect the block after the loop - // FixMe: What happens when using break commands? - foreach (GraphNode! g in cutPoint.Succecessors) - { - if (!loopNodes.Contains(g)) - { - Block b; - if (visited.TryGetValue(g,out b) ) - newSucc.Add(b); - } - } - TransferCmd tcmd; - assert orig.TransferCmd!=null; - if (newSucc.Length==0) - tcmd = new ReturnCmd(orig.TransferCmd.tok); - else - tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc); - // FixMe: Genertate IToken for counterexample creation - Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd); - Blocks.Add(newb); - m_checkableBlocks.Add(newb); - return newb; - } + private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List! loopNodes, + Dictionary! visited, String! prefix) + { + BlockSeq! newSucc = new BlockSeq(); + Block! orig = cutPoint.Block; + + // detect the block after the loop + // FixMe: What happens when using break commands? + foreach (GraphNode! g in cutPoint.Succecessors) + { + if (!loopNodes.Contains(g)) + { + Block b; + if (visited.TryGetValue(g,out b) ) + newSucc.Add(b); + } + } + TransferCmd tcmd; + assert orig.TransferCmd!=null; + if (newSucc.Length==0) + tcmd = new ReturnCmd(orig.TransferCmd.tok); + else + tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc); + // FixMe: Genertate IToken for counterexample creation + Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd); + Blocks.Add(newb); + m_checkableBlocks.Add(newb); + return newb; + } - private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List! loopNodes) - { - loopNodes.Add(current); - if (false) System.Diagnostics.Debugger.Break(); - foreach (GraphNode! g in current.Predecessors) - { - if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue; - GatherLoopBodyNodes(g, cutPoint, loopNodes); - } - } - - private List! GatherLoopExitNodes(List! loopNodes) - { - List! exitnodes = new List(); - - foreach (GraphNode! g in loopNodes) - { - foreach (GraphNode! s in g.Succecessors) - { - if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s); - } - } - return exitnodes; - } - - private void AddHavocCmd(Block! b, List! loopNodes) - { - List! loopBlocks = new List(); - foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block); - HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok); - CmdSeq! body = new CmdSeq(); - body.Add(hcmd); - body.AddRange(b.Cmds); - b.Cmds = body; - } + private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List! loopNodes) + { + loopNodes.Add(current); + if (false) System.Diagnostics.Debugger.Break(); + foreach (GraphNode! g in current.Predecessors) + { + if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue; + GatherLoopBodyNodes(g, cutPoint, loopNodes); + } + } + + private List! GatherLoopExitNodes(List! loopNodes) + { + List! exitnodes = new List(); + + foreach (GraphNode! g in loopNodes) + { + foreach (GraphNode! s in g.Succecessors) + { + if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s); + } + } + return exitnodes; + } + + private void AddHavocCmd(Block! b, List! loopNodes) + { + List! loopBlocks = new List(); + foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block); + HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok); + CmdSeq! body = new CmdSeq(); + body.Add(hcmd); + body.AddRange(b.Cmds); + b.Cmds = body; + } - private HavocCmd! HavocLoopTargets(List! bl, IToken! tok) - { - VariableSeq varsToHavoc = new VariableSeq(); - foreach ( Block! b in bl ) - { - foreach ( Cmd! c in b.Cmds ) - { - c.AddAssignedVariables(varsToHavoc); - } - } - IdentifierExprSeq havocExprs = new IdentifierExprSeq(); - foreach ( Variable! v in varsToHavoc ) - { - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - if(!havocExprs.Has(ie)) - havocExprs.Add(ie); - } - // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct - // the source location for this later on - return new HavocCmd(tok,havocExprs); - } - + private HavocCmd! HavocLoopTargets(List! bl, IToken! tok) + { + VariableSeq varsToHavoc = new VariableSeq(); + foreach ( Block! b in bl ) + { + foreach ( Cmd! c in b.Cmds ) + { + c.AddAssignedVariables(varsToHavoc); + } + } + IdentifierExprSeq havocExprs = new IdentifierExprSeq(); + foreach ( Variable! v in varsToHavoc ) + { + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + if(!havocExprs.Has(ie)) + havocExprs.Add(ie); + } + // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct + // the source location for this later on + return new HavocCmd(tok,havocExprs); + } + #endregion @@ -1009,7 +1111,7 @@ namespace VC assume gcmd.labelTargets != null; foreach (Block! succ in gcmd.labelTargets) { - g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) ); + g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) ); } } beingVisited.Remove(b); @@ -1020,17 +1122,17 @@ namespace VC } } - #endregion + #endregion #endregion #region Program Passification private void GenerateReachVars(Implementation! impl) { - Hashtable gotoCmdOrigins = new Hashtable(); - Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); - AddBlocksBetween(impl); - + Hashtable gotoCmdOrigins = new Hashtable(); + Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); + AddBlocksBetween(impl); + #region Insert pre- and post-conditions and where clauses as assume and assert statements { CmdSeq cc = new CmdSeq(); -- cgit v1.2.3