From da777a0ba223a867082255fe33e2ee1ef5975369 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 14 Jun 2024 19:23:21 -0700 Subject: [PATCH] increase verbosity level of various messages CBMC generates too much console output. This commit increases the verbosity level required for various progress and performance statistics messages. --- .../cbmc/export-symex-ready-goto/test-correct.desc | 2 +- regression/cbmc/json1/test.desc | 2 +- regression/cbmc/sat-solver/test.desc | 2 +- src/cbmc/cbmc_parse_options.cpp | 2 +- src/goto-checker/bmc_util.cpp | 5 +++-- src/goto-checker/multi_path_symex_only_checker.cpp | 4 ++-- src/goto-checker/single_path_symex_checker.cpp | 4 ++-- .../single_path_symex_only_checker.cpp | 4 ++-- src/goto-programs/initialize_goto_model.cpp | 4 ++-- src/solvers/prop/prop_conv_solver.cpp | 8 ++++---- src/solvers/refinement/bv_refinement_loop.cpp | 14 +++++++------- 11 files changed, 26 insertions(+), 25 deletions(-) diff --git a/regression/cbmc/export-symex-ready-goto/test-correct.desc b/regression/cbmc/export-symex-ready-goto/test-correct.desc index e6b592328c7..1e2a07a3a1d 100644 --- a/regression/cbmc/export-symex-ready-goto/test-correct.desc +++ b/regression/cbmc/export-symex-ready-goto/test-correct.desc @@ -1,6 +1,6 @@ CORE test.c ---export-symex-ready-goto exported.symex.ready.goto +--export-symex-ready-goto exported.symex.ready.goto --verbosity 10 ^Parsing test.c$ ^Converting$ ^Type-checking test$ diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc index b9eb6a30118..64615201bee 100644 --- a/regression/cbmc/json1/test.desc +++ b/regression/cbmc/json1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---json-ui --stop-on-fail +--json-ui --stop-on-fail --verbosity 10 activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/sat-solver/test.desc b/regression/cbmc/sat-solver/test.desc index 78e0e506126..02d5a0c383b 100644 --- a/regression/cbmc/sat-solver/test.desc +++ b/regression/cbmc/sat-solver/test.desc @@ -1,6 +1,6 @@ CORE broken-z3-smt-backend broken-cprover-smt-backend no-new-smt test.c ---sat-solver cadical +--sat-solver cadical --verbosity 10 ^EXIT=10$ ^SIGNAL=0$ Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cf3d5e6102e..8c4a6d6fcd9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -838,7 +838,7 @@ int cbmc_parse_optionst::get_goto_program( return CPROVER_EXIT_SUCCESS; } - log.status() << config.object_bits_info() << messaget::eom; + log.statistics() << config.object_bits_info() << messaget::eom; return -1; // no error, continue } diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index b434a4d3a38..fcdd4f76142 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -350,8 +350,9 @@ void postprocess_equation( std::chrono::duration postprocess_equation_runtime = std::chrono::duration( postprocess_equation_stop - postprocess_equation_start); - log.status() << "Runtime Postprocess Equation: " - << postprocess_equation_runtime.count() << "s" << messaget::eom; + log.statistics() << "Runtime Postprocess Equation: " + << postprocess_equation_runtime.count() << "s" + << messaget::eom; } std::chrono::duration prepare_property_decider( diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index 2755a92b54d..ed094eb53e5 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -85,8 +85,8 @@ void multi_path_symex_only_checkert::generate_equation() const auto symex_stop = std::chrono::steady_clock::now(); std::chrono::duration symex_runtime = std::chrono::duration(symex_stop - symex_start); - log.status() << "Runtime Symex: " << symex_runtime.count() << "s" - << messaget::eom; + log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s" + << messaget::eom; postprocess_equation(symex, equation, options, ns, ui_message_handler); } diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 7b6e0b2078e..9d3d21c691b 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -82,8 +82,8 @@ operator()(propertiest &properties) worklist->pop(); } - log.status() << "Runtime Symex: " << symex_runtime.count() << "s" - << messaget::eom; + log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s" + << messaget::eom; final_update_properties(properties, result.updated_properties); diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp index 518c0b501ee..3f8ad17627a 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -52,8 +52,8 @@ operator()(propertiest &properties) worklist->pop(); } - log.status() << "Runtime Symex: " << symex_runtime.count() << "s" - << messaget::eom; + log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s" + << messaget::eom; final_update_properties(properties, result.updated_properties); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 1e34c9d0e88..b7aada2c44f 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -93,7 +93,7 @@ void initialize_from_source_files( languaget &language = *lf.language; language.set_language_options(options, message_handler); - msg.status() << "Parsing " << filename << messaget::eom; + msg.progress() << "Parsing " << filename << messaget::eom; if(language.parse(infile, filename, message_handler)) { @@ -103,7 +103,7 @@ void initialize_from_source_files( lf.get_modules(); } - msg.status() << "Converting" << messaget::eom; + msg.progress() << "Converting" << messaget::eom; if(language_files.typecheck(symbol_table, message_handler)) { diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index cd0e5392c1f..597f95c7067 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -447,18 +447,18 @@ prop_conv_solvert::dec_solve(const exprt &assumption) { const auto post_process_start = std::chrono::steady_clock::now(); - log.statistics() << "Post-processing" << messaget::eom; + log.progress() << "Post-processing" << messaget::eom; finish_eager_conversion(); post_processing_done = true; const auto post_process_stop = std::chrono::steady_clock::now(); std::chrono::duration post_process_runtime = std::chrono::duration(post_process_stop - post_process_start); - log.status() << "Runtime Post-process: " << post_process_runtime.count() - << "s" << messaget::eom; + log.statistics() << "Runtime Post-process: " << post_process_runtime.count() + << "s" << messaget::eom; } - log.statistics() << "Solving with " << prop.solver_text() << messaget::eom; + log.progress() << "Solving with " << prop.solver_text() << messaget::eom; if(assumption.is_nil()) push(); diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index da418cf0329..f55b56097be 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -24,7 +24,7 @@ bv_refinementt::bv_refinementt(const infot &info) decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) { // do the usual post-processing - log.status() << "BV-Refinement: post-processing" << messaget::eom; + log.progress() << "BV-Refinement: post-processing" << messaget::eom; finish_eager_conversion(); log.debug() << "Solving with " << prop.solver_text() << messaget::eom; @@ -36,7 +36,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) { iteration++; - log.status() << "BV-Refinement: iteration " << iteration << messaget::eom; + log.progress() << "BV-Refinement: iteration " << iteration << messaget::eom; // output the very same information in a structured fashion if(config_.output_xml) @@ -54,12 +54,12 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) { log.status() << "BV-Refinement: got SAT, and it simulates => SAT" << messaget::eom; - log.status() << "Total iterations: " << iteration << messaget::eom; + log.statistics() << "Total iterations: " << iteration << messaget::eom; return resultt::D_SATISFIABLE; } else - log.status() << "BV-Refinement: got SAT, and it is spurious, refining" - << messaget::eom; + log.progress() << "BV-Refinement: got SAT, and it is spurious, refining" + << messaget::eom; break; case resultt::D_UNSATISFIABLE: @@ -69,11 +69,11 @@ decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) log.status() << "BV-Refinement: got UNSAT, and the proof passes => UNSAT" << messaget::eom; - log.status() << "Total iterations: " << iteration << messaget::eom; + log.statistics() << "Total iterations: " << iteration << messaget::eom; return resultt::D_UNSATISFIABLE; } else - log.status() + log.progress() << "BV-Refinement: got UNSAT, and the proof fails, refining" << messaget::eom; break;