cprover
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/std_code.h>
16 
20 {
21 public:
23  exprt vector1,
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 
57  bool has_two_input_vectors() const
58  {
59  return vector2().is_not_nil();
60  }
61 
62  const exprt::operandst &indices() const
63  {
64  return op2().operands();
65  }
66 
68  {
69  return op2().operands();
70  }
71 
72  vector_exprt lower() const;
73 };
74 
75 template <>
77 {
78  return base.id() == ID_shuffle_vector;
79 }
80 
81 inline 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 {
118 public:
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 
164 template <>
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 
181 inline const side_effect_expr_overflowt &
183 {
184  const auto &side_effect_expr = to_side_effect_expr(expr);
185  PRECONDITION(
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);
196  PRECONDITION(
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 {
206 public:
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 
218 inline const history_exprt &
219 to_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 
228 #endif // CPROVER_ANSI_C_C_EXPR_H
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
Definition: c_expr.h:165
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
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition: c_expr.h:92
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:219
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
Definition: c_expr.h:76
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
A class for an expression that indicates a history variable.
Definition: c_expr.h:205
history_exprt(exprt variable, const irep_idt &id)
Definition: c_expr.h:207
const exprt & expression() const
Definition: c_expr.h:212
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exprt & op2()
Definition: std_expr.h:856
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition: c_expr.h:20
vector_typet & type()
Definition: c_expr.h:32
exprt & vector2()
Definition: c_expr.h:52
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:13
const vector_typet & type() const
Definition: c_expr.h:27
vector_exprt lower() const
Definition: c_expr.cpp:32
const exprt & vector2() const
Definition: c_expr.h:47
exprt::operandst & indices()
Definition: c_expr.h:67
exprt & vector1()
Definition: c_expr.h:42
const exprt & vector1() const
Definition: c_expr.h:37
const exprt::operandst & indices() const
Definition: c_expr.h:62
bool has_two_input_vectors() const
Definition: c_expr.h:57
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
const exprt & result() const
Definition: c_expr.h:158
const exprt & lhs() const
Definition: c_expr.h:138
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:1896
const irep_idt & get_statement() const
Definition: std_code.h:1918
Generic base class for unary expressions.
Definition: std_expr.h:281
Vector constructor from list of elements.
Definition: std_expr.h:1566
The vector type.
Definition: std_types.h:975
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:49
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:1952