cprover
pointer_logic.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Logic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "pointer_logic.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/invariant.h>
20 #include <util/prefix.h>
21 #include <util/std_expr.h>
22 
24 {
25  if(expr.type().get_bool("#dynamic"))
26  return true;
27 
28  if(expr.id()==ID_symbol)
29  if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()),
30  "symex_dynamic::"))
31  return true;
32 
33  return false;
34 }
35 
36 void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const
37 {
38  o.clear();
39  std::size_t nr=0;
40 
42  it=objects.begin();
43  it!=objects.end();
44  it++, nr++)
45  if(is_dynamic_object(*it))
46  o.push_back(nr);
47 }
48 
49 std::size_t pointer_logict::add_object(const exprt &expr)
50 {
51  // remove any index/member
52 
53  if(expr.id()==ID_index)
54  {
55  assert(expr.operands().size()==2);
56  return add_object(expr.op0());
57  }
58  else if(expr.id()==ID_member)
59  {
60  assert(expr.operands().size()==1);
61  return add_object(expr.op0());
62  }
63 
64  return objects.number(expr);
65 }
66 
68  std::size_t object,
69  const pointer_typet &type) const
70 {
71  pointert pointer(object, 0);
72  return pointer_expr(pointer, type);
73 }
74 
76  const pointert &pointer,
77  const pointer_typet &type) const
78 {
79  if(pointer.object==null_object) // NULL?
80  {
81  if(pointer.offset==0)
82  {
83  constant_exprt result(type);
84  result.set_value(ID_NULL);
85  return result;
86  }
87  else
88  {
89  constant_exprt null(type);
90  null.set_value(ID_NULL);
91  return plus_exprt(null,
93  }
94  }
95  else if(pointer.object==invalid_object) // INVALID?
96  {
97  constant_exprt result(type);
98  result.set_value("INVALID");
99  return result;
100  }
101 
102  if(pointer.object>=objects.size())
103  {
104  constant_exprt result(type);
105  result.set_value("INVALID-"+std::to_string(pointer.object));
106  return result;
107  }
108 
109  const exprt &object_expr=objects[pointer.object];
110 
111  exprt deep_object=object_rec(pointer.offset, type, object_expr);
112 
113  return address_of_exprt(deep_object, type);
114 }
115 
117  const mp_integer &offset,
118  const typet &pointer_type,
119  const exprt &src) const
120 {
121  if(src.type().id()==ID_array)
122  {
123  mp_integer size=
125 
126  if(size<=0)
127  return src;
128 
129  mp_integer index=offset/size;
130  mp_integer rest=offset%size;
131  if(rest<0)
132  rest=-rest;
133 
134  index_exprt tmp(src.type().subtype());
135  tmp.index()=from_integer(index, typet(ID_integer));
136  tmp.array()=src;
137 
138  return object_rec(rest, pointer_type, tmp);
139  }
140  else if(src.type().id()==ID_struct)
141  {
142  const struct_typet::componentst &components=
143  to_struct_type(src.type()).components();
144 
145  if(offset<0)
146  return src;
147 
148  mp_integer current_offset=0;
149 
150  for(const auto &c : components)
151  {
152  assert(offset>=current_offset);
153 
154  const typet &subtype=c.type();
155 
156  mp_integer sub_size=pointer_offset_size(subtype, ns);
157  assert(sub_size>0);
158  mp_integer new_offset=current_offset+sub_size;
159 
160  if(new_offset>offset)
161  {
162  // found it
163  member_exprt tmp(src, c);
164 
165  return object_rec(
166  offset-current_offset, pointer_type, tmp);
167  }
168 
169  assert(new_offset<=offset);
170  current_offset=new_offset;
171  assert(current_offset<=offset);
172  }
173 
174  return src;
175  }
176  else if(src.type().id()==ID_union)
177  return src;
178 
179  return src;
180 }
181 
183 {
184  // add NULL
185  null_object=objects.number(exprt(ID_NULL));
186  assert(null_object==0);
187 
188  // add INVALID
189  invalid_object=objects.number(exprt("INVALID"));
190 }
191 
193 {
194 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
number_type number(const key_type &a)
Definition: numbering.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:72
size_type size() const
Definition: numbering.h:66
std::vector< componentt > componentst
Definition: std_types.h:243
typet & type()
Definition: expr.h:56
void get_dynamic_objects(std::vector< std::size_t > &objects) const
A constant literal expression.
Definition: std_expr.h:4424
const namespacet & ns
Definition: pointer_logic.h:75
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:4446
The pointer type.
Definition: std_types.h:1426
iterator begin()
Definition: numbering.h:85
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_dynamic_object(const exprt &expr) const
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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
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 pointer_expr(const pointert &pointer, const pointer_typet &type) const
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
Pointer Logic.
pointer_logict(const namespacet &_ns)
objectst objects
Definition: pointer_logic.h:27
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
iterator end()
Definition: numbering.h:98
Pointer Logic.
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t add_object(const exprt &expr)
std::size_t null_object
Definition: pointer_logic.h:76
exprt object_rec(const mp_integer &offset, const typet &pointer_type, const exprt &src) const
std::size_t invalid_object
Definition: pointer_logic.h:76
array index operator
Definition: std_expr.h:1462