Added support for verifying Dafny program snapshots from the command-line.

7 files changed, 49 insertions, 4 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e64c0da6..39b1ea95 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -17,6 +17,7 @@ namespace Microsoft.Dafny {
   public class Translator {

     [NotDelayed]

     public Translator() {

+      InsertChecksums = 0 < CommandLineOptions.Clo.VerifySnapshots;

       Bpl.Program boogieProgram = ReadPrelude();

       if (boogieProgram != null) {

         sink = boogieProgram;

@@ -2507,7 +2508,7 @@ namespace Microsoft.Dafny {
     public void InsertUniqueIdForImplementation(Bpl.Declaration decl)

     {

       var impl = decl as Bpl.Implementation;

-      var prefix = UniqueIdPrefix ?? decl.tok.filename;

+      var prefix = UniqueIdPrefix ?? System.Text.RegularExpressions.Regex.Replace(decl.tok.filename, @".v\d+.dfy", ".dfy");

       if (impl != null && !string.IsNullOrEmpty(prefix))

       {

         decl.AddAttribute("id", prefix + ":" + impl.Name + ":0");

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 8f5b5300..01ee269e 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Dafny
     }

 

 

-    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames)

+    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true)

     {

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

 

@@ -110,7 +110,21 @@ namespace Microsoft.Dafny
         {

           Console.WriteLine();

           Console.WriteLine("-------------------- {0} --------------------", f);

-          var ev = ProcessFiles(new List<string> { f });

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

+          if (exitValue != ev && ev != ExitValue.VERIFIED)

+          {

+            exitValue = ev;

+          }

+        }

+        return exitValue;

+      }

+

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

+      {

+        var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);

+        foreach (var s in snapshotsByVersion)

+        {

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

           if (exitValue != ev && ev != ExitValue.VERIFIED)

           {

             exitValue = ev;

@@ -213,7 +227,7 @@ namespace Microsoft.Dafny
           ExecutionEngine.CollectModSets(program);

           ExecutionEngine.CoalesceBlocks(program);

           ExecutionEngine.Inline(program);

-          return ExecutionEngine.InferAndVerify(program, stats);

+          return ExecutionEngine.InferAndVerify(program, stats, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? "main_program_id" : null);

 

         default:

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected outcome

diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy
new file mode 100644
index 00000000..73db9f9c
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v0.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures false;

diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy
new file mode 100644
index 00000000..28f9f283
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy
@@ -0,0 +1,8 @@
+method foo()

+{

+  bar();

+  assert false;

+}

+

+method bar()

+  ensures true;

diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg
new file mode 100644
index 00000000..07cb869f
--- /dev/null
+++ b/Test/dafny0/snapshots/lit.local.cfg
@@ -0,0 +1,5 @@
+# This test is unusual in that we don't use the .bpl files
+# directly on the command line. So instead we'll invoke
+# files in this directory with extension '.snapshot'. There
+# will only be one for now
+config.suffixes = ['.snapshot']
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
new file mode 100644
index 00000000..6d2f880f
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
new file mode 100644
index 00000000..7906e7a5
--- /dev/null
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 3 verified, 0 errors

+Snapshots0.v1.dfy(4,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 1 error