Add support for counting spec/impl/proof lines by supressing, e.g., ghost statements

4 files changed, 118 insertions, 41 deletions

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 60578e33..34b509a0 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -11,6 +11,21 @@ using Bpl = Microsoft.Boogie;
 

 namespace Microsoft.Dafny {

   public class Main {

+

+      private static void MaybePrintProgram(Program program, string filename)

+      {

+          if (filename != null) {

+              TextWriter tw;

+              if (filename == "-") {

+                  tw = System.Console.Out;

+              } else {

+                  tw = new System.IO.StreamWriter(filename);

+              }

+              Printer pr = new Printer(tw, DafnyOptions.O.PrintMode);

+              pr.PrintProgram(program);

+          }

+      }

+   

     /// <summary>

     /// Returns null on success, or an error string otherwise.

     /// </summary>

@@ -47,35 +62,14 @@ namespace Microsoft.Dafny {
 

       program = new Program(programName, module, builtIns);

 

-      if (DafnyOptions.O.DafnyPrintFile != null) {

-        string filename = DafnyOptions.O.DafnyPrintFile;

-        if (filename == "-") {

-          Printer pr = new Printer(System.Console.Out);

-          pr.PrintProgram(program);

-        } else {

-          using (TextWriter writer = new System.IO.StreamWriter(filename)) {

-            Printer pr = new Printer(writer);

-            pr.PrintProgram(program);

-          }

-        }

-      }

+      MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile);

 

       if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }

 

       Dafny.Resolver r = new Dafny.Resolver(program);

       r.ResolveProgram(program);

-      if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

-        string filename = DafnyOptions.O.DafnyPrintResolvedFile;

-        if (filename == "-") {

-          Printer pr = new Printer(System.Console.Out);

-          pr.PrintProgram(program);

-        } else {

-          using (TextWriter writer = new System.IO.StreamWriter(filename)) {

-            Printer pr = new Printer(writer);

-            pr.PrintProgram(program);

-          }

-        }

-      }

+      MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile);

+

       if (r.ErrorCount != 0) {

         return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, program.Name);

       }

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index aa275ade..f9146cca 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -35,6 +35,9 @@ namespace Microsoft.Dafny
     public int InductionHeuristic = 6;

     public string DafnyPrelude = null;

     public string DafnyPrintFile = null;

+    public enum PrintModes { Everything, NoIncludes, NoGhost };

+    public PrintModes PrintMode;

+    public bool DafnyVerify = true;

     public string DafnyPrintResolvedFile = null;

     public bool Compile = true;

     public bool ForceCompile = false;

@@ -43,6 +46,7 @@ namespace Microsoft.Dafny
     public bool DisallowIncludes = false;

     public bool DisableNLarith = false;

     public string AutoReqPrintFile = null;

+    public bool ignoreAutoReq = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -60,6 +64,26 @@ namespace Microsoft.Dafny
           }

           return true;

 

+        case "printMode":

+          if (ps.ConfirmArgumentCount(1)) {

+            if (args[ps.i].Equals("Everything")) {

+              PrintMode = PrintModes.Everything;

+            }

+            else if (args[ps.i].Equals("NoIncludes"))

+            {

+                PrintMode = PrintModes.NoIncludes;

+            }

+            else if (args[ps.i].Equals("NoGhost"))

+            {

+                PrintMode = PrintModes.NoGhost;

+            }

+            else

+            {

+                throw new Exception("Invalid value for printMode");

+            }

+          }

+          return true;

+

         case "rprint":

           if (ps.ConfirmArgumentCount(1)) {

             DafnyPrintResolvedFile = args[ps.i];

@@ -77,6 +101,15 @@ namespace Microsoft.Dafny
             return true;

           }

 

+        case "dafnyVerify":

+            {

+                int verify = 0;

+                if (ps.GetNumericArgument(ref verify, 2)) {

+                    DafnyVerify = verify != 0; // convert to boolean

+                }

+                return true;

+            }

+

         case "spillTargetCode": {

             int spill = 0;

             if (ps.GetNumericArgument(ref spill, 2)) {

@@ -116,6 +149,10 @@ namespace Microsoft.Dafny
           }

           return true;

 

+        case "noAutoReq":

+          ignoreAutoReq = true;

+          return true;

+

         default:

           break;

       }

@@ -146,9 +183,17 @@ namespace Microsoft.Dafny
   /dprint:<file>

                 print Dafny program after parsing it

                 (use - as <file> to print to console)

+  /printMode:<Everything|NoIncludes|NoGhost>

+                NoIncludes disables printing of {:verify false} methods incorporated via the

+                include mechanism, as well as datatypes and fields included from other files.

+                NoGhost disables printing of functions, ghost methods, and proof statements in

+                implementation methods.  It also disables anything NoIncludes disables.

   /rprint:<file>

                 print Dafny program after resolving it

                 (use - as <file> to print to console)

+  /dafnyVerify:<n>

+                0 - stop after typechecking

+                1 - continue on to translation, verification, and compilation

   /compile:<n>  0 - do not compile Dafny program

                 1 (default) - upon successful verification of the Dafny

                     program, compile Dafny program to .NET assembly

@@ -185,6 +230,7 @@ namespace Microsoft.Dafny
                 Results in more manual work, but also produces more predictable behavior.

   /autoReqPrint:<file>

                 Print out requirements that were automatically generated by autoReq.

+  /noAutoReq    Ignore autoReq attributes

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index c1a911f6..3b1c018c 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -14,6 +14,7 @@ using Bpl = Microsoft.Boogie;
 namespace Microsoft.Dafny {

   public class Printer {

     TextWriter wr;

+    DafnyOptions.PrintModes printMode;

 

     [ContractInvariantMethod]

     void ObjectInvariant()

@@ -21,9 +22,10 @@ namespace Microsoft.Dafny {
       Contract.Invariant(wr!=null);

     }

 

-    public Printer(TextWriter wr) {

+    public Printer(TextWriter wr, DafnyOptions.PrintModes printMode = DafnyOptions.PrintModes.Everything) {

       Contract.Requires(wr != null);

       this.wr = wr;

+      this.printMode = printMode;

     }

 

     public static string ExprToString(Expression expr)

@@ -75,7 +77,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(iter != null);

       using (var wr = new System.IO.StringWriter()) {

         var pr = new Printer(wr);

-        pr.PrintIteratorClass(iter, 0);

+        pr.PrintIteratorClass(iter, 0, null);

         return ToStringWithoutNewline(wr);

       }

     }

@@ -127,18 +129,20 @@ namespace Microsoft.Dafny {
       if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

         wr.WriteLine();

         wr.WriteLine("/*");

-        PrintModuleDefinition(prog.BuiltIns.SystemModule, 0);

+        PrintModuleDefinition(prog.BuiltIns.SystemModule, 0, Path.GetFullPath(DafnyOptions.O.DafnyPrintResolvedFile));

         wr.WriteLine("*/");

       }

       wr.WriteLine();

-      PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0);

+      PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.Name));

+      wr.Flush();

     }

 

-    public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent) {

+    public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, string fileBeingPrinted) {

       Contract.Requires(decls!= null);

       int i = 0;

       foreach (TopLevelDecl d in decls) {

         Contract.Assert(d != null);

+        if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }

         if (d is OpaqueTypeDecl) {

           var at = (OpaqueTypeDecl)d;

           if (i++ != 0) { wr.WriteLine(); }

@@ -189,7 +193,7 @@ namespace Microsoft.Dafny {
             // also print the members that were created as part of the interpretation of the iterator

             Contract.Assert(iter.Members.Count != 0);  // filled in during resolution

             wr.WriteLine("/*---------- iterator members ----------");

-            PrintIteratorClass(iter, indent);

+            PrintIteratorClass(iter, indent, fileBeingPrinted);

             wr.WriteLine("---------- iterator members ----------*/");

           }

 

@@ -197,12 +201,12 @@ namespace Microsoft.Dafny {
           ClassDecl cl = (ClassDecl)d;

           if (!cl.IsDefaultClass) {

             if (i++ != 0) { wr.WriteLine(); }

-            PrintClass(cl, indent);

+            PrintClass(cl, indent, fileBeingPrinted);

           } else if (cl.Members.Count == 0) {

             // print nothing

           } else {

             if (i++ != 0) { wr.WriteLine(); }

-            PrintMembers(cl.Members, indent);

+            PrintMembers(cl.Members, indent, fileBeingPrinted);

           }

 

         } else if (d is ModuleDecl) {

@@ -210,7 +214,7 @@ namespace Microsoft.Dafny {
           Indent(indent);

           if (d is LiteralModuleDecl) {

             ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef;

-            PrintModuleDefinition(module, indent);

+            PrintModuleDefinition(module, indent, fileBeingPrinted);

           } else if (d is AliasModuleDecl) {

             wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened");

             wr.Write(" {0} ", ((AliasModuleDecl)d).Name);

@@ -227,7 +231,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void PrintModuleDefinition(ModuleDefinition module, int indent) {

+    void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) {

       Contract.Requires(module != null);

       Contract.Requires(0 <= indent);

       if (module.IsAbstract) {

@@ -243,7 +247,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine("{ }");

       } else {

         wr.WriteLine("{");

-        PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount);

+        PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);

         Indent(indent);

         wr.WriteLine("}");

       }

@@ -283,14 +287,14 @@ namespace Microsoft.Dafny {
       PrintDecreasesSpec(iter.Decreases, ind);

     }

 

-    private void PrintIteratorClass(IteratorDecl iter, int indent) {

+    private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) {

       PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);

       wr.WriteLine(" {");

-      PrintMembers(iter.Members, indent + IndentAmount);

+      PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted);

       Indent(indent); wr.WriteLine("}");

     }

 

-    public void PrintClass(ClassDecl c, int indent) {

+    public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) {

       Contract.Requires(c != null);

       Indent(indent);

       PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);

@@ -301,18 +305,19 @@ namespace Microsoft.Dafny {
         wr.WriteLine(" { }");

       } else {

         wr.WriteLine(" {");

-        PrintMembers(c.Members, indent + IndentAmount);

+        PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted);

         Indent(indent);

         wr.WriteLine("}");

       }

     }

 

-    public void PrintMembers(List<MemberDecl> members, int indent)

+    public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted)

     {

       Contract.Requires(members != null);

 

       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

       foreach (MemberDecl m in members) {

+        if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; }

         if (m is Method) {

           if (state != 0) { wr.WriteLine(); }

           PrintMethod((Method)m, indent, false);

@@ -437,6 +442,8 @@ namespace Microsoft.Dafny {
 

     public void PrintFunction(Function f, int indent, bool printSignatureOnly) {

       Contract.Requires(f != null);

+

+      if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; }

       var isPredicate = f is Predicate || f is PrefixPredicate;

       Indent(indent);

       string k = isPredicate ? "predicate" : f is CoPredicate ? "copredicate" : "function";

@@ -482,9 +489,31 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name)

+    {

+      if (printMode == DafnyOptions.PrintModes.NoGhost && IsGhost)

+          { return true; }

+      if (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)

+      {

+          bool verify = true;

+          if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify)

+          { return true; }

+          if (name.Contains("INTERNAL") || name.StartsWith("reveal_"))

+          { return true; }

+      }

+      return false;

+    }

+

+    private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted)

+    {

+        return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)

+               && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted);

+    }

+

     public void PrintMethod(Method method, int indent, bool printSignatureOnly) {

       Contract.Requires(method != null);

 

+      if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; }

       Indent(indent);

       string k = method is Constructor ? "constructor" : method is CoLemma ? "colemma" : method is Lemma ? "lemma" : "method";

       if (method.IsStatic) { k = "static " + k; }

@@ -568,6 +597,7 @@ namespace Microsoft.Dafny {
 

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

       Contract.Requires(decs != null);

+      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

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

         Indent(indent);

         wr.Write("decreases");

@@ -599,6 +629,7 @@ namespace Microsoft.Dafny {
     internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent, bool newLine = true) {

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

+      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

       foreach (MaybeFreeExpression e in ee)

       {

         Contract.Assert(e != null);

@@ -655,6 +686,8 @@ namespace Microsoft.Dafny {
     /// </summary>

     public void PrintStatement(Statement stmt, int indent) {

       Contract.Requires(stmt != null);

+

+      if (stmt.IsGhost && printMode == DafnyOptions.PrintModes.NoGhost) { return; }

       for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {

         if (label.Data.Name != null) {

           wr.WriteLine("label {0}:", label.Data.Name);

@@ -663,6 +696,7 @@ namespace Microsoft.Dafny {
       }

 

       if (stmt is PredicateStmt) {

+        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

         Expression expr = ((PredicateStmt)stmt).Expr;

         wr.Write(stmt is AssertStmt ? "assert" : "assume");

         if (stmt.Attributes != null) {

@@ -792,6 +826,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is CalcStmt) {

         CalcStmt s = (CalcStmt)stmt;

+        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }   // Calcs don't get a "ghost" attribute, but they are.

         wr.Write("calc ");

         if (!s.Op.Equals(CalcStmt.DefaultOp)) {

           PrintCalcOp(s.Op);

@@ -877,6 +912,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

+        if (s.Locals.Exists(v => v.IsGhost) && printMode == DafnyOptions.PrintModes.NoGhost) { return; }

         if (s.Locals.Exists(v => v.IsGhost)) {

           wr.Write("ghost ");

         }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 99d4938e..8046a7ac 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -147,7 +147,8 @@ namespace Microsoft.Dafny
         if (err != null) {

           exitValue = ExitValue.DAFNY_ERROR;

           printer.ErrorWriteLine(Console.Out, err);

-        } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {

+        } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck

+            && DafnyOptions.O.DafnyVerify) {

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

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

           if (CommandLineOptions.Clo.PrintFile != null)