cprover
pointer_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for Pointers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "pointer_expr.h"
10 
11 #include "arith_tools.h"
12 #include "byte_operators.h"
13 #include "c_types.h"
14 #include "expr_util.h"
15 #include "pointer_offset_size.h"
16 #include "simplify_expr.h"
17 
18 void dynamic_object_exprt::set_instance(unsigned int instance)
19 {
20  op0() = from_integer(instance, typet(ID_natural));
21 }
22 
24 {
25  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
26 }
27 
30  const namespacet &ns,
31  const exprt &expr,
33 {
34  if(expr.id() == ID_index)
35  {
36  const index_exprt &index = to_index_expr(expr);
37 
38  build_object_descriptor_rec(ns, index.array(), dest);
39 
40  auto sub_size = size_of_expr(expr.type(), ns);
41  CHECK_RETURN(sub_size.has_value());
42 
43  dest.offset() = plus_exprt(
44  dest.offset(),
45  mult_exprt(
47  typecast_exprt::conditional_cast(sub_size.value(), index_type())));
48  }
49  else if(expr.id() == ID_member)
50  {
51  const member_exprt &member = to_member_expr(expr);
52  const exprt &struct_op = member.struct_op();
53 
54  build_object_descriptor_rec(ns, struct_op, dest);
55 
56  auto offset = member_offset_expr(member, ns);
57  CHECK_RETURN(offset.has_value());
58 
59  dest.offset() = plus_exprt(
60  dest.offset(),
61  typecast_exprt::conditional_cast(offset.value(), index_type()));
62  }
63  else if(
64  expr.id() == ID_byte_extract_little_endian ||
65  expr.id() == ID_byte_extract_big_endian)
66  {
67  const byte_extract_exprt &be = to_byte_extract_expr(expr);
68 
69  dest.object() = be.op();
70 
71  build_object_descriptor_rec(ns, be.op(), dest);
72 
73  dest.offset() = plus_exprt(
74  dest.offset(),
76  to_byte_extract_expr(expr).offset(), index_type()));
77  }
78  else if(expr.id() == ID_typecast)
79  {
80  const typecast_exprt &tc = to_typecast_expr(expr);
81 
82  dest.object() = tc.op();
83 
84  build_object_descriptor_rec(ns, tc.op(), dest);
85  }
86  else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
87  {
88  const exprt &pointer = skip_typecast(deref->pointer());
89  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
90  {
91  dest.object() = address_of->object();
92  build_object_descriptor_rec(ns, address_of->object(), dest);
93  }
94  }
95  else if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
96  {
97  const exprt &object = skip_typecast(address_of->object());
98  if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(object))
99  {
100  dest.object() = deref->pointer();
101  build_object_descriptor_rec(ns, deref->pointer(), dest);
102  }
103  }
104 }
105 
107 void object_descriptor_exprt::build(const exprt &expr, const namespacet &ns)
108 {
109  PRECONDITION(object().id() == ID_unknown);
110  object() = expr;
111 
112  if(offset().id() == ID_unknown)
113  offset() = from_integer(0, index_type());
114 
115  build_object_descriptor_rec(ns, expr, *this);
116  simplify(offset(), ns);
117 }
118 
120  : unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
121 {
122 }
123 
125  : nullary_exprt(ID_object_address, pointer_type(object.type()))
126 {
127  set(ID_identifier, object.get_identifier());
128 }
129 
131 {
132  return symbol_exprt(object_identifier(), to_pointer_type(type()).subtype());
133 }
134 
136  exprt base,
137  const irep_idt &component_name,
138  pointer_typet _type)
139  : unary_exprt(ID_field_address, std::move(base), std::move(_type))
140 {
141  const auto &base_type = base.type();
142  PRECONDITION(base_type.id() == ID_pointer);
143  const auto &base_sub_type = base_type.subtype();
144  PRECONDITION(
145  base_sub_type.id() == ID_struct || base_sub_type.id() == ID_struct_tag ||
146  base_sub_type.id() == ID_union || base_sub_type.id() == ID_union_tag);
147  set(ID_component_name, component_name);
148 }
149 
151  : binary_exprt(
152  std::move(base),
153  ID_element_address,
154  std::move(index),
156  to_array_type(base.type()).subtype(),
157  to_pointer_type(base.type()).get_width()))
158 {
159 }
160 
162 {
163  const exprt *p = &expr;
164 
165  while(true)
166  {
167  if(p->id() == ID_member)
168  p = &to_member_expr(*p).compound();
169  else if(p->id() == ID_index)
170  p = &to_index_expr(*p).array();
171  else
172  break;
173  }
174 
175  return *p;
176 }
177 
186  const exprt &expr,
187  const namespacet &ns,
188  const validation_modet vm)
189 {
190  check(expr, vm);
191 
192  const auto &dereference_expr = to_dereference_expr(expr);
193 
194  const typet &type_of_operand = dereference_expr.pointer().type();
195 
196  const pointer_typet *pointer_type =
197  type_try_dynamic_cast<pointer_typet>(type_of_operand);
198 
199  DATA_CHECK(
200  vm,
201  pointer_type,
202  "dereference expression's operand must have a pointer type");
203 
204  DATA_CHECK(
205  vm,
206  dereference_expr.type() == pointer_type->subtype(),
207  "dereference expression's type must match the subtype of the type of its "
208  "operand");
209 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
field_address_exprt::base
exprt & base()
Definition: pointer_expr.h:472
arith_tools.h
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: pointer_expr.cpp:107
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
dereference_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
Definition: pointer_expr.cpp:185
object_address_exprt::object_address_exprt
object_address_exprt(const symbol_exprt &)
Definition: pointer_expr.cpp:124
field_address_exprt::field_address_exprt
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
Definition: pointer_expr.cpp:135
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: pointer_expr.cpp:119
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
exprt
Base class for all expressions.
Definition: expr.h:54
object_address_exprt::object_identifier
irep_idt object_identifier() const
Definition: pointer_expr.h:401
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: pointer_expr.h:184
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
object_address_exprt::object_expr
symbol_exprt object_expr() const
Definition: pointer_expr.cpp:130
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
nullary_exprt
An expression without operands.
Definition: std_expr.h:22
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: pointer_expr.cpp:23
byte_operators.h
Expression classes for byte-level operators.
object_address_exprt::type
const pointer_typet & type() const
Definition: pointer_expr.h:406
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2654
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
pointer_expr.h
API to expression classes for Pointers.
element_address_exprt::element_address_exprt
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
Definition: pointer_expr.cpp:150
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2654
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
field_address_exprt::component_name
const irep_idt & component_name() const
Definition: pointer_expr.h:503
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
expr_util.h
Deprecated expression utility functions.
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: pointer_expr.cpp:18
build_object_descriptor_rec
static void build_object_descriptor_rec(const namespacet &ns, const exprt &expr, object_descriptor_exprt &dest)
Build an object_descriptor_exprt from a given expr.
Definition: pointer_expr.cpp:29
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:279
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
index_exprt
Array index operator.
Definition: std_expr.h:1328
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
object_descriptor_exprt::object
exprt & object()
Definition: pointer_expr.h:173
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:220
c_types.h
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:651
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:189