Merge pull request #689 from diffblue/aig-past

better error reporting when $past is unsupported

Author: tautschnig

regression/verilog/system-functions/past1.aig.desc

@@ -0,0 +1,7 @@
+CORE
+past1.sv
+--aig
+^\[main\.p0\] ##0 \(\$past\(main\.counter, 0\)\) == 0: FAILURE: property not supported by netlist BMC engine$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/system-functions/past1.bdd.desc

@@ -0,0 +1,7 @@
+CORE
+past1.sv
+--bdd
+^\[main\.p0\] ##0 \(\$past\(main\.counter, 0\)\) == 0: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/system-functions/past2.desc

@@ -1,8 +1,8 @@
 CORE
 past2.sv
 --bdd
-^file .* line \d+: error: no support for \$past when using AIG backends$
-^EXIT=6$
+^\[main\.p0\] always \(main\.counter == 0 \|-> \(\$past\(main\.counter, 1\)\) == 0\): FAILURE: property not supported by BDD engine$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/ebmc/bdd_engine.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "bdd_engine.h"
 
+#include <util/expr_util.h>
 #include <util/format_expr.h>
 
 #include <solvers/bdd/miniBDD/miniBDD.h>
@@ -175,6 +176,17 @@ property_checker_resultt bdd_enginet::operator()()
 {
   try
   {
+    for(auto &property : properties.properties)
+    {
+      // no support for $past
+      if(has_subexpr(property.normalized_expr, ID_verilog_past))
+        property.failure("property not supported by BDD engine");
+    }
+
+    // any properties left?
+    if(!properties.has_unknown_property())
+      return property_checker_resultt::VERIFICATION_RESULT;
+
     const auto property_map = properties.make_property_map();
 
     message.status() << "Building netlist" << messaget::eom;
@@ -882,7 +894,8 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr)
     expr.id() == ID_implies || is_temporal_operator(expr))
   {
     for(const auto & op : expr.operands())
-      get_atomic_propositions(op);
+      if(op.type().id() == ID_bool)
+        get_atomic_propositions(op);
   }
   else
   {

src/ebmc/ebmc_properties.h

@@ -182,6 +182,15 @@ class ebmc_propertiest
     return true;
   }
 
+  bool has_unknown_property() const
+  {
+    for(const auto &p : properties)
+      if(p.is_unknown())
+        return true;
+
+    return false;
+  }
+
   bool requires_lasso_constraints() const
   {
     for(const auto &p : properties)

src/trans-netlist/unwind_netlist.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "unwind_netlist.h"
 
 #include <util/ebmc_util.h>
+#include <util/expr_util.h>
 
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
@@ -170,6 +171,10 @@ Function: netlist_bmc_supports_property
 
 bool netlist_bmc_supports_property(const exprt &expr)
 {
+  // No $past.
+  if(has_subexpr(expr, ID_verilog_past))
+    return false;
+
   // We do AG p only.
   if(expr.id() == ID_AG)
     return !has_temporal_operator(to_AG_expr(expr).op());