about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/util/ExprRangeEvaluator.h40
-rw-r--r--include/klee/util/Ref.h12
-rw-r--r--lib/Core/ImpliedValue.cpp20
-rw-r--r--lib/Expr/Constraints.cpp4
-rw-r--r--lib/Expr/Expr.cpp16
-rw-r--r--lib/Expr/ExprPPrinter.cpp2
-rw-r--r--lib/Solver/FastCexSolver.cpp20
-rw-r--r--lib/Solver/STPBuilder.cpp50
8 files changed, 76 insertions, 88 deletions
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index b40b9e02..c5637341 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -97,7 +97,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
 
   case Expr::Read: {
-    const ReadExpr *re = static_ref_cast<const ReadExpr>(e);
+    const ReadExpr *re = cast<ReadExpr>(e);
     T index = evaluate(re->index);
 
     assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read");
@@ -106,7 +106,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
   }
 
   case Expr::Select: {
-    const SelectExpr *se = static_ref_cast<const SelectExpr>(e);
+    const SelectExpr *se = cast<SelectExpr>(e);
     T cond = evaluate(se->cond);
       
     if (cond.mustEqual(1)) {
@@ -130,37 +130,37 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     // Arithmetic
 
   case Expr::Add: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).add(evaluate(be->right), width);
   }
   case Expr::Sub: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).sub(evaluate(be->right), width);
   }
   case Expr::Mul: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).mul(evaluate(be->right), width);
   }
   case Expr::UDiv: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).udiv(evaluate(be->right), width);
   }
   case Expr::SDiv: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).sdiv(evaluate(be->right), width);
   }
   case Expr::URem: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).urem(evaluate(be->right), width);
   }
   case Expr::SRem: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     unsigned width = be->left->getWidth();
     return evaluate(be->left).srem(evaluate(be->right), width);
   }
@@ -168,31 +168,31 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     // Binary
 
   case Expr::And: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     return evaluate(be->left).binaryAnd(evaluate(be->right));
   }
   case Expr::Or: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     return evaluate(be->left).binaryOr(evaluate(be->right));
   }
   case Expr::Xor: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     return evaluate(be->left).binaryXor(evaluate(be->right));
   }
   case Expr::Shl: {
-    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    BinaryExpr *be = cast<BinaryExpr>(e);
     //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).shl(evaluate(be->right), width);
     break;
   }
   case Expr::LShr: {
-    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    BinaryExpr *be = cast<BinaryExpr>(e);
     //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).lshr(evaluate(be->right), width);
     break;
   }
   case Expr::AShr: {
-    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    BinaryExpr *be = cast<BinaryExpr>(e);
     //    unsigned width = be->left->getWidth();
     //    return evaluate(be->left).ashr(evaluate(be->right), width);
     break;
@@ -201,7 +201,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     // Comparison
 
   case Expr::Eq: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
       
@@ -214,7 +214,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
   }
 
   case Expr::Ult: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
       
@@ -226,7 +226,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
   }
   case Expr::Ule: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
       
@@ -238,7 +238,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
   }
   case Expr::Slt: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
     unsigned bits = be->left->getWidth();
@@ -251,7 +251,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
   }
   case Expr::Sle: {
-    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    const BinaryExpr *be = cast<BinaryExpr>(e);
     T left = evaluate(be->left);
     T right = evaluate(be->right);
     unsigned bits = be->left->getWidth();
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index b56d5d6a..d1c2e56b 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -46,8 +46,6 @@ public:
   template<class U> friend class ref;
   template<class U> friend U* dyn_ref_cast(ref &src);
   template<class U> friend const U* dyn_ref_cast(const ref &src);
-  template<class U> friend U* static_ref_cast(ref &src);
-  template<class U> friend const U* static_ref_cast(const ref &src);
 
   // constructor from pointer
   ref(T *p) : ptr(p) {
@@ -133,16 +131,6 @@ const U* dyn_ref_cast(const ref<Expr> &src) {
   return dyn_cast<U>(src.ptr);
 }
 
-template<class U>
-U* static_ref_cast(ref<Expr> &src) {
-  return static_cast<U*>(src.ptr);
-}
-
-template<class U>
-const U* static_ref_cast(const ref<Expr> &src) {
-  return static_cast<const U*>(src.ptr);
-}
-
 } // end namespace klee
 
 namespace llvm {
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index d1037839..8ebc0aef 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -43,7 +43,7 @@ static void _getImpliedValue(ref<Expr> e,
     // under certain circumstances (all values known, known value
     // unique, or range known, max / min hit). Seems unlikely this
     // would work often enough to be worth the effort.
-    ReadExpr *re = static_ref_cast<ReadExpr>(e);
+    ReadExpr *re = cast<ReadExpr>(e);
     results.push_back(std::make_pair(re, 
                                      ConstantExpr::create(value, e->getWidth())));
     break;
@@ -51,7 +51,7 @@ static void _getImpliedValue(ref<Expr> e,
     
   case Expr::Select: {
     // not much to do, could improve with range analysis
-    SelectExpr *se = static_ref_cast<SelectExpr>(e);
+    SelectExpr *se = cast<SelectExpr>(e);
     
     if (se->trueExpr->isConstant()) {
       if (se->falseExpr->isConstant()) {
@@ -70,7 +70,7 @@ static void _getImpliedValue(ref<Expr> e,
   }
 
   case Expr::Concat: {
-    ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
+    ConcatExpr *ce = cast<ConcatExpr>(e);
     _getImpliedValue(ce->getKid(0), (value >> ce->getKid(1)->getWidth()) & ((1 << ce->getKid(0)->getWidth()) - 1), results);
     _getImpliedValue(ce->getKid(1), value & ((1 << ce->getKid(1)->getWidth()) - 1), results);
     break;
@@ -85,7 +85,7 @@ static void _getImpliedValue(ref<Expr> e,
 
   case Expr::ZExt: 
   case Expr::SExt: {
-    CastExpr *ce = static_ref_cast<CastExpr>(e);
+    CastExpr *ce = cast<CastExpr>(e);
     _getImpliedValue(ce->src, 
                      bits64::truncateToNBits(value, 
 					     ce->src->getWidth()),
@@ -96,7 +96,7 @@ static void _getImpliedValue(ref<Expr> e,
     // Arithmetic
 
   case Expr::Add: { // constants on left
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (be->left->isConstant()) {
       uint64_t nvalue = ints::sub(value,
                                   be->left->getConstantValue(),
@@ -106,7 +106,7 @@ static void _getImpliedValue(ref<Expr> e,
     break;
   }
   case Expr::Sub: { // constants on left
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (be->left->isConstant()) {
       uint64_t nvalue = ints::sub(be->left->getConstantValue(),
                                   value,
@@ -131,7 +131,7 @@ static void _getImpliedValue(ref<Expr> e,
     // Binary
 
   case Expr::And: {
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (be->getWidth() == Expr::Bool) {
       if (value) {
         _getImpliedValue(be->left, value, results);
@@ -145,7 +145,7 @@ static void _getImpliedValue(ref<Expr> e,
     break;
   }
   case Expr::Or: {
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (!value) {
       _getImpliedValue(be->left, 0, results);
       _getImpliedValue(be->right, 0, results);
@@ -155,7 +155,7 @@ static void _getImpliedValue(ref<Expr> e,
     break;
   }
   case Expr::Xor: { // constants on left
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (be->left->isConstant()) {
       _getImpliedValue(be->right, value ^ be->left->getConstantValue(), results);
     }
@@ -167,7 +167,7 @@ static void _getImpliedValue(ref<Expr> e,
     value = !value;
     /* fallthru */
   case Expr::Eq: {
-    EqExpr *ee = static_ref_cast<EqExpr>(e);
+    EqExpr *ee = cast<EqExpr>(e);
     if (value) {
       if (ee->left->isConstant())
         _getImpliedValue(ee->right, ee->left->getConstantValue(), results);
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 93384060..3fa58ffd 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -127,14 +127,14 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
     
     // split to enable finer grained independence and other optimizations
   case Expr::And: {
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     addConstraintInternal(be->left);
     addConstraintInternal(be->right);
     break;
   }
 
   case Expr::Eq: {
-    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    BinaryExpr *be = cast<BinaryExpr>(e);
     if (be->left->isConstant()) {
       ExprReplaceVisitor visitor(be->right, be->left);
       rewriteConstraints(visitor);
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 9a78f188..3d3b6dd7 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -439,8 +439,8 @@ ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
 
   // Merge contiguous Extracts
   if (l->getKind() == Expr::Extract && r->getKind() == Expr::Extract) {
-    const ExtractExpr* ee_left = static_ref_cast<ExtractExpr>(l);
-    const ExtractExpr* ee_right = static_ref_cast<ExtractExpr>(r);
+    const ExtractExpr* ee_left = cast<ExtractExpr>(l);
+    const ExtractExpr* ee_right = cast<ExtractExpr>(r);
     if (ee_left->expr == ee_right->expr &&
 	ee_right->offset + ee_right->width == ee_left->offset) {
       return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
@@ -985,7 +985,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
       // 0 != ...
       
       if (rk == Expr::Eq) {
-        const EqExpr *ree = static_ref_cast<EqExpr>(r);
+        const EqExpr *ree = cast<EqExpr>(r);
 
         // eliminate double negation
         if (ree->left->isConstant() &&
@@ -994,7 +994,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
           return ree->right;
         }
       } else if (rk == Expr::Or) {
-        const OrExpr *roe = static_ref_cast<OrExpr>(r);
+        const OrExpr *roe = cast<OrExpr>(r);
 
         // transform not(or(a,b)) to and(not a, not b)
         return AndExpr::create(Expr::createNot(roe->left),
@@ -1003,7 +1003,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     }
   } else if (rk == Expr::SExt) {
     // (sext(a,T)==c) == (a==c)
-    const SExtExpr *see = static_ref_cast<SExtExpr>(r);
+    const SExtExpr *see = cast<SExtExpr>(r);
     Expr::Width fromBits = see->src->getWidth();
     uint64_t trunc = bits64::truncateToNBits(value, fromBits);
 
@@ -1016,7 +1016,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     }
   } else if (rk == Expr::ZExt) {
     // (zext(a,T)==c) == (a==c)
-    const ZExtExpr *zee = static_ref_cast<ZExtExpr>(r);
+    const ZExtExpr *zee = cast<ZExtExpr>(r);
     Expr::Width fromBits = zee->src->getWidth();
     uint64_t trunc = bits64::truncateToNBits(value, fromBits);
     
@@ -1028,14 +1028,14 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
       return ConstantExpr::create(0, Expr::Bool);
     }
   } else if (rk==Expr::Add) {
-    const AddExpr *ae = static_ref_cast<AddExpr>(r);
+    const AddExpr *ae = cast<AddExpr>(r);
     if (ae->left->isConstant()) {
       // c0 = c1 + b => c0 - c1 = b
       return EqExpr_createPartialR(SubExpr::create(cl, ae->left),
                                    ae->right.get());
     }
   } else if (rk==Expr::Sub) {
-    const SubExpr *se = static_ref_cast<SubExpr>(r);
+    const SubExpr *se = cast<SubExpr>(r);
     if (se->left->isConstant()) {
       // c0 = c1 - b => c1 - c0 = b
       return EqExpr_createPartialR(SubExpr::create(se->left, cl),
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index e996b260..6be93c38 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -290,7 +290,7 @@ class PPrinter : public ExprPPrinter {
       return NULL;
     
     if (stride == -1)
-      return static_ref_cast<ReadExpr>(e.get());
+      return cast<ReadExpr>(e.get());
     else return base;
   }
 
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index ee46be4f..cc0068ca 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -410,7 +410,7 @@ public:
     case Expr::NotOptimized: break;
 
     case Expr::Read: {
-      ReadExpr *re = static_ref_cast<ReadExpr>(e);
+      ReadExpr *re = cast<ReadExpr>(e);
       const Array *array = re->updates.root;
       CexObjectData &cod = objectValues.find(array->id)->second;
 
@@ -435,7 +435,7 @@ public:
     }
 
     case Expr::Select: {
-      SelectExpr *se = static_ref_cast<SelectExpr>(e);
+      SelectExpr *se = cast<SelectExpr>(e);
       ValueRange cond = evalRangeForExpr(se->cond);
       if (cond.isFixed()) {
         if (cond.min()) {
@@ -482,7 +482,7 @@ public:
       // the extraction a byte at a time, then checking the evaluated
       // value, isolating for that range, and continuing.
     case Expr::Concat: {
-      ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
+      ConcatExpr *ce = cast<ConcatExpr>(e);
       if (ce->is2ByteConcat()) {
 	forceExprToRange(ce->getKid(0), range.extract( 8, 16));
 	forceExprToRange(ce->getKid(1), range.extract( 0,  8));
@@ -521,7 +521,7 @@ public:
       // For ZExt this simplifies to just intersection with the
       // possible input range.
     case Expr::ZExt: {
-      CastExpr *ce = static_ref_cast<CastExpr>(e);
+      CastExpr *ce = cast<CastExpr>(e);
       unsigned inBits = ce->src->getWidth();
       ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits)));
       forceExprToRange(ce->src, input);
@@ -530,7 +530,7 @@ public:
       // For SExt instead of doing the intersection we just take the output range
       // minus the impossible values. This is nicer since it is a single interval.
     case Expr::SExt: {
-      CastExpr *ce = static_ref_cast<CastExpr>(e);
+      CastExpr *ce = cast<CastExpr>(e);
       unsigned inBits = ce->src->getWidth();
       unsigned outBits = ce->width;
       ValueRange output = range.set_difference(ValueRange(1<<(inBits-1),
@@ -544,7 +544,7 @@ public:
       // Binary
 
     case Expr::And: {
-      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      BinaryExpr *be = cast<BinaryExpr>(e);
       if (be->getWidth()==Expr::Bool) {
         if (range.isFixed()) {
           ValueRange left = evalRangeForExpr(be->left);
@@ -575,7 +575,7 @@ public:
     }
 
     case Expr::Or: {
-      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      BinaryExpr *be = cast<BinaryExpr>(e);
       if (be->getWidth()==Expr::Bool) {
         if (range.isFixed()) {
           ValueRange left = evalRangeForExpr(be->left);
@@ -611,7 +611,7 @@ public:
       // Comparison
 
     case Expr::Eq: {
-      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      BinaryExpr *be = cast<BinaryExpr>(e);
       if (range.isFixed()) {
         if (be->left->isConstant()) {
           uint64_t value = be->left->getConstantValue();
@@ -637,7 +637,7 @@ public:
     }
 
     case Expr::Ult: {
-      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      BinaryExpr *be = cast<BinaryExpr>(e);
       
       // XXX heuristic / lossy, what order if conflict
 
@@ -668,7 +668,7 @@ public:
       break;
     }
     case Expr::Ule: {
-      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      BinaryExpr *be = cast<BinaryExpr>(e);
       
       // XXX heuristic / lossy, what order if conflict
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index d1f7360c..ee5b777b 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -464,12 +464,12 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     
   // Special
   case Expr::NotOptimized: {
-    NotOptimizedExpr *noe = static_ref_cast<NotOptimizedExpr>(e);
+    NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
     return construct(noe->src, width_out);
   }
 
   case Expr::Read: {
-    ReadExpr *re = static_ref_cast<ReadExpr>(e);
+    ReadExpr *re = cast<ReadExpr>(e);
     *width_out = 8;
     return vc_readExpr(vc,
                        getArrayForUpdate(re->updates.root, re->updates.head),
@@ -477,7 +477,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
     
   case Expr::Select: {
-    SelectExpr *se = static_ref_cast<SelectExpr>(e);
+    SelectExpr *se = cast<SelectExpr>(e);
     ExprHandle cond = construct(se->cond, 0);
     ExprHandle tExpr = construct(se->trueExpr, width_out);
     ExprHandle fExpr = construct(se->falseExpr, width_out);
@@ -485,7 +485,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Concat: {
-    ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
+    ConcatExpr *ce = cast<ConcatExpr>(e);
     unsigned numKids = ce->getNumKids();
     ExprHandle res = construct(ce->getKid(numKids-1), 0);
     for (int i=numKids-2; i>=0; i--) {
@@ -496,7 +496,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Extract: {
-    ExtractExpr *ee = static_ref_cast<ExtractExpr>(e);
+    ExtractExpr *ee = cast<ExtractExpr>(e);
     ExprHandle src = construct(ee->expr, width_out);    
     *width_out = ee->getWidth();
     if (*width_out==1) {
@@ -510,7 +510,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   case Expr::ZExt: {
     int srcWidth;
-    CastExpr *ce = static_ref_cast<CastExpr>(e);
+    CastExpr *ce = cast<CastExpr>(e);
     ExprHandle src = construct(ce->src, &srcWidth);
     *width_out = ce->getWidth();
     if (srcWidth==1) {
@@ -522,7 +522,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   case Expr::SExt: {
     int srcWidth;
-    CastExpr *ce = static_ref_cast<CastExpr>(e);
+    CastExpr *ce = cast<CastExpr>(e);
     ExprHandle src = construct(ce->src, &srcWidth);
     *width_out = ce->getWidth();
     if (srcWidth==1) {
@@ -535,7 +535,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     // Arithmetic
 
   case Expr::Add: {
-    AddExpr *ae = static_ref_cast<AddExpr>(e);
+    AddExpr *ae = cast<AddExpr>(e);
     ExprHandle left = construct(ae->left, width_out);
     ExprHandle right = construct(ae->right, width_out);
     assert(*width_out!=1 && "uncanonicalized add");
@@ -543,7 +543,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Sub: {
-    SubExpr *se = static_ref_cast<SubExpr>(e);
+    SubExpr *se = cast<SubExpr>(e);
     ExprHandle left = construct(se->left, width_out);
     ExprHandle right = construct(se->right, width_out);
     assert(*width_out!=1 && "uncanonicalized sub");
@@ -551,7 +551,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   } 
 
   case Expr::Mul: {
-    MulExpr *me = static_ref_cast<MulExpr>(e);
+    MulExpr *me = cast<MulExpr>(e);
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
@@ -565,7 +565,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::UDiv: {
-    UDivExpr *de = static_ref_cast<UDivExpr>(e);
+    UDivExpr *de = cast<UDivExpr>(e);
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized udiv");
     
@@ -587,7 +587,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::SDiv: {
-    SDivExpr *de = static_ref_cast<SDivExpr>(e);
+    SDivExpr *de = cast<SDivExpr>(e);
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
@@ -607,7 +607,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::URem: {
-    URemExpr *de = static_ref_cast<URemExpr>(e);
+    URemExpr *de = cast<URemExpr>(e);
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized urem");
     
@@ -643,7 +643,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::SRem: {
-    SRemExpr *de = static_ref_cast<SRemExpr>(e);
+    SRemExpr *de = cast<SRemExpr>(e);
     ExprHandle left = construct(de->left, width_out);
     ExprHandle right = construct(de->right, width_out);
     assert(*width_out!=1 && "uncanonicalized srem");
@@ -671,7 +671,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     // Binary
 
   case Expr::And: {
-    AndExpr *ae = static_ref_cast<AndExpr>(e);
+    AndExpr *ae = cast<AndExpr>(e);
     ExprHandle left = construct(ae->left, width_out);
     ExprHandle right = construct(ae->right, width_out);
     if (*width_out==1) {
@@ -681,7 +681,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     }
   }
   case Expr::Or: {
-    OrExpr *oe = static_ref_cast<OrExpr>(e);
+    OrExpr *oe = cast<OrExpr>(e);
     ExprHandle left = construct(oe->left, width_out);
     ExprHandle right = construct(oe->right, width_out);
     if (*width_out==1) {
@@ -692,7 +692,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Xor: {
-    XorExpr *xe = static_ref_cast<XorExpr>(e);
+    XorExpr *xe = cast<XorExpr>(e);
     ExprHandle left = construct(xe->left, width_out);
     ExprHandle right = construct(xe->right, width_out);
     
@@ -706,7 +706,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Shl: {
-    ShlExpr *se = static_ref_cast<ShlExpr>(e);
+    ShlExpr *se = cast<ShlExpr>(e);
     ExprHandle left = construct(se->left, width_out);
     assert(*width_out!=1 && "uncanonicalized shl");
 
@@ -720,7 +720,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::LShr: {
-    LShrExpr *lse = static_ref_cast<LShrExpr>(e);
+    LShrExpr *lse = cast<LShrExpr>(e);
     ExprHandle left = construct(lse->left, width_out);
     unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
@@ -735,7 +735,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::AShr: {
-    AShrExpr *ase = static_ref_cast<AShrExpr>(e);
+    AShrExpr *ase = cast<AShrExpr>(e);
     ExprHandle left = construct(ase->left, width_out);
     assert(*width_out!=1 && "uncanonicalized ashr");
     
@@ -753,7 +753,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     // Comparison
 
   case Expr::Eq: {
-    EqExpr *ee = static_ref_cast<EqExpr>(e);
+    EqExpr *ee = cast<EqExpr>(e);
     ExprHandle left = construct(ee->left, width_out);
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
@@ -770,7 +770,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Ult: {
-    UltExpr *ue = static_ref_cast<UltExpr>(e);
+    UltExpr *ue = cast<UltExpr>(e);
     ExprHandle left = construct(ue->left, width_out);
     ExprHandle right = construct(ue->right, width_out);
     assert(*width_out!=1 && "uncanonicalized ult");
@@ -779,7 +779,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Ule: {
-    UleExpr *ue = static_ref_cast<UleExpr>(e);
+    UleExpr *ue = cast<UleExpr>(e);
     ExprHandle left = construct(ue->left, width_out);
     ExprHandle right = construct(ue->right, width_out);
     assert(*width_out!=1 && "uncanonicalized ule");
@@ -788,7 +788,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Slt: {
-    SltExpr *se = static_ref_cast<SltExpr>(e);
+    SltExpr *se = cast<SltExpr>(e);
     ExprHandle left = construct(se->left, width_out);
     ExprHandle right = construct(se->right, width_out);
     assert(*width_out!=1 && "uncanonicalized slt");
@@ -797,7 +797,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
   }
 
   case Expr::Sle: {
-    SleExpr *se = static_ref_cast<SleExpr>(e);
+    SleExpr *se = cast<SleExpr>(e);
     ExprHandle left = construct(se->left, width_out);
     ExprHandle right = construct(se->right, width_out);
     assert(*width_out!=1 && "uncanonicalized sle");