From 890b8b12cd33a63e1859de4680b3ee3c8b3bfaee Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 10 Jan 2018 18:59:28 +0000 Subject: [PATCH 1/9] Remove exceptions: add per-function entry point This removes high-level exception-related instructions from a single function, at the cost of some accuracy as we can no longer analyse other functions to determine whether or not they may throw, and therefore always assume they will. --- src/goto-programs/remove_exceptions.cpp | 59 ++++++++++++++++++++----- src/goto-programs/remove_exceptions.h | 6 +++ 2 files changed, 53 insertions(+), 12 deletions(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 5d2d758edb6..f0a8b9b7e5f 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -79,23 +79,25 @@ class remove_exceptionst typedef std::vector> catch_handlerst; typedef std::vector stack_catcht; + typedef std::function function_may_throwt; public: explicit remove_exceptionst( - symbol_tablet &_symbol_table, - std::map> &_exceptions_map, + symbol_table_baset &_symbol_table, + function_may_throwt _function_may_throw, bool remove_added_instanceof) : symbol_table(_symbol_table), - exceptions_map(_exceptions_map), + function_may_throw(_function_may_throw), remove_added_instanceof(remove_added_instanceof) { } void operator()(goto_functionst &goto_functions); + void operator()(goto_programt &goto_program); protected: - symbol_tablet &symbol_table; - std::map> &exceptions_map; + symbol_table_baset &symbol_table; + function_may_throwt function_may_throw; bool remove_added_instanceof; symbol_exprt get_inflight_exception_global(); @@ -177,8 +179,7 @@ bool remove_exceptionst::function_or_callees_may_throw( "identifier expected to be a symbol"); const irep_idt &function_name= to_symbol_expr(function_expr).get_identifier(); - bool callee_may_throw = !exceptions_map[function_name].empty(); - if(callee_may_throw) + if(function_may_throw(function_name)) return true; } } @@ -424,9 +425,7 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - bool callee_may_throw = !exceptions_map[callee_id].empty(); - - if(callee_may_throw) + if(function_may_throw(callee_id)) { add_exception_dispatch_sequence( goto_program, instr_it, stack_catch, locals); @@ -557,22 +556,58 @@ void remove_exceptionst::operator()(goto_functionst &goto_functions) instrument_exceptions(it->second.body); } +void remove_exceptionst::operator()(goto_programt &goto_program) +{ + instrument_exceptions(goto_program); +} + /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions( - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type) { const namespacet ns(symbol_table); std::map> exceptions_map; uncaught_exceptions(goto_functions, ns, exceptions_map); + // NOLINTNEXTLINE + auto function_may_throw = [&exceptions_map](const irep_idt &id) { + return !exceptions_map[id].empty(); + }; remove_exceptionst remove_exceptions( symbol_table, - exceptions_map, + function_may_throw, type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); remove_exceptions(goto_functions); } +/// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing +/// them with explicit exception propagation. +/// Note this is somewhat less accurate than the whole-goto-model version, +/// because we can't inspect other functions to determine whether they throw +/// or not, and therefore must assume they do and always introduce post-call +/// exception dispatch. +/// \param goto_program: program to remove exceptions from +/// \param symbol_table: global symbol table. The `@inflight_exception` global +/// may be added if not already present. It will not be initialised; that is +/// the caller's responsibility. +/// \param type: specifies whether instanceof operations generated by this pass +/// should be lowered to class-identifier comparisons (using +/// remove_instanceof). +void remove_exceptions( + goto_programt &goto_program, + symbol_table_baset &symbol_table, + remove_exceptions_typest type) +{ + auto any_function_may_throw = [](const irep_idt &id) { return true; }; + + remove_exceptionst remove_exceptions( + symbol_table, + any_function_may_throw, + type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); + remove_exceptions(goto_program); +} + /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type) { diff --git a/src/goto-programs/remove_exceptions.h b/src/goto-programs/remove_exceptions.h index 632559cbf91..20d83f93807 100644 --- a/src/goto-programs/remove_exceptions.h +++ b/src/goto-programs/remove_exceptions.h @@ -29,6 +29,12 @@ enum class remove_exceptions_typest DONT_REMOVE_INSTANCEOF, }; +void remove_exceptions( + goto_programt &goto_program, + symbol_table_baset &symbol_table, + remove_exceptions_typest type = + remove_exceptions_typest::DONT_REMOVE_INSTANCEOF); + void remove_exceptions( goto_modelt &goto_model, remove_exceptions_typest type = From 98741f928c54c3b5e3b2c18360371ea1470f18f3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 2 Mar 2018 09:30:50 +0000 Subject: [PATCH 2/9] Java frontend: note availability of synthetic methods This informs symex-driven lazy loading that certain synthetic methods can be given bodies on demand by the Java frontend, similar to how normal methods we have bytecode for are treated. --- src/java_bytecode/java_bytecode_language.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index bf226bb38f4..9c72934c9cc 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -814,6 +814,9 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const // Add all concrete methods to map for(const auto &kv : method_bytecode) methods.insert(kv.first); + // Add all synthetic methods to map + for(const auto &kv : synthetic_methods) + methods.insert(kv.first); } /// \brief Promote a lazy-converted method (one whose type is known but whose From 8df9350d26d1dee70105e532aa05e8985f631015 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 2 Mar 2018 10:27:40 +0000 Subject: [PATCH 3/9] Java frontend: rename externally driven loading This name is more accurate, as the frontend is no longer in charge of choosing what gets loaded and why -- it just obeys convert_lazy_method requests given by the driver program. --- src/java_bytecode/java_bytecode_language.cpp | 4 ++-- src/java_bytecode/java_bytecode_language.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 9c72934c9cc..6f4ae143fed 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -58,8 +58,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); - if(cmd.isset("lazy-methods-context-sensitive")) - lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE; + if(cmd.isset("symex-driven-lazy-loading")) + lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER; else if(cmd.isset("lazy-methods")) lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE; else diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index dc708eef744..04a70935f37 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -63,7 +63,7 @@ enum lazy_methods_modet { LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, - LAZY_METHODS_MODE_CONTEXT_SENSITIVE + LAZY_METHODS_MODE_EXTERNAL_DRIVER }; class java_bytecode_languaget:public languaget From 978ca5bf0f66d4a176c990d3a5b5fa475e988e0d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 2 Mar 2018 10:48:17 +0000 Subject: [PATCH 4/9] Add callback after symex to bmct This permits frontend programs to intervene after symex executes, either in addition to or instead of running bmc. Its current use case is to implement show-goto-functions and similar debug output options when symex-driven lazy loading means that function bodies are not populated until symex has run. When --paths is in use, the callback will be made every time symex finishes a path. --- src/cbmc/bmc.cpp | 27 ++++++++++++++++++++------- src/cbmc/bmc.h | 31 +++++++++++++++++++++---------- 2 files changed, 41 insertions(+), 17 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 8359d4a2d97..c2a1e8db7d4 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -377,6 +377,15 @@ safety_checkert::resultt bmct::execute( const goto_functionst &goto_functions = goto_model.get_goto_functions(); + // This provides the driver program the opportunity to do things like a + // symbol-table or goto-functions dump instead of actually running the + // checker, like show-vcc except driver-program specific. + // In particular clients that use symex-driven program loading need to print + // GOTO functions after symex, as function bodies are not produced until + // symex first requests them. + if(driver_callback_after_symex && driver_callback_after_symex()) + return safety_checkert::resultt::SAFE; // to indicate non-error + // add a partial ordering, if required if(equation.has_threads()) { @@ -616,14 +625,15 @@ void bmct::setup_unwind() // creating those function bodies on demand. /// \param ui: user-interface mode (plain text, XML output, JSON output, ...) /// \param message: used for logging -/// \param frontend_configure_bmc: function provided by the frontend program, -/// which applies frontend-specific configuration to a bmct before running. +/// \param driver_configure_bmc: function provided by the driver program, +/// which applies driver-specific configuration to a bmct before running. int bmct::do_language_agnostic_bmc( const optionst &opts, abstract_goto_modelt &model, const ui_message_handlert::uit &ui, messaget &message, - std::function frontend_configure_bmc) + std::function driver_configure_bmc, + std::function callback_after_symex) { const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); @@ -637,9 +647,10 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, mh, pc, worklist); + bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex); bmc.set_ui(ui); - frontend_configure_bmc(bmc, symbol_table); + if(driver_configure_bmc) + driver_configure_bmc(bmc, symbol_table); result = bmc.run(model); } INVARIANT( @@ -682,8 +693,10 @@ int bmct::do_language_agnostic_bmc( pc, resume.equation, resume.state, - worklist); - frontend_configure_bmc(pe, symbol_table); + worklist, + callback_after_symex); + if(driver_configure_bmc) + driver_configure_bmc(pe, symbol_table); result &= pe.run(model); worklist.pop_front(); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 9daad327d66..d4feb6847e0 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -74,7 +74,8 @@ class bmct:public safety_checkert const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, - goto_symext::branch_worklistt &_branch_worklist) + goto_symext::branch_worklistt &_branch_worklist, + std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), @@ -83,7 +84,8 @@ class bmct:public safety_checkert branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN) + ui(ui_message_handlert::uit::PLAIN), + driver_callback_after_symex(callback_after_symex) { symex.constant_propagation=options.get_bool_option("propagation"); symex.record_coverage= @@ -128,10 +130,9 @@ class bmct:public safety_checkert abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, - std::function frontend_configure_bmc = - [](bmct &_bmc, const symbol_tablet &) { // NOLINT (*) - // Empty default implementation - }); + std::function + driver_configure_bmc = nullptr, + std::function callback_after_symex = nullptr); protected: /// \brief Constructor for path exploration from saved state @@ -147,7 +148,8 @@ class bmct:public safety_checkert message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, - goto_symext::branch_worklistt &_branch_worklist) + goto_symext::branch_worklistt &_branch_worklist, + std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), @@ -156,7 +158,8 @@ class bmct:public safety_checkert branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN) + ui(ui_message_handlert::uit::PLAIN), + driver_callback_after_symex(callback_after_symex) { symex.constant_propagation = options.get_bool_option("propagation"); symex.record_coverage = @@ -238,6 +241,12 @@ class bmct:public safety_checkert /// full-program model-checking from the entry point of the program. virtual void perform_symbolic_execution( goto_symext::get_goto_functiont get_goto_function); + + /// Optional callback, to be run after symex but before handing the resulting + /// equation to the solver. If it returns true then we will skip the solver + /// stage and return "safe" (no assertions violated / coverage goals reached), + /// similar to the behaviour when 'show-vcc' or 'program-only' are specified. + std::function driver_callback_after_symex; }; /// \brief Symbolic execution from a saved branch point @@ -260,14 +269,16 @@ class path_explorert : public bmct prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, - goto_symext::branch_worklistt &branch_worklist) + goto_symext::branch_worklistt &branch_worklist, + std::function callback_after_symex) : bmct( _options, outer_symbol_table, _message_handler, _prop_conv, saved_equation, - branch_worklist), + branch_worklist, + callback_after_symex), saved_state(saved_state) { } From 7b5d73b22d7a7a73a4c9c6aa8f719685162049e7 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 2 Mar 2018 10:50:21 +0000 Subject: [PATCH 5/9] JBMC: use symex-driven lazy loading This adds the symex-driven-lazy-loading option, which causes functions to be loaded only when symex first requests their body. This means that all frontend effort can be saved relating to functions that symex reveals to be inaccessible, such as virtual function calls whose full array of possible targets are known to be unreachable as a result of value-set analysis on the type of the callee instance. --- src/jbmc/jbmc_parse_options.cpp | 194 ++++++++++++++++++++++++++++---- src/jbmc/jbmc_parse_options.h | 6 +- 2 files changed, 174 insertions(+), 26 deletions(-) diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 06d429287d5..b1aa03b0aa0 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -48,7 +48,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -378,6 +377,23 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.get_value("symex-coverage-report")); PARSE_OPTIONS_GOTO_TRACE(cmdline, options); + + if(cmdline.isset("symex-driven-lazy-loading")) + { + options.set_option("symex-driven-lazy-loading", true); + for(const char *opt : + { "nondet-static", + "full-slice", + "show-properties", + "lazy-methods" }) + { + if(cmdline.isset(opt)) + { + throw std::string("Option ") + opt + + " can't be used with --symex-driven-lazy-loading"; + } + } + } } /// invoke main modules @@ -472,24 +488,7 @@ int jbmc_parse_optionst::doit() return 0; } - std::unique_ptr goto_model_ptr; - int get_goto_program_ret=get_goto_program(goto_model_ptr, options); - if(get_goto_program_ret!=-1) - return get_goto_program_ret; - - goto_modelt &goto_model = *goto_model_ptr; - - if(cmdline.isset("show-properties")) - { - show_properties( - goto_model, get_message_handler(), ui_message_handler.get_ui()); - return 0; // should contemplate EX_OK from sysexits.h - } - - if(set_properties(goto_model)) - return 7; // should contemplate EX_USAGE from sysexits.h - - std::function configure_bmc; + std::function configure_bmc = nullptr; if(options.get_bool_option("java-unwind-enum-static")) { configure_bmc = []( @@ -508,15 +507,76 @@ int jbmc_parse_optionst::doit() }); }; } + + if(!cmdline.isset("symex-driven-lazy-loading")) + { + std::unique_ptr goto_model_ptr; + int get_goto_program_ret=get_goto_program(goto_model_ptr, options); + if(get_goto_program_ret!=-1) + return get_goto_program_ret; + + goto_modelt &goto_model = *goto_model_ptr; + + if(cmdline.isset("show-properties")) + { + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); + return 0; // should contemplate EX_OK from sysexits.h + } + + if(set_properties(goto_model)) + return 7; // should contemplate EX_USAGE from sysexits.h + + // The `configure_bmc` callback passed will enable enum-unwind-static if + // applicable. + return bmct::do_language_agnostic_bmc( + options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); + } else { - configure_bmc = []( - bmct &bmc, const symbol_tablet &symbol_table) { // NOLINT (*) - // NOOP + // 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); + + // 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 + // trip an invariant when it tries to load it) + if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point())) + { + error() << "the program has no entry point"; + return 6; + } + + // Add failed symbols for any symbol created prior to loading any + // particular function: + add_failed_symbols(lazy_goto_model.symbol_table); + + // If applicable, parse the coverage instrumentation configuration, which + // will be used in process_goto_function: + cover_config = + get_cover_config( + options, lazy_goto_model.symbol_table, get_message_handler()); + + // Provide show-goto-functions and similar dump functions after symex + // executes. If --paths is active, these dump routines run after every + // paths iteration. Its return value indicates that if we ran any dump + // function, then we should skip the actual solver phase. + auto callback_after_symex = [this, &lazy_goto_model]() { // NOLINT (*) + return show_loaded_functions(lazy_goto_model); }; + + // The `configure_bmc` callback passed will enable enum-unwind-static if + // applicable. + return + bmct::do_language_agnostic_bmc( + options, + lazy_goto_model, + ui_message_handler.get_ui(), + *this, + configure_bmc, + callback_after_symex); } - return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); } bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model) @@ -643,6 +703,10 @@ void jbmc_parse_optionst::process_goto_function( journalling_symbol_tablet &symbol_table = function.get_symbol_table(); namespacet ns(symbol_table); goto_functionst::goto_functiont &goto_function = function.get_goto_function(); + + bool using_symex_driven_loading = + options.get_bool_option("symex-driven-lazy-loading"); + try { // Removal of RTTI inspection: @@ -650,6 +714,19 @@ void jbmc_parse_optionst::process_goto_function( // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(function); + if(using_symex_driven_loading) + { + // remove exceptions + // If using symex-driven function loading we need to do this now so that + // symex doesn't have to cope with exception-handling constructs; however + // the results are slightly worse than running it in whole-program mode + // (e.g. dead catch sites will be retained) + remove_exceptions( + goto_function.body, + symbol_table, + remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); + } + auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { // NOLINT(*) return symbol_table.lookup_ref(id).value.is_nil() && @@ -699,6 +776,28 @@ void jbmc_parse_optionst::process_goto_function( symbol_table); } + // If using symex-driven function loading we must insert the coverage goals + // now so symex sees its targets; otherwise we leave this until + // process_goto_functions, as we haven't run remove_exceptions yet, and that + // pass alters the CFG. + if(using_symex_driven_loading) + { + // instrument cover goals + if(cmdline.isset("cover")) + { + INVARIANT( + cover_config != nullptr, "cover config should have been parsed"); + instrument_cover_goals(*cover_config, function, get_message_handler()); + } + + // label the assertions + label_properties(goto_function.body); + + goto_function.body.update(); + function.compute_location_numbers(); + goto_function.body.compute_loop_numbers(); + } + // update the function member in each instruction function.update_instructions_function(); } @@ -722,6 +821,39 @@ void jbmc_parse_optionst::process_goto_function( } } +bool jbmc_parse_optionst::show_loaded_functions( + const abstract_goto_modelt &goto_model) +{ + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table( + goto_model.get_symbol_table(), ui_message_handler.get_ui()); + return true; + } + + if(cmdline.isset("show-loops")) + { + show_loop_ids(ui_message_handler.get_ui(), goto_model.get_goto_functions()); + return true; + } + + if( + cmdline.isset("show-goto-functions") || + cmdline.isset("list-goto-functions")) + { + namespacet ns(goto_model.get_symbol_table()); + show_goto_functions( + ns, + get_message_handler(), + ui_message_handler.get_ui(), + goto_model.get_goto_functions(), + cmdline.isset("list-goto-functions")); + return true; + } + + return false; +} + bool jbmc_parse_optionst::process_goto_functions( goto_modelt &goto_model, const optionst &options) @@ -729,7 +861,17 @@ bool jbmc_parse_optionst::process_goto_functions( try { status() << "Running GOTO functions transformation passes" << eom; - // remove catch and throw (introduces instanceof but request it is removed) + + bool using_symex_driven_loading = + options.get_bool_option("symex-driven-lazy-loading"); + + // When using symex-driven lazy loading, *all* relevant processing is done + // during process_goto_function, so we have nothing to do here. + if(using_symex_driven_loading) + return false; + + // remove catch and throw + // (introduces instanceof but request it is removed) remove_exceptions( goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); @@ -865,6 +1007,8 @@ void jbmc_parse_optionst::help() // This one is handled by jbmc_parse_options not by the Java frontend, // hence its presence here: " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*) + // Currently only supported in the JBMC frontend: + " --symex-driven-lazy-loading only load functions when first entered by symbolic execution\n" // NOLINT(*) "\n" "BMC options:\n" HELP_BMC diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index a2e2aa1cdcd..874a988cbdb 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -72,7 +73,8 @@ class optionst; JAVA_BYTECODE_LANGUAGE_OPTIONS \ "(java-unwind-enum-static)" \ "(localize-faults)(localize-faults-method):" \ - OPT_GOTO_TRACE + OPT_GOTO_TRACE \ + "(symex-driven-lazy-loading)" // clang-format on class jbmc_parse_optionst: @@ -97,11 +99,13 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; + std::unique_ptr cover_config; void eval_verbosity(); void get_command_line_options(optionst &); int get_goto_program( std::unique_ptr &goto_model, const optionst &); + bool show_loaded_functions(const abstract_goto_modelt &goto_model); bool set_properties(goto_modelt &goto_model); }; From 8aa38e787f80e2fa1215d65862b5495a1c088cd3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 19 Jan 2018 16:24:44 +0000 Subject: [PATCH 6/9] Add tests for symex-driven lazy loading This adds variants of the three test directories that use JBMC (cbmc-java, jbmc-strings and strings-smoke-tests) to run with --symex-driven-lazy-loading, except for the small number of tests that are expected to fail for harmless reasons, and one that is expected to fail and which may be a bug (strings-smoke-tests/java_append_char). --- regression/cbmc-java/CMakeLists.txt | 7 +++++++ regression/cbmc-java/Makefile | 2 ++ regression/cbmc-java/NondetInit/test_lazy.desc | 4 +++- regression/cbmc-java/covered1/test.desc | 4 +++- regression/cbmc-java/generic_class_bound1/test.desc | 5 ++++- regression/cbmc-java/jsr1/test.desc | 4 +++- regression/cbmc-java/lambda2/test_no_crash.desc | 3 ++- regression/cbmc-java/lazyloading1/test.desc | 4 +++- regression/cbmc-java/lazyloading10/test.desc | 5 ++++- regression/cbmc-java/lazyloading11/test.desc | 4 +++- regression/cbmc-java/lazyloading2/test.desc | 4 +++- regression/cbmc-java/lazyloading3/test.desc | 4 +++- regression/cbmc-java/lazyloading4/test.desc | 5 ++++- regression/cbmc-java/lazyloading5/test.desc | 5 ++++- regression/cbmc-java/lazyloading6/test.desc | 4 +++- regression/cbmc-java/lazyloading7/test.desc | 4 +++- regression/cbmc-java/lazyloading8/test.desc | 4 +++- regression/cbmc-java/lazyloading9/test.desc | 5 ++++- regression/cbmc-java/lazyloading_array_parameter/test.desc | 5 ++++- regression/cbmc-java/lazyloading_cyclic_class/test.desc | 4 +++- .../lazyloading_indirect_array_parameter/test.desc | 5 ++++- .../lazyloading_indirect_generic_array_parameter/test.desc | 5 ++++- regression/cbmc-java/lazyloading_inheritance/test.desc | 4 +++- .../cbmc-java/lazyloading_inheritance_field/test.desc | 4 +++- .../cbmc-java/lazyloading_multiple_array_types/test.desc | 5 ++++- .../lazyloading_multiple_generic_parameters/test.desc | 5 ++++- .../lazyloading_nested_generic_parameters/test.desc | 1 + regression/cbmc-java/lazyloading_recursive_class/test.desc | 4 +++- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_removed_by_lazy_loading.desc | 4 +++- .../check_runs_with_lazy_loading.desc | 5 ++++- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_removed_by_lazy_loading.desc | 4 +++- .../check_runs_with_lazy_loading.desc | 5 ++++- .../check_clinit_normally_present.desc | 2 +- .../check_clinit_removed_by_lazy_loading.desc | 4 +++- .../check_runs_with_lazy_loading.desc | 5 ++++- regression/cbmc-java/lvt-groovy/test.desc | 3 ++- regression/cbmc-java/lvt-unexpected/test.desc | 4 +++- regression/cbmc-java/method_parmeters1/test.desc | 4 +++- regression/cbmc-java/method_parmeters2/test.desc | 4 +++- regression/cbmc-java/package_friendly1/test.desc | 4 +++- .../cbmc-java/remove_virtual_function_typecast/test.desc | 4 +++- regression/cbmc-java/removed_virtual_functions/test.desc | 4 +++- regression/cbmc-java/virtual10/test.desc | 2 +- regression/cbmc-java/virtual7/test.desc | 6 +++--- regression/jbmc-strings/CMakeLists.txt | 7 +++++++ regression/jbmc-strings/Makefile | 4 ++++ regression/jbmc-strings/StringIndexOf/test.desc | 1 - regression/jbmc-strings/java_char_array_init/test.desc | 1 - regression/strings-smoke-tests/CMakeLists.txt | 7 +++++++ regression/strings-smoke-tests/Makefile | 4 ++++ 52 files changed, 164 insertions(+), 47 deletions(-) diff --git a/regression/cbmc-java/CMakeLists.txt b/regression/cbmc-java/CMakeLists.txt index afe0ea5761a..2742f7ba078 100644 --- a/regression/cbmc-java/CMakeLists.txt +++ b/regression/cbmc-java/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "cbmc-java-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure" + "CORE" +) diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index e94b327bb43..15894631527 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -2,9 +2,11 @@ default: tests.log test: @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure tests.log: ../test.pl @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure show: @for dir in *; do \ diff --git a/regression/cbmc-java/NondetInit/test_lazy.desc b/regression/cbmc-java/NondetInit/test_lazy.desc index 9ca92cb5696..6840ea97697 100644 --- a/regression/cbmc-java/NondetInit/test_lazy.desc +++ b/regression/cbmc-java/NondetInit/test_lazy.desc @@ -1,5 +1,7 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --function Test.check --lazy-methods ^VERIFICATION SUCCESSFUL$ -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc index 8982c0321db..fc05584a808 100644 --- a/regression/cbmc-java/covered1/test.desc +++ b/regression/cbmc-java/covered1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure covered1.class --cover location --json-ui --show-properties ^EXIT=0$ @@ -25,3 +25,5 @@ covered1.class .*\"coveredLines\": \"35\",$ -- ^warning: ignoring +-- +This fails with symex-driven lazy loading because it does not currently support --show-properties. diff --git a/regression/cbmc-java/generic_class_bound1/test.desc b/regression/cbmc-java/generic_class_bound1/test.desc index 0195fb3ecc4..0da89d44def 100644 --- a/regression/cbmc-java/generic_class_bound1/test.desc +++ b/regression/cbmc-java/generic_class_bound1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Gn.class --cover location ^EXIT=0$ @@ -9,3 +9,6 @@ Gn.class .*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED .*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED -- +-- +This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable +from the entry point, so with symex-driven loading the functions foo1 and the constructor don't get created at all. diff --git a/regression/cbmc-java/jsr1/test.desc b/regression/cbmc-java/jsr1/test.desc index faec2ddbb03..b7cb6825d52 100644 --- a/regression/cbmc-java/jsr1/test.desc +++ b/regression/cbmc-java/jsr1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class --show-goto-functions ^EXIT=0$ @@ -6,3 +6,5 @@ edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class -- \\"statement\\" \(\\"jsr\\"\) \\"statement\\" \(\\"ret\\"\) +-- +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/lambda2/test_no_crash.desc b/regression/cbmc-java/lambda2/test_no_crash.desc index 933732babea..f05242bf10d 100644 --- a/regression/cbmc-java/lambda2/test_no_crash.desc +++ b/regression/cbmc-java/lambda2/test_no_crash.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure SymStream.class --verbosity 10 --show-goto-functions ^EXIT=0 @@ -6,3 +6,4 @@ SymStream.class -- -- just to test that it doesn't crash in this situation, cf. TG-2684 +Doesn't work with symex-driven loading because there is no entry point (we want to load the entire class) diff --git a/regression/cbmc-java/lazyloading1/test.desc b/regression/cbmc-java/lazyloading1/test.desc index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading1/test.desc +++ b/regression/cbmc-java/lazyloading1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.main ^EXIT=0$ @@ -6,3 +6,5 @@ test.class elaborate java::A\.f:\(\)V -- elaborate java::B\.g:\(\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading10/test.desc b/regression/cbmc-java/lazyloading10/test.desc index 38fb7495a08..3a1f2da5ae8 100644 --- a/regression/cbmc-java/lazyloading10/test.desc +++ b/regression/cbmc-java/lazyloading10/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety ^EXIT=6$ @@ -6,3 +6,6 @@ test.class entry point 'test\.sety' is ambiguous between: test\.sety:\(I\)V test\.sety:\(F\)V +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading11/test.desc b/regression/cbmc-java/lazyloading11/test.desc index 1114831afb3..ee2ef683627 100644 --- a/regression/cbmc-java/lazyloading11/test.desc +++ b/regression/cbmc-java/lazyloading11/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' --lazy-methods-extra-entry-point 'test.sety:(F)V' ^EXIT=0$ @@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V CI lazy methods: elaborate java::test\.sety:\(F\)V -- CI lazy methods: elaborate java::test\.setx:\(I\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading2/test.desc b/regression/cbmc-java/lazyloading2/test.desc index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading2/test.desc +++ b/regression/cbmc-java/lazyloading2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.main ^EXIT=0$ @@ -6,3 +6,5 @@ test.class elaborate java::A\.f:\(\)V -- elaborate java::B\.g:\(\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading3/test.desc b/regression/cbmc-java/lazyloading3/test.desc index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading3/test.desc +++ b/regression/cbmc-java/lazyloading3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.main ^EXIT=0$ @@ -6,3 +6,5 @@ test.class elaborate java::A\.f:\(\)V -- elaborate java::B\.g:\(\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading4/test.desc b/regression/cbmc-java/lazyloading4/test.desc index e7822c6deba..9df5b91931e 100644 --- a/regression/cbmc-java/lazyloading4/test.desc +++ b/regression/cbmc-java/lazyloading4/test.desc @@ -1,6 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Main.class --lazy-methods ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading5/test.desc b/regression/cbmc-java/lazyloading5/test.desc index a3226adccaa..fa309520217 100644 --- a/regression/cbmc-java/lazyloading5/test.desc +++ b/regression/cbmc-java/lazyloading5/test.desc @@ -1,6 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --function test.main ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading6/test.desc b/regression/cbmc-java/lazyloading6/test.desc index dd4bbf33bc9..ce055cbbc7b 100644 --- a/regression/cbmc-java/lazyloading6/test.desc +++ b/regression/cbmc-java/lazyloading6/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx ^EXIT=0$ @@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.setx:\(I\)V -- CI lazy methods: elaborate java::test\.sety:\(I\)V CI lazy methods: elaborate java::test\.sety:\(F\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading7/test.desc b/regression/cbmc-java/lazyloading7/test.desc index 3b2e305f66c..009f489aeff 100644 --- a/regression/cbmc-java/lazyloading7/test.desc +++ b/regression/cbmc-java/lazyloading7/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' ^EXIT=0$ @@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V -- CI lazy methods: elaborate java::test\.setx:\(I\)V CI lazy methods: elaborate java::test\.sety:\(F\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading8/test.desc b/regression/cbmc-java/lazyloading8/test.desc index 777f1673de9..2476aa30841 100644 --- a/regression/cbmc-java/lazyloading8/test.desc +++ b/regression/cbmc-java/lazyloading8/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(F)V' ^EXIT=0$ @@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(F\)V -- CI lazy methods: elaborate java::test\.sety:\(I\)V CI lazy methods: elaborate java::test\.setx:\(I\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading9/test.desc b/regression/cbmc-java/lazyloading9/test.desc index ddd4fbd51c0..09f407629c7 100644 --- a/regression/cbmc-java/lazyloading9/test.desc +++ b/regression/cbmc-java/lazyloading9/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.*' ^EXIT=0$ @@ -7,3 +7,6 @@ VERIFICATION SUCCESSFUL CI lazy methods: elaborate java::test\.setx:\(I\)V CI lazy methods: elaborate java::test\.sety:\(I\)V CI lazy methods: elaborate java::test\.sety:\(F\)V +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_array_parameter/test.desc b/regression/cbmc-java/lazyloading_array_parameter/test.desc index 15e3f99d782..51ac926c68a 100644 --- a/regression/cbmc-java/lazyloading_array_parameter/test.desc +++ b/regression/cbmc-java/lazyloading_array_parameter/test.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.g ^EXIT=0$ ^SIGNAL=0$ elaborate java::test\.f:\(\)I VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_cyclic_class/test.desc b/regression/cbmc-java/lazyloading_cyclic_class/test.desc index c39c5e62349..fec143df213 100644 --- a/regression/cbmc-java/lazyloading_cyclic_class/test.desc +++ b/regression/cbmc-java/lazyloading_cyclic_class/test.desc @@ -1,7 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.test ^EXIT=0$ ^SIGNAL=0$ elaborate java::Base\.f:\(\)V -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc index 15e3f99d782..51ac926c68a 100644 --- a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc +++ b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.g ^EXIT=0$ ^SIGNAL=0$ elaborate java::test\.f:\(\)I VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc index 15e3f99d782..51ac926c68a 100644 --- a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc +++ b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.g ^EXIT=0$ ^SIGNAL=0$ elaborate java::test\.f:\(\)I VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_inheritance/test.desc b/regression/cbmc-java/lazyloading_inheritance/test.desc index 12ef42a2183..76ed72b1f69 100644 --- a/regression/cbmc-java/lazyloading_inheritance/test.desc +++ b/regression/cbmc-java/lazyloading_inheritance/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.test ^EXIT=0$ @@ -7,3 +7,5 @@ elaborate java::Base\.f:\(\)V -- elaborate java::Derived\.f:\(\)V elaborate java::Middle\.f:\(\)V +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_inheritance_field/test.desc b/regression/cbmc-java/lazyloading_inheritance_field/test.desc index c39c5e62349..fec143df213 100644 --- a/regression/cbmc-java/lazyloading_inheritance_field/test.desc +++ b/regression/cbmc-java/lazyloading_inheritance_field/test.desc @@ -1,7 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.test ^EXIT=0$ ^SIGNAL=0$ elaborate java::Base\.f:\(\)V -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc index f15d1291c02..faa9503717a 100644 --- a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc +++ b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --verbosity 10 --function Test.check ^EXIT=0$ @@ -6,3 +6,6 @@ Test.class elaborate java::A\.f:\(\)I elaborate java::B\.g:\(\)I VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc index 15e3f99d782..51ac926c68a 100644 --- a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc +++ b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.g ^EXIT=0$ ^SIGNAL=0$ elaborate java::test\.f:\(\)I VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc index ae44ea6da9b..579f3933553 100644 --- a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc +++ b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc @@ -11,3 +11,4 @@ The right methods are loaded, but verification is not successful because __CPROVER_start doesn't create appropriately typed input for this kind of nested generic parameter, so dynamic cast checks fail upon fetching the generic type's field. +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_recursive_class/test.desc b/regression/cbmc-java/lazyloading_recursive_class/test.desc index c39c5e62349..fec143df213 100644 --- a/regression/cbmc-java/lazyloading_recursive_class/test.desc +++ b/regression/cbmc-java/lazyloading_recursive_class/test.desc @@ -1,7 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure test.class --lazy-methods --verbosity 10 --function test.test ^EXIT=0$ ^SIGNAL=0$ elaborate java::Base\.f:\(\)V -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc index ddcd21bd5f2..f05b7408521 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --show-goto-functions --function Test.main java::Unused::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc index 7cb991a807f..49c88acd878 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc @@ -1,6 +1,8 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --show-goto-functions --function Test.main -- java::Unused::clinit_wrapper Unused\.\(\) +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc index 67aa49a0689..0c6c32b0319 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc @@ -1,4 +1,7 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --function Test.main VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc index 32ea1eabe00..18c1eda7556 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --show-goto-functions --function Test.main java::Unused1::clinit_wrapper diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc index 3fb25e852a4..7a6c066bf9d 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc @@ -1,7 +1,9 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --show-goto-functions --function Test.main -- java::Unused1::clinit_wrapper java::Unused2::clinit_wrapper Unused2\.\(\) +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc index 67aa49a0689..0c6c32b0319 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc @@ -1,4 +1,7 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --function Test.main VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc index 689fdc3efad..81312c026c4 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --show-goto-functions --function Test.main java::Opaque\.:\(\)V diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc index ec1d71302d6..b0256ccbad8 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc @@ -1,6 +1,8 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --show-goto-functions --function Test.main -- java::Opaque\.:\(\)V java::Opaque::clinit_wrapper +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc index 67aa49a0689..0c6c32b0319 100644 --- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc +++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc @@ -1,4 +1,7 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --lazy-methods --function Test.main VERIFICATION SUCCESSFUL +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/lvt-groovy/test.desc b/regression/cbmc-java/lvt-groovy/test.desc index 050fcd09c7e..6f8c52c05ca 100644 --- a/regression/cbmc-java/lvt-groovy/test.desc +++ b/regression/cbmc-java/lvt-groovy/test.desc @@ -1,7 +1,8 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure DetectSplitPackagesTask.class --show-symbol-table ^EXIT=0$ ^SIGNAL=0$ -- -- +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/lvt-unexpected/test.desc b/regression/cbmc-java/lvt-unexpected/test.desc index 7164d59e21f..fed0105ff68 100644 --- a/regression/cbmc-java/lvt-unexpected/test.desc +++ b/regression/cbmc-java/lvt-unexpected/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure unexpected.class --verbosity 10 --show-symbol-table ^EXIT=0$ @@ -10,3 +10,5 @@ expected by the bytecode to goto conversion algorithms. Namely, the live range of parameter x in that method is not preceeded by a store_i instruction, which is perfectly possibly as per the JVM specs but currently additionally required in CBMC. + +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/method_parmeters1/test.desc b/regression/cbmc-java/method_parmeters1/test.desc index 909aa8ab6b4..6960d310ed7 100644 --- a/regression/cbmc-java/method_parmeters1/test.desc +++ b/regression/cbmc-java/method_parmeters1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure method_parameters.class --verbosity 10 --show-symbol-table ^EXIT=0$ @@ -7,3 +7,5 @@ method_parameters.class -- The purpose of the test is ensuring that the bytecode -> symbol table AST generation happens correctly. The generated .class file does not contain LVTs. + +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/method_parmeters2/test.desc b/regression/cbmc-java/method_parmeters2/test.desc index 507e8d4ef11..da1c3e0267c 100644 --- a/regression/cbmc-java/method_parmeters2/test.desc +++ b/regression/cbmc-java/method_parmeters2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure method_parameters.class --verbosity 10 --show-symbol-table ^EXIT=0$ @@ -8,3 +8,5 @@ method_parameters.class The purpose of the test is ensuring that the bytecode -> symbol table AST generation happens correctly. The generated .class file DOES contain LVTs, i.e., it has been compiled with with "javac -g". + +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/package_friendly1/test.desc b/regression/cbmc-java/package_friendly1/test.desc index 527f5b9bfe0..1b9f7ad4080 100644 --- a/regression/cbmc-java/package_friendly1/test.desc +++ b/regression/cbmc-java/package_friendly1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure main.class package_friendly1.class package_friendly2.class --show-goto-functions ^main[.]main[\(][\)].*$ @@ -7,3 +7,5 @@ package_friendly1.class package_friendly2.class --show-goto-functions ^SIGNAL=0$ -- ^warning: ignoring +-- +This doesn't work under symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/remove_virtual_function_typecast/test.desc b/regression/cbmc-java/remove_virtual_function_typecast/test.desc index 32be1c0c99a..05841fcdc63 100644 --- a/regression/cbmc-java/remove_virtual_function_typecast/test.desc +++ b/regression/cbmc-java/remove_virtual_function_typecast/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure VirtualFunctions.class --lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function VirtualFunctions.check --show-goto-functions \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$ @@ -6,3 +6,5 @@ VirtualFunctions.class b \. VirtualFunctions\$B\.f:\(\)V\(\);$ \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$ -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/removed_virtual_functions/test.desc b/regression/cbmc-java/removed_virtual_functions/test.desc index 36b47b39757..93a66232f62 100644 --- a/regression/cbmc-java/removed_virtual_functions/test.desc +++ b/regression/cbmc-java/removed_virtual_functions/test.desc @@ -1,6 +1,8 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure ArrayListEquals.class --lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions e2 . ArrayList\$Itr.hasNext:\(\)Z\(\); -- e2 . ListIterator.hasNext:\(\)Z\(\); +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/virtual10/test.desc b/regression/cbmc-java/virtual10/test.desc index df1d033f0a4..ea746c52c19 100644 --- a/regression/cbmc-java/virtual10/test.desc +++ b/regression/cbmc-java/virtual10/test.desc @@ -1,6 +1,6 @@ CORE E.class ---show-goto-functions +--function E.f --show-goto-functions IF.*"java::D" IF.*"java::O" IF.*"java::C" diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index 6e420f8430c..7d23df44236 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/regression/cbmc-java/virtual7/test.desc @@ -3,6 +3,6 @@ test.class --show-goto-functions --function test.main ^EXIT=0$ ^SIGNAL=0$ -IF.*"java::C".*THEN GOTO [12] -IF.*"java::D".*THEN GOTO [12] -IF.*"java::A".*THEN GOTO [12] +IF.*"java::C".*THEN GOTO +IF.*"java::D".*THEN GOTO +IF.*"java::A".*THEN GOTO diff --git a/regression/jbmc-strings/CMakeLists.txt b/regression/jbmc-strings/CMakeLists.txt index afe0ea5761a..9b4832e9833 100644 --- a/regression/jbmc-strings/CMakeLists.txt +++ b/regression/jbmc-strings/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "jbmc-strings-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure" + "CORE" +) diff --git a/regression/jbmc-strings/Makefile b/regression/jbmc-strings/Makefile index 58058dbc77a..79788e2eb69 100644 --- a/regression/jbmc-strings/Makefile +++ b/regression/jbmc-strings/Makefile @@ -2,15 +2,19 @@ default: tests.log test: @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure testfuture: @../test.pl -p -c ../../../src/jbmc/jbmc -CF + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF testall: @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK tests.log: ../test.pl @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure show: @for dir in *; do \ diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc index 8b52eaea4dd..2e22278a15b 100644 --- a/regression/jbmc-strings/StringIndexOf/test.desc +++ b/regression/jbmc-strings/StringIndexOf/test.desc @@ -4,4 +4,3 @@ Test.class ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- diff --git a/regression/jbmc-strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc index 47fcb2fd1ce..5ecb589e1f8 100644 --- a/regression/jbmc-strings/java_char_array_init/test.desc +++ b/regression/jbmc-strings/java_char_array_init/test.desc @@ -7,4 +7,3 @@ assertion.* file test_init.java line 31 .* SUCCESS$ assertion.* file test_init.java line 33 .* SUCCESS$ assertion.* file test_init.java line 35 .* FAILURE$ assertion.* file test_init.java line 37 .* FAILURE$ --- diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt index afe0ea5761a..8c8577192c0 100644 --- a/regression/strings-smoke-tests/CMakeLists.txt +++ b/regression/strings-smoke-tests/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "strings-smoke-tests-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure" + "CORE" +) diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile index 58058dbc77a..79788e2eb69 100644 --- a/regression/strings-smoke-tests/Makefile +++ b/regression/strings-smoke-tests/Makefile @@ -2,15 +2,19 @@ default: tests.log test: @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure testfuture: @../test.pl -p -c ../../../src/jbmc/jbmc -CF + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF testall: @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK tests.log: ../test.pl @../test.pl -p -c ../../../src/jbmc/jbmc + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure show: @for dir in *; do \ From ccb2cf3044778f0b4c6579e21bb5556ffde96cd3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 2 Mar 2018 10:06:18 +0000 Subject: [PATCH 7/9] Fix broken test descriptions --- regression/cbmc-java/exceptions26/test.desc | 1 + regression/cbmc-java/exceptions27/test.desc | 1 + 2 files changed, 2 insertions(+) diff --git a/regression/cbmc-java/exceptions26/test.desc b/regression/cbmc-java/exceptions26/test.desc index 0e2ccfc7f46..eb2dc18d2cb 100644 --- a/regression/cbmc-java/exceptions26/test.desc +++ b/regression/cbmc-java/exceptions26/test.desc @@ -1,5 +1,6 @@ CORE test.class + ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions27/test.desc b/regression/cbmc-java/exceptions27/test.desc index b4d6b49e539..459f879662b 100644 --- a/regression/cbmc-java/exceptions27/test.desc +++ b/regression/cbmc-java/exceptions27/test.desc @@ -1,5 +1,6 @@ CORE test.class + VERIFICATION SUCCESSFUL -- ^warning: ignoring From 6c7949457f640cf25363b8d0ed14b4eb79fd3c1c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 22 Mar 2018 10:23:43 +0000 Subject: [PATCH 8/9] Fix broken static_init_order test descriptions These were trying to match for a blank line, which doesn't occur in the output any more, and was surely not intentionally searched for in the first place. This only causes a problem under Windows (or more likely, under certain versions of Perl), probably due to a change in empty line stripping. --- regression/cbmc-java/static_init_order/test1.desc | 1 - regression/cbmc-java/static_init_order/test2.desc | 1 - 2 files changed, 2 deletions(-) diff --git a/regression/cbmc-java/static_init_order/test1.desc b/regression/cbmc-java/static_init_order/test1.desc index d80e6850004..26702c679cd 100644 --- a/regression/cbmc-java/static_init_order/test1.desc +++ b/regression/cbmc-java/static_init_order/test1.desc @@ -1,7 +1,6 @@ CORE static_init_order.class --function static_init_order.test1 --trace - ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/static_init_order/test2.desc b/regression/cbmc-java/static_init_order/test2.desc index 367eae926c4..9ed5642c7ef 100644 --- a/regression/cbmc-java/static_init_order/test2.desc +++ b/regression/cbmc-java/static_init_order/test2.desc @@ -1,7 +1,6 @@ CORE static_init_order.class --function static_init_order.test2 - ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From 953e2df2cd35e025b5068fcd63c743e694c14de1 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 22 Mar 2018 11:02:37 +0000 Subject: [PATCH 9/9] Enable show-properties with symex-driven lazy loading This can be accommodated using the same post-symex reporting phase as show-goto-functions et al. The one cbmc-java test that uses --show-properties is consequently re-enabled. --- regression/cbmc-java/covered1/test.desc | 30 ++++++++++++++----------- src/jbmc/jbmc_parse_options.cpp | 12 +++++++++- 2 files changed, 28 insertions(+), 14 deletions(-) diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc index fc05584a808..8f6adc9d0a3 100644 --- a/regression/cbmc-java/covered1/test.desc +++ b/regression/cbmc-java/covered1/test.desc @@ -1,19 +1,19 @@ -CORE symex-driven-lazy-loading-expected-failure +CORE covered1.class ---cover location --json-ui --show-properties +--cover location --json-ui --show-properties --function 'covered1.' ^EXIT=0$ ^SIGNAL=0$ .*\"coveredLines\": \"22\",$ -.*\"coveredLines\": \"4\",$ -.*\"coveredLines\": \"6\",$ -.*\"coveredLines\": \"7\",$ -.*\"coveredLines\": \"23\",$ -.*\"coveredLines\": \"24\",$ -.*\"coveredLines\": \"25\",$ -.*\"coveredLines\": \"31\",$ -.*\"coveredLines\": \"32\",$ -.*\"coveredLines\": \"33\",$ -.*\"coveredLines\": \"36\",$ +(.*\"coveredLines\": \"4\")|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"6\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"7\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"23\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"24\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"25\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"31\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"32\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"33\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ +.*\"coveredLines\": \"36\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$ .*\"coveredLines\": \"26\",$ .*\"coveredLines\": \"28\",$ .*\"coveredLines\": \"28\",$ @@ -26,4 +26,8 @@ covered1.class -- ^warning: ignoring -- -This fails with symex-driven lazy loading because it does not currently support --show-properties. +The alternation between the grouped and ungrouped reporting formats for coveredLines accommodates the +difference between symex-driven-lazy-loading (which currently causes jbmc to use the grouped format) +and normal loading (which uses the ungrouped format). +The cause of the difference appears to be symex-driven loading being more pessimistic about possible +exceptions coming from callees, which in turn changes the shape of the CFG. diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index b1aa03b0aa0..eb5ba67b98e 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -384,7 +384,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) for(const char *opt : { "nondet-static", "full-slice", - "show-properties", "lazy-methods" }) { if(cmdline.isset(opt)) @@ -851,6 +850,17 @@ bool jbmc_parse_optionst::show_loaded_functions( return true; } + if(cmdline.isset("show-properties")) + { + namespacet ns(goto_model.get_symbol_table()); + show_properties( + ns, + get_message_handler(), + ui_message_handler.get_ui(), + goto_model.get_goto_functions()); + return true; + } + return false; }