Merge pull request #498 from diffblue/ic3-liveness-to-safety

liveness-to-safety for IC3 and BDDs

Author: tautschnig

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;