DafnyExtension: Worked on integrating the verification result caching.

4 files changed, 102 insertions, 5 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 776cf601..72ef4205 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -419,7 +419,7 @@ namespace Microsoft.Dafny {
       PrintType(f.Type);

     }

 

-    void PrintSpec(string kind, List<Expression> ee, int indent) {

+    internal void PrintSpec(string kind, List<Expression> ee, int indent) {

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

       foreach (Expression e in ee) {

@@ -431,7 +431,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void PrintDecreasesSpec(Specification<Expression> decs, int indent) {

+    internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {

       Contract.Requires(decs != null);

       if (decs.Expressions != null && decs.Expressions.Count != 0) {

         Indent(indent);

@@ -446,7 +446,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs) {

+    internal void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs) {

       Contract.Requires(kind != null);

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

       if (ee != null && ee.Count != 0) {

@@ -461,7 +461,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent) {

+    internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent) {

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

       foreach (MaybeFreeExpression e in ee)

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e45e9eed..33a2a36a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -42,6 +42,8 @@ namespace Microsoft.Dafny {
     readonly Bpl.Program sink;

     readonly PredefinedDecls predef;

 

+    public bool InsertChecksums { get; set; }

+

     internal class PredefinedDecls {

       public readonly Bpl.Type RefType;

       public readonly Bpl.Type BoxType;

@@ -365,6 +367,22 @@ namespace Microsoft.Dafny {
           }

         }

       }

+

+      foreach (var decl in sink.TopLevelDeclarations)

+      {

+        var impl = decl as Implementation;

+        if (impl != null && impl.FindStringAttribute("checksum") == null)

+        {

+          impl.AddAttribute("checksum", "dummy");

+        }

+

+        var func = decl as Bpl.Function;

+        if (func != null && func.FindStringAttribute("checksum") == null)

+        {

+          func.AddAttribute("checksum", "dummy");

+        }

+      }

+

       return sink;

     }

 

@@ -1941,7 +1959,7 @@ namespace Microsoft.Dafny {
       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);

       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

       GenerateImplPrelude(m, inParams, outParams, builder, localVariables);

-

+      

       Bpl.StmtList stmts;

       if (!wellformednessProc) {

         if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoMethod)) {

@@ -2115,6 +2133,11 @@ namespace Microsoft.Dafny {
         localVariables, stmts, kv);

       sink.TopLevelDeclarations.Add(impl);

 

+      if (InsertChecksums)

+      {

+        InsertChecksum(m, impl);

+      }

+

       currentModule = null;

       codeContext = null;

       loopHeapVarCount = 0;

@@ -2122,6 +2145,48 @@ namespace Microsoft.Dafny {
       _tmpIEs.Clear();

     }

 

+    private static void InsertChecksum(Method m, Bpl.Declaration decl, bool specificationOnly = false)

+    {

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

+      using (var writer = new System.IO.StringWriter())

+      {

+        var printer = new Printer(writer);

+        printer.PrintAttributes(m.Attributes);

+        printer.PrintSpec("", m.Req, 0);

+        printer.PrintFrameSpecLine("", m.Mod.Expressions, 0, null);

+        printer.PrintSpec("", m.Ens, 0);

+        printer.PrintDecreasesSpec(m.Decreases, 0);

+        if (!specificationOnly && m.Body != null)

+        {

+          printer.PrintStatement(m.Body, 0);

+        }

+        md5.ComputeHash(Encoding.UTF8.GetBytes(writer.ToString()));

+      }

+      var checksum = string.Join("", md5.Hash);

+      decl.AddAttribute("checksum", checksum);

+    }

+

+    private static void InsertChecksum(Function f, Bpl.Declaration decl, bool specificationOnly = false)

+    {

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

+      using (var writer = new System.IO.StringWriter())

+      {

+        var printer = new Printer(writer);

+        printer.PrintAttributes(f.Attributes);

+        printer.PrintSpec("", f.Req, 0);

+        printer.PrintFrameSpecLine("", f.Reads, 0, null);

+        printer.PrintSpec("", f.Ens, 0);

+        printer.PrintDecreasesSpec(f.Decreases, 0);

+        if (!specificationOnly && f.Body != null)

+        {

+          printer.PrintExtendedExpr(f.Body, 0, false, false);

+        }

+        md5.ComputeHash(Encoding.UTF8.GetBytes(writer.ToString()));

+      }

+      var checksum = string.Join("", md5.Hash);

+      decl.AddAttribute("checksum", checksum);

+    }

+

     void CheckFrameWellFormed(List<FrameExpression> fes, VariableSeq locals, StmtListBuilder builder, ExpressionTranslator etran) {

       Contract.Requires(fes != null);

       Contract.Requires(locals != null);

@@ -2442,6 +2507,11 @@ namespace Microsoft.Dafny {
         req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null));

       sink.TopLevelDeclarations.Add(proc);

 

+      if (InsertChecksums)

+      {

+        InsertChecksum(f, proc, true);

+      }

+

       VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

       Bpl.VariableSeq locals = new Bpl.VariableSeq();

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

@@ -2519,6 +2589,11 @@ namespace Microsoft.Dafny {
         locals, builder.Collect(f.tok));

       sink.TopLevelDeclarations.Add(impl);

 

+      if (InsertChecksums)

+      {

+        InsertChecksum(f, impl);

+      }

+

       Contract.Assert(currentModule == f.EnclosingClass.Module);

       currentModule = null;

     }

@@ -3762,6 +3837,12 @@ namespace Microsoft.Dafny {
       }

       Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);

       Bpl.Function func = new Bpl.Function(f.tok, f.FullCompileName, typeParams, args, res);

+

+      if (InsertChecksums)

+      {

+        InsertChecksum(f, func);

+      }

+

       sink.TopLevelDeclarations.Add(func);

 

       if (f.IsRecursive) {

@@ -3771,6 +3852,12 @@ namespace Microsoft.Dafny {
 

       res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

       Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);

+

+      if (InsertChecksums)

+      {

+        InsertChecksum(f, canCallF);

+      }

+

       sink.TopLevelDeclarations.Add(canCallF);

     }

 

@@ -3885,6 +3972,11 @@ namespace Microsoft.Dafny {
       var name = MethodName(m, kind);

       var proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);

 

+      if (InsertChecksums)

+      {

+        InsertChecksum(m, proc, true);

+      }

+

       currentModule = null;

       codeContext = null;

 

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 4f3275f5..415bf996 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -40,6 +40,8 @@ namespace DafnyLanguage
         options.ApplyDefaultOptions();

 

         ExecutionEngine.printer = new ConsolePrinter();

+        // TODO(wuestholz): Turn this on as soon as the error locations are updated properly.

+        // Dafny.DafnyOptions.Clo.VerifySnapshots = true;

       }

     }

 

@@ -147,6 +149,7 @@ namespace DafnyLanguage
 

     public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {

       Dafny.Translator translator = new Dafny.Translator();

+      translator.InsertChecksums = true;

       Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

 

       PipelineOutcome oc = BoogiePipeline(boogieProgram, er);

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index f5faf697..1705e3ed 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -257,6 +257,8 @@ namespace DafnyLanguage
         bufferChangesPostVerificationStart.Clear();

         bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));

         verificationDisabled = false;

+        // TODO(wuestholz): Only drop verification results from this buffer.

+        Microsoft.Boogie.ExecutionEngine.EmptyCache();

         NotifyAboutChangedTags(_buffer.CurrentSnapshot);

       }

     }