Chore: Not generate boogie translation if not verifying (#6067)

### What was changed?
I ensure the `Options.DafnyVerify` is set to false if `--no-verify` is
provided, except if `--bprint` is set

### How has this been tested?
A new driver test verifies the new behavior. Without the test, I got it
wrong, so I'm confident that the test ensures the behavior is correct.
I don't think there is another way to test that the Boogie translation
does not happen when it won't actually verify;

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

Makefile

@@ -110,6 +110,8 @@ update-rs-module:
 
 update-go-module:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
+	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
+
 
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)

Source/DafnyCore/DafnyOptions.cs

@@ -6,6 +6,7 @@
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
 using System.CommandLine;
+using System.CommandLine.Binding;
 using System.Diagnostics;
 using System.Globalization;
 using System.Linq;
@@ -75,6 +76,17 @@ public T Get<T>(Option<T> option) {
       return (T)Options.OptionArguments.GetOrDefault(option, () => (object)default(T));
     }
 
+
+    public T GetOrOptionDefault<T>(Option<T> option) {
+      return (T)Options.OptionArguments.GetOrDefault(option, () =>
+       ((IValueDescriptor<T>)option) is {
+         HasDefaultValue: true
+       } valueDescriptor
+          ? valueDescriptor.GetDefaultValue()
+          : (object)default(T)
+      );
+    }
+
     public object Get(Option option) {
       return Options.OptionArguments[option];
     }

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -107,9 +107,14 @@ static BoogieOptionBag() {
     });
     DafnyOptions.RegisterLegacyBinding(Cores,
       (o, f) => o.VcsCores = f == 0 ? (1 + System.Environment.ProcessorCount) / 2 : (int)f);
-    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, value) => {
-      var shouldVerify = !value && !options.Get(HiddenNoVerify);
-      options.Verify = shouldVerify;
+    DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => {
+      var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify);
+      options.Verify = shouldVerify; // Boogie won't verify
+      options.DafnyVerify =
+        shouldVerify ||
+        options.Get(DeveloperOptionBag.BoogiePrint) != null ||
+        options.Get(DeveloperOptionBag.SplitPrint) != null ||
+        options.Get(DeveloperOptionBag.PassivePrint) != null;
     });
     DafnyOptions.RegisterLegacyBinding(VerificationTimeLimit, (o, f) => o.TimeLimit = f);
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -22,6 +22,7 @@
 using JetBrains.Annotations;
 using Microsoft.Dafny;
 using Microsoft.Dafny.Triggers;
+using Serilog.Events;
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
@@ -700,6 +701,10 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
         return new Bpl.Program();
       }
 
+      if (Options.GetOrOptionDefault(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) {
+        Options.OutputWriter.WriteLine("Starting translation to Boogie of module " + forModule.FullDafnyName);
+      }
+
       foreach (var plugin in p.Options.Plugins) {
         foreach (var rewriter in plugin.GetRewriters(p.Reporter)) {
           rewriter.PreVerify(forModule);

Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs

@@ -287,25 +287,34 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
       if (err != null) {
         exitValue = ExitValue.DAFNY_ERROR;
         options.Printer.ErrorWriteLine(options.OutputWriter, err);
-      } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck
-          && options.DafnyVerify) {
+      } else if (dafnyProgram != null && !options.NoResolve && !options.NoTypecheck) {
 
+        bool verified;
+        PipelineOutcome outcome;
+        IDictionary<string, PipelineStatistics> moduleStats;
         dafnyProgram.ProofDependencyManager = depManager;
-        var boogiePrograms =
-          await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
-
-        string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
-        var (verified, outcome, moduleStats) =
-          await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId);
-
-        if (options.TrackVerificationCoverage) {
-          ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options, dafnyProgram.Reporter, depManager);
-          var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
-          if (coverageReportDir != null) {
-            await new CoverageReporter(options).SerializeVerificationCoverageReport(
-              depManager, dafnyProgram,
-              boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
-              coverageReportDir);
+        if (!options.DafnyVerify) {
+          verified = false;
+          outcome = PipelineOutcome.Done;
+          moduleStats = new Dictionary<string, PipelineStatistics>();
+        } else {
+          var boogiePrograms =
+            await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
+
+          string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1]));
+          (verified, outcome, moduleStats) =
+            await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId);
+
+          if (options.TrackVerificationCoverage) {
+            ProofDependencyWarnings.WarnAboutSuspiciousDependenciesUsingStoredPartialResults(options,
+              dafnyProgram.Reporter, depManager);
+            var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
+            if (coverageReportDir != null) {
+              await new CoverageReporter(options).SerializeVerificationCoverageReport(
+                depManager, dafnyProgram,
+                boogiePrograms.SelectMany(tp => tp.Item2.AllCoveredElements),
+                coverageReportDir);
+            }
           }
         }
 
@@ -329,7 +338,7 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
         }
 
         var failBecauseOfDiagnostics = dafnyProgram.Reporter.FailCompilationMessage;
-        if (!verified) {
+        if (!verified && options.DafnyVerify) {
           exitValue = ExitValue.VERIFICATION_ERROR;
         } else if (!compiled) {
           exitValue = ExitValue.COMPILE_ERROR;

Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafnyFromDafny.go

@@ -102,9 +102,9 @@ TAIL_CALL_START:
 			e = _in1
 			stack = _in2
 			goto TAIL_CALL_START
-			goto L0_0
+			goto L0
 		}
-	L0_0:
+	L0:
 	} else if func(_is_3 Sequence) bool {
 		return InstanceOf(_is_3, (*LazySequence)(nil))
 	}(e) {
@@ -152,9 +152,9 @@ TAIL_CALL_START:
 				e = _in7
 				stack = _in8
 				goto TAIL_CALL_START
-				goto L1_1_0_0_0
+				goto L1
 			}
-		L1_1_0_0_0:
+		L1:
 		}
 	} else {
 		if !(false) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCases.dfy

@@ -0,0 +1,26 @@
+// NONUNIFORM: Only testing the translation to Boogie aspect of the pipeline depending on checks
+// RUN: %baredafny run  %args --log-level verbose "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesNoTranslation.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --bprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+// RUN: %baredafny run  %args --log-level verbose --no-verify --sprint:file.bpl "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/TranslationCasesTranslate.check"
+
+module VerifiableModule {
+  @Test
+  method CanTest() {
+    assert 1 == 1;
+    expect 1 == 1;
+  }
+  method Main() {
+    CanTest();
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesNoTranslation.check

@@ -0,0 +1 @@
+// CHECK-NOT: Starting translation to Boogie of module VerifiableModule

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TranslationCasesTranslate.check

@@ -0,0 +1 @@
+// CHECK: Starting translation to Boogie of module VerifiableModule

Source/TestDafny/MultiBackendTest.cs

@@ -507,7 +507,7 @@ await output.WriteLineAsync(
     }
     await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:");
     await output.WriteLineAsync(outputString);
-    await output.WriteLineAsync("Error:");
+    await output.WriteLineAsync($"Error (code={exitCode}):");
     await output.WriteLineAsync(error);
     return exitCode;
   }