Semantic vs non-semantic options (dafny-lang#5397)

Fixes dafny-lang#4985

### Description

#### Main Change
Options come in several flavors. Some options do not affect the
correctness of the program, such as those that affect logging or
performance. Other options do affects the semantics. These may be
configurable per module, such as `function-syntax`, or they may be
'global', which means the value this has for a dependency affects what
value it should have for the dependent, such as `unicode-char` or
`allow-warnings`.

Previously, options were only marked as global or not, so it was not
possible to distinguish between non-semantic options and semantic
options that are configurable at the module level. This PR adds
registration to make that distinction, and uses that to determine which
module level options to track in doo files, which fixes bugs that would
occur when using non-default values for these options in combination
with doo files.

#### Minor changes
- Fix a bug that would prevent using Doo files, due to their read stream
being disposed before they were fully read.
- Add a hidden option `--hidden-no-verify` that allows building doo
files without verifying then, as if you had verified them. This is
useful for building and committing the standard library without
verifying it, which is safe because CI will still build it with
verification as well.

### How has this been tested?
- Added the test `semanticOptions.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -36,9 +36,7 @@ static Printer() {
         options.PrintMode = value;
       });
 
-      DooFile.RegisterNoChecksNeeded(new Option[] {
-        PrintMode
-      });
+      DooFile.RegisterNoChecksNeeded(PrintMode, false);
     }
 
     public static readonly Option<PrintModes> PrintMode = new("--print-mode", () => PrintModes.Everything, @"

Source/DafnyCore/AST/Members/Function.cs

@@ -315,7 +315,7 @@ static Function() {
     DafnyOptions.RegisterLegacyBinding(FunctionSyntaxOption, (options, value) => {
       options.FunctionSyntax = functionSyntaxOptionsMap[value];
     });
-    DooFile.RegisterNoChecksNeeded(FunctionSyntaxOption);
+    DooFile.RegisterNoChecksNeeded(FunctionSyntaxOption, true);
   }
 
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -11,7 +11,7 @@ public abstract class MethodOrFunction : MemberDecl {
     "Allow exporting callables with preconditions, and importing callables with postconditions");
 
   static MethodOrFunction() {
-    DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.CheckOptionLibraryImpliesLocal);
+    DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError);
   }
 
   public readonly List<TypeParameter> TypeArgs;

Source/DafnyCore/Auditor/Auditor.cs

@@ -66,11 +66,9 @@ static Auditor() {
                                  "md-ietf", "markdown-ietf",
                                  "txt");
 
-    DooFile.RegisterNoChecksNeeded(
-      ReportFileOption,
-      ReportFormatOption,
-      CompareReportOption
-    );
+    DooFile.RegisterNoChecksNeeded(ReportFileOption, false);
+    DooFile.RegisterNoChecksNeeded(ReportFormatOption, false);
+    DooFile.RegisterNoChecksNeeded(CompareReportOption, false);
   }
 
   /// <summary>

Source/DafnyCore/DooFile.cs

@@ -12,6 +12,8 @@
 using Microsoft.Dafny;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Tomlyn;
+using Tomlyn.Helpers;
+using Tomlyn.Model;
 
 namespace DafnyCore;
 
@@ -59,29 +61,32 @@ public static ManifestData Read(TextReader reader) {
     }
 
     public void Write(TextWriter writer) {
-      writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n"));
+      var content = Toml.FromModel(this, new TomlModelOptions() {
+        ConvertToToml = obj => {
+          if (obj is Enum) {
+            TomlFormatHelper.ToString(obj.ToString()!, TomlPropertyDisplayKind.Default);
+            return obj.ToString();
+          }
+
+          return obj;
+        }
+      }).Replace("\r\n", "\n");
+      writer.Write(content);
     }
   }
 
   public ManifestData Manifest { get; set; }
 
   public string ProgramText { get; set; }
 
-  // This must be independent from any user-provided options,
-  // and remain fixed over the lifetime of a single .doo file format version.
-  // We don't want to attempt to read the program text using --function-syntax:3 for example.
-  // If we change default option values in future Dafny major version bumps,
-  // this must be configured to stay the same.
-  private static DafnyOptions ProgramSerializationOptions => DafnyOptions.Default;
-
-  public static Task<DooFile> Read(string path) {
+  public static async Task<DooFile> Read(string path) {
     using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
-    return Read(archive);
+    return await Read(archive);
   }
 
-  public static Task<DooFile> Read(Stream stream) {
+  public static async Task<DooFile> Read(Stream stream) {
     using var archive = new ZipArchive(stream);
-    return Read(archive);
+    return await Read(archive);
   }
 
   private static async Task<DooFile> Read(ZipArchive archive) {
@@ -113,7 +118,7 @@ public DooFile(Program dafnyProgram) {
     var tw = new StringWriter {
       NewLine = "\n"
     };
-    var pr = new Printer(tw, ProgramSerializationOptions, PrintModes.Serialization);
+    var pr = new Printer(tw, dafnyProgram.Options, PrintModes.Serialization);
     // afterResolver is false because we don't yet have a way to safely skip resolution
     // when reading the program back into memory.
     // It's probably worth serializing a program in a more efficient way first
@@ -174,6 +179,7 @@ public static DafnyOptions CheckAndGetLibraryOptions(ErrorReporter reporter, str
       }
 
       result.Options.OptionArguments[option] = libraryValue;
+      result.ApplyBinding(option);
       var prefix = $"cannot load {options.GetPrintPath(libraryFile)}";
       success = success && check(reporter, origin, prefix, option, localValue, libraryValue);
     }
@@ -236,8 +242,10 @@ public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility
     }
   }
 
-  public static void RegisterNoChecksNeeded(params Option[] options) {
-    foreach (var option in options) {
+  public static void RegisterNoChecksNeeded(Option option, bool semantic) {
+    if (semantic) {
+      RegisterLibraryCheck(option, OptionCompatibility.NoOpOptionCheck);
+    } else {
       if (OptionChecks.ContainsKey(option)) {
         throw new ArgumentException($"Option already registered as needing a library check: {option.Name}");
       }

Source/DafnyCore/GeneratedFromDafny.cs

@@ -921,7 +921,7 @@ public static Dafny.ISequence<__T> SetToSeq<__T>(Dafny.ISet<__T> s) {
             goto after__ASSIGN_SUCH_THAT_0;
           }
         }
-        throw new System.Exception("assign-such-that search produced no value (line 7247)");
+        throw new System.Exception("assign-such-that search produced no value (line 7245)");
       after__ASSIGN_SUCH_THAT_0:;
         _113_left = Dafny.Set<__T>.Difference(_113_left, Dafny.Set<__T>.FromElements(_114_x));
         xs = Dafny.Sequence<__T>.Concat(xs, Dafny.Sequence<__T>.FromElements(_114_x));

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -44,9 +44,11 @@ public static class BoogieOptionBag {
     ArgumentHelpName = "count",
   };
 
-  public static readonly Option<bool> NoVerify = new("--no-verify",
-    "Skip verification") {
-    ArgumentHelpName = "count"
+  public static readonly Option<bool> NoVerify = new("--no-verify", "Skip verification");
+
+  public static readonly Option<bool> HiddenNoVerify = new("--hidden-no-verify",
+    "Allows building unverified libraries without recording that they were not verified.") {
+    IsHidden = true
   };
 
   public static readonly Option<uint> VerificationTimeLimit = new("--verification-time-limit",
@@ -105,7 +107,10 @@ static BoogieOptionBag() {
     });
     DafnyOptions.RegisterLegacyBinding(Cores,
       (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f);
-    DafnyOptions.RegisterLegacyBinding(NoVerify, (o, f) => o.Verify = !f);
+    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => {
+      var shouldVerify = !value && !options.Get(HiddenNoVerify);
+      options.Verify = shouldVerify;
+    });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 
     DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => {
@@ -141,21 +146,20 @@ static BoogieOptionBag() {
     DooFile.RegisterLibraryChecks(
       new Dictionary<Option, OptionCompatibility.OptionCheck> {
         { BoogieArguments, OptionCompatibility.CheckOptionMatches },
-        { NoVerify, OptionCompatibility.CheckOptionLibraryImpliesLocal },
+        { NoVerify, OptionCompatibility.OptionLibraryImpliesLocalError },
       }
     );
-    DooFile.RegisterNoChecksNeeded(
-      Cores,
-      VerificationTimeLimit,
-      VerificationErrorLimit,
-      IsolateAssertions,
-      SolverLog,
-      SolverOption,
-      SolverOptionHelp,
-      SolverPath,
-      SolverPlugin,
-      SolverResourceLimit
-    );
+    DooFile.RegisterNoChecksNeeded(HiddenNoVerify, false);
+    DooFile.RegisterNoChecksNeeded(Cores, false);
+    DooFile.RegisterNoChecksNeeded(VerificationTimeLimit, false);
+    DooFile.RegisterNoChecksNeeded(VerificationErrorLimit, false);
+    DooFile.RegisterNoChecksNeeded(IsolateAssertions, false);
+    DooFile.RegisterNoChecksNeeded(SolverLog, false);
+    DooFile.RegisterNoChecksNeeded(SolverOption, false);
+    DooFile.RegisterNoChecksNeeded(SolverOptionHelp, false);
+    DooFile.RegisterNoChecksNeeded(SolverPath, false);
+    DooFile.RegisterNoChecksNeeded(SolverPlugin, false);
+    DooFile.RegisterNoChecksNeeded(SolverResourceLimit, false);
   }
 
   private static IReadOnlyList<string> SplitArguments(string commandLine) {

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -52,10 +52,6 @@ public enum AssertionShowMode { None, Implicit, All }
   public static readonly Option<bool> StdIn = new("--stdin", () => false,
     @"Read standard input and treat it as an input .dfy file.");
 
-  public static readonly Option<bool> Check = new("--check", () => false, @"
-Instead of formatting files, verify that all files are already
-formatted through and return a non-zero exit code if it is not the case".TrimStart());
-
   public static readonly Option<bool> OptimizeErasableDatatypeWrapper = new("--optimize-erasable-datatype-wrapper", () => true, @"
 false - Include all non-ghost datatype constructors in the compiled code
 true - In the compiled target code, transform any non-extern
@@ -316,10 +312,6 @@ public enum SystemModuleMode {
     IsHidden = true
   };
 
-  public static readonly Option<bool> UseJavadocLikeDocstringRewriterOption = new("--javadoclike-docstring-plugin",
-    "Rewrite docstrings using a simple Javadoc-to-markdown converter"
-  );
-
   public enum TestAssumptionsMode {
     None,
     Externs
@@ -496,8 +488,6 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DafnyOptions.RegisterLegacyBinding(InternalIncludeRuntimeOptionForExecution, (options, value) => { options.IncludeRuntime = value; });
     DafnyOptions.RegisterLegacyBinding(SystemModule, (options, value) => { options.SystemModuleTranslationMode = value; });
     DafnyOptions.RegisterLegacyBinding(UseBaseFileName, (o, f) => o.UseBaseNameForFileName = f);
-    DafnyOptions.RegisterLegacyBinding(UseJavadocLikeDocstringRewriterOption,
-      (options, value) => { options.UseJavadocLikeDocstringRewriter = value; });
     DafnyOptions.RegisterLegacyBinding(WarnShadowing, (options, value) => { options.WarnShadowing = value; });
     DafnyOptions.RegisterLegacyBinding(WarnMissingConstructorParenthesis,
       (options, value) => { options.DisallowConstructorCaseWithoutParentheses = value; });
@@ -517,18 +507,10 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
 
     DafnyOptions.RegisterLegacyBinding(PluginOption, (options, value) => { options.AdditionalPluginArguments = value; });
 
-    DafnyOptions.RegisterLegacyBinding(Check, (options, value) => {
-      options.FormatCheck = value;
-    });
-
     DafnyOptions.RegisterLegacyBinding(StdIn, (options, value) => {
       options.UseStdin = value;
     });
 
-    DafnyOptions.RegisterLegacyBinding(FormatPrint, (options, value) => {
-      options.DafnyPrintFile = value ? "-" : null;
-    });
-
     DafnyOptions.RegisterLegacyBinding(Prelude, (options, value) => {
       options.DafnyPrelude = value?.FullName;
       options.ExpandFilename(options.DafnyPrelude, x => options.DafnyPrelude = x, options.LogPrefix,
@@ -578,72 +560,55 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       new Dictionary<Option, OptionCompatibility.OptionCheck>() {
         { UnicodeCharacters, OptionCompatibility.CheckOptionMatches },
         { EnforceDeterminism, OptionCompatibility.CheckOptionLocalImpliesLibrary },
-        { RelaxDefiniteAssignment, OptionCompatibility.CheckOptionLibraryImpliesLocal },
-        { AllowAxioms, OptionCompatibility.CheckOptionLibraryImpliesLocal },
-        { AllowWarnings, (reporter, origin, prefix, option, localValue, libraryValue) => {
-            if (OptionCompatibility.OptionValuesImplied(libraryValue, localValue)) {
-              return true;
-            }
-            string message = OptionCompatibility.LocalImpliesLibraryMessage(prefix, option, localValue, libraryValue);
-            reporter.Warning(MessageSource.Project, ResolutionErrors.ErrorId.none, origin, message);
-            return false;
-          }
-        }
+        { RelaxDefiniteAssignment, OptionCompatibility.OptionLibraryImpliesLocalError },
+        { AllowAxioms, OptionCompatibility.OptionLibraryImpliesLocalError },
+        { AllowWarnings, OptionCompatibility.OptionLibraryImpliesLocalWarning },
+        { AllowDeprecation, OptionCompatibility.OptionLibraryImpliesLocalWarning },
+        { WarnShadowing, OptionCompatibility.OptionLibraryImpliesLocalWarning },
+        { UseStandardLibraries, OptionCompatibility.OptionLibraryImpliesLocalError },
       }
     );
-    DooFile.RegisterNoChecksNeeded(
-      WarnAsErrors,
-      ProgressOption,
-      LogLocation,
-      LogLevelOption,
-      ManualTriggerOption,
-      ShowHints,
-      Check,
-      Libraries,
-      Output,
-      PluginOption,
-      Prelude,
-      Target,
-      Verbose,
-      AllowDeprecation,
-      FormatPrint,
-      JsonDiagnostics,
-      QuantifierSyntax,
-      SpillTranslation,
-      StdIn,
-      TestAssumptions,
-      WarnShadowing,
-      ManualLemmaInduction,
-      TypeInferenceDebug,
-      GeneralTraits,
-      GeneralNewtypes,
-      TypeSystemRefresh,
-      VerificationLogFormat,
-      VerifyIncludedFiles,
-      DisableNonLinearArithmetic,
-      NewTypeInferenceDebug,
-      UseBaseFileName,
-      WarnMissingConstructorParenthesis,
-      UseJavadocLikeDocstringRewriterOption,
-      IncludeRuntimeOption,
-      InternalIncludeRuntimeOptionForExecution,
-      WarnContradictoryAssumptions,
-      WarnRedundantAssumptions,
-      VerificationCoverageReport,
-      NoTimeStampForCoverageReport,
-      DefaultFunctionOpacity,
-      UseStandardLibraries,
-      OptimizeErasableDatatypeWrapper,
-      AddCompileSuffix,
-      SystemModule,
-      ExecutionCoverageReport,
-      ExtractCounterexample,
-      ShowProofObligationExpressions
-      );
+    DooFile.RegisterNoChecksNeeded(WarnAsErrors, false);
+    DooFile.RegisterNoChecksNeeded(ProgressOption, false);
+    DooFile.RegisterNoChecksNeeded(LogLocation, false);
+    DooFile.RegisterNoChecksNeeded(LogLevelOption, false);
+    DooFile.RegisterNoChecksNeeded(ManualTriggerOption, true);
+    DooFile.RegisterNoChecksNeeded(ShowHints, false);
+    DooFile.RegisterNoChecksNeeded(Libraries, false);
+    DooFile.RegisterNoChecksNeeded(Output, false);
+    DooFile.RegisterNoChecksNeeded(PluginOption, false);
+    DooFile.RegisterNoChecksNeeded(Prelude, false);
+    DooFile.RegisterNoChecksNeeded(Target, false);
+    DooFile.RegisterNoChecksNeeded(Verbose, false);
+    DooFile.RegisterNoChecksNeeded(JsonDiagnostics, false);
+    DooFile.RegisterNoChecksNeeded(QuantifierSyntax, true);
+    DooFile.RegisterNoChecksNeeded(SpillTranslation, false);
+    DooFile.RegisterNoChecksNeeded(StdIn, false);
+    DooFile.RegisterNoChecksNeeded(TestAssumptions, false);
+    DooFile.RegisterNoChecksNeeded(ManualLemmaInduction, true);
+    DooFile.RegisterNoChecksNeeded(TypeInferenceDebug, false);
+    DooFile.RegisterNoChecksNeeded(GeneralTraits, false);
+    DooFile.RegisterNoChecksNeeded(GeneralNewtypes, false);
+    DooFile.RegisterNoChecksNeeded(TypeSystemRefresh, false);
+    DooFile.RegisterNoChecksNeeded(VerificationLogFormat, false);
+    DooFile.RegisterNoChecksNeeded(VerifyIncludedFiles, false);
+    DooFile.RegisterNoChecksNeeded(DisableNonLinearArithmetic, true);
+    DooFile.RegisterNoChecksNeeded(NewTypeInferenceDebug, false);
+    DooFile.RegisterNoChecksNeeded(UseBaseFileName, false);
+    DooFile.RegisterNoChecksNeeded(WarnMissingConstructorParenthesis, true);
+    DooFile.RegisterNoChecksNeeded(IncludeRuntimeOption, false);
+    DooFile.RegisterNoChecksNeeded(InternalIncludeRuntimeOptionForExecution, false);
+    DooFile.RegisterNoChecksNeeded(WarnContradictoryAssumptions, true);
+    DooFile.RegisterNoChecksNeeded(WarnRedundantAssumptions, true);
+    DooFile.RegisterNoChecksNeeded(VerificationCoverageReport, false);
+    DooFile.RegisterNoChecksNeeded(NoTimeStampForCoverageReport, false);
+    DooFile.RegisterNoChecksNeeded(DefaultFunctionOpacity, true);
+    DooFile.RegisterNoChecksNeeded(OptimizeErasableDatatypeWrapper, false); // TODO needs translation record registration
+    DooFile.RegisterNoChecksNeeded(AddCompileSuffix, false);  // TODO needs translation record registration
+    DooFile.RegisterNoChecksNeeded(SystemModule, false);
+    DooFile.RegisterNoChecksNeeded(ExecutionCoverageReport, false);
+    DooFile.RegisterNoChecksNeeded(ExtractCounterexample, false);
+    DooFile.RegisterNoChecksNeeded(ShowProofObligationExpressions, false);
   }
-
-  public static readonly Option<bool> FormatPrint = new("--print",
-    @"Print Dafny program to stdout after formatting it instead of altering the files.") {
-  };
 }
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -20,11 +20,6 @@ static DafnyCommands() {
     }, false, "Dafny input files and/or a Dafny project file");
   }
 
-  public static IEnumerable<Option> FormatOptions => new Option[] {
-    CommonOptionBag.Check,
-    CommonOptionBag.FormatPrint,
-  }.Concat(ParserOptions);
-
   public static readonly IReadOnlyList<Option> VerificationOptions = new Option[] {
     CommonOptionBag.ProgressOption,
     CommonOptionBag.RelaxDefiniteAssignment,
@@ -55,6 +50,7 @@ static DafnyCommands() {
 
   public static readonly IReadOnlyList<Option> TranslationOptions = new Option[] {
     BoogieOptionBag.NoVerify,
+    BoogieOptionBag.HiddenNoVerify,
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.OptimizeErasableDatatypeWrapper,
     CommonOptionBag.TestAssumptions,