Skip to content

Commit 946b6e2

Browse files
romainbrenguierromainbrenguier
committed
Extend numeric_cast for constant expressions
This requires moving some declarations to arith_tools, because overload needs to be declared in the same struct. This also adds a numeric_cast_v function which returns a value instead of an optional but an invariant can fail.
1 parent 20b5366 commit 946b6e2

File tree

2 files changed

+125
-67
lines changed

2 files changed

+125
-67
lines changed

‎src/util/arith_tools.h

+125
Original file line numberDiff line numberDiff line change
@@ -11,21 +11,146 @@ Author: Daniel Kroening, [email protected]
1111
#define CPROVER_UTIL_ARITH_TOOLS_H
1212

1313
#include "mp_arith.h"
14+
#include "optional.h"
15+
#include "invariant.h"
1416

1517
class exprt;
1618
class constant_exprt;
1719
class typet;
1820

1921
// this one will go away
2022
// returns 'true' on error
23+
/// \deprecated: use the constant_exprt version instead
2124
bool to_integer(const exprt &expr, mp_integer &int_value);
2225

2326
// returns 'true' on error
27+
/// \deprecated: use numeric_cast<mp_integer> instead
2428
bool to_integer(const constant_exprt &expr, mp_integer &int_value);
2529

2630
// returns 'true' on error
2731
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);
2832

33+
/// Numerical cast provides a unified way of converting from one numerical type
34+
/// to another.
35+
/// Generic case doesn't exist, this has to be specialized for different types.
36+
template <typename Target, typename = void>
37+
struct numeric_castt final
38+
{
39+
};
40+
41+
/// Convert expression to mp_integer
42+
template <>
43+
struct numeric_castt<mp_integer> final
44+
{
45+
optionalt<mp_integer> operator()(const exprt &expr) const
46+
{
47+
mp_integer out;
48+
if(to_integer(expr, out))
49+
return {};
50+
return out;
51+
}
52+
};
53+
54+
/// Convert mp_integer or expr to any integral type
55+
template <typename T>
56+
struct numeric_castt<T,
57+
typename std::enable_if<std::is_integral<T>::value>::type>
58+
{
59+
private:
60+
// Unchecked conversion from mp_integer when T is signed
61+
template <typename U = T,
62+
typename std::enable_if<std::is_signed<U>::value, int>::type = 0>
63+
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
64+
{
65+
return mpi.to_long();
66+
}
67+
68+
// Unchecked conversion from mp_integer when T is unsigned
69+
template <typename U = T,
70+
typename std::enable_if<!std::is_signed<U>::value, int>::type = 0>
71+
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
72+
{
73+
return mpi.to_ulong();
74+
}
75+
76+
public:
77+
// Conversion from mp_integer to integral type T
78+
optionalt<T> operator()(const mp_integer &mpi) const
79+
{
80+
#if !defined(_MSC_VER) || _MSC_VER >= 1900
81+
static_assert(
82+
std::numeric_limits<T>::max() <=
83+
std::numeric_limits<decltype(get_val(mpi))>::max() &&
84+
std::numeric_limits<T>::min() >=
85+
std::numeric_limits<decltype(get_val(mpi))>::min(),
86+
"Numeric cast only works for types smaller than long long");
87+
#else
88+
// std::numeric_limits<> methods are not declared constexpr in old versions
89+
// of VS
90+
PRECONDITION(
91+
std::numeric_limits<T>::max() <=
92+
std::numeric_limits<decltype(get_val(mpi))>::max() &&
93+
std::numeric_limits<T>::min() >=
94+
std::numeric_limits<decltype(get_val(mpi))>::min());
95+
#endif
96+
if(
97+
mpi <= std::numeric_limits<T>::max() &&
98+
mpi >= std::numeric_limits<T>::min())
99+
// to_long converts to long long which is the largest signed numeric type
100+
return static_cast<T>(get_val(mpi));
101+
else
102+
return {};
103+
}
104+
105+
// Conversion from expression
106+
optionalt<T> operator()(const exprt &expr) const
107+
{
108+
if(auto mpi_opt = numeric_castt<mp_integer>{}(expr))
109+
return numeric_castt<T>{}(*mpi_opt);
110+
else
111+
return {};
112+
}
113+
};
114+
115+
/// Converts an expression to any integral type
116+
/// \tparam Target: type to convert to
117+
/// \param arg: expression to convert
118+
/// \return optional integer of type Target if conversion is possible,
119+
/// empty optional otherwise.
120+
template <typename Target>
121+
optionalt<Target> numeric_cast(const exprt &arg)
122+
{
123+
return numeric_castt<Target>{}(arg);
124+
}
125+
126+
/// Convert an mp_integer to integral type Target
127+
/// An invariant with fail with message "Bad conversion" if conversion
128+
/// is not possible.
129+
/// \tparam Target: type to convert to
130+
/// \param arg: mp_integer
131+
/// \return value of type Target
132+
template <typename Target>
133+
Target numeric_cast_v(const mp_integer &arg)
134+
{
135+
const auto maybe = numeric_castt<Target>{}(arg);
136+
INVARIANT(maybe, "Bad conversion");
137+
return *maybe;
138+
}
139+
140+
/// Convert an expression to integral type Target
141+
/// An invariant with fail with message "Bad conversion" if conversion
142+
/// is not possible.
143+
/// \tparam Target: type to convert to
144+
/// \param arg: constant expression
145+
/// \return value of type Target
146+
template <typename Target>
147+
Target numeric_cast_v(const exprt &arg)
148+
{
149+
const auto maybe = numeric_castt<Target>{}(arg);
150+
INVARIANT(maybe, "Bad conversion");
151+
return *maybe;
152+
}
153+
29154
// PRECONDITION(false) in case of unsupported type
30155
constant_exprt from_integer(const mp_integer &int_value, const typet &type);
31156

‎src/util/mp_arith.h

-67
Original file line numberDiff line numberDiff line change
@@ -62,71 +62,4 @@ unsigned integer2unsigned(const mp_integer &);
6262

6363
const mp_integer mp_zero=string2integer("0");
6464

65-
/// Numerical cast provides a unified way of converting from one numerical type
66-
/// to another.
67-
/// Generic case doesn't exist, this has to be specialized for different types.
68-
template <typename T, typename = void>
69-
struct numeric_castt final
70-
{
71-
};
72-
73-
/// Convert mp_integer to any signed type
74-
/// \tparam T: type to convert to
75-
/// \param mpi: mp_integer to convert
76-
/// \return optional integer of type T if conversion is possible,
77-
/// empty optional otherwise.
78-
template <typename T>
79-
struct numeric_castt<T,
80-
typename std::enable_if<std::is_integral<T>::value &&
81-
std::is_signed<T>::value>::type>
82-
{
83-
static optionalt<T> numeric_cast(const mp_integer &mpi)
84-
{
85-
static_assert(
86-
std::numeric_limits<T>::max() <=
87-
std::numeric_limits<decltype(mpi.to_long())>::max() &&
88-
std::numeric_limits<T>::min() >=
89-
std::numeric_limits<decltype(mpi.to_long())>::min(),
90-
"Numeric cast only works for types smaller than long long");
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>(mpi.to_long())};
96-
else
97-
return {};
98-
}
99-
};
100-
101-
/// Convert mp_integer to any unsigned type
102-
/// \tparam T: type to convert to
103-
/// \param mpi: mp_integer to convert
104-
/// \return optional integer of type T if conversion is possible,
105-
/// empty optional otherwise.
106-
template <typename T>
107-
struct numeric_castt<T,
108-
typename std::enable_if<std::is_integral<T>::value &&
109-
!std::is_signed<T>::value>::type>
110-
{
111-
static optionalt<T> numeric_cast(const mp_integer &mpi)
112-
{
113-
static_assert(
114-
std::numeric_limits<T>::max() <=
115-
std::numeric_limits<decltype(mpi.to_ulong())>::max() &&
116-
std::numeric_limits<T>::min() >=
117-
std::numeric_limits<decltype(mpi.to_ulong())>::min(),
118-
"Numeric cast only works for types smaller than unsigned long long");
119-
if(mpi <= std::numeric_limits<T>::max() && mpi >= 0)
120-
return {static_cast<T>(mpi.to_ulong())};
121-
else
122-
return {};
123-
}
124-
};
125-
126-
template <typename T>
127-
optionalt<T> numeric_cast(const mp_integer &mpi)
128-
{
129-
return numeric_castt<T>::numeric_cast(mpi);
130-
}
131-
13265
#endif // CPROVER_UTIL_MP_ARITH_H

0 commit comments

Comments
 (0)