CBMC
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 "pointer_predicates.h"
17 #include "simplify_expr.h"
18 
19 void dynamic_object_exprt::set_instance(unsigned int instance)
20 {
21  op0() = from_integer(instance, typet(ID_natural));
22 }
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(),
46  mult_exprt(
48  typecast_exprt::conditional_cast(sub_size.value(), c_index_type())));
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(
65  expr.id() == ID_byte_extract_little_endian ||
66  expr.id() == ID_byte_extract_big_endian)
67  {
68  const byte_extract_exprt &be = to_byte_extract_expr(expr);
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());
90  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(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 
108 void object_descriptor_exprt::build(const exprt &expr, const namespacet &ns)
109 {
110  PRECONDITION(object().id() == ID_unknown);
111  object() = expr;
112 
113  if(offset().id() == ID_unknown)
114  offset() = from_integer(0, c_index_type());
115 
116  build_object_descriptor_rec(ns, expr, *this);
117  simplify(offset(), ns);
118 }
119 
121  : unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
122 {
123 }
124 
126  : object_address_exprt(object, pointer_type(object.type()))
127 {
128 }
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 
139 {
140  return symbol_exprt(object_identifier(), to_pointer_type(type()).base_type());
141 }
142 
144  exprt compound_ptr,
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();
152  PRECONDITION(
153  compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag ||
154  compound_type.id() == ID_union || compound_type.id() == ID_union_tag);
155  set(ID_component_name, component_name);
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),
174  ID_element_address,
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 
215  const pointer_typet *pointer_type =
216  type_try_dynamic_cast<pointer_typet>(type_of_operand);
217 
218  DATA_CHECK(
219  vm,
220  pointer_type,
221  "dereference expression's operand must have a pointer type");
222 
223  DATA_CHECK(
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 
231 {
232  return and_exprt(
233  {same_object(op0(), op1()),
234  same_object(op1(), op2()),
235  r_ok_exprt(
239  pointer_offset(op1()), ID_le, pointer_offset(op2()))});
240 }
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)
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)
Definition: pointer_expr.h:755
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.
Definition: pointer_expr.h:646
element_address_exprt(const exprt &base, exprt index)
constructor for element addresses.
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
const typet & compound_type() const
Definition: pointer_expr.h:597
const irep_idt & component_name() const
Definition: pointer_expr.h:602
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 & array()
Definition: std_expr.h:1440
exprt & index()
Definition: std_expr.h:1450
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 & compound() const
Definition: std_expr.h:2843
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
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:494
symbol_exprt object_expr() const
const pointer_typet & type() const
Definition: pointer_expr.h:505
irep_idt object_identifier() const
Definition: pointer_expr.h:500
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
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...
const exprt & root_object() const
Definition: pointer_expr.h:204
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 ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:858
Expression to hold a symbol (variable)
Definition: std_expr.h:113
exprt & op1()
Definition: expr.h:128
exprt & op2()
Definition: expr.h:131
exprt & op0()
Definition: expr.h:125
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 & op() const
Definition: std_expr.h:326
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:788
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1478
#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