cprover
pointer_arithmetic.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 "pointer_arithmetic.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/std_expr.h>
13 
15 {
16  pointer.make_nil();
17  offset.make_nil();
18  read(src);
19 }
20 
22 {
23  if(src.id()==ID_plus)
24  {
25  forall_operands(it, src)
26  {
27  if(it->type().id()==ID_pointer)
28  read(*it);
29  else
30  add_to_offset(*it);
31  }
32  }
33  else if(src.id()==ID_minus)
34  {
35  auto const &minus_src = to_minus_expr(src);
36  read(minus_src.op0());
37  const unary_minus_exprt unary_minus(
38  minus_src.op1(), minus_src.op1().type());
39  add_to_offset(unary_minus);
40  }
41  else if(src.id()==ID_address_of)
42  {
43  auto const &address_of_src = to_address_of_expr(src);
44  if(address_of_src.op().id() == ID_index)
45  {
46  const index_exprt &index_expr = to_index_expr(address_of_src.op());
47 
48  if(index_expr.index().is_zero())
49  make_pointer(address_of_src);
50  else
51  {
52  add_to_offset(index_expr.index());
53  // produce &x[0] + i instead of &x[i]
54  auto new_address_of_src = address_of_src;
55  new_address_of_src.op().op1() =
56  from_integer(0, index_expr.index().type());
57  make_pointer(new_address_of_src);
58  }
59  }
60  else
61  make_pointer(address_of_src);
62  }
63  else
64  make_pointer(src);
65 }
66 
68 {
69  if(offset.is_nil())
70  offset=src;
71  else if(offset.id()==ID_plus)
73  else
74  {
75  exprt new_offset=plus_exprt(offset, src);
76 
77  if(new_offset.op1().type()!=offset.type())
78  new_offset.op1().make_typecast(offset.type());
79 
80  offset=new_offset;
81  }
82 }
83 
85 {
86  if(pointer.is_nil())
87  pointer=src;
88  else
89  add_to_offset(src);
90 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
arith_tools.h
pointer_arithmetic.h
irept::make_nil
void make_nil()
Definition: irep.h:315
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
pointer_arithmetict::pointer
exprt pointer
Definition: pointer_arithmetic.h:17
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1128
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
pointer_arithmetict::add_to_offset
void add_to_offset(const exprt &src)
Definition: pointer_arithmetic.cpp:67
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
exprt::op1
exprt & op1()
Definition: expr.h:87
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:469
pointer_arithmetict::offset
exprt offset
Definition: pointer_arithmetic.h:17
pointer_arithmetict::read
void read(const exprt &src)
Definition: pointer_arithmetic.cpp:21
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
pointer_arithmetict::make_pointer
void make_pointer(const exprt &src)
Definition: pointer_arithmetic.cpp:84
index_exprt
Array index operator.
Definition: std_expr.h:1595
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
std_expr.h
pointer_arithmetict::pointer_arithmetict
pointer_arithmetict(const exprt &src)
Definition: pointer_arithmetic.cpp:14