cprover
Loading...
Searching...
No Matches
arith_tools.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <limits>
19
20class typet;
21
26bool to_integer(const constant_exprt &expr, mp_integer &int_value);
27
31template <typename Target, typename = void>
32struct numeric_castt final
33{
34};
35
37template <>
39{
41 {
42 if(expr.id() != ID_constant)
43 return {};
44 else
45 return operator()(to_constant_expr(expr));
46 }
47
49 {
50 mp_integer out;
51 if(to_integer(expr, out))
52 return {};
53 else
54 return out;
55 }
56};
57
59template <typename T>
61 typename std::enable_if<std::is_integral<T>::value>::type>
62{
63private:
64 // Unchecked conversion from mp_integer when T is signed
65 template <typename U = T,
66 typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
67 static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
68 {
69 return mpi.to_long();
70 }
71
72 // Unchecked conversion from mp_integer when T is unsigned
73 template <typename U = T,
74 typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
75 static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
76 {
77 return mpi.to_ulong();
78 }
79
80public:
81 // Conversion from mp_integer to integral type T
83 {
84 static_assert(
85 std::numeric_limits<T>::max() <=
86 std::numeric_limits<decltype(get_val(mpi))>::max() &&
87 std::numeric_limits<T>::min() >=
88 std::numeric_limits<decltype(get_val(mpi))>::min(),
89 "Numeric cast only works for types smaller than long long");
90
91 if(
92 mpi <= std::numeric_limits<T>::max() &&
93 mpi >= std::numeric_limits<T>::min())
94 // to_long converts to long long which is the largest signed numeric type
95 return static_cast<T>(get_val(mpi));
96 else
97 return {};
98 }
99
100 // Conversion from expression
101 optionalt<T> operator()(const exprt &expr) const
102 {
103 if(expr.id() == ID_constant)
104 return numeric_castt<T>{}(to_constant_expr(expr));
105 else
106 return {};
107 }
108
109 // Conversion from expression
111 {
112 if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
113 return numeric_castt<T>{}(*mpi_opt);
114 else
115 return {};
116 }
117};
118
124template <typename Target>
126{
127 return numeric_castt<Target>{}(arg);
128}
129
135template <typename Target>
136Target numeric_cast_v(const mp_integer &arg)
137{
138 const auto maybe = numeric_castt<Target>{}(arg);
139 INVARIANT(maybe, "mp_integer should be convertible to target integral type");
140 return *maybe;
141}
142
148template <typename Target>
150{
151 const auto maybe = numeric_castt<Target>{}(arg);
153 maybe,
154 "expression should be convertible to target integral type",
156 return *maybe;
157}
158
159// PRECONDITION(false) in case of unsupported type
160constant_exprt from_integer(const mp_integer &int_value, const typet &type);
161
162// ceil(log2(size))
163std::size_t address_bits(const mp_integer &size);
164
165mp_integer power(const mp_integer &base, const mp_integer &exponent);
166
167void mp_min(mp_integer &a, const mp_integer &b);
168void mp_max(mp_integer &a, const mp_integer &b);
169
170bool get_bvrep_bit(
171 const irep_idt &src,
172 std::size_t width,
173 std::size_t bit_index);
174
176make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
177
178irep_idt integer2bvrep(const mp_integer &, std::size_t width);
179mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
180
181#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)
Definition: arith_tools.cpp:99
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)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:125
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:136
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:19
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.
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:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const irep_idt & id() const
Definition: irep.h:396
The type of an expression, extends irept.
Definition: type.h:29
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12
#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:2840
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
Definition: arith_tools.h:67
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
Definition: arith_tools.h:75
optionalt< mp_integer > operator()(const constant_exprt &expr) const
Definition: arith_tools.h:48
optionalt< mp_integer > operator()(const exprt &expr) const
Definition: arith_tools.h:40
Numerical cast provides a unified way of converting from one numerical type to another.
Definition: arith_tools.h:33
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45