diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 18 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 4 | ||||
| -rw-r--r-- | lib/Core/Memory.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/SeedInfo.cpp | 22 | ||||
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 61 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 8 |
6 files changed, 66 insertions, 53 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2be099bd..a5ec8daa 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -438,7 +438,7 @@ void Executor::initializeGlobals(ExecutionState &state) { addr = Expr::createPointer(0); } else { addr = Expr::createPointer((unsigned long) (void*) f); - legalFunctions.insert(f); + legalFunctions.insert((uint64_t) (unsigned long) (void*) f); } globalAddresses.insert(std::make_pair(f, addr)); @@ -1554,14 +1554,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { (void) success; StatePair res = fork(*free, EqExpr::create(v, value), true); if (res.first) { - void *addr = (void*) (unsigned long) value->getConstantValue(); - std::set<void*>::iterator it = legalFunctions.find(addr); - if (it != legalFunctions.end()) { + uint64_t addr = value->getZExtValue(); + if (legalFunctions.count(addr)) { f = (Function*) addr; // Don't give warning on unique resolution if (res.second || !first) - klee_warning_once(addr, + klee_warning_once((void*) (unsigned long) addr, "resolved symbolic function pointer to: %s", f->getName().c_str()); @@ -2373,13 +2372,13 @@ std::string Executor::getAddressInfo(ExecutionState &state, info << "\taddress: " << address << "\n"; uint64_t example; if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) { - example = CE->getConstantValue(); + example = CE->getZExtValue(); } else { ref<ConstantExpr> value; bool success = solver->getValue(state, address, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; - example = value->getConstantValue(); + example = value->getZExtValue(); info << "\texample: " << example << "\n"; std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address); info << "\trange: [" << res.first << ", " << res.second <<"]\n"; @@ -2650,9 +2649,8 @@ void Executor::executeAlloc(ExecutionState &state, const ObjectState *reallocFrom) { size = toUnique(state, size); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) { - MemoryObject *mo = - memory->allocate(CE->getConstantValue(), isLocal, false, - state.prevPC->inst); + MemoryObject *mo = memory->allocate(CE->getZExtValue(), isLocal, false, + state.prevPC->inst); if (!mo) { bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType)); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 4dd89f2a..9cfcf627 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -135,8 +135,8 @@ private: std::map<const llvm::GlobalValue*, ref<Expr> > globalAddresses; /// The set of legal function addresses, used to validate function - /// pointers. - std::set<void*> legalFunctions; + /// pointers. We use the actual Function* address as the function address. + std::set<uint64_t> legalFunctions; /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 49198df8..05c226d3 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -430,7 +430,7 @@ void ObjectState::write8(ref<Expr> offset, ref<Expr> value) { ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) { - return read((unsigned) CE->getConstantValue(), width); + return read(CE->getZExtValue(32), width); } else { switch (width) { default: assert(0 && "invalid type"); @@ -619,7 +619,7 @@ ref<Expr> ObjectState::read64(ref<Expr> offset) const { void ObjectState::write(ref<Expr> offset, ref<Expr> value) { Expr::Width w = value->getWidth(); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) { - write(CE->getConstantValue(), value); + write(CE->getZExtValue(32), value); } else { switch(w) { case Expr::Bool: write1(offset, value); break; @@ -635,7 +635,7 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) { void ObjectState::write(unsigned offset, ref<Expr> value) { Expr::Width w = value->getWidth(); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { - uint64_t val = CE->getConstantValue(); + uint64_t val = CE->getZExtValue(); switch(w) { case Expr::Bool: case Expr::Int8: write8(offset, val); break; diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index dc3ff931..b540d271 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -79,7 +79,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, ReadExpr *re = it->get(); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) { directReads.insert(std::make_pair(re->updates.root, - (unsigned) CE->getConstantValue())); + (unsigned) CE->getZExtValue(32))); } } @@ -93,7 +93,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, // If not in bindings then this can't be a violation? Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array); if (it2 != assignment.bindings.end()) { - ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)); + ref<Expr> isSeed = EqExpr::create(read, + ConstantExpr::alloc(it2->second[i], + Expr::Int8)); bool res; bool success = solver->mustBeFalse(tmp, isSeed, res); assert(success && "FIXME: Unhandled solver failure"); @@ -103,8 +105,10 @@ void SeedInfo::patchSeed(const ExecutionState &state, bool success = solver->getValue(tmp, read, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; - it2->second[i] = value->getConstantValue(); - tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8))); + it2->second[i] = value->getZExtValue(8); + tmp.addConstraint(EqExpr::create(read, + ConstantExpr::alloc(it2->second[i], + Expr::Int8))); } else { tmp.addConstraint(isSeed); } @@ -126,7 +130,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, for (unsigned i=0; i<array->size; ++i) { ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); - ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)); + ref<Expr> isSeed = EqExpr::create(read, + ConstantExpr::alloc(it->second[i], + Expr::Int8)); bool res; bool success = solver->mustBeFalse(tmp, isSeed, res); assert(success && "FIXME: Unhandled solver failure"); @@ -136,8 +142,10 @@ void SeedInfo::patchSeed(const ExecutionState &state, bool success = solver->getValue(tmp, read, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; - it->second[i] = value->getConstantValue(); - tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8))); + it->second[i] = value->getZExtValue(8); + tmp.addConstraint(EqExpr::create(read, + ConstantExpr::alloc(it->second[i], + Expr::Int8))); } else { tmp.addConstraint(isSeed); } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 8c2fcfe6..e9f40a49 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -453,17 +453,19 @@ public: // FIXME: This is imprecise, we need to look through the existing writes // to see if this is an initial read or not. if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) { - if (CE->getConstantValue() < array->size) { + uint64_t index = CE->getZExtValue(); + + if (index < array->size) { // If the range is fixed, just set that; even if it conflicts with the // previous range it should be a better guess. if (range.isFixed()) { - cod.setPossibleValue(CE->getConstantValue(), range.min()); + cod.setPossibleValue(index, range.min()); } else { - CexValueData cvd = cod.getPossibleValues(CE->getConstantValue()); + CexValueData cvd = cod.getPossibleValues(index); CexValueData tmp = cvd.set_intersection(range); if (!tmp.isEmpty()) - cod.setPossibleValues(CE->getConstantValue(), tmp); + cod.setPossibleValues(index, tmp); } } } else { @@ -637,23 +639,26 @@ public: BinaryExpr *be = cast<BinaryExpr>(e); if (range.isFixed()) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) { - uint64_t value = CE->getConstantValue(); - if (range.min()) { - propogatePossibleValue(be->right, value); - } else { - if (value==0) { - propogatePossibleValues(be->right, - CexValueData(1, - ints::sext(1, - be->right->getWidth(), - 1))); + // FIXME: Handle large widths? + if (CE->getWidth() <= 64) { + uint64_t value = CE->getZExtValue(); + if (range.min()) { + propogatePossibleValue(be->right, value); } else { - // XXX heuristic / lossy, could be better to pick larger range? - propogatePossibleValues(be->right, CexValueData(0, value-1)); + CexValueData range; + if (value==0) { + range = CexValueData(1, + bits64::maxValueOfNBits(CE->getWidth())); + } else { + // FIXME: heuristic / lossy, could be better to pick larger + // range? + range = CexValueData(0, value - 1); + } + propogatePossibleValues(be->right, range); } + } else { + // XXX what now } - } else { - // XXX what now } } break; @@ -833,15 +838,17 @@ public: BinaryExpr *be = cast<BinaryExpr>(e); if (range.isFixed()) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) { - uint64_t value = CE->getConstantValue(); - if (range.min()) { - // If the equality is true, then propogate the value. - propogateExactValue(be->right, value); - } else { - // If the equality is false and the comparison is of booleans, then - // we can infer the value to propogate. - if (be->right->getWidth() == Expr::Bool) { - propogateExactValue(be->right, !value); + // FIXME: Handle large widths? + if (CE->getWidth() <= 64) { + uint64_t value = CE->getZExtValue(); + if (range.min()) { + // If the equality is true, then propogate the value. + propogateExactValue(be->right, value); + } else { + // If the equality is false and the comparison is of booleans, + // then we can infer the value to propogate. + if (be->right->getWidth() == Expr::Bool) + propogateExactValue(be->right, !value); } } } diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 3d6f789e..2c03c483 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -587,7 +587,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) { if (CE->getWidth() <= 64) { - uint64_t divisor = CE->getConstantValue(); + uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { return bvRightShift(left, @@ -629,7 +629,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) { if (CE->getWidth() <= 64) { - uint64_t divisor = CE->getConstantValue(); + uint64_t divisor = CE->getZExtValue(); if (bits64::isPowerOfTwo(divisor)) { unsigned bits = bits64::indexOfSingleBit(divisor); @@ -644,8 +644,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { } } - // Use fast division to compute modulo without explicit division for - // constant divisor. + // Use fast division to compute modulo without explicit division for + // constant divisor. if (optimizeDivides) { if (*width_out == 32) { //only works for 32-bit division |