liveness-to-safety for IC3 and BDDs

regression/ebmc/liveness-to-safety/failing1.bdd.desc

@@ -0,0 +1,7 @@
+CORE
+failing1.sv
+--bdd --liveness-to-safety
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.p0\] always s_eventually main\.my_bit: REFUTED$
+--

regression/ebmc/liveness-to-safety/failing1.ic3.desc

@@ -0,0 +1,7 @@
+CORE
+failing1.sv
+--ic3 --liveness-to-safety
+^EXIT=1$
+^SIGNAL=0$
+^property FAILED$
+--

regression/ebmc/liveness-to-safety/failing2.ic3.desc

@@ -0,0 +1,7 @@
+CORE
+failing2.sv
+--ic3 --liveness-to-safety
+^EXIT=1$
+^SIGNAL=0$
+^property FAILED$
+--

regression/ebmc/liveness-to-safety/passing1.bdd.desc

@@ -0,0 +1,7 @@
+CORE
+passing1.sv
+--liveness-to-safety --bdd
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.p0\] always s_eventually main\.my_bit: PROVED$
+--

regression/ebmc/liveness-to-safety/passing1.ic3.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+passing1.sv
+--liveness-to-safety --ic3
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+IC3 gives wrong result.

regression/ebmc/liveness-to-safety/passing2.ic3.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+passing2.sv
+--ic3 --liveness-to-safety
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+IC3 gives wrong result.

src/ebmc/bdd_engine.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/format_expr.h>
 
+#include <ebmc/liveness_to_safety.h>
+#include <ebmc/transition_system.h>
 #include <solvers/bdd/miniBDD/miniBDD.h>
 #include <solvers/sat/satcheck.h>
 #include <temporal-logic/temporal_expr.h>
@@ -186,13 +188,18 @@ property_checker_resultt bdd_enginet::operator()()
     if(!properties.has_unknown_property())
       return property_checker_resultt{properties};
 
+    // possibly apply liveness-to-safety
+    if(cmdline.isset("liveness-to-safety"))
+      liveness_to_safety(transition_system, properties);
+
     const auto property_map = properties.make_property_map();
 
     message.status() << "Building netlist" << messaget::eom;
 
     convert_trans_to_netlist(
       transition_system.symbol_table,
       transition_system.main_symbol->name,
+      transition_system.trans_expr,
       property_map,
       netlist,
       message.get_message_handler());

src/ebmc/cegar/bmc_cegar.cpp

@@ -229,11 +229,15 @@ void bmc_cegart::make_netlist()
 
   try
   {
+    const symbolt &module_symbol = ns.lookup(main_module);
+    const transt &trans = to_trans_expr(module_symbol.value);
+
     std::map<irep_idt, exprt> property_map;
 
     convert_trans_to_netlist(
       symbol_table,
       main_module,
+      trans,
       property_map,
       concrete_netlist,
       get_message_handler());

src/ebmc/ebmc_base.cpp

@@ -152,6 +152,7 @@ bool ebmc_baset::make_netlist(netlistt &netlist)
     convert_trans_to_netlist(
       transition_system.symbol_table,
       transition_system.main_symbol->name,
+      transition_system.trans_expr,
       properties.make_property_map(),
       netlist,
       message.get_message_handler());

src/ebmc/ebmc_parse_options.cpp

@@ -236,6 +236,15 @@ int ebmc_parse_optionst::doit()
       ebmc_baset ebmc_base(cmdline, ui_message_handler);
       ebmc_base.transition_system = std::move(transition_system);
 
+      auto result = ebmc_base.get_properties();
+
+      if(result != -1)
+        return result;
+
+      // possibly apply liveness-to-safety
+      if(cmdline.isset("liveness-to-safety"))
+        liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
+
       if(cmdline.isset("show-varmap"))
       {
         netlistt netlist;
@@ -271,15 +280,6 @@ int ebmc_parse_optionst::doit()
         return 0;
       }
 
-      auto result = ebmc_base.get_properties();
-
-      if(result != -1)
-        return result;
-
-      // possibly apply liveness-to-safety
-      if(cmdline.isset("liveness-to-safety"))
-        liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
-
       if(cmdline.isset("smv-netlist"))
       {
         netlistt netlist;

src/ebmc/property_checker.cpp

@@ -224,6 +224,7 @@ property_checker_resultt bit_level_bmc(
     convert_trans_to_netlist(
       transition_system.symbol_table,
       transition_system.main_symbol->name,
+      transition_system.trans_expr,
       properties.make_property_map(),
       netlist,
       message.get_message_handler());

src/ic3/m1ain.cc

@@ -11,6 +11,7 @@ Author: Eugene Goldberg, [email protected]
 #include <util/cmdline.h>
 #include <util/ui_message.h>
 
+#include <ebmc/liveness_to_safety.h>
 #include <ebmc/property_checker.h>
 #include <ebmc/report_results.h>
 
@@ -95,12 +96,17 @@ int ic3_enginet::operator()()
     properties = ebmc_propertiest::from_command_line(
       cmdline, transition_system, message.get_message_handler());
 
+    // possibly apply liveness-to-safety
+    if(cmdline.isset("liveness-to-safety"))
+      liveness_to_safety(transition_system, properties);
+
     // make net-list
     message.status() << "Generating Netlist" << messaget::eom;
 
     convert_trans_to_netlist(
       transition_system.symbol_table,
       transition_system.main_symbol->name,
+      transition_system.trans_expr,
       properties.make_property_map(),
       netlist,
       message.get_message_handler());

src/trans-netlist/trans_to_netlist.cpp

@@ -51,6 +51,7 @@ class convert_trans_to_netlistt:public messaget
 
   void operator()(
     const irep_idt &module,
+    const transt &,
     const std::map<irep_idt, exprt> &properties);
 
 protected:
@@ -255,6 +256,7 @@ Function: convert_trans_to_netlistt::operator()
 
 void convert_trans_to_netlistt::operator()(
   const irep_idt &module,
+  const transt &trans,
   const std::map<irep_idt, exprt> &properties)
 {
   // setup
@@ -286,9 +288,7 @@ void convert_trans_to_netlistt::operator()(
     }
   }
 
-  const symbolt &module_symbol=ns.lookup(module);
-  const transt &trans=to_trans_expr(module_symbol.value);
-  mode = module_symbol.mode;
+  mode = ns.lookup(module).mode;
 
   // build the net-list
   aig_prop_constraintt aig_prop(dest, get_message_handler());
@@ -810,11 +810,12 @@ Function: convert_trans_to_netlist
 void convert_trans_to_netlist(
   symbol_table_baset &symbol_table,
   const irep_idt &module,
+  const transt &trans_expr,
   const std::map<irep_idt, exprt> &properties,
   netlistt &dest,
   message_handlert &message_handler)
 {
   convert_trans_to_netlistt c(symbol_table, dest, message_handler);
 
-  c(module, properties);
+  c(module, trans_expr, properties);
 }

src/trans-netlist/trans_to_netlist.h

@@ -10,13 +10,15 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_TRANS_NETLIST_TRANS_H
 
 #include <util/expr.h>
+#include <util/mathematical_expr.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/symbol_table_base.h>
 
 void convert_trans_to_netlist(
   symbol_table_baset &,
   const irep_idt &module,
+  const transt &,
   const std::map<irep_idt, exprt> &properties,
   class netlistt &dest,
   message_handlert &);