diff options
author | MichalMoskal <unknown> | 2010-12-17 00:33:23 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2010-12-17 00:33:23 +0000 |
commit | 5b6a6e266c32f211c9f1ceff1d9605592b2016dd (patch) | |
tree | 92cbb7d5189293a0a421e3273cbb0ff7f39ae13a | |
parent | 12c28b0c769090a4d444cd31d7e871f707dd06a1 (diff) |
Add new feature: {:selective_checking} on procedures. See testcase for a description (it was implemented in VCC before and is quite useful).
-rw-r--r-- | Source/VCGeneration/VC.cs | 58 | ||||
-rw-r--r-- | Test/test2/Answer | 18 | ||||
-rw-r--r-- | Test/test2/SelectiveChecking.bpl | 49 | ||||
-rw-r--r-- | Test/test2/runtest.bat | 2 |
4 files changed, 124 insertions, 3 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 18d4791f..54bd5358 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -16,7 +16,6 @@ using System.Diagnostics.Contracts; using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
-
namespace VC {
using Bpl = Microsoft.Boogie;
@@ -2274,7 +2273,8 @@ namespace VC { if (axioms.Count > 0) {
CmdSeq cmds = new CmdSeq();
- foreach (Expr ax in axioms) {Contract.Assert(ax != null);
+ foreach (Expr ax in axioms) {
+ Contract.Assert(ax != null);
cmds.Add(new AssumeCmd(ax.tok, ax));
}
Block entryBlock = cce.NonNull( impl.Blocks[0]);
@@ -2283,6 +2283,7 @@ namespace VC { }
}
+ HandleSelectiveChecking(impl);
// #region Constant Folding
@@ -2298,6 +2299,59 @@ namespace VC { return gotoCmdOrigins;
}
+ private static void HandleSelectiveChecking(Implementation impl)
+ {
+ if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
+ QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "selective_checking")) {
+
+ var startPoints = new List<Block>();
+ foreach (var b in impl.Blocks) {
+ foreach (Cmd c in b.Cmds) {
+ var p = c as PredicateCmd;
+ if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) {
+ startPoints.Add(b);
+ break;
+ }
+ }
+ }
+
+ var blocksToCheck = new HashSet<Block>();
+ foreach (var b in startPoints) {
+ var todo = new Stack<Block>();
+ var wasThere = blocksToCheck.Contains(b);
+ todo.Push(b);
+ while (todo.Count > 0) {
+ var x = todo.Pop();
+ if (blocksToCheck.Contains(x)) continue;
+ blocksToCheck.Add(x);
+ var ex = x.TransferCmd as GotoCmd;
+ if (ex != null)
+ foreach (Block e in ex.labelTargets)
+ todo.Push(e);
+ }
+ if (!wasThere) blocksToCheck.Remove(b);
+ }
+
+ foreach (var b in impl.Blocks) {
+ if (blocksToCheck.Contains(b)) continue;
+ var newCmds = new CmdSeq();
+ var copyMode = false;
+ foreach (Cmd c in b.Cmds) {
+ var p = c as PredicateCmd;
+ if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here"))
+ copyMode = true;
+ var asrt = c as AssertCmd;
+ if (copyMode || asrt == null)
+ newCmds.Add(c);
+ else
+ newCmds.Add(AssertTurnedIntoAssume(asrt));
+ }
+
+ b.Cmds = newCmds;
+ }
+ }
+ }
+
// Used by lazy/stratified inlining
protected virtual void addExitAssert(string implName, Block exitBlock)
{
diff --git a/Test/test2/Answer b/Test/test2/Answer index 4c0cbfc1..ca050273 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -381,6 +381,24 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
+-------------------- SelectiveChecking.bpl --------------------
+SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(15,3): anon0
+SelectiveChecking.bpl(30,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(24,3): anon0
+ SelectiveChecking.bpl(27,5): anon3_Then
+ SelectiveChecking.bpl(30,3): anon2
+SelectiveChecking.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(37,3): anon0
+SelectiveChecking.bpl(39,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ SelectiveChecking.bpl(37,3): anon0
+
+Boogie program verifier finished with 1 verified, 4 errors
+
-------------------- Arrays.bpl /typeEncoding:m --------------------
Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
diff --git a/Test/test2/SelectiveChecking.bpl b/Test/test2/SelectiveChecking.bpl new file mode 100644 index 00000000..2f08618a --- /dev/null +++ b/Test/test2/SelectiveChecking.bpl @@ -0,0 +1,49 @@ +/* +In functions marked with {:selective_checking} all asserts are turned into assumes, +except for the ones reachable from the commands marked with {:start_checking_here}. +Thus, "assume {:start_checking_here} whatever;" is an inverse of "assume false;". +The first one disables all verification before it, and the second one disables +all verification after. +*/ + +procedure {:selective_checking} foo() +{ + var x, y, z : int; + + assert x < y; + assert y < z; + assume {:start_checking_here} true; + assert x < z; +} + +procedure {:selective_checking} foo_fail1() +{ + var x, y, z : int; + + assert x < y; + assume {:start_checking_here} true; + assert x < z; +} + +procedure {:selective_checking} foo_fail2() +{ + var x, y, z : int; + + assert x < y; + + if (*) { + assume {:start_checking_here} true; + } + + assert x < z; +} + +procedure foo_no_selch() +{ + var x, y, z : int; + + assert x < y; + assume {:start_checking_here} true; + assert x < z; +} + diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat index f704e263..c9d4feac 100644 --- a/Test/test2/runtest.bat +++ b/Test/test2/runtest.bat @@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl strings-no-where.bpl strings-where.bpl
Structured.bpl Where.bpl UpdateExpr.bpl
NeverPattern.bpl NullaryMaps.bpl Implies.bpl
- IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl) do (
+ IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /noinfer %%f
|