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 "range.h"
21 #include "simplify_expr.h"
22 
24 {
25  const std::string val=id2string(get_value());
26  return val.find_first_not_of('0')==std::string::npos;
27 }
28 
30 {
31  if(op.empty())
32  return false_exprt();
33  else if(op.size()==1)
34  return op.front();
35  else
36  {
37  return or_exprt(exprt::operandst(op));
38  }
39 }
40 
41 void dynamic_object_exprt::set_instance(unsigned int instance)
42 {
43  op0()=from_integer(instance, typet(ID_natural));
44 }
45 
47 {
48  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
49 }
50 
52 {
53  if(op.empty())
54  return true_exprt();
55  else if(op.size()==1)
56  return op.front();
57  else
58  {
59  return and_exprt(exprt::operandst(op));
60  }
61 }
62 
65  const namespacet &ns,
66  const exprt &expr,
68 {
69  if(expr.id()==ID_index)
70  {
71  const index_exprt &index=to_index_expr(expr);
72 
73  build_object_descriptor_rec(ns, index.array(), dest);
74 
75  auto sub_size = size_of_expr(expr.type(), ns);
76  CHECK_RETURN(sub_size.has_value());
77 
78  dest.offset() = plus_exprt(
79  dest.offset(),
80  mult_exprt(
82  typecast_exprt::conditional_cast(sub_size.value(), index_type())));
83  }
84  else if(expr.id()==ID_member)
85  {
86  const member_exprt &member=to_member_expr(expr);
87  const exprt &struct_op=member.struct_op();
88 
89  build_object_descriptor_rec(ns, struct_op, dest);
90 
91  auto offset = member_offset_expr(member, ns);
92  CHECK_RETURN(offset.has_value());
93 
94  dest.offset() = plus_exprt(
95  dest.offset(),
96  typecast_exprt::conditional_cast(offset.value(), index_type()));
97  }
98  else if(expr.id()==ID_byte_extract_little_endian ||
99  expr.id()==ID_byte_extract_big_endian)
100  {
102 
103  dest.object()=be.op();
104 
105  build_object_descriptor_rec(ns, be.op(), dest);
106 
107  dest.offset() = plus_exprt(
108  dest.offset(),
110  to_byte_extract_expr(expr).offset(), index_type()));
111  }
112  else if(expr.id()==ID_typecast)
113  {
114  const typecast_exprt &tc=to_typecast_expr(expr);
115 
116  dest.object()=tc.op();
117 
118  build_object_descriptor_rec(ns, tc.op(), dest);
119  }
120  else if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
121  {
122  const exprt &pointer = skip_typecast(deref->pointer());
123  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
124  {
125  dest.object() = address_of->object();
126  build_object_descriptor_rec(ns, address_of->object(), dest);
127  }
128  }
129  else if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
130  {
131  const exprt &object = skip_typecast(address_of->object());
132  if(const auto deref = expr_try_dynamic_cast<dereference_exprt>(object))
133  {
134  dest.object() = deref->pointer();
135  build_object_descriptor_rec(ns, deref->pointer(), dest);
136  }
137  }
138 }
139 
142  const exprt &expr,
143  const namespacet &ns)
144 {
145  PRECONDITION(object().id() == ID_unknown);
146  object()=expr;
147 
148  if(offset().id()==ID_unknown)
150 
151  build_object_descriptor_rec(ns, expr, *this);
152  simplify(offset(), ns);
153 }
154 
156  exprt _src,
157  const irep_idt &_id,
158  const std::size_t _distance)
159  : binary_exprt(std::move(_src), _id, from_integer(_distance, integer_typet()))
160 {
161 }
162 
163 extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index)
165  std::move(_src),
166  ID_extractbit,
167  from_integer(_index, integer_typet()))
168 {
169 }
170 
172  exprt _src,
173  const std::size_t _upper,
174  const std::size_t _lower,
175  typet _type)
176  : expr_protectedt(ID_extractbits, std::move(_type))
177 {
178  PRECONDITION(_upper >= _lower);
180  std::move(_src),
181  from_integer(_upper, integer_typet()),
182  from_integer(_lower, integer_typet()));
183 }
184 
186  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
187 {
188 }
189 
190 // Implementation of struct_exprt::component for const / non const overloads.
191 template <typename T>
192 auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
193  -> decltype(struct_expr.op0())
194 {
195  static_assert(
196  std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
197  const auto index =
198  to_struct_type(ns.follow(struct_expr.type())).component_number(name);
200  index < struct_expr.operands().size(),
201  "component matching index should exist");
202  return struct_expr.operands()[index];
203 }
204 
207 {
208  return ::component(*this, name, ns);
209 }
210 
212 const exprt &
213 struct_exprt::component(const irep_idt &name, const namespacet &ns) const
214 {
215  return ::component(*this, name, ns);
216 }
217 
219 {
220  const exprt *p = &object();
221 
222  while(true)
223  {
224  if(p->id() == ID_member)
225  p = &to_member_expr(*p).compound();
226  else if(p->id() == ID_index)
227  p = &to_index_expr(*p).array();
228  else
229  break;
230  }
231 
232  return *p;
233 }
234 
243  const exprt &expr,
244  const namespacet &ns,
245  const validation_modet vm)
246 {
247  check(expr, vm);
248 
249  const auto &member_expr = to_member_expr(expr);
250 
251  const typet &compound_type = ns.follow(member_expr.compound().type());
252  const auto *struct_union_type =
253  type_try_dynamic_cast<struct_union_typet>(compound_type);
254  DATA_CHECK(
255  vm,
256  struct_union_type != nullptr,
257  "member must address a struct, union or compatible type");
258 
259  const auto &component =
260  struct_union_type->get_component(member_expr.get_component_name());
261 
262  DATA_CHECK(
263  vm,
264  component.is_not_nil(),
265  "member component '" + id2string(member_expr.get_component_name()) +
266  "' must exist on addressed type");
267 
268  DATA_CHECK(
269  vm,
270  component.type() == member_expr.type(),
271  "member expression's type must match the addressed struct or union "
272  "component");
273 }
274 
283  const exprt &expr,
284  const namespacet &ns,
285  const validation_modet vm)
286 {
287  check(expr, vm);
288 
289  const auto &dereference_expr = to_dereference_expr(expr);
290 
291  const typet &type_of_operand = dereference_expr.pointer().type();
292 
293  const pointer_typet *pointer_type =
294  type_try_dynamic_cast<pointer_typet>(type_of_operand);
295 
296  DATA_CHECK(
297  vm,
298  pointer_type,
299  "dereference expression's operand must have a pointer type");
300 
301  DATA_CHECK(
302  vm,
303  dereference_expr.type() == pointer_type->subtype(),
304  "dereference expression's type must match the subtype of the type of its "
305  "operand");
306 }
307 
308 void let_exprt::validate(const exprt &expr, const validation_modet vm)
309 {
310  check(expr, vm);
311 
312  const auto &let_expr = to_let_expr(expr);
313 
314  DATA_CHECK(
315  vm,
316  let_expr.values().size() == let_expr.variables().size(),
317  "number of variables must match number of values");
318 
319  for(const auto &binding :
320  make_range(let_expr.variables()).zip(let_expr.values()))
321  {
322  DATA_CHECK(
323  vm,
324  binding.first.id() == ID_symbol,
325  "let binding symbols must be symbols");
326 
327  DATA_CHECK(
328  vm,
329  binding.first.type() == binding.second.type(),
330  "let bindings must be type consistent");
331  }
332 }
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:2021
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:217
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:51
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2498
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:141
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:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1831
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:282
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:185
and_exprt
Boolean AND.
Definition: std_expr.h:2136
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:880
exprt
Base class for all expressions.
Definition: expr.h:52
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:268
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:600
exprt::op0
exprt & op0()
Definition: expr.h:102
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:308
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:64
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:46
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:29
or_exprt
Boolean OR.
Definition: std_expr.h:2244
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:3456
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
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:693
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4289
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:985
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
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:242
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:418
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:613
range.h
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3963
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3404
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:2632
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: std_expr.cpp:41
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2704
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:23
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:2047
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:157
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:3489
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:206
index_exprt
Array index operator.
Definition: std_expr.h:1292
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2012
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:1858
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
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
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:4193
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
c_types.h
expr_protectedt
Base class for all expressions.
Definition: expr.h:366
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2911
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870