Make the -quiet flag skip counter-example printing (#1163)

llvm_util/cmd_args_def.h

@@ -21,6 +21,7 @@ config::smt_benchmark_dir = opt_smt_bench_dir;
 smt::solver_print_queries(opt_smt_verbose);
 smt::solver_tactic_verbose(opt_tactic_verbose);
 config::debug = opt_debug;
+config::quiet = opt_quiet;
 config::max_offset_bits = opt_max_offset_in_bits;
 config::max_sizet_bits  = opt_max_sizet_in_bits;
 

llvm_util/compare.cpp

@@ -6,6 +6,7 @@
 #include "llvm_util/llvm_optimizer.h"
 #include "smt/smt.h"
 #include "tools/transform.h"
+#include "util/config.h"
 
 #include <sstream>
 #include <utility>
@@ -96,7 +97,7 @@ Results verify(llvm::Function &F1, llvm::Function &F2,
 } // namespace
 
 bool Verifier::compareFunctions(llvm::Function &F1, llvm::Function &F2) {
-  auto r = verify(F1, F2, TLI, smt_init, out, !quiet, always_verify);
+  auto r = verify(F1, F2, TLI, smt_init, out, !config::quiet, always_verify);
   if (r.status == Results::ERROR) {
     out << "ERROR: " << r.error;
     ++num_errors;
@@ -134,7 +135,7 @@ bool Verifier::compareFunctions(llvm::Function &F1, llvm::Function &F2) {
 
   case Results::UNSOUND:
     out << "Transformation doesn't verify!\n\n";
-    if (!quiet)
+    if (!config::quiet)
       out << r.errs << endl;
     ++num_unsound;
     return false;
@@ -160,13 +161,13 @@ bool Verifier::compareFunctions(llvm::Function &F1, llvm::Function &F2) {
 
     case Results::FAILED_TO_PROVE:
       out << "Failed to verify the reverse transformation\n\n";
-      if (!quiet)
+      if (!config::quiet)
         out << r.errs << endl;
       return true;
 
     case Results::UNSOUND:
       out << "Reverse transformation doesn't verify!\n\n";
-      if (!quiet)
+      if (!config::quiet)
         out << r.errs << endl;
       return false;
     }

llvm_util/compare.h

@@ -18,7 +18,6 @@ struct Verifier {
   unsigned num_unsound = 0;
   unsigned num_failed = 0;
   unsigned num_errors = 0;
-  bool quiet = false;
   bool always_verify = false;
   bool print_dot = false;
   bool bidirectional = false;

tools/alive-exec.cpp

@@ -54,7 +54,7 @@ optional<StateValue> exec(llvm::Function &F,
     return {};
   }
 
-  if (!opt_quiet)
+  if (!config::quiet)
     Func->print(cout << "\n----------------------------------------\n");
 
   {
@@ -99,7 +99,7 @@ optional<StateValue> exec(llvm::Function &F,
     auto It = curr_bb->instrs().begin();
     Solver solver(true);
 
-    if (!opt_quiet)
+    if (!config::quiet)
       cout << "Executing " << curr_bb->getName() << '\n';
 
     while (true) {
@@ -120,7 +120,7 @@ optional<StateValue> exec(llvm::Function &F,
       if (dynamic_cast<const Return*>(&next_instr)) {
         assert(r.isSat());
         auto ret = eval(r, state.returnVal().val);
-        if (!opt_quiet)
+        if (!config::quiet)
           cout << "Returned " << ret << '\n';
         return ret;
       }
@@ -137,7 +137,7 @@ optional<StateValue> exec(llvm::Function &F,
               return {};
 
             if (r.isSat()) {
-              if (!opt_quiet)
+              if (!config::quiet)
                 cout << "  >> Jump to " << dst.getName() << "\n\n";
               curr_bb = &dst;
               state.startBB(dst);
@@ -166,7 +166,7 @@ optional<StateValue> exec(llvm::Function &F,
         return {};
       }
 
-      if (!opt_quiet) {
+      if (!config::quiet) {
         cout << name;
         if (name[0] == '%') {
           auto v = eval(r, val.val);

tools/alive-tv.cpp

@@ -138,7 +138,6 @@ and "tgt5" will unused.
   llvm_util::initializer llvm_util_init(*out, DL);
   smt::smt_initializer smt_init;
   Verifier verifier(TLI, smt_init, *out);
-  verifier.quiet = opt_quiet;
   verifier.always_verify = opt_always_verify;
   verifier.print_dot = opt_print_dot;
   verifier.bidirectional = opt_bidirectional;

tools/quick-fuzz.cpp

@@ -922,7 +922,6 @@ reduced using llvm-reduce.
   llvm_util::initializer llvm_util_init(*out, DL);
   smt::smt_initializer smt_init;
   Verifier verifier(TLI, smt_init, *out);
-  verifier.quiet = opt_quiet;
   verifier.always_verify = opt_always_verify;
   verifier.print_dot = opt_print_dot;
   verifier.bidirectional = opt_bidirectional;

tools/transform.cpp

@@ -167,6 +167,12 @@ static bool error(Errors &errs, State &src_state, State &tgt_state,
     }
   }
 
+  // Return early if instance reporting is not requested.
+  if (config::quiet) {
+    errs.add(msg, true);
+    return false;
+  }
+
   // minimize the model
   optional<Result> newr;
 

tv/tv.cpp

@@ -248,7 +248,7 @@ struct TVLegacyPass final : public llvm::ModulePass {
     if (!opt_always_verify) {
       // Compare Alive2 IR and skip if syntactically equal
       if (src_tostr == tgt_tostr) {
-        if (!opt_quiet) {
+        if (!config::quiet) {
           TransformPrintOpts print_opts;
           print_opts.skip_tgt = true;
           t.print(*out, print_opts);
@@ -311,7 +311,7 @@ struct TVLegacyPass final : public llvm::ModulePass {
     smt_init->reset();
     t.preprocess();
     TransformVerify verifier(t, false);
-    if (!opt_quiet)
+    if (!config::quiet)
       t.print(*out);
 
     {

util/config.cpp

@@ -19,6 +19,7 @@ bool tgt_is_asm = false;
 bool fail_if_src_is_ub = false;
 bool disallow_ub_exploitation = false;
 bool debug = false;
+bool quiet = false;
 unsigned src_unroll_cnt = 0;
 unsigned tgt_unroll_cnt = 0;
 unsigned max_offset_bits = 64;

util/config.h

@@ -31,6 +31,8 @@ extern bool disallow_ub_exploitation;
 
 extern bool debug;
 
+extern bool quiet;
+
 extern unsigned src_unroll_cnt;
 
 extern unsigned tgt_unroll_cnt;