From cd90c7ddae24d22bc87eccb82084b8cb544e74d4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 3 Dec 2018 00:24:35 +0000 Subject: [PATCH 1/2] Remove cmdlinet from init/lazy_goto_model It should be possible to build a goto model without requiring a cmdlinet, e.g. in unit tests. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 6 +++++- jbmc/src/jbmc/jbmc_parse_options.cpp | 8 ++++++-- .../pointer-analysis/custom_value_set_analysis.cpp | 12 +++++------- src/cbmc/cbmc_parse_options.cpp | 11 ++++++++++- src/goto-analyzer/goto_analyzer_parse_options.cpp | 11 ++++++++++- src/goto-programs/initialize_goto_model.cpp | 11 +++++------ src/goto-programs/initialize_goto_model.h | 3 +-- src/goto-programs/lazy_goto_model.cpp | 12 +++++------- src/goto-programs/lazy_goto_model.h | 6 +++--- src/langapi/language_ui.cpp | 9 +++++++-- 10 files changed, 57 insertions(+), 32 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 1480391ef3a..d4845f12489 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -77,6 +77,9 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + if(cmdline.isset("function")) + options.set_option("function", cmdline.get_value("function")); + parse_java_language_options(cmdline, options); // check assertions @@ -352,7 +355,8 @@ int janalyzer_parse_optionst::doit() try { - goto_model = initialize_goto_model(cmdline, get_message_handler(), options); + goto_model = + initialize_goto_model(cmdline.args, get_message_handler(), options); } catch(const char *e) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ac6487e3dea..5a9ce86259b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -108,6 +108,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) } jbmc_parse_optionst::set_default_options(options); + + if(cmdline.isset("function")) + options.set_option("function", cmdline.get_value("function")); + parse_java_language_options(cmdline, options); parse_java_object_factory_options(cmdline, options); @@ -550,7 +554,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, options); + lazy_goto_model.initialize(cmdline.args, options); class_hierarchy = util_make_unique(lazy_goto_model.symbol_table); @@ -630,7 +634,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, options); + lazy_goto_model.initialize(cmdline.args, options); class_hierarchy = util_make_unique(lazy_goto_model.symbol_table); diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 6423212d269..c4785c8347c 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -172,20 +172,18 @@ SCENARIO("test_value_set_analysis", { config.set_arch("none"); config.main = ""; - cmdlinet command_line; // This classpath is the default, but the config object // is global and previous unit tests may have altered it - command_line.set("java-cp-include-files", "CustomVSATest.class"); config.java.classpath={"."}; - command_line.args.push_back("pointer-analysis/CustomVSATest.jar"); - register_language(new_java_bytecode_language); optionst options; - parse_java_language_options(command_line, options); + options.set_option("java-cp-include-files", "CustomVSATest.class"); + + register_language(new_java_bytecode_language); - goto_modelt goto_model = - initialize_goto_model(command_line, null_message_handler, options); + goto_modelt goto_model = initialize_goto_model( + {"pointer-analysis/CustomVSATest.jar"}, 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 8b01624d82c..8663179c435 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -111,6 +111,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_options(options); parse_c_object_factory_options(cmdline, options); + if(cmdline.isset("function")) + options.set_option("function", cmdline.get_value("function")); + if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions")) { error() << "--cover and --unwinding-assertions must not be given together" @@ -403,6 +406,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("validate-ssa-equation", true); } + if(cmdline.isset("validate-goto-model")) + { + options.set_option("validate-goto-model", true); + } + PARSE_OPTIONS_GOTO_TRACE(cmdline, options); } @@ -594,7 +602,8 @@ int cbmc_parse_optionst::get_goto_program( try { - goto_model = initialize_goto_model(cmdline, ui_message_handler, options); + goto_model = + initialize_goto_model(cmdline.args, ui_message_handler, options); if(cmdline.isset("show-symbol-table")) { diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2d6ccad8963..ee3c381e7e7 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -88,6 +88,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + if(cmdline.isset("function")) + options.set_option("function", cmdline.get_value("function")); + #if 0 if(cmdline.isset("c89")) config.ansi_c.set_c89(); @@ -298,6 +301,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) } } } + + if(cmdline.isset("validate-goto-model")) + { + options.set_option("validate-goto-model", true); + } } /// For the task, build the appropriate kind of analyzer @@ -390,7 +398,8 @@ int goto_analyzer_parse_optionst::doit() try { - goto_model = initialize_goto_model(cmdline, get_message_handler(), options); + goto_model = + initialize_goto_model(cmdline.args, 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 dadf7d24998..80c2086a873 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -14,10 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include +#include #include #include @@ -30,12 +30,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "read_goto_binary.h" goto_modelt initialize_goto_model( - const cmdlinet &cmdline, + const std::vector &files, message_handlert &message_handler, const optionst &options) { messaget msg(message_handler); - const std::vector &files=cmdline.args; if(files.empty()) { throw invalid_command_line_argument_exceptiont( @@ -124,7 +123,7 @@ goto_modelt initialize_goto_model( bool entry_point_generation_failed=false; - if(binaries_provided_start && cmdline.isset("function")) + if(binaries_provided_start && options.is_set("function")) { // Rebuild the entry-point, using the language annotation of the // existing __CPROVER_start function: @@ -139,7 +138,7 @@ goto_modelt initialize_goto_model( if(binaries.empty()) { // Enable/disable stub generation for opaque methods - bool stubs_enabled=cmdline.isset("generate-opaque-stubs"); + bool stubs_enabled = options.is_set("generate-opaque-stubs"); language_files.set_should_generate_opaque_method_stubs(stubs_enabled); } @@ -166,7 +165,7 @@ goto_modelt initialize_goto_model( goto_model.goto_functions, message_handler); - if(cmdline.isset("validate-goto-model")) + if(options.is_set("validate-goto-model")) { goto_model.validate(validation_modet::EXCEPTION); } diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h index e063beeadfa..139263e09d5 100644 --- a/src/goto-programs/initialize_goto_model.h +++ b/src/goto-programs/initialize_goto_model.h @@ -14,12 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" -class cmdlinet; class message_handlert; class optionst; goto_modelt initialize_goto_model( - const cmdlinet &cmdline, + const std::vector &files, message_handlert &message_handler, const optionst &options); diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index fceab494f8e..0752523b3a3 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -9,10 +9,10 @@ #include -#include #include #include #include +#include #include #include @@ -105,16 +105,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) /// language implements `languaget::convert_lazy_method`; any method not handled /// there must be populated eagerly. See `lazy_goto_modelt::get_goto_function` /// for more detail. -/// \param cmdline: command-line arguments specifying source files and GOTO -/// binaries to load +/// \param files: source files and GOTO binaries to load /// \param options: options to pass on to the language front-ends void lazy_goto_modelt::initialize( - const cmdlinet &cmdline, + const std::vector &files, const optionst &options) { messaget msg(message_handler); - const std::vector &files=cmdline.args; if(files.empty()) { throw invalid_command_line_argument_exceptiont( @@ -201,7 +199,7 @@ void lazy_goto_modelt::initialize( bool entry_point_generation_failed=false; - if(binaries_provided_start && cmdline.isset("function")) + if(binaries_provided_start && options.is_set("function")) { // Rebuild the entry-point, using the language annotation of the // existing __CPROVER_start function: @@ -216,7 +214,7 @@ void lazy_goto_modelt::initialize( if(binaries.empty()) { // Enable/disable stub generation for opaque methods - bool stubs_enabled=cmdline.isset("generate-opaque-stubs"); + bool stubs_enabled = options.is_set("generate-opaque-stubs"); language_files.set_should_generate_opaque_method_stubs(stubs_enabled); } diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index a55b0ca49e7..0db373d55e1 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -13,7 +13,6 @@ #include "lazy_goto_functions_map.h" #include "goto_convert_functions.h" -class cmdlinet; class optionst; /// A GOTO model that produces function bodies on demand. It owns a @@ -28,7 +27,7 @@ class optionst; /// The typical use case looks like: /// /// lazy_goto_modelt model(...callback parameters...); -/// model.initialize(cmdline, options); +/// model.initialize(cmdline.args, options); /// model.get_goto_function("needed_function1") /// model.get_goto_function("needed_function2"); /// ... @@ -179,7 +178,8 @@ class lazy_goto_modelt : public abstract_goto_modelt message_handler); } - void initialize(const cmdlinet &cmdline, const optionst &options); + void + initialize(const std::vector &files, const optionst &options); /// Eagerly loads all functions from the symbol table. void load_all_functions() const; diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 2513d96c30f..3cbcd30ff69 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include +#include +#include #include #include "language.h" @@ -112,8 +113,12 @@ bool language_uit::final() { language_files.set_message_handler(*message_handler); + // TODO: This should be moved elsewhere because it is not used in + // this repository. // Enable/disable stub generation for opaque methods - bool stubs_enabled=_cmdline.isset("generate-opaque-stubs"); + bool stubs_enabled = false; + if(options != nullptr) + stubs_enabled = options->is_set("generate-opaque-stubs"); language_files.set_should_generate_opaque_method_stubs(stubs_enabled); if(language_files.final(symbol_table)) From 7183e66b9cc9fb5f82bf84a7263a29109c4e1c0b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 3 Dec 2018 00:53:46 +0000 Subject: [PATCH 2/2] Reformat #if-#endif to make clang-format happy --- src/goto-analyzer/goto_analyzer_parse_options.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index ee3c381e7e7..9bc226c9a62 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -91,7 +91,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); - #if 0 +#if 0 if(cmdline.isset("c89")) config.ansi_c.set_c89(); @@ -109,9 +109,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cpp11")) config.cpp.set_cpp11(); - #endif +#endif - #if 0 +#if 0 // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -127,7 +127,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) // magic error label if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); - #endif +#endif // Select a specific analysis if(cmdline.isset("taint"))