BMC: word-level property instantiation now uses mp_integer

This changes the time frame index type from std::size_t by mp_integer, which
avoids having to deal with possible overflow when adding.

Author: kroening

src/trans-word-level/instantiate_word_level.cpp

@@ -29,9 +29,9 @@ Function: timeframe_identifier
 \*******************************************************************/
 
 std::string
-timeframe_identifier(std::size_t timeframe, const irep_idt &identifier)
+timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier)
 {
-  return id2string(identifier)+"@"+std::to_string(timeframe);
+  return id2string(identifier) + "@" + integer2string(timeframe);
 }
 
 /*******************************************************************\
@@ -46,7 +46,7 @@ Function: timeframe_symbol
 
 \*******************************************************************/
 
-symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt src)
+symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 {
   auto result = std::move(src);
   result.set_identifier(
@@ -69,23 +69,23 @@ symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  wl_instantiatet(std::size_t _no_timeframes, const namespacet &_ns)
+  wl_instantiatet(const mp_integer &_no_timeframes, const namespacet &_ns)
     : no_timeframes(_no_timeframes), ns(_ns)
   {
   }
 
   /// Instantiate the given expression for timeframe t
-  [[nodiscard]] exprt operator()(exprt expr, std::size_t t) const
+  [[nodiscard]] exprt operator()(exprt expr, const mp_integer &t) const
   {
     return instantiate_rec(std::move(expr), t);
   }
 
 protected:
-  std::size_t no_timeframes;
+  const mp_integer &no_timeframes;
   const namespacet &ns;
 
-  [[nodiscard]] exprt instantiate_rec(exprt, std::size_t t) const;
-  [[nodiscard]] typet instantiate_rec(typet, std::size_t t) const;
+  [[nodiscard]] exprt instantiate_rec(exprt, const mp_integer &t) const;
+  [[nodiscard]] typet instantiate_rec(typet, const mp_integer &t) const;
 };
 
 /*******************************************************************\
@@ -100,7 +100,7 @@ Function: wl_instantiatet::instantiate_rec
 
 \*******************************************************************/
 
-exprt wl_instantiatet::instantiate_rec(exprt expr, const std::size_t t) const
+exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
 {
   expr.type() = instantiate_rec(expr.type(), t);
 
@@ -158,7 +158,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const std::size_t t) const
         if(to_integer_non_constant(ternary_expr.op0(), offset))
           throw "failed to convert sva_cycle_delay offset";
 
-        const auto u = t + offset.to_ulong();
+        const auto u = t + offset;
 
         // Do we exceed the bound? Make it 'true'
         if(u >= no_timeframes)
@@ -186,7 +186,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const std::size_t t) const
 
         for(mp_integer offset=from; offset<to; ++offset)
         {
-          auto u = t + offset.to_ulong();
+          auto u = t + offset;
 
           if(u >= no_timeframes)
           {
@@ -219,7 +219,7 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const std::size_t t) const
 
     exprt::operandst conjuncts;
 
-    for(auto u = t; u < no_timeframes; u++)
+    for(auto u = t; u < no_timeframes; ++u)
     {
       conjuncts.push_back(instantiate_rec(op, u));
     }
@@ -261,11 +261,11 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const std::size_t t) const
     exprt::operandst conjuncts = {};
     const auto i = t;
 
-    for(std::size_t k = 0; k < i; k++)
+    for(mp_integer k = 0; k < i; ++k)
     {
       exprt::operandst disjuncts = {not_exprt(lasso_symbol(k, i))};
 
-      for(std::size_t j = k; j <= i; j++)
+      for(mp_integer j = k; j <= i; ++j)
       {
         disjuncts.push_back(instantiate_rec(p, j));
       }
@@ -338,7 +338,7 @@ Function: wl_instantiatet::instantiate_rec
 
 \*******************************************************************/
 
-typet wl_instantiatet::instantiate_rec(typet type, std::size_t) const
+typet wl_instantiatet::instantiate_rec(typet type, const mp_integer &) const
 {
   return type;
 }
@@ -357,8 +357,8 @@ Function: instantiate
 
 exprt instantiate(
   const exprt &expr,
-  std::size_t t,
-  std::size_t no_timeframes,
+  const mp_integer &t,
+  const mp_integer &no_timeframes,
   const namespacet &ns)
 {
   wl_instantiatet wl_instantiate(no_timeframes, ns);

src/trans-word-level/instantiate_word_level.h

@@ -9,19 +9,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 #define CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 
-#include <solvers/prop/prop_conv.h>
-
+#include <util/mp_arith.h>
 #include <util/namespace.h>
 
+#include <solvers/prop/prop_conv.h>
+
 exprt instantiate(
   const exprt &expr,
-  std::size_t current,
-  std::size_t no_timeframes,
+  const mp_integer &current,
+  const mp_integer &no_timeframes,
   const namespacet &);
 
 std::string
-timeframe_identifier(std::size_t timeframe, const irep_idt &identifier);
+timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
 
-symbol_exprt timeframe_symbol(std::size_t timeframe, symbol_exprt);
+symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt);
 
 #endif

src/trans-word-level/property.cpp

@@ -109,8 +109,8 @@ Function: states_equal
 \*******************************************************************/
 
 exprt states_equal(
-  std::size_t k,
-  std::size_t i,
+  const mp_integer &k,
+  const mp_integer &i,
   const std::vector<symbol_exprt> &variables_to_compare)
 {
   // We require k<i to avoid the symmetric constraints.
@@ -141,13 +141,13 @@ Function: lasso_symbol
 
 \*******************************************************************/
 
-symbol_exprt lasso_symbol(std::size_t k, std::size_t i)
+symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i)
 {
   // True when states i and k are equal.
   // We require k<i to avoid the symmetric constraints.
   PRECONDITION(k < i);
   irep_idt lasso_identifier =
-    "lasso::" + std::to_string(i) + "-back-to-" + std::to_string(k);
+    "lasso::" + integer2string(i) + "-back-to-" + integer2string(k);
   return symbol_exprt(lasso_identifier, bool_typet());
 }
 
@@ -165,7 +165,7 @@ Function: lasso_constraints
 
 void lasso_constraints(
   decision_proceduret &solver,
-  std::size_t no_timeframes,
+  const mp_integer &no_timeframes,
   const namespacet &ns,
   const irep_idt &module_identifier)
 {
@@ -204,9 +204,9 @@ void lasso_constraints(
     }
   }
 
-  for(std::size_t i = 1; i < no_timeframes; i++)
+  for(mp_integer i = 1; i < no_timeframes; ++i)
   {
-    for(std::size_t k = 0; k < i; k++)
+    for(mp_integer k = 0; k < i; ++k)
     {
       // Is there a loop back from time frame i back to time frame k?
       auto lasso_symbol = ::lasso_symbol(k, i);

src/trans-word-level/property.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/expr.h>
 #include <util/message.h>
+#include <util/mp_arith.h>
 #include <util/namespace.h>
 
 #include <solvers/decision_procedure.h>
@@ -30,13 +31,13 @@ bool bmc_supports_property(const exprt &);
 /// given state has already been seen earlier in the trace.
 void lasso_constraints(
   decision_proceduret &,
-  std::size_t no_timeframes,
+  const mp_integer &no_timeframes,
   const namespacet &,
   const irep_idt &module_identifier);
 
 /// Is there a loop from i back to k?
 /// Precondition: k<i
-symbol_exprt lasso_symbol(std::size_t k, std::size_t i);
+symbol_exprt lasso_symbol(const mp_integer &k, const mp_integer &i);
 
 /// Returns true iff the given property requires lasso constraints for BMC.
 bool requires_lasso_constraints(const exprt &);