Refactor the error reporting code

The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.

1 files changed, 52 insertions, 67 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4223fb7f..cb71b80d 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -6,24 +6,25 @@ using IToken = Microsoft.Boogie.IToken;
 

 namespace Microsoft.Dafny

 {

-  [ContractClass(typeof(IRewriterContracts))]

-  public interface IRewriter

+  public abstract class IRewriter

   {

-    void PreResolve(ModuleDefinition m);

-    void PostResolve(ModuleDefinition m);

-    // After SCC/Cyclicity/Recursivity analysis:

-    void PostCyclicityResolve(ModuleDefinition m);

-  }

-  [ContractClassFor(typeof(IRewriter))]

-  abstract class IRewriterContracts : IRewriter

-  {

-    public void PreResolve(ModuleDefinition m) {

+    protected readonly ErrorReporter reporter;

+

+    public IRewriter(ErrorReporter reporter) {

+      Contract.Requires(reporter != null);

+      this.reporter = reporter;

+    }

+

+    internal virtual void PreResolve(ModuleDefinition m) {

       Contract.Requires(m != null);

     }

-    public void PostResolve(ModuleDefinition m) {

+

+    internal virtual void PostResolve(ModuleDefinition m) {

       Contract.Requires(m != null);

     }

-    public void PostCyclicityResolve(ModuleDefinition m) {

+

+    // After SCC/Cyclicity/Recursivity analysis:

+    internal virtual void PostCyclicityResolve(ModuleDefinition m) {

       Contract.Requires(m != null);

     }

   }

@@ -37,33 +38,26 @@ namespace Microsoft.Dafny
     }

   }

 

-  public class TriggersRewriter : IRewriter {

-    Resolver Resolver;

-

-    internal TriggersRewriter(Resolver resolver) {

-      Contract.Requires(resolver != null);

-      this.Resolver = resolver;

+  public class TriggerGeneratingRewriter : IRewriter {

+    internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {

+      Contract.Requires(reporter != null);

     }

 

-    public void PreResolve(ModuleDefinition m) { }

-

-    public void PostResolve(ModuleDefinition m) {

+    internal override void PostResolve(ModuleDefinition m) {

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         if (decl is Function) {

           var function = (Function)decl;

-          TriggerGenerator.AddTriggers(function.Ens, Resolver);

-          TriggerGenerator.AddTriggers(function.Req, Resolver);

-          TriggerGenerator.AddTriggers(function.Body, Resolver);

+          //TriggerGenerator.AddTriggers(function.Ens, Resolver);

+          //TriggerGenerator.AddTriggers(function.Req, Resolver);

+          //TriggerGenerator.AddTriggers(function.Body, Resolver);

         } else if (decl is Method) {

           var method = (Method)decl;

-          TriggerGenerator.AddTriggers(method.Ens, Resolver);

-          TriggerGenerator.AddTriggers(method.Req, Resolver);

-          TriggerGenerator.AddTriggers(method.Body, Resolver);

+          //TriggerGenerator.AddTriggers(method.Ens, Resolver);

+          //TriggerGenerator.AddTriggers(method.Req, Resolver);

+          //TriggerGenerator.AddTriggers(method.Body, Resolver);

         }

       }

     }

-

-    public void PostCyclicityResolve(ModuleDefinition m) { }

   }

 

   /// <summary>

@@ -106,7 +100,12 @@ namespace Microsoft.Dafny
   /// </summary>

   public class AutoContractsRewriter : IRewriter

   {

-    public void PreResolve(ModuleDefinition m) {

+    public AutoContractsRewriter(ErrorReporter reporter)

+      : base(reporter) {

+      Contract.Requires(reporter != null);

+    }

+

+    internal override void PreResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

         bool sayYes = true;

         if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {

@@ -162,7 +161,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    public void PostResolve(ModuleDefinition m) {

+    internal override void PostResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

         bool sayYes = true;

         if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {

@@ -171,9 +170,6 @@ namespace Microsoft.Dafny
       }

     }

 

-    public void PostCyclicityResolve(ModuleDefinition m) { 

-    }

-

     void ProcessClassPostResolve(ClassDecl cl) {

       // Find all fields of a reference type, and make a note of whether or not the reference type has a Repr field.

       // Also, find the Repr field and the function Valid in class "cl"

@@ -416,20 +412,20 @@ namespace Microsoft.Dafny
   /// specifically asks to see it via the reveal_foo() lemma

   /// </summary>

   public class OpaqueFunctionRewriter : IRewriter {

-    readonly ResolutionErrorReporter reporter;

     protected Dictionary<Function, Function> fullVersion; // Given an opaque function, retrieve the full

     protected Dictionary<Function, Function> original;    // Given a full version of an opaque function, find the original opaque version

     protected Dictionary<Lemma, Function> revealOriginal; // Map reveal_* lemmas back to their original functions

 

-    public OpaqueFunctionRewriter(ResolutionErrorReporter reporter)

-      : base() {

-      this.reporter = reporter;

+    public OpaqueFunctionRewriter(ErrorReporter reporter)

+      : base(reporter) {

+      Contract.Requires(reporter != null);

+

       fullVersion = new Dictionary<Function, Function>();

       original = new Dictionary<Function, Function>();

       revealOriginal = new Dictionary<Lemma, Function>();

     }

 

-    public void PreResolve(ModuleDefinition m) {

+    internal override void PreResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

         if (d is ClassDecl) {

           DuplicateOpaqueClassFunctions((ClassDecl)d);

@@ -437,7 +433,7 @@ namespace Microsoft.Dafny
       }

     }    

 

-    public void PostResolve(ModuleDefinition m) {

+    internal override void PostResolve(ModuleDefinition m) {

       // Fix up the ensures clause of the full version of the function,

       // since it may refer to the original opaque function      

       foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {        

@@ -462,7 +458,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    public void PostCyclicityResolve(ModuleDefinition m) {

+    internal override void PostCyclicityResolve(ModuleDefinition m) {

       // Add layer quantifier if the function is recursive 

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         if (decl is Lemma) {

@@ -507,7 +503,7 @@ namespace Microsoft.Dafny
           if (!Attributes.Contains(f.Attributes, "opaque")) {

             // Nothing to do

           } else if (f.IsProtected) {

-            reporter.Error(f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");

+            reporter.Error(MessageSource.Rewriter, f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");

           } else if (!RefinementToken.IsInherited(f.tok, c.Module)) {

             // Create a copy, which will be the internal version with a full body

             // which will allow us to verify that the ensures are true

@@ -721,19 +717,16 @@ namespace Microsoft.Dafny
   /// </summary>

   public class AutoReqFunctionRewriter : IRewriter {

     Function parentFunction;

-    Resolver resolver;

     OpaqueFunctionRewriter opaqueInfo;

     bool containsMatch; // TODO: Track this per-requirement, rather than per-function

 

-    public AutoReqFunctionRewriter(Resolver r, OpaqueFunctionRewriter o) {

-      this.resolver = r;

+    public AutoReqFunctionRewriter(ErrorReporter reporter, OpaqueFunctionRewriter o)

+      : base(reporter) {

+      Contract.Requires(reporter != null);

       this.opaqueInfo = o;

     }

 

-    public void PreResolve(ModuleDefinition m) { 

-    }    

-

-    public void PostResolve(ModuleDefinition m) {

+    internal override void PostResolve(ModuleDefinition m) {

       var components = m.CallGraph.TopologicallySortedComponents();

 

       foreach (var scComponent in components) {  // Visit the call graph bottom up, so anything we call already has its prequisites calculated

@@ -806,9 +799,6 @@ namespace Microsoft.Dafny
       }

     }

 

-    public void PostCyclicityResolve(ModuleDefinition m) { 

-    }

-

     Expression subVars(List<Formal> formals, List<Expression> values, Expression e, Expression f_this) {

       Contract.Assert(formals != null);

       Contract.Assert(values != null);

@@ -839,7 +829,7 @@ namespace Microsoft.Dafny
       }

 

       if (!tip.Equals("")) {

-        resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);

+        reporter.Info(MessageSource.Rewriter, f.tok, tip);

         if (DafnyOptions.O.AutoReqPrintFile != null) {

           using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {

             writer.WriteLine(f.Name);

@@ -866,7 +856,7 @@ namespace Microsoft.Dafny
       }

 

       if (!tip.Equals("")) {

-        resolver.ReportAdditionalInformation(method.tok, tip, method.tok.val.Length);

+        reporter.Info(MessageSource.Rewriter, method.tok, tip);

         if (DafnyOptions.O.AutoReqPrintFile != null) {

           using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {

             writer.WriteLine(method.Name);

@@ -1061,7 +1051,7 @@ namespace Microsoft.Dafny
             Expression allReqsSatisfied = andify(e.Term.tok, auto_reqs);

             Expression allReqsSatisfiedAndTerm = Expression.CreateAnd(allReqsSatisfied, e.Term);

             e.UpdateTerm(allReqsSatisfiedAndTerm);

-            resolver.ReportAdditionalInformation(e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&", e.tok.val.Length);

+            reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&");

         }

       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

@@ -1108,7 +1098,12 @@ namespace Microsoft.Dafny
   /// </summary>

   public class TimeLimitRewriter : IRewriter

   {

-    public void PreResolve(ModuleDefinition m) {

+    public TimeLimitRewriter(ErrorReporter reporter)

+      : base(reporter) {

+      Contract.Requires(reporter != null);

+    }

+

+    internal override void PreResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

         if (d is ClassDecl) {

           var c = (ClassDecl)d;

@@ -1136,16 +1131,6 @@ namespace Microsoft.Dafny
         }

       }

     }

-

-    public void PostResolve(ModuleDefinition m)

-    {

-      // Nothing to do here

-    }

-

-    public void PostCyclicityResolve(ModuleDefinition m) {

-      // Nothing to do here

-    }

-

   }