cprover
simplify_expr_pointer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
10 
11 #include <cassert>
12 
13 #include "c_types.h"
14 #include "expr.h"
15 #include "namespace.h"
16 #include "std_expr.h"
17 #include "pointer_offset_size.h"
18 #include "arith_tools.h"
19 #include "config.h"
20 #include "expr_util.h"
21 #include "threeval.h"
22 #include "prefix.h"
23 #include "pointer_predicates.h"
24 
26  const exprt &expr,
27  mp_integer &address)
28 {
29  if(expr.id()==ID_dereference &&
30  expr.operands().size()==1)
31  {
32  if(expr.op0().id()==ID_typecast &&
33  expr.op0().operands().size()==1 &&
34  expr.op0().op0().is_constant() &&
35  !to_integer(expr.op0().op0(), address))
36  return true;
37 
38  if(expr.op0().is_constant())
39  {
40  if(to_constant_expr(expr.op0()).get_value()==ID_NULL &&
41  config.ansi_c.NULL_is_zero) // NULL
42  {
43  address=0;
44  return true;
45  }
46  else if(!to_integer(expr.op0(), address))
47  return true;
48  }
49  }
50 
51  return false;
52 }
53 
55 {
56  if(expr.id()==ID_index)
57  {
58  if(expr.operands().size()==2)
59  {
60  bool result=true;
61  if(!simplify_address_of_arg(expr.op0()))
62  result=false;
63  if(!simplify_rec(expr.op1()))
64  result=false;
65 
66  // rewrite (*(type *)int) [index] by
67  // pushing the index inside
68 
69  mp_integer address;
70  if(is_dereference_integer_object(expr.op0(), address))
71  {
72  // push index into address
73 
74  mp_integer step_size, index;
75 
76  step_size=pointer_offset_size(expr.type(), ns);
77 
78  if(!to_integer(expr.op1(), index) &&
79  step_size!=-1)
80  {
82  pointer_type.subtype()=expr.type();
83  typecast_exprt typecast_expr(
84  from_integer(step_size*index+address, index_type()), pointer_type);
85  exprt new_expr=dereference_exprt(typecast_expr, expr.type());
86  expr=new_expr;
87  result=true;
88  }
89  }
90 
91  return result;
92  }
93  }
94  else if(expr.id()==ID_member)
95  {
96  if(expr.operands().size()==1)
97  {
98  bool result=true;
99  if(!simplify_address_of_arg(expr.op0()))
100  result=false;
101 
102  const typet &op_type=ns.follow(expr.op0().type());
103 
104  if(op_type.id()==ID_struct)
105  {
106  // rewrite NULL -> member by
107  // pushing the member inside
108 
109  mp_integer address;
110  if(is_dereference_integer_object(expr.op0(), address))
111  {
112  const struct_typet &struct_type=to_struct_type(op_type);
113  const irep_idt &member=to_member_expr(expr).get_component_name();
114  mp_integer offset=member_offset(struct_type, member, ns);
115  if(offset!=-1)
116  {
118  pointer_type.subtype()=expr.type();
119  typecast_exprt typecast_expr(
120  from_integer(address+offset, index_type()), pointer_type);
121  exprt new_expr=dereference_exprt(typecast_expr, expr.type());
122  expr=new_expr;
123  result=true;
124  }
125  }
126  }
127 
128  return result;
129  }
130  }
131  else if(expr.id()==ID_dereference)
132  {
133  if(expr.operands().size()==1)
134  return simplify_rec(expr.op0());
135  }
136  else if(expr.id()==ID_if)
137  {
138  if(expr.operands().size()==3)
139  {
140  bool result=true;
141  if(!simplify_rec(expr.op0()))
142  result=false;
143  if(!simplify_address_of_arg(expr.op1()))
144  result=false;
145  if(!simplify_address_of_arg(expr.op2()))
146  result=false;
147 
148  // op0 is a constant?
149  if(expr.op0().is_true())
150  {
151  result=false;
152  exprt tmp;
153  tmp.swap(expr.op1());
154  expr.swap(tmp);
155  }
156  else if(expr.op0().is_false())
157  {
158  result=false;
159  exprt tmp;
160  tmp.swap(expr.op2());
161  expr.swap(tmp);
162  }
163 
164  return result;
165  }
166  }
167 
168  return true;
169 }
170 
172 {
173  if(expr.operands().size()!=1)
174  return true;
175 
176  if(ns.follow(expr.type()).id()!=ID_pointer)
177  return true;
178 
179  exprt &object=expr.op0();
180 
181  bool result=simplify_address_of_arg(object);
182 
183  if(object.id()==ID_index)
184  {
185  index_exprt &index_expr=to_index_expr(object);
186 
187  if(!index_expr.index().is_zero())
188  {
189  // we normalize &a[i] to (&a[0])+i
190  exprt offset;
191  offset.swap(index_expr.op1());
192  index_expr.op1()=from_integer(0, offset.type());
193 
194  exprt addition(ID_plus, expr.type());
195  addition.move_to_operands(expr, offset);
196 
197  expr.swap(addition);
198  return false;
199  }
200  }
201  else if(object.id()==ID_dereference)
202  {
203  // simplify &*p to p
204  assert(object.operands().size()==1);
205  exprt tmp=object.op0();
206  expr=tmp;
207  return false;
208  }
209 
210  return result;
211 }
212 
214 {
215  if(expr.operands().size()!=1)
216  return true;
217 
218  exprt &ptr=expr.op0();
219 
220  if(ptr.id()==ID_if && ptr.operands().size()==3)
221  {
222  if_exprt if_expr=lift_if(expr, 0);
225  simplify_if(if_expr);
226  expr.swap(if_expr);
227 
228  return false;
229  }
230 
231  if(ptr.type().id()!=ID_pointer)
232  return true;
233 
234  if(ptr.id()==ID_address_of)
235  {
236  if(ptr.operands().size()!=1)
237  return true;
238 
239  mp_integer offset=compute_pointer_offset(ptr.op0(), ns);
240 
241  if(offset!=-1)
242  {
243  expr=from_integer(offset, expr.type());
244  return false;
245  }
246  }
247  else if(ptr.id()==ID_typecast) // pointer typecast
248  {
249  if(ptr.operands().size()!=1)
250  return true;
251 
252  const typet &op_type=ns.follow(ptr.op0().type());
253 
254  if(op_type.id()==ID_pointer)
255  {
256  // Cast from pointer to pointer.
257  // This just passes through, remove typecast.
258  exprt tmp=ptr.op0();
259  ptr=tmp;
260 
261  // recursive call
262  simplify_node(expr);
263  return false;
264  }
265  else if(op_type.id()==ID_signedbv ||
266  op_type.id()==ID_unsignedbv)
267  {
268  // Cast from integer to pointer, say (int *)x.
269 
270  if(ptr.op0().is_constant())
271  {
272  // (T *)0x1234 -> 0x1234
273  exprt tmp=ptr.op0();
274  tmp.make_typecast(expr.type());
275  simplify_node(tmp);
276  expr.swap(tmp);
277  return false;
278  }
279  else
280  {
281  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
282  // which is re-written to 'a'.
283 
284  typet type=ns.follow(expr.type());
285  exprt tmp=ptr.op0();
286  if(tmp.id()==ID_plus && tmp.operands().size()==2)
287  {
288  if(tmp.op0().id()==ID_typecast &&
289  tmp.op0().operands().size()==1 &&
290  tmp.op0().op0().id()==ID_address_of)
291  {
292  expr=tmp.op1();
293  if(type!=expr.type())
294  expr.make_typecast(type);
295 
296  simplify_node(expr);
297  return false;
298  }
299  else if(tmp.op1().id()==ID_typecast &&
300  tmp.op1().operands().size()==1 &&
301  tmp.op1().op0().id()==ID_address_of)
302  {
303  expr=tmp.op0();
304  if(type!=expr.type())
305  expr.make_typecast(type);
306 
307  simplify_node(expr);
308  return false;
309  }
310  }
311  }
312  }
313  }
314  else if(ptr.id()==ID_plus) // pointer arithmetic
315  {
316  exprt::operandst ptr_expr;
317  exprt::operandst int_expr;
318 
319  for(const auto &op : ptr.operands())
320  {
321  if(op.type().id()==ID_pointer)
322  ptr_expr.push_back(op);
323  else if(!op.is_zero())
324  {
325  exprt tmp=op;
326  if(tmp.type()!=expr.type())
327  {
328  tmp.make_typecast(expr.type());
329  simplify_node(tmp);
330  }
331 
332  int_expr.push_back(tmp);
333  }
334  }
335 
336  if(ptr_expr.size()!=1 || int_expr.empty())
337  return true;
338 
339  typet pointer_sub_type=ptr_expr.front().type().subtype();
340  if(pointer_sub_type.id()==ID_empty)
341  pointer_sub_type=char_type();
342 
343  mp_integer element_size=
344  pointer_offset_size(pointer_sub_type, ns);
345 
346  if(element_size<0)
347  return true;
348 
349  // this might change the type of the pointer!
350  exprt pointer_offset_expr=pointer_offset(ptr_expr.front());
351  simplify_node(pointer_offset_expr);
352 
353  exprt sum;
354 
355  if(int_expr.size()==1)
356  sum=int_expr.front();
357  else
358  {
359  sum=exprt(ID_plus, expr.type());
360  sum.operands()=int_expr;
361  }
362 
363  simplify_node(sum);
364 
365  exprt size_expr=
366  from_integer(element_size, expr.type());
367 
368  binary_exprt product(sum, ID_mult, size_expr, expr.type());
369 
370  simplify_node(product);
371 
372  expr=binary_exprt(pointer_offset_expr, ID_plus, product, expr.type());
373 
374  simplify_node(expr);
375 
376  return false;
377  }
378  else if(ptr.id()==ID_constant &&
379  ptr.get(ID_value)==ID_NULL)
380  {
381  expr=from_integer(0, expr.type());
382 
383  simplify_node(expr);
384 
385  return false;
386  }
387 
388  return true;
389 }
390 
392 {
393  assert(expr.type().id()==ID_bool);
394  assert(expr.operands().size()==2);
395  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
396 
397  exprt tmp0=expr.op0();
398  if(tmp0.id()==ID_typecast)
399  tmp0=expr.op0().op0();
400  if(tmp0.op0().id()==ID_index &&
401  to_index_expr(tmp0.op0()).index().is_zero())
402  tmp0=address_of_exprt(to_index_expr(tmp0.op0()).array());
403  exprt tmp1=expr.op1();
404  if(tmp1.id()==ID_typecast)
405  tmp1=expr.op1().op0();
406  if(tmp1.op0().id()==ID_index &&
407  to_index_expr(tmp1.op0()).index().is_zero())
408  tmp1=address_of_exprt(to_index_expr(tmp1.op0()).array());
409  assert(tmp0.id()==ID_address_of);
410  assert(tmp1.id()==ID_address_of);
411 
412  if(tmp0.operands().size()!=1)
413  return true;
414  if(tmp1.operands().size()!=1)
415  return true;
416 
417  if(tmp0.op0().id()==ID_symbol &&
418  tmp1.op0().id()==ID_symbol)
419  {
420  bool equal=
421  tmp0.op0().get(ID_identifier)==
422  tmp1.op0().get(ID_identifier);
423 
424  expr.make_bool(expr.id()==ID_equal?equal:!equal);
425 
426  return false;
427  }
428 
429  return true;
430 }
431 
433 {
434  assert(expr.type().id()==ID_bool);
435  assert(expr.operands().size()==2);
436  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
437 
438  forall_operands(it, expr)
439  {
440  assert(it->id()==ID_pointer_object);
441  assert(it->operands().size()==1);
442  const exprt &op=it->op0();
443 
444  if(op.id()==ID_address_of)
445  {
446  if(op.operands().size()!=1 ||
447  (op.op0().id()!=ID_symbol &&
448  op.op0().id()!=ID_dynamic_object &&
449  op.op0().id()!=ID_string_constant))
450  return true;
451  }
452  else if(op.id()!=ID_constant ||
453  op.get(ID_value)!=ID_NULL)
454  return true;
455  }
456 
457  bool equal=expr.op0().op0()==expr.op1().op0();
458 
459  expr.make_bool(expr.id()==ID_equal?equal:!equal);
460 
461  return false;
462 }
463 
465 {
466  if(expr.operands().size()!=1)
467  return true;
468 
469  exprt &op=expr.op0();
470 
471  bool result=simplify_object(op);
472 
473  if(op.id()==ID_if)
474  {
475  const if_exprt &if_expr=to_if_expr(op);
476  exprt cond=if_expr.cond();
477 
478  exprt p_o_false=expr;
479  p_o_false.op0()=if_expr.false_case();
480 
481  expr.op0()=if_expr.true_case();
482 
483  expr=if_exprt(cond, expr, p_o_false, expr.type());
484  simplify_rec(expr);
485 
486  return false;
487  }
488 
489  return result;
490 }
491 
493 {
494  if(expr.operands().size()!=1)
495  return true;
496 
497  exprt &op=expr.op0();
498 
499  if(op.id()==ID_if && op.operands().size()==3)
500  {
501  if_exprt if_expr=lift_if(expr, 0);
504  simplify_if(if_expr);
505  expr.swap(if_expr);
506 
507  return false;
508  }
509 
510  bool result=true;
511 
512  if(!simplify_object(op))
513  result=false;
514 
515  // NULL is not dynamic
516  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
517  {
518  expr=false_exprt();
519  return false;
520  }
521 
522  // &something depends on the something
523  if(op.id()==ID_address_of && op.operands().size()==1)
524  {
525  if(op.op0().id()==ID_symbol)
526  {
527  const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
528 
529  // this is for the benefit of symex
530  expr.make_bool(has_prefix(id2string(identifier), "symex_dynamic::"));
531  return false;
532  }
533  else if(op.op0().id()==ID_string_constant)
534  {
535  expr=false_exprt();
536  return false;
537  }
538  else if(op.op0().id()==ID_array)
539  {
540  expr=false_exprt();
541  return false;
542  }
543  }
544 
545  return result;
546 }
547 
549 {
550  if(expr.operands().size()!=1)
551  return true;
552 
553  exprt &op=expr.op0();
554 
555  bool result=true;
556 
557  if(!simplify_object(op))
558  result=false;
559 
560  // NULL is not invalid
561  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
562  {
563  expr=false_exprt();
564  return false;
565  }
566 
567  // &anything is not invalid
568  if(op.id()==ID_address_of)
569  {
570  expr=false_exprt();
571  return false;
572  }
573 
574  return result;
575 }
576 
578 {
579  if(a==b)
580  return tvt(true);
581 
582  if(a.id()==ID_address_of && b.id()==ID_address_of &&
583  a.operands().size()==1 && b.operands().size()==1)
584  return objects_equal_address_of(a.op0(), b.op0());
585 
586  if(a.id()==ID_constant && b.id()==ID_constant &&
587  a.get(ID_value)==ID_NULL && b.get(ID_value)==ID_NULL)
588  return tvt(true);
589 
590  if(a.id()==ID_constant && b.id()==ID_address_of &&
591  a.get(ID_value)==ID_NULL)
592  return tvt(false);
593 
594  if(b.id()==ID_constant && a.id()==ID_address_of &&
595  b.get(ID_value)==ID_NULL)
596  return tvt(false);
597 
598  return tvt::unknown();
599 }
600 
602 {
603  if(a==b)
604  return tvt(true);
605 
606  if(a.id()==ID_symbol && b.id()==ID_symbol)
607  {
608  if(a.get(ID_identifier)==b.get(ID_identifier))
609  return tvt(true);
610  }
611  else if(a.id()==ID_index && b.id()==ID_index)
612  {
613  if(a.operands().size()==2 && b.operands().size()==2)
614  return objects_equal_address_of(a.op0(), b.op0());
615  }
616  else if(a.id()==ID_member && b.id()==ID_member)
617  {
618  if(a.operands().size()==1 && b.operands().size()==1)
619  return objects_equal_address_of(a.op0(), b.op0());
620  }
621 
622  return tvt::unknown();
623 }
624 
626 {
627  if(expr.operands().size()!=1)
628  return true;
629 
630  exprt &op=expr.op0();
631 
632  bool result=true;
633 
634  if(!simplify_object(op))
635  result=false;
636 
637  if(op.id()==ID_address_of && op.operands().size()==1)
638  {
639  if(op.op0().id()==ID_symbol)
640  {
641  // just get the type
642  const typet &type=ns.follow(op.op0().type());
643 
644  exprt size=size_of_expr(type, ns);
645 
646  if(size.is_not_nil())
647  {
648  typet type=expr.type();
649 
650  if(size.type()!=type)
651  {
652  size.make_typecast(type);
653  simplify_node(size);
654  }
655 
656  expr=size;
657  return false;
658  }
659  }
660  else if(op.op0().id()==ID_string_constant)
661  {
662  typet type=expr.type();
663  expr=from_integer(op.op0().get(ID_value).size()+1, type);
664  return false;
665  }
666  }
667 
668  return result;
669 }
670 
672 {
673  if(expr.operands().size()!=1)
674  return true;
675 
676  // we expand the definition
677  exprt def=good_pointer_def(expr.op0(), ns);
678 
679  // recursive call
680  simplify_node(def);
681 
682  expr.swap(def);
683 
684  return false;
685 }
The type of an expression.
Definition: type.h:20
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
bool simplify_pointer_object(exprt &expr)
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Deprecated expression utility functions.
bool simplify_dynamic_object(exprt &expr)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
static tvt unknown()
Definition: threeval.h:33
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
bool is_false() const
Definition: expr.cpp:140
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
bool simplify_inequality_pointer_object(exprt &expr)
bool NULL_is_zero
Definition: config.h:86
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
bool simplify_address_of_arg(exprt &expr)
void make_bool(bool value)
Definition: expr.cpp:147
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
bool simplify_good_pointer(exprt &expr)
bool simplify_object(exprt &expr)
A generic base class for binary expressions.
Definition: std_expr.h:471
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The pointer type.
Definition: std_types.h:1343
Operator to dereference a pointer.
Definition: std_expr.h:2701
bool simplify_address_of(exprt &expr)
API to expression classes.
bool simplify_pointer_offset(exprt &expr)
Definition: threeval.h:19
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
#define forall_operands(it, expr)
Definition: expr.h:17
size_t size() const
Definition: dstring.h:77
bitvector_typet index_type()
Definition: c_types.cpp:15
Operator to return the address of an object.
Definition: std_expr.h:2593
exprt & false_case()
Definition: std_expr.h:2815
Various predicates over pointers in programs.
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
static tvt objects_equal(const exprt &a, const exprt &b)
bool simplify_rec(exprt &expr)
exprt & index()
Definition: std_expr.h:1208
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:144
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
exprt pointer_offset(const exprt &pointer)
const namespacet & ns
irep_idt get_component_name() const
Definition: std_expr.h:3249
void swap(irept &irep)
Definition: irep.h:231
bool is_zero() const
Definition: expr.cpp:236
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
bool simplify_inequality_address_of(exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
bool simplify_invalid_pointer(exprt &expr)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool simplify_object_size(exprt &expr)
void make_typecast(const typet &_type)
Definition: expr.cpp:90
bitvector_typet char_type()
Definition: c_types.cpp:113
array index operator
Definition: std_expr.h:1170