cprover
Loading...
Searching...
No Matches
pointer_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for Pointers
4
5Author: 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
18void 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(),
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(),
62 }
63 else if(
64 expr.id() == ID_byte_extract_little_endian ||
65 expr.id() == ID_byte_extract_big_endian)
66 {
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(), c_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
108{
109 PRECONDITION(object().id() == ID_unknown);
110 object() = expr;
111
112 if(offset().id() == ID_unknown)
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{
133}
134
136 exprt compound_ptr,
137 const irep_idt &component_name,
138 pointer_typet _type)
139 : unary_exprt(ID_field_address, std::move(compound_ptr), std::move(_type))
140{
141 const auto &compound_ptr_type = compound_ptr.type();
142 PRECONDITION(compound_ptr_type.id() == ID_pointer);
143 const auto &compound_type = to_pointer_type(compound_ptr_type).base_type();
145 compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag ||
146 compound_type.id() == ID_union || compound_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()).element_type(),
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
197 type_try_dynamic_cast<pointer_typet>(type_of_operand);
198
200 vm,
202 "dereference expression's operand must have a pointer type");
203
205 vm,
206 dereference_expr.type() == pointer_type->base_type(),
207 "dereference expression's type must match the base type of the type of its "
208 "operand");
209}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void base_type(typet &type, const namespacet &ns)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
bitvector_typet c_index_type()
Definition c_types.cpp:16
address_of_exprt(const exprt &op)
A base class for binary expressions.
Definition std_expr.h:550
exprt & op0()
Definition expr.h:99
Expression of type type extracted from some object op starting at position offset (given in number of...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
unsigned int get_instance() const
void set_instance(unsigned int instance)
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const irep_idt & component_name() const
const typet & compound_type() const
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2667
const exprt & compound() const
Definition std_expr.h:2708
const exprt & struct_op() const
Definition std_expr.h:2697
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
An expression without operands.
Definition std_expr.h:22
const pointer_typet & type() const
symbol_exprt object_expr() const
irep_idt object_identifier() const
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
const exprt & root_object() const
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...
The plus expression Associativity is not specified.
Definition std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Expression to hold a symbol (variable)
Definition std_expr.h:80
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
const exprt & op() const
Definition std_expr.h:293
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
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.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet