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 "namespace.h"
16 #include "pointer_offset_size.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(), 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(),
62  typecast_exprt::conditional_cast(offset.value(), index_type()));
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(), 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, 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 {
127  const exprt *p = &object();
128 
129  while(true)
130  {
131  if(p->id() == ID_member)
132  p = &to_member_expr(*p).compound();
133  else if(p->id() == ID_index)
134  p = &to_index_expr(*p).array();
135  else
136  break;
137  }
138 
139  return *p;
140 }
141 
150  const exprt &expr,
151  const namespacet &ns,
152  const validation_modet vm)
153 {
154  check(expr, vm);
155 
156  const auto &dereference_expr = to_dereference_expr(expr);
157 
158  const typet &type_of_operand = dereference_expr.pointer().type();
159 
160  const pointer_typet *pointer_type =
161  type_try_dynamic_cast<pointer_typet>(type_of_operand);
162 
163  DATA_CHECK(
164  vm,
165  pointer_type,
166  "dereference expression's operand must have a pointer type");
167 
168  DATA_CHECK(
169  vm,
170  dereference_expr.type() == pointer_type->subtype(),
171  "dereference expression's type must match the subtype of the type of its "
172  "operand");
173 }
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
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:218
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:108
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
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:1297
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
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:149
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: pointer_expr.cpp:120
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:831
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
namespace.h
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: pointer_expr.cpp:24
byte_operators.h
Expression classes for byte-level operators.
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:2569
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2558
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_expr.h
API to expression classes for Pointers.
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
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:294
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: pointer_expr.cpp:125
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
expr_util.h
Deprecated expression utility functions.
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: pointer_expr.cpp:19
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:30
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:1815
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
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
index_exprt
Array index operator.
Definition: std_expr.h:1243
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
object_descriptor_exprt::object
exprt & object()
Definition: pointer_expr.h:47
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:219
c_types.h
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:279
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:59