Fixed issues in the verification result caching (old expressions).

10 files changed, 150 insertions, 18 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 066808ae..d143e480 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2558,12 +2558,21 @@ namespace Microsoft.Boogie {
       return Proc.Modifies.Except(oldProcedure.Modifies, comparer).Select(e => new IdentifierExpr(Token.NoToken, e.Decl));

     }

 

-    public Expr Postcondition(Procedure procedure, Program program)

+    public IEnumerable<IdentifierExpr> ModifiedBefore(Procedure oldProcedure)

     {

-      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

+      Contract.Requires(oldProcedure != null);

+

+      return oldProcedure.Modifies.Except(Proc.Modifies, comparer).Select(e => new IdentifierExpr(Token.NoToken, e.Decl));

+    }

+

+    public Expr Postcondition(Procedure procedure, List<Expr> modifies, Dictionary<Variable, Expr> oldSubst, Program program)

+    {

+      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && modifies != null && oldSubst != null && program != null);

+

+      Substitution substOldCombined = v => { Expr s; if (oldSubst.TryGetValue(v, out s)) { return s; } return calleeSubstitutionOld(v); };

 

-      var ensures = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition, program));

-      return Conjunction(ensures);

+      var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies);

+      return Conjunction(clauses);

     }

 

     public Expr CheckedPrecondition(Procedure procedure, Program program)

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index bacdfaf8..d8a446a7 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -190,7 +190,7 @@ namespace Microsoft.Boogie
         var after = new List<Cmd>();

         Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

         // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.

-        var canUseSpecs = DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program);

+        var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);

         if (canUseSpecs)

         {

           var desugaring = node.Desugaring;

@@ -202,8 +202,8 @@ namespace Microsoft.Boogie
             beforePrecondtionCheck.Add(assume);

           }

 

-          assumedExpr = node.Postcondition(oldProc, Program);

           var unmods = node.UnmodifiedBefore(oldProc);

+          var eqs = new List<Expr>();

           foreach (var unmod in unmods)

           {

             var oldUnmod = new LocalVariable(Token.NoToken,

@@ -211,16 +211,22 @@ namespace Microsoft.Boogie
             var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));

             var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);

             before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));

-            var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));

-            if (assumedExpr == null)

-            {

-              assumedExpr = eq;

-            }

-            else

-            {

-              assumedExpr = LiteralExpr.And(assumedExpr, eq);

-            }

+            eqs.Add(LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl)));

+          }

+

+          var mods = node.ModifiedBefore(oldProc);

+          var oldSubst = new Dictionary<Variable, Expr>();

+          foreach (var mod in mods)

+          {

+            var oldMod = new LocalVariable(Token.NoToken,

+              new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName), mod.Type));

+            oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod);

+            var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod));

+            var rhs = new IdentifierExpr(Token.NoToken, mod.Decl);

+            before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));

           }

+          

+          assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program);

         }

 

         if (assumedExpr != null)

@@ -340,13 +346,15 @@ namespace Microsoft.Boogie
       }

     }

 

-    public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)

+    public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg)

     {

       Contract.Requires(oldProc != null && newProg != null);

 

       var funcs = newProg.Functions;

+      var globals = newProg.GlobalVariables;

       return oldProc.DependenciesCollected

-             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));

+             && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)))

+             && oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name));

     }

 

     public override Procedure VisitProcedure(Procedure node)

diff --git a/Test/snapshots/Snapshots31.v0.bpl b/Test/snapshots/Snapshots31.v0.bpl
new file mode 100644
index 00000000..845a6cef
--- /dev/null
+++ b/Test/snapshots/Snapshots31.v0.bpl
@@ -0,0 +1,15 @@
+var g: int;

+

+procedure {:checksum "0"} P();

+  requires g == 0;

+  modifies g;

+

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

+{

+    call Q();

+    assert 0 < g;

+}

+

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

+  modifies g;

+  ensures old(g) < g;

diff --git a/Test/snapshots/Snapshots31.v1.bpl b/Test/snapshots/Snapshots31.v1.bpl
new file mode 100644
index 00000000..a3b37168
--- /dev/null
+++ b/Test/snapshots/Snapshots31.v1.bpl
@@ -0,0 +1,14 @@
+var g: int;

+

+procedure {:checksum "0"} P();

+  requires g == 0;

+  modifies g;

+

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

+{

+    call Q();

+    assert 0 < g;

+}

+

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

+  modifies g;

diff --git a/Test/snapshots/Snapshots32.v0.bpl b/Test/snapshots/Snapshots32.v0.bpl
new file mode 100644
index 00000000..845a6cef
--- /dev/null
+++ b/Test/snapshots/Snapshots32.v0.bpl
@@ -0,0 +1,15 @@
+var g: int;

+

+procedure {:checksum "0"} P();

+  requires g == 0;

+  modifies g;

+

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

+{

+    call Q();

+    assert 0 < g;

+}

+

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

+  modifies g;

+  ensures old(g) < g;

diff --git a/Test/snapshots/Snapshots32.v1.bpl b/Test/snapshots/Snapshots32.v1.bpl
new file mode 100644
index 00000000..cbffe891
--- /dev/null
+++ b/Test/snapshots/Snapshots32.v1.bpl
@@ -0,0 +1,12 @@
+var g: int;

+

+procedure {:checksum "0"} P();

+  requires g == 0;

+

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

+{

+    call Q();

+    assert 0 < g;

+}

+

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

diff --git a/Test/snapshots/Snapshots33.v0.bpl b/Test/snapshots/Snapshots33.v0.bpl
new file mode 100644
index 00000000..845a6cef
--- /dev/null
+++ b/Test/snapshots/Snapshots33.v0.bpl
@@ -0,0 +1,15 @@
+var g: int;

+

+procedure {:checksum "0"} P();

+  requires g == 0;

+  modifies g;

+

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

+{

+    call Q();

+    assert 0 < g;

+}

+

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

+  modifies g;

+  ensures old(g) < g;

diff --git a/Test/snapshots/Snapshots33.v1.bpl b/Test/snapshots/Snapshots33.v1.bpl
new file mode 100644
index 00000000..1c6d6dbf
--- /dev/null
+++ b/Test/snapshots/Snapshots33.v1.bpl
@@ -0,0 +1,8 @@
+procedure {:checksum "5"} P();

+

+implementation {:id "P"} {:checksum "4"} P()

+{

+    call Q();

+}

+

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

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index fb476128..a203ffac 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl > "%t"

 // RUN: %diff "%s.expect" "%t"

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index d8642441..7f912427 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -126,6 +126,7 @@ Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):

+  >>> added before: y##old##0 := y;

   >>> added after: a##post##0 := a##post##0 && y < z;

 Processing command (at <unknown location>) a##post##0 := a##post##0 && y < z;

   >>> AssumeNegationOfAssumptionVariable

@@ -546,3 +547,38 @@ Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not ho
 Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):

+  >>> added after: a##post##0 := a##post##0 && call0old#AT#g < g;

+Processing command (at <unknown location>) a##post##0 := a##post##0 && call0old#AT#g < g;

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;

+  >>> MarkAsPartiallyVerified

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):

+  >>> added before: g##old##0 := g;

+  >>> added after: a##post##0 := a##post##0 && g##old##0 < g;

+Processing command (at <unknown location>) a##post##0 := a##post##0 && g##old##0 < g;

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;

+  >>> MarkAsPartiallyVerified

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):

+  >>> added after: a##post##0 := a##post##0 && false;

+

+Boogie program verifier finished with 1 verified, 0 errors