liveness engine

Author: kroening

Diff for: 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 for: 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 for: src/ebmc/liveness_engine.cpp

@@ -0,0 +1,154 @@
+/*******************************************************************\
+
+Module: Liveness Engine
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "liveness_engine.h"
+
+#include <util/format_expr.h>
+
+#include <temporal-logic/ctl.h>
+#include <temporal-logic/ltl.h>
+#include <verilog/sva_expr.h>
+
+#include <deque>
+#include <unordered_map>
+
+// 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<is_live_exprt, bool, irep_hash> truth;
+
+  std::deque<std::pair<is_live_exprt, bool>> 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_exprt> 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 for: src/ebmc/liveness_engine.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Liveness Engine
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#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 for: src/ebmc/property_checker.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #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