Merge pull request #1052 from diffblue/netlist-expr

netlists can now track properties with arbitrary shapes

Author: tautschnig

src/ebmc/bdd_engine.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ebmc/liveness_to_safety.h>
 #include <ebmc/transition_system.h>
 #include <solvers/bdd/miniBDD/miniBDD.h>
+#include <solvers/prop/literal_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <temporal-logic/ctl.h>
 #include <temporal-logic/ltl.h>
@@ -1057,7 +1058,14 @@ void bdd_enginet::build_BDDs()
         // find the netlist property
         auto netlist_property = netlist.properties.find(property.identifier);
         CHECK_RETURN(netlist_property != netlist.properties.end());
-        auto l = std::get<netlistt::Gpt>(netlist_property->second).p;
+        DATA_INVARIANT(
+          netlist_property->second.id() == ID_sva_always,
+          "assumed property must be sva_always");
+        auto &p = to_sva_always_expr(netlist_property->second).op();
+        DATA_INVARIANT(
+          p.id() == ID_literal,
+          "assumed property must be sva_assume sva_assert literal");
+        auto l = to_literal_expr(p).get_literal();
         constraints_BDDs.push_back(aig2bdd(l, BDDs));
       }
     }

src/temporal-logic/temporal_logic.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr_util.h>
 
+#include <verilog/sva_expr.h>
+
 bool is_temporal_operator(const exprt &expr)
 {
   return is_CTL_operator(expr) || is_LTL_operator(expr) ||
@@ -136,3 +138,17 @@ bool is_SVA(const exprt &expr)
 
   return !has_subexpr(expr, non_SVA_operator);
 }
+
+bool is_SVA_always_p(const exprt &expr)
+{
+  return expr.id() == ID_sva_always &&
+         !has_temporal_operator(to_sva_always_expr(expr).op());
+}
+
+bool is_SVA_always_s_eventually_p(const exprt &expr)
+{
+  return expr.id() == ID_sva_always &&
+         to_sva_always_expr(expr).op().id() == ID_sva_s_eventually &&
+         !has_temporal_operator(
+           to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op());
+}

src/temporal-logic/temporal_logic.h

@@ -71,4 +71,10 @@ bool is_SVA_operator(const exprt &);
 /// Returns true iff the given expression is an SVA expression
 bool is_SVA(const exprt &);
 
+/// Returns true iff the given expression is always p
+bool is_SVA_always_p(const exprt &);
+
+/// Returns true iff the given expression is always s_eventually p
+bool is_SVA_always_s_eventually_p(const exprt &);
+
 #endif

src/trans-netlist/instantiate_netlist.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ebmc/ebmc_error.h>
 #include <solvers/flattening/boolbv.h>
+#include <solvers/prop/literal_expr.h>
+#include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
 #include <cassert>
@@ -272,3 +274,86 @@ literalt instantiate_var_mapt::get_literal(
   return var_map.get_current(symbol, bit);
 }
 
+/*******************************************************************\
+
+Function: netlist_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::optional<exprt> netlist_property(
+  propt &solver,
+  const var_mapt &var_map,
+  const exprt &expr,
+  const namespacet &ns,
+  message_handlert &message_handler)
+{
+  if(is_temporal_operator(expr))
+  {
+    if(is_LTL_operator(expr) || is_CTL_operator(expr))
+    {
+      exprt copy = expr;
+      for(auto &op : copy.operands())
+      {
+        auto op_opt =
+          netlist_property(solver, var_map, op, ns, message_handler);
+        if(op_opt.has_value())
+          op = op_opt.value();
+        else
+          return {};
+      }
+      return copy;
+    }
+    else if(is_SVA_operator(expr))
+    {
+      if(expr.id() == ID_sva_always || expr.id() == ID_sva_assume)
+      {
+        auto copy = expr;
+        auto &op = to_unary_expr(copy).op();
+        auto op_opt =
+          netlist_property(solver, var_map, op, ns, message_handler);
+        if(op_opt.has_value())
+        {
+          op = op_opt.value();
+          return copy;
+        }
+        else
+          return {};
+      }
+      else
+        return {};
+    }
+    else
+      return {};
+  }
+  else if(!has_temporal_operator(expr))
+  {
+    auto l = instantiate_convert(solver, var_map, expr, ns, message_handler);
+    return literal_exprt{l};
+  }
+  else if(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not ||
+    expr.id() == ID_implies || expr.id() == ID_xor || expr.id() == ID_xnor)
+  {
+    exprt copy = expr;
+    for(auto &op : copy.operands())
+    {
+      auto op_opt = netlist_property(solver, var_map, op, ns, message_handler);
+      if(op_opt.has_value())
+        op = op_opt.value();
+      else
+        return {};
+    }
+    return copy;
+  }
+  else
+  {
+    // contains temporal operator, but not propositional skeleton
+    return {};
+  }
+}

src/trans-netlist/instantiate_netlist.h

@@ -30,7 +30,14 @@ literalt instantiate_convert(
   const exprt &expr,
   const namespacet &,
   message_handlert &);
-  
+
+std::optional<exprt> netlist_property(
+  propt &solver,
+  const var_mapt &var_map,
+  const exprt &expr,
+  const namespacet &,
+  message_handlert &);
+
 void instantiate_convert(
   propt &solver,
   const var_mapt &var_map,

src/trans-netlist/netlist.cpp

@@ -6,11 +6,19 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <ctype.h>
+#include "netlist.h"
+
+#include <util/namespace.h>
+#include <util/symbol_table.h>
 
+#include <smvlang/expr2smv.h>
 #include <solvers/flattening/boolbv_width.h>
+#include <solvers/prop/literal_expr.h>
+#include <temporal-logic/temporal_logic.h>
+#include <verilog/sva_expr.h>
 
-#include "netlist.h"
+#include <ctype.h>
+#include <sstream>
 
 /*******************************************************************\
 
@@ -352,30 +360,54 @@ void netlistt::output_smv(std::ostream &out) const
   out << "-- Properties" << '\n';
   out << '\n';
 
-  for(auto &[id, property] : properties)
+  for(auto &[id, netlist_expr] : properties)
   {
-    if(std::holds_alternative<Gpt>(property))
+    if(is_CTL(netlist_expr))
     {
       out << "-- " << id << '\n';
-      out << "LTLSPEC G ";
-      print_smv(out, std::get<Gpt>(property).p);
+      out << "CTLSPEC ";
+      print_smv(out, netlist_expr);
       out << '\n';
     }
-    else if(std::holds_alternative<GFpt>(property))
+    else if(is_LTL(netlist_expr))
     {
       out << "-- " << id << '\n';
-      out << "LTLSPEC G F ";
-      print_smv(out, std::get<GFpt>(property).p);
+      out << "LTLSPEC ";
+      print_smv(out, netlist_expr);
       out << '\n';
     }
-    else if(std::holds_alternative<not_translatedt>(property))
+    else if(is_SVA(netlist_expr))
+    {
+      if(is_SVA_always_p(netlist_expr))
+      {
+        out << "-- " << id << '\n';
+        out << "CTLSPEC AG ";
+        print_smv(out, to_sva_always_expr(netlist_expr).op());
+        out << '\n';
+      }
+      else if(is_SVA_always_s_eventually_p(netlist_expr))
+      {
+        out << "-- " << id << '\n';
+        out << "CTLSPEC AG AF ";
+        print_smv(
+          out,
+          to_sva_s_eventually_expr(to_sva_always_expr(netlist_expr).op()).op());
+        out << '\n';
+      }
+      else
+      {
+        out << "-- " << id << '\n';
+        out << "-- not translated\n";
+        out << '\n';
+      }
+    }
+    else
     {
+      // neither LTL nor CTL nor SVA
       out << "-- " << id << '\n';
       out << "-- not translated\n";
       out << '\n';
     }
-    else
-      UNREACHABLE;
   }
 }
 
@@ -467,3 +499,36 @@ void netlistt::print_smv(
     out << "unknown";
 }
 
+/*******************************************************************\
+
+Function: netlistt::print_smv
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void netlistt::print_smv(std::ostream &out, const exprt &expr) const
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+
+  // replace literal expressions by symbols
+
+  exprt replaced = expr;
+  replaced.visit_pre(
+    [this](exprt &node)
+    {
+      if(node.id() == ID_literal)
+      {
+        std::ostringstream buffer;
+        print_smv(buffer, to_literal_expr(node).get_literal());
+        node = symbol_exprt{buffer.str(), node.type()};
+      }
+    });
+
+  out << expr2smv(replaced, ns);
+}

src/trans-netlist/netlist.h

@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_TRANS_NETLIST_H
 #define CPROVER_TRANS_NETLIST_H
 
+#include <util/expr.h>
+
 #include "aig.h"
 #include "var_map.h"
 
@@ -53,29 +55,15 @@ class netlistt:public aig_plus_constraintst
   bvt initial;
   bvt transition;
 
-  struct Gpt
-  {
-    literalt p;
-  };
-
-  struct GFpt
-  {
-    literalt p;
-  };
-
-  struct not_translatedt
-  {
-  };
-
-  using propertyt = std::variant<Gpt, GFpt, not_translatedt>;
-
-  // map from property ID to property netlist nodes
-  using propertiest = std::map<irep_idt, propertyt>;
+  // Map from property ID to a netlist property,
+  // which uses literal_exprt.
+  using propertiest = std::map<irep_idt, exprt>;
   propertiest properties;
 
 protected:
   static std::string id2smv(const irep_idt &id);
-  void print_smv(std::ostream &out, literalt l) const;
+  void print_smv(std::ostream &, literalt) const;
+  void print_smv(std::ostream &, const exprt &) const;
 };
 
 #endif