Merge pull request #1204 from diffblue/bmc-throughout

BMC: LHS of SVA `throughout` is a state predicate

Author: tautschnig

src/trans-word-level/instantiate_word_level.cpp

@@ -207,7 +207,7 @@ exprt instantiate(
 
 /*******************************************************************\
 
-Function: instantiate_property
+Function: instantiate_state_predicate
 
   Inputs:
 
@@ -217,11 +217,12 @@ Function: instantiate_property
 
 \*******************************************************************/
 
-exprt instantiate_property(
+exprt instantiate_state_predicate(
   const exprt &expr,
   const mp_integer &current,
   const mp_integer &no_timeframes)
 {
+  PRECONDITION(expr.type().id() == ID_bool);
   wl_instantiatet wl_instantiate(no_timeframes, false);
   return wl_instantiate(expr, current);
 }

src/trans-word-level/instantiate_word_level.h

@@ -21,7 +21,7 @@ exprt instantiate(
 
 // Instantiate an atomic state predicate in the given time frame.
 // Must not contain next_symbol or any temporal operators.
-exprt instantiate_property(
+exprt instantiate_state_predicate(
   const exprt &,
   const mp_integer &current,
   const mp_integer &no_timeframes);

src/trans-word-level/property.cpp

@@ -511,7 +511,8 @@ static obligationst property_obligations_rec(
   {
     // we rely on NNF
     auto &if_expr = to_if_expr(property_expr);
-    auto cond = instantiate_property(if_expr.cond(), current, no_timeframes);
+    auto cond =
+      instantiate_state_predicate(if_expr.cond(), current, no_timeframes);
     auto obligations_true =
       property_obligations_rec(if_expr.true_case(), current, no_timeframes)
         .conjunction();
@@ -571,7 +572,8 @@ static obligationst property_obligations_rec(
     {
       // state formula
       return obligationst{
-        current, instantiate_property(property_expr, current, no_timeframes)};
+        current,
+        instantiate_state_predicate(property_expr, current, no_timeframes)};
     }
   }
   else if(property_expr.id() == ID_sva_implies)
@@ -739,7 +741,8 @@ static obligationst property_obligations_rec(
   else
   {
     return obligationst{
-      current, instantiate_property(property_expr, current, no_timeframes)};
+      current,
+      instantiate_state_predicate(property_expr, current, no_timeframes)};
   }
 }
 
@@ -755,26 +758,6 @@ Function: property_obligations
 
 \*******************************************************************/
 
-obligationst property_obligations(
-  const exprt &property_expr,
-  const mp_integer &t,
-  const mp_integer &no_timeframes)
-{
-  return property_obligations_rec(property_expr, t, no_timeframes);
-}
-
-/*******************************************************************\
-
-Function: property_obligations
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 obligationst property_obligations(
   const exprt &property_expr,
   const mp_integer &no_timeframes)

src/trans-word-level/property.h

@@ -22,11 +22,4 @@ exprt::operandst property(
 /// Is the given property supported by word-level unwinding?
 bool bmc_supports_property(const exprt &);
 
-class obligationst;
-
-obligationst property_obligations(
-  const exprt &,
-  const mp_integer &t,
-  const mp_integer &no_timeframes);
-
 #endif

src/trans-word-level/sequence.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "instantiate_word_level.h"
 #include "obligations.h"
-#include "property.h"
 
 // condition on counters for ocurrences of non-consecutive repetitions
 exprt sequence_count_condition(
@@ -259,9 +258,9 @@ sequence_matchest instantiate_sequence_rec(
 
       for(mp_integer new_t = t; new_t <= match.end_time; ++new_t)
       {
-        auto obligations =
-          property_obligations(throughout.lhs(), new_t, no_timeframes);
-        conjuncts.push_back(obligations.conjunction().second);
+        auto lhs_inst =
+          instantiate_state_predicate(throughout.lhs(), new_t, no_timeframes);
+        conjuncts.push_back(lhs_inst);
       }
 
       result.emplace_back(match.end_time, conjunction(conjuncts));
@@ -437,7 +436,8 @@ sequence_matchest instantiate_sequence_rec(
   {
     // a state predicate
     auto &predicate = to_sva_boolean_expr(expr).op();
-    auto instantiated = instantiate_property(predicate, t, no_timeframes);
+    auto instantiated =
+      instantiate_state_predicate(predicate, t, no_timeframes);
     return {{t, instantiated}};
   }
   else