diff options
| -rw-r--r-- | Source/VCGeneration/DoomCheck.ssc | 39 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomErrorHandler.ssc | 47 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.ssc | 9 | ||||
| -rw-r--r-- | Test/doomed/doomed.bpl | 4 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 18 |
5 files changed, 110 insertions, 7 deletions
diff --git a/Source/VCGeneration/DoomCheck.ssc b/Source/VCGeneration/DoomCheck.ssc index ecefedea..492f333c 100644 --- a/Source/VCGeneration/DoomCheck.ssc +++ b/Source/VCGeneration/DoomCheck.ssc @@ -233,7 +233,7 @@ namespace VC public InclusionOrder(Implementation! impl) {
/*
We now compute for each block the set of blocks that
- are reached on every execution reaching this block.
+ are reached on every execution reaching this block (dominator).
We first compute it form the start block to the current
block and second from the Term block to the current one.
Finally we build the union.
@@ -292,16 +292,49 @@ namespace VC return false;
}
+
+ /*
+ Warning: this is a very slow implementation. There should be
+ a map from Block to InclusionTree to prevent running through
+ the tree over and over again.
+ */
+ private void MarkUndoomedFromCE(Block! b, InclusionTree! node)
+ {
+ if (node.EquivBlock.Contains(b) ) {
+ //Console.WriteLine("Block {0} does not need to be checked - appears in CE", b.Label);
+ node.HasBeenChecked = true;
+ node.IsDoomed = false;
+ MarkUndoomedParents(node);
+ return;
+ } else
+ {
+ foreach (InclusionTree! c in node.Children)
+ {
+ MarkUndoomedFromCE(b, c);
+ }
+ }
+ }
+
// Takes the outcome for the current reachvar and marks all blocks
// the do not need any further checking because they share the same
// desteny
- // returns false if an explicite assert false was found.
+ // returns false if an explicite assert false was found.
+ // Warning: Still slow; we do not need to do this while constructing the error report!
public bool SetCurrentResult(Variable! reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb) {
if (outcome!=ProverInterface.Outcome.Valid) {
if (currentNode != null) {
currentNode.IsDoomed = false;
currentNode.HasBeenChecked = true;
- MarkUndoomedParents(currentNode);
+ MarkUndoomedParents(currentNode);
+ if (cb != null) {
+ foreach (Block! b in cb.TraceNodes)
+ {
+ MarkUndoomedFromCE(b, RootNode);
+ }
+ } else {
+ Console.WriteLine("ErrorHandler is not valid! ------ (DoomCheck)");
+ }
+
currentNode = FindNextNode(currentNode);
}
} else {
diff --git a/Source/VCGeneration/DoomErrorHandler.ssc b/Source/VCGeneration/DoomErrorHandler.ssc index 08bc2217..860f5334 100644 --- a/Source/VCGeneration/DoomErrorHandler.ssc +++ b/Source/VCGeneration/DoomErrorHandler.ssc @@ -41,6 +41,53 @@ namespace VC m_DoomedBlocks = doomedblocks;
m_TraceBlocks = traceblocks;
}
+
+ private List<Block!>! m_CurrentTrace = new List<Block!>();
+
+ public List<Block!>! TraceNodes
+ {
+ get
+ {
+ return m_CurrentTrace;
+ }
+ }
+
+ public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+ m_CurrentTrace.Clear();
+ //Console.Write("Used Blocks: ");
+ List<Block!> traceNodes = new List<Block!>();
+ List<AssertCmd!> assertNodes = new List<AssertCmd!>();
+ foreach (string! s in labels) {
+ Absy node = Label2Absy(s);
+ if (node is Block) {
+ Block b = (Block)node;
+ traceNodes.Add(b);
+ //Console.Write("{0}, ", b.Label);
+ } else {
+ AssertCmd a = (AssertCmd)node;
+ assertNodes.Add(a);
+ }
+ }
+ m_CurrentTrace.AddRange(traceNodes);
+ //Console.WriteLine();
+// assert assertNodes.Count > 0;
+// assert traceNodes.Count == assertNodes.Count;
+//
+// foreach (AssertCmd a in assertNodes) {
+// // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)
+// foreach (Block b in traceNodes) {
+// if (b.Cmds.Has(a)) {
+// BlockSeq trace = new BlockSeq();
+// trace.Add(b);
+// goto NEXT_ASSERT;
+// }
+// }
+// assert false; // there was no block that contains the assert
+// NEXT_ASSERT: {}
+// }
+
+ }
+
}
}
\ No newline at end of file diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc index fc3d35f7..775cd9e0 100644 --- a/Source/VCGeneration/VCDoomed.ssc +++ b/Source/VCGeneration/VCDoomed.ssc @@ -74,7 +74,7 @@ namespace VC 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);
@@ -82,11 +82,11 @@ namespace VC while (dc.GetNextBlock(out b) && !doomfound) {
assert b!=null;
outcome = ProverInterface.Outcome.Undetermined;
-
+ //Console.WriteLine("Checking block {0} ...",b.Label);
Variable v = null;
m_BlockReachabilityMap.TryGetValue(b, out v);
assert v!=null;
-
+ _totalchecks++;
if (!dc.CheckLabel(v, out outcome) ) {
return Outcome.Inconclusive;
}
@@ -108,6 +108,9 @@ namespace VC }
checker.Close();
+
+ Console.WriteLine("Number of Checked Blocks: {0}", _totalchecks);
+
#region Try to produce a counter example (brute force)
if (dc.DoomedSequences.Count>0 ) {
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl index 77eec249..741a54c5 100644 --- a/Test/doomed/doomed.bpl +++ b/Test/doomed/doomed.bpl @@ -21,7 +21,9 @@ procedure evilbranch(x:int) } else {
y := 2;
}
- assert y!=2;
+ assume y!=2;
+
+ assert x<0;
}
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl index eb60536f..c3193a01 100644 --- a/Test/doomed/notdoomed.bpl +++ b/Test/doomed/notdoomed.bpl @@ -35,5 +35,23 @@ procedure c(x:int) }
}
+procedure useCE(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+ if(x<7) {
+ y := 5;
+ } else {
+ y := 6;
+ }
+
+}
+
+
|