ExprBuilder.h

Go to the documentation of this file.

//===-- ExprBuilder.h -------------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
 
#ifndef KLEE_EXPRBUILDER_H
#define KLEE_EXPRBUILDER_H
 
#include "Expr.h"
 
namespace klee {
  class ExprBuilder {
  protected:
    ExprBuilder();
 
  public:
    virtual ~ExprBuilder();
 
    // Expressions
 
    virtual ref<Expr> Constant(const llvm::APInt &Value) = 0;
    virtual ref<Expr> NotOptimized(const ref<Expr> &Index) = 0;
    virtual ref<Expr> Read(const UpdateList &Updates, 
                           const ref<Expr> &Index) = 0;
    virtual ref<Expr> Select(const ref<Expr> &Cond,
                             const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Extract(const ref<Expr> &LHS, 
                              unsigned Offset, Expr::Width W) = 0;
    virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) = 0;
    virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) = 0;
    virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Not(const ref<Expr> &LHS) = 0;
    virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
    virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
 
    // Utility functions
 
    ref<Expr> False() { return ConstantExpr::alloc(0, Expr::Bool); }
 
    ref<Expr> True() { return ConstantExpr::alloc(1, Expr::Bool); }
 
    ref<Expr> Constant(uint64_t Value, Expr::Width W) {
      return Constant(llvm::APInt(W, Value));
    }
  };
 
  ExprBuilder *createDefaultExprBuilder();
 
  ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base);
 
  ExprBuilder *createSimplifyingExprBuilder(ExprBuilder *Base);
}
 
#endif /* KLEE_EXPRBUILDER_H */