Implemented an optimization for assignments to assumption variables that are injected by the verification result caching for calls within loops.

10 files changed, 166 insertions, 4 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 8c6685e4..a7693b00 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1886,6 +1886,7 @@ namespace Microsoft.Boogie {
   public class CallCmd : CallCommonality, IPotentialErrorNode {

     public string/*!*/ callee { get; set; }

     public Procedure Proc;

+    public LocalVariable AssignedAssumptionVariable;

 

     // Element of the following lists can be null, which means that

     // the call happens with * as these parameters

@@ -2086,6 +2087,10 @@ namespace Microsoft.Boogie {
         Contract.Assert(e != null);

         vars.Add(e.Decl);

       }

+      if (AssignedAssumptionVariable != null)

+      {

+        vars.Add(AssignedAssumptionVariable);

+      }

     }

 

     public override void Typecheck(TypecheckingContext tc)

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index fbc46de8..b54a45c1 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -429,6 +429,14 @@ namespace Microsoft.Boogie {
       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

         HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

+        if (impl.InjectedAssumptionVariables != null)

+        {

+          // The injected assumption variables should always be considered to be live.

+          foreach (var v in impl.InjectedAssumptionVariables)

+          {

+            liveVarsAfter.Add(v);

+          }

+        }

         if (block.TransferCmd is GotoCmd) {

           GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;

           if (gotoCmd.labelTargets != null) {

@@ -497,7 +505,7 @@ namespace Microsoft.Boogie {
         HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;

         foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) {

           Contract.Assert(expr != null);

-          if (expr.Decl != null) {

+          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) {

             liveSet.Remove(expr.Decl);

           }

         }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 9d1eea24..5c3324cc 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -153,11 +153,13 @@ namespace Microsoft.Boogie
       var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);

       if (oldProc != null

           && DependencyCollector.DependenciesChecksum(oldProc) != DependencyCollector.DependenciesChecksum(node.Proc)

-          && DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))

+          && DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program)

+          && node.AssignedAssumptionVariable == null)

       {

         var lv = new LocalVariable(Token.NoToken,

           new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),

           new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

+        node.AssignedAssumptionVariable = lv;

         currentImplementation.InjectAssumptionVariable(lv);

 

         var before = new List<Cmd>();

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 5eaadf23..0898641b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1590,7 +1590,11 @@ namespace VC {
 

         HavocCmd hc = (HavocCmd)c;

         Contract.Assert(c != null);

-        List<IdentifierExpr> havocVars = hc.Vars;

+        // If an assumption variable for postconditions is included here, it must have been assigned within a loop.

+        // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop

+        // invariant) in the previous snapshot and are therefore not going refer to the assumption variable after

+        // the loop. We can achieve this by simply not updating/adding it in the incarnation map.

+        List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList();

         // First, compute the new incarnations

         foreach (IdentifierExpr ie in havocVars) {

           Contract.Assert(ie != null);

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

+

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

+{

+    var x: int;

+

+    x := 0;

+    while (*)

+    {

+        while (*)

+        {

+            assert true;

+

+            call N();

+

+            call N();

+

+            x := x + 1;

+

+            assert x == 1;

+        }

+

+        call N();

+

+        assert false;

+    }

+

+    assert true;

+}

+

+procedure {:checksum "2"} N();

+  ensures false;

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

+

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

+{

+    var x: int;

+

+    x := 0;

+    while (*)

+    {

+        while (*)

+        {

+            assert true;

+

+            call N();

+

+            call N();

+

+            x := x + 1;

+

+            assert x == 1;  // error

+        }

+

+        call N();

+

+        assert false;  // error

+    }

+

+    assert true;

+}

+

+procedure {:checksum "3"} N();

+  ensures true;

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

+

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

+{

+    while (true)

+    {

+        assert 0 == 0;

+        

+        call N();

+        call N();

+

+        if (*)

+        {

+            break;

+        }

+

+        assert 1 != 1;

+    }

+

+    assert 2 != 2;

+}

+

+procedure {:checksum "2"} N();

+  ensures false;

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

+

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

+{

+    while (true)

+    {

+        assert 0 == 0;

+        

+        call N();

+        call N();

+

+        if (*)

+        {

+            break;

+        }

+

+        assert 1 != 1;  // error

+    }

+

+    assert 2 != 2;  // error

+}

+

+procedure {:checksum "3"} N();

+  ensures true;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index ffa54a53..e2d566d8 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 > "%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 > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 41193348..8b363791 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -149,3 +149,34 @@ Execution trace:
     Snapshots16.v1.bpl(14,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots17.v1.bpl(7,7): anon0

+    Snapshots17.v1.bpl(10,9): anon6_LoopHead

+    Snapshots17.v1.bpl(12,13): anon6_LoopBody

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

+Execution trace:

+    Snapshots17.v1.bpl(7,7): anon0

+    Snapshots17.v1.bpl(10,9): anon6_LoopHead

+    Snapshots17.v1.bpl(10,9): anon6_LoopDone

+

+Boogie program verifier finished with 0 verified, 2 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

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

+Execution trace:

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

+    Snapshots18.v1.bpl(5,5): anon5_LoopHead

+    Snapshots18.v1.bpl(7,9): anon5_LoopBody

+    Snapshots18.v1.bpl(12,9): anon6_Else

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

+Execution trace:

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

+    Snapshots18.v1.bpl(5,5): anon5_LoopHead

+    Snapshots18.v1.bpl(7,9): anon5_LoopBody

+    Snapshots18.v1.bpl(14,13): anon6_Then

+    Snapshots18.v1.bpl(20,5): anon4

+

+Boogie program verifier finished with 0 verified, 2 errors