CBMC
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 "std_expr.h"
16 
17 #include <limits>
18 
19 class typet;
20 
25 bool to_integer(const constant_exprt &expr, mp_integer &int_value);
26 
30 template <typename Target, typename = void>
31 struct numeric_castt final
32 {
33 };
34 
36 template <>
38 {
39  std::optional<mp_integer> operator()(const exprt &expr) const
40  {
41  if(!expr.is_constant())
42  return {};
43  else
44  return operator()(to_constant_expr(expr));
45  }
46 
47  std::optional<mp_integer> operator()(const constant_exprt &expr) const
48  {
49  mp_integer out;
50  if(to_integer(expr, out))
51  return {};
52  else
53  return out;
54  }
55 };
56 
58 template <typename T>
59 struct numeric_castt<T,
60  typename std::enable_if<std::is_integral<T>::value>::type>
61 {
62 private:
63  // Unchecked conversion from mp_integer when T is signed
64  template <typename U = T,
65  typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
66  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
67  {
68  return mpi.to_long();
69  }
70 
71  // Unchecked conversion from mp_integer when T is unsigned
72  template <typename U = T,
73  typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
74  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
75  {
76  return mpi.to_ulong();
77  }
78 
79 public:
80  // Conversion from mp_integer to integral type T
81  std::optional<T> operator()(const mp_integer &mpi) const
82  {
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 
90  if(
91  mpi <= std::numeric_limits<T>::max() &&
92  mpi >= std::numeric_limits<T>::min())
93  // to_long converts to long long which is the largest signed numeric type
94  return static_cast<T>(get_val(mpi));
95  else
96  return std::nullopt;
97  }
98 
99  // Conversion from expression
100  std::optional<T> operator()(const exprt &expr) const
101  {
102  if(expr.is_constant())
103  return numeric_castt<T>{}(to_constant_expr(expr));
104  else
105  return std::nullopt;
106  }
107 
108  // Conversion from expression
109  std::optional<T> operator()(const constant_exprt &expr) const
110  {
111  if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
112  return numeric_castt<T>{}(*mpi_opt);
113  else
114  return std::nullopt;
115  }
116 };
117 
123 template <typename Target>
124 std::optional<Target> numeric_cast(const exprt &arg)
125 {
126  return numeric_castt<Target>{}(arg);
127 }
128 
134 template <typename Target>
135 Target numeric_cast_v(const mp_integer &arg)
136 {
137  const auto maybe = numeric_castt<Target>{}(arg);
138  INVARIANT(maybe, "mp_integer should be convertible to target integral type");
139  return *maybe;
140 }
141 
147 template <typename Target>
148 Target numeric_cast_v(const constant_exprt &arg)
149 {
150  const auto maybe = numeric_castt<Target>{}(arg);
152  maybe,
153  "expression should be convertible to target integral type",
155  return *maybe;
156 }
157 
158 // PRECONDITION(false) in case of unsupported type
159 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
160 
161 // ceil(log2(size))
162 std::size_t address_bits(const mp_integer &size);
163 
164 mp_integer power(const mp_integer &base, const mp_integer &exponent);
165 
166 void mp_min(mp_integer &a, const mp_integer &b);
167 void mp_max(mp_integer &a, const mp_integer &b);
168 
169 bool get_bvrep_bit(
170  const irep_idt &src,
171  std::size_t width,
172  std::size_t bit_index);
173 
174 irep_idt
175 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
176 
177 irep_idt integer2bvrep(const mp_integer &, std::size_t width);
178 mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
179 
180 #endif // CPROVER_UTIL_ARITH_TOOLS_H
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
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
irep_idt integer2bvrep(const mp_integer &, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
void mp_max(mp_integer &a, const mp_integer &b)
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:135
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
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.
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:124
mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
void mp_min(mp_integer &a, const mp_integer &b)
A constant literal expression.
Definition: std_expr.h:2990
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
The type of an expression, extends irept.
Definition: type.h:29
BigInt mp_integer
Definition: smt_terms.h:17
#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:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
Definition: arith_tools.h:66
std::optional< T > operator()(const constant_exprt &expr) const
Definition: arith_tools.h:109
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
Definition: arith_tools.h:74
Convert expression to mp_integer.
Definition: arith_tools.h:38
std::optional< mp_integer > operator()(const constant_exprt &expr) const
Definition: arith_tools.h:47
std::optional< mp_integer > operator()(const exprt &expr) const
Definition: arith_tools.h:39
Numerical cast provides a unified way of converting from one numerical type to another.
Definition: arith_tools.h:32
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45