cprover
Loading...
Searching...
No Matches
expr_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "expr_util.h"
10
11#include "arith_tools.h"
12#include "bitvector_expr.h"
13#include "byte_operators.h"
14#include "c_types.h"
15#include "config.h"
16#include "expr_iterator.h"
17#include "namespace.h"
18#include "pointer_expr.h"
19#include "pointer_offset_size.h"
20
21#include <algorithm>
22#include <unordered_set>
23
24bool is_assignable(const exprt &expr)
25{
26 if(expr.id() == ID_index)
27 return is_assignable(to_index_expr(expr).array());
28 else if(expr.id() == ID_member)
29 return is_assignable(to_member_expr(expr).compound());
30 else if(expr.id() == ID_dereference)
31 return true;
32 else if(expr.id() == ID_symbol)
33 return true;
34 else
35 return false;
36}
37
39{
40 const exprt::operandst &operands=expr.operands();
41
42 if(operands.size()<=2)
43 return expr;
44
45 // types must be identical for make_binary to be safe to use
46 const typet &type=expr.type();
47
48 exprt previous=operands.front();
49 PRECONDITION(previous.type()==type);
50
51 for(exprt::operandst::const_iterator
52 it=++operands.begin();
53 it!=operands.end();
54 ++it)
55 {
56 PRECONDITION(it->type()==type);
57
58 exprt tmp=expr;
59 tmp.operands().clear();
60 tmp.operands().resize(2);
61 to_binary_expr(tmp).op0().swap(previous);
62 to_binary_expr(tmp).op1() = *it;
63 previous.swap(tmp);
64 }
65
66 return previous;
67}
68
70{
71 const exprt::operandst &designator=src.designator();
72 PRECONDITION(!designator.empty());
73
74 with_exprt result{exprt{}, exprt{}, exprt{}};
75 exprt *dest=&result;
76
77 for(const auto &expr : designator)
78 {
80
81 if(expr.id() == ID_index_designator)
82 {
83 tmp.where() = to_index_designator(expr).index();
84 }
85 else if(expr.id() == ID_member_designator)
86 {
87 // irep_idt component_name=
88 // to_member_designator(*it).get_component_name();
89 }
90 else
92
93 *dest=tmp;
94 dest=&to_with_expr(*dest).new_value();
95 }
96
97 return result;
98}
99
101 const exprt &src,
102 const namespacet &ns)
103{
104 // We frequently need to check if a numerical type is not zero.
105 // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
106 // Note that this returns a proper bool_typet(), not a C/C++ boolean.
107 // To get a C/C++ boolean, add a further typecast.
108
109 const typet &src_type = src.type().id() == ID_c_enum_tag
111 : src.type();
112
113 if(src_type.id()==ID_bool) // already there
114 return src; // do nothing
115
116 irep_idt id=
118
119 exprt zero=from_integer(0, src_type);
120 // Use tag type if applicable:
121 zero.type() = src.type();
122
123 binary_relation_exprt comparison(src, id, std::move(zero));
124 comparison.add_source_location()=src.source_location();
125
126 return std::move(comparison);
127}
128
130{
131 if(src.id() == ID_not)
132 return to_not_expr(src).op();
133 else if(src.is_true())
134 return false_exprt();
135 else if(src.is_false())
136 return true_exprt();
137 else
138 return not_exprt(src);
139}
140
142 const exprt &expr,
143 const std::function<bool(const exprt &)> &pred)
144{
145 const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
146 return it != expr.depth_end();
147}
148
149bool has_subexpr(const exprt &src, const irep_idt &id)
150{
151 return has_subexpr(
152 src, [&](const exprt &subexpr) { return subexpr.id() == id; });
153}
154
156 const typet &type,
157 const std::function<bool(const typet &)> &pred,
158 const namespacet &ns)
159{
160 std::vector<std::reference_wrapper<const typet>> stack;
161 std::unordered_set<typet, irep_hash> visited;
162
163 const auto push_if_not_visited = [&](const typet &t) {
164 if(visited.insert(t).second)
165 stack.emplace_back(t);
166 };
167
169 while(!stack.empty())
170 {
171 const typet &top = stack.back().get();
172 stack.pop_back();
173
174 if(pred(top))
175 return true;
176 else if(top.id() == ID_c_enum_tag)
178 else if(top.id() == ID_struct_tag)
180 else if(top.id() == ID_union_tag)
182 else if(top.id() == ID_struct || top.id() == ID_union)
183 {
184 for(const auto &comp : to_struct_union_type(top).components())
186 }
187 else
188 {
189 for(const auto &subtype : to_type_with_subtypes(top).subtypes())
190 push_if_not_visited(subtype);
191 }
192 }
193
194 return false;
195}
196
197bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
198{
199 return has_subtype(
200 type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
201}
202
203if_exprt lift_if(const exprt &src, std::size_t operand_number)
204{
207
209 const exprt true_case=if_expr.true_case();
210 const exprt false_case=if_expr.false_case();
211
212 if_exprt result(if_expr.cond(), src, src);
213 result.true_case().operands()[operand_number]=true_case;
214 result.false_case().operands()[operand_number]=false_case;
215
216 return result;
217}
218
219const exprt &skip_typecast(const exprt &expr)
220{
221 if(expr.id()!=ID_typecast)
222 return expr;
223
224 return skip_typecast(to_typecast_expr(expr).op());
225}
226
230{
231 if(
232 expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
233 expr.id() == ID_side_effect)
234 {
235 return false;
236 }
237
238 if(expr.id() == ID_address_of)
239 {
240 return is_constant_address_of(to_address_of_expr(expr).object());
241 }
242 else if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
243 {
244 if(!is_constant(index->array()) || !index->index().is_constant())
245 return false;
246
247 const auto &array_type = to_array_type(index->array().type());
248 if(!array_type.size().is_constant())
249 return false;
250
251 const mp_integer size =
253 const mp_integer index_int =
255
256 return index_int >= 0 && index_int < size;
257 }
259 {
260 if(!is_constant(be->op()) || !be->offset().is_constant())
261 return false;
262
263 const auto op_bits = pointer_offset_bits(be->op().type(), ns);
264 if(!op_bits.has_value())
265 return false;
266
267 const auto extract_bits = pointer_offset_bits(be->type(), ns);
268 if(!extract_bits.has_value())
269 return false;
270
271 const mp_integer offset_bits =
273 be->get_bits_per_byte();
274
275 return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
276 }
277 else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
278 {
279 if(
280 !is_constant(eb->src()) || !eb->lower().is_constant() ||
281 !eb->upper().is_constant())
282 {
283 return false;
284 }
285
286 const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
287 if(!src_bits.has_value())
288 return false;
289
290 const mp_integer lower_bound =
292 const mp_integer upper_bound =
294
295 return lower_bound >= 0 && lower_bound <= upper_bound &&
296 upper_bound < src_bits;
297 }
298 else
299 {
300 // std::all_of returns true when there are no operands
301 return std::all_of(
302 expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
303 return is_constant(e);
304 });
305 }
306}
307
310{
311 if(expr.id() == ID_symbol)
312 {
313 return true;
314 }
315 else if(expr.id() == ID_index)
316 {
317 const index_exprt &index_expr = to_index_expr(expr);
318
319 return is_constant_address_of(index_expr.array()) &&
320 is_constant(index_expr.index());
321 }
322 else if(expr.id() == ID_member)
323 {
324 return is_constant_address_of(to_member_expr(expr).compound());
325 }
326 else if(expr.id() == ID_dereference)
327 {
329
330 return is_constant(deref.pointer());
331 }
332 else if(expr.id() == ID_string_constant)
333 return true;
334
335 return false;
336}
337
339{
340 if(value)
341 return true_exprt();
342 else
343 return false_exprt();
344}
345
347{
348 PRECONDITION(a.is_boolean() && b.is_boolean());
349 if(b.is_constant())
350 {
351 if(b.get(ID_value) == ID_false)
352 return false_exprt{};
353 return a;
354 }
355 if(a.is_constant())
356 {
357 if(a.get(ID_value) == ID_false)
358 return false_exprt{};
359 return b;
360 }
361 if(b.id() == ID_and)
362 {
363 b.add_to_operands(std::move(a));
364 return b;
365 }
366 return and_exprt{std::move(a), std::move(b)};
367}
368
370{
371 if(expr.type().id() != ID_pointer)
372 return false;
373
374 if(expr.get_value() == ID_NULL)
375 return true;
376
377 // We used to support "0" (when NULL_is_zero), but really front-ends should
378 // resolve this and generate ID_NULL instead.
379#if 0
380 return config.ansi_c.NULL_is_zero && expr.value_is_zero_string();
381#else
382 INVARIANT(
383 !expr.value_is_zero_string() || !config.ansi_c.NULL_is_zero,
384 "front-end should use ID_NULL");
385 return false;
386#endif
387}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
Expression classes for byte-level operators.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
const namespacet & ns
Definition expr_util.h:102
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2942
const irep_idt & get_value() const
Definition std_expr.h:2950
bool value_is_zero_string() const
Definition std_expr.cpp:18
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
The Boolean constant false.
Definition std_expr.h:3017
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Array index operator.
Definition std_expr.h:1410
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
exprt::operandst & designator()
Definition std_expr.h:2634
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
Forward depth-first search iterators These iterators' copy operations are expensive,...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition expr_util.cpp:69
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2539
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2303
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2486
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:219