diff options
author | qunyanm <unknown> | 2016-02-11 14:29:37 -0800 |
---|---|---|
committer | qunyanm <unknown> | 2016-02-11 14:29:37 -0800 |
commit | 3edef4354012d635ac5d44b8a33078af7211d0d3 (patch) | |
tree | 5b6dd0607a72a556b08928fe640a84f7b6915ce2 /Source | |
parent | 1007154ab8ee7774588fd1e4cfcf5ae1ae165ea0 (diff) |
Add /view:<view1, view2> option to filter module exports to be printed.
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/DafnyMain.cs | 8 | ||||
-rw-r--r-- | Source/Dafny/DafnyOptions.cs | 795 | ||||
-rw-r--r-- | Source/Dafny/Printer.cs | 57 |
3 files changed, 457 insertions, 403 deletions
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 251d8656..fd2e00fb 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -12,7 +12,7 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny {
public class Main {
- private static void MaybePrintProgram(Program program, string filename)
+ private static void MaybePrintProgram(Program program, string filename, bool afterResolver)
{
if (filename != null) {
TextWriter tw;
@@ -22,7 +22,7 @@ namespace Microsoft.Dafny { tw = new System.IO.StreamWriter(filename);
}
Printer pr = new Printer(tw, DafnyOptions.O.PrintMode);
- pr.PrintProgram(program);
+ pr.PrintProgram(program, afterResolver);
}
}
@@ -62,13 +62,13 @@ namespace Microsoft.Dafny { program = new Program(programName, module, builtIns, reporter);
- MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile);
+ MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile, false);
if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
Dafny.Resolver r = new Dafny.Resolver(program);
r.ResolveProgram(program);
- MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile);
+ MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile, true);
if (reporter.Count(ErrorLevel.Error) != 0) {
return string.Format("{0} resolution/type errors detected in {1}", reporter.Count(ErrorLevel.Error), program.Name);
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b61ba555..f3b38a84 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1,222 +1,228 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using Bpl = Microsoft.Boogie; - -namespace Microsoft.Dafny -{ - public class DafnyOptions : Bpl.CommandLineOptions - { - private ErrorReporter errorReporter; - - public DafnyOptions(ErrorReporter errorReporter = null) - : base("Dafny", "Dafny program verifier") { - this.errorReporter = errorReporter; - SetZ3ExecutableName(); - } - - public override string VersionNumber { - get { - return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion -#if ENABLE_IRONDAFNY - + "[IronDafny]" -#endif - ; - } - } - public override string VersionSuffix { - get { - return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft."; - } - } - - private static DafnyOptions clo; - public static DafnyOptions O { - get { return clo; } - } - - public static void Install(DafnyOptions options) { - Contract.Requires(options != null); - clo = options; - Bpl.CommandLineOptions.Install(options); - } - - public bool UnicodeOutput = false; - public bool DisallowSoundnessCheating = false; - public bool Dafnycc = false; - public int Induction = 3; - public int InductionHeuristic = 6; - public string DafnyPrelude = null; - public string DafnyPrintFile = null; - public enum PrintModes { Everything, NoIncludes, NoGhost }; - public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything - public bool DafnyVerify = true; - public string DafnyPrintResolvedFile = null; - public bool Compile = true; - public bool ForceCompile = false; - public bool RunAfterCompile = false; - public bool SpillTargetCode = false; - public bool DisallowIncludes = false; - public bool DisableNLarith = false; - public string AutoReqPrintFile = null; - public bool ignoreAutoReq = false; - public bool AllowGlobals = false; - public bool CountVerificationErrors = true; - public bool Optimize = false; +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny
+{
+ public class DafnyOptions : Bpl.CommandLineOptions
+ {
+ private ErrorReporter errorReporter;
+
+ public DafnyOptions(ErrorReporter errorReporter = null)
+ : base("Dafny", "Dafny program verifier") {
+ this.errorReporter = errorReporter;
+ SetZ3ExecutableName();
+ }
+
+ public override string VersionNumber {
+ get {
+ return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion
+#if ENABLE_IRONDAFNY
+ + "[IronDafny]"
+#endif
+ ;
+ }
+ }
+ public override string VersionSuffix {
+ get {
+ return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft.";
+ }
+ }
+
+ private static DafnyOptions clo;
+ public static DafnyOptions O {
+ get { return clo; }
+ }
+
+ public static void Install(DafnyOptions options) {
+ Contract.Requires(options != null);
+ clo = options;
+ Bpl.CommandLineOptions.Install(options);
+ }
+
+ public bool UnicodeOutput = false;
+ public bool DisallowSoundnessCheating = false;
+ public bool Dafnycc = false;
+ public int Induction = 3;
+ public int InductionHeuristic = 6;
+ public string DafnyPrelude = null;
+ public string DafnyPrintFile = null;
+ public enum PrintModes { Everything, NoIncludes, NoGhost };
+ public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
+ public bool DafnyVerify = true;
+ public string DafnyPrintResolvedFile = null;
+ public List<string> DafnyPrintExportedViews = new List<string>();
+ public bool Compile = true;
+ public bool ForceCompile = false;
+ public bool RunAfterCompile = false;
+ public bool SpillTargetCode = false;
+ public bool DisallowIncludes = false;
+ public bool DisableNLarith = false;
+ public string AutoReqPrintFile = null;
+ public bool ignoreAutoReq = false;
+ public bool AllowGlobals = false;
+ public bool CountVerificationErrors = true;
+ public bool Optimize = false;
public bool AutoTriggers = false;
public bool RewriteFocalPredicates = true;
- public bool PrintTooltips = false; - public bool PrintStats = false; - public bool PrintFunctionCallGraph = false; + public bool PrintTooltips = false;
+ public bool PrintStats = false;
+ public bool PrintFunctionCallGraph = false;
public bool WarnShadowing = false;
- public bool IronDafny = -#if ENABLE_IRONDAFNY - true -#else - false -#endif - ; - - protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { - var args = ps.args; // convenient synonym - - switch (name) { - case "dprelude": - if (ps.ConfirmArgumentCount(1)) { - DafnyPrelude = args[ps.i]; - } - return true; - - case "dprint": - if (ps.ConfirmArgumentCount(1)) { - DafnyPrintFile = args[ps.i]; - } - 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]; - } - return true; - - case "compile": { - int compile = 0; - if (ps.GetNumericArgument(ref compile, 4)) { - // convert option to two booleans - Compile = compile != 0; - ForceCompile = compile == 2; - RunAfterCompile = compile == 3; - } - 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)) { - SpillTargetCode = spill != 0; // convert to a boolean - } - return true; - } - - case "dafnycc": - Dafnycc = true; - Induction = 0; - Compile = false; - UseAbstractInterpretation = false; // /noinfer - return true; - - case "noCheating": { - int cheat = 0; // 0 is default, allows cheating - if (ps.GetNumericArgument(ref cheat, 2)) { - DisallowSoundnessCheating = cheat == 1; - } - return true; - } - - case "induction": - ps.GetNumericArgument(ref Induction, 4); - return true; - - case "inductionHeuristic": - ps.GetNumericArgument(ref InductionHeuristic, 7); - return true; - - case "noIncludes": - DisallowIncludes = true; - return true; - - case "noNLarith": - DisableNLarith = true; - this.AddZ3Option("smt.arith.nl=false"); - return true; - - case "autoReqPrint": - if (ps.ConfirmArgumentCount(1)) { - AutoReqPrintFile = args[ps.i]; - } - return true; - - case "noAutoReq": - ignoreAutoReq = true; - return true; - - case "allowGlobals": - AllowGlobals = true; - return true; - - case "stats": - PrintStats = true; - return true; - - case "funcCallGraph": - PrintFunctionCallGraph = true; - return true; - - case "warnShadowing": - WarnShadowing = true; - return true; - - case "countVerificationErrors": { - int countErrors = 1; // defaults to reporting verification errors - if (ps.GetNumericArgument(ref countErrors, 2)) { - CountVerificationErrors = countErrors == 1; - } - return true; - } - - case "printTooltips": - PrintTooltips = true; + public bool IronDafny =
+#if ENABLE_IRONDAFNY
+ true
+#else
+ false
+#endif
+ ;
+
+ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
+ var args = ps.args; // convenient synonym
+
+ switch (name) {
+ case "dprelude":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrelude = args[ps.i];
+ }
+ return true;
+
+ case "dprint":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrintFile = args[ps.i];
+ }
+ 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];
+ }
+ return true;
+ case "view":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrintExportedViews = args[ps.i].Split(',').ToList();
+ }
+ return true;
+
+ case "compile": {
+ int compile = 0;
+ if (ps.GetNumericArgument(ref compile, 4)) {
+ // convert option to two booleans
+ Compile = compile != 0;
+ ForceCompile = compile == 2;
+ RunAfterCompile = compile == 3;
+ }
+ 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)) {
+ SpillTargetCode = spill != 0; // convert to a boolean
+ }
+ return true;
+ }
+
+ case "dafnycc":
+ Dafnycc = true;
+ Induction = 0;
+ Compile = false;
+ UseAbstractInterpretation = false; // /noinfer
+ return true;
+
+ case "noCheating": {
+ int cheat = 0; // 0 is default, allows cheating
+ if (ps.GetNumericArgument(ref cheat, 2)) {
+ DisallowSoundnessCheating = cheat == 1;
+ }
+ return true;
+ }
+
+ case "induction":
+ ps.GetNumericArgument(ref Induction, 4);
+ return true;
+
+ case "inductionHeuristic":
+ ps.GetNumericArgument(ref InductionHeuristic, 7);
+ return true;
+
+ case "noIncludes":
+ DisallowIncludes = true;
+ return true;
+
+ case "noNLarith":
+ DisableNLarith = true;
+ this.AddZ3Option("smt.arith.nl=false");
+ return true;
+
+ case "autoReqPrint":
+ if (ps.ConfirmArgumentCount(1)) {
+ AutoReqPrintFile = args[ps.i];
+ }
+ return true;
+
+ case "noAutoReq":
+ ignoreAutoReq = true;
+ return true;
+
+ case "allowGlobals":
+ AllowGlobals = true;
+ return true;
+
+ case "stats":
+ PrintStats = true;
+ return true;
+
+ case "funcCallGraph":
+ PrintFunctionCallGraph = true;
+ return true;
+
+ case "warnShadowing":
+ WarnShadowing = true;
+ return true;
+
+ case "countVerificationErrors": {
+ int countErrors = 1; // defaults to reporting verification errors
+ if (ps.GetNumericArgument(ref countErrors, 2)) {
+ CountVerificationErrors = countErrors == 1;
+ }
+ return true;
+ }
+
+ case "printTooltips":
+ PrintTooltips = true;
return true;
case "autoTriggers": {
@@ -225,182 +231,187 @@ namespace Microsoft.Dafny AutoTriggers = autoTriggers == 1;
}
return true;
- } - + }
+
case "rewriteFocalPredicates": {
int rewriteFocalPredicates = 0;
if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) {
- RewriteFocalPredicates = rewriteFocalPredicates == 1; - } - return true; - } - - case "optimize": { - Optimize = true; - return true; - } - - case "noIronDafny": { - IronDafny = false; - return true; - } - - case "ironDafny": { - IronDafny = true; - return true; - } - - default: - break; - } - // not a Dafny-specific option, so defer to superclass - return base.ParseOption(name, ps); - } - - public override void ApplyDefaultOptions() { - base.ApplyDefaultOptions(); - - // expand macros in filenames, now that LogPrefix is fully determined - ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp); - ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp); - } - - public override void AttributeUsage() { - // TODO: provide attribute help here - } - - - /// <summary> - /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. - /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. - /// For developers though (and people getting this from source), it's convenient to be able to run right away, - /// so we vendor a Windows version. - /// </summary> - private void SetZ3ExecutableName() { - var platform = (int)System.Environment.OSVersion.Platform; - - // http://www.mono-project.com/docs/faq/technical/ - var isUnix = platform == 4 || platform == 128; - - var z3binName = isUnix ? "z3" : "z3.exe"; - var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); - var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); - var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); - - if (!System.IO.File.Exists(z3BinPath) && !isUnix) { - // This is most likely a Windows user running from source without downloading z3 - // separately; this is ok, since we vendor z3.exe. - z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); - } - - if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { - var tok = new Bpl.Token(1, 1) { filename = "*** " }; - errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", - z3binName, z3BinDir, System.Environment.NewLine); - } else { - Z3ExecutablePath = z3BinPath; - } - } - - public override void Usage() { - Console.WriteLine(@" ---- Dafny options --------------------------------------------------------- - - Multiple .dfy files supplied on the command line are concatenated into one - Dafny program. - - /dprelude:<file> - choose Dafny prelude file - /dprint:<file> - print Dafny program after parsing it - (use - as <file> to print to console) - /printMode:<Everything|NoIncludes|NoGhost> - Everything is the default. - 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 - Program.exe (if the program has a Main method) or - Program.dll (othewise), where Program.dfy is the name - of the last .dfy file on the command line - 2 - always attempt to compile Dafny program to C# program - out.cs, regardless of verification outcome - 3 - if there is a Main method and there are no verification - errors, compiles program in memory (i.e., does not write - an output file) and runs it - /spillTargetCode:<n> - 0 (default) - don't write the compiled Dafny program (but - still compile it, if /compile indicates to do so) - 1 - write the compiled Dafny program as a .cs file - /dafnycc Disable features not supported by DafnyCC - /noCheating:<n> - 0 (default) - allow assume statements and free invariants - 1 - treat all assumptions as asserts, and drop free. - /induction:<n> - 0 - never do induction, not even when attributes request it - 1 - only apply induction when attributes request it - 2 - apply induction as requested (by attributes) and also - for heuristically chosen quantifiers - 3 (default) - apply induction as requested, and for - heuristically chosen quantifiers and lemmas - /inductionHeuristic:<n> - 0 - least discriminating induction heuristic (that is, lean - toward applying induction more often) - 1,2,3,4,5 - levels in between, ordered as follows as far as - how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6 - 6 (default) - most discriminating - /noIncludes Ignore include directives - /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%). - 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 - /allowGlobals Allow the implicit class '_default' to contain fields, instance functions, - and instance methods. These class members are declared at the module scope, - outside of explicit classes. This command-line option is provided to simplify - a transition from the behavior in the language prior to version 1.9.3, from - which point onward all functions and methods declared at the module scope are - implicitly static and fields declarations are not allowed at the module scope. - /countVerificationErrors:<n> - 0 - If preprocessing succeeds, set exit code to 0 regardless of the number - of verification errors. - 1 (default) - If preprocessing succeeds, set exit code to the number of - verification errors. - /autoTriggers:<n> - 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. - 1 - Add a {:trigger} to each user-level quantifier. Existing - annotations are preserved. - /rewriteFocalPredicates:<n> - 0 - Don't rewrite predicates in the body of prefix lemmas. - 1 (default) - In the body of prefix lemmas, rewrite any use of a focal predicate - P to P#[_k-1]. - /optimize Produce optimized C# code, meaning: - - selects optimized C# prelude by passing - /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires - System.Collections.Immutable.dll in the source directory to successfully - compile). - - passes /optimize flag to csc.exe. - /stats Print interesting statistics about the Dafny files supplied. - /funcCallGraph Print out the function call graph. Format is: func,mod=callee* - /warnShadowing Emits a warning if the name of a declared variable caused another variable - to be shadowed - /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of - these features may cause your code to become incompatible with future - releases of Dafny. - /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. - /printTooltips - Dump additional positional information (displayed as mouse-over tooltips by - the VS plugin) to stdout as 'Info' messages. -"); - base.Usage(); // also print the Boogie options - } - } -} + RewriteFocalPredicates = rewriteFocalPredicates == 1;
+ }
+ return true;
+ }
+
+ case "optimize": {
+ Optimize = true;
+ return true;
+ }
+
+ case "noIronDafny": {
+ IronDafny = false;
+ return true;
+ }
+
+ case "ironDafny": {
+ IronDafny = true;
+ return true;
+ }
+
+ default:
+ break;
+ }
+ // not a Dafny-specific option, so defer to superclass
+ return base.ParseOption(name, ps);
+ }
+
+ public override void ApplyDefaultOptions() {
+ base.ApplyDefaultOptions();
+
+ // expand macros in filenames, now that LogPrefix is fully determined
+ ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);
+ ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);
+ }
+
+ public override void AttributeUsage() {
+ // TODO: provide attribute help here
+ }
+
+
+ /// <summary>
+ /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency.
+ /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.
+ /// For developers though (and people getting this from source), it's convenient to be able to run right away,
+ /// so we vendor a Windows version.
+ /// </summary>
+ private void SetZ3ExecutableName() {
+ var platform = (int)System.Environment.OSVersion.Platform;
+
+ // http://www.mono-project.com/docs/faq/technical/
+ var isUnix = platform == 4 || platform == 128;
+
+ var z3binName = isUnix ? "z3" : "z3.exe";
+ var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+ var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");
+ var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);
+
+ if (!System.IO.File.Exists(z3BinPath) && !isUnix) {
+ // This is most likely a Windows user running from source without downloading z3
+ // separately; this is ok, since we vendor z3.exe.
+ z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);
+ }
+
+ if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {
+ var tok = new Bpl.Token(1, 1) { filename = "*** " };
+ errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.",
+ z3binName, z3BinDir, System.Environment.NewLine);
+ } else {
+ Z3ExecutablePath = z3BinPath;
+ }
+ }
+
+ public override void Usage() {
+ Console.WriteLine(@" ---- Dafny options ---------------------------------------------------------
+
+ Multiple .dfy files supplied on the command line are concatenated into one
+ Dafny program.
+
+ /dprelude:<file>
+ choose Dafny prelude file
+ /dprint:<file>
+ print Dafny program after parsing it
+ (use - as <file> to print to console)
+ /printMode:<Everything|NoIncludes|NoGhost>
+ Everything is the default.
+ 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)
+ /view:<view1, view2>
+ print the filtered views of a module after it is resolved (/rprint).
+ if print before the module is resolved (/dprint), then everthing in the module is printed
+ if no view is specified, then everything in the module is printed.
+
+ /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
+ Program.exe (if the program has a Main method) or
+ Program.dll (othewise), where Program.dfy is the name
+ of the last .dfy file on the command line
+ 2 - always attempt to compile Dafny program to C# program
+ out.cs, regardless of verification outcome
+ 3 - if there is a Main method and there are no verification
+ errors, compiles program in memory (i.e., does not write
+ an output file) and runs it
+ /spillTargetCode:<n>
+ 0 (default) - don't write the compiled Dafny program (but
+ still compile it, if /compile indicates to do so)
+ 1 - write the compiled Dafny program as a .cs file
+ /dafnycc Disable features not supported by DafnyCC
+ /noCheating:<n>
+ 0 (default) - allow assume statements and free invariants
+ 1 - treat all assumptions as asserts, and drop free.
+ /induction:<n>
+ 0 - never do induction, not even when attributes request it
+ 1 - only apply induction when attributes request it
+ 2 - apply induction as requested (by attributes) and also
+ for heuristically chosen quantifiers
+ 3 (default) - apply induction as requested, and for
+ heuristically chosen quantifiers and lemmas
+ /inductionHeuristic:<n>
+ 0 - least discriminating induction heuristic (that is, lean
+ toward applying induction more often)
+ 1,2,3,4,5 - levels in between, ordered as follows as far as
+ how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
+ 6 (default) - most discriminating
+ /noIncludes Ignore include directives
+ /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%).
+ 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
+ /allowGlobals Allow the implicit class '_default' to contain fields, instance functions,
+ and instance methods. These class members are declared at the module scope,
+ outside of explicit classes. This command-line option is provided to simplify
+ a transition from the behavior in the language prior to version 1.9.3, from
+ which point onward all functions and methods declared at the module scope are
+ implicitly static and fields declarations are not allowed at the module scope.
+ /countVerificationErrors:<n>
+ 0 - If preprocessing succeeds, set exit code to 0 regardless of the number
+ of verification errors.
+ 1 (default) - If preprocessing succeeds, set exit code to the number of
+ verification errors.
+ /autoTriggers:<n>
+ 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.
+ 1 - Add a {:trigger} to each user-level quantifier. Existing
+ annotations are preserved.
+ /rewriteFocalPredicates:<n>
+ 0 - Don't rewrite predicates in the body of prefix lemmas.
+ 1 (default) - In the body of prefix lemmas, rewrite any use of a focal predicate
+ P to P#[_k-1].
+ /optimize Produce optimized C# code, meaning:
+ - selects optimized C# prelude by passing
+ /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires
+ System.Collections.Immutable.dll in the source directory to successfully
+ compile).
+ - passes /optimize flag to csc.exe.
+ /stats Print interesting statistics about the Dafny files supplied.
+ /funcCallGraph Print out the function call graph. Format is: func,mod=callee*
+ /warnShadowing Emits a warning if the name of a declared variable caused another variable
+ to be shadowed
+ /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of
+ these features may cause your code to become incompatible with future
+ releases of Dafny.
+ /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default.
+ /printTooltips
+ Dump additional positional information (displayed as mouse-over tooltips by
+ the VS plugin) to stdout as 'Info' messages.
+");
+ base.Usage(); // also print the Boogie options
+ }
+ }
+}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 86c493f1..0ba6f439 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -14,7 +14,8 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { public class Printer { TextWriter wr; - DafnyOptions.PrintModes printMode; + DafnyOptions.PrintModes printMode;
+ bool afterResolver; [ContractInvariantMethod] void ObjectInvariant() @@ -129,8 +130,9 @@ namespace Microsoft.Dafny { return sb.ToString(0, len); } - public void PrintProgram(Program prog) { - Contract.Requires(prog != null); + public void PrintProgram(Program prog, bool afterResolver) { + Contract.Requires(prog != null);
+ this.afterResolver = afterResolver; if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version); wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); @@ -239,7 +241,7 @@ namespace Microsoft.Dafny { PrintMembers(cl.Members, indent, fileBeingPrinted); } - } else if (d is ModuleDecl) { + } else if (d is ModuleDecl) {
wr.WriteLine(); Indent(indent); if (d is LiteralModuleDecl) { @@ -252,13 +254,37 @@ namespace Microsoft.Dafny { } else if (d is ModuleFacadeDecl) { wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); - wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); + wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val));
+ } else if (d is ModuleExportDecl) {
+ ModuleExportDecl e = (ModuleExportDecl)d;
+ if (e.IsDefault) wr.Write("default ");
+ wr.Write("export {0}", e.Name);
+ if (e.Extends.Count > 0) wr.Write(" extends {0}", Util.Comma(e.Extends, id => id));
+ PrintModuleExportDecl(e, indent, fileBeingPrinted);
} } else { Contract.Assert(false); // unexpected TopLevelDecl } } + }
+
+ void PrintModuleExportDecl(ModuleExportDecl m, int indent, string fileBeingPrinted) {
+ ModuleSignature sig = m.Signature;
+ if (sig == null) {
+ wr.Write(" {");
+ // has been resolved yet, just print the strings
+ wr.Write("{0}", Util.Comma(m.Exports, id => id.Name));
+ wr.Write("}");
+ } else {
+ wr.WriteLine(" {");
+ // print the decls and members in the module
+ List<TopLevelDecl> decls = sig.TopLevels.Values.ToList();
+ List<MemberDecl> members = sig.StaticMembers.Values.ToList();
+ PrintTopLevelDecls(decls, indent + IndentAmount, fileBeingPrinted);
+ PrintMembers(members, indent + IndentAmount, fileBeingPrinted);
+ Indent(indent); wr.WriteLine("}");
+ }
} void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) { @@ -277,11 +303,28 @@ namespace Microsoft.Dafny { wr.WriteLine("{ }"); } else { wr.WriteLine("{"); - PrintCallGraph(module, indent + IndentAmount); - PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted); + PrintCallGraph(module, indent + IndentAmount);
+ PrintTopLevelDeclsOrExportedView(module, indent, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } + }
+
+ void PrintTopLevelDeclsOrExportedView(ModuleDefinition module, int indent, string fileBeingPrinted) {
+ bool printViewsOnly = false;
+ List<TopLevelDecl> decls = new List<TopLevelDecl>();
+ // only filter based on view name after resolver.
+ if (afterResolver) {
+ foreach (var nameOfView in DafnyOptions.O.DafnyPrintExportedViews) {
+ foreach (var decl in module.TopLevelDecls) {
+ if (decl.FullName.Equals(nameOfView)) {
+ printViewsOnly = true;
+ decls.Add(decl);
+ }
+ }
+ }
+ }
+ PrintTopLevelDecls(printViewsOnly ? decls : module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);
} void PrintIteratorSignature(IteratorDecl iter, int indent) { |