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 const exprt &src,
71 const namespacet &ns)
72{
73 // We frequently need to check if a numerical type is not zero.
74 // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
75 // Note that this returns a proper bool_typet(), not a C/C++ boolean.
76 // To get a C/C++ boolean, add a further typecast.
77
78 const typet &src_type = src.type().id() == ID_c_enum_tag
80 : src.type();
81
82 if(src_type.id()==ID_bool) // already there
83 return src; // do nothing
84
85 irep_idt id=
87
89 // Use tag type if applicable:
90 zero.type() = src.type();
91
92 binary_relation_exprt comparison(src, id, std::move(zero));
93 comparison.add_source_location()=src.source_location();
94
95 return std::move(comparison);
96}
97
99{
100 if(src.id() == ID_not)
101 return to_not_expr(src).op();
102 else if(src.is_true())
103 return false_exprt();
104 else if(src.is_false())
105 return true_exprt();
106 else
107 return not_exprt(src);
108}
109
111 const exprt &expr,
112 const std::function<bool(const exprt &)> &pred)
113{
114 const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
115 return it != expr.depth_end();
116}
117
118bool has_subexpr(const exprt &src, const irep_idt &id)
119{
120 return has_subexpr(
121 src, [&](const exprt &subexpr) { return subexpr.id() == id; });
122}
123
125 const typet &type,
126 const std::function<bool(const typet &)> &pred,
127 const namespacet &ns)
128{
129 std::vector<std::reference_wrapper<const typet>> stack;
130 std::unordered_set<typet, irep_hash> visited;
131
132 const auto push_if_not_visited = [&](const typet &t) {
133 if(visited.insert(t).second)
134 stack.emplace_back(t);
135 };
136
138 while(!stack.empty())
139 {
140 const typet &top = stack.back().get();
141 stack.pop_back();
142
143 if(pred(top))
144 return true;
145 else if(top.id() == ID_c_enum_tag)
147 else if(top.id() == ID_struct_tag)
149 else if(top.id() == ID_union_tag)
151 else if(top.id() == ID_struct || top.id() == ID_union)
152 {
153 for(const auto &comp : to_struct_union_type(top).components())
155 }
156 else
157 {
158 for(const auto &subtype : to_type_with_subtypes(top).subtypes())
159 push_if_not_visited(subtype);
160 }
161 }
162
163 return false;
164}
165
166bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
167{
168 return has_subtype(
169 type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
170}
171
172if_exprt lift_if(const exprt &src, std::size_t operand_number)
173{
176
178 const exprt true_case=if_expr.true_case();
179 const exprt false_case=if_expr.false_case();
180
181 if_exprt result(if_expr.cond(), src, src);
182 result.true_case().operands()[operand_number]=true_case;
183 result.false_case().operands()[operand_number]=false_case;
184
185 return result;
186}
187
188const exprt &skip_typecast(const exprt &expr)
189{
190 if(expr.id()!=ID_typecast)
191 return expr;
192
193 return skip_typecast(to_typecast_expr(expr).op());
194}
195
199{
200 if(
201 expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
202 expr.id() == ID_side_effect)
203 {
204 return false;
205 }
206
207 if(expr.id() == ID_address_of)
208 {
209 return is_constant_address_of(to_address_of_expr(expr).object());
210 }
211 else if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
212 {
213 if(!is_constant(index->array()) || !index->index().is_constant())
214 return false;
215
216 const auto &array_type = to_array_type(index->array().type());
217 if(!array_type.size().is_constant())
218 return false;
219
220 const mp_integer size =
222 const mp_integer index_int =
224
225 return index_int >= 0 && index_int < size;
226 }
228 {
229 if(!is_constant(be->op()) || !be->offset().is_constant())
230 return false;
231
232 const auto op_bits = pointer_offset_bits(be->op().type(), ns);
233 if(!op_bits.has_value())
234 return false;
235
236 const auto extract_bits = pointer_offset_bits(be->type(), ns);
237 if(!extract_bits.has_value())
238 return false;
239
240 const mp_integer offset_bits =
242 be->get_bits_per_byte();
243
244 return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
245 }
246 else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
247 {
248 if(!is_constant(eb->src()) || !eb->index().is_constant())
249 {
250 return false;
251 }
252
253 const auto eb_bits = pointer_offset_bits(eb->type(), ns);
254 if(!eb_bits.has_value())
255 return false;
256
257 const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
258 if(!src_bits.has_value())
259 return false;
260
261 const mp_integer lower_bound =
263 const mp_integer upper_bound = lower_bound + eb_bits.value() - 1;
264
265 return lower_bound >= 0 && lower_bound <= upper_bound &&
266 upper_bound < src_bits.value();
267 }
268 else
269 {
270 // std::all_of returns true when there are no operands
271 return std::all_of(
272 expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
273 return is_constant(e);
274 });
275 }
276}
277
280{
281 if(expr.id() == ID_symbol)
282 {
283 return true;
284 }
285 else if(expr.id() == ID_index)
286 {
287 const index_exprt &index_expr = to_index_expr(expr);
288
289 return is_constant_address_of(index_expr.array()) &&
290 is_constant(index_expr.index());
291 }
292 else if(expr.id() == ID_member)
293 {
294 return is_constant_address_of(to_member_expr(expr).compound());
295 }
296 else if(expr.id() == ID_dereference)
297 {
299
300 return is_constant(deref.pointer());
301 }
302 else if(expr.id() == ID_string_constant)
303 return true;
304
305 return false;
306}
307
309{
310 if(value)
311 return true_exprt();
312 else
313 return false_exprt();
314}
315
317{
318 return conjunction(a, b);
319}
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
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:100
A constant literal expression.
Definition std_expr.h:3118
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:3200
The trinary if-then-else operator.
Definition std_expr.h:2502
exprt & false_case()
Definition std_expr.h:2539
exprt & true_case()
Definition std_expr.h:2529
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:2459
The Boolean constant true.
Definition std_expr.h:3191
The type of an expression, extends irept.
Definition type.h:29
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
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:69
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
Definition expr_util.cpp:98
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
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
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:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
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