klee
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
15namespace klee {
18 protected:
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 /* KLEE_EXPRBUILDER_H */
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
virtual ref< Expr > Ule(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 > Xor(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ref< Expr > False()
Definition: ExprBuilder.h:64
virtual ref< Expr > Sle(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 > Or(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Not(const ref< Expr > &LHS)=0
virtual ref< Expr > ZExt(const ref< Expr > &LHS, Expr::Width W)=0
virtual ref< Expr > UDiv(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 > Extract(const ref< Expr > &LHS, unsigned Offset, Expr::Width W)=0
virtual ref< Expr > And(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 > LShr(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > SExt(const ref< Expr > &LHS, Expr::Width W)=0
virtual ref< Expr > Mul(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Select(const ref< Expr > &Cond, 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 > Ne(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 > SRem(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 > Shl(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 > SDiv(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ~ExprBuilder()
Definition: ExprBuilder.cpp:17
virtual ref< Expr > Ult(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ref< Expr > True()
Definition: ExprBuilder.h:66
virtual ref< Expr > Read(const UpdateList &Updates, const ref< Expr > &Index)=0
virtual ref< Expr > Ugt(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > NotOptimized(const ref< Expr > &Index)=0
virtual ref< Expr > Sgt(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
virtual ref< Expr > Constant(const llvm::APInt &Value)=0
virtual ref< Expr > Add(const ref< Expr > &LHS, const ref< Expr > &RHS)=0
ref< Expr > Constant(uint64_t Value, Expr::Width W)
Definition: ExprBuilder.h:68
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:97
static const Width Bool
Definition: Expr.h:100
Class representing a complete list of updates into an array.
Definition: Expr.h:539
Definition: main.cpp:291
ExprBuilder * createDefaultExprBuilder()
ExprBuilder * createConstantFoldingExprBuilder(ExprBuilder *Base)
ExprBuilder * createSimplifyingExprBuilder(ExprBuilder *Base)