From ef0f09358632576a24a5de90ed1d2fe2b95fcdb8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 15 Jan 2019 18:27:37 +0000 Subject: [PATCH 1/7] Do collect properties from inlined functions They are not inlined using goto_partial_inline anymore. --- src/goto-checker/properties.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 58de8528ba1..49a23ce9a86 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 From 661a39c1558e06c47788749d50a263d47b5acc8c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 15:15:13 +0000 Subject: [PATCH 2/7] Allow UNKNOWN as neutral element in property status updates --- src/goto-checker/properties.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 49a23ce9a86..26126526b3a 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -166,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: From c3e5f4ed6ba4bb1debc7aca21ca99b52ae57066d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Dec 2018 12:49:30 +0000 Subject: [PATCH 3/7] Add properties_result_from_symex_target_equation Updates the property infos with properties created by goto-symex and sets the status of already determined properies. --- src/goto-checker/bmc_util.cpp | 50 +++++++++++++++++++++++++++++++++++ src/goto-checker/bmc_util.h | 9 +++++++ 2 files changed, 59 insertions(+) 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)" \ From 79bde98f9f0f2199a610962678082861f204ed1a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 11:47:21 +0000 Subject: [PATCH 4/7] Add multi path symex only checker multi_path_symex_only_checkert is a bounded model checking algorithm that determines the status of properties through symbolic execution and constant propagation. I.e. it doesn't call the SAT solver. If desired CBMC could expose this to support a symex-only BMC algorithm. For now, this is used to implement show-vcc and program-only (which are rather orthogonal to the BMC algorithm used, but currently assume symex-only). --- src/goto-checker/Makefile | 1 + .../multi_path_symex_only_checker.cpp | 98 +++++++++++++++++++ .../multi_path_symex_only_checker.h | 41 ++++++++ 3 files changed, 140 insertions(+) create mode 100644 src/goto-checker/multi_path_symex_only_checker.cpp create mode 100644 src/goto-checker/multi_path_symex_only_checker.h 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/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 From f1c6488aa17d774cb675702c6ca915aeb1f0f06d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 23 Sep 2018 18:07:18 +0100 Subject: [PATCH 5/7] Use goto verifier for program-only and show-vcc in CBMC --- src/cbmc/cbmc_parse_options.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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); } From 1b8f38b9ee4501d17d78ff478850176332fdeedf Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 14:39:47 +0000 Subject: [PATCH 6/7] Goto checkers for Java require further preprocessing --- jbmc/src/java_bytecode/Makefile | 1 + jbmc/src/java_bytecode/java_bmc_util.cpp | 41 +++++++++++++++++++ jbmc/src/java_bytecode/java_bmc_util.h | 25 +++++++++++ .../java_multi_path_symex_only_checker.h | 33 +++++++++++++++ 4 files changed, 100 insertions(+) create mode 100644 jbmc/src/java_bytecode/java_bmc_util.cpp create mode 100644 jbmc/src/java_bytecode/java_bmc_util.h create mode 100644 jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h 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 From 380945460556b05f37d05a80de2219c022f28096 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 13 Jan 2019 17:26:44 +0000 Subject: [PATCH 7/7] Use goto verifier for program-only and show-vcc in JBMC --- jbmc/src/java_bytecode/module_dependencies.txt | 1 + jbmc/src/jbmc/jbmc_parse_options.cpp | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) 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(