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/arith_tools.h>
17 #include <util/bitvector_expr.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
23 
24 #include "util.h"
25 
26 /*
27  * This code is copied wholesale from analyses/goto_check.cpp.
28  */
29 
30 
32 {
34  program.instructions.begin(),
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_nonconst());
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  if(t->has_condition())
69  add_overflow_checks(t, t->get_condition(), added);
70 
71  checked.insert(t->location_number);
72 }
73 
76 {
78  add_overflow_checks(t, ignore);
79 }
80 
83  const exprt &expr,
85 {
86  exprt overflow;
87  overflow_expr(expr, overflow);
88 
89  if(overflow!=false_exprt())
90  {
91  accumulate_overflow(t, overflow, added);
92  }
93 }
94 
96  const exprt &expr,
97  expr_sett &cases)
98 {
99  forall_operands(it, expr)
100  {
101  overflow_expr(*it, cases);
102  }
103 
104  const typet &type = expr.type();
105 
106  if(expr.id()==ID_typecast)
107  {
108  const auto &typecast_expr = to_typecast_expr(expr);
109 
110  if(typecast_expr.op().id() == ID_constant)
111  return;
112 
113  const typet &old_type = typecast_expr.op().type();
114  const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
115  const std::size_t old_width = to_bitvector_type(old_type).get_width();
116 
117  if(type.id()==ID_signedbv)
118  {
119  if(old_type.id()==ID_signedbv)
120  {
121  // signed -> signed
122  if(new_width >= old_width)
123  {
124  // Always safe.
125  return;
126  }
127 
128  cases.insert(binary_relation_exprt(
129  typecast_expr.op(),
130  ID_gt,
131  from_integer(power(2, new_width - 1) - 1, old_type)));
132 
133  cases.insert(binary_relation_exprt(
134  typecast_expr.op(),
135  ID_lt,
136  from_integer(-power(2, new_width - 1), old_type)));
137  }
138  else if(old_type.id()==ID_unsignedbv)
139  {
140  // unsigned -> signed
141  if(new_width >= old_width + 1)
142  {
143  // Always safe.
144  return;
145  }
146 
147  cases.insert(binary_relation_exprt(
148  typecast_expr.op(),
149  ID_gt,
150  from_integer(power(2, new_width - 1) - 1, old_type)));
151  }
152  }
153  else if(type.id()==ID_unsignedbv)
154  {
155  if(old_type.id()==ID_signedbv)
156  {
157  // signed -> unsigned
158  cases.insert(binary_relation_exprt(
159  typecast_expr.op(), ID_lt, from_integer(0, old_type)));
160  if(new_width < old_width - 1)
161  {
162  // Need to check for overflow as well as signedness.
163  cases.insert(binary_relation_exprt(
164  typecast_expr.op(),
165  ID_gt,
166  from_integer(power(2, new_width - 1) - 1, old_type)));
167  }
168  }
169  else if(old_type.id()==ID_unsignedbv)
170  {
171  // unsigned -> unsigned
172  if(new_width>=old_width)
173  {
174  // Always safe.
175  return;
176  }
177 
178  cases.insert(binary_relation_exprt(
179  typecast_expr.op(),
180  ID_gt,
181  from_integer(power(2, new_width - 1) - 1, old_type)));
182  }
183  }
184  }
185  else if(expr.id()==ID_div)
186  {
187  const auto &div_expr = to_div_expr(expr);
188 
189  // Undefined for signed INT_MIN / -1
190  if(type.id()==ID_signedbv)
191  {
192  equal_exprt int_min_eq(
193  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
194  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
195 
196  cases.insert(and_exprt(int_min_eq, minus_one_eq));
197  }
198  }
199  else if(expr.id()==ID_unary_minus)
200  {
201  if(type.id()==ID_signedbv)
202  {
203  // Overflow on unary- can only happen with the smallest
204  // representable number.
205  cases.insert(equal_exprt(
206  to_unary_minus_expr(expr).op(),
207  to_signedbv_type(type).smallest_expr()));
208  }
209  }
210  else if(expr.id()==ID_plus ||
211  expr.id()==ID_minus ||
212  expr.id()==ID_mult)
213  {
214  // A generic arithmetic operation.
215  // The overflow checks are binary.
216  for(std::size_t i = 1; i < expr.operands().size(); i++)
217  {
218  exprt tmp;
219 
220  if(i == 1)
221  {
222  tmp = to_multi_ary_expr(expr).op0();
223  }
224  else
225  {
226  tmp = expr;
227  tmp.operands().resize(i);
228  }
229 
230  binary_overflow_exprt overflow{tmp, expr.id(), expr.operands()[i]};
231 
232  fix_types(overflow);
233 
234  cases.insert(overflow);
235  }
236  }
237 }
238 
240 {
241  expr_sett cases;
242 
243  overflow_expr(expr, cases);
244 
245  overflow=false_exprt();
246 
247  for(expr_sett::iterator it=cases.begin();
248  it!=cases.end();
249  ++it)
250  {
251  if(overflow==false_exprt())
252  {
253  overflow=*it;
254  }
255  else
256  {
257  overflow=or_exprt(overflow, *it);
258  }
259  }
260 }
261 
263 {
264  typet &t1=overflow.op0().type();
265  typet &t2=overflow.op1().type();
266  const typet &t=join_types(t1, t2);
267 
268  if(t1!=t)
269  {
270  overflow.op0()=typecast_exprt(overflow.op0(), t);
271  }
272 
273  if(t2!=t)
274  {
275  overflow.op1()=typecast_exprt(overflow.op1(), t);
276  }
277 }
278 
281  const exprt &expr,
283 {
285  t,
287  assignment->swap(*t);
288 
289  added.push_back(assignment);
290 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
overflow_instrumenter.h
Loop Acceleration.
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1029
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
and_exprt
Boolean AND.
Definition: std_expr.h:1834
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
equal_exprt
Equality.
Definition: std_expr.h:1139
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1008
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:565
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:623
overflow_instrumentert::accumulate_overflow
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
Definition: overflow_instrumenter.cpp:279
or_exprt
Boolean OR.
Definition: std_expr.h:1942
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
binary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
Definition: bitvector_expr.h:687
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:713
overflow_instrumentert::fix_types
void fix_types(binary_exprt &overflow)
Definition: overflow_instrumenter.cpp:262
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
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:407
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
std_code.h
goto_program.h
Concrete Goto Program.
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
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
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
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:569
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:383
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
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:639
exprt::operands
operandst & operands()
Definition: expr.h:96
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:760
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:815
overflow_instrumentert::program
goto_programt & program
Definition: overflow_instrumenter.h:56
std_expr.h
API to expression classes.
util.h
Loop Acceleration.
overflow_instrumentert::overflow_expr
void overflow_expr(const exprt &expr, expr_sett &cases)
Definition: overflow_instrumenter.cpp:95
overflow_instrumentert::add_overflow_checks
void add_overflow_checks()
Definition: overflow_instrumenter.cpp:31
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:103