diff options
| -rw-r--r-- | include/klee/Expr.h | 4 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 6 | ||||
| -rw-r--r-- | lib/Expr/ExprBuilder.cpp | 495 | ||||
| -rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 2 | ||||
| -rw-r--r-- | test/Expr/Parser/ConstantFolding.pc | 67 |
5 files changed, 511 insertions, 63 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 79a8ec6f..24a1cb2e 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -411,7 +411,6 @@ public: ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Not(); ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); @@ -422,6 +421,9 @@ public: ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS); ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS); + + ref<ConstantExpr> Neg(); + ref<ConstantExpr> Not(); }; diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 5ef71d8c..b6833f24 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -373,6 +373,12 @@ ref<ConstantExpr> ConstantExpr::Add(const ref<ConstantExpr> &RHS) { getWidth()); } +ref<ConstantExpr> ConstantExpr::Neg() { + return ConstantExpr::create(ints::sub(0, + getConstantValue(), getWidth()), + getWidth()); +} + ref<ConstantExpr> ConstantExpr::Sub(const ref<ConstantExpr> &RHS) { return ConstantExpr::create(ints::sub(getConstantValue(), RHS->getConstantValue(), getWidth()), diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp index 0445222d..d36614d6 100644 --- a/lib/Expr/ExprBuilder.cpp +++ b/lib/Expr/ExprBuilder.cpp @@ -147,21 +147,172 @@ namespace { } }; - class ConstantFoldingExprBuilder : public ExprBuilder { + /// ChainedBuilder - Helper class for construct specialized expression + /// builders, which implements (non-virtual) methods which forward to a base + /// expression builder, for all expressions. + class ChainedBuilder { + protected: + /// Builder - The builder that this specialized builder is contained + /// within. Provided for convenience to clients. + ExprBuilder *Builder; + + /// Base - The base builder class for constructing expressions. ExprBuilder *Base; public: - ConstantFoldingExprBuilder(ExprBuilder *_Base) : Base(_Base) {} - ~ConstantFoldingExprBuilder() { - delete Base; + ChainedBuilder(ExprBuilder *_Builder, ExprBuilder *_Base) + : Builder(_Builder), Base(_Base) {} + ~ChainedBuilder() { delete Base; } + + ref<Expr> Constant(uint64_t Value, Expr::Width W) { + return Base->Constant(Value, W); + } + + ref<Expr> NotOptimized(const ref<Expr> &Index) { + return Base->NotOptimized(Index); + } + + ref<Expr> Read(const UpdateList &Updates, + const ref<Expr> &Index) { + return Base->Read(Updates, Index); + } + + ref<Expr> Select(const ref<Expr> &Cond, + const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Select(Cond, LHS, RHS); + } + + ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Concat(LHS, RHS); + } + + ref<Expr> Extract(const ref<Expr> &LHS, + unsigned Offset, Expr::Width W) { + return Base->Extract(LHS, Offset, W); + } + + ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) { + return Base->ZExt(LHS, W); + } + + ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) { + return Base->SExt(LHS, W); + } + + ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Add(LHS, RHS); + } + + ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Sub(LHS, RHS); + } + + ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Mul(LHS, RHS); + } + + ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->UDiv(LHS, RHS); + } + + ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->SDiv(LHS, RHS); + } + + ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->URem(LHS, RHS); + } + + ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->SRem(LHS, RHS); + } + + ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->And(LHS, RHS); + } + + ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Or(LHS, RHS); + } + + ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Xor(LHS, RHS); + } + + ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Shl(LHS, RHS); + } + + ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->LShr(LHS, RHS); + } + + ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->AShr(LHS, RHS); + } + + ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Eq(LHS, RHS); + } + + ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Ne(LHS, RHS); + } + + ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Ult(LHS, RHS); + } + + ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Ule(LHS, RHS); + } + + ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Ugt(LHS, RHS); + } + + ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Uge(LHS, RHS); + } + + ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Slt(LHS, RHS); } + ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Sle(LHS, RHS); + } + + ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Sgt(LHS, RHS); + } + + ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) { + return Base->Sge(LHS, RHS); + } + }; + + /// ConstantSpecializedExprBuilder - A base expression builder class which + /// handles dispatching to a helper class, based on whether the arguments are + /// constant or not. + /// + /// The SpecializedBuilder template argument should be a helper class which + /// implements methods for all the expression construction functions. These + /// methods can be specialized to take [Non]ConstantExpr when desired. + template<typename SpecializedBuilder> + class ConstantSpecializedExprBuilder : public ExprBuilder { + SpecializedBuilder Builder; + + public: + ConstantSpecializedExprBuilder(ExprBuilder *Base) : Builder(this, Base) {} + ~ConstantSpecializedExprBuilder() {} + virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) { - return Base->Constant(Value, W); + return Builder.Constant(Value, W); } virtual ref<Expr> NotOptimized(const ref<Expr> &Index) { - return Base->NotOptimized(Index); + return Builder.NotOptimized(Index); } virtual ref<Expr> Read(const UpdateList &Updates, @@ -170,8 +321,11 @@ namespace { const UpdateNode *UN = Updates.head; while (UN && Eq(Index, UN->index)->isFalse()) UN = UN->next; - - return Base->Read(UpdateList(Updates.root, UN), Index); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Index)) + return Builder.Read(UpdateList(Updates.root, UN), CE); + + return Builder.Read(UpdateList(Updates.root, UN), Index); } virtual ref<Expr> Select(const ref<Expr> &Cond, @@ -179,15 +333,20 @@ namespace { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Cond)) return CE->isTrue() ? LHS : RHS; - return Base->Select(Cond, LHS, RHS); + return Builder.Select(cast<NonConstantExpr>(Cond), LHS, RHS); } virtual ref<Expr> Concat(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Concat(RCE); + return Builder.Concat(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Concat(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Concat(LHS, RHS); + return Builder.Concat(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Extract(const ref<Expr> &LHS, @@ -195,214 +354,428 @@ namespace { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS)) return CE->Extract(Offset, W); - return Base->Extract(LHS, Offset, W); + return Builder.Extract(cast<NonConstantExpr>(LHS), Offset, W); } virtual ref<Expr> ZExt(const ref<Expr> &LHS, Expr::Width W) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS)) return CE->ZExt(W); - return Base->ZExt(LHS, W); + return Builder.ZExt(cast<NonConstantExpr>(LHS), W); } virtual ref<Expr> SExt(const ref<Expr> &LHS, Expr::Width W) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(LHS)) return CE->SExt(W); - return Base->SExt(LHS, W); + return Builder.SExt(cast<NonConstantExpr>(LHS), W); } virtual ref<Expr> Add(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Add(RCE); + return Builder.Add(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Add(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Add(LHS, RHS); + return Builder.Add(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Sub(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Sub(RCE); + return Builder.Sub(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Sub(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Sub(LHS, RHS); + return Builder.Sub(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Mul(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Mul(RCE); + return Builder.Mul(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Mul(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Mul(LHS, RHS); + return Builder.Mul(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> UDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->UDiv(RCE); + return Builder.UDiv(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.UDiv(cast<NonConstantExpr>(LHS), RCE); + } - return Base->UDiv(LHS, RHS); + return Builder.UDiv(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> SDiv(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->SDiv(RCE); + return Builder.SDiv(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.SDiv(cast<NonConstantExpr>(LHS), RCE); + } - return Base->SDiv(LHS, RHS); + return Builder.SDiv(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> URem(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->URem(RCE); + return Builder.URem(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.URem(cast<NonConstantExpr>(LHS), RCE); + } - return Base->URem(LHS, RHS); + return Builder.URem(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> SRem(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->SRem(RCE); + return Builder.SRem(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.SRem(cast<NonConstantExpr>(LHS), RCE); + } - return Base->SRem(LHS, RHS); + return Builder.SRem(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> And(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->And(RCE); + return Builder.And(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.And(cast<NonConstantExpr>(LHS), RCE); + } - return Base->And(LHS, RHS); + return Builder.And(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Or(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Or(RCE); + return Builder.Or(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Or(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Or(LHS, RHS); + return Builder.Or(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Xor(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Xor(RCE); + return Builder.Xor(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Xor(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Xor(LHS, RHS); + return Builder.Xor(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Shl(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Shl(RCE); + return Builder.Shl(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Shl(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Shl(LHS, RHS); + return Builder.Shl(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> LShr(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->LShr(RCE); + return Builder.LShr(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.LShr(cast<NonConstantExpr>(LHS), RCE); + } - return Base->LShr(LHS, RHS); + return Builder.LShr(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> AShr(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->AShr(RCE); + return Builder.AShr(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.AShr(cast<NonConstantExpr>(LHS), RCE); + } - return Base->AShr(LHS, RHS); + return Builder.AShr(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Eq(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Eq(RCE); + return Builder.Eq(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Eq(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Eq(LHS, RHS); + return Builder.Eq(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Ne(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Ne(RCE); + return Builder.Ne(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Ne(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Ne(LHS, RHS); + return Builder.Ne(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Ult(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Ult(RCE); + return Builder.Ult(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Ult(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Ult(LHS, RHS); + return Builder.Ult(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Ule(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Ule(RCE); + return Builder.Ule(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Ule(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Ule(LHS, RHS); + return Builder.Ule(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Ugt(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Ugt(RCE); + return Builder.Ugt(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Ugt(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Ugt(LHS, RHS); + return Builder.Ugt(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Uge(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Uge(RCE); + return Builder.Uge(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Uge(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Uge(LHS, RHS); + return Builder.Uge(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Slt(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Slt(RCE); + return Builder.Slt(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Slt(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Slt(LHS, RHS); + return Builder.Slt(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Sle(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Sle(RCE); + return Builder.Sle(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Sle(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Sle(LHS, RHS); + return Builder.Sle(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Sgt(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Sgt(RCE); + return Builder.Sgt(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Sgt(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Sgt(LHS, RHS); + return Builder.Sgt(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } virtual ref<Expr> Sge(const ref<Expr> &LHS, const ref<Expr> &RHS) { - if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) + if (ConstantExpr *LCE = dyn_cast<ConstantExpr>(LHS)) { if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) return LCE->Sge(RCE); + return Builder.Sge(LCE, cast<NonConstantExpr>(RHS)); + } else if (ConstantExpr *RCE = dyn_cast<ConstantExpr>(RHS)) { + return Builder.Sge(cast<NonConstantExpr>(LHS), RCE); + } - return Base->Sge(LHS, RHS); + return Builder.Sge(cast<NonConstantExpr>(LHS), + cast<NonConstantExpr>(RHS)); } }; + class ConstantFoldingBuilder : + public ChainedBuilder { + public: + ConstantFoldingBuilder(ExprBuilder *Builder, ExprBuilder *Base) + : ChainedBuilder(Builder, Base) {} + + ref<Expr> Add(const ref<ConstantExpr> &LHS, + const ref<NonConstantExpr> &RHS) { + // 0 + X ==> X + if (LHS->isZero()) + return RHS; + + switch (RHS->getKind()) { + default: break; + + case Expr::Add: { + BinaryExpr *BE = cast<BinaryExpr>(RHS); + // C_0 + (C_1 + X) ==> (C_0 + C1) + X + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left)) + return Builder->Add(LHS->Add(CE), BE->right); + // C_0 + (X + C_1) ==> (C_0 + C1) + X + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right)) + return Builder->Add(LHS->Add(CE), BE->left); + break; + } + + case Expr::Sub: { + BinaryExpr *BE = cast<BinaryExpr>(RHS); + // C_0 + (C_1 - X) ==> (C_0 + C1) - X + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left)) + return Builder->Sub(LHS->Add(CE), BE->right); + // C_0 + (X - C_1) ==> (C_0 - C1) + X + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right)) + return Builder->Add(LHS->Sub(CE), BE->left); + break; + } + } + + return Base->Add(LHS, RHS); + } + + ref<Expr> Add(const ref<NonConstantExpr> &LHS, + const ref<ConstantExpr> &RHS) { + return Add(RHS, LHS); + } + + ref<Expr> Add(const ref<NonConstantExpr> &LHS, + const ref<NonConstantExpr> &RHS) { + switch (LHS->getKind()) { + default: break; + + case Expr::Add: { + BinaryExpr *BE = cast<BinaryExpr>(LHS); + // (X + Y) + Z ==> X + (Y + Z) + return Builder->Add(BE->left, + Builder->Add(BE->right, RHS)); + } + + case Expr::Sub: { + BinaryExpr *BE = cast<BinaryExpr>(LHS); + // (X - Y) + Z ==> X + (Z - Y) + return Builder->Add(BE->left, + Builder->Sub(RHS, BE->right)); + } + } + + switch (RHS->getKind()) { + default: break; + + case Expr::Add: { + BinaryExpr *BE = cast<BinaryExpr>(RHS); + // X + (C_0 + Y) ==> C_0 + (X + Y) + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left)) + return Builder->Add(CE, Builder->Add(LHS, BE->right)); + // X + (Y + C_0) ==> C_0 + (X + Y) + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right)) + return Builder->Add(CE, Builder->Add(LHS, BE->left)); + break; + } + + case Expr::Sub: { + BinaryExpr *BE = cast<BinaryExpr>(RHS); + // X + (C_0 - Y) ==> C_0 + (X - Y) + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->left)) + return Builder->Add(CE, Builder->Sub(LHS, BE->right)); + // X + (Y - C_0) ==> -C_0 + (X + Y) + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(BE->right)) + return Builder->Add(CE->Neg(), Builder->Add(LHS, BE->left)); + break; + } + } + + return Base->Add(LHS, RHS); + } + }; + + typedef ConstantSpecializedExprBuilder<ConstantFoldingBuilder> + ConstantFoldingExprBuilder; + class SimplifyingExprBuilder : public ExprBuilder { ExprBuilder *Base; public: SimplifyingExprBuilder(ExprBuilder *_Base) : Base(_Base) {} - ~SimplifyingExprBuilder() { + ~SimplifyingExprBuilder() { delete Base; } diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index d7c77fb0..c78791ef 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -566,7 +566,7 @@ void ExprPPrinter::printQuery(std::ostream &os, // Print expressions to obtain values for, if any. if (evalExprsBegin != evalExprsEnd) { - PC.breakLine(indent - 1); + p.printSeparator(PC, q->isFalse(), indent-1); PC << '['; for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) { p.print(*it, PC); diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc index 6c345b47..9e4a981d 100644 --- a/test/Expr/Parser/ConstantFolding.pc +++ b/test/Expr/Parser/ConstantFolding.pc @@ -1,5 +1,72 @@ # RUN: %kleaver --builder=constant-folding -print-ast %s > %t +array a[64] : w32 -> w8 = symbolic + # RUN: grep -A 2 \"# Query 1\" %t > %t2 # RUN: grep \"(query .. false)\" %t2 (query [] (Not (Ult (w32 0) (w32 1)))) + +# Check -- 0 + X ==> X +# RUN: grep -A 2 \"# Query 2\" %t > %t2 +# RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2 +(query [] false [(Add w8 0 (Read w8 0 a))]) +# RUN: grep -A 2 \"# Query 3\" %t > %t2 +# RUN: grep \"(query .. false .(Read w8 0 a).)\" %t2 +(query [] false [(Add w8 (Read w8 0 a) 0)]) + +# Check -- C_0 + (C_1 + X) ==> (C_0 + C_1) + X +# RUN: grep -A 2 \"# Query 4\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2 +(query [] false [(Add w8 10 (Add w8 20 (Read w8 0 a)))]) + +# Check -- C_0 + (X + C_1) ==> (C_0 + C_1) + X +# RUN: grep -A 2 \"# Query 5\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 30 (Read w8 0 a)).)\" %t2 +(query [] false [(Add w8 10 (Add w8 (Read w8 0 a) 20))]) + +# Check -- C_0 + (C_1 - X) ==> (C_0 + C_1) - X +# RUN: grep -A 2 \"# Query 6\" %t > %t2 +# RUN: grep \"(query .. false .(Sub w8 30 (Read w8 0 a)).)\" %t2 +(query [] false [(Add w8 10 (Sub w8 20 (Read w8 0 a)))]) + +# Check -- C_0 + (X - C_1) ==> (C_0 - C_1) + X +# RUN: grep -A 2 \"# Query 7\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 246 (Read w8 0 a)).)\" %t2 +(query [] false [(Add w8 10 (Sub w8 (Read w8 0 a) 20))]) + +# Check -- (X + Y) + Z ==> X + (Y + Z) +# RUN: grep -A 3 \"# Query 8\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2 +# RUN: grep \"(Add w8 (Read w8 1 a) (Read w8 2 a)\" %t2 +(query [] false [(Add w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- (X - Y) + Z ==> X + (Z - Y) +# RUN: grep -A 3 \"# Query 9\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 (Read w8 0 a)\" %t2 +# RUN: grep \"(Sub w8 (Read w8 2 a) (Read w8 1 a)\" %t2 +(query [] false [(Add w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- X + (C + Y) ==> C + (X + Y) +# RUN: grep -A 3 \"# Query 10\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 10\" %t2 +# RUN: grep \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))]) + +# Check -- X + (Y + C) ==> C + (X + Y) +# RUN: grep -A 3 \"# Query 11\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 10\" %t2 +# RUN: grep \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))]) + +# Check -- X + (C - Y) ==> C + (X - Y) +# RUN: grep -A 3 \"# Query 12\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 10\" %t2 +# RUN: grep \"(Sub w8 (Read w8 0 a) (Read w8 1 a)\" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))]) + +# Check -- X + (Y - C) ==> -C + (X + Y) +# RUN: grep -A 3 \"# Query 13\" %t > %t2 +# RUN: grep \"(query .. false .(Add w8 246\" %t2 +# RUN: grep \"(Add w8 (Read w8 0 a) (Read w8 1 a)\" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))]) + |