From f087eaa15b64cca94edb097743dfc0b3ec028d2d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 18 Oct 2023 05:58:26 -0700 Subject: [PATCH 1/2] ebmc: re-enable --cegar This resurrects the defunct CEGAR implementation in ebmc. --- src/ebmc/cegar/bmc_cegar.cpp | 33 ++++++++---------------- src/ebmc/cegar/bmc_cegar.h | 45 ++++++++++++++++++++------------- src/ebmc/cegar/simulate.cpp | 15 +++++++++-- src/ebmc/ebmc_base.h | 3 ++- src/ebmc/ebmc_parse_options.cpp | 32 ++++++++--------------- 5 files changed, 64 insertions(+), 64 deletions(-) diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp index 84f8ebae..5230557f 100644 --- a/src/ebmc/cegar/bmc_cegar.cpp +++ b/src/ebmc/cegar/bmc_cegar.cpp @@ -31,9 +31,7 @@ Function: bmc_cegart::bmc_cegar void bmc_cegart::bmc_cegar() { - make_netlist(); - - if(properties.empty()) + if(properties.properties.empty()) { error() << "No properties given" << eom; return; @@ -213,7 +211,7 @@ void bmc_cegart::cegar_loop() /*******************************************************************\ -Function: bmc_cegart::make_netlist +Function: do_bmc_cegar Inputs: @@ -223,25 +221,14 @@ Function: bmc_cegart::make_netlist \*******************************************************************/ -void bmc_cegart::make_netlist() +int do_bmc_cegar( + const netlistt &netlist, + ebmc_propertiest &properties, + const namespacet &ns, + message_handlert &message_handler) { - // make net-list - status() << "Making Netlist" << eom; - - try - { - convert_trans_to_netlist( - symbol_table, main_module, - concrete_netlist, get_message_handler()); - } - - catch(const std::string &error_msg) - { - error() << error_msg << eom; - return; - } + bmc_cegart bmc_cegar(netlist, properties, ns, message_handler); - statistics() - << "Latches: " << concrete_netlist.var_map.latches.size() - << ", nodes: " << concrete_netlist.number_of_nodes() << eom; + bmc_cegar.bmc_cegar(); + return 0; } diff --git a/src/ebmc/cegar/bmc_cegar.h b/src/ebmc/cegar/bmc_cegar.h index 50cd2daf..02c280a2 100644 --- a/src/ebmc/cegar/bmc_cegar.h +++ b/src/ebmc/cegar/bmc_cegar.h @@ -6,10 +6,15 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include +#ifndef EBMC_CEGAR_BMC_CEGAR_H +#define EBMC_CEGAR_BMC_CEGAR_H + #include #include +#include +#include +#include #include #include @@ -17,36 +22,30 @@ class bmc_cegart:public messaget { public: bmc_cegart( - symbol_table_baset &_symbol_table, - const irep_idt &_main_module, - message_handlert &_message_handler, - const std::list &_properties) + const netlistt &_netlist, + ebmc_propertiest &_properties, + const namespacet &_ns, + message_handlert &_message_handler) : messaget(_message_handler), - symbol_table(_symbol_table), - ns(_symbol_table), - main_module(_main_module), - properties(_properties) + properties(_properties), + concrete_netlist(_netlist), + ns(_ns) { } void bmc_cegar(); protected: - symbol_table_baset &symbol_table; - const namespacet ns; - const irep_idt &main_module; - const std::list &properties; - + ebmc_propertiest &properties; bmc_mapt bmc_map; netlistt concrete_netlist, abstract_netlist; + const namespacet &ns; bool initial_abstraction; typedef std::set cut_pointst; cut_pointst cut_points; - - void make_netlist(); - + void cegar_loop(); void abstract(); @@ -62,3 +61,15 @@ class bmc_cegart:public messaget std::list prop_bv; }; + +class ebmc_propertiest; +class message_handlert; +class netlistt; + +int do_bmc_cegar( + const netlistt &, + ebmc_propertiest &, + const namespacet &, + message_handlert &); + +#endif // EBMC_CEGAR_BMC_CEGAR_H diff --git a/src/ebmc/cegar/simulate.cpp b/src/ebmc/cegar/simulate.cpp index 5a791ab5..de9e8f37 100644 --- a/src/ebmc/cegar/simulate.cpp +++ b/src/ebmc/cegar/simulate.cpp @@ -41,8 +41,19 @@ bool bmc_cegart::simulate(unsigned bound) case propt::resultt::P_SATISFIABLE: status() << "SAT: bug found within bound" << eom; - show_counterexample(properties, prop_bv, get_message_handler(), solver, - bmc_map, ns); + { + std::list property_expr_list; + for(auto &p : properties.properties) + property_expr_list.push_back(p.expr); + + show_counterexample( + property_expr_list, + prop_bv, + get_message_handler(), + solver, + bmc_map, + ns); + } return true; case propt::resultt::P_UNSATISFIABLE: diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h index dc62d8ae..2726fc35 100644 --- a/src/ebmc/ebmc_base.h +++ b/src/ebmc/ebmc_base.h @@ -37,6 +37,8 @@ class ebmc_baset bool make_netlist(netlistt &); transition_systemt transition_system; + + using propertyt = ebmc_propertiest::propertyt; ebmc_propertiest properties; protected: @@ -58,7 +60,6 @@ class ebmc_baset bool typecheck(); std::size_t bound; - using propertyt = ebmc_propertiest::propertyt; public: int do_compute_ct(); diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 5559b3ec..ca02819d 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -28,6 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "cegar/bmc_cegar.h" + #ifdef HAVE_INTERPOLATION #include "interpolation/interpolation_expr.h" #include "interpolation/interpolation_netlist.h" @@ -112,26 +114,6 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("show-symbol-table")) return show_symbol_table(cmdline, ui_message_handler); - if(cmdline.isset("cegar")) - { - throw ebmc_errort() << "This option is currently disabled"; - -#if 0 - namespacet ns(symbol_table); - var_mapt var_map(symbol_table, main_symbol->name); - - bmc_cegart bmc_cegar( - var_map, - *trans_expr, - ns, - *this, - prop_expr_list); - - bmc_cegar.bmc_cegar(); - return 0; -#endif - } - if(cmdline.isset("coverage")) { throw ebmc_errort() << "This option is currently disabled"; @@ -292,7 +274,15 @@ int ebmc_parse_optionst::doit() if(result != -1) return result; - if(cmdline.isset("compute-ct")) + if(cmdline.isset("cegar")) + { + netlistt netlist; + ebmc_base.make_netlist(netlist); + const namespacet ns(ebmc_base.transition_system.symbol_table); + return do_bmc_cegar( + netlist, ebmc_base.properties, ns, ui_message_handler); + } + else if(cmdline.isset("compute-ct")) return ebmc_base.do_compute_ct(); // possibly apply liveness-to-safety From 2a6d0ff378d66ea587df725ae8e84727bd62fd79 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 18 Oct 2023 06:05:08 -0700 Subject: [PATCH 2/2] ebmc: add a basic test for CEGAR --- regression/ebmc/cegar/basic1.desc | 6 ++++++ regression/ebmc/cegar/basic1.sv | 12 ++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 regression/ebmc/cegar/basic1.desc create mode 100644 regression/ebmc/cegar/basic1.sv diff --git a/regression/ebmc/cegar/basic1.desc b/regression/ebmc/cegar/basic1.desc new file mode 100644 index 00000000..0db2b67c --- /dev/null +++ b/regression/ebmc/cegar/basic1.desc @@ -0,0 +1,6 @@ +KNOWNBUG +basic1.sv +--cegar +SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/ebmc/cegar/basic1.sv b/regression/ebmc/cegar/basic1.sv new file mode 100644 index 00000000..105aa941 --- /dev/null +++ b/regression/ebmc/cegar/basic1.sv @@ -0,0 +1,12 @@ +module top(input clk); + + reg important; + reg not_important; + + initial important = 1; + always @(posedge clk) + important = important; + + assert property (important == 1); + +endmodule