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 bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);
33 
37 template <typename Target, typename = void>
38 struct numeric_castt final
39 {
40 };
41 
43 template <>
45 {
47  {
48  mp_integer out;
49  if(expr.id() != ID_constant || to_integer(to_constant_expr(expr), out))
50  return {};
51  return out;
52  }
53 };
54 
56 template <typename T>
57 struct numeric_castt<T,
58  typename std::enable_if<std::is_integral<T>::value>::type>
59 {
60 private:
61  // Unchecked conversion from mp_integer when T is signed
62  template <typename U = T,
63  typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
64  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
65  {
66  return mpi.to_long();
67  }
68 
69  // Unchecked conversion from mp_integer when T is unsigned
70  template <typename U = T,
71  typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
72  static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
73  {
74  return mpi.to_ulong();
75  }
76 
77 public:
78  // Conversion from mp_integer to integral type T
80  {
81 #if !defined(_MSC_VER) || _MSC_VER >= 1900
82  static_assert(
83  std::numeric_limits<T>::max() <=
84  std::numeric_limits<decltype(get_val(mpi))>::max() &&
85  std::numeric_limits<T>::min() >=
86  std::numeric_limits<decltype(get_val(mpi))>::min(),
87  "Numeric cast only works for types smaller than long long");
88 #else
89  // std::numeric_limits<> methods are not declared constexpr in old versions
90  // of VS
92  std::numeric_limits<T>::max() <=
93  std::numeric_limits<decltype(get_val(mpi))>::max() &&
94  std::numeric_limits<T>::min() >=
95  std::numeric_limits<decltype(get_val(mpi))>::min());
96 #endif
97  if(
98  mpi <= std::numeric_limits<T>::max() &&
99  mpi >= std::numeric_limits<T>::min())
100  // to_long converts to long long which is the largest signed numeric type
101  return static_cast<T>(get_val(mpi));
102  else
103  return {};
104  }
105 
106  // Conversion from expression
107  optionalt<T> operator()(const exprt &expr) const
108  {
109  if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
110  return numeric_castt<T>{}(*mpi_opt);
111  else
112  return {};
113  }
114 };
115 
121 template <typename Target>
123 {
124  return numeric_castt<Target>{}(arg);
125 }
126 
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, "Bad conversion");
138  return *maybe;
139 }
140 
147 template <typename Target>
148 Target numeric_cast_v(const exprt &arg)
149 {
150  const auto maybe = numeric_castt<Target>{}(arg);
151  INVARIANT(maybe, "Bad conversion");
152  return *maybe;
153 }
154 
155 // PRECONDITION(false) in case of unsupported type
156 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
157 
158 // ceil(log2(size))
159 std::size_t address_bits(const mp_integer &size);
160 
161 mp_integer power(const mp_integer &base, const mp_integer &exponent);
162 
163 void mp_min(mp_integer &a, const mp_integer &b);
164 void mp_max(mp_integer &a, const mp_integer &b);
165 
166 #endif // CPROVER_UTIL_ARITH_TOOLS_H
The type of an expression.
Definition: type.h:22
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 with fail with message "Bad conversion" if...
Definition: arith_tools.h:134
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
Definition: arith_tools.h:64
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:94
Numerical cast provides a unified way of converting from one numerical type to another.
Definition: arith_tools.h:38
void mp_min(mp_integer &a, const mp_integer &b)
STL namespace.
A constant literal expression.
Definition: std_expr.h:4422
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
Convert expression to mp_integer.
Definition: arith_tools.h:44
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:72
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:122
API to expression classes.
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
optionalt< mp_integer > operator()(const exprt &expr) const
Definition: arith_tools.h:46
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
#define DEPRECATED(msg)
Definition: deprecate.h:23
Base class for all expressions.
Definition: expr.h:42
constant_exprt from_integer(const mp_integer &int_value, const typet &type)