Worked on the verification result caching.

5 files changed, 116 insertions, 102 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a9466f8d..3325d742 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3266,28 +3266,53 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public List<LocalVariable> PossiblyFalseAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)

+    IList<LocalVariable> doomedInjectedAssumptionVariables;

+    public IList<LocalVariable> DoomedInjectedAssumptionVariables

+    {

+      get

+      {

+        return doomedInjectedAssumptionVariables != null ? doomedInjectedAssumptionVariables : new List<LocalVariable>();

+      }

+    }

+

+    public List<LocalVariable> RelevantInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)

     {

       return InjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();

     }

 

+    public List<LocalVariable> RelevantDoomedInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)

+    {

+      return DoomedInjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();

+    }

+

     public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap, out bool isTrue)

     {

       Contract.Requires(incarnationMap != null);

 

-      var vars = PossiblyFalseAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList();

+      var vars = RelevantInjectedAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList();

       isTrue = vars.Count == 0;

       return LiteralExpr.BinaryTreeAnd(vars);

     }

 

-    public void InjectAssumptionVariable(LocalVariable variable)

+    public void InjectAssumptionVariable(LocalVariable variable, bool isDoomed = false)

     {

-      if (injectedAssumptionVariables == null)

+      LocVars.Add(variable);

+      if (isDoomed)

       {

-        injectedAssumptionVariables = new List<LocalVariable>();

+        if (doomedInjectedAssumptionVariables == null)

+        {

+          doomedInjectedAssumptionVariables = new List<LocalVariable>();

+        }

+        doomedInjectedAssumptionVariables.Add(variable);

+      }

+      else

+      {

+        if (injectedAssumptionVariables == null)

+        {

+          injectedAssumptionVariables = new List<LocalVariable>();

+        }

+        injectedAssumptionVariables.Add(variable);

       }

-      injectedAssumptionVariables.Add(variable);

-      LocVars.Add(variable);

     }

 

     public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 724885ed..2b16651b 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1999,7 +1999,6 @@ namespace Microsoft.Boogie {
     public string/*!*/ callee { get; set; }

     public Procedure Proc;

     public LocalVariable AssignedAssumptionVariable;

-    public string ProcDependencyChecksumInPreviousSnapshot { get; set; }

 

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

     // the call happens with * as these parameters

@@ -2087,14 +2086,6 @@ namespace Microsoft.Boogie {
         stream.Write(" := ");

       }

       stream.Write(TokenTextWriter.SanitizeIdentifier(callee));

-      if (stream.UseForComputingChecksums)

-      {

-        var c = ProcDependencyChecksumInPreviousSnapshot != null ? ProcDependencyChecksumInPreviousSnapshot : Proc.DependencyChecksum;

-        if (c != null)

-        {

-          stream.Write(string.Format("[dependency_checksum:{0}]", c));

-        }

-      }

       stream.Write("(");

       sep = "";

       foreach (Expr arg in Ins) {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 2993feb7..1c051ca5 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -1,5 +1,6 @@
 using System;

 using System.Collections.Generic;

+using System.Linq;

 using Microsoft.Boogie.GraphUtil;

 using System.Diagnostics.Contracts;

 

@@ -423,7 +424,7 @@ namespace Microsoft.Boogie {
         HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

 

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

-        foreach (var v in impl.InjectedAssumptionVariables)

+        foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables))

         {

           liveVarsAfter.Add(v);

         }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index e647ea3b..f8b29a69 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -155,6 +155,8 @@ namespace Microsoft.Boogie
                 if (p != null)

                 {

                   SetAssertionChecksumsInCachedSnapshot(impl, p);

+                  eai.Inject(impl, p);

+                  run.RewrittenImplementationCount++;

                 }

               }

             }

@@ -220,53 +222,53 @@ namespace Microsoft.Boogie
           && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

       {

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

+        var before = new List<Cmd>();

+        var after = new List<Cmd>();

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

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

+        if (canUseSpecs)

         {

-          var before = new List<Cmd>();

-          var pre = node.CheckedPrecondition(oldProc, Program);

-          if (pre != null)

+          var precond = node.CheckedPrecondition(oldProc, Program);

+          if (precond != null)

           {

-            

-            var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

+            var assume = new AssumeCmd(Token.NoToken, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

             before.Add(assume);

           }

 

-          var after = new List<Cmd>();

-          var post = node.Postcondition(oldProc, Program);

-          var mods = node.UnmodifiedBefore(oldProc);

-          foreach (var m in mods)

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

+          var unmods = node.UnmodifiedBefore(oldProc);

+          foreach (var unmod in unmods)

           {

-            var mPre = new LocalVariable(Token.NoToken,

-              new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.Type));

+            var oldUnmod = new LocalVariable(Token.NoToken,

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

             before.Add(new AssignCmd(Token.NoToken,

-                         new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, mPre)) },

-                         new List<Expr> { new IdentifierExpr(Token.NoToken, m.Decl) }));

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

-            if (post == null)

+                         new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod)) },

+                         new List<Expr> { new IdentifierExpr(Token.NoToken, unmod.Decl) }));

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

+            if (assumedExpr == null)

             {

-              post = eq;

+              assumedExpr = eq;

             }

             else

             {

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

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

             }

           }

+        }

 

-          if (post != 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 lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

-            var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), post);

-            var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

-            after.Add(assumed);

-          }

-          node.ExtendDesugaring(before, after);

-          node.ProcDependencyChecksumInPreviousSnapshot = oldProc.DependencyChecksum;

+        if (assumedExpr != 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, !canUseSpecs);

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

+          var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);

+          var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+          after.Add(assumed);

         }

+        node.ExtendDesugaring(before, after);

       }

 

       return result;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8295a873..98f0110a 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1489,7 +1489,8 @@ namespace VC {
         }

         Contract.Assert(copy != null);

         var dropCmd = false;

-        var possiblyFalseAssumpVars = currentImplementation != null ? currentImplementation.PossiblyFalseAssumptionVariables(incarnationMap) : null;

+        var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

+        var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

@@ -1498,59 +1499,49 @@ namespace VC {
 

           var subsumption = Wlp.Subsumption(ac);

           var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;

-          if (alwaysUseSubsumption

-              && currentImplementation != null

+          if (currentImplementation != null

               && currentImplementation.HasCachedSnapshot

-              && ((!currentImplementation.AnyErrorsInCachedSnapshot

-                   && 2 <= possiblyFalseAssumpVars.Count)

-                   || (currentImplementation.AnyErrorsInCachedSnapshot

-                       && possiblyFalseAssumpVars.Any()

-                       && ac.Checksum != null

-                       && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

-                       && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))))

+              && !currentImplementation.AnyErrorsInCachedSnapshot

+              && currentImplementation.InjectedAssumptionVariables.Count == 1)

+          { }

+          else if (relevantDoomedAssumpVars.Any())

+          { }

+          else if (currentImplementation != null

+                   && currentImplementation.HasCachedSnapshot

+                   && ac.Checksum != null

+                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

+                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))

           {

-            // Bind the assertion expression to a local variable.

-            var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);

-            var identExpr = new IdentifierExpr(Token.NoToken, incarnation);

-            incarnationMap[incarnation] = identExpr;

-            ac.IncarnationMap[incarnation] = identExpr;

-            passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

-            copy = identExpr;

             bool isTrue;

             var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

-            Expr expr = identExpr;

-            if (!isTrue)

-            {

-              expr = LiteralExpr.Imp(assmVars, expr);

-            }

-            else

+            if (!isTrue && alwaysUseSubsumption)

             {

-              // TODO(wuestholz): Maybe we could drop the assertion in this case.

+              // Bind the assertion expression to a local variable.

+              var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);

+              var identExpr = new IdentifierExpr(Token.NoToken, incarnation);

+              incarnationMap[incarnation] = identExpr;

+              ac.IncarnationMap[incarnation] = identExpr;

+              passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

+              copy = identExpr;

+              passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));

             }

-            passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));

-          }

-          else if (currentImplementation != null

-                   && ac.Checksum != null

-                   && currentImplementation.HasCachedSnapshot

-                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

-                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum)

-                   && possiblyFalseAssumpVars.Count == 0)

-          {

-            if (alwaysUseSubsumption)

+            else if (isTrue)

             {

-              // Turn it into an assume statement.

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

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

+              if (alwaysUseSubsumption)

+              {

+                // Turn it into an assume statement.

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

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

+              }

+              dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

             }

-            dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

           }

           else if (currentImplementation != null

                    && currentImplementation.HasCachedSnapshot

-                   && currentImplementation.AnyErrorsInCachedSnapshot

+                   && relevantAssumpVars.Count == 0

                    && ac.Checksum != null

                    && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

-                   && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum)

-                   && possiblyFalseAssumpVars.Count == 0)

+                   && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))

           {

             if (alwaysUseSubsumption)

             {

@@ -1568,22 +1559,26 @@ namespace VC {
         else if (pc is AssumeCmd

                  && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot"))

         {

-          bool isTrue;

-          var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

-          if (!isTrue)

+          if (!relevantDoomedAssumpVars.Any()

+              && currentImplementation.HasCachedSnapshot

+              && pc.Checksum != null

+              && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum)

+              && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum))

+          {

+            bool isTrue;

+            var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

+            if (!isTrue)

+            {

+              copy = LiteralExpr.Imp(assmVars, copy);

+            }

+          }

+          else

           {

-            copy = LiteralExpr.Imp(assmVars, copy);

+            dropCmd = true;

           }

-          dropCmd = true;

         }

         pc.Expr = copy;

-        if (!dropCmd

-            || !currentImplementation.HasCachedSnapshot

-            || !currentImplementation.AnyErrorsInCachedSnapshot

-            || (currentImplementation.AnyErrorsInCachedSnapshot

-                && pc.Checksum != null

-                && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum)

-                && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum)))

+        if (!dropCmd)

         {

           passiveCmds.Add(pc);

         }