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
exprt::op2
exprt & op2()
Definition: expr.h:105
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
to_side_effect_expr_overflow
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
to_history_expr
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:219
side_effect_expr_overflowt::rhs
exprt & rhs()
Definition: c_expr.h:143
shuffle_vector_exprt
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition: c_expr.h:20
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
side_effect_expr_overflowt::lhs
const exprt & lhs() const
Definition: c_expr.h:138
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
exprt::op0
exprt & op0()
Definition: expr.h:99
vector_typet
The vector type.
Definition: std_types.h:975
bool_typet
The Boolean type.
Definition: std_types.h:36
shuffle_vector_exprt::type
const vector_typet & type() const
Definition: c_expr.h:27
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1566
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:856
shuffle_vector_exprt::vector2
const exprt & vector2() const
Definition: c_expr.h:47
validate_expr
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:81
shuffle_vector_exprt::type
vector_typet & type()
Definition: c_expr.h:32
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
expr_protectedt::op0
exprt & op0()
Definition: expr.h:99
side_effect_expr_overflowt::lhs
exprt & lhs()
Definition: c_expr.h:133
shuffle_vector_exprt::vector2
exprt & vector2()
Definition: c_expr.h:52
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:850
exprt::op1
exprt & op1()
Definition: expr.h:102
side_effect_expr_overflowt::side_effect_expr_overflowt
side_effect_expr_overflowt(const irep_idt &kind, exprt _lhs, exprt _rhs, exprt _result, const source_locationt &loc)
Definition: c_expr.h:119
to_shuffle_vector_expr
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition: c_expr.h:92
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
can_cast_expr< shuffle_vector_exprt >
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
Definition: c_expr.h:76
shuffle_vector_exprt::lower
vector_exprt lower() const
Definition: c_expr.cpp:32
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1918
shuffle_vector_exprt::indices
exprt::operandst & indices()
Definition: c_expr.h:67
source_locationt
Definition: source_location.h:19
can_cast_expr< side_effect_expr_overflowt >
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
Definition: c_expr.h:165
shuffle_vector_exprt::indices
const exprt::operandst & indices() const
Definition: c_expr.h:62
history_exprt
A class for an expression that indicates a history variable.
Definition: c_expr.h:205
side_effect_expr_overflowt::result
exprt & result()
Definition: c_expr.h:153
shuffle_vector_exprt::vector1
const exprt & vector1() const
Definition: c_expr.h:37
history_exprt::history_exprt
history_exprt(exprt variable, const irep_idt &id)
Definition: c_expr.h:207
side_effect_expr_overflowt
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
exprt::operands
operandst & operands()
Definition: expr.h:92
side_effect_expr_overflowt::rhs
const exprt & rhs() const
Definition: c_expr.h:148
shuffle_vector_exprt::has_two_input_vectors
bool has_two_input_vectors() const
Definition: c_expr.h:57
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:844
history_exprt::expression
const exprt & expression() const
Definition: c_expr.h:212
side_effect_expr_overflowt::result
const exprt & result() const
Definition: c_expr.h:158
shuffle_vector_exprt::shuffle_vector_exprt
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:13
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
shuffle_vector_exprt::vector1
exprt & vector1()
Definition: c_expr.h:42