Merge pull request #389 from diffblue/bmc-unsupported-property

ebmc: reporting when unsupported property is given

Author: tautschnig

regression/ebmc/smv/bdd_unsupported_property.desc

@@ -0,0 +1,9 @@
+CORE
+bdd_unsupported_property.smv
+--bdd
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BDD engine$
+^\[main::spec2\] G main::var::x = FALSE: REFUTED$
+--
+^warning: ignoring

regression/ebmc/smv/bdd_unsupported_property.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN init(x) := 1;
+
+LTLSPEC !G x=0
+LTLSPEC G x=0

regression/ebmc/smv/bmc_unsupported_property1.desc

@@ -0,0 +1,9 @@
+CORE
+bmc_unsupported_property1.smv
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
+^\[main::spec2\] G main::var::x = FALSE: REFUTED$
+--
+^warning: ignoring

regression/ebmc/smv/bmc_unsupported_property1.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN init(x) := 1;
+
+LTLSPEC !G x=0
+LTLSPEC G x=0

regression/ebmc/smv/bmc_unsupported_property2.desc

@@ -0,0 +1,9 @@
+CORE
+bmc_unsupported_property2.smv
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
+^\[main::spec2\] G main::var::x = TRUE: PROVED up to bound 1$
+--
+^warning: ignoring

regression/ebmc/smv/bmc_unsupported_property2.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN init(x) := 1;
+ASSIGN next(x) := x;
+
+LTLSPEC !G x=0 -- unsupported
+LTLSPEC G x=1 -- should pass

src/ebmc/bmc.cpp

@@ -46,6 +46,13 @@ void bmc(
     if(property.is_disabled() || property.is_failure())
       continue;
 
+    // Is it supported by the BMC engine?
+    if(!bmc_supports_property(property.expr))
+    {
+      property.failure("property not supported by BMC engine");
+      continue;
+    }
+
     ::property(
       property.expr,
       property.timeframe_handles,

src/trans-netlist/unwind_netlist.cpp

@@ -7,10 +7,14 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include "unwind_netlist.h"
-#include "instantiate_netlist.h"
 
 #include <util/ebmc_util.h>
 
+#include <temporal-logic/temporal_expr.h>
+#include <verilog/sva_expr.h>
+
+#include "instantiate_netlist.h"
+
 /*******************************************************************\
 
 Function: unwind
@@ -175,12 +179,18 @@ void unwind_property(
     prop_bv.resize(map.get_no_timeframes(), const_literal(true));
     return;
   }
-  
-  if(property_expr.id()!=ID_AG &&
-     property_expr.id()!=ID_sva_always)
-    throw "unsupported property - only SVA always implemented";
 
-  const exprt &p = to_unary_expr(property_expr).op();
+  // 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++)
   {

src/trans-word-level/property.cpp

@@ -13,12 +13,41 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+#include <temporal-logic/temporal_expr.h>
+#include <verilog/sva_expr.h>
+
 #include "instantiate_word_level.h"
 
 #include <cstdlib>
 
 /*******************************************************************\
 
+Function: bmc_supports_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool bmc_supports_property(const exprt &expr)
+{
+  if(expr.is_constant())
+    return true;
+  else if(expr.id() == ID_AG)
+    return true;
+  else if(expr.id() == ID_G)
+    return true;
+  else if(expr.id() == ID_sva_always)
+    return true;
+  else
+    return false;
+}
+
+/*******************************************************************\
+
 Function: property
 
   Inputs:
@@ -45,16 +74,17 @@ void property(
     return;
   }
 
-  if(
-    property_expr.id() != ID_AG && property_expr.id() != ID_G &&
-    property_expr.id() != ID_sva_always)
-  {
-    message.error() << "unsupported property - only SVA always implemented"
-                    << messaget::eom;
-    exit(1);
-  }
-
-  const exprt &p = to_unary_expr(property_expr).op();
+  // 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(std::size_t c = 0; c < no_timeframes; c++)
   {

src/trans-word-level/property.h

@@ -23,6 +23,9 @@ void property(
   std::size_t no_timeframes,
   const namespacet &);
 
+/// Is the given property supported by word-level unwinding?
+bool bmc_supports_property(const exprt &);
+
 /// Adds a constraint that can be used to determine whether the
 /// given state has already been seen earlier in the trace.
 void lasso_constraints(