From ff4e0374e27e43fa897f99726d33ab61e8bd2627 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Mon, 8 Jun 2009 05:53:15 +0000 Subject: Kill off Concat::is[248]ByteConcat, and fix FastCexSolver for this case. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73049 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Expr.h | 6 ------ lib/Solver/FastCexSolver.cpp | 25 ++++--------------------- 2 files changed, 4 insertions(+), 27 deletions(-) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index dd31896a..d1fdfa73 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -669,12 +669,6 @@ public: const ref &kid7, const ref &kid8); virtual ref rebuild(ref kids[]) const { return create(kids[0], kids[1]); } - - - /* These will be eliminated */ - bool is2ByteConcat() const { return false; } - bool is4ByteConcat() const { return false; } - bool is8ByteConcat() const { return false; } private: ConcatExpr(const ref &l, const ref &r) : left(l), right(r) { diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 1efeb0cb..882e0f28 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -504,27 +504,10 @@ public: // value, isolating for that range, and continuing. case Expr::Concat: { ConcatExpr *ce = cast(e); - if (ce->is2ByteConcat()) { - forceExprToRange(ce->getKid(0), range.extract( 8, 16)); - forceExprToRange(ce->getKid(1), range.extract( 0, 8)); - } - else if (ce->is4ByteConcat()) { - forceExprToRange(ce->getKid(0), range.extract(24, 32)); - forceExprToRange(ce->getKid(1), range.extract(16, 24)); - forceExprToRange(ce->getKid(2), range.extract( 8, 16)); - forceExprToRange(ce->getKid(3), range.extract( 0, 8)); - } - else if (ce->is8ByteConcat()) { - forceExprToRange(ce->getKid(0), range.extract(56, 64)); - forceExprToRange(ce->getKid(1), range.extract(48, 56)); - forceExprToRange(ce->getKid(2), range.extract(40, 48)); - forceExprToRange(ce->getKid(3), range.extract(32, 40)); - forceExprToRange(ce->getKid(4), range.extract(24, 32)); - forceExprToRange(ce->getKid(5), range.extract(16, 24)); - forceExprToRange(ce->getKid(6), range.extract( 8, 16)); - forceExprToRange(ce->getKid(7), range.extract( 0, 8)); - } - + Expr::Width LSBWidth = ce->getKid(1)->getWidth(); + Expr::Width MSBWidth = ce->getKid(1)->getWidth(); + forceExprToRange(ce->getKid(0), range.extract(LSBWidth, MSBWidth)); + forceExprToRange(ce->getKid(1), range.extract(0, LSBWidth)); break; } -- cgit 1.4.1