Worked on adding support for "canned errors".

5 files changed, 60 insertions, 30 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e67be411..6568eb75 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2626,7 +2626,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    sealed class ChecksumComparer : IEqualityComparer<byte[]>

+    public sealed class ChecksumComparer : IEqualityComparer<byte[]>

     {

       static IEqualityComparer<byte[]> defaultComparer;

       public static IEqualityComparer<byte[]> Default

@@ -2764,18 +2764,24 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public ISet<byte[]> ErrorChecksumsInCachedSnapshot { get; private set; }

+    public IDictionary<byte[], object> ErrorChecksumToCachedError { get; private set; }

 

-    public void SetErrorChecksumsInCachedSnapshot(IEnumerable<byte[]> errorChecksums)

+    public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], object>> errors)

     {

-      ErrorChecksumsInCachedSnapshot = new HashSet<byte[]>(errorChecksums, ChecksumComparer.Default);

+      Contract.Requires(errors != null);

+

+      ErrorChecksumToCachedError = new Dictionary<byte[], object>(ChecksumComparer.Default);

+      foreach (var kv in errors)

+      {

+        ErrorChecksumToCachedError[kv.Item1] = kv.Item2;

+      }

     }

 

     public bool NoErrorsInCachedSnapshot

     {

       get

       {

-        return ErrorChecksumsInCachedSnapshot != null && !ErrorChecksumsInCachedSnapshot.Any();

+        return ErrorChecksumToCachedError != null && !ErrorChecksumToCachedError.Any();

       }

     }

 

@@ -2783,7 +2789,7 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        return ErrorChecksumsInCachedSnapshot != null && ErrorChecksumsInCachedSnapshot.Any();

+        return ErrorChecksumToCachedError != null && ErrorChecksumToCachedError.Any();

       }

     }

 

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 48a35e80..04726cff 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -420,15 +420,20 @@ namespace Microsoft.Boogie
     static IDictionary<string, IList<CancellationTokenSource>> RequestIdToCancellationTokenSources = new ConcurrentDictionary<string, IList<CancellationTokenSource>>();

 

 

-    public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true)

+    public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

 

+      if (programId == null)

+      {

+        programId = "main_program_id";

+      }

+

       if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)

       {

         foreach (var f in fileNames)

         {

-          ProcessFiles(new List<string> { f }, lookForSnapshots);

+          ProcessFiles(new List<string> { f }, lookForSnapshots, f);

         }

         return;

       }

@@ -438,7 +443,7 @@ namespace Microsoft.Boogie
         var snapshotsByVersion = LookForSnapshots(fileNames);

         foreach (var s in snapshotsByVersion)

         {

-          ProcessFiles(new List<string>(s), false);

+          ProcessFiles(new List<string>(s), false, programId);

         }

         return;

       }

@@ -493,7 +498,7 @@ namespace Microsoft.Boogie
         Inline(program);

 

         var stats = new PipelineStatistics();

-        oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? "main_program_id" : null);

+        oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? programId : null);

         switch (oc)

         {

           case PipelineOutcome.Done:

@@ -886,7 +891,7 @@ namespace Microsoft.Boogie
 

       if (1 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId);

+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId);

       }

 

       #region Verify each implementation

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 916340a5..b9c04661 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie
       return result;

     }

 

-    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId)

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

     {

       var eai = new CachedVerificationResultInjector(program, implementations);

 

@@ -121,7 +121,7 @@ namespace Microsoft.Boogie
       {

         int priority;

         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);

-        if (vr != null)

+        if (vr != null && vr.ProgramId == programId)

         {

           if (priority == Priority.LOW)

           {

@@ -172,11 +172,11 @@ namespace Microsoft.Boogie
     {

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

       {

-        implementation.SetErrorChecksumsInCachedSnapshot(result.Errors.Select(cex => cex.Checksum));

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

       }

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

       {

-        implementation.SetErrorChecksumsInCachedSnapshot(new List<byte[]>());

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

       }

     }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index abbcf4aa..33f36a31 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1513,7 +1513,7 @@ namespace VC {
                       && currentImplementation.InjectedAssumptionVariables.Any()

                       && ac.Checksum != null

                       && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

-                      && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum))))

+                      && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum))))

           {

             // Bind the assertion expression to a local variable.

             var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, new IdentifierExpr(Token.NoToken, CurrentTemporaryVariableForAssertions));

@@ -1529,10 +1529,11 @@ namespace VC {
                    && currentImplementation.AnyErrorsInCachedSnapshot

                    && ac.Checksum != null

                    && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

-                   && currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum)

+                   && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

                    && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

-            // TODO(wuestholz): Uncomment this once the canned errors are reported.

+            // Turn it into an assume statement.

+            // TODO(wuestholz): Uncomment this once the canned errors are reported.            

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

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

             currentImplementation.AddCannedFailingAssertion(ac);

@@ -1552,7 +1553,7 @@ namespace VC {
             || (currentImplementation.AnyErrorsInCachedSnapshot

                 && pc.Checksum != null

                 && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))

-                && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum)))

+                && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(pc.Checksum)))

         {

           passiveCmds.Add(pc);

         }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 9aa764e2..3e601511 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1481,17 +1481,6 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

-      // Report all canned failing assertions for this implementation.

-      if (impl.CannedFailingAssertions != null)

-      {

-        foreach (var a in impl.CannedFailingAssertions)

-        {

-          // TODO(wuestholz): Implement this.

-          // var cex = AssertCmdToCounterexample(a, ...);

-          // callback.OnCounterexample(cex, ...);

-        }

-      }

-

       // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct

       foreach (var b in impl.Blocks)

       {

@@ -1631,6 +1620,34 @@ namespace VC {
 

       Outcome outcome = Outcome.Correct;

 

+      // Report all canned failing assertions for this implementation.

+      if (impl.CannedFailingAssertions != null && impl.CannedFailingAssertions.Any())

+      {

+        // TODO(wuestholz): Uncomment this.

+        // outcome = Outcome.Errors;

+        foreach (var a in impl.CannedFailingAssertions)

+        {

+          var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;

+          if (oldCex != null)

+          {

+            // TODO(wuestholz): Maybe we could create a "fresh" counterexample instead.

+            // TransferCmd trCmd = null;

+            // var oldRetCex = oldCex as ReturnCounterexample;

+            // if (oldRetCex != null)

+            // {

+            //   trCmd = oldRetCex.FailingReturn;

+            // }

+            // var cex = AssertCmdToCounterexample(a, trCmd, oldCex.Trace, oldCex.Model, oldCex.MvInfo, oldCex.Context);

+            // cex.RequestId = oldCex.RequestId;

+

+            // TODO(wuestholz): Uncomment this.

+            // var oldReqId = oldCex.RequestId;

+            // callback.OnCounterexample(oldCex, null);

+            // oldCex.RequestId = oldReqId;

+          }

+        }

+      }

+

       Cores = CommandLineOptions.Clo.VcsCores;

       Stack<Split> work = new Stack<Split>();

       List<Split> currently_running = new List<Split>();

@@ -2660,6 +2677,7 @@ namespace VC {
         #region Get rid of empty blocks

         {

           RemoveEmptyBlocksIterative(impl.Blocks);

+          // TODO(wuestholz): Update impl.AssertionChecksums and maybe impl.CannedFailingAssertions.

           impl.PruneUnreachableBlocks();

         }

         #endregion Get rid of empty blocks