Make caching of verification results more fine-grained for changes that affect preconditions.

5 files changed, 94 insertions, 25 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a1a54024..56bfc90f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2427,6 +2427,28 @@ namespace Microsoft.Boogie {
       functionDependencies.Add(function);

     }

 

+    public bool SignatureEquals(DeclWithFormals other)

+    {

+      Contract.Requires(other != null);

+

+      string sig = null;

+      string otherSig = null;

+      using (var strWr = new System.IO.StringWriter())

+      using (var tokTxtWr = new TokenTextWriter("<no file>", strWr, false, false))

+      {

+        EmitSignature(tokTxtWr, this is Function);

+        sig = strWr.ToString();

+      }

+

+      using (var otherStrWr = new System.IO.StringWriter())

+      using (var otherTokTxtWr = new TokenTextWriter("<no file>", otherStrWr, false, false))

+      {

+        EmitSignature(otherTokTxtWr, other is Function);

+        otherSig = otherStrWr.ToString();

+      }

+      return sig == otherSig;

+    }

+

     protected void EmitSignature(TokenTextWriter stream, bool shortRet) {

       Contract.Requires(stream != null);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

@@ -3295,6 +3317,8 @@ namespace Microsoft.Boogie {
       RecycledFailingAssertions.Add(assertion);

     }

 

+    public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; }

+

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

     [ContractInvariantMethod]

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 137e2363..eb8b8e1e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1144,6 +1144,12 @@ namespace Microsoft.Boogie {
         return;

       }

 

+      if (cmd.IrrelevantForChecksumComputation)

+      {

+        cmd.Checksum = currentChecksum;

+        return;

+      }

+

       var assumeCmd = cmd as AssumeCmd;

       if (assumeCmd != null

           && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization"))

@@ -1161,7 +1167,7 @@ namespace Microsoft.Boogie {
         if (havocCmd != null)

         {

           tokTxtWr.Write("havoc ");

-          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##post##")).OrderBy(e => e.Name).ToList();

+          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##cached##")).OrderBy(e => e.Name).ToList();

           relevantVars.Emit(tokTxtWr, true);

           tokTxtWr.WriteLine(";");

         }

@@ -1244,6 +1250,7 @@ namespace Microsoft.Boogie {
   public abstract class Cmd : Absy {

     public byte[] Checksum { get; internal set; }

     public byte[] SugaredCmdChecksum { get; internal set; }

+    public bool IrrelevantForChecksumComputation { get; set; }

 

     public Cmd(IToken/*!*/ tok)

       : base(tok) {

@@ -2849,7 +2856,7 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies);

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

@@ -2860,30 +2867,10 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

-    private static Expr Conjunction(IEnumerable<Expr> conjuncts)

-    {

-      // TODO(wuestholz): Maybe we should use 'LiteralExpr.BinaryTreeAnd' instead.

-      Expr result = null;

-      foreach (var c in conjuncts)

-      {

-        if (result != null)

-        {

-          result = LiteralExpr.And(result, c);

-          result.Type = Type.Bool;

-        }

-        else

-        {

-          result = c;

-          result.Type = Type.Bool;

-        }

-      }

-      return result;

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3a943b8..c19140d7 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -467,6 +467,29 @@ namespace Microsoft.Boogie {
         var mid = (start + end) / 2;

         return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

     }

+

+    public static Expr And(IEnumerable<Expr> conjuncts, bool returnNullIfEmpty = false)

+    {

+      Expr result = null;

+      foreach (var c in conjuncts)

+      {

+        if (result != null)

+        {

+          result = LiteralExpr.And(result, c);

+          result.Type = Type.Bool;

+        }

+        else

+        {

+          result = c;

+          result.Type = Type.Bool;

+        }

+      }

+      if (result == null && !returnNullIfEmpty)

+      {

+        result = Expr.True;

+      }

+      return result;

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 77086f0f..0feb5e35 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -539,7 +539,7 @@ namespace Microsoft.Boogie {
         HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;

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

           Contract.Assert(expr != null);

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

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

             liveSet.Remove(expr.Decl);

           }

         }

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 181b80a1..7f021c43 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -583,6 +583,15 @@ namespace Microsoft.Boogie {
       return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr);

     }

 

+    public static Expr FunctionCallReresolvingApply(Substitution always, Substitution forOld, Expr expr, Program program)

+    {

+      Contract.Requires(always != null);

+      Contract.Requires(forOld != null);

+      Contract.Requires(expr != null);

+      Contract.Ensures(Contract.Result<Expr>() != null);

+      return (Expr)new FunctionCallReresolvingNormalSubstituter(program, always, forOld).Visit(expr);

+    }

+

     // ----------------------------- Substitutions for Cmd -------------------------------

 

     /// <summary>

@@ -660,7 +669,7 @@ namespace Microsoft.Boogie {
 

     // ------------------------------------------------------------

 

-    private sealed class NormalSubstituter : Duplicator

+    private class NormalSubstituter : Duplicator

     {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

@@ -744,6 +753,32 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private sealed class FunctionCallReresolvingNormalSubstituter : NormalSubstituter

+    {

+      readonly Program Program;

+

+      public FunctionCallReresolvingNormalSubstituter(Program program, Substitution always, Substitution forold)

+        : base(always, forold)

+      {

+        Program = program;

+      }

+

+      public override Expr VisitNAryExpr(NAryExpr node)

+      {

+        var result = base.VisitNAryExpr(node);

+        var nAryExpr = result as NAryExpr;

+        if (nAryExpr != null)

+        {

+          var funCall = nAryExpr.Fun as FunctionCall;

+          if (funCall != null)

+          {

+            funCall.Func = Program.FindFunction(funCall.FunctionName);

+          }

+        }

+        return result;

+      }

+    }

+

     private class ReplacingOldSubstituter : Duplicator {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;