Add new feature: {:selective_checking} on procedures. See testcase for a description (it was implemented in VCC before and is quite useful).

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