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 <algorithm>
12#include <unordered_set>
13
14#include "arith_tools.h"
15#include "c_types.h"
16#include "expr_iterator.h"
17#include "namespace.h"
18#include "pointer_expr.h"
19#include "std_expr.h"
20
21bool is_assignable(const exprt &expr)
22{
23 if(expr.id() == ID_index)
24 return is_assignable(to_index_expr(expr).array());
25 else if(expr.id() == ID_member)
26 return is_assignable(to_member_expr(expr).compound());
27 else if(expr.id() == ID_dereference)
28 return true;
29 else if(expr.id() == ID_symbol)
30 return true;
31 else
32 return false;
33}
34
36{
37 const exprt::operandst &operands=expr.operands();
38
39 if(operands.size()<=2)
40 return expr;
41
42 // types must be identical for make_binary to be safe to use
43 const typet &type=expr.type();
44
45 exprt previous=operands.front();
46 PRECONDITION(previous.type()==type);
47
48 for(exprt::operandst::const_iterator
49 it=++operands.begin();
50 it!=operands.end();
51 ++it)
52 {
53 PRECONDITION(it->type()==type);
54
55 exprt tmp=expr;
56 tmp.operands().clear();
57 tmp.operands().resize(2);
58 to_binary_expr(tmp).op0().swap(previous);
59 to_binary_expr(tmp).op1() = *it;
60 previous.swap(tmp);
61 }
62
63 return previous;
64}
65
67{
68 const exprt::operandst &designator=src.designator();
69 PRECONDITION(!designator.empty());
70
71 with_exprt result{exprt{}, exprt{}, exprt{}};
72 exprt *dest=&result;
73
74 for(const auto &expr : designator)
75 {
77
78 if(expr.id() == ID_index_designator)
79 {
80 tmp.where() = to_index_designator(expr).index();
81 }
82 else if(expr.id() == ID_member_designator)
83 {
84 // irep_idt component_name=
85 // to_member_designator(*it).get_component_name();
86 }
87 else
89
90 *dest=tmp;
91 dest=&to_with_expr(*dest).new_value();
92 }
93
94 return result;
95}
96
98 const exprt &src,
99 const namespacet &ns)
100{
101 // We frequently need to check if a numerical type is not zero.
102 // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
103 // Note that this returns a proper bool_typet(), not a C/C++ boolean.
104 // To get a C/C++ boolean, add a further typecast.
105
106 const typet &src_type = src.type().id() == ID_c_enum_tag
108 : src.type();
109
110 if(src_type.id()==ID_bool) // already there
111 return src; // do nothing
112
113 irep_idt id=
115
116 exprt zero=from_integer(0, src_type);
117 // Use tag type if applicable:
118 zero.type() = src.type();
119
120 binary_relation_exprt comparison(src, id, std::move(zero));
121 comparison.add_source_location()=src.source_location();
122
123 return std::move(comparison);
124}
125
127{
128 if(src.id() == ID_not)
129 return to_not_expr(src).op();
130 else if(src.is_true())
131 return false_exprt();
132 else if(src.is_false())
133 return true_exprt();
134 else
135 return not_exprt(src);
136}
137
139 const exprt &expr,
140 const std::function<bool(const exprt &)> &pred)
141{
142 const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
143 return it != expr.depth_end();
144}
145
146bool has_subexpr(const exprt &src, const irep_idt &id)
147{
148 return has_subexpr(
149 src, [&](const exprt &subexpr) { return subexpr.id() == id; });
150}
151
153 const typet &type,
154 const std::function<bool(const typet &)> &pred,
155 const namespacet &ns)
156{
157 std::vector<std::reference_wrapper<const typet>> stack;
158 std::unordered_set<typet, irep_hash> visited;
159
160 const auto push_if_not_visited = [&](const typet &t) {
161 if(visited.insert(t).second)
162 stack.emplace_back(t);
163 };
164
166 while(!stack.empty())
167 {
168 const typet &top = stack.back().get();
169 stack.pop_back();
170
171 if(pred(top))
172 return true;
173 else if(top.id() == ID_c_enum_tag)
175 else if(top.id() == ID_struct_tag)
177 else if(top.id() == ID_union_tag)
179 else if(top.id() == ID_struct || top.id() == ID_union)
180 {
181 for(const auto &comp : to_struct_union_type(top).components())
183 }
184 else
185 {
186 for(const auto &subtype : to_type_with_subtypes(top).subtypes())
187 push_if_not_visited(subtype);
188 }
189 }
190
191 return false;
192}
193
194bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
195{
196 return has_subtype(
197 type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
198}
199
200if_exprt lift_if(const exprt &src, std::size_t operand_number)
201{
204
206 const exprt true_case=if_expr.true_case();
207 const exprt false_case=if_expr.false_case();
208
209 if_exprt result(if_expr.cond(), src, src);
210 result.true_case().operands()[operand_number]=true_case;
211 result.false_case().operands()[operand_number]=false_case;
212
213 return result;
214}
215
216const exprt &skip_typecast(const exprt &expr)
217{
218 if(expr.id()!=ID_typecast)
219 return expr;
220
221 return skip_typecast(to_typecast_expr(expr).op());
222}
223
226bool is_constantt::is_constant(const exprt &expr) const
227{
228 if(expr.is_constant())
229 return true;
230
231 if(expr.id() == ID_address_of)
232 {
233 return is_constant_address_of(to_address_of_expr(expr).object());
234 }
235 else if(
236 expr.id() == ID_typecast || expr.id() == ID_array_of ||
237 expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
238 expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
239 expr.id() == ID_empty_union ||
240 // byte_update works, byte_extract may be out-of-bounds
241 expr.id() == ID_byte_update_big_endian ||
243 {
244 return std::all_of(
245 expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
246 return is_constant(e);
247 });
248 }
249
250 return false;
251}
252
255{
256 if(expr.id() == ID_symbol)
257 {
258 return true;
259 }
260 else if(expr.id() == ID_index)
261 {
262 const index_exprt &index_expr = to_index_expr(expr);
263
264 return is_constant_address_of(index_expr.array()) &&
265 is_constant(index_expr.index());
266 }
267 else if(expr.id() == ID_member)
268 {
269 return is_constant_address_of(to_member_expr(expr).compound());
270 }
271 else if(expr.id() == ID_dereference)
272 {
274
275 return is_constant(deref.pointer());
276 }
277 else if(expr.id() == ID_string_constant)
278 return true;
279
280 return false;
281}
282
284{
285 if(value)
286 return true_exprt();
287 else
288 return false_exprt();
289}
290
292{
293 PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
294 if(b.is_constant())
295 {
296 if(b.get(ID_value) == ID_false)
297 return false_exprt{};
298 return a;
299 }
300 if(a.is_constant())
301 {
302 if(a.get(ID_value) == ID_false)
303 return false_exprt{};
304 return b;
305 }
306 if(b.id() == ID_and)
307 {
308 b.add_to_operands(std::move(a));
309 return b;
310 }
311 return and_exprt{std::move(a), std::move(b)};
312}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:344
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
A constant literal expression.
Definition std_expr.h:2807
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:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
depth_iteratort depth_end()
Definition expr.cpp:267
depth_iteratort depth_begin()
Definition expr.cpp:265
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:42
bool is_constant() const
Return whether the expression is a constant.
Definition expr.cpp:26
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const source_locationt & source_location() const
Definition expr.h:230
The Boolean constant false.
Definition std_expr.h:2865
The trinary if-then-else operator.
Definition std_expr.h:2226
exprt & false_case()
Definition std_expr.h:2263
exprt & true_case()
Definition std_expr.h:2253
const exprt & index() const
Definition std_expr.h:2399
Array index operator.
Definition std_expr.h:1328
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
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:2181
const componentst & components() const
Definition std_types.h:147
The Boolean constant true.
Definition std_expr.h:2856
subtypest & subtypes()
Definition type.h:206
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:293
Operator to update elements in structs and arrays.
Definition std_expr.h:2496
exprt::operandst & designator()
Definition std_expr.h:2522
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
exprt & new_value()
Definition std_expr.h:2342
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:66
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:97
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:21
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:35
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 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.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2427
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2374
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 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:221