Did some refactoring.

2 files changed, 14 insertions, 37 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 76caa5d3..a431904e 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -337,14 +337,17 @@ namespace Microsoft.Boogie
     public ConditionGeneration.Outcome Outcome { get; set; }

     public List<Counterexample> Errors;

 

-    public VerificationResult(string requestId, string checksum, string depsChecksum, string implementationName, IToken implementationToken, string programId = null)

+    public ISet<byte[]> AssertionChecksums { get; private set; }

+

+    public VerificationResult(string requestId, Implementation implementation, string programId = null)

     {

-      Checksum = checksum;

-      DependeciesChecksum = depsChecksum;

+      Checksum = implementation.Checksum;

+      DependeciesChecksum = implementation.DependencyChecksum;

       RequestId = requestId;

-      ImplementationName = implementationName;

-      ImplementationToken = implementationToken;

+      ImplementationName = implementation.Name;

+      ImplementationToken = implementation.tok;

       ProgramId = programId;

+      AssertionChecksums = implementation.AssertionChecksums;

     }

   }

 

@@ -1131,7 +1134,7 @@ namespace Microsoft.Boogie
       {

         #region Verify the implementation

 

-        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependencyChecksum, impl.Name, impl.tok, programId);

+        verificationResult = new VerificationResult(requestId, impl, programId);

 

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

         {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 268ab9bd..7f33ecef 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -130,13 +130,12 @@ namespace Microsoft.Boogie
             run.LowPriorityImplementationCount++;

             if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

             {

-              SetErrorChecksumsInCachedSnapshot(impl, vr);

+              SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);

               if (vr.ProgramId != null)

               {

                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

                 if (p != null)

                 {

-                  SetAssertionChecksumsInCachedSnapshot(impl, p);

                   eai.Inject(impl, p);

                   run.RewrittenImplementationCount++;

                 }

@@ -148,13 +147,12 @@ namespace Microsoft.Boogie
             run.MediumPriorityImplementationCount++;

             if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

             {

-              SetErrorChecksumsInCachedSnapshot(impl, vr);

+              SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);

               if (vr.ProgramId != null)

               {

                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

                 if (p != null)

                 {

-                  SetAssertionChecksumsInCachedSnapshot(impl, p);

                   eai.Inject(impl, p);

                   run.RewrittenImplementationCount++;

                 }

@@ -168,14 +166,6 @@ namespace Microsoft.Boogie
           else if (priority == Priority.SKIP)

           {

             run.SkippedImplementationCount++;

-            if (vr.ProgramId != null)

-            {

-              var p = ExecutionEngine.CachedProgram(vr.ProgramId);

-              if (p != null)

-              {

-                SetAssertionChecksums(impl, p);

-              }

-            }

           }

         }

       }

@@ -183,33 +173,17 @@ namespace Microsoft.Boogie
       Statistics.AddRun(requestId, run);

     }

 

-    private static void SetErrorChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)

+    private static void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)

     {

       if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

       {

         implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], object>(cex.Checksum, cex)));

+        implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;

       }

       else if (result.Outcome == ConditionGeneration.Outcome.Correct)

       {

         implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], object>>());

-      }

-    }

-

-    private static void SetAssertionChecksums(Implementation implementation, Program program)

-    {

-      var implPrevSnap = program.FindImplementation(implementation.Id);

-      if (implPrevSnap != null)

-      {

-        implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;

-      }

-    }

-

-    private static void SetAssertionChecksumsInCachedSnapshot(Implementation implementation, Program program)

-    {

-      var cachedImpl = program.FindImplementation(implementation.Id);

-      if (cachedImpl != null)

-      {

-        implementation.AssertionChecksumsInCachedSnapshot = cachedImpl.AssertionChecksums;

+        implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;

       }

     }