cprover
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 "boolbv.h"
10
11#include <util/invariant.h>
12
14{
15 if(expr.id()==ID_overflow_plus ||
16 expr.id()==ID_overflow_minus)
17 {
18 const auto &overflow_expr = to_binary_expr(expr);
19
20 const bvt &bv0 = convert_bv(overflow_expr.lhs());
21 const bvt &bv1 = convert_bv(overflow_expr.rhs());
22
23 if(bv0.size()!=bv1.size())
24 return SUB::convert_rest(expr);
25
27 overflow_expr.lhs().type().id() == ID_signedbv
30
31 return expr.id()==ID_overflow_minus?
32 bv_utils.overflow_sub(bv0, bv1, rep):
33 bv_utils.overflow_add(bv0, bv1, rep);
34 }
35 else if(expr.id()==ID_overflow_mult)
36 {
37 const auto &overflow_expr = to_binary_expr(expr);
38
39 if(
40 overflow_expr.lhs().type().id() != ID_unsignedbv &&
41 overflow_expr.lhs().type().id() != ID_signedbv)
42 return SUB::convert_rest(expr);
43
44 bvt bv0 = convert_bv(overflow_expr.lhs());
45 bvt bv1 = convert_bv(overflow_expr.rhs(), bv0.size());
46
48 overflow_expr.lhs().type().id() == ID_signedbv
51
53 overflow_expr.lhs().type() == overflow_expr.rhs().type(),
54 "operands of overflow_mult expression shall have same type");
55
56 std::size_t old_size=bv0.size();
57 std::size_t new_size=old_size*2;
58
59 // sign/zero extension
60 bv0=bv_utils.extension(bv0, new_size, rep);
61 bv1=bv_utils.extension(bv1, new_size, rep);
62
63 bvt result=bv_utils.multiplier(bv0, bv1, rep);
64
66 {
67 bvt bv_overflow;
68 bv_overflow.reserve(old_size);
69
70 // get top result bits
71 for(std::size_t i=old_size; i<result.size(); i++)
72 bv_overflow.push_back(result[i]);
73
74 return prop.lor(bv_overflow);
75 }
76 else
77 {
78 bvt bv_overflow;
79 bv_overflow.reserve(old_size);
80
81 // get top result bits, plus one more
82 DATA_INVARIANT(old_size!=0, "zero-size operand");
83 for(std::size_t i=old_size-1; i<result.size(); i++)
84 bv_overflow.push_back(result[i]);
85
86 // these need to be either all 1's or all 0's
87 literalt all_one=prop.land(bv_overflow);
88 literalt all_zero=!prop.lor(bv_overflow);
89 return !prop.lor(all_one, all_zero);
90 }
91 }
92 else if(expr.id() == ID_overflow_shl)
93 {
94 const auto &overflow_expr = to_binary_expr(expr);
95
96 const bvt &bv0 = convert_bv(overflow_expr.lhs());
97 const bvt &bv1 = convert_bv(overflow_expr.rhs());
98
99 std::size_t old_size = bv0.size();
100 std::size_t new_size = old_size * 2;
101
103 overflow_expr.lhs().type().id() == ID_signedbv
106
107 bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
108
109 bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);
110
111 // a negative shift is undefined; yet this isn't an overflow
112 literalt neg_shift = overflow_expr.lhs().type().id() == ID_unsignedbv
113 ? const_literal(false)
114 : bv1.back(); // sign bit
115
116 // an undefined shift of a non-zero value always results in overflow; the
117 // use of unsigned comparision is safe here as we cover the signed negative
118 // case via neg_shift
119 literalt undef =
121 bv1,
122 ID_gt,
123 bv_utils.build_constant(old_size, bv1.size()),
125
126 literalt overflow;
127
129 {
130 // get top result bits
131 result.erase(result.begin(), result.begin() + old_size);
132
133 // one of the top bits is non-zero
134 overflow=prop.lor(result);
135 }
136 else
137 {
138 // get top result bits plus sign bit
139 DATA_INVARIANT(old_size != 0, "zero-size operand");
140 result.erase(result.begin(), result.begin() + old_size - 1);
141
142 // the sign bit has changed
143 literalt sign_change=!prop.lequal(bv0.back(), result.front());
144
145 // these need to be either all 1's or all 0's
146 literalt all_one=prop.land(result);
147 literalt all_zero=!prop.lor(result);
148
149 overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero));
150 }
151
152 // a negative shift isn't an overflow; else check the conditions built
153 // above
154 return
155 prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
156 }
157 else if(expr.id()==ID_overflow_unary_minus)
158 {
159 const auto &overflow_expr = to_unary_expr(expr);
160
161 const bvt &bv = convert_bv(overflow_expr.op());
162
163 return bv_utils.overflow_negate(bv);
164 }
165
166 return SUB::convert_rest(expr);
167}
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:40
bv_utilst bv_utils
Definition: boolbv.h:114
virtual literalt convert_overflow(const exprt &expr)
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:363
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:387
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:477
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:543
representationt
Definition: bv_utils.h:28
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:806
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:105
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1279
Base class for all expressions.
Definition: expr.h:54
const irep_idt & id() const
Definition: irep.h:396
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328