Merge pull request #283 from diffblue/bdd-refuse

ebmc: BDD engine now refuses properties it does not support

Author: tautschnig

regression/ebmc/BDD/BDD_SVA1.desc

@@ -0,0 +1,16 @@
+CORE
+BDD_SVA1.sv
+--bdd
+^EXIT=10$
+^SIGNAL=0$
+^\[top\.property\.p0\] always top\.my_bit: PROVED$
+^\[top\.property\.p1\] always top\.my_bit: PROVED$
+^\[top\.property\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): UNKNOWN$
+^\[top\.property\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): PROVED$
+^\[top\.property\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): UNKNOWN$
+^\[top\.property\.p5\] always eventually top\.counter == 8: UNKNOWN$
+^\[top\.property\.p6\] always \(top\.counter == 0 \|-> \(eventually top\.counter == 8\)\): UNKNOWN$
+^\[top\.property\.p7\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until top\.counter == 6\)\): UNKNOWN$
+^\[top\.property\.p8\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until_with top\.counter == 5\)\): UNKNOWN$
+--
+^warning: ignoring

regression/ebmc/BDD/BDD_SVA1.sv

@@ -0,0 +1,24 @@
+module top(input clock);
+
+  reg my_bit;
+  reg [31:0] counter;
+
+  initial my_bit=1;
+  initial counter=0;
+
+  always @(posedge clock) begin
+    my_bit=my_bit;
+    counter=counter+1;
+  end
+  
+  p0: assert property (my_bit);
+  p1: assert property (always my_bit);
+  p2: assert property (counter==3 |-> nexttime counter==4);
+  p3: assert property (counter==3 |=> counter==4);
+  p4: assert property (counter==3 |=> nexttime counter==5);
+  p5: assert property (eventually counter==8);
+  p6: assert property (counter==0 |-> eventually counter==8);
+  p7: assert property (counter==0 |-> counter<=5 until counter==6);
+  p8: assert property (counter==0 |-> counter<=5 until_with counter==5);
+
+endmodule

src/ebmc/bdd_engine.cpp

@@ -419,12 +419,14 @@ void bdd_enginet::check_property(propertyt &property)
   message.status() << "Checking " << property.name << messaget::eom;
   property.status=propertyt::statust::UNKNOWN;
 
-  // special treatment for always
+  // special treatment for AGp
+  auto is_AGp = [](const exprt &expr) {
+    return (expr.id() == ID_AG || expr.id() == ID_sva_always) &&
+           !has_temporal_operator(to_unary_expr(expr).op());
+  };
 
-  if(property.expr.id()==ID_AG ||
-     property.expr.id()==ID_sva_always)
+  if(is_AGp(property.expr))
   {
-    // recursive call
     const exprt &sub_expr = to_unary_expr(property.expr).op();
     BDD p=property2BDD(sub_expr);
 
@@ -491,7 +493,7 @@ void bdd_enginet::check_property(propertyt &property)
       peak_bdd_nodes=std::max(peak_bdd_nodes, mgr.number_of_nodes());
     }
   }
-  else
+  else if(!has_temporal_operator(property.expr))
   {
     // We check whether the BDD for the negation of the property
     // contains an initial state.

src/trans-word-level/property.cpp

@@ -214,3 +214,45 @@ bool requires_lasso_constraints(const exprt &expr)
 
   return false;
 }
+
+/*******************************************************************\
+
+Function: has_temporal_operator
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool has_temporal_operator(const exprt &expr)
+{
+  for(auto subexpr_it = expr.depth_cbegin(), subexpr_end = expr.depth_cend();
+      subexpr_it != subexpr_end;
+      subexpr_it++)
+  {
+    // clang-format off
+    if(
+      subexpr_it->id() == ID_AG || subexpr_it->id() == ID_EG ||
+      subexpr_it->id() == ID_AF || subexpr_it->id() == ID_EF ||
+      subexpr_it->id() == ID_AX || subexpr_it->id() == ID_EX ||
+      subexpr_it->id() == ID_A || subexpr_it->id() == ID_E ||
+      subexpr_it->id() == ID_U || subexpr_it->id() == ID_R ||
+      subexpr_it->id() == ID_G || subexpr_it->id() == ID_F ||
+      subexpr_it->id() == ID_X ||
+      subexpr_it->id() == ID_sva_always || subexpr_it->id() == ID_sva_always ||
+      subexpr_it->id() == ID_sva_nexttime || subexpr_it->id() == ID_sva_s_nexttime ||
+      subexpr_it->id() == ID_sva_until || subexpr_it->id() == ID_sva_s_until ||
+      subexpr_it->id() == ID_sva_until_with || subexpr_it->id() == ID_sva_s_until_with ||
+      subexpr_it->id() == ID_sva_eventually ||
+      subexpr_it->id() == ID_sva_s_eventually)
+    {
+      return true;
+    }
+    // clang-format on
+  }
+
+  return false;
+}

src/trans-word-level/property.h

@@ -38,8 +38,7 @@ symbol_exprt lasso_symbol(std::size_t k, std::size_t i);
 /// Returns true iff the given property requires lasso constraints for BMC.
 bool requires_lasso_constraints(const exprt &);
 
-/// Returns true iff the given property is a liveness property when
-/// given an infinite trace.
-bool is_liveness_property(const exprt &);
+/// Returns true iff the given expression contains a temporal operator
+bool has_temporal_operator(const exprt &);
 
 #endif