expr_op.h

Go to the documentation of this file.

#ifndef ILANG_ILA_AST_EXPR_OP_H__
#define ILANG_ILA_AST_EXPR_OP_H__

#include <ilang/ila/ast/expr.h>

namespace ilang {

// Add new op to the END of the list to ensure backward compatibility
enum AstUidExprOp {
  kInvalid = 0,
  kNegate,
  kNot,
  kComplement,
  kAnd,
  kOr,
  kXor,
  kShiftLeft,
  kArithShiftRight,
  kLogicShiftRight,
  kAdd,
  kSubtract,
  kMultiply,
  kEqual,
  kLessThan,
  kGreaterThan,
  kUnsignedLessThan,
  kUnsignedGreaterThan,
  kLoad,
  kStore,
  kConcatenate,
  kExtract,
  kZeroExtend,
  kSignedExtend,
  kApplyFunc,
  kImply,
  kIfThenElse,
  kDivide,
  kRotateLeft,
  kRotateRight,
  kSignedRemainder,
  kUnsignedRemainder,
  kSignedModular
}; // enum AstUidExprOp

// Forward declaration.
class Func;

class ExprOp : public Expr {
public:
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  ExprOp(const ExprPtr& arg);
  ExprOp(const ExprPtr& arg0, const ExprPtr& arg1);
  ExprOp(const ExprPtr& arg0, const ExprPtr& arg1, const ExprPtr& arg2);
  ExprOp(const ExprPtr& arg0, const int& param1);
  ExprOp(const ExprPtr& arg0, const int& param1, const int& param2);
  ExprOp(const ExprPtrVec& args);

  virtual ~ExprOp();

  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
  virtual AstUidExprOp uid() const = 0;

  std::string op_name() const;

  bool is_op() const { return true; }

  // ------------------------- METHODS -------------------------------------- //
  virtual z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                             const std::string& suffix) const = 0;

  std::ostream& Print(std::ostream& out) const;

protected:
  // ------------------------- HELPERS -------------------------------------- //
  SortPtr GetSortBinaryOperation(const ExprPtr& e0, const ExprPtr& e1);
  SortPtr GetSortBinaryComparison(const ExprPtr& e0, const ExprPtr& e1);

private:
  // ------------------------- MEMBERS -------------------------------------- //
  InstrLvlAbsPtr GetHost(const ExprSet& args) const;

}; // class ExprOp

/******************************************************************************/
// Unary
/******************************************************************************/

class ExprOpNeg : public ExprOp {
public:
  ExprOpNeg(const ExprPtr& arg);
  AstUidExprOp uid() const { return AstUidExprOp::kNegate; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpNeg

class ExprOpNot : public ExprOp {
public:
  ExprOpNot(const ExprPtr& arg);
  AstUidExprOp uid() const { return AstUidExprOp::kNot; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpNot

class ExprOpCompl : public ExprOp {
public:
  ExprOpCompl(const ExprPtr& arg);
  AstUidExprOp uid() const { return AstUidExprOp::kComplement; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpCompl

/******************************************************************************/
// Binary operation
/******************************************************************************/

class ExprOpAnd : public ExprOp {
public:
  ExprOpAnd(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kAnd; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpAnd

class ExprOpOr : public ExprOp {
public:
  ExprOpOr(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kOr; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpOr

class ExprOpXor : public ExprOp {
public:
  ExprOpXor(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kXor; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpXor

class ExprOpShl : public ExprOp {
public:
  ExprOpShl(const ExprPtr& bv, const ExprPtr& n);
  AstUidExprOp uid() const { return AstUidExprOp::kShiftLeft; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpShl

class ExprOpAshr : public ExprOp {
public:
  ExprOpAshr(const ExprPtr& bv, const ExprPtr& n);
  AstUidExprOp uid() const { return AstUidExprOp::kArithShiftRight; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpAshr

class ExprOpLshr : public ExprOp {
public:
  ExprOpLshr(const ExprPtr& bv, const ExprPtr& n);
  AstUidExprOp uid() const { return AstUidExprOp::kLogicShiftRight; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpLshr

class ExprOpAdd : public ExprOp {
public:
  ExprOpAdd(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kAdd; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpAdd

class ExprOpSub : public ExprOp {
public:
  ExprOpSub(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kSubtract; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpSub

class ExprOpDiv : public ExprOp {
public:
  ExprOpDiv(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kDivide; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpDiv

class ExprOpSRem : public ExprOp {
public:
  ExprOpSRem(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kSignedRemainder; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpSRem

class ExprOpURem : public ExprOp {
public:
  ExprOpURem(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kUnsignedRemainder; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpURem

class ExprOpSMod : public ExprOp {
public:
  ExprOpSMod(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kSignedModular; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpSMod

// TODO ExprOpUMod

class ExprOpMul : public ExprOp {
public:
  ExprOpMul(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kMultiply; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpMul

/******************************************************************************/
// Binary comparison
/******************************************************************************/

class ExprOpEq : public ExprOp {
public:
  ExprOpEq(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kEqual; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpEq

// Not equal is implemented in asthub with Eq and Not.

class ExprOpLt : public ExprOp {
public:
  ExprOpLt(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kLessThan; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpLt

class ExprOpGt : public ExprOp {
public:
  ExprOpGt(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kGreaterThan; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpGt

// Signed less than or equal to is implemented in asthub with Eq and Lt.

// Signed greater than or equal to is implemented in asthub with Eq and Gt.

class ExprOpUlt : public ExprOp {
public:
  ExprOpUlt(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kUnsignedLessThan; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpUlt

class ExprOpUgt : public ExprOp {
public:
  ExprOpUgt(const ExprPtr& arg0, const ExprPtr& arg1);
  AstUidExprOp uid() const { return AstUidExprOp::kUnsignedGreaterThan; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpUgt

// Unsigned less than or equal to is implemented in asthub with Eq and ULt.

// Unsigned greater than or equal to is implemented in asthub with Eq and UGt.

/******************************************************************************/
// Memory
/******************************************************************************/

class ExprOpLoad : public ExprOp {
public:
  ExprOpLoad(const ExprPtr& mem, const ExprPtr& addr);
  AstUidExprOp uid() const { return AstUidExprOp::kLoad; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpLoad

class ExprOpStore : public ExprOp {
public:
  ExprOpStore(const ExprPtr& mem, const ExprPtr& addr, const ExprPtr& data);
  AstUidExprOp uid() const { return AstUidExprOp::kStore; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpStore

/******************************************************************************/
// Bit-manipulation
/******************************************************************************/

class ExprOpConcat : public ExprOp {
public:
  ExprOpConcat(const ExprPtr& hi, const ExprPtr& lo);
  AstUidExprOp uid() const { return AstUidExprOp::kConcatenate; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpConcat

class ExprOpExtract : public ExprOp {
public:
  ExprOpExtract(const ExprPtr& bv, const int& hi, const int& lo);
  AstUidExprOp uid() const { return AstUidExprOp::kExtract; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpExtract

class ExprOpZExt : public ExprOp {
public:
  ExprOpZExt(const ExprPtr& bv, const int& bit_width);
  AstUidExprOp uid() const { return AstUidExprOp::kZeroExtend; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpZExtend

class ExprOpSExt : public ExprOp {
public:
  ExprOpSExt(const ExprPtr& bv, const int& bit_width);
  AstUidExprOp uid() const { return AstUidExprOp::kSignedExtend; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpSExt

class ExprOpLRotate : public ExprOp {
public:
  ExprOpLRotate(const ExprPtr& bv, const int& immediate);
  AstUidExprOp uid() const { return AstUidExprOp::kRotateLeft; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpLRotate

class ExprOpRRotate : public ExprOp {
public:
  ExprOpRRotate(const ExprPtr& bv, const int& immediate);
  AstUidExprOp uid() const { return AstUidExprOp::kRotateRight; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpRRotate

/******************************************************************************/
// Function usage
/******************************************************************************/

class ExprOpAppFunc : public ExprOp {
public:
  typedef std::shared_ptr<Func> FuncPtr;

  ExprOpAppFunc(const FuncPtr& f, const ExprPtrVec& args);
  AstUidExprOp uid() const { return AstUidExprOp::kApplyFunc; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
  inline FuncPtr func() const { return f; }

private:
  FuncPtr f;
}; // class ExprOpAppFunc

/******************************************************************************/
// Others
/******************************************************************************/

class ExprOpImply : public ExprOp {
public:
  ExprOpImply(const ExprPtr& ante, const ExprPtr& cons);
  AstUidExprOp uid() const { return AstUidExprOp::kImply; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpImply

class ExprOpIte : public ExprOp {
public:
  ExprOpIte(const ExprPtr& cnd, const ExprPtr& true_expr,
            const ExprPtr& false_expr);
  AstUidExprOp uid() const { return AstUidExprOp::kIfThenElse; }
  z3::expr GetZ3Expr(z3::context& ctx, const Z3ExprVec& expr_vec,
                     const std::string& suffix) const;
}; // class ExprOpIte

} // namespace ilang

#endif // ILANG_ILA_AST_EXPR_OP_H__