ebmc: netlist unwinding now uses netlist property node

Instead of doing its own expression conversion, netlist unwinding now uses
the netlist node given in the netlist property datastructure.

Author: kroening

src/ebmc/bdd_engine.cpp

@@ -364,6 +364,10 @@ void bdd_enginet::compute_counterexample(
   propertyt &property,
   unsigned number_of_timeframes)
 {
+  // Supported by BMC engine?
+  if(!netlist_bmc_supports_property(property.normalized_expr))
+    return;
+
   message.status() << "Computing counterexample with " << number_of_timeframes
                    << " timeframe(s)" << messaget::eom;
 
@@ -372,16 +376,14 @@ void bdd_enginet::compute_counterexample(
   satcheckt solver{message.get_message_handler()};
   bmc_map.map_timeframes(netlist, number_of_timeframes, solver);
 
-  const namespacet ns(transition_system.symbol_table);
-
   ::unwind(netlist, bmc_map, message, solver);
+
+  // find the netlist property
+  auto netlist_property = netlist.properties.find(property.identifier);
+  CHECK_RETURN(netlist_property != netlist.properties.end());
+
   ::unwind_property(
-    property.normalized_expr,
-    property.timeframe_literals,
-    message.get_message_handler(),
-    solver,
-    bmc_map,
-    ns);
+    netlist_property->second, bmc_map, property.timeframe_literals);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;
@@ -402,6 +404,8 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
+  const namespacet ns(transition_system.symbol_table);
+
   property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }

src/ebmc/ebmc_base.cpp

@@ -208,13 +208,12 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
         continue;
       }
 
+      // look up the property in the netlist
+      auto netlist_property = netlist.properties.find(property.identifier);
+      CHECK_RETURN(netlist_property != netlist.properties.end());
+
       ::unwind_property(
-        property.normalized_expr,
-        property.timeframe_literals,
-        message.get_message_handler(),
-        solver,
-        bmc_map,
-        ns);
+        netlist_property->second, bmc_map, property.timeframe_literals);
 
       // freeze for incremental usage
       for(auto l : property.timeframe_literals)

src/ebmc/ebmc_properties.cpp

@@ -67,12 +67,8 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
 
       properties.properties.push_back(propertyt());
       properties.properties.back().number = properties.properties.size() - 1;
-
-      if(symbol.pretty_name.empty())
-        properties.properties.back().name = symbol.name;
-      else
-        properties.properties.back().name = symbol.pretty_name;
-
+      properties.properties.back().identifier = symbol.name;
+      properties.properties.back().name = symbol.display_name();
       properties.properties.back().original_expr = symbol.value;
       properties.properties.back().normalized_expr =
         normalize_property(symbol.value);

src/ebmc/ebmc_properties.h

@@ -26,7 +26,7 @@ class ebmc_propertiest
   {
   public:
     std::size_t number = 0;
-    irep_idt name;
+    irep_idt identifier, name;
     source_locationt location;
     std::string expr_string;
     irep_idt mode;

src/ebmc/report_results.cpp

@@ -55,7 +55,8 @@ void report_results(
         continue;
 
       json_objectt json_property;
-      json_property["identifier"] = json_stringt(id2string(property.name));
+      json_property["identifier"] =
+        json_stringt(id2string(property.identifier));
       json_property["status"] = json_stringt(property.status_as_string());
 
       if(property.has_witness_trace())
@@ -77,7 +78,7 @@ void report_results(
         continue;
 
       xmlt xml_result("result");
-      xml_result.set_attribute("property", id2string(property.name));
+      xml_result.set_attribute("property", id2string(property.identifier));
       xml_result.set_attribute("status", property.status_as_string());
 
       if(property.has_witness_trace())

src/trans-netlist/unwind_netlist.cpp

@@ -34,7 +34,7 @@ void unwind(
   messaget &message,
   cnft &solver,
   bool add_initial_state,
-  unsigned t)
+  std::size_t t)
 {
   bool first=(t==0);
   bool last=(t==bmc_map.timeframe_map.size()-1);
@@ -123,7 +123,7 @@ void unwind(
   cnft &solver,
   bool add_initial_state)
 {
-  for(unsigned t=0; t<bmc_map.timeframe_map.size(); t++)
+  for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
     unwind(netlist, bmc_map, message, solver, add_initial_state, t);
 }
 
@@ -140,15 +140,16 @@ Function: unwind_property
 \*******************************************************************/
 
 void unwind_property(
+  const netlistt::propertyt &property,
   const bmc_mapt &bmc_map,
-  literalt property_node,
   bvt &prop_bv)
 {
+  PRECONDITION(std::holds_alternative<netlistt::Gpt>(property));
+  auto property_node = std::get<netlistt::Gpt>(property).p;
+
   prop_bv.resize(bmc_map.timeframe_map.size());
 
-  for(unsigned t=0;
-      t<bmc_map.timeframe_map.size();
-      t++)
+  for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
   {
     literalt l=bmc_map.translate(t, property_node);
     prop_bv[t]=l;
@@ -157,51 +158,6 @@ void unwind_property(
 
 /*******************************************************************\
 
-Function: unwind_property
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void unwind_property(
-  const exprt &property_expr,
-  bvt &prop_bv,
-  message_handlert &message_handler,
-  propt &solver,
-  const bmc_mapt &map,
-  const namespacet &ns)
-{
-  if(property_expr.is_true())
-  {
-    prop_bv.resize(map.get_no_timeframes(), const_literal(true));
-    return;
-  }
-
-  // We want AG p.
-  auto &p = [](const exprt &expr) -> const exprt & {
-    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);
-  }(property_expr);
-
-  for(unsigned c=0; c<map.get_no_timeframes(); c++)
-  {
-    literalt l=instantiate_convert(solver, map, p, c, c+1, ns, message_handler);
-    prop_bv.push_back(l);
-  }
-}
-
-/*******************************************************************\
-
 Function: netlist_bmc_supports_property
 
   Inputs:

src/trans-netlist/unwind_netlist.h

@@ -10,12 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_TRANS_UNWIND_NETLIST_GRAPH_H
 
 #include <util/message.h>
-#include <util/namespace.h>
 
 #include <solvers/sat/cnf.h>
 
-#include "netlist.h"
 #include "bmc_map.h"
+#include "netlist.h"
 
 void unwind(
   const netlistt &netlist,
@@ -31,24 +30,15 @@ void unwind(
   messaget &message,
   cnft &solver,
   bool add_initial_state,
-  unsigned timeframe);
-
-// unwind a property that has not yet been converted
-void unwind_property(
-  const exprt &property_expr,
-  bvt &prop_bv,
-  message_handlert &,
-  propt &solver,
-  const bmc_mapt &,
-  const namespacet &);
+  std::size_t timeframe);
 
 // Is the property supported?
-bool netlist_bmc_supports_property(const exprt &);
+bool netlist_bmc_supports_property(const class exprt &);
 
-// unwind a property that is given as netlist node
+// unwind a netlist property
 void unwind_property(
+  const netlistt::propertyt &,
   const bmc_mapt &,
-  literalt property_node,
   bvt &prop_bv);
 
 #endif