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 "pointer_predicates.h"
17#include "simplify_expr.h"
18
23
25{
26 return std::stoul(id2string(to_constant_expr(op0()).get_value()));
27}
28
31 const namespacet &ns,
32 const exprt &expr,
34{
35 if(expr.id() == ID_index)
36 {
37 const index_exprt &index = to_index_expr(expr);
38
39 build_object_descriptor_rec(ns, index.array(), dest);
40
41 auto sub_size = size_of_expr(expr.type(), ns);
42 CHECK_RETURN(sub_size.has_value());
43
44 dest.offset() = plus_exprt(
45 dest.offset(),
49 }
50 else if(expr.id() == ID_member)
51 {
52 const member_exprt &member = to_member_expr(expr);
53 const exprt &struct_op = member.struct_op();
54
55 build_object_descriptor_rec(ns, struct_op, dest);
56
57 auto offset = member_offset_expr(member, ns);
58 CHECK_RETURN(offset.has_value());
59
60 dest.offset() = plus_exprt(
61 dest.offset(),
63 }
64 else if(
67 {
69
70 dest.object() = be.op();
71
72 build_object_descriptor_rec(ns, be.op(), dest);
73
74 dest.offset() = plus_exprt(
75 dest.offset(),
77 to_byte_extract_expr(expr).offset(), c_index_type()));
78 }
79 else if(expr.id() == ID_typecast)
80 {
81 const typecast_exprt &tc = to_typecast_expr(expr);
82
83 dest.object() = tc.op();
84
85 build_object_descriptor_rec(ns, tc.op(), dest);
86 }
87 else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
88 {
89 const exprt &pointer = skip_typecast(deref->pointer());
91 {
92 dest.object() = address_of->object();
93 build_object_descriptor_rec(ns, address_of->object(), dest);
94 }
95 }
96 else if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
97 {
98 const exprt &object = skip_typecast(address_of->object());
99 if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(object))
100 {
101 dest.object() = deref->pointer();
102 build_object_descriptor_rec(ns, deref->pointer(), dest);
103 }
104 }
105}
106
109{
110 PRECONDITION(object().id() == ID_unknown);
111 object() = expr;
112
113 if(offset().id() == ID_unknown)
115
116 build_object_descriptor_rec(ns, expr, *this);
117 simplify(offset(), ns);
118}
119
124
129
131 const symbol_exprt &object,
132 pointer_typet type)
133 : nullary_exprt(ID_object_address, std::move(type))
134{
135 set(ID_identifier, object.get_identifier());
136}
137
142
145 const irep_idt &component_name,
146 pointer_typet _type)
147 : unary_exprt(ID_field_address, std::move(compound_ptr), std::move(_type))
148{
149 const auto &base_type = field_address_exprt::base().type();
150 PRECONDITION(base_type.id() == ID_pointer);
151 const auto &compound_type = to_pointer_type(base_type).base_type();
156}
157
160 base,
161 std::move(index),
163 to_pointer_type(base.type()).base_type(),
164 to_pointer_type(base.type()).get_width()))
165{
166}
167
169 exprt base,
170 exprt index,
171 pointer_typet type)
172 : binary_exprt(
173 std::move(base),
175 std::move(index),
176 std::move(type))
177{
178}
179
181{
182 const exprt *p = &expr;
183
184 while(true)
185 {
186 if(p->id() == ID_member)
187 p = &to_member_expr(*p).compound();
188 else if(p->id() == ID_index)
189 p = &to_index_expr(*p).array();
190 else
191 break;
192 }
193
194 return *p;
195}
196
205 const exprt &expr,
206 const namespacet &ns,
207 const validation_modet vm)
208{
209 check(expr, vm);
210
211 const auto &dereference_expr = to_dereference_expr(expr);
212
213 const typet &type_of_operand = dereference_expr.pointer().type();
214
217
219 vm,
221 "dereference expression's operand must have a pointer type");
222
224 vm,
225 dereference_expr.type() == pointer_type->base_type(),
226 "dereference expression's type must match the base type of the type of its "
227 "operand");
228}
229
241
252
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:240
bitvector_typet c_index_type()
Definition c_types.cpp:16
address_of_exprt(const exprt &op)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
A base class for binary expressions.
Definition std_expr.h:583
exprt & op0()
Definition expr.h:125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
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:39
unsigned int get_instance() const
void set_instance(unsigned int instance)
Operator to return the address of an array element relative to a base address.
element_address_exprt(const exprt &base, exprt index)
constructor for element addresses.
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
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:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:2794
const exprt & struct_op() const
Definition std_expr.h:2832
Binary minus.
Definition std_expr.h:1006
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3026
Boolean negation.
Definition std_expr.h:2278
An expression without operands.
Definition std_expr.h:22
Operator to return the address of an object.
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:947
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.
const exprt & dead_ptr() const
const exprt & deallocated_ptr() const
exprt lower(const namespacet &ns) const
A predicate that indicates that an address range is ok to read.
const exprt & deallocated_ptr() const
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const exprt & dead_ptr() const
const exprt & pointer() const
const exprt & size() const
A predicate that indicates that an address range is ok to read.
Expression to hold a symbol (variable)
Definition std_expr.h:113
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
exprt & op2()
Definition expr.h:131
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
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.
exprt pointer_offset(const exprt &pointer)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
Various predicates over pointers in programs.
bool simplify(exprt &expr, const namespacet &ns)
#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:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
#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