Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLineOptions to separate the options that belong to these 3 tools.

4 files changed, 153 insertions, 20 deletions

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:<file>

+                choose Dafny prelude file

+  /dprint:<file>

+                print Dafny program after parsing it

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

+  /compile:<n>  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:<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 ghost methods

+  /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

+");

+    }

+  }

+}

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 @@
     <Compile Include="Compiler.cs" />

     <Compile Include="DafnyAst.cs" />

     <Compile Include="DafnyMain.cs" />

+    <Compile Include="DafnyOptions.cs" />

     <Compile Include="Printer.cs" />

     <Compile Include="Resolver.cs" />

     <Compile Include="SccGraph.cs" />

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<Expression>();

           m.Ens.ForEach(mfe => posts.Add(mfe.E));

           var allIns = new List<Formal>();

@@ -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<List<VarType>>() != null);

 

-      if (CommandLineOptions.Clo.DafnyInduction == 0) {

+      if (DafnyOptions.O.Induction == 0) {

         return new List<VarType>();  // don't apply induction

       }

 

@@ -6774,7 +6774,7 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (CommandLineOptions.Clo.DafnyInduction < 2) {

+      if (DafnyOptions.O.Induction < 2) {

         return new List<VarType>();  // don't apply induction

       }

 

@@ -6809,7 +6809,7 @@ namespace Microsoft.Dafny {
     /// Parameter 'n' is allowed to be a ThisSurrogate.

     /// </summary>

     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