From 2638d7607aa02c36c0ec6a5228049c643b3696e3 Mon Sep 17 00:00:00 2001 From: schaef Date: Thu, 28 Jan 2010 15:56:09 +0000 Subject: Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebug.bpl --- Source/VCGeneration/VCDoomed.ssc | 297 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 286 insertions(+), 11 deletions(-) (limited to 'Source/VCGeneration/VCDoomed.ssc') diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index 775cd9e0..7a235424 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -37,6 +37,213 @@ namespace VC m_BlockReachabilityMap = new Dictionary(); } + + private void Impl2Dot(Implementation! impl, string! filename) { + List! nodes = new List(); + List! edges = new List(); + + string nodestyle = "[shape=box];" ; + + foreach (Block! b in impl.Blocks) { + nodes.Add(string.Format("\"{0}\" {1}", b.Label, nodestyle) ); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc!=null) { + assert gc.labelTargets!=null; + foreach (Block! b_ in gc.labelTargets) { + edges.Add(String.Format("\"{0}\" -> \"{1}\";", b.Label, b_.Label ) ); + } + } + } + + using (StreamWriter sw = new StreamWriter(filename)) + { + sw.WriteLine(String.Format("digraph {0} {{", impl.Name)); +// foreach (string! s in nodes) { +// sw.WriteLine(s); +// } + foreach (string! s in edges) { + sw.WriteLine(s); + } + sw.WriteLine("}}"); + sw.Close(); + } + } + + private const string _copyPrefix = "Yeah"; + + private Block! CopyImplBlocks(Block! b, ref List! blocklist, Block! targetBlock, ref Dictionary! alreadySeen) { + Block seen; + if (alreadySeen.TryGetValue(b, out seen) ) { + assert seen!=null; + return seen; + } + + GotoCmd gc = b.TransferCmd as GotoCmd; + TransferCmd tcmd = null; + if (gc!=null) { + BlockSeq! bseq = new BlockSeq(); + assert gc.labelTargets!=null; + foreach (Block! c in gc.labelTargets) { + bseq.Add(CopyImplBlocks(c, ref blocklist, targetBlock, ref alreadySeen)); + } + tcmd = new GotoCmd(gc.tok, bseq); + } else { +// BlockSeq! bseq_ = new BlockSeq(); +// bseq_.Add(targetBlock); + 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) { + if (!ContainsReachVariable(_c)) + cl.Add( codeCopier.CopyCmd(_c)); + } + + Block! b_ = new Block(b.tok, b.Label+_copyPrefix, cl, tcmd); + 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) { + GotoCmd gc = b.TransferCmd as GotoCmd; + + if (gc!=null) { + assert gc.labelTargets!=null; + foreach (Block! gt in gc.labelTargets) { + if (gt==target) { + assert gc.labelTargets.Length==1; + assert gc.labelTargets[0]!=null; + b.TransferCmd = new ReturnCmd(gc.tok); + return; + } else { + RemoveArtificialGoto(gt, target); + } + } + + } + } + + static public bool UseItAsDebugger = false; + +// public static Implementation _tmpImpl = null; // (MsSchaef) HACK! + + public static Block firstNonDebugBlock = null; + public static Block firstDebugBlock = null; + + private void ModifyImplForDebugging(Implementation! impl) + { + //List 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! blist = new List(); + Dictionary! tmpdict = new Dictionary(); + 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(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(); + impl.Blocks.Add(newfirst); + impl.Blocks.AddRange(blist); + + Impl2Dot(impl, String.Format("c:/dot/{0}_copied.dot", impl.Name) ); + #endregion + } + } + + void RemoveReachVars(Block! b) { + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc!=null) { + assert gc.labelTargets!=null; + + CmdSeq! cs = new CmdSeq(); + foreach (Cmd! c in b.Cmds) { + if (!ContainsReachVariable(c)) cs.Add(c); + } + b.Cmds = cs; + + foreach (Block! c in gc.labelTargets) { + if (c.Label != "GeneratedUnifiedExit") { + RemoveReachVars(c); + } + } + } + } + + void RemoveLastBlock(Block! b) + { + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc==null) { + //Console.WriteLine("WARNING: Check Node {0}", b.Label); + return; + } + assert gc!=null; + assert gc.labelTargets !=null; + BlockSeq! tmp = new BlockSeq(); + foreach (Block! c in gc.labelTargets) { + // 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) { + _copiedBlock.Add(b); + GotoCmd gc = b.TransferCmd as GotoCmd; + if (gc!=null) { + assert gc.labelTargets!=null; + foreach (Block! c in gc.labelTargets) { + FindCopiedBlocks(c); + } + } + } + + private List! _copiedBlock = new List(); + /// /// MSchaef: /// - remove loops and add reach variables @@ -47,13 +254,24 @@ namespace VC /// public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback) throws UnexpectedProverOutputException; - { + { + + UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug; + Stopwatch watch = new Stopwatch(); + + //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) ); + if (CommandLineOptions.Clo.TraceVerify) { Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name); } Console.WriteLine("Checking function {0} for doomed points:", 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(); @@ -64,21 +282,63 @@ namespace VC Dictionary copiedblocks; impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks, out copiedblocks); assert copiedblocks!=null; + +// List! blist = new List(); +// blist.AddRange(impl.Blocks); + + if (UseItAsDebugger) ModifyImplForDebugging(impl); + ComputePredecessors(impl.Blocks); - + m_BlockReachabilityMap = new Dictionary(); - PassifyProgram(impl, program); + GenerateReachVars(impl); + + if (UseItAsDebugger) RemoveReachVars((!)firstDebugBlock); + + PassifyProgram(impl); + + #endregion - //EmitImpl(impl,false); + //EmitImpl(impl,false); + + + //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) ); + +// --------------------------------------------------------------------------- + if (UseItAsDebugger) { + 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) ); + + + watch.Stop(); + Console.WriteLine("Transformations takes: {0}", watch.Elapsed.ToString() ); + watch.Reset(); Checker! checker = FindCheckerFor(impl, 1000); DoomCheck dc = new DoomCheck(impl, checker); + int _totalchecks = 0; Block b = null; ProverInterface.Outcome outcome; dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback); bool doomfound = false; + + bool __debug = true; + + System.TimeSpan ts = watch.Elapsed; + while (dc.GetNextBlock(out b) && !doomfound) { assert b!=null; outcome = ProverInterface.Outcome.Undetermined; @@ -87,9 +347,19 @@ 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) ) { return Outcome.Inconclusive; } + watch.Stop(); + ts+=watch.Elapsed; + Console.WriteLine(" --- {0} elapsed", watch.Elapsed.ToString()); + watch.Reset(); + switch (outcome) { case ProverInterface.Outcome.Valid: { @@ -117,7 +387,7 @@ namespace VC ConsoleColor col = Console.ForegroundColor; Console.ForegroundColor = ConsoleColor.Red; Console.WriteLine(" {0} is DOOMED!", impl.Name); - Console.ForegroundColor = col; + Console.ForegroundColor = col; SearchCounterexample(impl, dc.ErrorHandler, callback); Console.WriteLine("------------------------------ \n\n"); @@ -130,6 +400,8 @@ namespace VC return Outcome.Correct; } + + private void SearchCounterexample(Implementation! impl, DoomErrorHandler! errh, VerifierCallback! callback) { if (errh.m_Reachvar==null) { assert false; @@ -179,6 +451,7 @@ namespace VC Dictionary! cmdbackup, int startidx, int endidx) { #region Modify implementation for (int i=startidx; i<=endidx; i++) { + if (_copiedBlock.Contains(impl.Blocks[i])) continue; CmdSeq! cs = new CmdSeq(); cmdbackup.Add(impl.Blocks[i],impl.Blocks[i].Cmds); foreach (Cmd! c in impl.Blocks[i].Cmds) { @@ -752,10 +1025,8 @@ namespace VC #endregion #region Program Passification - - private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl, - Program! program) - { + private void GenerateReachVars(Implementation! impl) + { Hashtable gotoCmdOrigins = new Hashtable(); Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); AddBlocksBetween(impl); @@ -801,8 +1072,12 @@ namespace VC exitBlock = (!)gc.labelTargets[0]; } #endregion - GenerateReachabilityPredicates(impl, exitBlock); - + GenerateReachabilityPredicates(impl, exitBlock); + } + + + private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl) + { current_impl = impl; Convert2PassiveCmd(impl); impl = current_impl; -- cgit v1.2.3