From 1e8f5b1603f163961a2a915472f9e3d49b518822 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 Apr 2019 16:17:53 +0100 Subject: [PATCH 1/4] janalyzer_parse_options is not a message In addition this class already inherits a messaget object of type messaget. --- .../src/janalyzer/janalyzer_parse_options.cpp | 87 ++++++++++--------- jbmc/src/janalyzer/janalyzer_parse_options.h | 2 +- 2 files changed, 49 insertions(+), 40 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 00e6645f376..77dd822eac5 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -59,7 +59,6 @@ Author: Daniel Kroening, kroening@kroening.com janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv) : parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler), - messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION) { } @@ -260,7 +259,8 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options) if(!options.get_bool_option("domain set")) { // Default to constants as it is light-weight but useful - status() << "Domain not specified, defaulting to --constants" << eom; + log.status() << "Domain not specified, defaulting to --constants" + << messaget::eom; options.set_option("constants", true); } } @@ -343,31 +343,33 @@ int janalyzer_parse_optionst::doit() optionst options; get_command_line_options(options); - eval_verbosity( + messaget::eval_verbosity( cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); // // Print a banner // - status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8 - << "-bit " << config.this_architecture() << " " - << config.this_operating_system() << eom; + log.status() << "JANALYZER version " << CBMC_VERSION << " " + << sizeof(void *) * 8 << "-bit " << config.this_architecture() + << " " << config.this_operating_system() << messaget::eom; register_languages(); if(cmdline.args.size() > 1) { - error() << "Only one .class, .jar or .gbf file should be directly " - "specified on the command-line. To force loading another another class " - "use '--java-load-class somepackage.SomeClass' or " - "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along " - "with '--classpath'" - << messaget::eom; + log.error() << "Only one .class, .jar or .gbf file should be directly " + "specified on the command-line. To force loading another " + "another class " + "use '--java-load-class somepackage.SomeClass' or " + "'--lazy-methods-extra-entry-point " + "somepackage.SomeClass.method' along " + "with '--classpath'" + << messaget::eom; return CPROVER_EXIT_USAGE_ERROR; } goto_model = - initialize_goto_model(cmdline.args, get_message_handler(), options); + initialize_goto_model(cmdline.args, log.get_message_handler(), options); if(process_goto_program(options)) return CPROVER_EXIT_INTERNAL_ERROR; @@ -386,7 +388,7 @@ int janalyzer_parse_optionst::doit() { show_goto_functions( goto_model, - get_message_handler(), + log.get_message_handler(), get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -404,14 +406,15 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-taint")) { - taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); + taint_analysis( + goto_model, taint_file, log.get_message_handler(), true, ""); return CPROVER_EXIT_SUCCESS; } else { std::string json_file = cmdline.get_value("json"); bool result = taint_analysis( - goto_model, taint_file, get_message_handler(), false, json_file); + goto_model, taint_file, log.get_message_handler(), false, json_file); return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS; } } @@ -432,7 +435,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - error() << "Failed to open json output `" << json_file << "'" << eom; + log.error() << "Failed to open json output `" << json_file << "'" + << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -457,7 +461,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - error() << "Failed to open json output `" << json_file << "'" << eom; + log.error() << "Failed to open json output `" << json_file << "'" + << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -482,7 +487,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) std::ofstream ofs(json_file); if(!ofs) { - error() << "Failed to open json output `" << json_file << "'" << eom; + log.error() << "Failed to open json output `" << json_file << "'" + << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -513,7 +519,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-properties")) { - show_properties(goto_model, get_message_handler(), get_ui()); + show_properties(goto_model, log.get_message_handler(), get_ui()); return CPROVER_EXIT_SUCCESS; } @@ -532,28 +538,29 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(!out) { - error() << "Failed to open output file `" << outfile << "'" << eom; + log.error() << "Failed to open output file `" << outfile << "'" + << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } // Build analyzer - status() << "Selecting abstract domain" << eom; + log.status() << "Selecting abstract domain" << messaget::eom; namespacet ns(goto_model.symbol_table); // Must live as long as the domain. std::unique_ptr analyzer(build_analyzer(options, ns)); if(analyzer == nullptr) { - status() << "Task / Interpreter / Domain combination not supported" - << messaget::eom; + log.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } // Run - status() << "Computing abstract states" << eom; + log.status() << "Computing abstract states" << messaget::eom; (*analyzer)(goto_model); // Perform the task - status() << "Performing task" << eom; + log.status() << "Performing task" << messaget::eom; bool result = true; if(options.get_bool_option("show")) { @@ -563,12 +570,12 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) else if(options.get_bool_option("verify")) { result = static_verifier( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, log.get_message_handler(), out); } else if(options.get_bool_option("simplify")) { result = static_simplifier( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, log.get_message_handler(), out); } else if(options.get_bool_option("unreachable-instructions")) { @@ -587,7 +594,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) } else { - error() << "Unhandled task" << eom; + log.error() << "Unhandled task" << messaget::eom; return CPROVER_EXIT_INTERNAL_ERROR; } @@ -596,7 +603,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) } // Final defensive error case - error() << "no analysis option given -- consider reading --help" << eom; + log.error() << "no analysis option given -- consider reading --help" + << messaget::eom; return CPROVER_EXIT_USAGE_ERROR; } @@ -605,23 +613,24 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) try { // remove function pointers - status() << "Removing function pointers and virtual functions" << eom; + log.status() << "Removing function pointers and virtual functions" + << messaget::eom; remove_function_pointers( - get_message_handler(), goto_model, cmdline.isset("pointer-check")); + log.get_message_handler(), goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); // remove Java throw and catch // This introduces instanceof, so order is important: - remove_exceptions_using_instanceof(goto_model, get_message_handler()); + remove_exceptions_using_instanceof(goto_model, log.get_message_handler()); // Java instanceof -> clsid comparison: class_hierarchyt class_hierarchy(goto_model.symbol_table); - remove_instanceof(goto_model, class_hierarchy, get_message_handler()); + remove_instanceof(goto_model, class_hierarchy, log.get_message_handler()); // do partial inlining - status() << "Partial Inlining" << eom; + log.status() << "Partial Inlining" << messaget::eom; goto_partial_inline(goto_model, ui_message_handler); // remove returns, gcc vectors, complex @@ -630,7 +639,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) remove_complex(goto_model); // add generic checks - status() << "Generic Property Instrumentation" << eom; + log.status() << "Generic Property Instrumentation" << messaget::eom; goto_check(options, goto_model); // recalculate numbers, etc. @@ -642,13 +651,13 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) catch(const char *e) { - error() << e << eom; + log.error() << e << messaget::eom; return true; } catch(const std::string &e) { - error() << e << eom; + log.error() << e << messaget::eom; return true; } @@ -659,7 +668,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) catch(const std::bad_alloc &) { - error() << "Out of memory" << eom; + log.error() << "Out of memory" << messaget::eom; return true; } diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index 04bd55f1d24..3140a94f72a 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -150,7 +150,7 @@ class optionst; JAVA_BYTECODE_LANGUAGE_OPTIONS // clang-format on -class janalyzer_parse_optionst : public parse_options_baset, public messaget +class janalyzer_parse_optionst : public parse_options_baset { public: virtual int doit() override; From a6a06ae924c2c4eae70564e7c0b685679dec3f29 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 Apr 2019 16:19:32 +0100 Subject: [PATCH 2/4] goto_diff_parse_options is not a message In addition the class already inherits a log field of type messaget. --- src/goto-diff/goto_diff_parse_options.cpp | 37 ++++++++++++----------- src/goto-diff/goto_diff_parse_options.h | 2 +- 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index e6d51aee67c..a85ed2c1c78 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -65,7 +65,6 @@ Author: Peter Schrammel goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv) : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv, ui_message_handler), - messaget(ui_message_handler), ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION) { } @@ -201,8 +200,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) if(options.get_bool_option("partial-loops") && options.get_bool_option("unwinding-assertions")) { - error() << "--partial-loops and --unwinding-assertions" - << " must not be given together" << eom; + log.error() << "--partial-loops and --unwinding-assertions" + << " must not be given together" << messaget::eom; exit(1); } @@ -224,19 +223,19 @@ int goto_diff_parse_optionst::doit() optionst options; get_command_line_options(options); - eval_verbosity( + messaget::eval_verbosity( cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); // // Print a banner // - status() << "GOTO-DIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8 - << "-bit " << config.this_architecture() << " " - << config.this_operating_system() << eom; + log.status() << "GOTO-DIFF version " << CBMC_VERSION << " " + << sizeof(void *) * 8 << "-bit " << config.this_architecture() + << " " << config.this_operating_system() << messaget::eom; if(cmdline.args.size()!=2) { - error() << "Please provide two programs to compare" << eom; + log.error() << "Please provide two programs to compare" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } @@ -264,12 +263,12 @@ int goto_diff_parse_optionst::doit() { show_goto_functions( goto_model1, - get_message_handler(), + log.get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); show_goto_functions( goto_model2, - get_message_handler(), + log.get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -321,16 +320,18 @@ bool goto_diff_parse_optionst::process_goto_program( remove_asm(goto_model); // add the library - status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; + log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" + << messaget::eom; link_to_library( - goto_model, get_message_handler(), cprover_cpp_library_factory); + goto_model, log.get_message_handler(), cprover_cpp_library_factory); link_to_library( - goto_model, get_message_handler(), cprover_c_library_factory); + goto_model, log.get_message_handler(), cprover_c_library_factory); // remove function pointers - status() << "Removal of function pointers and virtual functions" << eom; + log.status() << "Removal of function pointers and virtual functions" + << messaget::eom; remove_function_pointers( - get_message_handler(), goto_model, cmdline.isset("pointer-check")); + log.get_message_handler(), goto_model, cmdline.isset("pointer-check")); mm_io(goto_model); @@ -344,7 +345,7 @@ bool goto_diff_parse_optionst::process_goto_program( rewrite_union(goto_model); // add generic checks - status() << "Generic Property Instrumentation" << eom; + log.status() << "Generic Property Instrumentation" << messaget::eom; goto_check(options, goto_model); // checks don't know about adjusted float expressions @@ -364,9 +365,9 @@ bool goto_diff_parse_optionst::process_goto_program( remove_skip(goto_model); const auto cover_config = get_cover_config( - options, goto_model.symbol_table, get_message_handler()); + options, goto_model.symbol_table, log.get_message_handler()); if(instrument_cover_goals( - cover_config, goto_model, get_message_handler())) + cover_config, goto_model, log.get_message_handler())) return true; } diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index a2c067fbf9a..a350d061bf5 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -39,7 +39,7 @@ class optionst; "(compact-output)" // clang-format on -class goto_diff_parse_optionst : public parse_options_baset, public messaget +class goto_diff_parse_optionst : public parse_options_baset { public: virtual int doit(); From af222704e821e6774aa77ae921cba8dce3cade74 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 Apr 2019 16:20:26 +0100 Subject: [PATCH 3/4] jdiff_parse_options is not a message In addition the class already inherits a log field of type messaget. --- jbmc/src/jdiff/jdiff_parse_options.cpp | 30 +++++++++++++------------- jbmc/src/jdiff/jdiff_parse_options.h | 2 +- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 58e108d0022..61e13fe60a9 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -63,7 +63,6 @@ Author: Peter Schrammel jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv) : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler), - messaget(ui_message_handler), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION) { } @@ -186,19 +185,19 @@ int jdiff_parse_optionst::doit() optionst options; get_command_line_options(options); - eval_verbosity( + messaget::eval_verbosity( cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); // // Print a banner // - status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8 - << "-bit " << config.this_architecture() << " " - << config.this_operating_system() << eom; + log.status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8 + << "-bit " << config.this_architecture() << " " + << config.this_operating_system() << messaget::eom; if(cmdline.args.size() != 2) { - error() << "Please provide two programs to compare" << eom; + log.error() << "Please provide two programs to compare" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } @@ -226,12 +225,12 @@ int jdiff_parse_optionst::doit() { show_goto_functions( goto_model1, - get_message_handler(), + log.get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); show_goto_functions( goto_model2, - get_message_handler(), + log.get_message_handler(), ui_message_handler.get_ui(), cmdline.isset("list-goto-functions")); return CPROVER_EXIT_SUCCESS; @@ -275,20 +274,21 @@ bool jdiff_parse_optionst::process_goto_program( { { // remove function pointers - status() << "Removing function pointers and virtual functions" << eom; + log.status() << "Removing function pointers and virtual functions" + << messaget::eom; remove_function_pointers( - get_message_handler(), goto_model, cmdline.isset("pointer-check")); + log.get_message_handler(), goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); // remove Java throw and catch // This introduces instanceof, so order is important: - remove_exceptions_using_instanceof(goto_model, get_message_handler()); + remove_exceptions_using_instanceof(goto_model, log.get_message_handler()); // Java instanceof -> clsid comparison: class_hierarchyt class_hierarchy(goto_model.symbol_table); - remove_instanceof(goto_model, class_hierarchy, get_message_handler()); + remove_instanceof(goto_model, class_hierarchy, log.get_message_handler()); mm_io(goto_model); @@ -302,7 +302,7 @@ bool jdiff_parse_optionst::process_goto_program( rewrite_union(goto_model); // add generic checks - status() << "Generic Property Instrumentation" << eom; + log.status() << "Generic Property Instrumentation" << messaget::eom; goto_check(options, goto_model); // checks don't know about adjusted float expressions @@ -322,9 +322,9 @@ bool jdiff_parse_optionst::process_goto_program( if(cmdline.isset("cover")) { const auto cover_config = get_cover_config( - options, goto_model.symbol_table, get_message_handler()); + options, goto_model.symbol_table, log.get_message_handler()); if(instrument_cover_goals( - cover_config, goto_model, get_message_handler())) + cover_config, goto_model, log.get_message_handler())) return true; } diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index ae22e684bbc..fcb144b43b0 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -40,7 +40,7 @@ class goto_modelt; "(compact-output)" // clang-format on -class jdiff_parse_optionst : public parse_options_baset, public messaget +class jdiff_parse_optionst : public parse_options_baset { public: virtual int doit(); From f9b461a36534320a3db5cd285ffdba0ee83cc79b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 Apr 2019 16:53:42 +0100 Subject: [PATCH 4/4] Remove redundant logger field There is already an inherited field log referencing the same thing. --- src/goto-harness/goto_harness_parse_options.cpp | 11 +++++------ src/goto-harness/goto_harness_parse_options.h | 1 - 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index aa351b926be..4a55b659cf0 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -41,7 +41,7 @@ int goto_harness_parse_optionst::doit() { if(cmdline.isset("version")) { - logger.status() << CBMC_VERSION << '\n'; + log.status() << CBMC_VERSION << '\n'; return CPROVER_EXIT_SUCCESS; } @@ -55,7 +55,7 @@ int goto_harness_parse_optionst::doit() // Read goto binary into goto-model auto read_goto_binary_result = - read_goto_binary(got_harness_config.in_file, logger.get_message_handler()); + read_goto_binary(got_harness_config.in_file, log.get_message_handler()); if(!read_goto_binary_result.has_value()) { throw deserialization_exceptiont{"failed to read goto program from file `" + @@ -89,7 +89,7 @@ int goto_harness_parse_optionst::doit() // Write end result to new goto-binary if(write_goto_binary( - got_harness_config.out_file, goto_model, logger.get_message_handler())) + got_harness_config.out_file, goto_model, log.get_message_handler())) { throw system_exceptiont{"failed to write goto program from file `" + got_harness_config.out_file + "'"}; @@ -100,7 +100,7 @@ int goto_harness_parse_optionst::doit() void goto_harness_parse_optionst::help() { - logger.status() + log.status() << '\n' << banner_string("Goto-Harness", CBMC_VERSION) << '\n' << align_center_with_border("Copyright (C) 2019") << '\n' @@ -127,8 +127,7 @@ goto_harness_parse_optionst::goto_harness_parse_optionst( int argc, const char *argv[]) : parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv, ui_message_handler}, - ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION), - logger(ui_message_handler) + ui_message_handler(cmdline, std::string("GOTO-HARNESS ") + CBMC_VERSION) { } diff --git a/src/goto-harness/goto_harness_parse_options.h b/src/goto-harness/goto_harness_parse_options.h index 8665574c9da..c611d75e70b 100644 --- a/src/goto-harness/goto_harness_parse_options.h +++ b/src/goto-harness/goto_harness_parse_options.h @@ -46,7 +46,6 @@ class goto_harness_parse_optionst : public parse_options_baset }; ui_message_handlert ui_message_handler; - messaget logger; /// Handle command line arguments that are common to all /// harness generators.