about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/ExprBuilder.h79
1 files changed, 79 insertions, 0 deletions
diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h
new file mode 100644
index 00000000..e39da38c
--- /dev/null
+++ b/include/klee/ExprBuilder.h
@@ -0,0 +1,79 @@
+//===-- 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 {
+  /// ExprBuilder - Base expression builder class.
+  class ExprBuilder {
+  protected:
+    ExprBuilder();
+
+  public:
+    virtual ~ExprBuilder();
+
+    // Expressions
+
+    virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) = 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> 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;
+  };
+
+  /// createDefaultExprBuilder - Create an expression builder which does no
+  /// folding.
+  ExprBuilder *createDefaultExprBuilder();
+
+  /// createConstantFoldingExprBuilder - Create an expression builder which
+  /// folds constant expressions.
+  ///
+  /// Base - The base builder to use when constructing expressions.
+  ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base);
+
+  /// createFoldingExprBuilder - Create an expression builder which attemps to
+  /// fold redundant expressions and normalize expressions for improved caching.
+  ///
+  /// Base - The base builder to use when constructing expressions.
+  ExprBuilder *createFoldingExprBuilder(ExprBuilder *Base);
+}
+
+#endif