From fb4e7ef296b2485664dcf37908240b259076430d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 20 Feb 2023 03:55:24 -0800 Subject: [PATCH] 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 | 10 ++++++++ Source/ExecutionEngine/CommandLineOptions.cs | 15 +++++++----- Source/ExecutionEngine/ConsolePrinter.cs | 24 ++++++++++++++++++++ Test/commandline/quiet.bpl | 7 ++++++ Test/commandline/quiet.bpl.expect | 3 +++ Test/commandline/silent.bpl | 7 ++++++ Test/commandline/silent.bpl.expect | 0 7 files changed, 60 insertions(+), 6 deletions(-) create mode 100644 Test/commandline/quiet.bpl create mode 100644 Test/commandline/quiet.bpl.expect create mode 100644 Test/commandline/silent.bpl create mode 100644 Test/commandline/silent.bpl.expect diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index 4aaade7ec..55dbe5a84 100644 --- a/Source/Core/CoreOptions.cs +++ b/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; } diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index c495e6fcb..37090df4c 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/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 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 diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs index b951f9439..b47bfae5f 100644 --- a/Source/ExecutionEngine/ConsolePrinter.cs +++ b/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); diff --git a/Test/commandline/quiet.bpl b/Test/commandline/quiet.bpl new file mode 100644 index 000000000..97af37dfd --- /dev/null +++ b/Test/commandline/quiet.bpl @@ -0,0 +1,7 @@ +// RUN: %parallel-boogie -quiet "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure BadAssert() +{ + assert 1 == 2; +} diff --git a/Test/commandline/quiet.bpl.expect b/Test/commandline/quiet.bpl.expect new file mode 100644 index 000000000..44ffd83a3 --- /dev/null +++ b/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 diff --git a/Test/commandline/silent.bpl b/Test/commandline/silent.bpl new file mode 100644 index 000000000..369d98445 --- /dev/null +++ b/Test/commandline/silent.bpl @@ -0,0 +1,7 @@ +// RUN: %parallel-boogie -silent "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure BadAssert() +{ + assert 1 == 2; +} diff --git a/Test/commandline/silent.bpl.expect b/Test/commandline/silent.bpl.expect new file mode 100644 index 000000000..e69de29bb