cprover
arith_tools.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_ARITH_TOOLS_H
11 #define CPROVER_UTIL_ARITH_TOOLS_H
12 
13 #include "invariant.h"
14 #include "mp_arith.h"
15 #include "optional.h"
16 #include "std_expr.h"
17 
18 #include "deprecate.h"
19 
20 class typet;
21 
22 // this one will go away
23 // returns 'true' on error
25 DEPRECATED("Use the constant_exprt version instead")
26 bool to_integer(const exprt &expr, mp_integer &int_value);
27 
28 // returns 'true' on error
29 bool to_integer(const constant_exprt &expr, mp_integer &int_value);
30 
31 // returns 'true' on error
32 DEPRECATED("Use numeric_cast<unsigned>(e) instead")
33 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);
34 
38 template <typename Target, typename = void>
39 struct numeric_castt final
40 {
41 };
42 
44 template <>
46 {
48  {
49  mp_integer out;
50  if(expr.id() != ID_constant || to_integer(to_constant_expr(expr), out))
51  return {};
52  return out;
53  }
54 };
55 
57 template <typename T>
58 struct numeric_castt<T,
59  typename std::enable_if<std::is_integral<T>::value>::type>
60 {
61 private:
62  // Unchecked conversion from mp_integer when T is signed
63  template <typename U = T,
64  typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
65  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
66  {
67  return mpi.to_long();
68  }
69 
70  // Unchecked conversion from mp_integer when T is unsigned
71  template <typename U = T,
72  typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
73  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
74  {
75  return mpi.to_ulong();
76  }
77 
78 public:
79  // Conversion from mp_integer to integral type T
81  {
82 #if !defined(_MSC_VER) || _MSC_VER >= 1900
83  static_assert(
84  std::numeric_limits<T>::max() <=
85  std::numeric_limits<decltype(get_val(mpi))>::max() &&
86  std::numeric_limits<T>::min() >=
87  std::numeric_limits<decltype(get_val(mpi))>::min(),
88  "Numeric cast only works for types smaller than long long");
89 #else
90  // std::numeric_limits<> methods are not declared constexpr in old versions
91  // of VS
93  std::numeric_limits<T>::max() <=
94  std::numeric_limits<decltype(get_val(mpi))>::max() &&
95  std::numeric_limits<T>::min() >=
96  std::numeric_limits<decltype(get_val(mpi))>::min());
97 #endif
98  if(
99  mpi <= std::numeric_limits<T>::max() &&
100  mpi >= std::numeric_limits<T>::min())
101  // to_long converts to long long which is the largest signed numeric type
102  return static_cast<T>(get_val(mpi));
103  else
104  return {};
105  }
106 
107  // Conversion from expression
108  optionalt<T> operator()(const exprt &expr) const
109  {
110  if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
111  return numeric_castt<T>{}(*mpi_opt);
112  else
113  return {};
114  }
115 };
116 
122 template <typename Target>
124 {
125  return numeric_castt<Target>{}(arg);
126 }
127 
133 template <typename Target>
134 Target numeric_cast_v(const mp_integer &arg)
135 {
136  const auto maybe = numeric_castt<Target>{}(arg);
137  INVARIANT(maybe, "mp_integer should be convertible to target integral type");
138  return *maybe;
139 }
140 
146 template <typename Target>
147 Target numeric_cast_v(const exprt &arg)
148 {
149  const auto maybe = numeric_castt<Target>{}(arg);
151  maybe,
152  "expression should be convertible to target integral type",
154  return *maybe;
155 }
156 
157 // PRECONDITION(false) in case of unsupported type
158 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
159 
160 // ceil(log2(size))
161 std::size_t address_bits(const mp_integer &size);
162 
163 mp_integer power(const mp_integer &base, const mp_integer &exponent);
164 
165 void mp_min(mp_integer &a, const mp_integer &b);
166 void mp_max(mp_integer &a, const mp_integer &b);
167 
168 bool get_bvrep_bit(
169  const irep_idt &src,
170  std::size_t width,
171  std::size_t bit_index);
172 
173 irep_idt
174 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
175 
176 irep_idt integer2bvrep(const mp_integer &, std::size_t width);
177 mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
178 
179 #endif // CPROVER_UTIL_ARITH_TOOLS_H
irep_idt integer2bvrep(const mp_integer &, std::size_t width)
convert an integer to bit-vector representation with given width This uses two&#39;s complement for negat...
The type of an expression, extends irept.
Definition: type.h:27
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
BigInt mp_integer
Definition: mp_arith.h:22
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
Definition: arith_tools.h:134
mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
Definition: arith_tools.h:65
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Numerical cast provides a unified way of converting from one numerical type to another.
Definition: arith_tools.h:39
void mp_min(mp_integer &a, const mp_integer &b)
STL namespace.
A constant literal expression.
Definition: std_expr.h:4384
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
Convert expression to mp_integer.
Definition: arith_tools.h:45
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
const irep_idt & id() const
Definition: irep.h:259
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
Definition: arith_tools.h:73
void mp_max(mp_integer &a, const mp_integer &b)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
API to expression classes.
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
optionalt< mp_integer > operator()(const exprt &expr) const
Definition: arith_tools.h:47
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
#define DEPRECATED(msg)
Definition: deprecate.h:23
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Base class for all expressions.
Definition: expr.h:54
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:414
constant_exprt from_integer(const mp_integer &int_value, const typet &type)