cprover
Loading...
Searching...
No Matches
boolbv_overflow.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include <util/arith_tools.h>
10#include <util/bitvector_expr.h>
12#include <util/invariant.h>
13
14#include "boolbv.h"
15
17 propt &prop,
18 const bvt &bv0,
19 const bvt &bv1,
21{
22 bv_utilst bv_utils{prop};
23
24 std::size_t old_size = bv0.size();
25 std::size_t new_size = old_size * 2;
26
27 // sign/zero extension
28 const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep);
29 const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep);
30
31 bvt result_extended = bv_utils.multiplier(bv0_extended, bv1_extended, rep);
32 bvt bv{result_extended.begin(), result_extended.begin() + old_size};
33 bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()};
34
36 {
37 bv.push_back(prop.lor(bv_overflow));
38 }
39 else
40 {
41 // get top result bits, plus one more
42 bv_overflow.push_back(bv.back());
43
44 // these need to be either all 1's or all 0's
45 literalt all_one = prop.land(bv_overflow);
46 literalt all_zero = !prop.lor(bv_overflow);
47 bv.push_back(!prop.lor(all_one, all_zero));
48 }
49
50 return bv;
51}
52
54 propt &prop,
55 const bvt &bv0,
56 const bvt &bv1,
59{
60 bv_utilst bv_utils{prop};
61
62 std::size_t old_size = bv0.size();
63 std::size_t new_size = old_size * 2;
64
65 bvt result_extended = bv_utils.shift(
66 bv_utils.extension(bv0, new_size, rep0),
68 bv1);
69 bvt bv{result_extended.begin(), result_extended.begin() + old_size};
70 bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()};
71
72 // a negative shift is undefined; yet this isn't an overflow
74 ? const_literal(false)
75 : bv_utils.sign_bit(bv1);
76
77 // an undefined shift of a non-zero value always results in overflow
78 std::size_t cmp_width = std::max(bv1.size(), address_bits(old_size) + 1);
79 literalt undef = bv_utils.rel(
80 bv_utils.extension(bv1, cmp_width, rep1),
81 ID_gt,
82 bv_utils.build_constant(old_size, cmp_width),
83 rep1);
84
86 {
87 // one of the top bits is non-zero
88 bv.push_back(prop.lor(bv_overflow));
89 }
90 else
91 {
92 // get top result bits, plus one more
93 bv_overflow.push_back(bv.back());
94
95 // the sign bit has changed
96 literalt sign_change =
97 !prop.lequal(bv_utils.sign_bit(bv0), bv_utils.sign_bit(bv));
98
99 // these need to be either all 1's or all 0's
100 literalt all_one = prop.land(bv_overflow);
101 literalt all_zero = !prop.lor(bv_overflow);
102
103 bv.push_back(prop.lor(sign_change, !prop.lor(all_one, all_zero)));
104 }
105
106 // a negative shift isn't an overflow; else check the conditions built
107 // above
108 bv.back() =
109 prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), bv.back()));
110
111 return bv;
112}
113
115{
116 const bvt &bv0 = convert_bv(expr.lhs());
117 const bvt &bv1 = convert_bv(
118 expr.rhs(),
120 ? optionalt<std::size_t>{bv0.size()}
121 : nullopt);
122
127
128 if(
129 const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
130 {
131 if(bv0.size() != bv1.size())
132 return SUB::convert_rest(expr);
133
134 return bv_utils.overflow_add(bv0, bv1, rep);
135 }
136 if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
137 {
138 if(bv0.size() != bv1.size())
139 return SUB::convert_rest(expr);
140
141 return bv_utils.overflow_sub(bv0, bv1, rep);
142 }
143 else if(
144 const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
145 {
146 if(
149 {
150 return SUB::convert_rest(expr);
151 }
152
154 mult_overflow->lhs().type() == mult_overflow->rhs().type(),
155 "operands of overflow_mult expression shall have same type");
156
157 DATA_INVARIANT(!bv0.empty(), "zero-sized operand");
158
159 return mult_overflow_result(prop, bv0, bv1, rep).back();
160 }
161 else if(
162 const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
163 {
164 DATA_INVARIANT(!bv0.empty(), "zero-sized operand");
165
166 return shl_overflow_result(
167 prop,
168 bv0,
169 bv1,
170 rep,
174 .back();
175 }
176
177 return SUB::convert_rest(expr);
178}
179
181{
182 if(
183 const auto unary_minus_overflow =
185 {
186 const bvt &bv = convert_bv(unary_minus_overflow->op());
187
188 return bv_utils.overflow_negate(bv);
189 }
190
191 return SUB::convert_rest(expr);
192}
193
195{
196 const typet &type = expr.type();
197 const std::size_t width = boolbv_width(type);
198
199 if(expr.id() == ID_overflow_result_unary_minus)
200 {
201 const bvt op_bv = convert_bv(expr.op0());
202 bvt bv = bv_utils.negate(op_bv);
203 bv.push_back(bv_utils.overflow_negate(op_bv));
204 CHECK_RETURN(bv.size() == width);
205 return bv;
206 }
207 else if(expr.operands().size() != 2)
208 return conversion_failed(expr);
209
210 const bvt &bv0 = convert_bv(expr.op0());
211 const bvt &bv1 = convert_bv(expr.op1());
212 CHECK_RETURN(!bv0.empty() && !bv1.empty());
213
218
219 if(expr.id() == ID_overflow_result_plus)
220 {
221 CHECK_RETURN(bv0.size() == bv1.size());
222
224 {
225 // An overflow occurs if the signs of the two operands are the same
226 // and the sign of the sum is the opposite.
227 bvt bv = bv_utils.add(bv0, bv1);
228
229 literalt old_sign = bv_utils.sign_bit(bv0);
230 literalt sign_the_same = prop.lequal(old_sign, bv_utils.sign_bit(bv1));
231 literalt new_sign = bv_utils.sign_bit(bv);
232 bv.push_back(prop.land(sign_the_same, prop.lxor(new_sign, old_sign)));
233
234 CHECK_RETURN(bv.size() == width);
235 return bv;
236 }
237 else
238 {
239 // overflow is simply carry-out
240 bvt bv;
241 bv.reserve(width);
242 literalt carry = const_literal(false);
243
244 for(std::size_t i = 0; i < bv0.size(); i++)
245 bv.push_back(bv_utils.full_adder(bv0[i], bv1[i], carry, carry));
246
247 bv.push_back(carry);
248
249 CHECK_RETURN(bv.size() == width);
250 return bv;
251 }
252 }
253 else if(expr.id() == ID_overflow_result_minus)
254 {
255 CHECK_RETURN(bv0.size() == bv1.size());
256
258 {
259 bvt bv1_neg = bv_utils.negate(bv1);
260 bvt bv = bv_utils.add(bv0, bv1_neg);
261
262 // We special-case x-INT_MIN, which is >=0 if
263 // x is negative, always representable, and
264 // thus not an overflow.
265 literalt op1_is_int_min = bv_utils.is_int_min(bv1);
266 literalt op0_is_negative = bv_utils.sign_bit(bv0);
267
268 literalt old_sign = bv_utils.sign_bit(bv0);
269 literalt sign_the_same =
270 prop.lequal(old_sign, bv_utils.sign_bit(bv1_neg));
271 literalt new_sign = bv_utils.sign_bit(bv);
272 bv.push_back(prop.lselect(
273 op1_is_int_min,
274 !op0_is_negative,
275 prop.land(sign_the_same, prop.lxor(new_sign, old_sign))));
276
277 CHECK_RETURN(bv.size() == width);
278 return bv;
279 }
281 {
282 // overflow is simply _negated_ carry-out
283 bvt bv;
284 bv.reserve(width);
285 literalt carry = const_literal(true);
286
287 for(std::size_t i = 0; i < bv0.size(); i++)
288 bv.push_back(bv_utils.full_adder(bv0[i], !bv1[i], carry, carry));
289
290 bv.push_back(!carry);
291
292 CHECK_RETURN(bv.size() == width);
293 return bv;
294 }
295 else
297 }
298 else if(expr.id() == ID_overflow_result_mult)
299 {
300 CHECK_RETURN(bv0.size() == bv1.size());
301
302 bvt bv = mult_overflow_result(prop, bv0, bv1, rep);
303
304 CHECK_RETURN(bv.size() == width);
305 return bv;
306 }
307 else if(expr.id() == ID_overflow_result_shl)
308 {
310 prop,
311 bv0,
312 bv1,
313 rep,
317
318 CHECK_RETURN(bv.size() == width);
319 return bv;
320 }
321
322 return conversion_failed(expr);
323}
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
API to expression classes for bitvectors.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
Pre-defined bitvector types.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
static bvt shl_overflow_result(propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep0, bv_utilst::representationt rep1)
static bvt mult_overflow_result(propt &prop, const bvt &bv0, const bvt &bv1, bv_utilst::representationt rep)
exprt & lhs()
Definition std_expr.h:613
exprt & rhs()
Definition std_expr.h:623
exprt & op1()
Definition expr.h:128
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:38
virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr)
bv_utilst bv_utils
Definition boolbv.h:114
virtual bvt convert_overflow_result(const overflow_result_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:82
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
literalt is_int_min(const bvt &op)
Definition bv_utils.h:150
static literalt sign_bit(const bvt &op)
Definition bv_utils.h:139
bvt add(const bvt &op0, const bvt &op1)
Definition bv_utils.h:67
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:426
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.cpp:450
literalt overflow_negate(const bvt &op)
Definition bv_utils.cpp:602
representationt
Definition bv_utils.h:29
literalt full_adder(const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
Definition bv_utils.cpp:138
bvt negate(const bvt &op)
Definition bv_utils.cpp:588
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:396
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
virtual literalt convert_rest(const exprt &expr)
TO_BE_DOCUMENTED.
Definition prop.h:25
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lxor(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
The type of an expression, extends irept.
Definition type.h:29
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
nonstd::optional< T > optionalt
Definition optional.h:35
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534