klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprBuilder.h
Go to the documentation of this file.
1 //===-- ExprBuilder.h -------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXPRBUILDER_H
11 #define KLEE_EXPRBUILDER_H
12 
13 #include "Expr.h"
14 
15 namespace klee {
17  class ExprBuilder {
18  protected:
19  ExprBuilder();
20 
21  public:
22  virtual ~ExprBuilder();
23 
24  // Expressions
25 
26  virtual ref<Expr> Constant(const llvm::APInt &Value) = 0;
27  virtual ref<Expr> NotOptimized(const ref<Expr> &Index) = 0;
28  virtual ref<Expr> Read(const UpdateList &Updates,
29  const ref<Expr> &Index) = 0;
30  virtual ref<Expr> Select(const ref<Expr> &Cond,
31  const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
32  virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
33  virtual ref<Expr> Extract(const ref<Expr> &LHS,
34  unsigned Offset, Expr::Width W) = 0;
35  virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) = 0;
36  virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) = 0;
37  virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
38  virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
39  virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
40  virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
41  virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
42  virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
43  virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
44  virtual ref<Expr> Not(const ref<Expr> &LHS) = 0;
45  virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
46  virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
47  virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
48  virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
49  virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
50  virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
51  virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
52  virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
53  virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
54  virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
55  virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
56  virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
57  virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
58  virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
59  virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
60  virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) = 0;
61 
62  // Utility functions
63 
65 
67 
68  ref<Expr> Constant(uint64_t Value, Expr::Width W) {
69  return Constant(llvm::APInt(W, Value));
70  }
71  };
72 
75  ExprBuilder *createDefaultExprBuilder();
76 
81  ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base);
82 
88  ExprBuilder *createSimplifyingExprBuilder(ExprBuilder *Base);
89 }
90 
91 #endif
virtual ref< Expr > Ule(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > AShr(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ExprBuilder * createSimplifyingExprBuilder(ExprBuilder *Base)
virtual ref< Expr > Select(const ref< Expr > &Cond, const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ExprBuilder * createDefaultExprBuilder()
virtual ref< Expr > SExt(const ref< Expr > &LHS, Expr::Width W)=0
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
virtual ref< Expr > Add(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ~ExprBuilder()
Definition: ExprBuilder.cpp:17
virtual ref< Expr > LShr(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 > Mul(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
Class representing a complete list of updates into an array.
Definition: Expr.h:655
virtual ref< Expr > Concat(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Sge(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 > Sle(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 > URem(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 > SDiv(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 > Sgt(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Not(const ref< Expr > &LHS)=0
virtual ref< Expr > SRem(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
virtual ref< Expr > Uge(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Ne(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
virtual ref< Expr > Constant(const llvm::APInt &Value)=0
virtual ref< Expr > And(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ref< Expr > Constant(uint64_t Value, Expr::Width W)
Definition: ExprBuilder.h:68
virtual ref< Expr > Extract(const ref< Expr > &LHS, unsigned Offset, Expr::Width W)=0
virtual ref< Expr > NotOptimized(const ref< Expr > &Index)=0
virtual ref< Expr > UDiv(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ref< Expr > True()
Definition: ExprBuilder.h:66
static const Width Bool
Definition: Expr.h:97
ref< Expr > False()
Definition: ExprBuilder.h:64
ExprBuilder * createConstantFoldingExprBuilder(ExprBuilder *Base)
virtual ref< Expr > ZExt(const ref< Expr > &LHS, Expr::Width W)=0
virtual ref< Expr > Xor(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 > Or(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Read(const UpdateList &Updates, const ref< Expr > &Index)=0