Worked on an extension of the existing verification result caching.

2 files changed, 232 insertions, 36 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 6a4dbc07..925b414b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -317,9 +317,32 @@ namespace Microsoft.Boogie
 

   public class VerificationResult

   {

+    public readonly string RequestId;

     public readonly string Checksum;

     public readonly string DependeciesChecksum;

-    public readonly string RequestId;

+    public readonly string ImplementationName;

+    public readonly IToken ImplementationToken;

+

+    private readonly WeakReference program;

+    public Program Program

+    {

+      get

+      {

+        if (program == null)

+        {

+          return null;

+        }

+        try

+        {

+          var p = program.Target as Program;

+          return p;

+        }

+        catch (InvalidOperationException)

+        {

+          return null;

+        }

+      }

+    }

 

     public DateTime Start { get; set; }

     public DateTime End { get; set; }

@@ -328,24 +351,20 @@ namespace Microsoft.Boogie
     public int ProofObligationCountBefore { get; set; }

     public int ProofObligationCountAfter { get; set; }

 

-    public ConditionGeneration.Outcome Outcome;

+    public ConditionGeneration.Outcome Outcome { get; set; }

     public List<Counterexample> Errors;

 

-    public string ImplementationName { get; set; }

-    public IToken ImplementationToken { get; set; }

-

-    public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

-      : this(requestId, checksum, depsChecksum)

-    {

-      Outcome = outcome;

-      Errors = errors;

-    }

-

-    public VerificationResult(string requestId, string checksum, string depsChecksum)

+    public VerificationResult(string requestId, string checksum, string depsChecksum, string implementationName, IToken implementationToken, Program program = null)

     {

       Checksum = checksum;

       DependeciesChecksum = depsChecksum;

       RequestId = requestId;

+      ImplementationName = implementationName;

+      ImplementationToken = implementationToken;

+      if (program != null)

+      {

+        this.program = new WeakReference(program);

+      }

     }

   }

 

@@ -844,7 +863,7 @@ namespace Microsoft.Boogie
       Implementation[] stablePrioritizedImpls = null;

       if (0 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });

+        impls.Iter(impl => { DependencyCollector.DependenciesChecksum(impl); });

         stablePrioritizedImpls = impls.OrderByDescending(

           impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();

       }

@@ -855,6 +874,11 @@ namespace Microsoft.Boogie
 

       #endregion

 

+      if (1 < CommandLineOptions.Clo.VerifySnapshots)

+      {

+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls);

+      }

+

       #region Verify each implementation

 

       var outputCollector = new OutputCollector(stablePrioritizedImpls);

@@ -995,9 +1019,7 @@ namespace Microsoft.Boogie
       {

         #region Verify the implementation

 

-        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);

-        verificationResult.ImplementationName = impl.Name;

-        verificationResult.ImplementationToken = impl.tok;

+        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, 1 < CommandLineOptions.Clo.VerifySnapshots ? program : null);

 

         using (var vcgen = CreateVCGen(program, checkers))

         {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 044d84fe..a0dba9d2 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -10,40 +10,204 @@ using VC;
 namespace Microsoft.Boogie

 {

 

+  class CachedVerificationResultInjector : StandardVisitor

+  {

+    readonly IEnumerable<Implementation> Implementations;

+    readonly Program Program;

+    Program programInCachedSnapshot;

+    Implementation currentImplementation;

+    int assumptionVariableCount;

+    int temporaryVariableCount;

+

+    int FreshAssumptionVariableName

+    {

+      get

+      {

+        return assumptionVariableCount++;

+      }

+    }

+

+    int FreshTemporaryVariableName

+    {

+      get

+      {

+        return temporaryVariableCount++;

+      }

+    }

+

+    protected CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)

+    {

+      Implementations = implementations;

+      Program = program;

+    }

+

+    public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)

+    {

+      Contract.Requires(implementation != null && programInCachedSnapshot != null);

+

+      this.programInCachedSnapshot = programInCachedSnapshot;

+      assumptionVariableCount = 0;

+      temporaryVariableCount = 0;

+      currentImplementation = implementation;

+      var result = VisitImplementation(implementation);

+      currentImplementation = null;

+      this.programInCachedSnapshot = null;

+      return result;

+    }

+

+    public static void Inject(Program program, IEnumerable<Implementation> implementations)

+    {

+      var eai = new CachedVerificationResultInjector(program, implementations);

+

+      foreach (var impl in implementations)

+      {

+        if (ExecutionEngine.Cache.VerificationPriority(impl) == Priority.LOW)

+        {

+          var vr = ExecutionEngine.Cache.Lookup(impl.Id);

+          // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.

+          if (vr != null && 0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds)

+          {

+            if (vr.Errors != null)

+            {

+              impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();

+            }

+            else if (vr.Outcome == ConditionGeneration.Outcome.Correct)

+            {

+              impl.ErrorsInCachedSnapshot = new List<object>();

+            }

+            var p = vr.Program;

+            if (p != null)

+            {

+              eai.Inject(impl, p);

+            }

+          }

+        }

+      }

+    }

+

+    public override Cmd VisitCallCmd(CallCmd node)

+    {

+      var result = base.VisitCallCmd(node);

+

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      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))

+      {

+        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));

+        currentImplementation.InjectAssumptionVariable(lv);

+

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

+        if (currentImplementation.NoErrorsInCachedSnapshot

+            && oldProc.Requires.Any())

+        {

+          var pre = node.Precondition(oldProc, Program);

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

+          before.Add(assume);

+        }

+        else if (currentImplementation.AnyErrorsInCachedSnapshot)

+        {

+          // TODO(wuestholz): Add an assume statement if the precondition was verified in the previous snapshot.

+        }

+

+        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 });

+      }

+

+      return result;

+    }

+  }

+

+

   class DependencyCollector : ReadOnlyVisitor

   {

-    private HashSet<DeclWithFormals> dependencies;

+    private HashSet<Procedure> procedureDependencies;

+    private HashSet<Function> functionDependencies;

+    private bool allDependenciesHaveChecksum = true;

 

     public DependencyCollector()

     {

-      dependencies = new HashSet<DeclWithFormals>();

+      procedureDependencies = new HashSet<Procedure>();

+      functionDependencies = new HashSet<Function>();

     }

 

-    public static void Collect(Absy node, out List<DeclWithFormals> dependencies)

+    static bool Collect(Absy node, out ISet<Procedure> procedureDependencies, out ISet<Function> functionDependencies)

     {

       var dc = new DependencyCollector();

       dc.Visit(node);

-      dependencies = dc.dependencies.ToList();

+      procedureDependencies = dc.procedureDependencies;

+      functionDependencies = dc.functionDependencies;

+      return dc.allDependenciesHaveChecksum;

+    }

+

+    static bool Collect(Procedure proc, out ISet<Function> functionDependencies)

+    {

+      var dc = new DependencyCollector();

+      dc.Visit(proc);

+      functionDependencies = dc.functionDependencies;

+      return dc.allDependenciesHaveChecksum;

+    }

+

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

+    {

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

+

+      ISet<Function> oldDeps;

+      if (!Collect(oldProc, out oldDeps))

+      {

+        return false;

+      }

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      var funcs = newProg.TopLevelDeclarations.OfType<Function>();

+      return oldDeps.All(dep => funcs.Any(f => f.Name == dep.Name && f.Checksum == dep.Checksum));

     }

 

-    public static string DependenciesChecksum(Implementation impl)

+    public static string DependenciesChecksum(DeclWithFormals decl)

     {

-      List<DeclWithFormals> deps;

-      DependencyCollector.Collect(impl, out deps);

-      if (deps.Any(dep => dep.Checksum == null))

+      if (decl.DependenciesChecksum != null)

+      {

+        return decl.DependenciesChecksum;

+      }

+

+      ISet<Procedure> procDeps;

+      ISet<Function> funcDeps;

+      if (!DependencyCollector.Collect(decl, out procDeps, out funcDeps))

       {

         return null;

       }

 

       var md5 = System.Security.Cryptography.MD5.Create();

-      var data = Encoding.UTF8.GetBytes(deps.MapConcat(dep => dep.Checksum, ""));

+      var procChecksums = procDeps.MapConcat(dep => dep.Checksum, "");

+      var funcChecksums = funcDeps.MapConcat(dep => dep.Checksum, "");

+      var data = Encoding.UTF8.GetBytes(procChecksums + funcChecksums);

       var hashedData = md5.ComputeHash(data);

-      return BitConverter.ToString(hashedData);

+      var result = BitConverter.ToString(hashedData);

+      decl.DependenciesChecksum = result;

+      return result;

     }

 

     public override Procedure VisitProcedure(Procedure node)

     {

-      dependencies.Add(node);

+      procedureDependencies.Add(node);

+      allDependenciesHaveChecksum &= node.Checksum != null;

 

       foreach (var param in node.InParams)

       {

@@ -58,7 +222,8 @@ namespace Microsoft.Boogie
 

     public override Function VisitFunction(Function node)

     {

-      dependencies.Add(node);

+      functionDependencies.Add(node);

+      allDependenciesHaveChecksum &= node.Checksum != null;

 

       if (node.DefinitionAxiom != null)

       {

@@ -70,7 +235,7 @@ namespace Microsoft.Boogie
 

     public override Cmd VisitCallCmd(CallCmd node)

     {

-      var visited = dependencies.Contains(node.Proc);

+      var visited = procedureDependencies.Contains(node.Proc);

       if (!visited)

       {

         VisitProcedure(node.Proc);

@@ -84,7 +249,7 @@ namespace Microsoft.Boogie
       var funCall = node.Fun as FunctionCall;

       if (funCall != null)

       {

-        var visited = dependencies.Contains(funCall.Func);

+        var visited = functionDependencies.Contains(funCall.Func);

         if (!visited)

         {

           VisitFunction(funCall.Func);

@@ -96,6 +261,15 @@ namespace Microsoft.Boogie
   }

 

 

+  static internal class Priority

+  {

+    public static int LOW = 1;

+    public static int MEDIUM = 2;

+    public static int HIGH = 3;

+    public static int SKIP = int.MaxValue;

+  }

+

+

   public class VerificationResultCache

   {

     private readonly ConcurrentDictionary<string, VerificationResult> Cache = new ConcurrentDictionary<string, VerificationResult>();

@@ -152,7 +326,7 @@ namespace Microsoft.Boogie
 

     public bool NeedsToBeVerified(Implementation impl)

     {

-      return VerificationPriority(impl) < int.MaxValue;

+      return VerificationPriority(impl) < Priority.SKIP;

     }

 

 

@@ -160,19 +334,19 @@ namespace Microsoft.Boogie
     {

       if (!Cache.ContainsKey(impl.Id))

       {

-        return 3;  // high priority (has been never verified before)

+        return Priority.HIGH;  // high priority (has been never verified before)

       }

       else if (Cache[impl.Id].Checksum != impl.Checksum)

       {

-        return 2;  // medium priority (old snapshot has been verified before)

+        return Priority.MEDIUM;  // medium priority (old snapshot has been verified before)

       }

       else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)

       {

-        return 1;  // low priority (the same snapshot has been verified before, but a callee has changed)

+        return Priority.LOW;  // low priority (the same snapshot has been verified before, but a callee has changed)

       }

       else

       {

-        return int.MaxValue;  // skip verification (highest priority to get them done as soon as possible)

+        return Priority.SKIP;  // skip verification (highest priority to get them done as soon as possible)

       }

     }

   }