cprover
overflow_instrumenter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "overflow_instrumenter.h"
13 
14 #include <iostream>
15 
16 #include <util/std_expr.h>
17 #include <util/std_code.h>
18 #include <util/arith_tools.h>
19 #include <util/simplify_expr.h>
20 
22 
23 #include "util.h"
24 
25 /*
26  * This code is copied wholesale from analyses/goto_check.cpp.
27  */
28 
29 
31 {
33  program.instructions.begin());
34  init_overflow->make_assignment();
35  init_overflow->code=code_assignt(overflow_var, false_exprt());
36 
38  checked.clear();
39 
41  {
43  }
44 }
45 
49 {
50  if(checked.find(t->location_number)!=checked.end())
51  {
52  return;
53  }
54 
55  if(t->is_assign())
56  {
57  code_assignt &assignment=to_code_assign(t->code);
58 
59  if(assignment.lhs()==overflow_var)
60  {
61  return;
62  }
63 
64  add_overflow_checks(t, assignment.lhs(), added);
65  add_overflow_checks(t, assignment.rhs(), added);
66  }
67 
68  add_overflow_checks(t, t->guard, added);
69 
70  checked.insert(t->location_number);
71 }
72 
75 {
77  add_overflow_checks(t, ignore);
78 }
79 
82  const exprt &expr,
84 {
85  exprt overflow;
86  overflow_expr(expr, overflow);
87 
88  if(overflow!=false_exprt())
89  {
90  accumulate_overflow(t, overflow, added);
91  }
92 }
93 
95  const exprt &expr,
96  expr_sett &cases)
97 {
98  forall_operands(it, expr)
99  {
100  overflow_expr(*it, cases);
101  }
102 
103  const typet &type=ns.follow(expr.type());
104 
105  if(expr.id()==ID_typecast)
106  {
107  if(expr.op0().id()==ID_constant)
108  {
109  return;
110  }
111 
112  const typet &old_type=ns.follow(expr.op0().type());
113  const std::size_t new_width = expr.type().get_size_t(ID_width);
114  const std::size_t old_width = old_type.get_size_t(ID_width);
115 
116  if(type.id()==ID_signedbv)
117  {
118  if(old_type.id()==ID_signedbv)
119  {
120  // signed -> signed
121  if(new_width >= old_width)
122  {
123  // Always safe.
124  return;
125  }
126 
127  cases.insert(
128  binary_relation_exprt(expr.op0(), ID_gt,
129  from_integer(power(2, new_width - 1) - 1, old_type)));
130 
131  cases.insert(
132  binary_relation_exprt(expr.op0(), ID_lt,
133  from_integer(-power(2, new_width - 1), old_type)));
134  }
135  else if(old_type.id()==ID_unsignedbv)
136  {
137  // unsigned -> signed
138  if(new_width >= old_width + 1)
139  {
140  // Always safe.
141  return;
142  }
143 
144  cases.insert(
145  binary_relation_exprt(expr.op0(), ID_gt,
146  from_integer(power(2, new_width - 1) - 1, old_type)));
147  }
148  }
149  else if(type.id()==ID_unsignedbv)
150  {
151  if(old_type.id()==ID_signedbv)
152  {
153  // signed -> unsigned
154  cases.insert(
155  binary_relation_exprt(expr.op0(), ID_lt,
156  from_integer(0, old_type)));
157  if(new_width < old_width - 1)
158  {
159  // Need to check for overflow as well as signedness.
160  cases.insert(
161  binary_relation_exprt(expr.op0(), ID_gt,
162  from_integer(power(2, new_width - 1) - 1, old_type)));
163  }
164  }
165  else if(old_type.id()==ID_unsignedbv)
166  {
167  // unsigned -> unsigned
168  if(new_width>=old_width)
169  {
170  // Always safe.
171  return;
172  }
173 
174  cases.insert(
175  binary_relation_exprt(expr.op0(), ID_gt,
176  from_integer(power(2, new_width - 1) - 1, old_type)));
177  }
178  }
179  }
180  else if(expr.id()==ID_div)
181  {
182  // Undefined for signed INT_MIN / -1
183  if(type.id()==ID_signedbv)
184  {
185  equal_exprt int_min_eq(
186  expr.op0(), to_signedbv_type(type).smallest_expr());
187  equal_exprt minus_one_eq(expr.op1(), from_integer(-1, type));
188 
189  cases.insert(and_exprt(int_min_eq, minus_one_eq));
190  }
191  }
192  else if(expr.id()==ID_unary_minus)
193  {
194  if(type.id()==ID_signedbv)
195  {
196  // Overflow on unary- can only happen with the smallest
197  // representable number.
198  cases.insert(
199  equal_exprt(expr.op0(),
200  to_signedbv_type(type).smallest_expr()));
201  }
202  }
203  else if(expr.id()==ID_plus ||
204  expr.id()==ID_minus ||
205  expr.id()==ID_mult)
206  {
207  // A generic arithmetic operation.
208  exprt overflow("overflow-" + expr.id_string(), bool_typet());
209  overflow.operands()=expr.operands();
210 
211  if(expr.operands().size()>=3)
212  {
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=expr.op0();
221  }
222  else
223  {
224  tmp=expr;
225  tmp.operands().resize(i);
226  }
227 
228  overflow.operands().resize(2);
229  overflow.op0()=tmp;
230  overflow.op1()=expr.operands()[i];
231 
232  fix_types(overflow);
233 
234  cases.insert(overflow);
235  }
236  }
237  else
238  {
239  fix_types(overflow);
240  cases.insert(overflow);
241  }
242  }
243 }
244 
246 {
247  expr_sett cases;
248 
249  overflow_expr(expr, cases);
250 
251  overflow=false_exprt();
252 
253  for(expr_sett::iterator it=cases.begin();
254  it!=cases.end();
255  ++it)
256  {
257  if(overflow==false_exprt())
258  {
259  overflow=*it;
260  }
261  else
262  {
263  overflow=or_exprt(overflow, *it);
264  }
265  }
266 }
267 
269 {
270  typet &t1=overflow.op0().type();
271  typet &t2=overflow.op1().type();
272  const typet &t=join_types(t1, t2);
273 
274  if(t1!=t)
275  {
276  overflow.op0()=typecast_exprt(overflow.op0(), t);
277  }
278 
279  if(t2!=t)
280  {
281  overflow.op1()=typecast_exprt(overflow.op1(), t);
282  }
283 }
284 
287  const exprt &expr,
289 {
293  *assignment=a;
294  assignment->swap(*t);
295 
296  added.push_back(assignment);
297 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
overflow_instrumenter.h
overflow_instrumentert::ns
namespacet ns
Definition: overflow_instrumenter.h:60
arith_tools.h
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
and_exprt
Boolean AND.
Definition: std_expr.h:2409
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
bool_typet
The Boolean type.
Definition: std_types.h:28
equal_exprt
Equality.
Definition: std_expr.h:1484
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:416
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
overflow_instrumentert::accumulate_overflow
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
Definition: overflow_instrumenter.cpp:285
or_exprt
Boolean OR.
Definition: std_expr.h:2531
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:578
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
exprt::op1
exprt & op1()
Definition: expr.h:87
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
irept::id
const irep_idt & id() const
Definition: irep.h:259
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
std_code.h
goto_program.h
join_types
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
simplify_expr.h
overflow_instrumentert::overflow_var
const exprt & overflow_var
Definition: overflow_instrumenter.h:58
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
overflow_instrumentert::checked
std::set< unsigned > checked
Definition: overflow_instrumenter.h:61
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
overflow_instrumentert::fix_types
void fix_types(exprt &overflow)
Definition: overflow_instrumenter.cpp:268
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:218
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
exprt::operands
operandst & operands()
Definition: expr.h:78
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
overflow_instrumentert::program
goto_programt & program
Definition: overflow_instrumenter.h:56
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
util.h
overflow_instrumentert::overflow_expr
void overflow_expr(const exprt &expr, expr_sett &cases)
Definition: overflow_instrumenter.cpp:94
overflow_instrumentert::add_overflow_checks
void add_overflow_checks()
Definition: overflow_instrumenter.cpp:30
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414