From 3edef4354012d635ac5d44b8a33078af7211d0d3 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 11 Feb 2016 14:29:37 -0800 Subject: Add /view: option to filter module exports to be printed. --- Source/Dafny/DafnyMain.cs | 8 +- Source/Dafny/DafnyOptions.cs | 795 ++++++++++++++++++++++--------------------- 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 DafnyPrintExportedViews = new List(); + 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 - } - - - /// - /// 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. - /// - 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: - choose Dafny prelude file - /dprint: - print Dafny program after parsing it - (use - as to print to console) - /printMode: - 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: - print Dafny program after resolving it - (use - as to print to console) - /dafnyVerify: - 0 - stop after typechecking - 1 - continue on to translation, verification, and compilation - /compile: 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: - 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: - 0 (default) - allow assume statements and free invariants - 1 - treat all assumptions as asserts, and drop free. - /induction: - 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: - 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: - 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: - 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: - 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: - 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 + } + + + /// + /// 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. + /// + 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: + choose Dafny prelude file + /dprint: + print Dafny program after parsing it + (use - as to print to console) + /printMode: + 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: + print Dafny program after resolving it + (use - as to print to console) + /view: + 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: + 0 - stop after typechecking + 1 - continue on to translation, verification, and compilation + /compile: 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: + 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: + 0 (default) - allow assume statements and free invariants + 1 - treat all assumptions as asserts, and drop free. + /induction: + 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: + 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: + 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: + 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: + 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: + 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 decls = sig.TopLevels.Values.ToList(); + List 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 decls = new List(); + // 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) { -- cgit v1.2.3