From e721ac469b8aa3f964ad24917757168288826da1 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 10 Jul 2014 10:25:53 +0200
Subject: Worked on the more advanced verification result caching.

---
 Source/ExecutionEngine/ExecutionEngine.cs         |  2 +
 Source/ExecutionEngine/VerificationResultCache.cs | 62 +++++++++++++----------
 2 files changed, 36 insertions(+), 28 deletions(-)

(limited to 'Source/ExecutionEngine')

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ea69b29e..1b799bd5 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -880,6 +880,8 @@ namespace Microsoft.Boogie
       {
         // TODO(wuestholz): Maybe we should speed up this lookup.
         OtherDefinitionAxiomsCollector.Collect(program.TopLevelDeclarations.OfType<Axiom>());
+        // TODO(wuestholz): Maybe we should speed up this lookup.
+        program.TopLevelDeclarations.OfType<Function>().Iter(fun => { DependencyCollector.DependenciesChecksum(fun); });
         impls.Iter(impl => { DependencyCollector.DependenciesChecksum(impl); });
         stablePrioritizedImpls = impls.OrderByDescending(
           impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index b9c04661..b401ec67 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -198,40 +198,46 @@ 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)
           && 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>();
-        if (oldProc.Requires.Any())
+        if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
         {
-          var pre = node.CheckedPrecondition(oldProc, Program);
-          var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
-          before.Add(assume);
-        }
+          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>();
+          if (oldProc.Requires.Any())
+          {
+            var pre = node.CheckedPrecondition(oldProc, Program);
+            var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+            before.Add(assume);
+          }
 
-        var post = node.Postcondition(oldProc, Program);
-        var mods = node.UnmodifiedBefore(oldProc);
-        foreach (var m in mods)
+          var post = node.Postcondition(oldProc, Program);
+          var mods = node.UnmodifiedBefore(oldProc);
+          foreach (var m in mods)
+          {
+            var mPre = new LocalVariable(Token.NoToken,
+              new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.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));
+            post = LiteralExpr.And(post, eq);
+          }
+          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 });
+
+          node.ExtendDesugaring(before, new List<Cmd> { assumed });
+        }
+        else
         {
-          var mPre = new LocalVariable(Token.NoToken,
-            new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.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));
-          post = LiteralExpr.And(post, eq);
+          node.EmitDependenciesChecksum = true;
         }
-        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 });
-
-        node.ExtendDesugaring(before, new List<Cmd> { assumed });
       }
 
       return result;
-- 
cgit v1.2.3