From 5b467d13676fe6070c4dd41a5d3a06ae220c272c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 6 Oct 2018 22:26:16 +0100 Subject: [PATCH] Do not bypass options when parsing language cmdline --- .../src/janalyzer/janalyzer_parse_options.cpp | 4 +- jbmc/src/java_bytecode/Makefile | 1 + .../java_bytecode/java_bytecode_language.cpp | 131 +++++++++++------- .../java_bytecode/java_bytecode_language.h | 6 +- .../java_bytecode/java_class_loader_limit.cpp | 5 +- .../object_factory_parameters.cpp | 71 ++++++++++ .../java_bytecode/object_factory_parameters.h | 8 ++ jbmc/src/jbmc/jbmc_parse_options.cpp | 30 ++-- jbmc/src/jdiff/jdiff_languages.h | 5 +- jbmc/src/jdiff/jdiff_parse_options.cpp | 11 +- jbmc/src/jdiff/jdiff_parse_options.h | 3 +- .../java-testing-utils/load_java_class.cpp | 6 +- .../module_dependencies.txt | 1 + .../parse_java_annotations.cpp | 5 +- .../custom_value_set_analysis.cpp | 5 +- src/cbmc/cbmc_parse_options.cpp | 10 +- src/cbmc/cbmc_parse_options.h | 2 +- .../goto_analyzer_parse_options.cpp | 2 +- src/goto-programs/initialize_goto_model.cpp | 11 +- src/goto-programs/initialize_goto_model.h | 10 +- src/goto-programs/lazy_goto_model.cpp | 8 +- src/goto-programs/lazy_goto_model.h | 2 +- .../rebuild_goto_start_function.cpp | 16 +-- .../rebuild_goto_start_function.h | 6 +- src/langapi/language.h | 8 +- src/langapi/language_ui.cpp | 12 +- src/langapi/language_ui.h | 4 +- 27 files changed, 259 insertions(+), 124 deletions(-) create mode 100644 jbmc/src/java_bytecode/object_factory_parameters.cpp diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 43a40bcc6c9..5d25af30b4c 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -77,6 +77,8 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + parse_java_language_options(cmdline, options); + // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -350,7 +352,7 @@ int janalyzer_parse_optionst::doit() try { - goto_model = initialize_goto_model(cmdline, get_message_handler()); + goto_model = initialize_goto_model(cmdline, get_message_handler(), options); } catch(const char *e) diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 1a98ac1968a..4735583b0b0 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -35,6 +35,7 @@ SRC = bytecode_info.cpp \ java_types.cpp \ java_utils.cpp \ load_method_by_regex.cpp \ + object_factory_parameters.cpp \ mz_zip_archive.cpp \ remove_exceptions.cpp \ remove_instanceof.cpp \ diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index f688674cfd4..0e7860469c7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -10,14 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include -#include #include +#include #include +#include #include +#include #include -#include +#include +#include + #include #include @@ -39,45 +41,71 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2java.h" #include "load_method_by_regex.h" -/// Consume options that are java bytecode specific. -/// \param Command:line options -/// \return None -void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) +/// Parse options that are java bytecode specific. +/// \param cmd Command line +/// \param [out] options The options object that will be updated. +void parse_java_language_options(const cmdlinet &cmd, optionst &options) { - assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); - string_refinement_enabled = !cmd.isset("no-refine-strings"); - throw_runtime_exceptions = cmd.isset("throw-runtime-exceptions"); - assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check"); - throw_assertion_error = cmd.isset("throw-assertion-error"); - threading_support = cmd.isset("java-threading"); - - if(cmd.isset("max-nondet-array-length")) + options.set_option( + "java-assume-inputs-non-null", cmd.isset("java-assume-inputs-non-null")); + options.set_option( + "throw-runtime-exceptions", cmd.isset("throw-runtime-exceptions")); + options.set_option( + "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check")); + options.set_option( + "throw-assertion-error", cmd.isset("throw-assertion-error")); + options.set_option("java-threading", cmd.isset("java-threading")); + + if(cmd.isset("java-max-vla-length")) { - object_factory_parameters.max_nondet_array_length = - safe_string2size_t(cmd.get_value("max-nondet-array-length")); + options.set_option( + "java-max-vla-length", cmd.get_value("java-max-vla-length")); } - if(cmd.isset("max-nondet-tree-depth")) + options.set_option( + "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading")); + + if(cmd.isset("java-load-class")) + options.set_option("java-load-class", cmd.get_values("java-load-class")); + + if(cmd.isset("java-no-load-class")) { - object_factory_parameters.max_nondet_tree_depth = - safe_string2size_t(cmd.get_value("max-nondet-tree-depth")); + options.set_option( + "java-no-load-class", cmd.get_values("java-no-load-class")); } - - if(cmd.isset("max-nondet-string-length")) + if(cmd.isset("lazy-methods-extra-entry-point")) + { + options.set_option( + "lazy-methods-extra-entry-point", + cmd.get_values("lazy-methods-extra-entry-point")); + } + if(cmd.isset("java-cp-include-files")) { - object_factory_parameters.max_nondet_string_length = - safe_string2size_t(cmd.get_value("max-nondet-string-length")); + options.set_option( + "java-cp-include-files", cmd.get_value("java-cp-include-files")); } - if(cmd.isset("string-non-empty")) - object_factory_parameters.min_nondet_string_length = 1; +} - object_factory_parameters.string_printable = cmd.isset("string-printable"); - if(cmd.isset("java-max-vla-length")) - max_user_array_length = - safe_string2size_t(cmd.get_value("java-max-vla-length")); - if(cmd.isset("symex-driven-lazy-loading")) +/// Consume options that are java bytecode specific. +void java_bytecode_languaget::set_language_options(const optionst &options) +{ + object_factory_parameters.set(options); + + assume_inputs_non_null = + options.get_bool_option("java-assume-inputs-non-null"); + string_refinement_enabled = options.get_bool_option("refine-strings"); + throw_runtime_exceptions = + options.get_bool_option("throw-runtime-exceptions"); + assert_uncaught_exceptions = + options.get_bool_option("uncaught-exception-check"); + throw_assertion_error = options.get_bool_option("throw-assertion-error"); + threading_support = options.get_bool_option("java-threading"); + max_user_array_length = + options.get_unsigned_int_option("java-max-vla-length"); + + if(options.get_bool_option("symex-driven-lazy-loading")) lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER; - else if(!cmd.isset("no-lazy-methods")) + else if(options.get_bool_option("lazy-methods")) lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE; else lazy_methods_mode=LAZY_METHODS_MODE_EAGER; @@ -85,36 +113,36 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) if(throw_runtime_exceptions) { java_load_classes.insert( - java_load_classes.end(), - exception_needed_classes.begin(), - exception_needed_classes.end()); + java_load_classes.end(), + exception_needed_classes.begin(), + exception_needed_classes.end()); } - if(cmd.isset("java-load-class")) + + if(options.is_set("java-load-class")) { - const auto &values = cmd.get_values("java-load-class"); + const auto &load_values = options.get_list_option("java-load-class"); java_load_classes.insert( - java_load_classes.end(), values.begin(), values.end()); + java_load_classes.end(), load_values.begin(), load_values.end()); } - if(cmd.isset("java-no-load-class")) + if(options.is_set("java-no-load-class")) { - const auto &values = cmd.get_values("java-no-load-class"); - no_load_classes = {values.begin(), values.end()}; + const auto &no_load_values = options.get_list_option("java-no-load-class"); + no_load_classes = {no_load_values.begin(), no_load_values.end()}; } - - const std::list &extra_entry_points= - cmd.get_values("lazy-methods-extra-entry-point"); + const std::list &extra_entry_points = + options.get_list_option("lazy-methods-extra-entry-point"); std::transform( extra_entry_points.begin(), extra_entry_points.end(), std::back_inserter(extra_methods), build_load_method_by_regex); - const auto &new_points = build_extra_entry_points(cmd); + const auto &new_points = build_extra_entry_points(options); extra_methods.insert( extra_methods.end(), new_points.begin(), new_points.end()); - if(cmd.isset("java-cp-include-files")) + java_cp_include_files = options.get_option("java-cp-include-files"); + if(!java_cp_include_files.empty()) { - java_cp_include_files=cmd.get_value("java-cp-include-files"); // load file list from JSON file if(java_cp_include_files[0]=='@') { @@ -129,7 +157,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) throw "the JSON file has a wrong format"; jsont include_files=json_cp_config["jar"]; if(!include_files.is_array()) - throw "the JSON file has a wrong format"; + throw "the JSON file has a wrong format"; // add jars from JSON config file to classpath for(const jsont &file_entry : include_files.array) @@ -145,7 +173,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) else java_cp_include_files=".*"; - nondet_static = cmd.isset("nondet-static"); + nondet_static = options.get_bool_option("nondet-static"); language_options_initialized=true; } @@ -1219,8 +1247,7 @@ java_bytecode_languaget::~java_bytecode_languaget() /// specifying extra entry points. To provide a regex entry point, the command /// line option `--lazy-methods-extra-entry-point` can be used directly. std::vector -java_bytecode_languaget::build_extra_entry_points( - const cmdlinet &command_line) const +java_bytecode_languaget::build_extra_entry_points(const optionst &options) const { return {}; } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index cd428390f74..08980a1c70c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -88,7 +88,7 @@ enum lazy_methods_modet class java_bytecode_languaget:public languaget { public: - virtual void get_language_options(const cmdlinet &) override; + void set_language_options(const optionst &) override; virtual bool preprocess( std::istream &instream, @@ -196,7 +196,7 @@ class java_bytecode_languaget:public languaget private: virtual std::vector - build_extra_entry_points(const cmdlinet &command_line) const; + build_extra_entry_points(const optionst &) const; const std::unique_ptr pointer_type_selector; /// Maps synthetic method names on to the particular type of synthetic method @@ -213,4 +213,6 @@ class java_bytecode_languaget:public languaget std::unique_ptr new_java_bytecode_language(); +void parse_java_language_options(const cmdlinet &cmd, optionst &options); + #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H diff --git a/jbmc/src/java_bytecode/java_class_loader_limit.cpp b/jbmc/src/java_bytecode/java_class_loader_limit.cpp index f25e84fe7cf..71f258ad4ce 100644 --- a/jbmc/src/java_bytecode/java_class_loader_limit.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_limit.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + /// Initializes class with either regex matcher or match set. If the string /// starts with an `@` it is treated as a path to a JSON file. Otherwise, it is /// treated as a regex. @@ -48,8 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com void java_class_loader_limitt::setup_class_load_limit( const std::string &java_cp_include_files) { - if(java_cp_include_files.empty()) - throw "class regexp cannot be empty, `get_language_options` not called?"; + PRECONDITION(!java_cp_include_files.empty()); // '@' signals file reading with list of class files to load use_regex_match = java_cp_include_files[0] != '@'; diff --git a/jbmc/src/java_bytecode/object_factory_parameters.cpp b/jbmc/src/java_bytecode/object_factory_parameters.cpp new file mode 100644 index 00000000000..85d7dce4887 --- /dev/null +++ b/jbmc/src/java_bytecode/object_factory_parameters.cpp @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: Java Object Factory + +Author: Diffblue Ltd + +\*******************************************************************/ + +#include "object_factory_parameters.h" + +#include +#include + +void object_factory_parameterst::set(const optionst &options) +{ + if(options.is_set("max-nondet-array-length")) + { + max_nondet_array_length = + options.get_unsigned_int_option("max-nondet-array-length"); + } + if(options.is_set("max-nondet-tree-depth")) + { + max_nondet_tree_depth = + options.get_unsigned_int_option("max-nondet-tree-depth"); + } + if(options.is_set("max-nondet-string-length")) + { + max_nondet_string_length = + options.get_unsigned_int_option("max-nondet-string-length"); + } + if(options.is_set("string-printable")) + { + string_printable = options.get_bool_option("string-printable"); + } + if(options.is_set("min-nondet-string-length")) + { + min_nondet_string_length = + options.get_unsigned_int_option("min-nondet-string-length"); + } +} + +/// Parse the object factory parameters from a given command line +/// \param cmdline Command line +/// \param [out] options The options object that will be updated. +void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) +{ + if(cmdline.isset("max-nondet-array-length")) + { + options.set_option( + "max-nondet-array-length", cmdline.get_value("max-nondet-array-length")); + } + if(cmdline.isset("max-nondet-tree-depth")) + { + options.set_option( + "max-nondet-tree-depth", cmdline.get_value("max-nondet-tree-depth")); + } + if(cmdline.isset("max-nondet-string-length")) + { + options.set_option( + "max-nondet-string-length", + cmdline.get_value("max-nondet-string-length")); + } + if(cmdline.isset("string-printable")) + { + options.set_option("string-printable", cmdline.isset("string-printable")); + } + if(cmdline.isset("string-non-empty")) + { + options.set_option("min-nondet-string-length", 1); + } +} diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h index 838e5ed0b6a..991f944d90d 100644 --- a/jbmc/src/java_bytecode/object_factory_parameters.h +++ b/jbmc/src/java_bytecode/object_factory_parameters.h @@ -14,6 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +class cmdlinet; +class optionst; + #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 #define MAX_NONDET_STRING_LENGTH \ static_cast(std::numeric_limits::max()) @@ -56,6 +59,11 @@ struct object_factory_parameterst final /// Function id, used as a prefix for identifiers of temporaries irep_idt function_id; + + /// Assigns the parameters from given options + void set(const optionst &); }; +void parse_object_factory_options(const cmdlinet &, optionst &); + #endif diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 56d68cba1d3..5a2a499eb07 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -86,6 +86,7 @@ void jbmc_parse_optionst::set_default_options(optionst &options) options.set_option("assertions", true); options.set_option("assumptions", true); options.set_option("built-in-assertions", true); + options.set_option("lazy-methods", true); options.set_option("pretty-names", true); options.set_option("propagation", true); options.set_option("refine-strings", true); @@ -106,6 +107,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) } jbmc_parse_optionst::set_default_options(options); + parse_java_language_options(cmdline, options); + parse_object_factory_options(cmdline, options); if(cmdline.isset("show-symex-strategies")) { @@ -349,6 +352,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) PARSE_OPTIONS_GOTO_TRACE(cmdline, options); + if(cmdline.isset("no-lazy-methods")) + options.set_option("lazy-methods", false); + if(cmdline.isset("symex-driven-lazy-loading")) { options.set_option("symex-driven-lazy-loading", true); @@ -452,7 +458,7 @@ int jbmc_parse_optionst::doit() return 6; } - language->get_language_options(cmdline); + language->set_language_options(options); language->set_message_handler(get_message_handler()); status() << "Parsing " << filename << eom; @@ -483,20 +489,10 @@ int jbmc_parse_optionst::doit() }; } - object_factory_params.max_nondet_array_length = - cmdline.isset("max-nondet-array-length") - ? std::stoul(cmdline.get_value("max-nondet-array-length")) - : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - object_factory_params.max_nondet_string_length = - cmdline.isset("max-nondet-string-length") - ? std::stoul(cmdline.get_value("max-nondet-string-length")) - : MAX_NONDET_STRING_LENGTH; - object_factory_params.max_nondet_tree_depth = - cmdline.isset("max-nondet-tree-depth") - ? std::stoul(cmdline.get_value("max-nondet-tree-depth")) - : MAX_NONDET_TREE_DEPTH; - - stub_objects_are_not_null = cmdline.isset("java-assume-inputs-non-null"); + object_factory_params.set(options); + + stub_objects_are_not_null = + options.get_bool_option("java-assume-inputs-non-null"); if(!cmdline.isset("symex-driven-lazy-loading")) { @@ -531,7 +527,7 @@ int jbmc_parse_optionst::doit() // Use symex-driven lazy loading: lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object( *this, options, get_message_handler()); - lazy_goto_model.initialize(cmdline); + lazy_goto_model.initialize(cmdline, options); // The precise wording of this error matches goto-symex's complaint when no // __CPROVER_start exists (if we just go ahead and run it anyway it will @@ -608,7 +604,7 @@ int jbmc_parse_optionst::get_goto_program( { lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object( *this, options, get_message_handler()); - lazy_goto_model.initialize(cmdline); + lazy_goto_model.initialize(cmdline, options); // Show the class hierarchy if(cmdline.isset("show-class-hierarchy")) diff --git a/jbmc/src/jdiff/jdiff_languages.h b/jbmc/src/jdiff/jdiff_languages.h index 6cee4feabc4..22df0df0acd 100644 --- a/jbmc/src/jdiff/jdiff_languages.h +++ b/jbmc/src/jdiff/jdiff_languages.h @@ -20,8 +20,9 @@ class jdiff_languagest : public language_uit public: explicit jdiff_languagest( const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler) - : language_uit(cmdline, ui_message_handler) + ui_message_handlert &ui_message_handler, + optionst *options) + : language_uit(cmdline, ui_message_handler, options) { register_languages(); } diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 6464c51c7e3..2febeea897b 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -61,11 +61,13 @@ 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), - jdiff_languagest(cmdline, ui_message_handler), + jdiff_languagest(cmdline, ui_message_handler, &options), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler) + languages2(cmdline, ui_message_handler, &options) { } @@ -74,9 +76,9 @@ ::jdiff_parse_optionst::jdiff_parse_optionst( const char **argv, const std::string &extra_options) : parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv), - jdiff_languagest(cmdline, ui_message_handler), + jdiff_languagest(cmdline, ui_message_handler, &options), ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION), - languages2(cmdline, ui_message_handler) + languages2(cmdline, ui_message_handler, &options) { } @@ -93,6 +95,7 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options) // we always require these options cmdline.set("no-lazy-methods"); cmdline.set("no-refine-strings"); + parse_java_language_options(cmdline, options); if(cmdline.isset("cover")) parse_cover_options(cmdline, options); diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h index e562e55a833..e56f44633ee 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.h +++ b/jbmc/src/jdiff/jdiff_parse_options.h @@ -14,6 +14,7 @@ Author: Peter Schrammel #include +#include #include #include #include @@ -25,7 +26,6 @@ Author: Peter Schrammel #include "jdiff_languages.h" class goto_modelt; -class optionst; // clang-format off #define JDIFF_OPTIONS \ @@ -55,6 +55,7 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest const std::string &extra_options); protected: + optionst options; ui_message_handlert ui_message_handler; jdiff_languagest languages2; diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index f79676ee6e4..9604db8c2e2 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -14,6 +14,7 @@ #include #include +#include #include #include @@ -119,9 +120,12 @@ goto_modelt load_goto_model_from_java_class( std::istringstream java_code_stream("ignored"); + optionst options; + parse_java_language_options(command_line, options); + // Configure the language, load the class files language.set_message_handler(null_message_handler); - language.get_language_options(command_line); + language.set_language_options(options); language.parse(java_code_stream, filename); language.typecheck(lazy_goto_model.symbol_table, ""); language.generate_support_functions(lazy_goto_model.symbol_table); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt index 87cf9849bbf..4cbf833a097 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/module_dependencies.txt @@ -1,3 +1,4 @@ java-testing-utils testing-utils java_bytecode +util diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp index 81f448c2e1c..cc8c5014fc2 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp @@ -14,6 +14,7 @@ #include #include #include +#include class test_java_bytecode_languaget : public java_bytecode_languaget { @@ -173,7 +174,9 @@ SCENARIO( command_line.add_flag("no-refine-strings"); test_java_bytecode_languaget language; language.set_message_handler(null_message_handler); - language.get_language_options(command_line); + optionst options; + parse_java_language_options(command_line, options); + language.set_language_options(options); std::istringstream java_code_stream("ignored"); language.parse(java_code_stream, "AnnotationsEverywhere.class"); diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 4ce2e21c530..63ff199194a 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -17,6 +17,7 @@ Author: Chris Smowton, chris@smowton.net #include #include #include +#include /// An example customised value_sett. It makes a series of small changes /// to the underlying value_sett logic, which can then be verified by the @@ -180,9 +181,11 @@ SCENARIO("test_value_set_analysis", command_line.args.push_back("pointer-analysis/CustomVSATest.jar"); register_language(new_java_bytecode_language); + optionst options; + parse_java_language_options(command_line, options); goto_modelt goto_model = - initialize_goto_model(command_line, null_message_handler); + initialize_goto_model(command_line, null_message_handler, options); null_message_handlert message_handler; remove_java_new(goto_model, message_handler); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 1ff75f37070..2758996ba18 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -457,7 +457,7 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("preprocess")) { - preprocessing(); + preprocessing(options); return CPROVER_EXIT_SUCCESS; } @@ -495,7 +495,7 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - language->get_language_options(cmdline); + language->set_language_options(options); language->set_message_handler(get_message_handler()); status() << "Parsing " << filename << eom; @@ -578,7 +578,7 @@ int cbmc_parse_optionst::get_goto_program( try { - goto_model = initialize_goto_model(cmdline, ui_message_handler); + goto_model = initialize_goto_model(cmdline, ui_message_handler, options); if(cmdline.isset("show-symbol-table")) { @@ -645,7 +645,7 @@ int cbmc_parse_optionst::get_goto_program( return -1; // no error, continue } -void cbmc_parse_optionst::preprocessing() +void cbmc_parse_optionst::preprocessing(const optionst &options) { try { @@ -666,7 +666,7 @@ void cbmc_parse_optionst::preprocessing() } std::unique_ptr language=get_language_from_filename(filename); - language->get_language_options(cmdline); + language->set_language_options(options); if(language==nullptr) { diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index fcc207ffb20..c8ace68078c 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -112,7 +112,7 @@ class cbmc_parse_optionst: void register_languages(); void get_command_line_options(optionst &); - void preprocessing(); + void preprocessing(const optionst &); bool set_properties(); }; diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2108bccc248..9f92fa1c653 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -377,7 +377,7 @@ int goto_analyzer_parse_optionst::doit() try { - goto_model=initialize_goto_model(cmdline, get_message_handler()); + goto_model = initialize_goto_model(cmdline, get_message_handler(), options); } catch(const char *e) diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 73cc28ac366..4478dd7d856 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include +#include #include #include @@ -27,7 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com goto_modelt initialize_goto_model( const cmdlinet &cmdline, - message_handlert &message_handler) + message_handlert &message_handler, + const optionst &options) { messaget msg(message_handler); const std::vector &files=cmdline.args; @@ -85,7 +88,7 @@ goto_modelt initialize_goto_model( languaget &language=*lf.language; language.set_message_handler(message_handler); - language.get_language_options(cmdline); + language.set_language_options(options); msg.status() << "Parsing " << filename << messaget::eom; @@ -125,9 +128,7 @@ goto_modelt initialize_goto_model( // Rebuild the entry-point, using the language annotation of the // existing __CPROVER_start function: rebuild_goto_start_functiont rebuild_existing_start( - cmdline, - goto_model, - msg.get_message_handler()); + options, goto_model, msg.get_message_handler()); entry_point_generation_failed=rebuild_existing_start(); } else if(!binaries_provided_start) diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h index e6126d55af6..e063beeadfa 100644 --- a/src/goto-programs/initialize_goto_model.h +++ b/src/goto-programs/initialize_goto_model.h @@ -12,13 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H #define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H -#include -#include - #include "goto_model.h" +class cmdlinet; +class message_handlert; +class optionst; + goto_modelt initialize_goto_model( const cmdlinet &cmdline, - message_handlert &message_handler); + message_handlert &message_handler, + const optionst &options); #endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 90fcaaacf87..39a4b33fbb0 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -87,7 +87,9 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) } //! @endcond -void lazy_goto_modelt::initialize(const cmdlinet &cmdline) +void lazy_goto_modelt::initialize( + const cmdlinet &cmdline, + const optionst &options) { messaget msg(message_handler); @@ -141,7 +143,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) languaget &language=*lf.language; language.set_message_handler(message_handler); - language.get_language_options(cmdline); + language.set_language_options(options); msg.status() << "Parsing " << filename << messaget::eom; @@ -181,7 +183,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) // Rebuild the entry-point, using the language annotation of the // existing __CPROVER_start function: rebuild_lazy_goto_start_functiont rebuild_existing_start( - cmdline, *this, message_handler); + options, *this, message_handler); entry_point_generation_failed=rebuild_existing_start(); } else if(!binaries_provided_start) diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index ed2037dee6d..efba4c2dbce 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -82,7 +82,7 @@ class lazy_goto_modelt : public abstract_goto_modelt message_handler); } - void initialize(const cmdlinet &cmdline); + void initialize(const cmdlinet &cmdline, const optionst &options); /// Eagerly loads all functions from the symbol table. void load_all_functions() const; diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index e785dd95343..caee26f6757 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -24,15 +24,13 @@ /// function) and symbol table (to replace the _start function symbol) of the /// program. /// \param _message_handler: The message handler to report any messages with -template +template rebuild_goto_start_function_baset:: -rebuild_goto_start_function_baset( - const cmdlinet &cmdline, - maybe_lazy_goto_modelt &goto_model, - message_handlert &message_handler): - messaget(message_handler), - cmdline(cmdline), - goto_model(goto_model) + rebuild_goto_start_function_baset( + const optionst &options, + maybe_lazy_goto_modelt &goto_model, + message_handlert &message_handler) + : messaget(message_handler), options(options), goto_model(goto_model) { } @@ -53,7 +51,7 @@ bool rebuild_goto_start_function_baset::operator()() std::unique_ptr language=get_language_from_mode(mode); INVARIANT(language, "No language found for mode: "+id2string(mode)); language->set_message_handler(get_message_handler()); - language->get_language_options(cmdline); + language->set_language_options(options); // To create a new entry point we must first remove the old one remove_existing_entry_point(); diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h index 8d5ad9f8fbe..27a0e2d42df 100644 --- a/src/goto-programs/rebuild_goto_start_function.h +++ b/src/goto-programs/rebuild_goto_start_function.h @@ -10,7 +10,7 @@ #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H #include -class cmdlinet; +class optionst; #include "lazy_goto_model.h" @@ -29,7 +29,7 @@ class rebuild_goto_start_function_baset: public messaget { public: rebuild_goto_start_function_baset( - const cmdlinet &cmdline, + const optionst &options, maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler); @@ -40,7 +40,7 @@ class rebuild_goto_start_function_baset: public messaget void remove_existing_entry_point(); - const cmdlinet &cmdline; + const optionst &options; maybe_lazy_goto_modelt &goto_model; }; diff --git a/src/langapi/language.h b/src/langapi/language.h index 9e35daa17c9..b9cdb4c50d3 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -27,8 +27,8 @@ class symbol_tablet; class symbol_table_baset; class exprt; class namespacet; +class optionst; class typet; -class cmdlinet; #define OPT_FUNCTIONS \ "(function):" @@ -39,8 +39,10 @@ class cmdlinet; class languaget:public messaget { public: - // Parse language-specific options - virtual void get_language_options(const cmdlinet &) {} + /// Set language-specific options + virtual void set_language_options(const optionst &) + { + } // parse file diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 85b0371fbe6..2513d96c30f 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -23,9 +23,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// Constructor language_uit::language_uit( const cmdlinet &cmdline, - ui_message_handlert &_ui_message_handler): - _cmdline(cmdline), - ui_message_handler(_ui_message_handler) + ui_message_handlert &_ui_message_handler, + optionst *_options) + : _cmdline(cmdline), + ui_message_handler(_ui_message_handler), + options(_options) { set_message_handler(ui_message_handler); } @@ -72,7 +74,9 @@ bool language_uit::parse(const std::string &filename) languaget &language=*lf.language; language.set_message_handler(get_message_handler()); - language.get_language_options(_cmdline); + + if(options != nullptr) + language.set_language_options(*options); status() << "Parsing " << filename << eom; diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 44760c06648..35ebf0852d5 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -26,7 +26,8 @@ class language_uit:public messaget language_uit( const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler); + ui_message_handlert &ui_message_handler, + optionst *options = nullptr); virtual ~language_uit(); virtual bool parse(); @@ -53,6 +54,7 @@ class language_uit:public messaget protected: const cmdlinet &_cmdline; ui_message_handlert &ui_message_handler; + optionst *options; }; #endif // CPROVER_LANGAPI_LANGUAGE_UI_H