CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 "std_expr.h"
16
17#include <limits>
18
19class typet;
20
26
30template <typename Target, typename = void>
31struct numeric_castt final
32{
33};
34
36template <>
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
58template <typename T>
60 typename std::enable_if<std::is_integral<T>::value>::type>
61{
62private:
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
79public:
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
123template <typename Target>
124std::optional<Target> numeric_cast(const exprt &arg)
125{
126 return numeric_castt<Target>{}(arg);
127}
128
134template <typename Target>
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
147template <typename Target>
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
160
161// ceil(log2(size))
162std::size_t address_bits(const mp_integer &size);
163
164mp_integer power(const mp_integer &base, const mp_integer &exponent);
165
166void mp_min(mp_integer &a, const mp_integer &b);
167void mp_max(mp_integer &a, const mp_integer &b);
168
169bool get_bvrep_bit(
170 const irep_idt &src,
171 std::size_t width,
172 std::size_t bit_index);
173
175make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
176
177irep_idt integer2bvrep(const mp_integer &, std::size_t width);
178mp_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...
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
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.
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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
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
STL namespace.
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:3172
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
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
Definition arith_tools.h:74
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