From 4042fbb666e065ce23408d80ae1f2a36ea31e4b8 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Jul 2021 13:22:37 +0100 Subject: [PATCH 1/5] Correctly guard the use of the JSIL language --- src/goto-analyzer/goto_analyzer_parse_options.cpp | 7 ++++++- src/goto-cc/goto_cc_languages.cpp | 8 +++++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 8ba43feab03..4c0890722c8 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -24,7 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#ifdef HAVE_JSIL +# include +#endif #include #include @@ -69,7 +71,10 @@ void goto_analyzer_parse_optionst::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); + +#ifdef HAVE_JSIL register_language(new_jsil_language); +#endif } void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp index 3e0b56aeed4..7c3e06e5630 100644 --- a/src/goto-cc/goto_cc_languages.cpp +++ b/src/goto-cc/goto_cc_languages.cpp @@ -15,11 +15,17 @@ Author: CM Wintersteiger #include #include -#include + +#ifdef HAVE_JSIL +# include +#endif void goto_cc_modet::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); + +#ifdef HAVE_JSIL register_language(new_jsil_language); +#endif } From ff4797e0802a04a7b53224c011107fc65c7d17e8 Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Jul 2021 13:34:07 +0100 Subject: [PATCH 2/5] Separate out goto_analyzer's register_languages as with other tools --- src/goto-analyzer/Makefile | 3 +- src/goto-analyzer/goto_analyzer_languages.cpp | 31 +++++++++++++++++++ .../goto_analyzer_parse_options.cpp | 19 ------------ 3 files changed, 33 insertions(+), 20 deletions(-) create mode 100644 src/goto-analyzer/goto_analyzer_languages.cpp diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index a987fd38c6a..fc0aeb9b8fa 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -1,4 +1,5 @@ -SRC = goto_analyzer_main.cpp \ +SRC = goto_analyzer_languages.cpp \ + goto_analyzer_main.cpp \ goto_analyzer_parse_options.cpp \ taint_analysis.cpp \ taint_parser.cpp \ diff --git a/src/goto-analyzer/goto_analyzer_languages.cpp b/src/goto-analyzer/goto_analyzer_languages.cpp new file mode 100644 index 00000000000..2227340fe8e --- /dev/null +++ b/src/goto-analyzer/goto_analyzer_languages.cpp @@ -0,0 +1,31 @@ +/*******************************************************************\ + +Module: Language Registration + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +/// \file +/// Language Registration + +#include "goto_analyzer_parse_options.h" + +#include + +#include +#include + +#ifdef HAVE_JSIL +# include +#endif + +void goto_analyzer_parse_optionst::register_languages() +{ + register_language(new_ansi_c_language); + register_language(new_cpp_language); + +#ifdef HAVE_JSIL + register_language(new_jsil_language); +#endif +} diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4c0890722c8..d67aa7fbdf3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -16,18 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include -#include #include -#ifdef HAVE_JSIL -# include -#endif - #include #include #include @@ -39,9 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include - #include #include #include @@ -67,16 +58,6 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( { } -void goto_analyzer_parse_optionst::register_languages() -{ - register_language(new_ansi_c_language); - register_language(new_cpp_language); - -#ifdef HAVE_JSIL - register_language(new_jsil_language); -#endif -} - void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) { if(config.set(cmdline)) From d8c78b0d23fd5301037bca9cb5856195a7a52f9d Mon Sep 17 00:00:00 2001 From: martin Date: Fri, 9 Jul 2021 14:00:18 +0100 Subject: [PATCH 3/5] register_languages is now an interface not just a convention --- src/cbmc/cbmc_parse_options.h | 2 +- src/goto-analyzer/goto_analyzer_parse_options.h | 2 +- src/goto-diff/goto_diff_parse_options.h | 2 +- src/goto-harness/goto_harness_parse_options.cpp | 3 +++ src/goto-instrument/goto_instrument_parse_options.h | 2 +- .../memory_analyzer_parse_options.cpp | 9 ++++++++- src/memory-analyzer/memory_analyzer_parse_options.h | 2 ++ src/symtab2gb/symtab2gb_parse_options.cpp | 13 ++++++++++--- src/symtab2gb/symtab2gb_parse_options.h | 3 +++ src/util/parse_options.h | 4 ++++ 10 files changed, 34 insertions(+), 8 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 5c000c0e20b..04fa8985dc0 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -114,7 +114,7 @@ class cbmc_parse_optionst : public parse_options_baset protected: goto_modelt goto_model; - void register_languages(); + void register_languages() override; void get_command_line_options(optionst &); void preprocessing(const optionst &); bool set_properties(); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 0f8fa95ca72..3dea9c5e951 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -183,7 +183,7 @@ class goto_analyzer_parse_optionst: public parse_options_baset protected: goto_modelt goto_model; - virtual void register_languages(); + void register_languages() override; virtual void get_command_line_options(optionst &options); diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 88adb6bb6dc..64e30e0d8ea 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -49,7 +49,7 @@ class goto_diff_parse_optionst : public parse_options_baset goto_diff_parse_optionst(int argc, const char **argv); protected: - void register_languages(); + void register_languages() override; void get_command_line_options(optionst &options); diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index edde376dfb1..cf3d26687ee 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -108,6 +108,9 @@ int goto_harness_parse_optionst::doit() // This just sets up the defaults (and would interpret options such as --32). config.set(cmdline); + // Normally we would register language front-ends here but as goto-harness + // only works on goto binaries, we don't need to + // Read goto binary into goto-model auto read_goto_binary_result = read_goto_binary(got_harness_config.in_file, ui_message_handler); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5ce7b72d273..3d1e79c8a0a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -145,7 +145,7 @@ class goto_instrument_parse_optionst : public parse_options_baset } protected: - void register_languages(); + void register_languages() override; void get_goto_program(); void instrument_goto_program(); diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp index e58a04c53d9..3e6b93d5dc9 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.cpp +++ b/src/memory-analyzer/memory_analyzer_parse_options.cpp @@ -42,6 +42,13 @@ memory_analyzer_parse_optionst::memory_analyzer_parse_optionst( { } +void memory_analyzer_parse_optionst::register_languages() +{ + // For now only C is supported due to the additional challenges of + // mapping source code to debugging symbols in other languages. + register_language(new_ansi_c_language); +} + int memory_analyzer_parse_optionst::doit() { if(cmdline.isset("version")) @@ -91,7 +98,7 @@ int memory_analyzer_parse_optionst::doit() "--symtab-snapshot"); } - register_language(new_ansi_c_language); + register_languages(); std::string binary = cmdline.args.front(); diff --git a/src/memory-analyzer/memory_analyzer_parse_options.h b/src/memory-analyzer/memory_analyzer_parse_options.h index 37132791a12..9250add523f 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.h +++ b/src/memory-analyzer/memory_analyzer_parse_options.h @@ -37,6 +37,8 @@ class memory_analyzer_parse_optionst : public parse_options_baset protected: messaget message; + + void register_languages() override; }; #endif // CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index d8d9f3568e6..519d52670e6 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -96,6 +96,15 @@ static void run_symtab2gb( } } +void symtab2gb_parse_optionst::register_languages() +{ + // As this is a converter and linker it only really needs to support + // the JSON symtab front-end. + register_language(new_json_symtab_language); + // Workaround to allow external front-ends to use "C" mode + register_language(new_ansi_c_language); +} + int symtab2gb_parse_optionst::doit() { if(cmdline.isset("version")) @@ -114,9 +123,7 @@ int symtab2gb_parse_optionst::doit() { gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT); } - register_language(new_json_symtab_language); - // Workaround to allow external front-ends to use "C" mode - register_language(new_ansi_c_language); + register_languages(); config.set(cmdline); run_symtab2gb(symtab_filenames, gb_filename); return CPROVER_EXIT_SUCCESS; diff --git a/src/symtab2gb/symtab2gb_parse_options.h b/src/symtab2gb/symtab2gb_parse_options.h index 546af8bb085..c01378479d2 100644 --- a/src/symtab2gb/symtab2gb_parse_options.h +++ b/src/symtab2gb/symtab2gb_parse_options.h @@ -27,6 +27,9 @@ class symtab2gb_parse_optionst : public parse_options_baset symtab2gb_parse_optionst(int argc, const char *argv[]); void help() override; int doit() override; + +protected: + void register_languages() override; }; #endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H diff --git a/src/util/parse_options.h b/src/util/parse_options.h index d446a1c1e7d..5d27d5ec8a2 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -45,6 +45,10 @@ class parse_options_baset ui_message_handlert ui_message_handler; messaget log; + virtual void register_languages() + { + } + private: void unknown_option_msg(); }; From b16a5fc8a99efe08f1e307ecadae6b466cb3d41d Mon Sep 17 00:00:00 2001 From: martin Date: Sun, 11 Jul 2021 11:45:44 +0100 Subject: [PATCH 4/5] Make sure that member functions are correctly marked as override It seems that adding one override to a class triggers clang's override check. --- src/goto-diff/goto_diff_parse_options.h | 4 ++-- src/goto-instrument/goto_instrument_parse_options.h | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 64e30e0d8ea..94cca0f2463 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -43,8 +43,8 @@ class optionst; class goto_diff_parse_optionst : public parse_options_baset { public: - virtual int doit(); - virtual void help(); + int doit() override; + void help() override; goto_diff_parse_optionst(int argc, const char **argv); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 3d1e79c8a0a..d76c59c215d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -129,8 +129,8 @@ Author: Daniel Kroening, kroening@kroening.com class goto_instrument_parse_optionst : public parse_options_baset { public: - virtual int doit(); - virtual void help(); + int doit() override; + void help() override; goto_instrument_parse_optionst(int argc, const char **argv) : parse_options_baset( From 021116b078626d06805d7067b72d32eef0acb676 Mon Sep 17 00:00:00 2001 From: martin Date: Sun, 11 Jul 2021 13:26:24 +0100 Subject: [PATCH 5/5] Add override to register_languages in the Java tools --- jbmc/src/janalyzer/janalyzer_parse_options.h | 6 +++--- jbmc/src/jdiff/jdiff_parse_options.h | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h index b43bdcff6ba..539ac4cae9f 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.h +++ b/jbmc/src/janalyzer/janalyzer_parse_options.h @@ -154,8 +154,8 @@ class optionst; class janalyzer_parse_optionst : public parse_options_baset { public: - virtual int doit() override; - virtual void help() override; + int doit() override; + void help() override; janalyzer_parse_optionst(int argc, const char **argv); @@ -177,7 +177,7 @@ class janalyzer_parse_optionst : public parse_options_baset protected: std::unique_ptr class_hierarchy; - void register_languages(); + void register_languages() override; void get_command_line_options(optionst &options); diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index a38f9b2601e..6a151144457 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -42,13 +42,13 @@ class goto_modelt; class jdiff_parse_optionst : public parse_options_baset { public: - virtual int doit(); - virtual void help(); + int doit() override; + void help() override; jdiff_parse_optionst(int argc, const char **argv); protected: - void register_languages(); + void register_languages() override; void get_command_line_options(optionst &options);