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

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<Expr> &kid7, const ref<Expr> &kid8);
   
   virtual ref<Expr> rebuild(ref<Expr> 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<Expr> &l, const ref<Expr> &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<ConcatExpr>(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;
     }