From 9babcdba9cd48cab51306a91a42e427434ba64c1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 25 Aug 2024 13:51:25 -0700 Subject: [PATCH] extract property_checker function This extracts a function for selecting an engine and checking the given properties. The function only performs word-level and bit-level BMC at the moment; code for triggering the other engines will move gradually. --- src/ebmc/Makefile | 1 + src/ebmc/ebmc_base.cpp | 93 ------------------------ src/ebmc/ebmc_base.h | 1 - src/ebmc/ebmc_parse_options.cpp | 7 +- src/ebmc/ebmc_solver_factory.h | 2 +- src/ebmc/property_checker.cpp | 124 ++++++++++++++++++++++++++++++++ src/ebmc/property_checker.h | 21 ++++++ 7 files changed, 153 insertions(+), 96 deletions(-) create mode 100644 src/ebmc/property_checker.cpp create mode 100644 src/ebmc/property_checker.h diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 0c2962ccc..3b1c3159a 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -22,6 +22,7 @@ SRC = \ neural_liveness.cpp \ output_file.cpp \ output_verilog.cpp \ + property_checker.cpp \ random_traces.cpp \ ranking_function.cpp \ report_results.cpp \ diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index 03a5d4944..db81fff0e 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "bmc.h" #include "dimacs_writer.h" #include "ebmc_error.h" #include "ebmc_solver_factory.h" @@ -470,95 +469,3 @@ int ebmc_baset::do_compute_ct() return 0; } - -/*******************************************************************\ - -Function: ebmc_baset::do_word_level_bmc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int ebmc_baset::do_word_level_bmc() -{ - auto solver_factory = ebmc_solver_factory(cmdline); - - bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") || - cmdline.isset("show-formula"); - - int result = 0; - - try - { - if(cmdline.isset("max-bound")) - { - if(convert_only) - throw "please set a specific bound"; - - const std::size_t max_bound = - unsafe_string2size_t(cmdline.get_value("max-bound")); - - for(bound = 1; bound <= max_bound; bound++) - { - message.status() << "Doing BMC with bound " << bound << messaget::eom; - -#if 0 - const namespacet ns(transition_system.symbol_table); - CHECK_RETURN(trans_expr.has_value()); - ::unwind(*trans_expr, *message_handler, solver, bound+1, ns, true); - result=finish_word_level_bmc(solver); -#endif - } - - const namespacet ns(transition_system.symbol_table); - report_results(cmdline, properties, ns, message.get_message_handler()); - } - else - { - if(get_bound()) - return 1; - - if(!convert_only) - if(properties.properties.empty()) - throw "no properties"; - - bmc( - bound, - convert_only, - transition_system, - properties, - solver_factory, - message.get_message_handler()); - - if(!convert_only) - { - const namespacet ns(transition_system.symbol_table); - report_results(cmdline, properties, ns, message.get_message_handler()); - result = properties.exit_code(); - } - } - } - - 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; -} diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h index 2f878269a..e10ee5e75 100644 --- a/src/ebmc/ebmc_base.h +++ b/src/ebmc/ebmc_base.h @@ -64,7 +64,6 @@ class ebmc_baset public: int do_compute_ct(); int do_bit_level_bmc(); - int do_word_level_bmc(); }; #endif diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index f9a3bef7a..3f6506c48 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "k_induction.h" #include "liveness_to_safety.h" #include "neural_liveness.h" +#include "property_checker.h" #include "random_traces.h" #include "ranking_function.h" #include "show_trans.h" @@ -306,7 +307,11 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("aig") || cmdline.isset("dimacs")) return ebmc_base.do_bit_level_bmc(); else - return ebmc_base.do_word_level_bmc(); // default + 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/ebmc_solver_factory.h b/src/ebmc/ebmc_solver_factory.h index 82915c444..7cb956bfc 100644 --- a/src/ebmc/ebmc_solver_factory.h +++ b/src/ebmc/ebmc_solver_factory.h @@ -16,7 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include +#include #include class ebmc_solvert final diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp new file mode 100644 index 000000000..b2f1538ed --- /dev/null +++ b/src/ebmc/property_checker.cpp @@ -0,0 +1,124 @@ +/*******************************************************************\ + +Module: EBMC Property Checker + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "property_checker.h" + +#include + +#include "bmc.h" +#include "ebmc_error.h" +#include "ebmc_solver_factory.h" +#include "report_results.h" + +int word_level_bmc( + const cmdlinet &cmdline, + const transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + auto solver_factory = ebmc_solver_factory(cmdline); + + bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") || + cmdline.isset("show-formula"); + + int result = 0; + + try + { + if(cmdline.isset("max-bound")) + { + if(convert_only) + throw ebmc_errort() << "please set a specific bound"; + + const std::size_t max_bound = + unsafe_string2size_t(cmdline.get_value("max-bound")); + + for(std::size_t bound = 1; bound <= max_bound; bound++) + { + messaget message{message_handler}; + message.status() << "Doing BMC with bound " << bound << messaget::eom; + +#if 0 + const namespacet ns(transition_system.symbol_table); + CHECK_RETURN(trans_expr.has_value()); + ::unwind(*trans_expr, *message_handler, solver, bound+1, ns, true); + result=finish_word_level_bmc(solver); +#endif + } + + const namespacet ns(transition_system.symbol_table); + report_results(cmdline, properties, ns, message_handler); + } + else + { + std::size_t bound; + + if(cmdline.isset("bound")) + { + bound = unsafe_string2unsigned(cmdline.get_value("bound")); + } + else + { + messaget message{message_handler}; + message.warning() << "using default bound 1" << messaget::eom; + bound = 1; + } + + if(!convert_only) + if(properties.properties.empty()) + throw "no properties"; + + bmc( + bound, + convert_only, + transition_system, + properties, + solver_factory, + message_handler); + + if(!convert_only) + { + const namespacet ns(transition_system.symbol_table); + report_results(cmdline, properties, ns, message_handler); + result = properties.exit_code(); + } + } + } + + 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 property_checker( + const cmdlinet &cmdline, + const 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); +} diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h new file mode 100644 index 000000000..3a8f289a4 --- /dev/null +++ b/src/ebmc/property_checker.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: EBMC Property Checker + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_PROPERTY_CHECKER_H +#define CPROVER_EBMC_PROPERTY_CHECKER_H + +#include "ebmc_properties.h" +#include "transition_system.h" + +int property_checker( + const cmdlinet &, + const transition_systemt &, + ebmc_propertiest &, + message_handlert &); + +#endif