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 {
79 with_exprt tmp{exprt{}, exprt{}, exprt{}};
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=
117 src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
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
168 push_if_not_visited(type);
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)
177 push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
178 else if(top.id() == ID_struct_tag)
179 push_if_not_visited(ns.follow_tag(to_struct_tag_type(top)));
180 else if(top.id() == ID_union_tag)
181 push_if_not_visited(ns.follow_tag(to_union_tag_type(top)));
182 else if(top.id() == ID_struct || top.id() == ID_union)
183 {
184 for(const auto &comp : to_struct_union_type(top).components())
185 push_if_not_visited(comp.type());
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{
205 PRECONDITION(operand_number<src.operands().size());
206 PRECONDITION(src.operands()[operand_number].id()==ID_if);
207
208 const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
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 }
258 else if(auto be = expr_try_dynamic_cast<byte_extract_exprt>(expr))
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(!is_constant(eb->src()) || !eb->index().is_constant())
280 {
281 return false;
282 }
283
284 const auto eb_bits = pointer_offset_bits(eb->type(), ns);
285 if(!eb_bits.has_value())
286 return false;
287
288 const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
289 if(!src_bits.has_value())
290 return false;
291
292 const mp_integer lower_bound =
294 const mp_integer upper_bound = lower_bound + eb_bits.value() - 1;
295
296 return lower_bound >= 0 && lower_bound <= upper_bound &&
297 upper_bound < src_bits.value();
298 }
299 else
300 {
301 // std::all_of returns true when there are no operands
302 return std::all_of(
303 expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
304 return is_constant(e);
305 });
306 }
307}
308
311{
312 if(expr.id() == ID_symbol)
313 {
314 return true;
315 }
316 else if(expr.id() == ID_index)
317 {
318 const index_exprt &index_expr = to_index_expr(expr);
319
320 return is_constant_address_of(index_expr.array()) &&
321 is_constant(index_expr.index());
322 }
323 else if(expr.id() == ID_member)
324 {
325 return is_constant_address_of(to_member_expr(expr).compound());
326 }
327 else if(expr.id() == ID_dereference)
328 {
329 const dereference_exprt &deref = to_dereference_expr(expr);
330
331 return is_constant(deref.pointer());
332 }
333 else if(expr.id() == ID_string_constant)
334 return true;
335
336 return false;
337}
338
340{
341 if(value)
342 return true_exprt();
343 else
344 return false_exprt();
345}
346
348{
350 if(b.is_constant())
351 {
352 if(b.get(ID_value) == ID_false)
353 return false_exprt{};
354 return a;
355 }
356 if(a.is_constant())
357 {
358 if(a.get(ID_value) == ID_false)
359 return false_exprt{};
360 return b;
361 }
362 if(b.id() == ID_and)
363 {
364 b.add_to_operands(std::move(a));
365 return b;
366 }
367 return and_exprt{std::move(a), std::move(b)};
368}
369
371{
372 if(expr.type().id() != ID_pointer)
373 return false;
374
375 if(expr.get_value() == ID_NULL)
376 return true;
377
378 // We used to support "0" (when NULL_is_zero), but really front-ends should
379 // resolve this and generate ID_NULL instead.
380#if 0
382#else
383 INVARIANT(
385 "front-end should use ID_NULL");
386 return false;
387#endif
388}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
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
Boolean AND.
Definition std_expr.h:2120
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
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:2987
const irep_idt & get_value() const
Definition std_expr.h:2995
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:38
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
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
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:231
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
The Boolean constant false.
Definition std_expr.h:3064
The trinary if-then-else operator.
Definition std_expr.h:2370
exprt & cond()
Definition std_expr.h:2387
exprt & false_case()
Definition std_expr.h:2407
exprt & true_case()
Definition std_expr.h:2397
const exprt & index() const
Definition std_expr.h:2558
Array index operator.
Definition std_expr.h:1465
exprt & index()
Definition std_expr.h:1505
exprt & array()
Definition std_expr.h:1495
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
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:94
Boolean negation.
Definition std_expr.h:2327
The Boolean constant true.
Definition std_expr.h:3055
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
Operator to update elements in structs and arrays.
Definition std_expr.h:2655
exprt::operandst & designator()
Definition std_expr.h:2681
Operator to update elements in structs and arrays.
Definition std_expr.h:2471
exprt & new_value()
Definition std_expr.h:2501
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:17
#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:1533
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2586
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3037
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2352
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2533
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
bool NULL_is_zero
Definition config.h:226
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252