From ee8cbfa293ea50dff2ccc9113ed656f139ffa5cf Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 29 Dec 2024 15:10:37 +0000 Subject: [PATCH] liveness engine --- src/ebmc/Makefile | 1 + src/ebmc/ebmc_parse_options.h | 1 + src/ebmc/liveness_engine.cpp | 154 ++++++++++++++++++++++++++++++++++ src/ebmc/liveness_engine.h | 20 +++++ src/ebmc/property_checker.cpp | 6 ++ 5 files changed, 182 insertions(+) create mode 100644 src/ebmc/liveness_engine.cpp create mode 100644 src/ebmc/liveness_engine.h diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index ef4edd4dd..18565b672 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -19,6 +19,7 @@ SRC = \ k_induction.cpp \ liveness_to_safety.cpp \ live_signal.cpp \ + liveness_engine.cpp \ main.cpp \ netlist.cpp \ neural_liveness.cpp \ diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index d6abed1e8..575d3b3cc 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -40,6 +40,7 @@ class ebmc_parse_optionst:public parse_options_baset "(compute-interpolant)(interpolation)(interpolation-vmcai)" "(ic3)(property):(constr)(h)(new-mode)(aiger)" "(interpolation-word)(interpolator):(bdd)" + "(liveness)" "(ranking-function):" "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)" "(minisat)(cadical)" diff --git a/src/ebmc/liveness_engine.cpp b/src/ebmc/liveness_engine.cpp new file mode 100644 index 000000000..2219d13bf --- /dev/null +++ b/src/ebmc/liveness_engine.cpp @@ -0,0 +1,154 @@ +/*******************************************************************\ + +Module: Liveness Engine + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "liveness_engine.h" + +#include + +#include +#include +#include + +#include +#include + +// G F p +class is_live_exprt : public unary_predicate_exprt +{ +public: + explicit is_live_exprt(exprt op) + : unary_predicate_exprt{"is_live", std::move(op)} + { + } +}; + +class liveness_enginet +{ +public: + liveness_enginet( + const cmdlinet &_cmdline, + const transition_systemt &_transition_system, + message_handlert &_message_handler) + : cmdline(_cmdline), + transition_system(_transition_system), + message(_message_handler) + { + } + + void operator()(const is_live_exprt &); + +protected: + const cmdlinet &cmdline; + const transition_systemt &transition_system; + messaget message; + + std::unordered_map truth; + + std::deque> queue; + + void enqueue(const is_live_exprt &expr, bool value) + { + message.status() << (value ? "T: " : "F: "); + message.status() << format(expr) << messaget::eom; + queue.emplace_back(expr, value); + } + + static is_live_exprt negate_p(const is_live_exprt &expr) + { + if(expr.op().id() == ID_not) + return is_live_exprt{to_not_expr(expr.op()).op()}; + else if(expr.op().is_false()) + return is_live_exprt{true_exprt{}}; + else if(expr.op().is_true()) + return is_live_exprt{false_exprt{}}; + else + return is_live_exprt{not_exprt{expr.op()}}; + } +}; + +void liveness_enginet::operator()(const is_live_exprt &expr) +{ + enqueue(expr, false); + + while(!queue.empty()) + { + auto entry = queue.front(); + queue.pop_front(); + + auto truth_it = truth.find(entry.first); + if(truth_it != truth.end()) + { + if(truth_it->second != entry.second) + { + message.result() << "Contradiction on " << format(expr) + << messaget::eom; + return; + } + } + else + { + // ¬GFp ⇒ GF¬p + if(!entry.second) + enqueue(negate_p(entry.first), true); + } + } +} + +std::optional is_live_expr(const exprt &expr) +{ + // G F p + if( + expr.id() == ID_G && to_G_expr(expr).op().id() == ID_F && + !has_temporal_operator(to_F_expr(to_G_expr(expr).op()).op())) + { + auto p = to_F_expr(to_G_expr(expr).op()).op(); + return is_live_exprt{p}; + } + + // AG AF p + if( + expr.id() == ID_AG && to_AG_expr(expr).op().id() == ID_AF && + !has_temporal_operator(to_AF_expr(to_AG_expr(expr).op()).op())) + { + auto p = to_AF_expr(to_AG_expr(expr).op()).op(); + return is_live_exprt{p}; + } + + // always s_eventually p + if( + expr.id() == ID_sva_always && + to_sva_always_expr(expr).op().id() == ID_sva_s_eventually && + !has_temporal_operator( + to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op())) + { + // always s_eventually p --> AG AF p + auto p = to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op(); + return is_live_exprt{p}; + } + + return {}; +} + +property_checker_resultt liveness_engine( + const cmdlinet &cmdline, + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + for(auto &property : properties.properties) + { + auto is_live_opt = is_live_expr(property.normalized_expr); + if(is_live_opt.has_value()) + { + liveness_enginet{cmdline, transition_system, message_handler}( + *is_live_opt); + } + } + + return property_checker_resultt{properties}; +} diff --git a/src/ebmc/liveness_engine.h b/src/ebmc/liveness_engine.h new file mode 100644 index 000000000..203d8f8df --- /dev/null +++ b/src/ebmc/liveness_engine.h @@ -0,0 +1,20 @@ +/*******************************************************************\ + +Module: Liveness Engine + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_LIVENESS_ENGINE_H +#define CPROVER_EBMC_LIVENESS_ENGINE_H + +#include "property_checker.h" + +property_checker_resultt liveness_engine( + const cmdlinet &, + transition_systemt &, + ebmc_propertiest &, + message_handlert &); + +#endif diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 39b5ee9cd..b9bb68a31 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "ebmc_solver_factory.h" #include "ic3_engine.h" #include "k_induction.h" +#include "liveness_engine.h" #include "netlist.h" #include "output_file.h" #include "report_results.h" @@ -442,6 +443,11 @@ property_checker_resultt property_checker( cmdline, transition_system, properties, message_handler); #endif } + else if(cmdline.isset("liveness")) + { + return liveness_engine( + cmdline, transition_system, properties, message_handler); + } else if(cmdline.isset("bound")) { // word-level BMC