cprover
Loading...
Searching...
No Matches
overflow_instrumenter.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
13
14#include <iostream>
15
16#include <util/arith_tools.h>
17#include <util/bitvector_expr.h>
18#include <util/std_code.h>
19
21
22#include "util.h"
23
24/*
25 * This code is copied wholesale from analyses/goto_check.cpp.
26 */
27
28
30{
32 program.instructions.begin(),
34
36 checked.clear();
37
39 {
41 }
42}
43
47{
48 if(checked.find(t->location_number)!=checked.end())
49 {
50 return;
51 }
52
53 if(t->is_assign())
54 {
55 code_assignt &assignment = to_code_assign(t->code_nonconst());
56
57 if(assignment.lhs()==overflow_var)
58 {
59 return;
60 }
61
62 add_overflow_checks(t, assignment.lhs(), added);
63 add_overflow_checks(t, assignment.rhs(), added);
64 }
65
66 if(t->has_condition())
67 add_overflow_checks(t, t->get_condition(), added);
68
69 checked.insert(t->location_number);
70}
71
74{
76 add_overflow_checks(t, ignore);
77}
78
81 const exprt &expr,
83{
84 exprt overflow;
85 overflow_expr(expr, overflow);
86
87 if(overflow!=false_exprt())
88 {
89 accumulate_overflow(t, overflow, added);
90 }
91}
92
94 const exprt &expr,
95 expr_sett &cases)
96{
97 forall_operands(it, expr)
98 {
99 overflow_expr(*it, cases);
100 }
101
102 const typet &type = expr.type();
103
104 if(expr.id()==ID_typecast)
105 {
106 const auto &typecast_expr = to_typecast_expr(expr);
107
108 if(typecast_expr.op().id() == ID_constant)
109 return;
110
111 const typet &old_type = typecast_expr.op().type();
112 const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
113 const std::size_t old_width = to_bitvector_type(old_type).get_width();
114
115 if(type.id()==ID_signedbv)
116 {
117 if(old_type.id()==ID_signedbv)
118 {
119 // signed -> signed
120 if(new_width >= old_width)
121 {
122 // Always safe.
123 return;
124 }
125
126 cases.insert(binary_relation_exprt(
127 typecast_expr.op(),
128 ID_gt,
129 from_integer(power(2, new_width - 1) - 1, old_type)));
130
131 cases.insert(binary_relation_exprt(
132 typecast_expr.op(),
133 ID_lt,
134 from_integer(-power(2, new_width - 1), old_type)));
135 }
136 else if(old_type.id()==ID_unsignedbv)
137 {
138 // unsigned -> signed
139 if(new_width >= old_width + 1)
140 {
141 // Always safe.
142 return;
143 }
144
145 cases.insert(binary_relation_exprt(
146 typecast_expr.op(),
147 ID_gt,
148 from_integer(power(2, new_width - 1) - 1, old_type)));
149 }
150 }
151 else if(type.id()==ID_unsignedbv)
152 {
153 if(old_type.id()==ID_signedbv)
154 {
155 // signed -> unsigned
156 cases.insert(binary_relation_exprt(
157 typecast_expr.op(), ID_lt, from_integer(0, old_type)));
158 if(new_width < old_width - 1)
159 {
160 // Need to check for overflow as well as signedness.
161 cases.insert(binary_relation_exprt(
162 typecast_expr.op(),
163 ID_gt,
164 from_integer(power(2, new_width - 1) - 1, old_type)));
165 }
166 }
167 else if(old_type.id()==ID_unsignedbv)
168 {
169 // unsigned -> unsigned
170 if(new_width>=old_width)
171 {
172 // Always safe.
173 return;
174 }
175
176 cases.insert(binary_relation_exprt(
177 typecast_expr.op(),
178 ID_gt,
179 from_integer(power(2, new_width - 1) - 1, old_type)));
180 }
181 }
182 }
183 else if(expr.id()==ID_div)
184 {
185 const auto &div_expr = to_div_expr(expr);
186
187 // Undefined for signed INT_MIN / -1
188 if(type.id()==ID_signedbv)
189 {
190 equal_exprt int_min_eq(
191 div_expr.dividend(), to_signedbv_type(type).smallest_expr());
192 equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
193
194 cases.insert(and_exprt(int_min_eq, minus_one_eq));
195 }
196 }
197 else if(expr.id()==ID_unary_minus)
198 {
199 if(type.id()==ID_signedbv)
200 {
201 // Overflow on unary- can only happen with the smallest
202 // representable number.
203 cases.insert(equal_exprt(
204 to_unary_minus_expr(expr).op(),
205 to_signedbv_type(type).smallest_expr()));
206 }
207 }
208 else if(expr.id()==ID_plus ||
209 expr.id()==ID_minus ||
210 expr.id()==ID_mult)
211 {
212 // A generic arithmetic operation.
213 // The overflow checks are binary.
214 for(std::size_t i = 1; i < expr.operands().size(); i++)
215 {
216 exprt tmp;
217
218 if(i == 1)
219 {
220 tmp = to_multi_ary_expr(expr).op0();
221 }
222 else
223 {
224 tmp = expr;
225 tmp.operands().resize(i);
226 }
227
228 binary_overflow_exprt overflow{tmp, expr.id(), expr.operands()[i]};
229
230 fix_types(overflow);
231
232 cases.insert(overflow);
233 }
234 }
235}
236
238{
239 expr_sett cases;
240
241 overflow_expr(expr, cases);
242
243 overflow=false_exprt();
244
245 for(expr_sett::iterator it=cases.begin();
246 it!=cases.end();
247 ++it)
248 {
249 if(overflow==false_exprt())
250 {
251 overflow=*it;
252 }
253 else
254 {
255 overflow=or_exprt(overflow, *it);
256 }
257 }
258}
259
261{
262 typet &t1=overflow.op0().type();
263 typet &t2=overflow.op1().type();
264 const typet &t=join_types(t1, t2);
265
266 if(t1!=t)
267 {
268 overflow.op0()=typecast_exprt(overflow.op0(), t);
269 }
270
271 if(t2!=t)
272 {
273 overflow.op1()=typecast_exprt(overflow.op1(), t);
274 }
275}
276
279 const exprt &expr,
281{
283 t,
285 assignment->swap(*t);
286
287 added.push_back(assignment);
288}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Boolean AND.
Definition: std_expr.h:1974
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:864
A codet representing an assignment in the program.
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::iterator targett
Definition: goto_program.h:592
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:755
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
std::list< targett > targetst
Definition: goto_program.h:594
const irep_idt & id() const
Definition: irep.h:396
exprt & op0()
Definition: std_expr.h:844
Boolean OR.
Definition: std_expr.h:2082
std::set< unsigned > checked
void fix_types(binary_exprt &overflow)
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
void overflow_expr(const exprt &expr, expr_sett &cases)
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
std::unordered_set< exprt, irep_hash > expr_sett
#define forall_operands(it, expr)
Definition: expr.h:18
const code_assignt & to_code_assign(const codet &code)
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
Loop Acceleration.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition: util.cpp:70
Loop Acceleration.