Hi,
I'm using klee on x86_64 and encountered an overflow bug in
Solver::getRange(). The binary search fails if lo+hi is greater than
(2^64 -1). The sum overflows and doesn't allow the loop to terminate.
This bug was encountered when klee hit a memory out-of-bound error.
A fix is below.
Best,
Robby Cochran
===================================================================
--- lib/Solver/Solver.cpp (revision 79356)
+++ lib/Solver/Solver.cpp (working copy)
@@ -164,7 +164,7 @@
// binary search for # of useful bits
uint64_t lo=0, hi=width, mid, bits=0;
while (lo<hi) {
- mid = (lo+hi)/2;
+ mid = lo + (hi - lo)/2;
bool res;
bool success =
mustBeTrue(query.withExpr(
@@ -205,7 +205,7 @@
// binary search for min
lo=0, hi=bits64::maxValueOfNBits(bits);
while (lo<hi) {
- mid = (lo+hi)/2;
+ mid = lo + (hi - lo)/2;
bool res = false;
bool success =
mayBeTrue(query.withExpr(UleExpr::create(e,
@@ -229,7 +229,8 @@
// binary search for max
lo=min, hi=bits64::maxValueOfNBits(bits);
while (lo<hi) {
- mid = (lo+hi)/2;
+ mid = lo + (hi - lo)/2;
bool res;
bool success =
mustBeTrue(query.withExpr(UleExpr::create(e,
