From 4cc2d6cce8a03edc1e9230e75fbf7c186b70add8 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 3 Aug 2023 16:57:08 -0700
Subject: [PATCH 1/3] Deprecate support for old CLI

---
 Source/DafnyCore/DafnyOptions.cs              |  6 +-
 Source/DafnyCore/TestGenerationOptions.cs     | 68 +------------------
 Source/DafnyTestGeneration/DeadCodeCommand.cs | 16 ++---
 .../GenerateTestsCommand.cs                   | 34 ++++++----
 .../ProgramModification.cs                    |  2 +-
 docs/DafnyRef/Options.txt                     | 20 +-----
 docs/dev/news/4384.fix                        |  1 +
 7 files changed, 31 insertions(+), 116 deletions(-)
 create mode 100644 docs/dev/news/4384.fix

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 8bcbf9476d3..6eb521625e7 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -792,8 +792,8 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
           return true;
       }
 
-      // Unless this is an option for test generation, defer to superclass
-      return TestGenOptions.ParseOption(name, ps) || base.ParseOption(name, ps);
+      // Defer to superclass
+      return base.ParseOption(name, ps);
     }
 
     private static string[] ParseInnerArguments(string argumentsString) {
@@ -1462,8 +1462,6 @@ focal predicate P to P#[_k-1].
     /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
     /proverOpt:O:model.completion=true.
 
----- Test generation options -----------------------------------------------
-{TestGenOptions.Help}
 ---- Compilation options ---------------------------------------------------
 
 /compile:<n>
diff --git a/Source/DafnyCore/TestGenerationOptions.cs b/Source/DafnyCore/TestGenerationOptions.cs
index 72110edbb33..02a40421821 100644
--- a/Source/DafnyCore/TestGenerationOptions.cs
+++ b/Source/DafnyCore/TestGenerationOptions.cs
@@ -5,76 +5,14 @@
 namespace Microsoft.Dafny {
 
   public class TestGenerationOptions {
-
-    public static readonly string TestInlineAttribute = "testInline";
-    public static readonly string TestEntryAttribute = "testEntry";
+    public const string TestInlineAttribute = "testInline";
+    public const string TestEntryAttribute = "testEntry";
     public bool WarnDeadCode = false;
     public enum Modes { None, Block, Path };
     public Modes Mode = Modes.None;
     public uint SeqLengthLimit = 0;
     [CanBeNull] public string PrintBpl = null;
-    public bool DisablePrune = false;
+    public bool ForcePrune = false;
     public const uint DefaultTimeLimit = 10;
-
-    public bool ParseOption(string name, Bpl.CommandLineParseState ps) {
-      var args = ps.args;
-
-      switch (name) {
-
-        case "warnDeadCode":
-          WarnDeadCode = true;
-          Mode = Modes.Block;
-          return true;
-
-        case "generateTestMode":
-          if (ps.ConfirmArgumentCount(1)) {
-            Mode = args[ps.i] switch {
-              "None" => Modes.None,
-              "Block" => Modes.Block,
-              "Path" => Modes.Path,
-              _ => throw new Exception("Invalid value for generateTestMode")
-            };
-          }
-          return true;
-
-        case "generateTestSeqLengthLimit":
-          var limit = 0;
-          if (ps.GetIntArgument(ref limit)) {
-            SeqLengthLimit = (uint)limit;
-          }
-          return true;
-
-        case "generateTestPrintBpl":
-          if (ps.ConfirmArgumentCount(1)) {
-            PrintBpl = args[ps.i];
-          }
-          return true;
-
-        case "generateTestNoPrune":
-          DisablePrune = true;
-          return true;
-      }
-
-      return false;
-    }
-
-    public string Help => @"
-/warnDeadCode
-    Use counterexample generation to warn about potential dead code.
-/generateTestMode:<None|Block|Path>
-    None (default) - Has no effect.
-    Block - Prints block-coverage tests for the given program.
-    Path - Prints path-coverage tests for the given program.
-    Using /definiteAssignment:3, /generateTestNoPrune, 
-    /generateTestSeqLengthLimit, and /loopUnroll is highly recommended
-    when generating tests.
-/generateTestSeqLengthLimit:<n>
-    Add an axiom that sets the length of all sequences to be no greater 
-    than <n>. 0 (default) indicates no limit.
-/generateTestPrintBpl:<fileName>
-    Print the Boogie code used during test generation.
-/generateTestNoPrune
-    Disable axiom pruning that Dafny uses to speed up verification.";
-
   }
 }
diff --git a/Source/DafnyTestGeneration/DeadCodeCommand.cs b/Source/DafnyTestGeneration/DeadCodeCommand.cs
index c985b469028..95764d0a2e5 100644
--- a/Source/DafnyTestGeneration/DeadCodeCommand.cs
+++ b/Source/DafnyTestGeneration/DeadCodeCommand.cs
@@ -6,16 +6,17 @@
 using System.CommandLine;
 using System.CommandLine.Invocation;
 using System.Linq;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 
 public class DeadCodeCommand : ICommandSpec {
   public IEnumerable<Option> Options =>
     new Option[] {
-      // IMPORTANT: Before adding new options, make sure they are
-      // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
       GenerateTestsCommand.LoopUnroll,
       GenerateTestsCommand.SequenceLengthLimit,
+      GenerateTestsCommand.ForcePrune,
+      GenerateTestsCommand.PrintBpl,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverOptionHelp,
@@ -32,16 +33,7 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
-    // IMPORTANT: Before adding new default options, make sure they are
-    // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
-    dafnyOptions.Compile = true;
-    dafnyOptions.RunAfterCompile = false;
-    dafnyOptions.ForceCompile = false;
-    dafnyOptions.ForbidNondeterminism = true;
-    dafnyOptions.DefiniteAssignmentLevel = 2;
-
-    dafnyOptions.TestGenOptions.Mode = TestGenerationOptions.Modes.Block;
+    GenerateTestsCommand.PostProcess(dafnyOptions, options, context, TestGenerationOptions.Modes.Block);
     dafnyOptions.TestGenOptions.WarnDeadCode = true;
-    dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, false);
   }
 }
diff --git a/Source/DafnyTestGeneration/GenerateTestsCommand.cs b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
index 8af2fed9e5b..fd20c745353 100644
--- a/Source/DafnyTestGeneration/GenerateTestsCommand.cs
+++ b/Source/DafnyTestGeneration/GenerateTestsCommand.cs
@@ -4,6 +4,8 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using DafnyCore;
+using Microsoft.Boogie;
+
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
 
@@ -23,7 +25,7 @@ public class GenerateTestsCommand : ICommandSpec {
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit,
       PrintBpl,
-      DisablePrune
+      ForcePrune
     }.Concat(ICommandSpec.ConsoleOutputOptions).
       Concat(ICommandSpec.ResolverOptions);
 
@@ -57,8 +59,15 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
-    // IMPORTANT: Before adding new default options, make sure they are
-    // appropriately copied over in the CopyForProcedure method above
+    var mode = context.ParseResult.GetValueForArgument(modeArgument) switch {
+      Mode.Path => TestGenerationOptions.Modes.Path,
+      Mode.Block => TestGenerationOptions.Modes.Block,
+      _ => throw new ArgumentOutOfRangeException()
+    };
+    PostProcess(dafnyOptions, options, context, mode);
+  }
+
+  internal static void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context, TestGenerationOptions.Modes mode) {
     dafnyOptions.CompilerName = "cs";
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
@@ -66,14 +75,9 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     dafnyOptions.DeprecationNoise = 0;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
+    dafnyOptions.TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates;
     dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, false);
-
-    var mode = context.ParseResult.GetValueForArgument(modeArgument);
-    dafnyOptions.TestGenOptions.Mode = mode switch {
-      Mode.Path => TestGenerationOptions.Modes.Path,
-      Mode.Block => TestGenerationOptions.Modes.Block,
-      _ => throw new ArgumentOutOfRangeException()
-    };
+    dafnyOptions.TestGenOptions.Mode = mode;
   }
 
   public static readonly Option<uint> SequenceLengthLimit = new("--length-limit",
@@ -86,8 +90,8 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     "Print the Boogie code used during test generation.") {
     ArgumentHelpName = "filename"
   };
-  public static readonly Option<bool> DisablePrune = new("--no-prune",
-    "Disable axiom pruning that Dafny uses to speed up verification.") {
+  public static readonly Option<bool> ForcePrune = new("--force-prune",
+    "Enable axiom pruning that Dafny uses to speed up verification. This may negatively affect the quality of tests.") {
   };
   static GenerateTestsCommand() {
     DafnyOptions.RegisterLegacyBinding(LoopUnroll, (options, value) => {
@@ -99,15 +103,15 @@ static GenerateTestsCommand() {
     DafnyOptions.RegisterLegacyBinding(PrintBpl, (options, value) => {
       options.TestGenOptions.PrintBpl = value;
     });
-    DafnyOptions.RegisterLegacyBinding(DisablePrune, (options, value) => {
-      options.TestGenOptions.DisablePrune = value;
+    DafnyOptions.RegisterLegacyBinding(ForcePrune, (options, value) => {
+      options.TestGenOptions.ForcePrune = value;
     });
 
     DooFile.RegisterNoChecksNeeded(
       LoopUnroll,
       SequenceLengthLimit,
       PrintBpl,
-      DisablePrune
+      ForcePrune
     );
   }
 }
diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
index 05fff8e5617..1d5376b5a55 100644
--- a/Source/DafnyTestGeneration/ProgramModification.cs
+++ b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -115,7 +115,7 @@ private static void SetupForCounterexamples(DafnyOptions options) {
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
-      options.Prune = !options.TestGenOptions.DisablePrune;
+      options.Prune = options.TestGenOptions.ForcePrune;
     }
 
     /// <summary>
diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 90f89026270..32505661371 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -325,25 +325,7 @@ Usage: dafny [ option ... ] [ filename ... ]
       as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
       /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
       /proverOpt:O:model.completion=true.
-  
-  ---- Test generation options -----------------------------------------------
-  
-  /warnDeadCode
-      Use counterexample generation to warn about potential dead code.
-  /generateTestMode:<None|Block|Path>
-      None (default) - Has no effect.
-      Block - Prints block-coverage tests for the given program.
-      Path - Prints path-coverage tests for the given program.
-      Using /definiteAssignment:3, /generateTestNoPrune, 
-      /generateTestSeqLengthLimit, and /loopUnroll is highly recommended
-      when generating tests.
-  /generateTestSeqLengthLimit:<n>
-      Add an axiom that sets the length of all sequences to be no greater 
-      than <n>. 0 (default) indicates no limit.
-  /generateTestPrintBpl:<fileName>
-      Print the Boogie code used during test generation.
-  /generateTestNoPrune
-      Disable axiom pruning that Dafny uses to speed up verification.
+
   ---- Compilation options ---------------------------------------------------
   
   /compileSuffix:<value>
diff --git a/docs/dev/news/4384.fix b/docs/dev/news/4384.fix
new file mode 100644
index 00000000000..6b581df269c
--- /dev/null
+++ b/docs/dev/news/4384.fix
@@ -0,0 +1 @@
+Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests
\ No newline at end of file

From c4a316d0827b9e6aa69600a9270f54a17b5ade30 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 3 Aug 2023 17:02:40 -0700
Subject: [PATCH 2/3] Move release notes to the right location

---
 docs/dev/news/{4384.fix => 4385.fix} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename docs/dev/news/{4384.fix => 4385.fix} (100%)

diff --git a/docs/dev/news/4384.fix b/docs/dev/news/4385.fix
similarity index 100%
rename from docs/dev/news/4384.fix
rename to docs/dev/news/4385.fix

From 3caad1f21ad6677f37623cfa19833660facdd566 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Fri, 4 Aug 2023 10:01:30 -0700
Subject: [PATCH 3/3] Rebuild DafnyRef

---
 docs/DafnyRef/Options.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 32505661371..027681972ac 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -325,7 +325,7 @@ Usage: dafny [ option ... ] [ filename ... ]
       as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
       /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
       /proverOpt:O:model.completion=true.
-
+  
   ---- Compilation options ---------------------------------------------------
   
   /compileSuffix:<value>