diff options
-rw-r--r-- | include/klee/Expr.h | 2 | ||||
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 45 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 41 |
3 files changed, 43 insertions, 45 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 8eccdf11..212053b4 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -579,8 +579,6 @@ public: } static ref<Expr> create(const UpdateList &updates, ref<Expr> i); - static ref<Expr> extendRead(const UpdateList &updates, ref<Expr> i, - Expr::Width w); Width getWidth() const { assert(updates.root); return updates.root->getRange(); } Kind getKind() const { return Read; } diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 94bf2487..475b8b5c 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -54,6 +54,47 @@ llvm::cl::opt<double> ArrayValueSymbRatio( llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size")); }; +ref<Expr> extendRead(const UpdateList &ul, const ref<Expr> index, + Expr::Width w) { + switch (w) { + default: + assert(0 && "invalid width"); + case Expr::Int8: + return ReadExpr::alloc(ul, index); + case Expr::Int16: + return ConcatExpr::create( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + case Expr::Int32: + return ConcatExpr::create4( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + case Expr::Int64: + return ConcatExpr::create8( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + } +} + ref<Expr> ExprOptimizer::optimizeExpr(const ref<Expr> &e, bool valueOnly) { // Nothing to optimise for constant expressions if (isa<ConstantExpr>(e)) @@ -574,7 +615,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr( ref<Expr> firstIndex = MulExpr::create( ConstantExpr::create(holes[0], re->index->getWidth()), ConstantExpr::create(width / 8, re->index->getWidth())); - result = ReadExpr::extendRead(re->updates, firstIndex, width); + result = extendRead(re->updates, firstIndex, width); for (size_t i = 1; i < holes.size(); i++) { ref<Expr> temp_idx = MulExpr::create( ConstantExpr::create(holes[i], re->index->getWidth()), @@ -582,7 +623,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr( ref<Expr> cond = EqExpr::create( re->index, ConstantExpr::create(holes[i], re->index->getWidth())); ref<Expr> temp = SelectExpr::create( - cond, ReadExpr::extendRead(re->updates, temp_idx, width), result); + cond, extendRead(re->updates, temp_idx, width), result); result = temp; } } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 9e524f62..a5c7f652 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -81,47 +81,6 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) { } } -ref<Expr> ReadExpr::extendRead(const UpdateList &ul, const ref<Expr> index, - Expr::Width w) { - switch (w) { - default: - assert(0 && "invalid width"); - case Expr::Int8: - return ReadExpr::alloc(ul, index); - case Expr::Int16: - return ConcatExpr::create( - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), - ReadExpr::alloc(ul, index)); - case Expr::Int32: - return ConcatExpr::create4( - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), - ReadExpr::alloc(ul, index)); - case Expr::Int64: - return ConcatExpr::create8( - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), - ReadExpr::alloc( - ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), - ReadExpr::alloc(ul, index)); - } -} - int Expr::compare(const Expr &b) const { static ExprEquivSet equivs; int r = compare(b, equivs); |