cprover
std_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "std_expr.h"
10 
11 #include <util/namespace.h>
12 
13 #include "arith_tools.h"
14 #include "byte_operators.h"
15 #include "c_types.h"
16 #include "expr_util.h"
17 #include "mathematical_types.h"
18 #include "namespace.h"
19 #include "pointer_offset_size.h"
20 #include "simplify_expr.h"
21 
23 {
24  const std::string val=id2string(get_value());
25  return val.find_first_not_of('0')==std::string::npos;
26 }
27 
29 {
30  if(op.empty())
31  return false_exprt();
32  else if(op.size()==1)
33  return op.front();
34  else
35  {
36  return or_exprt(exprt::operandst(op));
37  }
38 }
39 
40 void dynamic_object_exprt::set_instance(unsigned int instance)
41 {
42  op0()=from_integer(instance, typet(ID_natural));
43 }
44 
46 {
47  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
48 }
49 
51 {
52  if(op.empty())
53  return true_exprt();
54  else if(op.size()==1)
55  return op.front();
56  else
57  {
58  return and_exprt(exprt::operandst(op));
59  }
60 }
61 
64  const namespacet &ns,
65  const exprt &expr,
67 {
68  if(expr.id()==ID_index)
69  {
70  const index_exprt &index=to_index_expr(expr);
71 
72  build_object_descriptor_rec(ns, index.array(), dest);
73 
74  auto sub_size = size_of_expr(expr.type(), ns);
75  CHECK_RETURN(sub_size.has_value());
76 
77  dest.offset() = plus_exprt(
78  dest.offset(),
79  mult_exprt(
81  typecast_exprt::conditional_cast(sub_size.value(), index_type())));
82  }
83  else if(expr.id()==ID_member)
84  {
85  const member_exprt &member=to_member_expr(expr);
86  const exprt &struct_op=member.struct_op();
87 
88  build_object_descriptor_rec(ns, struct_op, dest);
89 
90  auto offset = member_offset_expr(member, ns);
91  CHECK_RETURN(offset.has_value());
92 
93  dest.offset() = plus_exprt(
94  dest.offset(),
95  typecast_exprt::conditional_cast(offset.value(), index_type()));
96  }
97  else if(expr.id()==ID_byte_extract_little_endian ||
98  expr.id()==ID_byte_extract_big_endian)
99  {
101 
102  dest.object()=be.op();
103 
104  build_object_descriptor_rec(ns, be.op(), dest);
105 
106  dest.offset() = plus_exprt(
107  dest.offset(),
109  to_byte_extract_expr(expr).offset(), index_type()));
110  }
111  else if(expr.id()==ID_typecast)
112  {
113  const typecast_exprt &tc=to_typecast_expr(expr);
114 
115  dest.object()=tc.op();
116 
117  build_object_descriptor_rec(ns, tc.op(), dest);
118  }
119  else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
120  {
121  const exprt &pointer = skip_typecast(deref->pointer());
122  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
123  {
124  dest.object() = address_of->object();
125  build_object_descriptor_rec(ns, address_of->object(), dest);
126  }
127  }
128  else if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
129  {
130  const exprt &object = skip_typecast(address_of->object());
131  if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(object))
132  {
133  dest.object() = deref->pointer();
134  build_object_descriptor_rec(ns, deref->pointer(), dest);
135  }
136  }
137 }
138 
141  const exprt &expr,
142  const namespacet &ns)
143 {
144  PRECONDITION(object().id() == ID_unknown);
145  object()=expr;
146 
147  if(offset().id()==ID_unknown)
149 
150  build_object_descriptor_rec(ns, expr, *this);
151  simplify(offset(), ns);
152 }
153 
155  exprt _src,
156  const irep_idt &_id,
157  const std::size_t _distance)
158  : binary_exprt(std::move(_src), _id, from_integer(_distance, integer_typet()))
159 {
160 }
161 
162 extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index)
164  std::move(_src),
165  ID_extractbit,
166  from_integer(_index, integer_typet()))
167 {
168 }
169 
171  exprt _src,
172  const std::size_t _upper,
173  const std::size_t _lower,
174  typet _type)
175  : expr_protectedt(ID_extractbits, std::move(_type))
176 {
177  PRECONDITION(_upper >= _lower);
179  std::move(_src),
180  from_integer(_upper, integer_typet()),
181  from_integer(_lower, integer_typet()));
182 }
183 
185  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
186 {
187 }
188 
189 // Implementation of struct_exprt::component for const / non const overloads.
190 template <typename T>
191 auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
192  -> decltype(struct_expr.op0())
193 {
194  static_assert(
195  std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
196  const auto index =
197  to_struct_type(ns.follow(struct_expr.type())).component_number(name);
199  index < struct_expr.operands().size(),
200  "component matching index should exist");
201  return struct_expr.operands()[index];
202 }
203 
206 {
207  return ::component(*this, name, ns);
208 }
209 
211 const exprt &
212 struct_exprt::component(const irep_idt &name, const namespacet &ns) const
213 {
214  return ::component(*this, name, ns);
215 }
216 
218 {
219  const exprt *p = &object();
220 
221  while(true)
222  {
223  if(p->id() == ID_member)
224  p = &to_member_expr(*p).compound();
225  else if(p->id() == ID_index)
226  p = &to_index_expr(*p).array();
227  else
228  break;
229  }
230 
231  return *p;
232 }
233 
242  const exprt &expr,
243  const namespacet &ns,
244  const validation_modet vm)
245 {
246  check(expr, vm);
247 
248  const auto &member_expr = to_member_expr(expr);
249 
250  const typet &compound_type = ns.follow(member_expr.compound().type());
251  const auto *struct_union_type =
252  type_try_dynamic_cast<struct_union_typet>(compound_type);
253  DATA_CHECK(
254  vm,
255  struct_union_type != nullptr,
256  "member must address a struct, union or compatible type");
257 
258  const auto &component =
259  struct_union_type->get_component(member_expr.get_component_name());
260 
261  DATA_CHECK(
262  vm,
263  component.is_not_nil(),
264  "member component '" + id2string(member_expr.get_component_name()) +
265  "' must exist on addressed type");
266 
267  DATA_CHECK(
268  vm,
269  component.type() == member_expr.type(),
270  "member expression's type must match the addressed struct or union "
271  "component");
272 }
273 
282  const exprt &expr,
283  const namespacet &ns,
284  const validation_modet vm)
285 {
286  check(expr, vm);
287 
288  const auto &dereference_expr = to_dereference_expr(expr);
289 
290  const typet &type_of_operand = dereference_expr.pointer().type();
291 
292  const pointer_typet *pointer_type =
293  type_try_dynamic_cast<pointer_typet>(type_of_operand);
294 
295  DATA_CHECK(
296  vm,
297  pointer_type,
298  "dereference expression's operand must have a pointer type");
299 
300  DATA_CHECK(
301  vm,
302  dereference_expr.type() == pointer_type->subtype(),
303  "dereference expression's type must match the subtype of the type of its "
304  "operand");
305 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
pointer_offset_size.h
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2159
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:219
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:50
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2651
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: std_expr.cpp:140
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
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:67
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1452
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1959
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: std_expr.cpp:281
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:184
and_exprt
Boolean AND.
Definition: std_expr.h:2274
integer_typet
Unbounded, signed integers (mathematical integers, not bitvectors)
Definition: mathematical_types.h:21
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:980
exprt
Base class for all expressions.
Definition: expr.h:52
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:275
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:650
exprt::op0
exprt & op0()
Definition: expr.h:97
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:191
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: std_expr.cpp:63
namespace.h
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
mathematical_types.h
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:81
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: std_expr.cpp:45
byte_operators.h
Expression classes for byte-level operators.
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:28
or_exprt
Boolean OR.
Definition: std_expr.h:2387
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3614
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:53
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3604
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3593
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:756
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2533
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1090
index_exprt::index
exprt & index()
Definition: std_expr.h:1424
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1414
member_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition: std_expr.cpp:241
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:4153
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:295
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:217
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3562
expr_util.h
Deprecated expression utility functions.
extractbit_exprt::extractbit_exprt
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:2785
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3102
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2857
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:22
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:2185
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:28
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:151
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3647
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:205
index_exprt
Array index operator.
Definition: std_expr.h:1397
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2150
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1487
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1986
true_exprt
The Boolean constant true.
Definition: std_expr.h:4144
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:226
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4104
c_types.h
expr_protectedt
Base class for all expressions.
Definition: expr.h:358
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3069
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4129
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1998