From a59dcd55c564bb827cddba3fd6b8c4dbdfefc439 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 27 Aug 2024 11:48:37 -0700 Subject: [PATCH] move bit-level BMC to property_checker This moves the bit-level BMC engine invocation from ebmc_baset to property_checker(...). --- src/ebmc/ebmc_base.cpp | 267 ------------------------------ src/ebmc/ebmc_base.h | 7 - src/ebmc/ebmc_parse_options.cpp | 13 +- src/ebmc/property_checker.cpp | 276 +++++++++++++++++++++++++++++++- src/ebmc/property_checker.h | 2 +- 5 files changed, 278 insertions(+), 287 deletions(-) diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index db81fff0e..954ef2a4c 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -10,27 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include #include #include #include -#include -#include -#include -#include -#include "dimacs_writer.h" #include "ebmc_error.h" -#include "ebmc_solver_factory.h" #include "ebmc_version.h" -#include "output_file.h" -#include "report_results.h" -#include #include /*******************************************************************\ @@ -54,260 +41,6 @@ ebmc_baset::ebmc_baset( /*******************************************************************\ -Function: ebmc_baset::finish_bit_level_bmc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver) -{ - auto sat_start_time = std::chrono::steady_clock::now(); - - message.status() << "Solving with " << solver.solver_text() << messaget::eom; - - for(propertyt &property : properties.properties) - { - if(property.is_disabled()) - continue; - - if(property.is_failure()) - continue; - - if(property.is_assumed()) - continue; - - message.status() << "Checking " << property.name << messaget::eom; - - literalt property_literal=!solver.land(property.timeframe_literals); - - bvt assumptions; - assumptions.push_back(property_literal); - - propt::resultt prop_result = solver.prop_solve(assumptions); - - switch(prop_result) - { - case propt::resultt::P_SATISFIABLE: - { - property.refuted(); - message.result() << "SAT: counterexample found" << messaget::eom; - - namespacet ns(transition_system.symbol_table); - - property.witness_trace = - compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns); - } - break; - - case propt::resultt::P_UNSATISFIABLE: - message.result() << "UNSAT: No counterexample found within bound" - << messaget::eom; - property.proved_with_bound(bound); - break; - - case propt::resultt::P_ERROR: - message.error() << "Error from decision procedure" << messaget::eom; - return 2; - - default: - message.error() << "Unexpected result from decision procedure" - << messaget::eom; - return 1; - } - } - - auto sat_stop_time = std::chrono::steady_clock::now(); - - message.statistics() - << "Solver time: " - << std::chrono::duration(sat_stop_time - sat_start_time).count() - << messaget::eom; - - return properties.exit_code(); -} - -/*******************************************************************\ - -Function: ebmc_baset::get_bound - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool ebmc_baset::get_bound() -{ - if(!cmdline.isset("bound")) - { - message.warning() << "using default bound 1" << messaget::eom; - bound=1; - return false; - } - - bound=unsafe_string2unsigned(cmdline.get_value("bound")); - - return false; -} - -/*******************************************************************\ - -Function: ebmc_baset::do_bit_level_bmc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only) -{ - if(get_bound()) return 1; - - int result; - - try - { - bmc_mapt bmc_map; - - if(!convert_only) - if(properties.properties.empty()) - throw "no properties"; - - netlistt netlist; - if(make_netlist(netlist)) - throw 0; - - message.status() << "Unwinding Netlist" << messaget::eom; - - bmc_map.map_timeframes(netlist, bound+1, solver); - - ::unwind(netlist, bmc_map, message, solver); - - const namespacet ns(transition_system.symbol_table); - - // convert the properties - for(propertyt &property : properties.properties) - { - if(property.is_disabled()) - continue; - - if(!netlist_bmc_supports_property(property.normalized_expr)) - { - property.failure("property not supported by netlist BMC engine"); - continue; - } - - // look up the property in the netlist - auto netlist_property = netlist.properties.find(property.identifier); - CHECK_RETURN(netlist_property != netlist.properties.end()); - - ::unwind_property( - netlist_property->second, bmc_map, property.timeframe_literals); - - if(property.is_assumed()) - { - // force these to be true - for(auto l : property.timeframe_literals) - solver.l_set_to(l, true); - } - else - { - // freeze for incremental usage - for(auto l : property.timeframe_literals) - solver.set_frozen(l); - } - } - - if(convert_only) - result=0; - else - { - result = finish_bit_level_bmc(bmc_map, solver); - report_results(cmdline, properties, ns, message.get_message_handler()); - } - } - - catch(const char *e) - { - message.error() << e << messaget::eom; - return 10; - } - - catch(const std::string &e) - { - message.error() << e << messaget::eom; - return 10; - } - - catch(int) - { - return 10; - } - - return result; -} - -/*******************************************************************\ - -Function: ebmc_baset::do_bit_level_bmc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int ebmc_baset::do_bit_level_bmc() -{ - if(cmdline.isset("dimacs")) - { - if(cmdline.isset("outfile")) - { - auto outfile = output_filet{cmdline.get_value("outfile")}; - - message.status() << "Writing DIMACS CNF to `" << outfile.name() << "'" - << messaget::eom; - - dimacs_cnf_writert dimacs_cnf_writer{ - outfile.stream(), message.get_message_handler()}; - - return do_bit_level_bmc(dimacs_cnf_writer, true); - } - else - { - dimacs_cnf_writert dimacs_cnf_writer{ - std::cout, message.get_message_handler()}; - - return do_bit_level_bmc(dimacs_cnf_writer, true); - } - } - else - { - if(cmdline.isset("outfile")) - throw ebmc_errort() - << "Cannot write to outfile without file format option"; - - satcheckt satcheck{message.get_message_handler()}; - - message.status() << "Using " << satcheck.solver_text() << messaget::eom; - - return do_bit_level_bmc(satcheck, false); - } -} -/*******************************************************************\ - Function: ebmc_baset::get_properties Inputs: diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h index e10ee5e75..9d6ab6c5e 100644 --- a/src/ebmc/ebmc_base.h +++ b/src/ebmc/ebmc_base.h @@ -43,12 +43,6 @@ class ebmc_baset messaget message; const cmdlinet &cmdline; - bool get_bound(); - - // bit-level - int do_bit_level_bmc(cnft &solver, bool convert_only); - int finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver); - bool parse_property(const std::string &property); bool get_model_properties(); void show_properties(); @@ -63,7 +57,6 @@ class ebmc_baset public: int do_compute_ct(); - int do_bit_level_bmc(); }; #endif diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 3f6506c48..79c7dddba 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -304,14 +304,11 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("compute-ct")) return ebmc_base.do_compute_ct(); - if(cmdline.isset("aig") || cmdline.isset("dimacs")) - return ebmc_base.do_bit_level_bmc(); - else - return property_checker( - cmdline, - ebmc_base.transition_system, - ebmc_base.properties, - ui_message_handler); + return property_checker( + cmdline, + ebmc_base.transition_system, + ebmc_base.properties, + ui_message_handler); } } catch(const ebmc_errort &ebmc_error) diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index b2f1538ed..d4fc20505 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -10,11 +10,21 @@ Author: Daniel Kroening, dkr@amazon.com #include +#include +#include +#include +#include + #include "bmc.h" +#include "dimacs_writer.h" #include "ebmc_error.h" #include "ebmc_solver_factory.h" +#include "output_file.h" #include "report_results.h" +#include +#include + int word_level_bmc( const cmdlinet &cmdline, const transition_systemt &transition_system, @@ -112,13 +122,271 @@ int word_level_bmc( return result; } +int finish_bit_level_bmc( + std::size_t bound, + const bmc_mapt &bmc_map, + propt &solver, + const transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + auto sat_start_time = std::chrono::steady_clock::now(); + + messaget message{message_handler}; + message.status() << "Solving with " << solver.solver_text() << messaget::eom; + + for(auto &property : properties.properties) + { + if(property.is_disabled()) + continue; + + if(property.is_failure()) + continue; + + if(property.is_assumed()) + continue; + + message.status() << "Checking " << property.name << messaget::eom; + + literalt property_literal = !solver.land(property.timeframe_literals); + + bvt assumptions; + assumptions.push_back(property_literal); + + propt::resultt prop_result = solver.prop_solve(assumptions); + + switch(prop_result) + { + case propt::resultt::P_SATISFIABLE: + { + property.refuted(); + message.result() << "SAT: counterexample found" << messaget::eom; + + namespacet ns{transition_system.symbol_table}; + + property.witness_trace = + compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns); + } + break; + + case propt::resultt::P_UNSATISFIABLE: + message.result() << "UNSAT: No counterexample found within bound" + << messaget::eom; + property.proved_with_bound(bound); + break; + + case propt::resultt::P_ERROR: + message.error() << "Error from decision procedure" << messaget::eom; + return 2; + + default: + message.error() << "Unexpected result from decision procedure" + << messaget::eom; + return 1; + } + } + + auto sat_stop_time = std::chrono::steady_clock::now(); + + message.statistics() + << "Solver time: " + << std::chrono::duration(sat_stop_time - sat_start_time).count() + << messaget::eom; + + return properties.exit_code(); +} + +int bit_level_bmc( + cnft &solver, + bool convert_only, + const cmdlinet &cmdline, + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + messaget message{message_handler}; + + std::size_t bound; + + if(cmdline.isset("bound")) + { + bound = unsafe_string2unsigned(cmdline.get_value("bound")); + } + else + { + message.warning() << "using default bound 1" << messaget::eom; + bound = 1; + } + + int result; + + try + { + bmc_mapt bmc_map; + + if(!convert_only) + if(properties.properties.empty()) + throw "no properties"; + + // make net-list + netlistt netlist; + message.status() << "Generating Netlist" << messaget::eom; + + convert_trans_to_netlist( + transition_system.symbol_table, + transition_system.main_symbol->name, + properties.make_property_map(), + netlist, + message.get_message_handler()); + + message.statistics() << "Latches: " << netlist.var_map.latches.size() + << ", nodes: " << netlist.number_of_nodes() + << messaget::eom; + + messaget message{message_handler}; + message.status() << "Unwinding Netlist" << messaget::eom; + + bmc_map.map_timeframes(netlist, bound + 1, solver); + + ::unwind(netlist, bmc_map, message, solver); + + const namespacet ns(transition_system.symbol_table); + + // convert the properties + for(auto &property : properties.properties) + { + if(property.is_disabled()) + continue; + + if(!netlist_bmc_supports_property(property.normalized_expr)) + { + property.failure("property not supported by netlist BMC engine"); + continue; + } + + // look up the property in the netlist + auto netlist_property = netlist.properties.find(property.identifier); + CHECK_RETURN(netlist_property != netlist.properties.end()); + + ::unwind_property( + netlist_property->second, bmc_map, property.timeframe_literals); + + if(property.is_assumed()) + { + // force these to be true + for(auto l : property.timeframe_literals) + solver.l_set_to(l, true); + } + else + { + // freeze for incremental usage + for(auto l : property.timeframe_literals) + solver.set_frozen(l); + } + } + + if(convert_only) + result = 0; + else + { + result = finish_bit_level_bmc( + bound, bmc_map, solver, transition_system, properties, message_handler); + report_results(cmdline, properties, ns, message_handler); + } + } + + catch(const char *e) + { + messaget message{message_handler}; + message.error() << e << messaget::eom; + return 10; + } + + catch(const std::string &e) + { + messaget message{message_handler}; + message.error() << e << messaget::eom; + return 10; + } + + catch(int) + { + return 10; + } + + return result; +} + +int bit_level_bmc( + const cmdlinet &cmdline, + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + if(cmdline.isset("dimacs")) + { + if(cmdline.isset("outfile")) + { + auto outfile = output_filet{cmdline.get_value("outfile")}; + + messaget message{message_handler}; + message.status() << "Writing DIMACS CNF to `" << outfile.name() << "'" + << messaget::eom; + + dimacs_cnf_writert dimacs_cnf_writer{outfile.stream(), message_handler}; + + return bit_level_bmc( + dimacs_cnf_writer, + true, + cmdline, + transition_system, + properties, + message_handler); + } + else + { + dimacs_cnf_writert dimacs_cnf_writer{std::cout, message_handler}; + + return bit_level_bmc( + dimacs_cnf_writer, + true, + cmdline, + transition_system, + properties, + message_handler); + } + } + else + { + if(cmdline.isset("outfile")) + throw ebmc_errort() + << "Cannot write to outfile without file format option"; + + satcheckt satcheck{message_handler}; + + messaget message{message_handler}; + message.status() << "Using " << satcheck.solver_text() << messaget::eom; + + return bit_level_bmc( + satcheck, false, cmdline, transition_system, properties, message_handler); + } +} + int property_checker( const cmdlinet &cmdline, - const transition_systemt &transition_system, + transition_systemt &transition_system, ebmc_propertiest &properties, message_handlert &message_handler) { - // default engine is word-level BMC - return word_level_bmc( - cmdline, transition_system, properties, message_handler); + if(cmdline.isset("aig") || cmdline.isset("dimacs")) + { + return bit_level_bmc( + cmdline, transition_system, properties, message_handler); + } + else + { + // default engine is word-level BMC + return word_level_bmc( + cmdline, transition_system, properties, message_handler); + } } diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h index 3a8f289a4..8de660a71 100644 --- a/src/ebmc/property_checker.h +++ b/src/ebmc/property_checker.h @@ -14,7 +14,7 @@ Author: Daniel Kroening, dkr@amazon.com int property_checker( const cmdlinet &, - const transition_systemt &, + transition_systemt &, ebmc_propertiest &, message_handlert &);