diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 9 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomCheck.ssc | 81 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 297 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.ssc | 1 | ||||
| -rw-r--r-- | Test/doomed/doomdebug.bpl | 44 |
5 files changed, 405 insertions, 27 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 5912220d..aa07ec41 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -159,6 +159,7 @@ namespace Microsoft.Boogie public enum VCVariety { Structured, Block, Local, BlockNested, BlockReach, BlockNestedReach, Dag, Doomed, Unspecified }
public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed
+ public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set
public bool RemoveEmptyBlocks = true;
@@ -819,7 +820,12 @@ namespace Microsoft.Boogie }
}
break;
-
+
+ case "/DoomDebug":
+ vcVariety = VCVariety.Doomed;
+ useDoomDebug = true;
+ break;
+
case "-vc":
case "/vc":
if (ps.ConfirmArgumentCount(1)) {
@@ -1818,6 +1824,7 @@ namespace Microsoft.Boogie b = flat block, r = flat block reach,
s = structured, l = local, d = dag (default with /prover:z3)
doomed = doomed
+ /DoomDebug : Use Doom detection to debug (experimental)
/traceverify : print debug output during verification condition generation
/subsumption:<c> : apply subsumption to asserted conditions:
0 - never, 1 - not for quantifiers, 2 (default) - always
diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc index 492f333c..70b026e9 100644 --- a/Source/VCGeneration/DoomCheck.ssc +++ b/Source/VCGeneration/DoomCheck.ssc @@ -82,18 +82,20 @@ namespace VC }
}
- private DoomErrorHandler m_ErrHandler;
- private Implementation! m_PassiveImpl;
+ private DoomErrorHandler m_ErrHandler;
private Checker! m_Check;
private InclusionOrder! m_Order;
private Evc! m_Evc;
#endregion
[NotDelayed]
- public DoomCheck (Implementation! passive_impl, Checker! check) {
- m_PassiveImpl = passive_impl;
- m_Check = check;
- m_Order = new InclusionOrder(passive_impl);
+ public DoomCheck (Implementation! passive_impl, Checker! check) {
+ m_Check = check;
+ if (!VC.DCGen.UseItAsDebugger ) {
+ m_Order = new InclusionOrder(passive_impl.Blocks[0]);
+ } else {
+ m_Order = new InclusionOrder((!)VC.DCGen.firstNonDebugBlock );
+ }
Label2Absy = new Hashtable(); // This is only a dummy
m_Evc = new Evc(check);
base();
@@ -101,6 +103,7 @@ namespace VC VCExpr! vce = this.GenerateEVC(passive_impl, out l2a, check);
assert l2a!=null;
Label2Absy = l2a;
+// vce = check.VCExprGen.Implies(vce, vce);
m_Evc.Initialize(vce);
}
@@ -138,7 +141,17 @@ namespace VC #region Error Verification Condition Generation
-
+ /*
+ #region _TESTING_NEW_STUFF_
+ CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;
+ //VCExpr wp = Wlp.Block(block, SuccCorrect, context); // Computes wp.S.true
+
+ CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;
+ #endregion
+
+ */
+ private bool _tmpUseFreshBVars;
+
VCExpr! GenerateEVC(Implementation! impl, out Hashtable label2absy, Checker! ch)
{
TypecheckingContext tc = new TypecheckingContext(null);
@@ -147,15 +160,48 @@ namespace VC VCExpr! vc;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Doomed:
- vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+
+ if (!VC.DCGen.UseItAsDebugger ) {
+ vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);
+ }
+ #region _TESTING_NEW_STUFF_
+ else {
+
+
+ CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Block;
+ assert VC.DCGen.firstDebugBlock != null;
+ VCExpr! a = LetVC(VC.DCGen.firstDebugBlock, label2absy, ch.TheoremProver.Context);
+ CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Doomed;
+
+
+ VCExpr! b = LetVC((!)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
+
break;
+
default:
assert false; // unexpected enumeration value
}
return vc;
}
- VCExpr! LetVC(Block! startBlock,
+ public VCExpr! LetVC(Block! startBlock,
Hashtable/*<int, Absy!>*/! label2absy,
ProverContext! proverCtxt)
{
@@ -204,9 +250,11 @@ namespace VC VCContext context = new VCContext(label2absy, proverCtxt);
// m_Context = context;
+
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+
+ v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
- v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
bindings.Add(gen.LetBinding(v, vc));
blockVariables.Add(block, v);
}
@@ -223,14 +271,14 @@ namespace VC #region Attributes
public List<List<Block!>!>! DetectedBlock = new List<List<Block!>!>();
- Implementation! m_Impl;
+
InclusionTree! RootNode = new InclusionTree(null);
InclusionTree currentNode = null;
#endregion
[NotDelayed]
- public InclusionOrder(Implementation! impl) {
+ public InclusionOrder(Block! rootblock) {
/*
We now compute for each block the set of blocks that
are reached on every execution reaching this block (dominator).
@@ -238,14 +286,14 @@ namespace VC block and second from the Term block to the current one.
Finally we build the union.
*/
- m_Impl = impl;
+
base();
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(impl.Blocks[0], map2);
+ Block! exitblock = BreadthFirst(rootblock, map2);
BreadthFirstBwd(exitblock, map);
foreach (KeyValuePair<Block!, TraceNode!> kvp in map) {
@@ -264,7 +312,7 @@ namespace VC kvp.Value.Add(t0.block);
}
} else {
- assert false;
+ //assert false;
}
}
@@ -327,10 +375,13 @@ namespace VC currentNode.HasBeenChecked = true;
MarkUndoomedParents(currentNode);
if (cb != null) {
+ //Console.WriteLine("CE contains: ");
foreach (Block! b in cb.TraceNodes)
{
+ //Console.Write("{0}, ", b.Label);
MarkUndoomedFromCE(b, RootNode);
}
+ //Console.WriteLine();
} else {
Console.WriteLine("ErrorHandler is not valid! ------ (DoomCheck)");
}
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<Block, Variable!>();
}
+
+ private void Impl2Dot(Implementation! impl, string! filename) {
+ List<string!>! nodes = new List<string!>();
+ List<string!>! edges = new List<string!>();
+
+ 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<Block!>! blocklist, Block! targetBlock, ref Dictionary<Block!, Block!>! 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<Block!> 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<Block!>! blist = new List<Block!>();
+ Dictionary<Block!, Block!>! tmpdict = new Dictionary<Block!, Block!>();
+ 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<Block!>(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<Block!>();
+ 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<Block!>! _copiedBlock = new List<Block!>();
+
/// <summary>
/// MSchaef:
/// - remove loops and add reach variables
@@ -47,13 +254,24 @@ namespace VC /// </summary>
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<Incarnation, Absy!>();
@@ -64,21 +282,63 @@ namespace VC Dictionary<Block!, Block!> copiedblocks;
impl.Blocks = DCProgramTransformer.Convert2Dag(impl, program, cblocks, out copiedblocks);
assert copiedblocks!=null;
+
+// List<Block!>! blist = new List<Block!>();
+// blist.AddRange(impl.Blocks);
+
+ if (UseItAsDebugger) ModifyImplForDebugging(impl);
+
ComputePredecessors(impl.Blocks);
-
+
m_BlockReachabilityMap = new Dictionary<Block, Variable!>();
- 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<Block!, CmdSeq!>! 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;
diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc index d7692245..9700bc89 100644 --- a/Source/VCGeneration/Wlp.ssc +++ b/Source/VCGeneration/Wlp.ssc @@ -85,6 +85,7 @@ namespace VC { return gen.Implies(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
} else {
+ Console.WriteLine(cmd.ToString());
assert false; // unexpected command
}
}
diff --git a/Test/doomed/doomdebug.bpl b/Test/doomed/doomdebug.bpl new file mode 100644 index 00000000..0f45c13c --- /dev/null +++ b/Test/doomed/doomdebug.bpl @@ -0,0 +1,44 @@ +procedure badtrace(x:int, y:int, z:int)
+{
+ var xin : int;
+ xin := x+z;
+
+
+ if (y>5) {
+ xin:=5;
+ } else {
+ assert xin != x;
+ }
+}
+
+procedure baddiamond(x:int, y:int, z:int)
+{
+ var xin : int;
+ var yin : int;
+ var zin : int;
+ xin := x;
+ yin := y;
+ zin := z;
+
+ if (y<5) {
+ xin := xin -3;
+ } else {
+ zin := zin +10;
+ xin := 0;
+ }
+
+ if (x<100) {
+ yin := 3;
+ } else {
+ zin := 5;
+ }
+
+ if (z>5) {
+ yin := yin - 2;
+ xin := xin + 3;
+ }
+
+ zin:=zin+yin;
+
+ assert xin!=x;
+}
|