-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy patharith_tools.h
180 lines (151 loc) · 5.18 KB
/
arith_tools.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
/*******************************************************************\
Module:
Author: Daniel Kroening, [email protected]
\*******************************************************************/
#ifndef CPROVER_UTIL_ARITH_TOOLS_H
#define CPROVER_UTIL_ARITH_TOOLS_H
#include "invariant.h"
#include "mp_arith.h"
#include "std_expr.h"
#include <limits>
class typet;
/// Convert a constant expression \p expr to an arbitrary-precision integer.
/// \param expr: Source expression
/// \param [out] int_value: Integer value (only modified if conversion succeeds)
/// \return False if, and only if, the conversion was successful.
bool to_integer(const constant_exprt &expr, mp_integer &int_value);
/// Numerical cast provides a unified way of converting from one numerical type
/// to another.
/// Generic case doesn't exist, this has to be specialized for different types.
template <typename Target, typename = void>
struct numeric_castt final
{
};
/// Convert expression to mp_integer
template <>
struct numeric_castt<mp_integer> final
{
std::optional<mp_integer> operator()(const exprt &expr) const
{
if(!expr.is_constant())
return {};
else
return operator()(to_constant_expr(expr));
}
std::optional<mp_integer> operator()(const constant_exprt &expr) const
{
mp_integer out;
if(to_integer(expr, out))
return {};
else
return out;
}
};
/// Convert mp_integer or expr to any integral type
template <typename T>
struct numeric_castt<T,
typename std::enable_if<std::is_integral<T>::value>::type>
{
private:
// Unchecked conversion from mp_integer when T is signed
template <typename U = T,
typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
{
return mpi.to_long();
}
// Unchecked conversion from mp_integer when T is unsigned
template <typename U = T,
typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
{
return mpi.to_ulong();
}
public:
// Conversion from mp_integer to integral type T
std::optional<T> operator()(const mp_integer &mpi) const
{
static_assert(
std::numeric_limits<T>::max() <=
std::numeric_limits<decltype(get_val(mpi))>::max() &&
std::numeric_limits<T>::min() >=
std::numeric_limits<decltype(get_val(mpi))>::min(),
"Numeric cast only works for types smaller than long long");
if(
mpi <= std::numeric_limits<T>::max() &&
mpi >= std::numeric_limits<T>::min())
// to_long converts to long long which is the largest signed numeric type
return static_cast<T>(get_val(mpi));
else
return std::nullopt;
}
// Conversion from expression
std::optional<T> operator()(const exprt &expr) const
{
if(expr.is_constant())
return numeric_castt<T>{}(to_constant_expr(expr));
else
return std::nullopt;
}
// Conversion from expression
std::optional<T> operator()(const constant_exprt &expr) const
{
if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
return numeric_castt<T>{}(*mpi_opt);
else
return std::nullopt;
}
};
/// Converts an expression to any integral type
/// \tparam Target: type to convert to
/// \param arg: expression to convert
/// \return optional integer of type Target if conversion is possible, empty
/// optional otherwise.
template <typename Target>
std::optional<Target> numeric_cast(const exprt &arg)
{
return numeric_castt<Target>{}(arg);
}
/// Convert an mp_integer to integral type Target
/// An invariant will fail if the conversion is not possible.
/// \tparam Target: type to convert to
/// \param arg: mp_integer
/// \return value of type Target
template <typename Target>
Target numeric_cast_v(const mp_integer &arg)
{
const auto maybe = numeric_castt<Target>{}(arg);
INVARIANT(maybe, "mp_integer should be convertible to target integral type");
return *maybe;
}
/// Convert an expression to integral type Target
/// An invariant will fail if the conversion is not possible.
/// \tparam Target: type to convert to
/// \param arg: constant expression
/// \return value of type Target
template <typename Target>
Target numeric_cast_v(const constant_exprt &arg)
{
const auto maybe = numeric_castt<Target>{}(arg);
INVARIANT_WITH_DIAGNOSTICS(
maybe,
"expression should be convertible to target integral type",
irep_pretty_diagnosticst(arg));
return *maybe;
}
// PRECONDITION(false) in case of unsupported type
constant_exprt from_integer(const mp_integer &int_value, const typet &type);
// ceil(log2(size))
std::size_t address_bits(const mp_integer &size);
mp_integer power(const mp_integer &base, const mp_integer &exponent);
void mp_min(mp_integer &a, const mp_integer &b);
void mp_max(mp_integer &a, const mp_integer &b);
bool get_bvrep_bit(
const irep_idt &src,
std::size_t width,
std::size_t bit_index);
irep_idt
make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
irep_idt integer2bvrep(const mp_integer &, std::size_t width);
mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
#endif // CPROVER_UTIL_ARITH_TOOLS_H