diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-10-18 14:22:26 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-23 18:53:46 +0300 |
commit | 6f8acb87b332d77d76ad81d56ab7bcf1125afcf3 (patch) | |
tree | 6e1b8a9a9ac6f17035089c2927c6faced766e37e /lib | |
parent | bcd0cf245e9638a5f39c9340a28313dc6a3814c4 (diff) | |
download | klee-6f8acb87b332d77d76ad81d56ab7bcf1125afcf3.tar.gz |
Move unrelated function from ReadExpr class
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 45 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 41 |
2 files changed, 43 insertions, 43 deletions
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); |