liveness-to-safety for IC3 and BDDs

This adds support for the combination of IC3 or BDDs and the
liveness-to-safety translation.

Author: kroening

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,6 @@
+KNOWNBUG
+passing1.sv
+--liveness-to-safety --ic3
+^EXIT=0$
+^SIGNAL=0$
+--

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

@@ -0,0 +1,6 @@
+CORE
+passing2.sv
+--ic3 --liveness-to-safety
+^EXIT=0$
+^SIGNAL=0$
+--

src/ebmc/bdd_engine.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/format_expr.h>
 
 #include <ebmc/ebmc_properties.h>
+#include <ebmc/liveness_to_safety.h>
 #include <ebmc/transition_system.h>
 #include <solvers/bdd/miniBDD/miniBDD.h>
 #include <solvers/sat/satcheck.h>
@@ -177,13 +178,18 @@ int bdd_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);
+
     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

@@ -230,11 +230,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

@@ -420,6 +420,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

@@ -241,6 +241,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;
@@ -276,15 +285,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/ic3/m1ain.cc

@@ -12,6 +12,7 @@ Author: Eugene Goldberg, [email protected]
 #include <util/ui_message.h>
 
 #include <ebmc/ebmc_properties.h>
+#include <ebmc/liveness_to_safety.h>
 #include <ebmc/report_results.h>
 
 #include <trans-netlist/netlist.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:
@@ -253,6 +254,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
@@ -284,9 +286,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());
@@ -803,11 +803,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 &);