diff options
author | schaef <unknown> | 2009-11-19 13:47:20 +0000 |
---|---|---|
committer | schaef <unknown> | 2009-11-19 13:47:20 +0000 |
commit | eaf052fa512f87a16d16cbb6b4c78e7fbaaf85b8 (patch) | |
tree | f77c8514aa6c6ecbaed9b3c75d1815a79df1c67c /Source | |
parent | 62069bee7147d2f5ef620c0309ef1048ca95d0a7 (diff) |
doomed stuff: minor bug fixes / improved output / more test cases
Diffstat (limited to 'Source')
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 18 | ||||
-rw-r--r-- | Source/VCGeneration/DoomCheck.ssc | 9 | ||||
-rw-r--r-- | Source/VCGeneration/DoomErrorHandler.ssc | 2 | ||||
-rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 61 |
4 files changed, 67 insertions, 23 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 6eb16fa4..b9f3d5b2 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -272,7 +272,11 @@ namespace Microsoft.Boogie requires 0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories;
{
Console.WriteLine();
- Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");
+ } else {
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.ToolName, verified, errors, errors == 1 ? "" : "s");
+ }
if (inconclusives != 0) {
Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
}
@@ -517,8 +521,8 @@ namespace Microsoft.Boogie assert false; // unexpected outcome
case VCGen.Outcome.Correct:
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- Inform(String.Format("{0}doomed", timeIndication));
- errorCount++;
+ Inform(String.Format("{0}credible", timeIndication));
+ verified++;
} else {
Inform(String.Format("{0}verified", timeIndication));
verified++;
@@ -538,9 +542,9 @@ namespace Microsoft.Boogie break;
case VCGen.Outcome.Errors:
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
- Inform(String.Format("{0}credible", timeIndication));
- verified++;
- } else {
+ Inform(String.Format("{0}doomed", timeIndication));
+ errorCount++;
+ } //else {
assert errors != null; // guaranteed by postcondition of VerifyImplementation
if (errorReporter != null)
{
@@ -637,7 +641,7 @@ namespace Microsoft.Boogie }
errorCount++;
}
- }
+ //}
Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
}
break;
diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc index e888d115..cdbdcb6a 100644 --- a/Source/VCGeneration/DoomCheck.ssc +++ b/Source/VCGeneration/DoomCheck.ssc @@ -309,8 +309,13 @@ 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)) {
+ if (ECContainsAssertFalse(currentNode.EquivBlock)) {
+
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Blue;
Console.WriteLine("Assert false was detected, but ignored");
+ Console.ForegroundColor = col;
+
currentNode.HasBeenChecked = true;
currentNode.IsDoomed = false;
currentNode = currentNode.Parent;
@@ -324,7 +329,7 @@ namespace VC // cb.OnWarning("Doomed program points found!");
if (cb != null) {
- cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
+ cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
}
if (currentNode.EquivBlock.Count>0) {
diff --git a/Source/VCGeneration/DoomErrorHandler.ssc b/Source/VCGeneration/DoomErrorHandler.ssc index 6c8a7ec7..08bc2217 100644 --- a/Source/VCGeneration/DoomErrorHandler.ssc +++ b/Source/VCGeneration/DoomErrorHandler.ssc @@ -39,7 +39,7 @@ namespace VC public void OnDoom(Variable! reachvar, List<Block!>! doomedblocks, List<Block!>! traceblocks) {
m_Reachvar = reachvar;
m_DoomedBlocks = doomedblocks;
- m_TraceBlocks = traceblocks;
+ m_TraceBlocks = traceblocks;
}
}
diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index 84df1be4..fc3d35f7 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -24,6 +24,7 @@ namespace VC private Dictionary<Block, Variable!>! m_BlockReachabilityMap;
Dictionary<Block!, Block!>! m_copiedBlocks = new Dictionary<Block!, Block!>();
const string reachvarsuffix = "__ivebeenthere";
+ List<Cmd!>! m_doomedCmds = new List<Cmd!>();
#endregion
/// <summary>
/// Constructor. Initializes the theorem prover.
@@ -50,7 +51,7 @@ namespace VC if (CommandLineOptions.Clo.TraceVerify) {
Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);
}
- 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);
#region Transform the Program into loop-free passive form
@@ -91,8 +92,7 @@ namespace VC }
switch (outcome) {
- case ProverInterface.Outcome.Valid: {
- Console.WriteLine("[x] {0} is doomed", v.Name);
+ case ProverInterface.Outcome.Valid: {
doomfound=true;
break;
}
@@ -108,11 +108,22 @@ namespace VC }
checker.Close();
-
+ #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 = col;
+
SearchCounterexample(impl, dc.ErrorHandler, callback);
+ Console.WriteLine("------------------------------ \n\n");
+ return Outcome.Errors;
}
- Console.WriteLine();
+ #endregion
+
+ Console.WriteLine("------------------------------ \n\n");
+
return Outcome.Correct;
}
@@ -121,10 +132,8 @@ namespace VC assert false;
return;
}
- Console.WriteLine("{0} is doomed due to the following statements:", errh.m_Reachvar.Name );
-
- // modify the impl
-
+ m_doomedCmds.Clear();
+
assert errh.m_TraceBlocks != null;
assert errh.m_DoomedBlocks !=null;
List<Block!>! nondoomed = new List<Block!>();
@@ -138,8 +147,24 @@ namespace VC 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;
+ }
+ }
+ 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<Block!, CmdSeq!> kvp in cmdbackup) {
kvp.Key.Cmds = kvp.Value;
@@ -237,9 +262,19 @@ namespace VC } else if (outcome == ProverInterface.Outcome.Invalid) {
b.Cmds = backup;
if (startidx>=endidx) {
- if (!ContainsReachVariable(b.Cmds[endidx])) {
- Console.Write("Candidate L{0}: ", b.Cmds[endidx].tok.line );
- b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
+ 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>", Console.Out, false), 0);
+ Console.ForegroundColor = col;
+
+ m_doomedCmds.Add(b.Cmds[endidx]);
return true;
} else {
return false;
|