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(),
35 
37  checked.clear();
38 
40  {
42  }
43 }
44 
48 {
49  if(checked.find(t->location_number)!=checked.end())
50  {
51  return;
52  }
53 
54  if(t->is_assign())
55  {
56  code_assignt &assignment=to_code_assign(t->code);
57 
58  if(assignment.lhs()==overflow_var)
59  {
60  return;
61  }
62 
63  add_overflow_checks(t, assignment.lhs(), added);
64  add_overflow_checks(t, assignment.rhs(), added);
65  }
66 
67  if(t->has_condition())
68  add_overflow_checks(t, t->get_condition(), 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 = expr.type();
104 
105  if(expr.id()==ID_typecast)
106  {
107  const auto &typecast_expr = to_typecast_expr(expr);
108 
109  if(typecast_expr.op().id() == ID_constant)
110  return;
111 
112  const typet &old_type = typecast_expr.op().type();
113  const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
114  const std::size_t old_width = to_bitvector_type(old_type).get_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(binary_relation_exprt(
128  typecast_expr.op(),
129  ID_gt,
130  from_integer(power(2, new_width - 1) - 1, old_type)));
131 
132  cases.insert(binary_relation_exprt(
133  typecast_expr.op(),
134  ID_lt,
135  from_integer(-power(2, new_width - 1), old_type)));
136  }
137  else if(old_type.id()==ID_unsignedbv)
138  {
139  // unsigned -> signed
140  if(new_width >= old_width + 1)
141  {
142  // Always safe.
143  return;
144  }
145 
146  cases.insert(binary_relation_exprt(
147  typecast_expr.op(),
148  ID_gt,
149  from_integer(power(2, new_width - 1) - 1, old_type)));
150  }
151  }
152  else if(type.id()==ID_unsignedbv)
153  {
154  if(old_type.id()==ID_signedbv)
155  {
156  // signed -> unsigned
157  cases.insert(binary_relation_exprt(
158  typecast_expr.op(), ID_lt, from_integer(0, old_type)));
159  if(new_width < old_width - 1)
160  {
161  // Need to check for overflow as well as signedness.
162  cases.insert(binary_relation_exprt(
163  typecast_expr.op(),
164  ID_gt,
165  from_integer(power(2, new_width - 1) - 1, old_type)));
166  }
167  }
168  else if(old_type.id()==ID_unsignedbv)
169  {
170  // unsigned -> unsigned
171  if(new_width>=old_width)
172  {
173  // Always safe.
174  return;
175  }
176 
177  cases.insert(binary_relation_exprt(
178  typecast_expr.op(),
179  ID_gt,
180  from_integer(power(2, new_width - 1) - 1, old_type)));
181  }
182  }
183  }
184  else if(expr.id()==ID_div)
185  {
186  const auto &div_expr = to_div_expr(expr);
187 
188  // Undefined for signed INT_MIN / -1
189  if(type.id()==ID_signedbv)
190  {
191  equal_exprt int_min_eq(
192  div_expr.dividend(), to_signedbv_type(type).smallest_expr());
193  equal_exprt minus_one_eq(div_expr.divisor(), from_integer(-1, type));
194 
195  cases.insert(and_exprt(int_min_eq, minus_one_eq));
196  }
197  }
198  else if(expr.id()==ID_unary_minus)
199  {
200  if(type.id()==ID_signedbv)
201  {
202  // Overflow on unary- can only happen with the smallest
203  // representable number.
204  cases.insert(equal_exprt(
205  to_unary_minus_expr(expr).op(),
206  to_signedbv_type(type).smallest_expr()));
207  }
208  }
209  else if(expr.id()==ID_plus ||
210  expr.id()==ID_minus ||
211  expr.id()==ID_mult)
212  {
213  // A generic arithmetic operation.
214  multi_ary_exprt overflow(
215  "overflow-" + expr.id_string(), expr.operands(), bool_typet());
216 
217  if(expr.operands().size()>=3)
218  {
219  // The overflow checks are binary.
220  for(std::size_t i=1; i<expr.operands().size(); i++)
221  {
222  exprt tmp;
223 
224  if(i==1)
225  {
226  tmp = to_multi_ary_expr(expr).op0();
227  }
228  else
229  {
230  tmp=expr;
231  tmp.operands().resize(i);
232  }
233 
234  overflow.operands().resize(2);
235  overflow.op0()=tmp;
236  overflow.op1()=expr.operands()[i];
237 
238  fix_types(to_binary_expr(overflow));
239 
240  cases.insert(overflow);
241  }
242  }
243  else
244  {
245  fix_types(to_binary_expr(overflow));
246  cases.insert(overflow);
247  }
248  }
249 }
250 
252 {
253  expr_sett cases;
254 
255  overflow_expr(expr, cases);
256 
257  overflow=false_exprt();
258 
259  for(expr_sett::iterator it=cases.begin();
260  it!=cases.end();
261  ++it)
262  {
263  if(overflow==false_exprt())
264  {
265  overflow=*it;
266  }
267  else
268  {
269  overflow=or_exprt(overflow, *it);
270  }
271  }
272 }
273 
275 {
276  typet &t1=overflow.op0().type();
277  typet &t2=overflow.op1().type();
278  const typet &t=join_types(t1, t2);
279 
280  if(t1!=t)
281  {
282  overflow.op0()=typecast_exprt(overflow.op0(), t);
283  }
284 
285  if(t2!=t)
286  {
287  overflow.op1()=typecast_exprt(overflow.op1(), t);
288  }
289 }
290 
293  const exprt &expr,
295 {
297  t,
299  assignment->swap(*t);
300 
301  added.push_back(assignment);
302 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
overflow_instrumenter.h
Loop Acceleration.
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
and_exprt
Boolean AND.
Definition: std_expr.h:2137
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
bool_typet
The Boolean type.
Definition: std_types.h:37
equal_exprt
Equality.
Definition: std_expr.h:1190
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:1024
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:581
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:639
overflow_instrumentert::accumulate_overflow
void accumulate_overflow(goto_programt::targett t, const exprt &expr, goto_programt::targetst &added)
Definition: overflow_instrumenter.cpp:291
or_exprt
Boolean OR.
Definition: std_expr.h:2245
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:729
overflow_instrumentert::fix_types
void fix_types(binary_exprt &overflow)
Definition: overflow_instrumenter.cpp:274
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
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:408
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:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
std_code.h
goto_program.h
Concrete Goto Program.
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:1041
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:585
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:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
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:655
exprt::operands
operandst & operands()
Definition: expr.h:95
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
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:811
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
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:866
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: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:579
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089