aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Expr/ExprBuilder.cpp145
1 files changed, 21 insertions, 124 deletions
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index 0c8ce06e..098da6ea 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -854,142 +854,39 @@ namespace {
typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder>
ConstantFoldingExprBuilder;
- class SimplifyingExprBuilder : public ExprBuilder {
- ExprBuilder *Base;
-
+ class SimplifyingBuilder : public ChainedBuilder {
public:
- SimplifyingExprBuilder(ExprBuilder *_Base) : Base(_Base) {}
- ~SimplifyingExprBuilder() {
- delete Base;
- }
-
- virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) {
- return Base->Constant(Value, W);
- }
-
- virtual ref<Expr> NotOptimized(const ref<Expr> &Index) {
- return Base->NotOptimized(Index);
- }
-
- virtual ref<Expr> Read(const UpdateList &Updates,
- const ref<Expr> &Index) {
- return Base->Read(Updates, Index);
- }
-
- virtual ref<Expr> Select(const ref<Expr> &Cond,
- const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Select(Cond, LHS, RHS);
- }
-
- virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Concat(LHS, RHS);
- }
-
- virtual ref<Expr> Extract(const ref<Expr> &LHS,
- unsigned Offset, Expr::Width W) {
- return Base->Extract(LHS, Offset, W);
- }
-
- virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) {
- return Base->ZExt(LHS, W);
- }
-
- virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) {
- return Base->SExt(LHS, W);
- }
-
- virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Add(LHS, RHS);
- }
-
- virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Sub(LHS, RHS);
- }
-
- virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Mul(LHS, RHS);
- }
-
- virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->UDiv(LHS, RHS);
- }
-
- virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->SDiv(LHS, RHS);
- }
-
- virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->URem(LHS, RHS);
- }
-
- virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->SRem(LHS, RHS);
- }
-
- virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->And(LHS, RHS);
- }
-
- virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Or(LHS, RHS);
- }
-
- virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Xor(LHS, RHS);
- }
-
- virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Shl(LHS, RHS);
- }
-
- virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->LShr(LHS, RHS);
- }
-
- virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->AShr(LHS, RHS);
- }
-
- virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Eq(LHS, RHS);
- }
-
- virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Ne(LHS, RHS);
- }
-
- virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Ult(LHS, RHS);
- }
-
- virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Ule(LHS, RHS);
- }
-
- virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Ugt(LHS, RHS);
- }
+ SimplifyingBuilder(ExprBuilder *Builder, ExprBuilder *Base)
+ : ChainedBuilder(Builder, Base) {}
- virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Uge(LHS, RHS);
+ ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+ // X != Y ==> !(X == Y)
+ return Builder->Not(Builder->Eq(LHS, RHS));
}
- virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Slt(LHS, RHS);
+ ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+ // X u> Y ==> Y u< X
+ return Builder->Ult(RHS, LHS);
}
- virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Sle(LHS, RHS);
+ ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+ // X u>= Y ==> Y u<= X
+ return Builder->Ule(RHS, LHS);
}
- virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Sgt(LHS, RHS);
+ ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+ // X s> Y ==> Y s< X
+ return Builder->Slt(RHS, LHS);
}
- virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
- return Base->Sge(LHS, RHS);
+ ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) {
+ // X s>= Y ==> Y s<= X
+ return Builder->Sle(RHS, LHS);
}
};
+
+ typedef ConstantSpecializedExprBuilder<SimplifyingBuilder>
+ SimplifyingExprBuilder;
}
ExprBuilder *klee::createDefaultExprBuilder() {