From 73b9d30f3b18425e52ef80453977d8608a1db09b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 15 Nov 2011 18:48:02 -0800 Subject: Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools. --- Source/Dafny/DafnyMain.cs | 4 +- Source/Dafny/DafnyOptions.cs | 132 ++++++++++++++++++++++++++++++++++++++ Source/Dafny/DafnyPipeline.csproj | 1 + Source/Dafny/Translator.cs | 36 +++++------ 4 files changed, 153 insertions(+), 20 deletions(-) create mode 100644 Source/Dafny/DafnyOptions.cs (limited to 'Source/Dafny') diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 3f0b6e97..1d075415 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -49,8 +49,8 @@ namespace Microsoft.Dafny { program = new Program(programName, modules, builtIns); - if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) { - string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile; + if (DafnyOptions.O.DafnyPrintFile != null) { + string filename = DafnyOptions.O.DafnyPrintFile; if (filename == "-") { Printer pr = new Printer(System.Console.Out); pr.PrintProgram(program); diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs new file mode 100644 index 00000000..8c604b8a --- /dev/null +++ b/Source/Dafny/DafnyOptions.cs @@ -0,0 +1,132 @@ +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 + { + public DafnyOptions() + : base("Dafny", "Dafny program verifier") { + } + + 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 DisallowSoundnessCheating = false; + public int Induction = 3; + public int InductionHeuristic = 6; + public string DafnyPrelude = null; + public string DafnyPrintFile = null; + public bool Compile = true; + public bool ForceCompile = false; + + protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { + Contract.Requires(name != null); + Contract.Requires(ps != null); + 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 "compile": { + int compile = 0; + if (ps.GetNumericArgument(ref compile, 3)) { + Compile = compile == 1 || compile == 2; + ForceCompile = compile == 2; + } + 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; + + default: + break; + } + // not a Dafny-specific option, so defer to superclass + return base.ParseOption(name, ps); + } + + protected 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 + } + + 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) + /compile: 0 - do not compile Dafny program + 1 (default) - upon successful verification of the Dafny + program, compile Dafny program to C# program out.cs + 2 - always attempt to compile Dafny program to C# program + out.cs, regardless of verification outcome + /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 ghost methods + /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 +"); + } + } +} diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 40a8cacc..dfa9e503 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -154,6 +154,7 @@ + diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index f3373736..88f95f30 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -259,7 +259,7 @@ namespace Microsoft.Dafny { } static Bpl.Program ReadPrelude() { - string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude; + string preludePath = DafnyOptions.O.DafnyPrelude; if (preludePath == null) { //using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource @@ -1054,7 +1054,7 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts; if (!wellformednessProc) { - if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) { + if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) { var posts = new List(); m.Ens.ForEach(mfe => posts.Add(mfe.E)); var allIns = new List(); @@ -1805,7 +1805,7 @@ namespace Microsoft.Dafny { Bpl.Expr gTotal = IsTotal(e.Guard, etran); Bpl.Expr g = etran.TrExpr(e.Guard); Bpl.Expr bTotal = IsTotal(e.Body, etran); - if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) { return BplAnd(gTotal, BplAnd(g, bTotal)); } else { return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal)); @@ -1958,7 +1958,7 @@ namespace Microsoft.Dafny { var e = (PredicateExpr)expr; Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran); Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran); - if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) { return BplAnd(gCanCall, bCanCall); } else { Bpl.Expr g = etran.TrExpr(e.Guard); @@ -2369,7 +2369,7 @@ namespace Microsoft.Dafny { } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; CheckWellformed(e.Guard, options, locals, builder, etran); - if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) { bool splitHappened; var ss = TrSplitExpr(e.Guard, etran, out splitHappened); if (!splitHappened) { @@ -2843,7 +2843,7 @@ namespace Microsoft.Dafny { if (!wellformednessProc) { string comment = "user-defined preconditions"; foreach (MaybeFreeExpression p in m.Req) { - if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment)); } else { bool splitHappened; // we actually don't care @@ -2856,7 +2856,7 @@ namespace Microsoft.Dafny { } comment = "user-defined postconditions"; if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) { - if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment)); } else { bool splitHappened; // we actually don't care @@ -3330,7 +3330,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null); Contract.Requires(currentMethod != null && predef != null); if (stmt is PredicateStmt) { - if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) { AddComment(builder, stmt, "assert statement"); PredicateStmt s = (PredicateStmt)stmt; TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false); @@ -3958,7 +3958,7 @@ namespace Microsoft.Dafny { invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E))); invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran)))); - if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) { + if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E)))); } else { bool splitHappened; @@ -6578,7 +6578,7 @@ namespace Microsoft.Dafny { } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) { var e = (QuantifierExpr)expr; var inductionVariables = ApplyInduction(e); - if (2 <= CommandLineOptions.Clo.DafnyInduction && inductionVariables.Count != 0) { + if (2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) { // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation // (forall n :: (forall k :: k < n ==> P(k)) ==> P(n)) // For an existential (exists n :: P(n)), it is @@ -6689,7 +6689,7 @@ namespace Microsoft.Dafny { Contract.Requires(tracePrinter != null); Contract.Ensures(Contract.Result>() != null); - if (CommandLineOptions.Clo.DafnyInduction == 0) { + if (DafnyOptions.O.Induction == 0) { return new List(); // don't apply induction } @@ -6774,7 +6774,7 @@ namespace Microsoft.Dafny { } } - if (CommandLineOptions.Clo.DafnyInduction < 2) { + if (DafnyOptions.O.Induction < 2) { return new List(); // don't apply induction } @@ -6809,7 +6809,7 @@ namespace Microsoft.Dafny { /// Parameter 'n' is allowed to be a ThisSurrogate. /// bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) { - switch (CommandLineOptions.Clo.DafnyInductionHeuristic) { + switch (DafnyOptions.O.InductionHeuristic) { case 0: return true; case 1: return ContainsFreeVariable(expr, false, n); default: return VarOccursInArgumentToRecursiveFunction(expr, n, false); @@ -6827,7 +6827,7 @@ namespace Microsoft.Dafny { Contract.Requires(n != null); // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status. - var subExprIsProminent = CommandLineOptions.Clo.DafnyInductionHeuristic == 2 || CommandLineOptions.Clo.DafnyInductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false; + var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false; if (expr is ThisExpr) { return exprIsProminent && n is ThisSurrogate; @@ -6836,13 +6836,13 @@ namespace Microsoft.Dafny { return exprIsProminent && e.Var == n; } else if (expr is SeqSelectExpr) { var e = (SeqSelectExpr)expr; - var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent; + var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded) (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto } else if (expr is MultiSelectExpr) { var e = (MultiSelectExpr)expr; - var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent; + var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) || e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); } else if (expr is FunctionCallExpr) { @@ -6853,7 +6853,7 @@ namespace Microsoft.Dafny { bool inferredDecreases; // we don't actually care var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases); bool variantArgument; - if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) { + if (DafnyOptions.O.InductionHeuristic < 6) { variantArgument = rec; } else { // The receiver is considered to be "variant" if the function is recursive and the receiver participates @@ -6868,7 +6868,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < e.Function.Formals.Count; i++) { var f = e.Function.Formals[i]; var exp = e.Args[i]; - if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) { + if (DafnyOptions.O.InductionHeuristic < 6) { variantArgument = rec; } else { // The argument position is considered to be "variant" if the function is recursive and the argument participates -- cgit v1.2.3