CBMC
c_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes that are internal to the C frontend
4 
5 Author: 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 {
22 public:
24  exprt vector1,
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 
58  bool has_two_input_vectors() const
59  {
60  return vector2().is_not_nil();
61  }
62 
63  const exprt::operandst &indices() const
64  {
65  return op2().operands();
66  }
67 
69  {
70  return op2().operands();
71  }
72 
73  vector_exprt lower() const;
74 };
75 
76 template <>
78 {
79  return base.id() == ID_shuffle_vector;
80 }
81 
82 inline void validate_expr(const shuffle_vector_exprt &value)
83 {
84  validate_operands(value, 3, "shuffle_vector must have three operands");
85 }
86 
94 {
95  PRECONDITION(expr.id() == ID_shuffle_vector);
96  const shuffle_vector_exprt &ret =
97  static_cast<const shuffle_vector_exprt &>(expr);
98  validate_expr(ret);
99  return ret;
100 }
101 
104 {
105  PRECONDITION(expr.id() == ID_shuffle_vector);
106  shuffle_vector_exprt &ret = static_cast<shuffle_vector_exprt &>(expr);
107  validate_expr(ret);
108  return ret;
109 }
110 
118 {
119 public:
121  const irep_idt &kind,
122  exprt _lhs,
123  exprt _rhs,
124  exprt _result,
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 
165 template <>
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 
182 inline const side_effect_expr_overflowt &
184 {
185  const auto &side_effect_expr = to_side_effect_expr(expr);
186  PRECONDITION(
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 {
196  auto &side_effect_expr = to_side_effect_expr(expr);
197  PRECONDITION(
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 {
207 public:
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 
219 inline const history_exprt &
220 to_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);
225  validate_expr(ret);
226  return ret;
227 }
228 
233 {
234 public:
235  explicit conditional_target_group_exprt(exprt _condition, exprt _target_list)
236  : exprt(ID_conditional_target_group, empty_typet{})
237  {
238  add_to_operands(std::move(_condition));
239  add_to_operands(std::move(_target_list));
240  }
241 
242  static void check(
243  const exprt &expr,
245  {
246  DATA_CHECK(
247  vm,
248  expr.operands().size() == 2,
249  "conditional target expression must have two operands");
250 
251  DATA_CHECK(
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 
277  const exprt::operandst &targets() const
278  {
279  return op1().operands();
280  }
281 
283  {
284  return op1().operands();
285  }
286 };
287 
289 {
291 }
292 
293 template <>
295 {
296  return base.id() == ID_conditional_target_group;
297 }
298 
305 inline const conditional_target_group_exprt &
307 {
308  PRECONDITION(expr.id() == ID_conditional_target_group);
309  auto &ret = static_cast<const conditional_target_group_exprt &>(expr);
310  validate_expr(ret);
311  return ret;
312 }
313 
317 {
318  PRECONDITION(expr.id() == ID_conditional_target_group);
319  auto &ret = static_cast<conditional_target_group_exprt &>(expr);
320  validate_expr(ret);
321  return ret;
322 }
323 
327 {
328 public:
330  : unary_predicate_exprt(ID_enum_is_in_range, std::move(_op))
331  {
332  op().add_source_location().add_pragma("disable:enum-range-check");
333  }
334 
335  exprt lower(const namespacet &ns) const;
336 };
337 
338 template <>
340 {
341  return base.id() == ID_enum_is_in_range;
342 }
343 
344 inline 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 {
358  PRECONDITION(expr.id() == ID_enum_is_in_range);
359  const enum_is_in_range_exprt &ret =
360  static_cast<const enum_is_in_range_exprt &>(expr);
361  validate_expr(ret);
362  return ret;
363 }
364 
367 {
368  PRECONDITION(expr.id() == ID_enum_is_in_range);
369  enum_is_in_range_exprt &ret = static_cast<enum_is_in_range_exprt &>(expr);
370  validate_expr(ret);
371  return ret;
372 }
373 
377 {
378 public:
380  : unary_exprt(ID_bit_cast, std::move(expr), std::move(type))
381  {
382  }
383 
384  byte_extract_exprt lower() const;
385 };
386 
387 template <>
388 inline bool can_cast_expr<bit_cast_exprt>(const exprt &base)
389 {
390  return base.id() == ID_bit_cast;
391 }
392 
393 inline void validate_expr(const bit_cast_exprt &value)
394 {
395  validate_operands(value, 1, "bit_cast must have one operand");
396 }
397 
404 inline 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);
408  validate_expr(ret);
409  return ret;
410 }
411 
414 {
415  PRECONDITION(expr.id() == ID_bit_cast);
416  bit_cast_exprt &ret = static_cast<bit_cast_exprt &>(expr);
417  validate_expr(ret);
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 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
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
const bit_cast_exprt & to_bit_cast_expr(const exprt &expr)
Cast an exprt to a bit_cast_exprt.
Definition: c_expr.h:404
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
Definition: c_expr.h:294
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 shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition: c_expr.h:93
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 history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:220
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
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
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_expr.h:242
exprt::operandst & targets()
Definition: c_expr.h:282
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
conditional_target_group_exprt(exprt _condition, exprt _target_list)
Definition: c_expr.h:235
const exprt::operandst & targets() const
Definition: c_expr.h:277
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 & op1()
Definition: expr.h:136
source_locationt & add_source_location()
Definition: expr.h:236
exprt & op2()
Definition: expr.h:139
typet & type()
Return the type of the expression.
Definition: expr.h:84
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
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
history_exprt(exprt variable, const irep_idt &id)
Definition: c_expr.h:208
const exprt & expression() const
Definition: c_expr.h:213
bool is_not_nil() const
Definition: irep.h:372
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 & op2()
Definition: std_expr.h:944
exprt & op1()
Definition: std_expr.h:938
exprt & op0()
Definition: std_expr.h:932
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition: c_expr.h:21
vector_typet & type()
Definition: c_expr.h:33
exprt & vector2()
Definition: c_expr.h:53
const vector_typet & type() const
Definition: c_expr.h:28
vector_exprt lower() const
Definition: c_expr.cpp:37
shuffle_vector_exprt(exprt vector1, std::optional< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:16
const exprt & vector2() const
Definition: c_expr.h:48
exprt::operandst & indices()
Definition: c_expr.h:68
exprt & vector1()
Definition: c_expr.h:43
const exprt & vector1() const
Definition: c_expr.h:38
const exprt::operandst & indices() const
Definition: c_expr.h:63
bool has_two_input_vectors() const
Definition: c_expr.h:58
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:118
const exprt & result() const
Definition: c_expr.h:159
const exprt & lhs() const
Definition: c_expr.h:139
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
void add_pragma(const irep_idt &pragma)
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:1729
The vector type.
Definition: std_types.h:1061
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
#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