From 101d2df9be32daba69303c7a65ba73366321704a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jan 2019 14:59:32 +0000 Subject: [PATCH 1/4] Remove unnecessary use of "virtual" These functions are neither provided by any base classes nor is anyone inheriting from these classes. --- jbmc/src/janalyzer/janalyzer_parse_options.h | 6 +++--- jbmc/src/jdiff/jdiff_parse_options.h | 5 ++--- src/goto-diff/goto_diff_parse_options.h | 6 ++---- src/goto-instrument/goto_instrument_parse_options.h | 2 +- 4 files changed, 8 insertions(+), 11 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index 42b48315c53..04bd55f1d24 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -162,11 +162,11 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget ui_message_handlert ui_message_handler; goto_modelt goto_model; - virtual void register_languages(); + void register_languages(); - virtual void get_command_line_options(optionst &options); + void get_command_line_options(optionst &options); - virtual bool process_goto_program(const optionst &options); + bool process_goto_program(const optionst &options); virtual int perform_analysis(const optionst &options); diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index e56f44633ee..ec7a9b0700b 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -59,15 +59,14 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest ui_message_handlert ui_message_handler; jdiff_languagest languages2; - virtual void get_command_line_options(optionst &options); + void get_command_line_options(optionst &options); virtual int get_goto_program( const optionst &options, jdiff_languagest &languages, goto_modelt &goto_model); - virtual bool - process_goto_program(const optionst &options, goto_modelt &goto_model); + bool process_goto_program(const optionst &options, goto_modelt &goto_model); void preprocessing(); }; diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index e7822385f8d..ba7f511e949 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -59,16 +59,14 @@ class goto_diff_parse_optionst: ui_message_handlert ui_message_handler; goto_diff_languagest languages2; - virtual void get_command_line_options(optionst &options); + void get_command_line_options(optionst &options); virtual int get_goto_program( const optionst &options, goto_diff_languagest &languages, goto_modelt &goto_model); - virtual bool process_goto_program( - const optionst &options, - goto_modelt &goto_model); + bool process_goto_program(const optionst &options, goto_modelt &goto_model); void preprocessing(); }; diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 3c26973c8c1..647ec904b0b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -135,7 +135,7 @@ class goto_instrument_parse_optionst: protected: ui_message_handlert ui_message_handler; - virtual void register_languages(); + void register_languages(); void get_goto_program(); void instrument_goto_program(); From 750e2f32e1363a2ae33b0d3ad23ef5bfdef7ae51 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jan 2019 15:15:14 +0000 Subject: [PATCH 2/4] Remove useless method declaration "preprocessing" is not actually defined. --- jbmc/src/jdiff/jdiff_parse_options.h | 2 -- src/goto-diff/goto_diff_parse_options.h | 2 -- 2 files changed, 4 deletions(-) diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index ec7a9b0700b..653c2ff5352 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -67,8 +67,6 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest goto_modelt &goto_model); bool process_goto_program(const optionst &options, goto_modelt &goto_model); - - void preprocessing(); }; #endif // CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index ba7f511e949..c7155f08b94 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -67,8 +67,6 @@ class goto_diff_parse_optionst: goto_modelt &goto_model); bool process_goto_program(const optionst &options, goto_modelt &goto_model); - - void preprocessing(); }; #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H From 12e8e5adde03b4c9991a151a6dd84a3246f86e78 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jan 2019 15:16:04 +0000 Subject: [PATCH 3/4] Remove language_uit dependency from goto-diff Parsing is encapsulated in initialize_goto_model. --- src/goto-diff/goto_diff_languages.cpp | 4 +- src/goto-diff/goto_diff_languages.h | 33 ------- src/goto-diff/goto_diff_parse_options.cpp | 102 +++------------------- src/goto-diff/goto_diff_parse_options.h | 17 +--- 4 files changed, 18 insertions(+), 138 deletions(-) delete mode 100644 src/goto-diff/goto_diff_languages.h diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp index ecec4354e12..acc0817d634 100644 --- a/src/goto-diff/goto_diff_languages.cpp +++ b/src/goto-diff/goto_diff_languages.cpp @@ -9,14 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Language Registration -#include "goto_diff_languages.h" +#include "goto_diff_parse_options.h" #include #include #include -void goto_diff_languagest::register_languages() +void goto_diff_parse_optionst::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); diff --git a/src/goto-diff/goto_diff_languages.h b/src/goto-diff/goto_diff_languages.h deleted file mode 100644 index 7bd4c24e525..00000000000 --- a/src/goto-diff/goto_diff_languages.h +++ /dev/null @@ -1,33 +0,0 @@ -/*******************************************************************\ - -Module: GOTO-DIFF Languages - -Author: Peter Schrammel - -\*******************************************************************/ - -/// \file -/// GOTO-DIFF Languages - -#ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_LANGUAGES_H -#define CPROVER_GOTO_DIFF_GOTO_DIFF_LANGUAGES_H - -#include -#include - -class goto_diff_languagest:public language_uit -{ -public: - explicit goto_diff_languagest( - const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler) : - language_uit(cmdline, ui_message_handler) - { - register_languages(); - } - -protected: - virtual void register_languages(); -}; - -#endif // CPROVER_GOTO_DIFF_GOTO_DIFF_LANGUAGES_H diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index ad12b42d223..dfd595cbf2b 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -27,6 +27,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include @@ -62,24 +63,8 @@ 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), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler) -{ -} - -::goto_diff_parse_optionst::goto_diff_parse_optionst( - int argc, - const char **argv, - const std::string &extra_options) - : parse_options_baset( - GOTO_DIFF_OPTIONS + extra_options, - argc, - argv, - ui_message_handler), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler) + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION) { } @@ -253,21 +238,21 @@ int goto_diff_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - goto_modelt goto_model1, goto_model2; + register_languages(); - int get_goto_program_ret= - get_goto_program(options, *this, goto_model1); - if(get_goto_program_ret!=-1) - return get_goto_program_ret; - get_goto_program_ret= - get_goto_program(options, languages2, goto_model2); - if(get_goto_program_ret!=-1) - return get_goto_program_ret; + goto_modelt goto_model1 = + initialize_goto_model({cmdline.args[0]}, ui_message_handler, options); + if(process_goto_program(options, goto_model1)) + return CPROVER_EXIT_INTERNAL_ERROR; + goto_modelt goto_model2 = + initialize_goto_model({cmdline.args[1]}, ui_message_handler, options); + if(process_goto_program(options, goto_model2)) + return CPROVER_EXIT_INTERNAL_ERROR; if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_model1); - show_loop_ids(get_ui(), goto_model2); + show_loop_ids(ui_message_handler.get_ui(), goto_model1); + show_loop_ids(ui_message_handler.get_ui(), goto_model2); return CPROVER_EXIT_SUCCESS; } @@ -324,65 +309,6 @@ int goto_diff_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } -int goto_diff_parse_optionst::get_goto_program( - const optionst &options, - goto_diff_languagest &languages, - goto_modelt &goto_model) -{ - status() << "Reading program from `" << cmdline.args[0] << "'" << eom; - - if(is_goto_binary(cmdline.args[0])) - { - auto tmp_goto_model = - read_goto_binary(cmdline.args[0], languages.get_message_handler()); - if(!tmp_goto_model.has_value()) - return CPROVER_EXIT_INCORRECT_TASK; - - goto_model = std::move(*tmp_goto_model); - - config.set(cmdline); - - // This one is done. - cmdline.args.erase(cmdline.args.begin()); - } - else - { - // This is a a workaround to make parse() think that there is only - // one source file. - std::string arg2(""); - if(cmdline.args.size()==2) - { - arg2 = cmdline.args[1]; - cmdline.args.erase(--cmdline.args.end()); - } - - if(languages.parse() || - languages.typecheck() || - languages.final()) - return CPROVER_EXIT_INCORRECT_TASK; - - // we no longer need any parse trees or language files - languages.clear_parse(); - - status() << "Generating GOTO Program" << eom; - - goto_model.symbol_table=languages.symbol_table; - goto_convert( - goto_model.symbol_table, - goto_model.goto_functions, - ui_message_handler); - - if(process_goto_program(options, goto_model)) - return CPROVER_EXIT_INTERNAL_ERROR; - - // if we had a second argument then we will handle it next - if(arg2!="") - cmdline.args[0]=arg2; - } - - return -1; // no error, continue -} - bool goto_diff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index c7155f08b94..a2c067fbf9a 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -22,8 +22,6 @@ Author: Peter Schrammel #include #include -#include "goto_diff_languages.h" - class goto_modelt; class optionst; @@ -41,31 +39,20 @@ class optionst; "(compact-output)" // clang-format on -class goto_diff_parse_optionst: - public parse_options_baset, - public goto_diff_languagest +class goto_diff_parse_optionst : public parse_options_baset, public messaget { public: virtual int doit(); virtual void help(); goto_diff_parse_optionst(int argc, const char **argv); - goto_diff_parse_optionst( - int argc, - const char **argv, - const std::string &extra_options); protected: ui_message_handlert ui_message_handler; - goto_diff_languagest languages2; + void register_languages(); void get_command_line_options(optionst &options); - virtual int get_goto_program( - const optionst &options, - goto_diff_languagest &languages, - goto_modelt &goto_model); - bool process_goto_program(const optionst &options, goto_modelt &goto_model); }; From cb4352465698c6e8bc1002113951947d08251619 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jan 2019 15:16:53 +0000 Subject: [PATCH 4/4] Remove language_uit dependency from jdiff Parsing is encapsulated in initialize_goto_model. --- jbmc/src/jdiff/jdiff_languages.cpp | 4 +- jbmc/src/jdiff/jdiff_languages.h | 34 --------- jbmc/src/jdiff/jdiff_parse_options.cpp | 98 ++++---------------------- jbmc/src/jdiff/jdiff_parse_options.h | 16 +---- 4 files changed, 18 insertions(+), 134 deletions(-) delete mode 100644 jbmc/src/jdiff/jdiff_languages.h diff --git a/jbmc/src/jdiff/jdiff_languages.cpp b/jbmc/src/jdiff/jdiff_languages.cpp index 7a77f280018..aefd2f86b33 100644 --- a/jbmc/src/jdiff/jdiff_languages.cpp +++ b/jbmc/src/jdiff/jdiff_languages.cpp @@ -9,13 +9,13 @@ Author: Peter Schrammel /// \file /// Language Registration -#include "jdiff_languages.h" +#include "jdiff_parse_options.h" #include #include -void jdiff_languagest::register_languages() +void jdiff_parse_optionst::register_languages() { register_language(new_java_bytecode_language); } diff --git a/jbmc/src/jdiff/jdiff_languages.h b/jbmc/src/jdiff/jdiff_languages.h deleted file mode 100644 index 22df0df0acd..00000000000 --- a/jbmc/src/jdiff/jdiff_languages.h +++ /dev/null @@ -1,34 +0,0 @@ -/*******************************************************************\ - -Module: JDIFF Languages - -Author: Peter Schrammel - -\*******************************************************************/ - -/// \file -/// JDIFF Languages - -#ifndef CPROVER_JDIFF_JDIFF_LANGUAGES_H -#define CPROVER_JDIFF_JDIFF_LANGUAGES_H - -#include -#include - -class jdiff_languagest : public language_uit -{ -public: - explicit jdiff_languagest( - const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler, - optionst *options) - : language_uit(cmdline, ui_message_handler, options) - { - register_languages(); - } - -protected: - virtual void register_languages(); -}; - -#endif // CPROVER_JDIFF_JDIFF_LANGUAGES_H diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index ea77117ae63..cb479013d9e 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -27,6 +27,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include @@ -60,28 +61,10 @@ Author: Peter Schrammel #include #include -// TODO: do not use language_uit for this; requires a refactoring of -// initialize_goto_model to support parsing specific command line files jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv) : parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler), - jdiff_languagest(cmdline, ui_message_handler, &options), - ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler, &options) -{ -} - -::jdiff_parse_optionst::jdiff_parse_optionst( - int argc, - const char **argv, - const std::string &extra_options) - : parse_options_baset( - JDIFF_OPTIONS + extra_options, - argc, - argv, - ui_message_handler), - jdiff_languagest(cmdline, ui_message_handler, &options), - ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler, &options) + messaget(ui_message_handler), + ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION) { } @@ -219,19 +202,21 @@ int jdiff_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - goto_modelt goto_model1, goto_model2; + register_languages(); - int get_goto_program_ret = get_goto_program(options, *this, goto_model1); - if(get_goto_program_ret != -1) - return get_goto_program_ret; - get_goto_program_ret = get_goto_program(options, languages2, goto_model2); - if(get_goto_program_ret != -1) - return get_goto_program_ret; + goto_modelt goto_model1 = + initialize_goto_model({cmdline.args[0]}, ui_message_handler, options); + if(process_goto_program(options, goto_model1)) + return CPROVER_EXIT_INTERNAL_ERROR; + goto_modelt goto_model2 = + initialize_goto_model({cmdline.args[1]}, ui_message_handler, options); + if(process_goto_program(options, goto_model2)) + return CPROVER_EXIT_INTERNAL_ERROR; if(cmdline.isset("show-loops")) { - show_loop_ids(get_ui(), goto_model1); - show_loop_ids(get_ui(), goto_model2); + show_loop_ids(ui_message_handler.get_ui(), goto_model1); + show_loop_ids(ui_message_handler.get_ui(), goto_model2); return CPROVER_EXIT_SUCCESS; } @@ -284,61 +269,6 @@ int jdiff_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } -int jdiff_parse_optionst::get_goto_program( - const optionst &options, - jdiff_languagest &languages, - goto_modelt &goto_model) -{ - status() << "Reading program from `" << cmdline.args[0] << "'" << eom; - - if(is_goto_binary(cmdline.args[0])) - { - auto tmp_goto_model = - read_goto_binary(cmdline.args[0], languages.get_message_handler()); - if(!tmp_goto_model.has_value()) - return CPROVER_EXIT_INCORRECT_TASK; - - goto_model = std::move(*tmp_goto_model); - - config.set(cmdline); - - // This one is done. - cmdline.args.erase(cmdline.args.begin()); - } - else - { - // This is a a workaround to make parse() think that there is only - // one source file. - std::string arg2(""); - if(cmdline.args.size() == 2) - { - arg2 = cmdline.args[1]; - cmdline.args.erase(--cmdline.args.end()); - } - - if(languages.parse() || languages.typecheck() || languages.final()) - return CPROVER_EXIT_INCORRECT_TASK; - - // we no longer need any parse trees or language files - languages.clear_parse(); - - status() << "Generating GOTO Program" << eom; - - goto_model.symbol_table = languages.symbol_table; - goto_convert( - goto_model.symbol_table, goto_model.goto_functions, ui_message_handler); - - if(process_goto_program(options, goto_model)) - return CPROVER_EXIT_INTERNAL_ERROR; - - // if we had a second argument then we will handle it next - if(arg2 != "") - cmdline.args[0] = arg2; - } - - return -1; // no error, continue -} - bool jdiff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index 653c2ff5352..ae22e684bbc 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -23,8 +23,6 @@ Author: Peter Schrammel #include #include -#include "jdiff_languages.h" - class goto_modelt; // clang-format off @@ -42,30 +40,20 @@ class goto_modelt; "(compact-output)" // clang-format on -class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest +class jdiff_parse_optionst : public parse_options_baset, public messaget { public: virtual int doit(); virtual void help(); jdiff_parse_optionst(int argc, const char **argv); - jdiff_parse_optionst( - int argc, - const char **argv, - const std::string &extra_options); protected: - optionst options; ui_message_handlert ui_message_handler; - jdiff_languagest languages2; + void register_languages(); void get_command_line_options(optionst &options); - virtual int get_goto_program( - const optionst &options, - jdiff_languagest &languages, - goto_modelt &goto_model); - bool process_goto_program(const optionst &options, goto_modelt &goto_model); };