cprover
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/std_code.h>
16
20{
21public:
26
27 const vector_typet &type() const
28 {
29 return static_cast<const vector_typet &>(multi_ary_exprt::type());
30 }
31
33 {
34 return static_cast<vector_typet &>(multi_ary_exprt::type());
35 }
36
37 const exprt &vector1() const
38 {
39 return op0();
40 }
41
43 {
44 return op0();
45 }
46
47 const exprt &vector2() const
48 {
49 return op1();
50 }
51
53 {
54 return op1();
55 }
56
58 {
59 return vector2().is_not_nil();
60 }
61
63 {
64 return op2().operands();
65 }
66
68 {
69 return op2().operands();
70 }
71
72 vector_exprt lower() const;
73};
74
75template <>
77{
78 return base.id() == ID_shuffle_vector;
79}
80
81inline void validate_expr(const shuffle_vector_exprt &value)
82{
83 validate_operands(value, 3, "shuffle_vector must have three operands");
84}
85
93{
94 PRECONDITION(expr.id() == ID_shuffle_vector);
95 const shuffle_vector_exprt &ret =
96 static_cast<const shuffle_vector_exprt &>(expr);
97 validate_expr(ret);
98 return ret;
99}
100
103{
104 PRECONDITION(expr.id() == ID_shuffle_vector);
105 shuffle_vector_exprt &ret = static_cast<shuffle_vector_exprt &>(expr);
106 validate_expr(ret);
107 return ret;
108}
109
117{
118public:
120 const irep_idt &kind,
121 exprt _lhs,
122 exprt _rhs,
123 exprt _result,
124 const source_locationt &loc)
126 "overflow-" + id2string(kind),
127 {std::move(_lhs), std::move(_rhs), std::move(_result)},
128 bool_typet{},
129 loc)
130 {
131 }
132
134 {
135 return op0();
136 }
137
138 const exprt &lhs() const
139 {
140 return op0();
141 }
142
144 {
145 return op1();
146 }
147
148 const exprt &rhs() const
149 {
150 return op1();
151 }
152
154 {
155 return op2();
156 }
157
158 const exprt &result() const
159 {
160 return op2();
161 }
162};
163
164template <>
166{
167 if(base.id() != ID_side_effect)
168 return false;
169
170 const irep_idt &statement = to_side_effect_expr(base).get_statement();
171 return statement == ID_overflow_plus || statement == ID_overflow_mult ||
172 statement == ID_overflow_minus;
173}
174
181inline const side_effect_expr_overflowt &
183{
184 const auto &side_effect_expr = to_side_effect_expr(expr);
186 side_effect_expr.get_statement() == ID_overflow_plus ||
187 side_effect_expr.get_statement() == ID_overflow_mult ||
188 side_effect_expr.get_statement() == ID_overflow_minus);
189 return static_cast<const side_effect_expr_overflowt &>(side_effect_expr);
190}
191
194{
195 auto &side_effect_expr = to_side_effect_expr(expr);
197 side_effect_expr.get_statement() == ID_overflow_plus ||
198 side_effect_expr.get_statement() == ID_overflow_mult ||
199 side_effect_expr.get_statement() == ID_overflow_minus);
200 return static_cast<side_effect_expr_overflowt &>(side_effect_expr);
201}
202
205{
206public:
207 explicit history_exprt(exprt variable, const irep_idt &id)
208 : unary_exprt(id, std::move(variable))
209 {
210 }
211
212 const exprt &expression() const
213 {
214 return op0();
215 }
216};
217
218inline const history_exprt &
219to_history_expr(const exprt &expr, const irep_idt &id)
220{
221 PRECONDITION(id == ID_old || id == ID_loop_entry);
222 PRECONDITION(expr.id() == id);
223 auto &ret = static_cast<const history_exprt &>(expr);
224 validate_expr(ret);
225 return ret;
226}
227
232{
233public:
234 explicit conditional_target_group_exprt(exprt _condition, exprt _target_list)
235 : exprt(ID_conditional_target_group, empty_typet{})
236 {
237 add_to_operands(std::move(_condition));
238 add_to_operands(std::move(_target_list));
239 }
240
241 static void check(
242 const exprt &expr,
244 {
246 vm,
247 expr.operands().size() == 2,
248 "conditional target expression must have two operands");
249
251 vm,
252 expr.operands()[1].id() == ID_expression_list,
253 "conditional target second operand must be an ID_expression_list "
254 "expression, found " +
255 id2string(expr.operands()[1].id()));
256 }
257
258 static void validate(
259 const exprt &expr,
260 const namespacet &,
262 {
263 check(expr, vm);
264 }
265
266 const exprt &condition() const
267 {
268 return op0();
269 }
270
272 {
273 return op0();
274 }
275
277 {
278 return op1().operands();
279 }
280
282 {
283 return op1().operands();
284 }
285};
286
288{
290}
291
292template <>
294{
295 return base.id() == ID_conditional_target_group;
296}
297
306{
307 PRECONDITION(expr.id() == ID_conditional_target_group);
308 auto &ret = static_cast<const conditional_target_group_exprt &>(expr);
309 validate_expr(ret);
310 return ret;
311}
312
316{
317 PRECONDITION(expr.id() == ID_conditional_target_group);
318 auto &ret = static_cast<conditional_target_group_exprt &>(expr);
319 validate_expr(ret);
320 return ret;
321}
322
323#endif // CPROVER_ANSI_C_C_EXPR_H
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
Definition: c_expr.h:165
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition: c_expr.h:92
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:305
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
Definition: c_expr.h:293
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:219
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
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:182
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
Definition: c_expr.h:76
The Boolean type.
Definition: std_types.h:36
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:232
const exprt::operandst & targets() const
Definition: c_expr.h:276
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_expr.h:241
const exprt & condition() const
Definition: c_expr.h:266
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_expr.h:258
exprt::operandst & targets()
Definition: c_expr.h:281
conditional_target_group_exprt(exprt _condition, exprt _target_list)
Definition: c_expr.h:234
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
exprt & op2()
Definition: expr.h:105
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
A class for an expression that indicates a history variable.
Definition: c_expr.h:205
const exprt & expression() const
Definition: c_expr.h:212
history_exprt(exprt variable, const irep_idt &id)
Definition: c_expr.h:207
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
exprt & op2()
Definition: std_expr.h:856
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:20
const vector_typet & type() const
Definition: c_expr.h:27
const exprt & vector2() const
Definition: c_expr.h:47
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:13
const exprt::operandst & indices() const
Definition: c_expr.h:62
vector_exprt lower() const
Definition: c_expr.cpp:32
exprt & vector1()
Definition: c_expr.h:42
vector_typet & type()
Definition: c_expr.h:32
bool has_two_input_vectors() const
Definition: c_expr.h:57
exprt::operandst & indices()
Definition: c_expr.h:67
exprt & vector2()
Definition: c_expr.h:52
const exprt & vector1() const
Definition: c_expr.h:37
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
const exprt & lhs() const
Definition: c_expr.h:138
const exprt & result() const
Definition: c_expr.h:158
const exprt & rhs() const
Definition: c_expr.h:148
side_effect_expr_overflowt(const irep_idt &kind, exprt _lhs, exprt _rhs, exprt _result, const source_locationt &loc)
Definition: c_expr.h:119
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
Generic base class for unary expressions.
Definition: std_expr.h:281
Vector constructor from list of elements.
Definition: std_expr.h:1575
The vector type.
Definition: std_types.h:996
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:47
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
#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