Merge pull request #1064 from diffblue/smv-netlist-not-translated

netlists: include properties that are not translated in map

Author: tautschnig

regression/ebmc/smv-netlist/verilog1.desc

@@ -5,7 +5,10 @@ verilog1.sv
 ^VAR Verilog\.main\.x: boolean;$
 ^ASSIGN next\(Verilog\.main\.x\):=\!Verilog\.main\.x;$
 ^INIT !Verilog\.main\.x$
+^-- Verilog::main.assert.1$
 ^LTLSPEC G F Verilog\.main\.x$
+^-- Verilog::main.assert.2$
+^-- not translated$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-netlist/verilog1.sv

@@ -7,6 +7,9 @@ module main(input clk);
   always @(posedge clk)
     x = !x;
 
-  always assert property (always s_eventually x);
+  assert property (always s_eventually x);
+
+  // won't get translated
+  assert property (x[->5]);
 
 endmodule

src/ebmc/bdd_engine.cpp

@@ -412,7 +412,7 @@ void bdd_enginet::compute_counterexample(
   CHECK_RETURN(netlist_property != netlist.properties.end());
 
   property.timeframe_literals =
-    ::unwind_property(netlist_property->second, bmc_map);
+    ::unwind_property(netlist_property->second.value(), bmc_map);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;
@@ -1053,9 +1053,11 @@ void bdd_enginet::build_BDDs()
         // find the netlist property
         auto netlist_property = netlist.properties.find(property.identifier);
         CHECK_RETURN(netlist_property != netlist.properties.end());
+        CHECK_RETURN(netlist_property->second.has_value());
         DATA_INVARIANT(
-          netlist_property->second.id() == ID_G, "assumed property must be G");
-        auto &p = to_G_expr(netlist_property->second).op();
+          netlist_property->second.value().id() == ID_G,
+          "assumed property must be G");
+        auto &p = to_G_expr(netlist_property->second.value()).op();
         DATA_INVARIANT(
           p.id() == ID_literal, "assumed property must be G literal");
         auto l = to_literal_expr(p).get_literal();

src/ebmc/cegar/bmc_cegar.cpp

@@ -78,7 +78,7 @@ void bmc_cegart::unwind(
   for(auto &property_it : netlist.properties)
   {
     auto &prop_bv = prop_bv_map[property_it.first];
-    prop_bv = unwind_property(property_it.second, bmc_map);
+    prop_bv = unwind_property(property_it.second.value(), bmc_map);
 
     disjuncts.push_back(!solver.land(prop_bv));
   }

src/ebmc/property_checker.cpp

@@ -257,9 +257,10 @@ property_checker_resultt bit_level_bmc(
       // look up the property in the netlist
       auto netlist_property = netlist.properties.find(property.identifier);
       CHECK_RETURN(netlist_property != netlist.properties.end());
+      CHECK_RETURN(netlist_property->second.has_value());
 
       property.timeframe_literals =
-        ::unwind_property(netlist_property->second, bmc_map);
+        ::unwind_property(netlist_property->second.value(), bmc_map);
 
       if(property.is_assumed())
       {

src/trans-netlist/netlist.h

@@ -56,7 +56,8 @@ class netlistt:public aig_plus_constraintst
 
   // Map from property ID to a netlist property,
   // which uses literal_exprt.
-  using propertiest = std::map<irep_idt, exprt>;
+  // Maps to {} if translation was not possible.
+  using propertiest = std::map<irep_idt, std::optional<exprt>>;
   propertiest properties;
 };
 

src/trans-netlist/smv_netlist.cpp

@@ -241,30 +241,37 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
 
   for(auto &[id, netlist_expr] : netlist.properties)
   {
-    if(is_CTL(netlist_expr))
+    if(!netlist_expr.has_value())
+    {
+      // translation has failed
+      out << "-- " << id << '\n';
+      out << "-- not translated\n";
+      out << '\n';
+    }
+    else if(is_CTL(*netlist_expr))
     {
       out << "-- " << id << '\n';
       out << "CTLSPEC ";
-      print_smv(netlist, out, netlist_expr);
+      print_smv(netlist, out, *netlist_expr);
       out << '\n';
     }
-    else if(is_LTL(netlist_expr))
+    else if(is_LTL(*netlist_expr))
     {
       out << "-- " << id << '\n';
       out << "LTLSPEC ";
-      print_smv(netlist, out, netlist_expr);
+      print_smv(netlist, out, *netlist_expr);
       out << '\n';
     }
-    else if(is_SVA(netlist_expr))
+    else if(is_SVA(*netlist_expr))
     {
       // Should have been mapped to LTL
       DATA_INVARIANT(false, "smv_netlist got SVA");
     }
     else
     {
-      // neither LTL nor CTL nor SVA
+      // translated to something we can't print
       out << "-- " << id << '\n';
-      out << "-- not translated\n";
+      out << "-- cannot output\n";
       out << '\n';
     }
   }

src/trans-netlist/trans_to_netlist.cpp

@@ -332,8 +332,7 @@ void convert_trans_to_netlistt::operator()(
     auto netlist_expr_opt = netlist_property(
       aig_prop, dest.var_map, property_expr, ns, get_message_handler());
 
-    if(netlist_expr_opt.has_value())
-      dest.properties.emplace(id, netlist_expr_opt.value());
+    dest.properties.emplace(id, netlist_expr_opt);
   }
 
   // find the nondet nodes