From 90c73542afbaa8bd40d41ec45606e30dcb9efac3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 30 Aug 2024 09:16:22 -0700 Subject: [PATCH] introduce property_checker_resultt This introduces a type for the result from an engine, as a replacement for 'int'. --- src/ebmc/bdd_engine.cpp | 19 ++++----- src/ebmc/bdd_engine.h | 7 +--- src/ebmc/k_induction.cpp | 6 +-- src/ebmc/k_induction.h | 3 +- src/ebmc/property_checker.cpp | 79 +++++++++++++++++++---------------- src/ebmc/property_checker.h | 7 ++++ 6 files changed, 66 insertions(+), 55 deletions(-) diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index ddf1c2c42..ba6b17770 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -51,7 +51,7 @@ class bdd_enginet { } - int operator()(); + property_checker_resultt operator()(); protected: using propertiest = ebmc_propertiest; @@ -173,7 +173,7 @@ Function: bdd_enginet::operator() \*******************************************************************/ -int bdd_enginet::operator()() +property_checker_resultt bdd_enginet::operator()() { try { @@ -216,30 +216,29 @@ int bdd_enginet::operator()() } std::cout << '\n'; - - return 0; + + return property_checker_resultt::SUCCESS; } if(properties.properties.empty()) { message.error() << "no properties" << messaget::eom; - return 1; + return property_checker_resultt::ERROR; } for(propertyt &p : properties.properties) check_property(p); - report_results(cmdline, properties, ns, message.get_message_handler()); - return properties.exit_code(); + return property_checker_resultt::REPORT_RESULT; } catch(const char *error_msg) { message.error() << error_msg << messaget::eom; - return 1; + return property_checker_resultt::ERROR; } catch(int) { - return 1; + return property_checker_resultt::ERROR; } } @@ -1002,7 +1001,7 @@ Function: bdd_engine \*******************************************************************/ -int bdd_engine( +property_checker_resultt bdd_engine( const cmdlinet &cmdline, transition_systemt &transition_system, ebmc_propertiest &properties, diff --git a/src/ebmc/bdd_engine.h b/src/ebmc/bdd_engine.h index d333a1e7d..ec2981a05 100644 --- a/src/ebmc/bdd_engine.h +++ b/src/ebmc/bdd_engine.h @@ -9,12 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_EBMC_BDD_ENGINE_H #define CPROVER_EBMC_BDD_ENGINE_H -#include -#include +#include "property_checker.h" -#include "ebmc_properties.h" - -int bdd_engine( +property_checker_resultt bdd_engine( const cmdlinet &, transition_systemt &, ebmc_propertiest &, diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index d8f1e295e..e5d718175 100644 --- a/src/ebmc/k_induction.cpp +++ b/src/ebmc/k_induction.cpp @@ -118,7 +118,7 @@ Function: k_induction \*******************************************************************/ -int k_induction( +property_checker_resultt k_induction( const cmdlinet &cmdline, transition_systemt &transition_system, ebmc_propertiest &properties, @@ -154,9 +154,7 @@ int k_induction( k_induction( k, transition_system, properties, solver_factory, message_handler); - const namespacet ns(transition_system.symbol_table); - report_results(cmdline, properties, ns, message_handler); - return properties.exit_code(); + return property_checker_resultt::REPORT_RESULT; } /*******************************************************************\ diff --git a/src/ebmc/k_induction.h b/src/ebmc/k_induction.h index 260e448de..ffbec0043 100644 --- a/src/ebmc/k_induction.h +++ b/src/ebmc/k_induction.h @@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "ebmc_solver_factory.h" +#include "property_checker.h" class transition_systemt; class ebmc_propertiest; -int k_induction( +property_checker_resultt k_induction( const cmdlinet &, transition_systemt &, ebmc_propertiest &, diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 2af86c73f..1aabf0223 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -27,7 +27,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -int word_level_bmc( +property_checker_resultt word_level_bmc( const cmdlinet &cmdline, const transition_systemt &transition_system, ebmc_propertiest &properties, @@ -38,8 +38,6 @@ int word_level_bmc( bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") || cmdline.isset("show-formula"); - int result = 0; - try { if(cmdline.isset("max-bound")) @@ -93,12 +91,8 @@ int word_level_bmc( 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(); - } + if(convert_only) + return property_checker_resultt::SUCCESS; } } @@ -106,25 +100,25 @@ int word_level_bmc( { messaget message{message_handler}; message.error() << e << messaget::eom; - return 10; + return property_checker_resultt::ERROR; } catch(const std::string &e) { messaget message{message_handler}; message.error() << e << messaget::eom; - return 10; + return property_checker_resultt::ERROR; } catch(int) { - return 10; + return property_checker_resultt::ERROR; } - return result; + return property_checker_resultt::REPORT_RESULT; } -int finish_bit_level_bmc( +property_checker_resultt finish_bit_level_bmc( std::size_t bound, const bmc_mapt &bmc_map, propt &solver, @@ -179,12 +173,12 @@ int finish_bit_level_bmc( case propt::resultt::P_ERROR: message.error() << "Error from decision procedure" << messaget::eom; - return 2; + return property_checker_resultt::ERROR; default: message.error() << "Unexpected result from decision procedure" << messaget::eom; - return 1; + return property_checker_resultt::ERROR; } } @@ -195,10 +189,10 @@ int finish_bit_level_bmc( << std::chrono::duration(sat_stop_time - sat_start_time).count() << messaget::eom; - return properties.exit_code(); + return property_checker_resultt::REPORT_RESULT; } -int bit_level_bmc( +property_checker_resultt bit_level_bmc( cnft &solver, bool convert_only, const cmdlinet &cmdline, @@ -220,8 +214,6 @@ int bit_level_bmc( bound = 1; } - int result; - try { bmc_mapt bmc_map; @@ -288,12 +280,11 @@ int bit_level_bmc( } if(convert_only) - result = 0; + return property_checker_resultt::SUCCESS; else { - result = finish_bit_level_bmc( + return finish_bit_level_bmc( bound, bmc_map, solver, transition_system, properties, message_handler); - report_results(cmdline, properties, ns, message_handler); } } @@ -301,25 +292,23 @@ int bit_level_bmc( { messaget message{message_handler}; message.error() << e << messaget::eom; - return 10; + return property_checker_resultt::ERROR; } catch(const std::string &e) { messaget message{message_handler}; message.error() << e << messaget::eom; - return 10; + return property_checker_resultt::ERROR; } catch(int) { - return 10; + return property_checker_resultt::ERROR; } - - return result; } -int bit_level_bmc( +property_checker_resultt bit_level_bmc( const cmdlinet &cmdline, transition_systemt &transition_system, ebmc_propertiest &properties, @@ -380,23 +369,43 @@ int property_checker( ebmc_propertiest &properties, message_handlert &message_handler) { + property_checker_resultt result; + if(cmdline.isset("bdd") || cmdline.isset("show-bdds")) { - return bdd_engine(cmdline, transition_system, properties, message_handler); + result = + bdd_engine(cmdline, transition_system, properties, message_handler); } else if(cmdline.isset("aig") || cmdline.isset("dimacs")) { - return bit_level_bmc( - cmdline, transition_system, properties, message_handler); + result = + bit_level_bmc(cmdline, transition_system, properties, message_handler); } else if(cmdline.isset("k-induction")) { - return k_induction(cmdline, transition_system, properties, message_handler); + result = + k_induction(cmdline, transition_system, properties, message_handler); } else { // default engine is word-level BMC - return word_level_bmc( - cmdline, transition_system, properties, message_handler); + result = + word_level_bmc(cmdline, transition_system, properties, message_handler); + } + + switch(result) + { + case property_checker_resultt::ERROR: + return 10; + + case property_checker_resultt::SUCCESS: + return 0; + + case property_checker_resultt::REPORT_RESULT: + const namespacet ns{transition_system.symbol_table}; + report_results(cmdline, properties, ns, message_handler); + return properties.exit_code(); } + + UNREACHABLE; } diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h index 8de660a71..77f6d56df 100644 --- a/src/ebmc/property_checker.h +++ b/src/ebmc/property_checker.h @@ -12,6 +12,13 @@ Author: Daniel Kroening, dkr@amazon.com #include "ebmc_properties.h" #include "transition_system.h" +enum class property_checker_resultt +{ + REPORT_RESULT, + SUCCESS, + ERROR +}; + int property_checker( const cmdlinet &, transition_systemt &,