ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
expr_op.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_ILA_AST_EXPR_OP_H__
5 #define ILANG_ILA_AST_EXPR_OP_H__
6 
7 #include <ilang/ila/ast/expr.h>
8 
10 namespace ilang {
11 
12 // Forward declaration.
13 class Func;
14 
17 class ExprOp : public Expr {
18 public:
19  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
21  ExprOp(const ExprPtr arg);
23  ExprOp(const ExprPtr arg0, const ExprPtr arg1);
25  ExprOp(const ExprPtr arg0, const ExprPtr arg1, const ExprPtr arg2);
27  ExprOp(const ExprPtr arg0, const int& param1);
29  ExprOp(const ExprPtr arg0, const int& param1, const int& param2);
31  ExprOp(const ExprPtrVec& args);
32 
34  virtual ~ExprOp();
35 
36  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
38  virtual std::string op_name() const = 0;
39 
41  bool is_op() const { return true; }
42 
43  // ------------------------- METHODS -------------------------------------- //
45  virtual z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
46  const std::string& suffix = "") const = 0;
47 
49  std::ostream& Print(std::ostream& out) const;
50 
51 protected:
52  // ------------------------- HELPERS -------------------------------------- //
54  SortPtr GetSortBinaryOperation(const ExprPtr e0, const ExprPtr e1);
56  SortPtr GetSortBinaryComparison(const ExprPtr e0, const ExprPtr e1);
57 
58 private:
59  // ------------------------- MEMBERS -------------------------------------- //
60  InstrLvlAbsPtr GetHost(const ExprSet& args) const;
61 
62 }; // class ExprOp
63 
64 /******************************************************************************/
65 // Unary
66 /******************************************************************************/
67 
69 class ExprOpNeg : public ExprOp {
70 public:
72  ExprOpNeg(const ExprPtr arg);
73  std::string op_name() const { return "NEGATE"; }
74  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
75  const std::string& suffix = "") const;
76 }; // class ExprOpNeg
77 
79 class ExprOpNot : public ExprOp {
80 public:
82  ExprOpNot(const ExprPtr arg);
83  std::string op_name() const { return "NOT"; }
84  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
85  const std::string& suffix = "") const;
86 }; // class ExprOpNot
87 
89 class ExprOpCompl : public ExprOp {
90 public:
92  ExprOpCompl(const ExprPtr arg);
93  std::string op_name() const { return "COMPLEMENT"; }
94  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
95  const std::string& suffix = "") const;
96 }; // class ExprOpCompl
97 
98 /******************************************************************************/
99 // Binary operation
100 /******************************************************************************/
101 
103 class ExprOpAnd : public ExprOp {
104 public:
106  ExprOpAnd(const ExprPtr arg0, const ExprPtr arg1);
107  std::string op_name() const { return "AND"; }
108  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
109  const std::string& suffix = "") const;
110 }; // class ExprOpAnd
111 
113 class ExprOpOr : public ExprOp {
114 public:
116  ExprOpOr(const ExprPtr arg0, const ExprPtr arg1);
117  std::string op_name() const { return "OR"; }
118  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
119  const std::string& suffix = "") const;
120 }; // class ExprOpOr
121 
123 class ExprOpXor : public ExprOp {
124 public:
126  ExprOpXor(const ExprPtr arg0, const ExprPtr arg1);
127  std::string op_name() const { return "XOR"; }
128  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
129  const std::string& suffix = "") const;
130 }; // class ExprOpXor
131 
133 class ExprOpShl : public ExprOp {
134 public:
136  ExprOpShl(const ExprPtr bv, const ExprPtr n);
137  std::string op_name() const { return "SHL"; }
138  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
139  const std::string& suffix = "") const;
140 }; // class ExprOpShl
141 
143 class ExprOpAshr : public ExprOp {
144 public:
146  ExprOpAshr(const ExprPtr bv, const ExprPtr n);
147  std::string op_name() const { return "ASHR"; }
148  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
149  const std::string& suffix = "") const;
150 }; // class ExprOpAshr
151 
153 class ExprOpLshr : public ExprOp {
154 public:
156  ExprOpLshr(const ExprPtr bv, const ExprPtr n);
157  std::string op_name() const { return "LSHR"; }
158  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
159  const std::string& suffix = "") const;
160 }; // class ExprOpLshr
161 
163 class ExprOpAdd : public ExprOp {
164 public:
166  ExprOpAdd(const ExprPtr arg0, const ExprPtr arg1);
167  std::string op_name() const { return "ADD"; }
168  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
169  const std::string& suffix = "") const;
170 }; // class ExprOpAdd
171 
173 class ExprOpSub : public ExprOp {
174 public:
176  ExprOpSub(const ExprPtr arg0, const ExprPtr arg1);
177  std::string op_name() const { return "SUB"; }
178  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
179  const std::string& suffix = "") const;
180 }; // class ExprOpSub
181 
183 class ExprOpDiv : public ExprOp {
184 public:
186  ExprOpDiv(const ExprPtr arg0, const ExprPtr arg1);
187  std::string op_name() const { return "DIV"; }
188  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
189  const std::string& suffix = "") const;
190 }; // class ExprOpDiv
191 
193 class ExprOpSRem : public ExprOp {
194 public:
196  ExprOpSRem(const ExprPtr arg0, const ExprPtr arg1);
197  std::string op_name() const { return "SREM"; }
198  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
199  const std::string& suffix = "") const;
200 }; // class ExprOpSRem
201 
203 class ExprOpURem : public ExprOp {
204 public:
206  ExprOpURem(const ExprPtr arg0, const ExprPtr arg1);
207  std::string op_name() const { return "UREM"; }
208  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
209  const std::string& suffix = "") const;
210 }; // class ExprOpURem
211 
213 class ExprOpSMod : public ExprOp {
214 public:
216  ExprOpSMod(const ExprPtr arg0, const ExprPtr arg1);
217  std::string op_name() const { return "SMOD"; }
218  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
219  const std::string& suffix = "") const;
220 }; // class ExprOpSMod
221 
222 // TODO ExprOpUMod
223 
225 class ExprOpMul : public ExprOp {
226 public:
228  ExprOpMul(const ExprPtr arg0, const ExprPtr arg1);
229  std::string op_name() const { return "MUL"; }
230  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
231  const std::string& suffix = "") const;
232 }; // class ExprOpMul
233 
234 /******************************************************************************/
235 // Binary comparison
236 /******************************************************************************/
237 
239 class ExprOpEq : public ExprOp {
240 public:
242  ExprOpEq(const ExprPtr arg0, const ExprPtr arg1);
243  std::string op_name() const { return "EQ"; }
244  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
245  const std::string& suffix = "") const;
246 }; // class ExprOpEq
247 
248 // Not equal is implemented in ExprFuse with Eq and Not.
249 
251 class ExprOpLt : public ExprOp {
252 public:
254  ExprOpLt(const ExprPtr arg0, const ExprPtr arg1);
255  std::string op_name() const { return "LT"; }
256  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
257  const std::string& suffix = "") const;
258 }; // class ExprOpLt
259 
261 class ExprOpGt : public ExprOp {
262 public:
264  ExprOpGt(const ExprPtr arg0, const ExprPtr arg1);
265  std::string op_name() const { return "GT"; }
266  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
267  const std::string& suffix = "") const;
268 }; // class ExprOpGt
269 
270 // Signed less than or equal to is implemented in ExprFuse with Eq and Lt.
271 
272 // Signed greater than or equal to is implemented in ExprFuse with Eq and Gt.
273 
275 class ExprOpUlt : public ExprOp {
276 public:
278  ExprOpUlt(const ExprPtr arg0, const ExprPtr arg1);
279  std::string op_name() const { return "ULT"; }
280  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
281  const std::string& suffix = "") const;
282 }; // class ExprOpUlt
283 
285 class ExprOpUgt : public ExprOp {
286 public:
288  ExprOpUgt(const ExprPtr arg0, const ExprPtr arg1);
289  std::string op_name() const { return "UGT"; }
290  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
291  const std::string& suffix = "") const;
292 }; // class ExprOpUgt
293 
294 // Unsigned less than or equal to is implemented in ExprFuse with Eq and ULt.
295 
296 // Unsigned greater than or equal to is implemented in ExprFuse with Eq and UGt.
297 
298 /******************************************************************************/
299 // Memory
300 /******************************************************************************/
301 
303 class ExprOpLoad : public ExprOp {
304 public:
306  ExprOpLoad(const ExprPtr mem, const ExprPtr addr);
307  std::string op_name() const { return "LOAD"; }
308  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
309  const std::string& suffix = "") const;
310 }; // class ExprOpLoad
311 
313 class ExprOpStore : public ExprOp {
314 public:
316  ExprOpStore(const ExprPtr mem, const ExprPtr addr, const ExprPtr data);
317  std::string op_name() const { return "STORE"; }
318  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
319  const std::string& suffix = "") const;
320 }; // class ExprOpStore
321 
322 /******************************************************************************/
323 // Bit-manipulation
324 /******************************************************************************/
325 
327 class ExprOpConcat : public ExprOp {
328 public:
330  ExprOpConcat(const ExprPtr hi, const ExprPtr lo);
331  std::string op_name() const { return "CONCAT"; }
332  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
333  const std::string& suffix = "") const;
334 }; // class ExprOpConcat
335 
337 class ExprOpExtract : public ExprOp {
338 public:
340  ExprOpExtract(const ExprPtr bv, const int& hi, const int& lo);
341  std::string op_name() const { return "EXTRACT"; }
342  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
343  const std::string& suffix = "") const;
344 }; // class ExprOpExtract
345 
347 class ExprOpZExt : public ExprOp {
348 public:
350  ExprOpZExt(const ExprPtr bv, const int& bit_width);
351  std::string op_name() const { return "ZERO_EXTEND"; }
352  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
353  const std::string& suffix = "") const;
354 }; // class ExprOpZExtend
355 
357 class ExprOpSExt : public ExprOp {
358 public:
360  ExprOpSExt(const ExprPtr bv, const int& bit_width);
361  std::string op_name() const { return "SIGN_EXTEND"; }
362  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
363  const std::string& suffix = "") const;
364 }; // class ExprOpSExt
365 
367 class ExprOpLRotate : public ExprOp {
368 public:
370  ExprOpLRotate(const ExprPtr bv, const int& immediate);
371  std::string op_name() const { return "LEFT_ROTATE"; }
372  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
373  const std::string& suffix = "") const;
374 }; // class ExprOpLRotate
375 
377 class ExprOpRRotate : public ExprOp {
378 public:
380  ExprOpRRotate(const ExprPtr bv, const int& immediate);
381  std::string op_name() const { return "RIGHT_ROTATE"; }
382  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
383  const std::string& suffix = "") const;
384 }; // class ExprOpRRotate
385 
386 /******************************************************************************/
387 // Function usage
388 /******************************************************************************/
389 
391 class ExprOpAppFunc : public ExprOp {
392 public:
394  typedef std::shared_ptr<Func> FuncPtr;
395 
397  ExprOpAppFunc(const FuncPtr f, const ExprPtrVec& args);
398  std::string op_name() const { return "APP"; }
399  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
400  const std::string& suffix = "") const;
401  inline FuncPtr func() const { return f; }
402 
403 private:
405  FuncPtr f;
406 }; // class ExprOpAppFunc
407 
408 /******************************************************************************/
409 // Others
410 /******************************************************************************/
411 
413 class ExprOpImply : public ExprOp {
414 public:
416  ExprOpImply(const ExprPtr ante, const ExprPtr cons);
417  std::string op_name() const { return "IMPLY"; }
418  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
419  const std::string& suffix = "") const;
420 }; // class ExprOpImply
421 
423 class ExprOpIte : public ExprOp {
424 public:
426  ExprOpIte(const ExprPtr cnd, const ExprPtr true_expr,
427  const ExprPtr false_expr);
428  std::string op_name() const { return "ITE"; }
429  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
430  const std::string& suffix = "") const;
431 }; // class ExprOpIte
432 
433 } // namespace ilang
434 
435 #endif // ILANG_ILA_AST_EXPR_OP_H__
ilang::ExprOpExtract
The class wrapper for bitvector extraction.
Definition: expr_op.h:337
ilang::ExprOpImply::ExprOpImply
ExprOpImply(const ExprPtr ante, const ExprPtr cons)
Constructor for imply.
ilang::ExprOpOr::ExprOpOr
ExprOpOr(const ExprPtr arg0, const ExprPtr arg1)
Constructor for OR operation.
ilang::ExprOpZExt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:351
ilang::ExprOp::~ExprOp
virtual ~ExprOp()
Default destructor.
ilang::ExprOpOr::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:117
ilang::ExprOpZExt::ExprOpZExt
ExprOpZExt(const ExprPtr bv, const int &bit_width)
Constructor for bitvector zero-extend.
ilang::ExprOpExtract::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:341
ilang::ExprOpUgt
The class wrapper for binary comparison unsigned greater than.
Definition: expr_op.h:285
ilang::ExprOpAppFunc::FuncPtr
std::shared_ptr< Func > FuncPtr
Type for forware declaring Func.
Definition: expr_op.h:394
ilang::ExprOpIte::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:428
ilang::ExprOpSRem
The wrapper for signed remainder.
Definition: expr_op.h:193
ilang::ExprOpAppFunc
The class wrapper for apply uninterpreted function.
Definition: expr_op.h:391
ilang::ExprOpUlt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprPtr
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:133
ilang::ExprOpMul
The wrapper for unsigned multiplication.
Definition: expr_op.h:225
ilang::ExprOpAshr::ExprOpAshr
ExprOpAshr(const ExprPtr bv, const ExprPtr n)
Constructor for arithmetic right shifting a bit-vector.
ilang::ExprOpLRotate::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpZExt
The class wrapper for zero-extend.
Definition: expr_op.h:347
ilang::ExprOpLRotate::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:371
ilang::ExprOpAdd::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:167
ilang::ExprOpMul::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:229
ilang::ExprOpUgt::ExprOpUgt
ExprOpUgt(const ExprPtr arg0, const ExprPtr arg1)
Constructor for UGt comparison.
ilang::ExprOp::GetSortBinaryComparison
SortPtr GetSortBinaryComparison(const ExprPtr e0, const ExprPtr e1)
Derived the sort for binary comparisons.
ilang::Z3ExprVec
std::vector< z3::expr > Z3ExprVec
Vector type for z3 expression.
Definition: defines.h:18
ilang::ExprOpNeg::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpStore::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOp::is_op
bool is_op() const
Return trus since this is an operation.
Definition: expr_op.h:41
ilang::ExprOp::GetSortBinaryOperation
SortPtr GetSortBinaryOperation(const ExprPtr e0, const ExprPtr e1)
Derived the sort for binary operations.
ilang::ExprOpImply
The class wrapper for logical imply.
Definition: expr_op.h:413
ilang::ExprOpUlt
The class wrapper for binary comparison unsigned less than.
Definition: expr_op.h:275
ilang::ExprOpXor::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpAshr::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpConcat::ExprOpConcat
ExprOpConcat(const ExprPtr hi, const ExprPtr lo)
Constructor for bitvector concatenation.
ilang::ExprOpSMod::ExprOpSMod
ExprOpSMod(const ExprPtr arg0, const ExprPtr arg1)
Constructor for SREM operation.
ilang::ExprOpAppFunc::ExprOpAppFunc
ExprOpAppFunc(const FuncPtr f, const ExprPtrVec &args)
Constructor for apply uninterpreted function.
ilang::ExprOpUlt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:279
ilang::ExprOpSExt::ExprOpSExt
ExprOpSExt(const ExprPtr bv, const int &bit_width)
Constructor for bitvector sign-extend.
ilang::ExprOpEq::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpGt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpEq
The class wrapper for binary comparison EQ "==".
Definition: expr_op.h:239
ilang::ExprOpImply::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpAdd
The wrapper for unsigned addition.
Definition: expr_op.h:163
ilang::ExprOpSRem::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpNot::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:83
ilang::ExprOpAdd::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOp::op_name
virtual std::string op_name() const =0
Return the name of the operation.
ilang::ExprOpExtract::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOp::GetZ3Expr
virtual z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const =0
Return the z3 expression for the node.
ilang::ExprOpRRotate
The class wrapper for right-rotate.
Definition: expr_op.h:377
ilang::ExprOpSub::ExprOpSub
ExprOpSub(const ExprPtr arg0, const ExprPtr arg1)
Constructor for SUB operation.
ilang::ExprOpURem
The wrapper for unsigned remainder.
Definition: expr_op.h:203
ilang::ExprOpRRotate::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpDiv
The wrapper for unsigned division.
Definition: expr_op.h:183
ilang::ExprOpShl
The wrapper for left shifting a bit-vector.
Definition: expr_op.h:133
ilang::ExprOpCompl::ExprOpCompl
ExprOpCompl(const ExprPtr arg)
Constructor for Complement operation.
ilang::ExprOpLshr::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpShl::ExprOpShl
ExprOpShl(const ExprPtr bv, const ExprPtr n)
Constructor for left shifting a bit-vector.
expr.h
ilang::Expr::ExprPtr
std::shared_ptr< Expr > ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:28
ilang::ExprOp::Print
std::ostream & Print(std::ostream &out) const
Output to stream.
ilang::ExprOpXor::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:127
ilang::ExprOpGt
The class wrapper for binary comparison signed greater than ">".
Definition: expr_op.h:261
ilang::ExprOpAnd::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:107
ilang::ExprOpAshr::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:147
ilang::ExprOpLRotate
The class wrapper for left-rotate.
Definition: expr_op.h:367
ilang::ExprOpNot::ExprOpNot
ExprOpNot(const ExprPtr arg)
Constructor for Not operation.
ilang::ExprOpZExt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpLoad::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpNeg::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:73
ilang::ExprOpSMod
The wrapper for signed remainder.
Definition: expr_op.h:213
ilang::ExprOpXor::ExprOpXor
ExprOpXor(const ExprPtr arg0, const ExprPtr arg1)
Constructor for XOR operation.
ilang::ExprOpShl::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpIte::ExprOpIte
ExprOpIte(const ExprPtr cnd, const ExprPtr true_expr, const ExprPtr false_expr)
Constructor for if-then-else.
ilang::ExprOpStore::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:317
ilang::ExprOpSub::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpDiv::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:187
ilang::ExprOpSRem::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:197
ilang::ExprOpNeg
The wrapper for unary negate operation "-".
Definition: expr_op.h:69
ilang::ExprOpNot
The wrapper for unary not operation "!". (bool only)
Definition: expr_op.h:79
ilang::ExprOpImply::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:417
ilang::ExprOpMul::ExprOpMul
ExprOpMul(const ExprPtr arg0, const ExprPtr arg1)
Constructor for MUL operation.
ilang::ExprOpLshr
The wrapper for logical right shifting a bit-vector.
Definition: expr_op.h:153
ilang::ExprOpLoad
The class wrapper for memory load.
Definition: expr_op.h:303
ilang::Expr
The class for expression, which is the basic type for variables, constraints, state update expression...
Definition: expr.h:25
ilang::ExprOpShl::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:137
ilang::ExprOpEq::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:243
ilang::Expr::arg
ExprPtr arg(const size_t &i) const
Return the i-th argument.
Definition: expr.h:46
ilang::ExprSet
std::unordered_set< ExprPtr, ExprHash > ExprSet
Type for storing a set of Expr.
Definition: expr.h:148
ilang::ExprOpAnd
The wrapper for binary logical AND operation "&".
Definition: expr_op.h:103
ilang::ExprOpOr
The wrapper for binary logical OR operation "|".
Definition: expr_op.h:113
ilang::ExprOpSMod::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:217
ilang::ExprOpStore::ExprOpStore
ExprOpStore(const ExprPtr mem, const ExprPtr addr, const ExprPtr data)
Constructor for memory store.
ilang::ExprOpSMod::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpLRotate::ExprOpLRotate
ExprOpLRotate(const ExprPtr bv, const int &immediate)
Constructor for LRotate operation.
ilang::SortPtr
Sort::SortPtr SortPtr
Pointer type for storing/passing Sort.
Definition: sort.h:76
ilang::ExprOpNeg::ExprOpNeg
ExprOpNeg(const ExprPtr arg)
Constructor for Negate operation.
ilang::ExprOp
Expression for operations, e.g. AND, OR, ADD, etc. Operations are non-terminating nodes in the AST.
Definition: expr_op.h:17
ilang::ExprOpGt::ExprOpGt
ExprOpGt(const ExprPtr arg0, const ExprPtr arg1)
Constructor for Gt comparison.
ilang
ilang::ExprOpXor
The wrapper for binary logical XOR operation "^".
Definition: expr_op.h:123
ilang::ExprOpCompl::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:93
ilang::ExprOpConcat::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpGt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:265
ilang::ExprOpOr::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpEq::ExprOpEq
ExprOpEq(const ExprPtr arg0, const ExprPtr arg1)
Constructor for Equal comparison.
ilang::ExprOpLshr::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:157
ilang::ExprOpLt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:255
ilang::ExprOpLt
The class wrapper for binary comparison signed less than "<".
Definition: expr_op.h:251
ilang::ExprOpLshr::ExprOpLshr
ExprOpLshr(const ExprPtr bv, const ExprPtr n)
Constructor for logical right shifting a bit-vector.
ilang::ExprOpSub::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:177
ilang::ExprOpIte
The class wrapper for if-then-else.
Definition: expr_op.h:423
ilang::ExprOpDiv::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpLoad::ExprOpLoad
ExprOpLoad(const ExprPtr mem, const ExprPtr addr)
Constructor for memory load.
ilang::ExprOpURem::ExprOpURem
ExprOpURem(const ExprPtr arg0, const ExprPtr arg1)
Constructor for UREM operation.
ilang::ExprOpAnd::ExprOpAnd
ExprOpAnd(const ExprPtr arg0, const ExprPtr arg1)
Constructor for AND operation.
ilang::ExprOpDiv::ExprOpDiv
ExprOpDiv(const ExprPtr arg0, const ExprPtr arg1)
Constructor for DIV operation.
ilang::InstrLvlAbsPtr
InstrLvlAbs::InstrLvlAbsPtr InstrLvlAbsPtr
Pointer type for normal use of InstrLvlAbs.
Definition: instr_lvl_abs.h:326
ilang::ExprOpAppFunc::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:398
ilang::ExprOpAshr
The wrapper for arithmetic right shifting a bit-vector.
Definition: expr_op.h:143
ilang::ExprOpAnd::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOp::ExprOp
ExprOp(const ExprPtr arg)
Constructor for unary operators.
ilang::ExprOpURem::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:207
ilang::ExprOpURem::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpNot::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpLt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpSExt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::FuncPtr
Func::FuncPtr FuncPtr
Pointer type for normal use of Func.
Definition: func.h:79
ilang::ExprOpExtract::ExprOpExtract
ExprOpExtract(const ExprPtr bv, const int &hi, const int &lo)
Constructor for bitvector extraction.
ilang::ExprOpAppFunc::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpSExt
The class wrapper for sign-extend.
Definition: expr_op.h:357
ilang::ExprOpLt::ExprOpLt
ExprOpLt(const ExprPtr arg0, const ExprPtr arg1)
Construtor for Lt comparison.
ilang::ExprOpConcat
The class wrapper for bitvector concatenation.
Definition: expr_op.h:327
ilang::ExprOpConcat::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:331
ilang::ExprOpStore
The class wrapper for memory store.
Definition: expr_op.h:313
ilang::ExprOpSExt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:361
ilang::ExprOpLoad::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:307
ilang::ExprOpUlt::ExprOpUlt
ExprOpUlt(const ExprPtr arg0, const ExprPtr arg1)
Construtor for ULt comparison.
ilang::ExprOpCompl::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpSRem::ExprOpSRem
ExprOpSRem(const ExprPtr arg0, const ExprPtr arg1)
Constructor for SREM operation.
ilang::ExprOpUgt::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:289
ilang::ExprOpMul::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::Expr::ExprPtrVec
std::vector< ExprPtr > ExprPtrVec
Type for storing a set of Expr.
Definition: expr.h:30
ilang::ExprOpIte::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.
ilang::ExprOpRRotate::op_name
std::string op_name() const
Return the name of the operation.
Definition: expr_op.h:381
ilang::ExprOpSub
The wrapper for unsigned subtraction.
Definition: expr_op.h:173
ilang::ExprOpAdd::ExprOpAdd
ExprOpAdd(const ExprPtr arg0, const ExprPtr arg1)
Constructor for ADD operation.
ilang::ExprOpRRotate::ExprOpRRotate
ExprOpRRotate(const ExprPtr bv, const int &immediate)
Constructor for LRotate operation.
ilang::ExprOpCompl
The wrapper for unary bit-wise complement "~". (bv only)
Definition: expr_op.h:89
ilang::ExprOpUgt::GetZ3Expr
z3::expr GetZ3Expr(z3::context &ctx, const Z3ExprVec &expr_vec, const std::string &suffix="") const
Return the z3 expression for the node.