Added more tests and worked on adding support for "canned errors".

7 files changed, 100 insertions, 22 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 1f92c4ac..916340a5 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -92,7 +92,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    protected CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)

+    CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)

     {

       Implementations = implementations;

       Program = program;

@@ -106,12 +106,6 @@ namespace Microsoft.Boogie
       assumptionVariableCount = 0;

       temporaryVariableCount = 0;

       currentImplementation = implementation;

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = programInCachedSnapshot.Implementations().FirstOrDefault(i => i.Id == implementation.Id);

-      if (implPrevSnap != null)

-      {

-        currentImplementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

-      }

       var result = VisitImplementation(implementation);

       currentImplementation = null;

       this.programInCachedSnapshot = null;

@@ -134,19 +128,13 @@ namespace Microsoft.Boogie
             run.LowPriorityImplementationCount++;

             if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

             {

-              if (vr.Errors != null && vr.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

-              {

-                impl.SetErrorChecksumsInCachedSnapshot(vr.Errors.Select(cex => cex.Checksum));

-              }

-              else if (vr.Outcome == ConditionGeneration.Outcome.Correct)

-              {

-                impl.SetErrorChecksumsInCachedSnapshot(new List<byte[]>());

-              }

+              SetErrorChecksumsInCachedSnapshot(impl, vr);

               if (vr.ProgramId != null)

               {

                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

                 if (p != null)

                 {

+                  SetAssertionChecksumsInPreviousSnapshot(impl, p);

                   eai.Inject(impl, p);

                   run.RewrittenImplementationCount++;

                 }

@@ -156,6 +144,15 @@ namespace Microsoft.Boogie
           else if (priority == Priority.MEDIUM)

           {

             run.MediumPriorityImplementationCount++;

+            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

+            {

+              SetErrorChecksumsInCachedSnapshot(impl, vr);

+              var p = ExecutionEngine.CachedProgram(vr.ProgramId);

+              if (p != null)

+              {

+                SetAssertionChecksumsInPreviousSnapshot(impl, p);

+              }

+            }

           }

           else if (priority == Priority.HIGH)

           {

@@ -171,6 +168,28 @@ namespace Microsoft.Boogie
       Statistics.AddRun(requestId, run);

     }

 

+    private static void SetErrorChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)

+    {

+      if (result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

+      {

+        implementation.SetErrorChecksumsInCachedSnapshot(result.Errors.Select(cex => cex.Checksum));

+      }

+      else if (result.Outcome == ConditionGeneration.Outcome.Correct)

+      {

+        implementation.SetErrorChecksumsInCachedSnapshot(new List<byte[]>());

+      }

+    }

+

+    private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

+    {

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);

+      if (implPrevSnap != null)

+      {

+        implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

+      }

+    }

+

     public override Cmd VisitCallCmd(CallCmd node)

     {

       var result = base.VisitCallCmd(node);

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 787477ad..abbcf4aa 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1527,16 +1527,15 @@ namespace VC {
           }

           else if (currentImplementation != null

                    && currentImplementation.AnyErrorsInCachedSnapshot

-                   && currentImplementation.InjectedAssumptionVariables != null

-                   && currentImplementation.InjectedAssumptionVariables.Any()

                    && ac.Checksum != null

                    && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

                    && currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum)

-                   && !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v)))

+                   && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

-            ac.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), ac.Attributes);

+            // TODO(wuestholz): Uncomment this once the canned errors are reported.

+            // pc = new AssumeCmd(ac.tok, copy);

+            pc.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), pc.Attributes);

             currentImplementation.AddCannedFailingAssertion(ac);

-            // TODO(wuestholz): Turn the 'assert' command into an 'assume' command.

           }

         }

         else if (pc is AssumeCmd

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 505f18b7..9aa764e2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1481,7 +1481,16 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

-      // TODO(wuestholz): Report all canned failing assertions for this implementation.

+      // Report all canned failing assertions for this implementation.

+      if (impl.CannedFailingAssertions != null)

+      {

+        foreach (var a in impl.CannedFailingAssertions)

+        {

+          // TODO(wuestholz): Implement this.

+          // var cex = AssertCmdToCounterexample(a, ...);

+          // callback.OnCounterexample(cex, ...);

+        }

+      }

 

       // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct

       foreach (var b in impl.Blocks)

diff --git a/Test/snapshots/Snapshots21.v0.bpl b/Test/snapshots/Snapshots21.v0.bpl
new file mode 100644
index 00000000..4a4080f5
--- /dev/null
+++ b/Test/snapshots/Snapshots21.v0.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    if (*)

+    {

+        assert 1 != 1;  // error

+    }

+    else

+    {

+        assert 2 != 2;  // error

+    }

+

+    assert 3 != 3;

+}

diff --git a/Test/snapshots/Snapshots21.v1.bpl b/Test/snapshots/Snapshots21.v1.bpl
new file mode 100644
index 00000000..ef51e5ac
--- /dev/null
+++ b/Test/snapshots/Snapshots21.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "2"} M()

+{

+    if (*)

+    {

+        assert 1 == 1;

+    }

+    else

+    {

+        assert 2 != 2;  // error

+    }

+

+    assert 3 != 3;  // error

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 57ca7f5a..e73e4eba 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl > "%t"
+// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 7b9241d8..daabfca9 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -206,3 +206,24 @@ Execution trace:
     Snapshots20.v1.bpl(13,9): anon4_Else

 

 Boogie program verifier finished with 0 verified, 2 errors

+Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots21.v0.bpl(5,5): anon0

+    Snapshots21.v0.bpl(7,9): anon4_Then

+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots21.v0.bpl(5,5): anon0

+    Snapshots21.v0.bpl(11,9): anon4_Else

+

+Boogie program verifier finished with 0 verified, 2 errors

+Snapshots21.v1.bpl(11,9): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots21.v1.bpl(5,5): anon0

+    Snapshots21.v1.bpl(11,9): anon4_Else

+Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots21.v1.bpl(5,5): anon0

+    Snapshots21.v1.bpl(7,9): anon4_Then

+    Snapshots21.v1.bpl(14,5): anon3

+

+Boogie program verifier finished with 0 verified, 2 errors