CBMC
Loading...
Searching...
No Matches
c_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes that are internal to the C frontend
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_ANSI_C_C_EXPR_H
10#define CPROVER_ANSI_C_C_EXPR_H
11
14
15#include <util/byte_operators.h>
16#include <util/std_code.h>
17
21{
22public:
25 std::optional<exprt> vector2,
27
28 const vector_typet &type() const
29 {
30 return static_cast<const vector_typet &>(multi_ary_exprt::type());
31 }
32
34 {
35 return static_cast<vector_typet &>(multi_ary_exprt::type());
36 }
37
38 const exprt &vector1() const
39 {
40 return op0();
41 }
42
44 {
45 return op0();
46 }
47
48 const exprt &vector2() const
49 {
50 return op1();
51 }
52
54 {
55 return op1();
56 }
57
59 {
60 return vector2().is_not_nil();
61 }
62
64 {
65 return op2().operands();
66 }
67
69 {
70 return op2().operands();
71 }
72
73 vector_exprt lower() const;
74};
75
76template <>
78{
79 return base.id() == ID_shuffle_vector;
80}
81
82inline void validate_expr(const shuffle_vector_exprt &value)
83{
84 validate_operands(value, 3, "shuffle_vector must have three operands");
85}
86
94{
97 static_cast<const shuffle_vector_exprt &>(expr);
99 return ret;
100}
101
104{
106 shuffle_vector_exprt &ret = static_cast<shuffle_vector_exprt &>(expr);
108 return ret;
109}
110
118{
119public:
121 const irep_idt &kind,
122 exprt _lhs,
123 exprt _rhs,
125 const source_locationt &loc)
127 "overflow-" + id2string(kind),
128 {std::move(_lhs), std::move(_rhs), std::move(_result)},
129 bool_typet{},
130 loc)
131 {
132 }
133
135 {
136 return op0();
137 }
138
139 const exprt &lhs() const
140 {
141 return op0();
142 }
143
145 {
146 return op1();
147 }
148
149 const exprt &rhs() const
150 {
151 return op1();
152 }
153
155 {
156 return op2();
157 }
158
159 const exprt &result() const
160 {
161 return op2();
162 }
163};
164
165template <>
167{
168 if(base.id() != ID_side_effect)
169 return false;
170
171 const irep_idt &statement = to_side_effect_expr(base).get_statement();
172 return statement == ID_overflow_plus || statement == ID_overflow_mult ||
173 statement == ID_overflow_minus;
174}
175
182inline const side_effect_expr_overflowt &
184{
185 const auto &side_effect_expr = to_side_effect_expr(expr);
187 side_effect_expr.get_statement() == ID_overflow_plus ||
188 side_effect_expr.get_statement() == ID_overflow_mult ||
189 side_effect_expr.get_statement() == ID_overflow_minus);
190 return static_cast<const side_effect_expr_overflowt &>(side_effect_expr);
191}
192
195{
198 side_effect_expr.get_statement() == ID_overflow_plus ||
199 side_effect_expr.get_statement() == ID_overflow_mult ||
200 side_effect_expr.get_statement() == ID_overflow_minus);
201 return static_cast<side_effect_expr_overflowt &>(side_effect_expr);
202}
203
206{
207public:
208 explicit history_exprt(exprt variable, const irep_idt &id)
209 : unary_exprt(id, std::move(variable))
210 {
211 }
212
213 const exprt &expression() const
214 {
215 return op0();
216 }
217};
218
219inline const history_exprt &
220to_history_expr(const exprt &expr, const irep_idt &id)
221{
222 PRECONDITION(id == ID_old || id == ID_loop_entry);
223 PRECONDITION(expr.id() == id);
224 auto &ret = static_cast<const history_exprt &>(expr);
226 return ret;
227}
228
233{
234public:
241
242 static void check(
243 const exprt &expr,
245 {
247 vm,
248 expr.operands().size() == 2,
249 "conditional target expression must have two operands");
250
252 vm,
253 expr.operands()[1].id() == ID_expression_list,
254 "conditional target second operand must be an ID_expression_list "
255 "expression, found " +
256 id2string(expr.operands()[1].id()));
257 }
258
259 static void validate(
260 const exprt &expr,
261 const namespacet &,
263 {
264 check(expr, vm);
265 }
266
267 const exprt &condition() const
268 {
269 return op0();
270 }
271
273 {
274 return op0();
275 }
276
278 {
279 return op1().operands();
280 }
281
283 {
284 return op1().operands();
285 }
286};
287
292
293template <>
295{
296 return base.id() == ID_conditional_target_group;
297}
298
307{
309 auto &ret = static_cast<const conditional_target_group_exprt &>(expr);
311 return ret;
312}
313
317{
319 auto &ret = static_cast<conditional_target_group_exprt &>(expr);
321 return ret;
322}
323
327{
328public:
331 {
332 op().add_source_location().add_pragma("disable:enum-range-check");
333 }
334
335 exprt lower(const namespacet &ns) const;
336};
337
338template <>
340{
341 return base.id() == ID_enum_is_in_range;
342}
343
344inline void validate_expr(const enum_is_in_range_exprt &expr)
345{
347 expr, 1, "enum_is_in_range expression must have one operand");
348}
349
357{
360 static_cast<const enum_is_in_range_exprt &>(expr);
362 return ret;
363}
364
373
377{
378public:
380 : unary_exprt(ID_bit_cast, std::move(expr), std::move(type))
381 {
382 }
383
385};
386
387template <>
388inline bool can_cast_expr<bit_cast_exprt>(const exprt &base)
389{
390 return base.id() == ID_bit_cast;
391}
392
393inline void validate_expr(const bit_cast_exprt &value)
394{
395 validate_operands(value, 1, "bit_cast must have one operand");
396}
397
404inline const bit_cast_exprt &to_bit_cast_expr(const exprt &expr)
405{
406 PRECONDITION(expr.id() == ID_bit_cast);
407 const bit_cast_exprt &ret = static_cast<const bit_cast_exprt &>(expr);
409 return ret;
410}
411
414{
415 PRECONDITION(expr.id() == ID_bit_cast);
416 bit_cast_exprt &ret = static_cast<bit_cast_exprt &>(expr);
418 return ret;
419}
420
421#endif // CPROVER_ANSI_C_C_EXPR_H
Expression classes for byte-level operators.
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
Definition c_expr.h:166
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition c_expr.h:93
const enum_is_in_range_exprt & to_enum_is_in_range_expr(const exprt &expr)
Cast an exprt to an enum_is_in_range_exprt.
Definition c_expr.h:356
const bit_cast_exprt & to_bit_cast_expr(const exprt &expr)
Cast an exprt to a bit_cast_exprt.
Definition c_expr.h:404
const conditional_target_group_exprt & to_conditional_target_group_expr(const exprt &expr)
Cast an exprt to a conditional_target_group_exprt.
Definition c_expr.h:306
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
Definition c_expr.h:294
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition c_expr.h:220
bool can_cast_expr< enum_is_in_range_exprt >(const exprt &base)
Definition c_expr.h:339
void validate_expr(const shuffle_vector_exprt &value)
Definition c_expr.h:82
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
Definition c_expr.h:183
bool can_cast_expr< bit_cast_exprt >(const exprt &base)
Definition c_expr.h:388
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
Definition c_expr.h:77
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Reinterpret the bits of an expression of type S as an expression of type T where S and T have the sam...
Definition c_expr.h:377
bit_cast_exprt(exprt expr, typet type)
Definition c_expr.h:379
byte_extract_exprt lower() const
Definition c_expr.cpp:87
The Boolean type.
Definition std_types.h:36
Expression of type type extracted from some object op starting at position offset (given in number of...
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:233
const exprt::operandst & targets() const
Definition c_expr.h:277
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition c_expr.h:242
const exprt & condition() const
Definition c_expr.h:267
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition c_expr.h:259
exprt::operandst & targets()
Definition c_expr.h:282
conditional_target_group_exprt(exprt _condition, exprt _target_list)
Definition c_expr.h:235
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
The empty type.
Definition std_types.h:51
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:327
exprt lower(const namespacet &ns) const
Definition c_expr.cpp:71
enum_is_in_range_exprt(exprt _op)
Definition c_expr.h:329
exprt & op0()
Definition expr.h:133
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
exprt & op2()
Definition expr.h:139
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
A class for an expression that indicates a history variable.
Definition c_expr.h:206
const exprt & expression() const
Definition c_expr.h:213
history_exprt(exprt variable, const irep_idt &id)
Definition c_expr.h:208
const irep_idt & id() const
Definition irep.h:388
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
exprt & op1()
Definition std_expr.h:938
exprt & op0()
Definition std_expr.h:932
exprt & op2()
Definition std_expr.h:944
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition c_expr.h:21
const vector_typet & type() const
Definition c_expr.h:28
const exprt & vector2() const
Definition c_expr.h:48
const exprt::operandst & indices() const
Definition c_expr.h:63
vector_exprt lower() const
Definition c_expr.cpp:37
exprt & vector1()
Definition c_expr.h:43
vector_typet & type()
Definition c_expr.h:33
bool has_two_input_vectors() const
Definition c_expr.h:58
exprt::operandst & indices()
Definition c_expr.h:68
exprt & vector2()
Definition c_expr.h:53
const exprt & vector1() const
Definition c_expr.h:38
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition c_expr.h:118
const exprt & lhs() const
Definition c_expr.h:139
const exprt & result() const
Definition c_expr.h:159
const exprt & rhs() const
Definition c_expr.h:149
side_effect_expr_overflowt(const irep_idt &kind, exprt _lhs, exprt _rhs, exprt _result, const source_locationt &loc)
Definition c_expr.h:120
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:585
Vector constructor from list of elements.
Definition std_expr.h:1734
The vector type.
Definition std_types.h:1064
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet