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 <cassert>
14 
15 #include "arith_tools.h"
16 #include "byte_operators.h"
17 #include "c_types.h"
18 #include "pointer_offset_size.h"
19 
21 {
22  const std::string val=id2string(get_value());
23  return val.find_first_not_of('0')==std::string::npos;
24 }
25 
27 {
28  if(op.empty())
29  return false_exprt();
30  else if(op.size()==1)
31  return op.front();
32  else
33  {
34  or_exprt result;
35  result.operands()=op;
36  return std::move(result);
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  and_exprt result;
59  result.operands()=op;
60  return std::move(result);
61  }
62 }
63 
66  const namespacet &ns,
67  const exprt &expr,
69 {
70  if(expr.id()==ID_index)
71  {
72  const index_exprt &index=to_index_expr(expr);
73 
74  build_object_descriptor_rec(ns, index.array(), dest);
75 
76  exprt sub_size=size_of_expr(expr.type(), ns);
77  CHECK_RETURN(sub_size.is_not_nil());
78 
79  dest.offset()=
80  plus_exprt(dest.offset(),
82  typecast_exprt(sub_size, 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  exprt offset=member_offset_expr(member, ns);
92  CHECK_RETURN(offset.is_not_nil());
93 
94  dest.offset()=
95  plus_exprt(dest.offset(),
96  typecast_exprt(offset, 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()=
108  plus_exprt(dest.offset(),
109  typecast_exprt(to_byte_extract_expr(expr).offset(),
110  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 }
121 
124  const exprt &expr,
125  const namespacet &ns)
126 {
127  PRECONDITION(object().id() == ID_unknown);
128  object()=expr;
129 
130  if(offset().id()==ID_unknown)
132 
133  build_object_descriptor_rec(ns, expr, *this);
134 }
135 
137  const exprt &_src,
138  const irep_idt &_id,
139  const std::size_t _distance):
140  binary_exprt(_src, _id, from_integer(_distance, integer_typet()))
141 {
142 }
143 
145  const exprt &_src,
146  const std::size_t _index):
148  _src, ID_extractbit, from_integer(_index, integer_typet()))
149 {
150 }
151 
153  const exprt &_src,
154  const std::size_t _upper,
155  const std::size_t _lower,
156  const typet &_type):
157  exprt(ID_extractbits, _type)
158 {
159  PRECONDITION(_upper >= _lower);
160  operands().resize(3);
161  src()=_src;
162  upper()=from_integer(_upper, integer_typet());
163  lower()=from_integer(_lower, integer_typet());
164 }
165 
167  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
168 {
169 }
170 
171 // Implementation of struct_exprt::component for const / non const overloads.
172 template <typename T>
173 auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
174  -> decltype(struct_expr.op0())
175 {
176  static_assert(
177  std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
178  const auto index =
179  to_struct_type(ns.follow(struct_expr.type())).component_number(name);
181  index < struct_expr.operands().size(),
182  "component matching index should exist");
183  return struct_expr.operands()[index];
184 }
185 
188 {
189  return ::component(*this, name, ns);
190 }
191 
193 const exprt &
194 struct_exprt::component(const irep_idt &name, const namespacet &ns) const
195 {
196  return ::component(*this, name, ns);
197 }
198 
200 {
201  const exprt *p = &object();
202 
203  while(p->id() == ID_member || p->id() == ID_index)
204  {
206  p->has_operands(), "member and index expressions have operands");
207  p = &p->op0();
208  }
209 
210  return *p;
211 }
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:187
The type of an expression, extends irept.
Definition: type.h:27
exprt size_of_expr(const typet &type, const namespacet &ns)
Semantic type conversion.
Definition: std_expr.h:2277
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
const exprt & op() const
Definition: std_expr.h:371
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:166
unsigned int get_instance() const
Definition: std_expr.cpp:45
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
exprt & lower()
Definition: std_expr.h:3198
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2870
const irep_idt & get_value() const
Definition: std_expr.h:4403
typet & type()
Return the type of the expression.
Definition: expr.h:68
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bool value_is_zero_string() const
Definition: std_expr.cpp:20
Extract member of struct or union.
Definition: std_expr.h:3890
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
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
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
The Boolean constant true.
Definition: std_expr.h:4443
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:65
A base class for binary expressions.
Definition: std_expr.h:738
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
exprt & src()
Definition: std_expr.h:3188
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
Generic base class for unary expressions.
Definition: std_expr.h:331
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt & upper()
Definition: std_expr.h:3193
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
The Boolean constant false.
Definition: std_expr.h:4452
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:26
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
Pointer Logic.
Unbounded, signed integers (mathematical integers, not bitvectors)
exprt & index()
Definition: std_expr.h:1631
Base class for all expressions.
Definition: expr.h:54
const exprt & root_object() const
Definition: std_expr.cpp:199
const exprt & struct_op() const
Definition: std_expr.h:3931
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:35
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt & array()
Definition: std_expr.h:1621
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
Array index operator.
Definition: std_expr.h:1595