Merge pull request #497 from diffblue/ic3-not-supported

EBMC: give error message when unsupported property is passed to IC3

Author: kroening

regression/ebmc/ic3/not_supported1.desc

@@ -0,0 +1,7 @@
+CORE
+not_supported1.sv
+--ic3
+^\[main\.property\.p0\] always s_eventually main\.my_bit: FAILURE: property not supported by IC3 engine$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/ebmc/ic3/not_supported1.sv

@@ -0,0 +1,13 @@
+module main(input clk);
+
+  reg my_bit;
+
+  initial my_bit=0;
+
+  always @(posedge clk)
+    my_bit = !my_bit;
+
+  // expected to pass
+  p0: assert property (s_eventually my_bit);
+
+endmodule

src/ic3/m1ain.cc

@@ -12,10 +12,16 @@ Author: Eugene Goldberg, [email protected]
 #include <util/ui_message.h>
 
 #include <ebmc/ebmc_properties.h>
+#include <ebmc/report_results.h>
 
 #include <trans-netlist/netlist.h>
 #include <trans-netlist/trans_to_netlist.h>
 
+#include <temporal-logic/temporal_expr.h>
+#include <temporal-logic/temporal_logic.h>
+
+#include <verilog/sva_expr.h>
+
 #include <algorithm>
 #include <iostream>
 #include <map>
@@ -48,6 +54,26 @@ int do_ic3(const cmdlinet &cmdline,
   return(ic3_enginet(cmdline,ui_message_handler)());
 } /* end of function do_ic3 */
 
+bool ic3_supports_property(const exprt &expr)
+{
+  if(!is_temporal_operator(expr))
+    return false;
+  else 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;
+}
+
 /*==================================
 
     O P E R A T O R
@@ -87,6 +113,30 @@ int ic3_enginet::operator()()
       message.error() << "no properties" << messaget::eom;
       return 1;
     }
+
+    std::size_t number_of_properties = 0;
+
+    for(auto &property : properties.properties)
+    {
+      if(property.is_disabled())
+        continue;
+
+      // Is it supported by the IC3 engine?
+      if(!ic3_supports_property(property.normalized_expr))
+      {
+        property.failure("property not supported by IC3 engine");
+        continue;
+      }
+
+      number_of_properties++;
+    }
+
+    if(number_of_properties == 0)
+    {
+      namespacet ns(transition_system.symbol_table);
+      report_results(cmdline, properties, ns, message.get_message_handler());
+      return 10;
+    }
   }
   catch(const std::string &error_str)
   {