From 3fa56c68442f475e060dcf10f4cf17a72e27c4c8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 21 Apr 2024 12:05:39 -0700
Subject: [PATCH] netlist-BMC now reports error for unsupported properties

The netlist-based BMC implementation now reports a proper error in the report
when given an unsupported property.
---
 .../ebmc/smv/bmc_unsupported_property3.desc   |  9 +++++++
 .../ebmc/smv/bmc_unsupported_property3.smv    |  8 ++++++
 src/ebmc/ebmc_base.cpp                        |  9 +++++++
 src/trans-netlist/unwind_netlist.cpp          | 25 +++++++++++++++++++
 src/trans-netlist/unwind_netlist.h            |  3 +++
 5 files changed, 54 insertions(+)
 create mode 100644 regression/ebmc/smv/bmc_unsupported_property3.desc
 create mode 100644 regression/ebmc/smv/bmc_unsupported_property3.smv

diff --git a/regression/ebmc/smv/bmc_unsupported_property3.desc b/regression/ebmc/smv/bmc_unsupported_property3.desc
new file mode 100644
index 000000000..8640ec9d2
--- /dev/null
+++ b/regression/ebmc/smv/bmc_unsupported_property3.desc
@@ -0,0 +1,9 @@
+CORE
+bmc_unsupported_property3.smv
+--aig
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by netlist BMC engine$
+^\[main::spec2\] G main::var::x = FALSE: REFUTED$
+--
+^warning: ignoring
diff --git a/regression/ebmc/smv/bmc_unsupported_property3.smv b/regression/ebmc/smv/bmc_unsupported_property3.smv
new file mode 100644
index 000000000..03ed490fe
--- /dev/null
+++ b/regression/ebmc/smv/bmc_unsupported_property3.smv
@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN init(x) := 1;
+
+LTLSPEC !G x=0
+LTLSPEC G x=0
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
index c62d9f666..bddad5acd 100644
--- a/src/ebmc/ebmc_base.cpp
+++ b/src/ebmc/ebmc_base.cpp
@@ -77,6 +77,9 @@ int ebmc_baset::finish_bit_level_bmc(const bmc_mapt &bmc_map, propt &solver)
     if(property.is_disabled())
       continue;
 
+    if(property.is_failure())
+      continue;
+
     message.status() << "Checking " << property.name << messaget::eom;
 
     literalt property_literal=!solver.land(property.timeframe_literals);
@@ -199,6 +202,12 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
       if(property.is_disabled())
         continue;
 
+      if(!netlist_bmc_supports_property(property.normalized_expr))
+      {
+        property.failure("property not supported by netlist BMC engine");
+        continue;
+      }
+
       ::unwind_property(
         property.normalized_expr,
         property.timeframe_literals,
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
index 9fd603b28..b50bdc771 100644
--- a/src/trans-netlist/unwind_netlist.cpp
+++ b/src/trans-netlist/unwind_netlist.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ebmc_util.h>
 
 #include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
 #include "instantiate_netlist.h"
@@ -199,3 +200,27 @@ void unwind_property(
   }
 }
 
+/*******************************************************************\
+
+Function: netlist_bmc_supports_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool netlist_bmc_supports_property(const exprt &expr)
+{
+  // We do AG p only.
+  if(expr.id() == ID_AG)
+    return !has_temporal_operator(to_AG_expr(expr).op());
+  else if(expr.id() == ID_G)
+    return !has_temporal_operator(to_G_expr(expr).op());
+  else if(expr.id() == ID_sva_always)
+    return !has_temporal_operator(to_sva_always_expr(expr).op());
+  else
+    return false;
+}
diff --git a/src/trans-netlist/unwind_netlist.h b/src/trans-netlist/unwind_netlist.h
index 9ad9a02ad..67e50f0ce 100644
--- a/src/trans-netlist/unwind_netlist.h
+++ b/src/trans-netlist/unwind_netlist.h
@@ -42,6 +42,9 @@ void unwind_property(
   const bmc_mapt &,
   const namespacet &);
 
+// Is the property supported?
+bool netlist_bmc_supports_property(const exprt &);
+
 // unwind a property that is given as netlist node
 void unwind_property(
   const bmc_mapt &,