Add two options, /quiet and /silent (#694)

* Add two options, /quiet and /silent

The /quiet option suppresses output other than warnings and errors. The
/silent option suppresses all output except the exit code.

* More consistent verbosity level checking

* Clarify help text for `/silent`

Boogie doesn't set a non-zero exit code on verification errors.

Source/Core/CoreOptions.cs

@@ -35,6 +35,16 @@ public enum Inlining
 
     public bool Trace { get; }
 
+    public enum VerbosityLevel
+    {
+      Silent,
+      Quiet,
+      Normal,
+      Trace
+    }
+
+    public VerbosityLevel Verbosity { get; }
+
     public bool TraceVerify { get; }
 
     public int VerifySnapshots { get; }

Source/ExecutionEngine/CommandLineOptions.cs

@@ -431,10 +431,9 @@ public bool PrintWithUniqueASTIds {
     [Peer] public XmlSink XmlSink { get; set; }
     public bool Wait { get; set; }
 
-    public bool Trace {
-      get => trace;
-      set => trace = value;
-    }
+    public bool Trace => Verbosity == CoreOptions.VerbosityLevel.Trace;
+
+    public CoreOptions.VerbosityLevel Verbosity => verbosity;
 
     public bool NormalizeNames
     {
@@ -816,7 +815,6 @@ void ObjectInvariant5()
     private bool trustNoninterference = false;
     private bool trustRefinement = false;
     private bool trustInductiveSequentialization = false;
-    private bool trace = false;
     private int enhancedErrorMessages = 0;
     private int stagedHoudiniThreads = 1;
     private uint timeLimitPerAssertionInPercent = 10;
@@ -829,6 +827,7 @@ void ObjectInvariant5()
     private bool emitDebugInformation = true;
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
+    private CoreOptions.VerbosityLevel verbosity = CoreOptions.VerbosityLevel.Normal;
 
     public List<CoreOptions.ConcurrentHoudiniOptions> Cho { get; set; } = new();
 
@@ -1535,7 +1534,9 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("printInstrumented", x => printInstrumented = x) ||
               ps.CheckBooleanFlag("printWithUniqueIds", x => printWithUniqueAstIds = x) ||
               ps.CheckBooleanFlag("wait", x => Wait = x) ||
-              ps.CheckBooleanFlag("trace", x => trace = x) ||
+              ps.CheckBooleanFlag("trace", x => verbosity = CoreOptions.VerbosityLevel.Trace) ||
+              ps.CheckBooleanFlag("quiet", x => verbosity = CoreOptions.VerbosityLevel.Quiet) ||
+              ps.CheckBooleanFlag("silent", x => verbosity = CoreOptions.VerbosityLevel.Silent) ||
               ps.CheckBooleanFlag("traceTimes", x => TraceTimes = x) ||
               ps.CheckBooleanFlag("tracePOs", x => TraceProofObligations = x) ||
               ps.CheckBooleanFlag("noResolve", x => NoResolve = x) ||
@@ -2088,6 +2089,8 @@ print Boogie program after it has been instrumented with
 
   ---- Debugging and general tracing options ---------------------------------
 
+  /silent       print nothing at all
+  /quiet        print nothing but warnings and errors
   /trace        blurt out various debug trace information
   /traceTimes   output timing information at certain points in the pipeline
   /tracePOs     output information about the number of proof obligations

Source/ExecutionEngine/ConsolePrinter.cs

@@ -13,6 +13,10 @@ public class ConsolePrinter : OutputPrinter
   public virtual void ErrorWriteLine(TextWriter tw, string s)
   {
     Contract.Requires(s != null);
+    if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
+      return;
+    }
+
     if (!s.Contains("Error: ") && !s.Contains("Error BP"))
     {
       tw.WriteLine(s);
@@ -48,6 +52,10 @@ public virtual void ErrorWriteLine(TextWriter tw, string s)
   public virtual void ErrorWriteLine(TextWriter tw, string format, params object[] args)
   {
     Contract.Requires(format != null);
+    if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
+      return;
+    }
+
     string s = string.Format(format, args);
     ErrorWriteLine(tw, s);
   }
@@ -56,6 +64,10 @@ public virtual void ErrorWriteLine(TextWriter tw, string format, params object[]
   public virtual void AdvisoryWriteLine(TextWriter output, string format, params object[] args)
   {
     Contract.Requires(format != null);
+    if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
+      return;
+    }
+
     ConsoleColor col = Console.ForegroundColor;
     Console.ForegroundColor = ConsoleColor.Yellow;
     Console.WriteLine(format, args);
@@ -82,6 +94,10 @@ public virtual void WriteTrailer(TextWriter textWriter, PipelineStatistics stats
     Contract.Requires(0 <= stats.VerifiedCount && 0 <= stats.ErrorCount && 0 <= stats.InconclusiveCount &&
                       0 <= stats.TimeoutCount && 0 <= stats.OutOfMemoryCount);
 
+    if (Options.Verbosity <= CoreOptions.VerbosityLevel.Quiet) {
+      return;
+    }
+
     textWriter.WriteLine();
     if (Options.ShowVerifiedProcedureCount)
     {
@@ -128,6 +144,10 @@ public virtual void WriteErrorInformation(ErrorInformation errorInfo, TextWriter
   {
     Contract.Requires(errorInfo != null);
 
+    if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
+      return;
+    }
+
     ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw);
 
     foreach (var e in errorInfo.Aux)
@@ -148,6 +168,10 @@ public virtual void ReportBplError(IToken tok, string message, bool error, TextW
   {
     Contract.Requires(message != null);
 
+    if (Options.Verbosity == CoreOptions.VerbosityLevel.Silent) {
+      return;
+    }
+
     if (category != null)
     {
       message = string.Format("{0}: {1}", category, message);

Test/commandline/quiet.bpl

@@ -0,0 +1,7 @@
+// RUN: %parallel-boogie -quiet "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure BadAssert()
+{
+  assert 1 == 2;
+}

Test/commandline/quiet.bpl.expect

@@ -0,0 +1,3 @@
+quiet.bpl(6,3): Error: this assertion could not be proved
+Execution trace:
+    quiet.bpl(6,3): anon0

Test/commandline/silent.bpl

@@ -0,0 +1,7 @@
+// RUN: %parallel-boogie -silent "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure BadAssert()
+{
+  assert 1 == 2;
+}