diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index ea2a100d6d3..066a67240da 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -7,6 +7,7 @@ SRC = bytecode_info.cpp \ generic_parameter_specialization_map_keys.cpp \ jar_file.cpp \ jar_pool.cpp \ + java_bmc_util.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ java_bytecode_concurrency_instrumentation.cpp \ diff --git a/jbmc/src/java_bytecode/java_bmc_util.cpp b/jbmc/src/java_bytecode/java_bmc_util.cpp new file mode 100644 index 00000000000..99a9312ec52 --- /dev/null +++ b/jbmc/src/java_bytecode/java_bmc_util.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utils for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Bounded Model Checking Utils for Java + +#include "java_bmc_util.h" + +#include +#include +#include + +void java_setup_symex( + const optionst &options, + abstract_goto_modelt &goto_model, + symex_bmct &symex) +{ + // unwinds loops to number of enum elements + if(options.get_bool_option("java-unwind-enum-static")) + { + // clang-format off + // (it asks for the body to be at the same indent level as the parameters + // for some reason) + symex.add_loop_unwind_handler( + [&goto_model]( + const goto_symex_statet::call_stackt &context, + unsigned loop_num, + unsigned unwind, + unsigned &max_unwind) + { // NOLINT (*) + return java_enum_static_init_unwind_handler( + context, loop_num, unwind, max_unwind, goto_model.get_symbol_table()); + }); + // clang-format on + } +} diff --git a/jbmc/src/java_bytecode/java_bmc_util.h b/jbmc/src/java_bytecode/java_bmc_util.h new file mode 100644 index 00000000000..d21a21d7c4f --- /dev/null +++ b/jbmc/src/java_bytecode/java_bmc_util.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utils for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Bounded Model Checking Utils for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H +#define CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H + +class abstract_goto_modelt; +class optionst; +class symex_bmct; + +/// Registers Java-specific preprocessing handlers with goto-symex +void java_setup_symex( + const optionst &options, + abstract_goto_modelt &goto_model, + symex_bmct &symex); + +#endif // CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H diff --git a/jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h b/jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h new file mode 100644 index 00000000000..203abb82643 --- /dev/null +++ b/jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + +Module: Goto Checker using Bounded Model Checking for Java + +Author: Daniel Kroening, Peter Schrammel + + \*******************************************************************/ + +/// \file +/// Goto Checker using Bounded Model Checking for Java + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H +#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H + +#include + +#include "java_bmc_util.h" + +class java_multi_path_symex_only_checkert + : public multi_path_symex_only_checkert +{ +public: + java_multi_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : multi_path_symex_only_checkert(options, ui_message_handler, goto_model) + { + java_setup_symex(options, goto_model, symex); + } +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H diff --git a/jbmc/src/java_bytecode/module_dependencies.txt b/jbmc/src/java_bytecode/module_dependencies.txt index f011bcc8b52..5dd468c7cd5 100644 --- a/jbmc/src/java_bytecode/module_dependencies.txt +++ b/jbmc/src/java_bytecode/module_dependencies.txt @@ -1,5 +1,6 @@ analyses ansi-c # should go away +goto-checker goto-programs java_bytecode json diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 21ee7b91415..1e175a0489e 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -27,6 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include #include #include @@ -60,6 +62,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -563,6 +566,19 @@ int jbmc_parse_optionst::doit() goto_model.validate(validation_modet::INVARIANT); } + if( + options.get_bool_option("program-only") || + options.get_bool_option("show-vcc")) + { + if(!options.get_bool_option("paths")) + { + all_properties_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + return CPROVER_EXIT_SUCCESS; + } + } + // The `configure_bmc` callback passed will enable enum-unwind-static if // applicable. return bmct::do_language_agnostic_bmc( diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c1db43c5546..90aa52ea8c0 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -30,7 +30,10 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include +#include +#include #include #include @@ -553,6 +556,19 @@ int cbmc_parse_optionst::doit() goto_model.validate(validation_modet::INVARIANT); } + if( + options.get_bool_option("program-only") || + options.get_bool_option("show-vcc")) + { + if(!options.get_bool_option("paths")) + { + all_properties_verifiert verifier( + options, ui_message_handler, goto_model); + (void)verifier(); + return CPROVER_EXIT_SUCCESS; + } + } + return bmct::do_language_agnostic_bmc( options, goto_model, ui_message_handler); } diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 650944f72db..cc295d54732 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -1,6 +1,7 @@ SRC = bmc_util.cpp \ incremental_goto_checker.cpp \ goto_verifier.cpp \ + multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ solver_factory.cpp \ diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index b8b2279ed87..39f12454f7a 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -225,3 +225,53 @@ void slice( << " remaining after simplification" << messaget::eom; } +std::vector update_properties_status_from_symex_target_equation( + propertiest &properties, + const symex_target_equationt &equation) +{ + std::vector updated_properties; + + for(const auto &step : equation.SSA_steps) + { + if(!step.is_assert()) + continue; + + irep_idt property_id = step.get_property_id(); + + if(property_id.empty()) + continue; + + // Don't set false properties; we wouldn't have traces for them. + const auto status = step.cond_expr.is_true() ? property_statust::PASS + : property_statust::UNKNOWN; + auto emplace_result = properties.emplace( + property_id, property_infot{step.source.pc, step.comment, status}); + + if(emplace_result.second) + { + updated_properties.push_back(property_id); + } + else + { + property_infot &property_info = emplace_result.first->second; + property_statust old_status = property_info.status; + property_info.status |= status; + + if(property_info.status != old_status) + updated_properties.push_back(property_id); + } + } + + for(auto &property_pair : properties) + { + if(property_pair.second.status == property_statust::NOT_CHECKED) + { + // This could be a NOT_CHECKED, NOT_REACHABLE or PASS, + // but the equation doesn't give us precise information. + property_pair.second.status = property_statust::PASS; + updated_properties.push_back(property_pair.first); + } + } + + return updated_properties; +} diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 8ccb81e7df7..b8e85a6effb 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel #include +#include "properties.h" + class goto_tracet; class memory_model_baset; class message_handlert; @@ -67,6 +69,13 @@ void slice( const optionst &, ui_message_handlert &); +/// Sets property status to PASS for properties whose +/// conditions are constant true. +/// \return IDs of updated properties +std::vector update_properties_status_from_symex_target_equation( + propertiest &properties, + const symex_target_equationt &equation); + // clang-format off #define OPT_BMC \ "(program-only)" \ diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp new file mode 100644 index 00000000000..bea03d22eda --- /dev/null +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -0,0 +1,98 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution Only + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) + +#include "multi_path_symex_only_checker.h" + +#include + +#include +#include +#include + +#include "bmc_util.h" + +multi_path_symex_only_checkert::multi_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : incremental_goto_checkert(options, ui_message_handler), + goto_model(goto_model), + ns(goto_model.get_symbol_table(), symex_symbol_table), + symex( + ui_message_handler, + goto_model.get_symbol_table(), + equation, + options, + path_storage) +{ + setup_symex(symex, ns, options, ui_message_handler); +} + +incremental_goto_checkert::resultt multi_path_symex_only_checkert:: +operator()(propertiest &properties) +{ + perform_symex(); + + output_coverage_report(); + + if(options.get_bool_option("show-vcc")) + { + show_vcc(options, ui_message_handler, equation); + } + + if(options.get_bool_option("program-only")) + { + show_program(ns, equation); + } + + return resultt( + resultt::progresst::DONE, + update_properties_status_from_symex_target_equation(properties, equation)); +} + +void multi_path_symex_only_checkert::perform_symex() +{ + auto get_goto_function = + [this](const irep_idt &id) -> const goto_functionst::goto_functiont & { + return goto_model.get_goto_function(id); + }; + + // perform symbolic execution + symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table); + + // add a partial ordering, if required + // We won't be able to decide any properties by adding this, + // but we'd like to see the entire SSA. + if(equation.has_threads()) + { + std::unique_ptr memory_model = + get_memory_model(options, ns); + memory_model->set_message_handler(ui_message_handler); + (*memory_model)(equation); + } + + log.statistics() << "size of program expression: " + << equation.SSA_steps.size() << " steps" << messaget::eom; + + slice(symex, equation, ns, options, ui_message_handler); +} + +void multi_path_symex_only_checkert::output_coverage_report() +{ + std::string cov_out = options.get_option("symex-coverage-report"); + if( + !cov_out.empty() && + symex.output_coverage_report(goto_model.get_goto_functions(), cov_out)) + { + log.error() << "Failed to write symex coverage report to '" << cov_out + << "'" << messaget::eom; + } +} diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h new file mode 100644 index 00000000000..ba05aaef730 --- /dev/null +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution only + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) + +#ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H +#define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H + +#include "incremental_goto_checker.h" + +#include "symex_bmc.h" + +class multi_path_symex_only_checkert : public incremental_goto_checkert +{ +public: + multi_path_symex_only_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + resultt operator()(propertiest &) override; + +protected: + abstract_goto_modelt &goto_model; + symbol_tablet symex_symbol_table; + namespacet ns; + symex_target_equationt equation; + path_fifot path_storage; // should go away + symex_bmct symex; + + void perform_symex(); + void output_coverage_report(); +}; + +#endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 58de8528ba1..26126526b3a 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -69,10 +69,6 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model) const auto &goto_functions = goto_model.get_goto_functions(); for(const auto &function_pair : goto_functions.function_map) { - // don't collect properties from inlined functions - if(function_pair.second.is_inlined()) - continue; - const goto_programt &goto_program = function_pair.second.body; // need pointer to goto instruction @@ -170,10 +166,14 @@ bool has_properties_to_check(const propertiest &properties) property_statust &operator|=(property_statust &a, property_statust const &b) { // non-monotonic use is likely a bug + // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL + // clang-format off PRECONDITION( a == property_statust::NOT_CHECKED || (a == property_statust::UNKNOWN && b != property_statust::NOT_CHECKED) || + b == property_statust::UNKNOWN || a == b); + // clang-format on switch(a) { case property_statust::NOT_CHECKED: