CBMC
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 return src.make_with_expr();
72}
73
75 const exprt &src,
76 const namespacet &ns)
77{
78 // We frequently need to check if a numerical type is not zero.
79 // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
80 // Note that this returns a proper bool_typet(), not a C/C++ boolean.
81 // To get a C/C++ boolean, add a further typecast.
82
83 const typet &src_type = src.type().id() == ID_c_enum_tag
85 : src.type();
86
87 if(src_type.id()==ID_bool) // already there
88 return src; // do nothing
89
90 irep_idt id=
92
94 // Use tag type if applicable:
95 zero.type() = src.type();
96
97 binary_relation_exprt comparison(src, id, std::move(zero));
98 comparison.add_source_location()=src.source_location();
99
100 return std::move(comparison);
101}
102
104{
105 if(src.id() == ID_not)
106 return to_not_expr(src).op();
107 else if(src.is_true())
108 return false_exprt();
109 else if(src.is_false())
110 return true_exprt();
111 else
112 return not_exprt(src);
113}
114
116 const exprt &expr,
117 const std::function<bool(const exprt &)> &pred)
118{
119 const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
120 return it != expr.depth_end();
121}
122
123bool has_subexpr(const exprt &src, const irep_idt &id)
124{
125 return has_subexpr(
126 src, [&](const exprt &subexpr) { return subexpr.id() == id; });
127}
128
130 const typet &type,
131 const std::function<bool(const typet &)> &pred,
132 const namespacet &ns)
133{
134 std::vector<std::reference_wrapper<const typet>> stack;
135 std::unordered_set<typet, irep_hash> visited;
136
137 const auto push_if_not_visited = [&](const typet &t) {
138 if(visited.insert(t).second)
139 stack.emplace_back(t);
140 };
141
143 while(!stack.empty())
144 {
145 const typet &top = stack.back().get();
146 stack.pop_back();
147
148 if(pred(top))
149 return true;
150 else if(top.id() == ID_c_enum_tag)
152 else if(top.id() == ID_struct_tag)
154 else if(top.id() == ID_union_tag)
156 else if(top.id() == ID_struct || top.id() == ID_union)
157 {
158 for(const auto &comp : to_struct_union_type(top).components())
160 }
161 else
162 {
163 for(const auto &subtype : to_type_with_subtypes(top).subtypes())
164 push_if_not_visited(subtype);
165 }
166 }
167
168 return false;
169}
170
171bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
172{
173 return has_subtype(
174 type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
175}
176
177if_exprt lift_if(const exprt &src, std::size_t operand_number)
178{
181
183 const exprt true_case=if_expr.true_case();
184 const exprt false_case=if_expr.false_case();
185
186 if_exprt result(if_expr.cond(), src, src);
187 result.true_case().operands()[operand_number]=true_case;
188 result.false_case().operands()[operand_number]=false_case;
189
190 return result;
191}
192
193const exprt &skip_typecast(const exprt &expr)
194{
195 if(expr.id()!=ID_typecast)
196 return expr;
197
198 return skip_typecast(to_typecast_expr(expr).op());
199}
200
204{
205 if(
206 expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
207 expr.id() == ID_side_effect)
208 {
209 return false;
210 }
211
212 if(expr.id() == ID_address_of)
213 {
214 return is_constant_address_of(to_address_of_expr(expr).object());
215 }
216 else if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
217 {
218 if(!is_constant(index->array()) || !index->index().is_constant())
219 return false;
220
221 const auto &array_type = to_array_type(index->array().type());
222 if(!array_type.size().is_constant())
223 return false;
224
225 const mp_integer size =
227 const mp_integer index_int =
229
230 return index_int >= 0 && index_int < size;
231 }
233 {
234 if(!is_constant(be->op()) || !be->offset().is_constant())
235 return false;
236
237 const auto op_bits = pointer_offset_bits(be->op().type(), ns);
238 if(!op_bits.has_value())
239 return false;
240
241 const auto extract_bits = pointer_offset_bits(be->type(), ns);
242 if(!extract_bits.has_value())
243 return false;
244
245 const mp_integer offset_bits =
247 be->get_bits_per_byte();
248
249 return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
250 }
251 else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
252 {
253 if(!is_constant(eb->src()) || !eb->index().is_constant())
254 {
255 return false;
256 }
257
258 const auto eb_bits = pointer_offset_bits(eb->type(), ns);
259 if(!eb_bits.has_value())
260 return false;
261
262 const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
263 if(!src_bits.has_value())
264 return false;
265
266 const mp_integer lower_bound =
268 const mp_integer upper_bound = lower_bound + eb_bits.value() - 1;
269
270 return lower_bound >= 0 && lower_bound <= upper_bound &&
271 upper_bound < src_bits.value();
272 }
273 else
274 {
275 // std::all_of returns true when there are no operands
276 return std::all_of(
277 expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
278 return is_constant(e);
279 });
280 }
281}
282
285{
286 if(expr.id() == ID_symbol)
287 {
288 return true;
289 }
290 else if(expr.id() == ID_index)
291 {
292 const index_exprt &index_expr = to_index_expr(expr);
293
294 return is_constant_address_of(index_expr.array()) &&
295 is_constant(index_expr.index());
296 }
297 else if(expr.id() == ID_member)
298 {
299 return is_constant_address_of(to_member_expr(expr).compound());
300 }
301 else if(expr.id() == ID_dereference)
302 {
304
305 return is_constant(deref.pointer());
306 }
307 else if(expr.id() == ID_string_constant)
308 return true;
309
310 return false;
311}
312
314{
315 if(value)
316 return true_exprt();
317 else
318 return false_exprt();
319}
320
322{
323 PRECONDITION(a.is_boolean() && b.is_boolean());
324 if(b.is_constant())
325 {
326 if(b.get(ID_value) == ID_false)
327 return false_exprt{};
328 return a;
329 }
330 if(a.is_constant())
331 {
332 if(a.get(ID_value) == ID_false)
333 return false_exprt{};
334 return b;
335 }
336 if(b.id() == ID_and)
337 {
338 b.add_to_operands(std::move(a));
339 return b;
340 }
341 return and_exprt{std::move(a), std::move(b)};
342}
343
345{
346 return expr.is_null_pointer();
347}
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:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
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:104
A constant literal expression.
Definition std_expr.h:3117
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
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
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:231
The Boolean constant false.
Definition std_expr.h:3199
The trinary if-then-else operator.
Definition std_expr.h:2497
exprt & false_case()
Definition std_expr.h:2534
exprt & true_case()
Definition std_expr.h:2524
Array index operator.
Definition std_expr.h:1470
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:49
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:2454
The Boolean constant true.
Definition std_expr.h:3190
The type of an expression, extends irept.
Definition type.h:29
Operator to update elements in structs and arrays.
Definition std_expr.h:2782
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:194
Operator to update elements in structs and arrays.
Definition std_expr.h:2598
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
Definition expr_util.cpp:74
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.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
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:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
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
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition type.h:252