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