Added a feature for verifying several program snapshots (incl. result caching and prioritization).

9 files changed, 339 insertions, 67 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 99e9ee9e..a39e8696 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -12,6 +12,7 @@ namespace Microsoft.Boogie {
   using System;

   using System.IO;

   using System.Collections;

+  using System.Collections.Concurrent;

   using System.Collections.Generic;

   using PureCollections;

   using Microsoft.Boogie;

@@ -155,8 +156,29 @@ namespace Microsoft.Boogie {
       Dafny

     };

 

-    static void ProcessFiles(List<string> fileNames) {

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

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

+

+      if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)

+      {

+        var snapshots =

+          from n in fileNames

+          from f in Directory.GetFiles(Path.GetDirectoryName(Path.GetFullPath(n)), Path.GetFileNameWithoutExtension(n) + ".*" + Path.GetExtension(n))

+          select f;

+

+        var snapshotsByVersion =

+          from n in snapshots

+          group n by Path.GetFileNameWithoutExtension(n).Substring(Path.GetFileNameWithoutExtension(n).LastIndexOf(".")) into g

+          orderby g.Key

+          select g;

+

+        foreach (var s in snapshotsByVersion)

+        {

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

+        }

+        return;

+      }

+

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))

       {

           //BoogiePL.Errors.count = 0;

@@ -649,6 +671,25 @@ namespace Microsoft.Boogie {
       }

     }

 

+

+    internal struct VerificationResult

+    {

+      internal VerificationResult(string checksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

+      {

+        Checksum = checksum;

+        Outcome = outcome;

+        Errors = errors;

+      }

+

+      public readonly string Checksum;

+      public readonly ConditionGeneration.Outcome Outcome;

+      public readonly List<Counterexample> Errors;

+    }

+

+

+    static readonly ConcurrentDictionary<string, VerificationResult> VerificationResultCache = new ConcurrentDictionary<string, VerificationResult>();

+

+

     /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

@@ -790,83 +831,127 @@ namespace Microsoft.Boogie {
 

       // operate on a stable copy, in case it gets updated while we're running

       var decls = program.TopLevelDeclarations.ToArray();

-      foreach (Declaration decl in decls) {

-        Contract.Assert(decl != null);

+

+      var impls =

+        from d in decls

+        where d != null && d is Implementation && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(((Implementation)d).Name)) && !((Implementation)d).SkipVerification

+        select (Implementation)d;

+

+      var prioritizedImpls =

+        from i in impls

+        orderby i.Priority descending

+        select i;

+

+      foreach (var impl in prioritizedImpls)

+      {

         int prevAssertionCount = vcgen.CumulativeAssertionCount;

-        Implementation impl = decl as Implementation;

-        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

-          List<Counterexample/*!*/>/*?*/ errors;

-

-          DateTime start = new DateTime();  // to please compiler's definite assignment rules

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null) {

-            start = DateTime.UtcNow;

-            if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {

-              Console.WriteLine();

-              Console.WriteLine("Verifying {0} ...", impl.Name);

+        List<Counterexample/*!*/>/*?*/ errors;

+

+        DateTime start = new DateTime();  // to please compiler's definite assignment rules

+        if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null)

+        {

+          start = DateTime.UtcNow;

+          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)

+          {

+            Console.WriteLine();

+            Console.WriteLine("Verifying {0} ...", impl.Name);

+          }

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

+          }

+        }

+

+        VCGen.Outcome outcome;

+        try

+        {

+          if (CommandLineOptions.Clo.inferLeastForUnsat != null)

+          {

+            var svcgen = vcgen as VC.StratifiedVCGen;

+            Contract.Assert(svcgen != null);

+            var ss = new HashSet<string>();

+            foreach (var tdecl in program.TopLevelDeclarations)

+            {

+              var c = tdecl as Constant;

+              if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+              ss.Add(c.Name);

             }

-            if (CommandLineOptions.Clo.XmlSink != null) {

-              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

+            outcome = svcgen.FindLeastToVerify(impl, ref ss);

+            errors = new List<Counterexample>();

+            Console.Write("Result: ");

+            foreach (var s in ss)

+            {

+              Console.Write("{0} ", s);

             }

+            Console.WriteLine();

           }

-

-          VCGen.Outcome outcome;

-          try {

-            if (CommandLineOptions.Clo.inferLeastForUnsat != null) {

-              var svcgen = vcgen as VC.StratifiedVCGen;

-              Contract.Assert(svcgen != null);

-              var ss = new HashSet<string>();

-              foreach (var tdecl in program.TopLevelDeclarations) {

-                var c = tdecl as Constant;

-                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

-                ss.Add(c.Name);

-              }

-              outcome = svcgen.FindLeastToVerify(impl, ref ss);

-              errors = new List<Counterexample>();

-              Console.Write("Result: ");

-              foreach (var s in ss) {

-                Console.Write("{0} ", s);

+          else

+          {

+            if (!VerificationResultCache.ContainsKey(impl.Id) || VerificationResultCache[impl.Id].Checksum != impl.Checksum)

+            {

+              outcome = vcgen.VerifyImplementation(impl, out errors);

+            }

+            else

+            {

+              if (CommandLineOptions.Clo.Trace)

+              {

+                Console.WriteLine("Retrieving cached verification result for implementation {0}...", impl.Name);

               }

-              Console.WriteLine();

+              var result = VerificationResultCache[impl.Id];

+              outcome = result.Outcome;

+              errors = result.Errors;

             }

-            else {

-              outcome = vcgen.VerifyImplementation(impl, out errors);

-              if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {

-                for (int i = 0; i < errors.Count; i++) {

-                  errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

-                }

+            if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null)

+            {

+              for (int i = 0; i < errors.Count; i++)

+              {

+                errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

               }

             }

           }

-          catch (VCGenException e) {

-            ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          }

-          catch (UnexpectedProverOutputException upo) {

-            AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

-            errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

-          }

+        }

+        catch (VCGenException e)

+        {

+          ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

+          errors = null;

+          outcome = VCGen.Outcome.Inconclusive;

+        }

+        catch (UnexpectedProverOutputException upo)

+        {

+          AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+          errors = null;

+          outcome = VCGen.Outcome.Inconclusive;

+        }

 

-          string timeIndication = "";

-          DateTime end = DateTime.UtcNow;

-          TimeSpan elapsed = end - start;

-          if (CommandLineOptions.Clo.Trace) {

-            int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

-            timeIndication = string.Format("  [{0:F3} s, {1} proof obligation{2}]  ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");

-          } else if (CommandLineOptions.Clo.TraceProofObligations) {

-            int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

-            timeIndication = string.Format("  [{0} proof obligation{1}]  ", poCount, poCount == 1 ? "" : "s");

-          }

+        string timeIndication = "";

+        DateTime end = DateTime.UtcNow;

+        TimeSpan elapsed = end - start;

+        if (CommandLineOptions.Clo.Trace)

+        {

+          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

+          timeIndication = string.Format("  [{0:F3} s, {1} proof obligation{2}]  ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");

+        }

+        else if (CommandLineOptions.Clo.TraceProofObligations)

+        {

+          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

+          timeIndication = string.Format("  [{0} proof obligation{1}]  ", poCount, poCount == 1 ? "" : "s");

+        }

 

-          ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

+        if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

+        {

+          var result = new VerificationResult(impl.Checksum, outcome, errors);

+          VerificationResultCache[impl.Id] = result;

+        }

 

-          if (CommandLineOptions.Clo.XmlSink != null) {

-            CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

-          }

-          if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {

-            Console.Out.Flush();

-          }

+        ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

+

+        if (CommandLineOptions.Clo.XmlSink != null)

+        {

+          CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

+        }

+        if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+        {

+          Console.Out.Flush();

         }

       }

         

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c3a9a164..55b37f13 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2567,6 +2567,41 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public string Checksum

+    {

+      get

+      {

+        return FindStringAttribute("checksum");

+      }

+    }

+

+    public string Id

+    {

+      get

+      {

+        var id = FindStringAttribute("id");

+        if (id == null)

+        {

+          id = Name + ":0";

+        }

+        return id;

+      }

+    }

+

+    public int Priority

+    {

+      get

+      {

+        int priority = 0;

+        CheckIntAttribute("priority", ref priority);

+        if (priority <= 0)

+        {

+          priority = 1;

+        }

+        return priority;

+      }

+    }

+

     public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

       Contract.Requires(structuredStmts != null);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index f2299cc9..683935b4 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -363,6 +363,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3);  // 0 = print only structured,  1 = both structured and unstructured,  2 = only unstructured

     }

 

+    public bool VerifySnapshots;

     public string PrintFile = null;

     public int PrintUnstructured = 0;

     public int DoomStrategy = -1;

@@ -1311,7 +1312,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

               ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||

               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

-              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

+              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||

+              ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Test/alltests.txt b/Test/alltests.txt
index ebe396e9..c0eec7ad 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -28,3 +28,4 @@ stratifiedinline Use    Stratified inlining benchmarks
 extractloops     Use    Extract loops benchmarks

 havoc0           Use    HAVOC-generated bpl files

 AbsHoudini       Postponed    Test for abstract houdini

+snapshots        Use    Tests for program snapshot verification

diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
new file mode 100644
index 00000000..aac9cd03
--- /dev/null
+++ b/Test/snapshots/Answer
@@ -0,0 +1,27 @@
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0

+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): anon0

+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): anon0

+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): anon0

+

+Boogie program verifier finished with 0 verified, 4 errors

+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0

+c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): anon0

+

+Boogie program verifier finished with 2 verified, 2 errors

+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0

+

+Boogie program verifier finished with 2 verified, 1 error

diff --git a/Test/snapshots/Snapshots0.v0.bpl b/Test/snapshots/Snapshots0.v0.bpl
new file mode 100644
index 00000000..c75e9520
--- /dev/null
+++ b/Test/snapshots/Snapshots0.v0.bpl
@@ -0,0 +1,42 @@
+// id = "P1:0"

+// priority = 3

+// checksum = "123"

+// 

+// Action: verify

+procedure {:priority 3} {:checksum "123"} P1()

+{

+    assert false;

+}

+

+

+// id = "P2:0"

+// priority = 3

+// checksum = null

+//

+// Action: verify

+procedure {:priority 3} P2()

+{

+    assert false;

+}

+

+

+// id = "P3:0"

+// priority = 1

+// checksum = null

+//

+// Action: verify

+procedure P3()

+{

+    assert false;

+}

+

+

+// id = "P0:1"

+// priority = 5

+// checksum = "012"

+//

+// Action: verify

+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()

+{

+    assert false;

+}

diff --git a/Test/snapshots/Snapshots0.v1.bpl b/Test/snapshots/Snapshots0.v1.bpl
new file mode 100644
index 00000000..efd30c8f
--- /dev/null
+++ b/Test/snapshots/Snapshots0.v1.bpl
@@ -0,0 +1,42 @@
+// id = "P0:1"

+// priority = 5

+// checksum = "012"

+//

+// Action: skip

+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()

+{

+    assert false;

+}

+

+

+// id = "P1:0"

+// priority = 5

+// checksum = "234"

+//

+// Action: verify (unknown checksum)

+procedure {:priority 5} {:checksum "234"} P1()

+{

+    assert true;

+}

+

+

+// id = "P2:0"

+// priority = 3

+// checksum = null

+//

+// Action: verify (no checksum)

+procedure {:priority 3} P2()

+{

+    assert false;

+}

+

+

+// id = "P3:0"

+// priority = 1

+// checksum = "234"

+//

+// Action: verify (unknown checksum)

+procedure {:checksum "234"} P3()

+{

+    assert true;

+}

diff --git a/Test/snapshots/Snapshots0.v2.bpl b/Test/snapshots/Snapshots0.v2.bpl
new file mode 100644
index 00000000..156977f7
--- /dev/null
+++ b/Test/snapshots/Snapshots0.v2.bpl
@@ -0,0 +1,31 @@
+// id = "P0:1"

+// priority = 5

+// checksum = "012"

+//

+// Action: skip

+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()

+{

+    assert false;

+}

+

+

+// id = "P1:0"

+// priority = 1

+// checksum = "234"

+//

+// Action: skip

+procedure {:priority 1} {:checksum "234"} P1()

+{

+    assert true;

+}

+

+

+// id = "P3:0"

+// priority = 1

+// checksum = "234"

+//

+// Action: skip

+procedure {:checksum "234"} P3()

+{

+    assert true;

+}

diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
new file mode 100644
index 00000000..05421b85
--- /dev/null
+++ b/Test/snapshots/runtest.bat
@@ -0,0 +1,7 @@
+@echo off

+setlocal

+

+set BOOGIEDIR=..\..\Binaries

+set BGEXE=%BOOGIEDIR%\Boogie.exe

+

+%BGEXE% %* /verifySnapshots Snapshots0.bpl