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/std_expr.h>
19 #include <util/prefix.h>
21 
23 {
24  if(expr.type().get_bool("#dynamic"))
25  return true;
26 
27  if(expr.id()==ID_symbol)
28  if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()),
29  "symex_dynamic::"))
30  return true;
31 
32  return false;
33 }
34 
35 void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const
36 {
37  o.clear();
38  std::size_t nr=0;
39 
40  for(pointer_logict::objectst::const_iterator
41  it=objects.begin();
42  it!=objects.end();
43  it++, nr++)
44  if(is_dynamic_object(*it))
45  o.push_back(nr);
46 }
47 
48 std::size_t pointer_logict::add_object(const exprt &expr)
49 {
50  // remove any index/member
51 
52  if(expr.id()==ID_index)
53  {
54  assert(expr.operands().size()==2);
55  return add_object(expr.op0());
56  }
57  else if(expr.id()==ID_member)
58  {
59  assert(expr.operands().size()==1);
60  return add_object(expr.op0());
61  }
62 
63  return objects.number(expr);
64 }
65 
67  std::size_t object,
68  const typet &type) const
69 {
70  pointert pointer(object, 0);
71  return pointer_expr(pointer, type);
72 }
73 
75  const pointert &pointer,
76  const typet &type) const
77 {
78  if(pointer.object==null_object) // NULL?
79  {
80  if(pointer.offset==0)
81  {
82  constant_exprt result(type);
83  result.set_value(ID_NULL);
84  return result;
85  }
86  else
87  {
88  constant_exprt null(type);
89  null.set_value(ID_NULL);
90  return plus_exprt(null,
92  }
93  }
94  else if(pointer.object==invalid_object) // INVALID?
95  {
96  constant_exprt result(type);
97  result.set_value("INVALID");
98  return result;
99  }
100 
101  if(pointer.object>=objects.size())
102  {
103  constant_exprt result(type);
104  result.set_value("INVALID-"+std::to_string(pointer.object));
105  return result;
106  }
107 
108  const exprt &object_expr=objects[pointer.object];
109 
110  exprt deep_object=object_rec(pointer.offset, type, object_expr);
111 
112  exprt result;
113 
114  if(type.id()==ID_pointer)
115  result=exprt(ID_address_of, type);
116  else if(type.id()==ID_reference)
117  result=exprt("reference_to", type);
118  else
119  assert(0);
120 
121  result.copy_to_operands(deep_object);
122  return result;
123 }
124 
126  const mp_integer &offset,
127  const typet &pointer_type,
128  const exprt &src) const
129 {
130  if(src.type().id()==ID_array)
131  {
132  mp_integer size=
134 
135  if(size<=0)
136  return src;
137 
138  mp_integer index=offset/size;
139  mp_integer rest=offset%size;
140  if(rest<0)
141  rest=-rest;
142 
143  index_exprt tmp(src.type().subtype());
144  tmp.index()=from_integer(index, typet(ID_integer));
145  tmp.array()=src;
146 
147  return object_rec(rest, pointer_type, tmp);
148  }
149  else if(src.type().id()==ID_struct)
150  {
151  const struct_typet::componentst &components=
152  to_struct_type(src.type()).components();
153 
154  if(offset<0)
155  return src;
156 
157  mp_integer current_offset=0;
158 
159  for(struct_typet::componentst::const_iterator
160  it=components.begin();
161  it!=components.end();
162  it++)
163  {
164  assert(offset>=current_offset);
165 
166  const typet &subtype=it->type();
167 
168  mp_integer sub_size=pointer_offset_size(subtype, ns);
169  assert(sub_size>0);
170  mp_integer new_offset=current_offset+sub_size;
171 
172  if(new_offset>offset)
173  {
174  // found it
175  member_exprt tmp(subtype);
176  tmp.set_component_name(it->get_name());
177  tmp.op0()=src;
178 
179  return object_rec(
180  offset-current_offset, pointer_type, tmp);
181  }
182 
183  assert(new_offset<=offset);
184  current_offset=new_offset;
185  assert(current_offset<=offset);
186  }
187 
188  return src;
189  }
190  else if(src.type().id()==ID_union)
191  return src;
192 
193  return src;
194 }
195 
197 {
198  // add NULL
199  null_object=objects.number(exprt(ID_NULL));
200  assert(null_object==0);
201 
202  // add INVALID
203  invalid_object=objects.number(exprt("INVALID"));
204 }
205 
207 {
208 }
The type of an expression.
Definition: type.h:20
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
exprt & op0()
Definition: expr.h:84
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::vector< componentt > componentst
Definition: std_types.h:240
typet & type()
Definition: expr.h:60
void get_dynamic_objects(std::vector< std::size_t > &objects) const
A constant literal expression.
Definition: std_expr.h:3685
const namespacet & ns
Definition: pointer_logic.h:76
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:281
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Extract member of struct or union.
Definition: std_expr.h:3214
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3254
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_dynamic_object(const exprt &expr) const
The plus expression.
Definition: std_expr.h:702
exprt pointer_expr(const pointert &pointer, const typet &type) const
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.
pointer_logict(const namespacet &_ns)
objectst objects
Definition: pointer_logic.h:28
exprt & index()
Definition: std_expr.h:1208
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
Pointer Logic.
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
number_type number(const T &a)
Definition: numbering.h:80
std::size_t add_object(const exprt &expr)
std::size_t null_object
Definition: pointer_logic.h:77
exprt object_rec(const mp_integer &offset, const typet &pointer_type, const exprt &src) const
std::size_t invalid_object
Definition: pointer_logic.h:77
array index operator
Definition: std_expr.h:1170