Merge pull request #501 from diffblue/trans-to-netlist-properties

ebmc: trans_to_netlist now takes property map

Author: tautschnig

src/ebmc/bdd_engine.cpp

@@ -174,23 +174,26 @@ int bdd_enginet::operator()()
     transition_system =
       get_transition_system(cmdline, message.get_message_handler());
 
+    properties = ebmc_propertiest::from_command_line(
+      cmdline, transition_system, message.get_message_handler());
+
+    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,
+      property_map,
       netlist,
       message.get_message_handler());
 
     message.statistics() << "Latches: " << netlist.var_map.latches.size()
                          << ", nodes: " << netlist.number_of_nodes()
                          << messaget::eom;
 
-    properties = ebmc_propertiest::from_command_line(
-      cmdline, transition_system, message.get_message_handler());
-
-    for(const propertyt &p : properties.properties)
-      get_atomic_propositions(p.normalized_expr);
+    for(const auto &[_, expr] : property_map)
+      get_atomic_propositions(expr);
 
     message.status() << "Building BDD for netlist" << messaget::eom;
 

src/ebmc/cegar/bmc_cegar.cpp

@@ -230,9 +230,14 @@ void bmc_cegart::make_netlist()
 
   try
   {
+    std::map<irep_idt, exprt> property_map;
+
     convert_trans_to_netlist(
-      symbol_table, main_module,
-      concrete_netlist, get_message_handler());
+      symbol_table,
+      main_module,
+      property_map,
+      concrete_netlist,
+      get_message_handler());
   }
 
   catch(const std::string &error_msg)

src/ebmc/ebmc_base.cpp

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

src/ebmc/ebmc_parse_options.cpp

@@ -263,19 +263,6 @@ int ebmc_parse_optionst::doit()
         return 0;
       }
 
-      if(cmdline.isset("smv-netlist"))
-      {
-        netlistt netlist;
-        if(ebmc_base.make_netlist(netlist))
-          return 1;
-        std::cout << "-- Generated by EBMC " << EBMC_VERSION << '\n';
-        std::cout << "-- Generated from "
-                  << ebmc_base.transition_system.main_symbol->name << '\n';
-        std::cout << '\n';
-        netlist.output_smv(std::cout);
-        return 0;
-      }
-
       if(cmdline.isset("dot-netlist"))
       {
         netlistt netlist;
@@ -292,13 +279,26 @@ int ebmc_parse_optionst::doit()
       if(result != -1)
         return result;
 
-      if(cmdline.isset("compute-ct"))
-        return ebmc_base.do_compute_ct();
-
       // 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;
+        if(ebmc_base.make_netlist(netlist))
+          return 1;
+        std::cout << "-- Generated by EBMC " << EBMC_VERSION << '\n';
+        std::cout << "-- Generated from "
+                  << ebmc_base.transition_system.main_symbol->name << '\n';
+        std::cout << '\n';
+        netlist.output_smv(std::cout);
+        return 0;
+      }
+
+      if(cmdline.isset("compute-ct"))
+        return ebmc_base.do_compute_ct();
+
       if(cmdline.isset("aig") || cmdline.isset("dimacs"))
         return ebmc_base.do_bit_level_bmc();
       else

src/ebmc/ebmc_properties.h

@@ -202,6 +202,16 @@ class ebmc_propertiest
 
   bool select_property(const cmdlinet &, message_handlert &);
 
+  /// a map from property identifier to normalized expression
+  std::map<irep_idt, exprt> make_property_map() const
+  {
+    std::map<irep_idt, exprt> result;
+    for(auto &p : properties)
+      if(!p.is_disabled())
+        result.emplace(p.identifier, p.normalized_expr);
+    return result;
+  }
+
   // command-line tool exit code, depending on property status
   int exit_code() const;
 };

src/ic3/m1ain.cc

@@ -92,22 +92,23 @@ int ic3_enginet::operator()()
     auto transition_system =
       get_transition_system(cmdline, message.get_message_handler());
 
+    properties = ebmc_propertiest::from_command_line(
+      cmdline, transition_system, message.get_message_handler());
+
     // make net-list
     message.status() << "Generating Netlist" << messaget::eom;
 
     convert_trans_to_netlist(
       transition_system.symbol_table,
       transition_system.main_symbol->name,
+      properties.make_property_map(),
       netlist,
       message.get_message_handler());
 
     message.statistics() << "Latches: " << netlist.var_map.latches.size()
                          << ", nodes: " << netlist.number_of_nodes()
                          << messaget::eom;
 
-    properties = ebmc_propertiest::from_command_line(
-      cmdline, transition_system, message.get_message_handler());
-
     if(properties.properties.empty())
     {
       message.error() << "no properties" << messaget::eom;

src/trans-netlist/trans_to_netlist.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
-#include <temporal-logic/normalize_property.h>
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -50,8 +49,10 @@ class convert_trans_to_netlistt:public messaget
   {
   }
 
-  void operator()(const irep_idt &module);
-  
+  void operator()(
+    const irep_idt &module,
+    const std::map<irep_idt, exprt> &properties);
+
 protected:
   symbol_table_baset &symbol_table;
   const namespacet ns;
@@ -250,7 +251,9 @@ Function: convert_trans_to_netlistt::operator()
 
 \*******************************************************************/
 
-void convert_trans_to_netlistt::operator()(const irep_idt &module)
+void convert_trans_to_netlistt::operator()(
+  const irep_idt &module,
+  const std::map<irep_idt, exprt> &properties)
 {
   // setup
   lhs_map.clear();
@@ -317,73 +320,70 @@ void convert_trans_to_netlistt::operator()(const irep_idt &module)
     aig_prop, dest.var_map, trans.init(), ns, get_message_handler()));
 
   // properties
-  for(const auto &[id, symbol] : symbol_table)
+  for(const auto &[id, property_expr] : properties)
   {
-    if(symbol.module == module && symbol.is_property)
-    {
-      auto expr = normalize_property(symbol.value);
+    auto expr = property_expr; // copy
+
+    // we also convert propositions in assumptions
+    if(expr.id() == ID_sva_assume)
+      expr = to_sva_assume_expr(expr).op();
 
-      // we also convert propositions in assumptions
-      if(expr.id() == ID_sva_assume)
-        expr = to_sva_assume_expr(expr).op();
+    auto convert = [&aig_prop, this](const exprt &expr) -> literalt {
+      return instantiate_convert(
+        aig_prop, dest.var_map, expr, ns, get_message_handler());
+    };
 
-      auto convert = [&aig_prop, this](const exprt &expr) -> literalt {
-        return instantiate_convert(
-          aig_prop, dest.var_map, expr, ns, get_message_handler());
+    if(expr.id() == ID_AG || expr.id() == ID_G || expr.id() == ID_sva_always)
+    {
+      auto get_phi = [](const exprt &expr) {
+        if(expr.id() == ID_AG)
+          return to_AG_expr(expr).op();
+        else if(expr.id() == ID_G)
+          return to_G_expr(expr).op();
+        else if(expr.id() == ID_sva_always)
+          return to_sva_always_expr(expr).op();
+        else
+          PRECONDITION(false);
       };
 
-      if(expr.id() == ID_AG || expr.id() == ID_G || expr.id() == ID_sva_always)
+      auto phi = get_phi(expr);
+
+      if(!has_temporal_operator(phi))
+      {
+        // G p
+        dest.properties.emplace(id, netlistt::Gpt{convert(phi)});
+      }
+      else if(
+        phi.id() == ID_AF || phi.id() == ID_F ||
+        phi.id() == ID_sva_s_eventually)
       {
-        auto get_phi = [](const exprt &expr) {
-          if(expr.id() == ID_AG)
-            return to_AG_expr(expr).op();
-          else if(expr.id() == ID_G)
-            return to_G_expr(expr).op();
-          else if(expr.id() == ID_sva_always)
-            return to_sva_always_expr(expr).op();
+        auto get_psi = [](const exprt &expr) {
+          if(expr.id() == ID_AF)
+            return to_AF_expr(expr).op();
+          else if(expr.id() == ID_F)
+            return to_F_expr(expr).op();
+          else if(expr.id() == ID_sva_s_eventually)
+            return to_sva_s_eventually_expr(expr).op();
           else
             PRECONDITION(false);
         };
 
-        auto phi = get_phi(expr);
+        auto psi = get_psi(phi);
 
-        if(!has_temporal_operator(phi))
-        {
-          // G p
-          dest.properties.emplace(id, netlistt::Gpt{convert(phi)});
-        }
-        else if(
-          phi.id() == ID_AF || phi.id() == ID_F ||
-          phi.id() == ID_sva_s_eventually)
+        if(!has_temporal_operator(psi))
         {
-          auto get_psi = [](const exprt &expr) {
-            if(expr.id() == ID_AF)
-              return to_AF_expr(expr).op();
-            else if(expr.id() == ID_F)
-              return to_F_expr(expr).op();
-            else if(expr.id() == ID_sva_s_eventually)
-              return to_sva_s_eventually_expr(expr).op();
-            else
-              PRECONDITION(false);
-          };
-
-          auto psi = get_psi(phi);
-
-          if(!has_temporal_operator(psi))
-          {
-            // G F p
-            dest.properties.emplace(id, netlistt::GFpt{convert(psi)});
-          }
-          else
-          {
-            // unsupported
-          }
+          // G F p
+          dest.properties.emplace(id, netlistt::GFpt{convert(psi)});
         }
         else
         {
           // unsupported
         }
       }
+      else
+      {
+        // unsupported
+      }
     }
   }
 
@@ -810,10 +810,11 @@ Function: convert_trans_to_netlist
 void convert_trans_to_netlist(
   symbol_table_baset &symbol_table,
   const irep_idt &module,
+  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);
+  c(module, properties);
 }

src/trans-netlist/trans_to_netlist.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 void convert_trans_to_netlist(
   symbol_table_baset &,
   const irep_idt &module,
+  const std::map<irep_idt, exprt> &properties,
   class netlistt &dest,
   message_handlert &);