diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index d9e7bed4901..08dd4826684 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -38,7 +38,7 @@ namespace klee { typedef ImmutableMap SegmentMap; typedef std::map ConcreteAddressMap; typedef std::map SegmentAddressMap; - typedef std::map RemovedObjectsMap; + typedef std::map> RemovedObjectsMap; class AddressSpace { friend class ExecutionState; @@ -70,7 +70,8 @@ namespace klee { AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects), - segmentMap(b.segmentMap) { } + segmentMap(b.segmentMap), + removedObjectsMap(b.removedObjectsMap) { } ~AddressSpace() {} /// Looks up constant segment in concreteAddressMap. diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 6d75e354595..74d19277628 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2196,6 +2196,13 @@ ref Executor::getSizeForAlloca(ExecutionState& state, KInstruction *ki) co return size; } +static inline bool segmentIsDeleted(ExecutionState& state, + ref segment) { + auto& removedObjs = state.addressSpace.removedObjectsMap; + return removedObjs.find(segment->getZExtValue()) != removedObjs.end(); +} + + void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *i = ki->inst; switch (i->getOpcode()) { @@ -2763,88 +2770,80 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ICmpInst *ii = cast(ci); const auto& predicate = ii->getPredicate(); - const Cell &leftOriginal = eval(ki, 0, state); - const Cell &rightOriginal = eval(ki, 1, state); - - const auto leftSegment = - dyn_cast(leftOriginal.getSegment().get()); - const auto rightSegment = - dyn_cast(rightOriginal.getSegment().get()); - const auto leftValue = - dyn_cast(leftOriginal.getValue().get()); - const auto rightValue = - dyn_cast(rightOriginal.getValue().get()); - - ref leftArray; - ref rightArray; - - /// Only use symbolics with Constant values(offsets) - bool useOriginalValues = true; - - if (leftValue && rightValue && leftSegment && rightSegment) { - useOriginalValues = false; - } - - bool success = false; - bool deletedObject = false; - const auto &pointerWidth = Context::get().getPointerWidth(); + KValue left = eval(ki, 0, state); + KValue right = eval(ki, 1, state); - if (!useOriginalValues && - leftSegment->getWidth() == pointerWidth && - rightSegment->getWidth() == pointerWidth && - !leftSegment->isZero() && - !rightSegment->isZero() && - rightSegment->getZExtValue() != leftSegment->getZExtValue()) { + // is one of operands pointer and none of them is null? + if ((!left.getSegment()->isZero() || !right.getSegment()->isZero()) + && (!left.isZero() && !right.isZero())) { - ObjectPair op; - bool successRight, successLeft; - if (!state.addressSpace.resolveOneConstantSegment(leftOriginal, op)) { - successLeft = false; - const auto res = state.addressSpace.removedObjectsMap.find(leftSegment->getZExtValue(pointerWidth)); - if (res != state.addressSpace.removedObjectsMap.end()) { - leftArray = Expr::createTempRead(res->second, Context::get().getPointerWidth()); - } - } else { - successLeft = true; - leftArray = const_cast(op.first)->getSymbolicAddress( - arrayCache); + auto *leftSegment = dyn_cast(left.getSegment()); + auto *rightSegment = dyn_cast(right.getSegment()); + // for symbolic segments, we now support only the comparison for + // equality and inequality. In general, we will must fork. + if ((!leftSegment || !rightSegment) && + (predicate != ICmpInst::ICMP_EQ && + predicate != ICmpInst::ICMP_NE)) { + terminateStateOnExecError( + state, "Comparison other than (in)equality is not implemented" + "for symbolic pointers"); + break; } - if (!state.addressSpace.resolveOneConstantSegment(rightOriginal, op)) { - successRight = false; - const auto res = state.addressSpace.removedObjectsMap.find(rightSegment->getZExtValue(pointerWidth)); - if (res != state.addressSpace.removedObjectsMap.end()) { - rightArray = Expr::createTempRead(res->second, Context::get().getPointerWidth()); - } - } else { - successRight = true; - rightArray = const_cast(op.first)->getSymbolicAddress( - arrayCache); - } - success = successLeft && successRight; - deletedObject = successLeft == !successRight; - } - KValue left; - KValue right; + if (leftSegment && rightSegment) { + bool leftDeleted = segmentIsDeleted(state, leftSegment); + bool rightDeleted = segmentIsDeleted(state, rightSegment); + // some of the segments is deleted or + // the segments are different and are compared for less or greater + // (equal) to? + if (leftDeleted || rightDeleted || + ((leftSegment->getZExtValue() != rightSegment->getZExtValue()) && + (predicate != ICmpInst::ICMP_EQ && predicate != ICmpInst::ICMP_NE))) { + ObjectPair lookupResult; + // left is a pointer (and right is not a null, i.e., it is an integer + // value or another pointer) + if (!leftSegment->isZero()) { + bool success = state.addressSpace.resolveOneConstantSegment(left, lookupResult); + if (!success) { + auto& removedObjs = state.addressSpace.removedObjectsMap; + auto removedIt = removedObjs.find(leftSegment->getZExtValue()); + if (removedIt == removedObjs.end()) { + terminateStateOnExecError(state, + "Failed resolving constant segment"); + break; + } - if (!success && !deletedObject) { - left = static_cast(leftOriginal); - right = static_cast(rightOriginal); - } else { - klee_warning("Comparing pointers, using symbolic values instead of " - "segment for comparison"); - left = KValue(leftOriginal.getSegment(), leftArray); - right = KValue(rightOriginal.getSegment(), rightArray); - } + left = KValue(ConstantExpr::alloc(VALUES_SEGMENT, + leftSegment->getWidth()), + removedIt->second); + } else { + // FIXME: we should assert that the address does not overlap with any of the + // currently allocated objects... + left = KValue(ConstantExpr::alloc(VALUES_SEGMENT, leftSegment->getWidth()), + const_cast(lookupResult.first)->getSymbolicAddress(arrayCache)); + } + } + // right is a pointer (and left is not a null?) + if (!rightSegment->isZero()) { + bool success = state.addressSpace.resolveOneConstantSegment(right, lookupResult); + if (!success) { + auto& removedObjs = state.addressSpace.removedObjectsMap; + auto removedIt = removedObjs.find(rightSegment->getZExtValue()); + if (removedIt == removedObjs.end()) { + terminateStateOnExecError(state, + "Failed resolving constant segment"); + break; + } + right = KValue(ConstantExpr::alloc(VALUES_SEGMENT, + rightSegment->getWidth()), + removedIt->second); - if (deletedObject) { - switch(predicate) { - case ICmpInst::ICMP_EQ: - case ICmpInst::ICMP_NE: - bindLocal(ki, state, left.SymbCmp(right)); - return; - default: - break; + } else { + right = KValue(ConstantExpr::alloc(VALUES_SEGMENT, rightSegment->getWidth()), + const_cast(lookupResult.first)->getSymbolicAddress(arrayCache)); + } + } + } } } @@ -4606,8 +4605,8 @@ void Executor::executeFree(ExecutionState &state, StateTerminationType::Free, getKValueInfo(*it->second, addressOptim)); } else { - const_cast(mo)->initializeSymbolicArray(arrayCache); - it->second->addressSpace.removedObjectsMap.emplace(mo->segment, mo->symbolicAddress.getValue()); + it->second->addressSpace.removedObjectsMap.emplace( + mo->segment, const_cast(mo)->getSymbolicAddress(arrayCache)); it->second->addressSpace.unbindObject(mo); if (target) bindLocal(target, *it->second, KValue(Expr::createPointer(0))); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index dc98f3292b2..31063244173 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -72,7 +72,11 @@ void MemoryObject::getAllocInfo(std::string &result) const { void MemoryObject::initializeSymbolicArray(klee::ArrayCache &array) { if (!symbolicAddress) { - symbolicAddress = array.CreateArray(std::string("mo_addr_for_seg:") + std::to_string(segment), Context::get().getPointerWidth()); + auto tmparray = array.CreateArray(std::string("mo_addr_for_seg:") + + std::to_string(segment), + Context::get().getPointerWidth()); + symbolicAddress = Expr::createTempRead(tmparray, + Context::get().getPointerWidth()); } } @@ -80,8 +84,7 @@ ref MemoryObject::getSymbolicAddress(klee::ArrayCache &array) { if (!symbolicAddress) { initializeSymbolicArray(array); } - return Expr::createTempRead(symbolicAddress.getValue(), - Context::get().getPointerWidth()); + return symbolicAddress.getValue(); } /***/ diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index e8b4206826e..8a3b1529fa9 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -71,7 +71,7 @@ class MemoryObject { const llvm::Value *allocSite; /// Symbolic address for poiner comparison - llvm::Optional symbolicAddress; + llvm::Optional> symbolicAddress; // DO NOT IMPLEMENT MemoryObject(const MemoryObject &b);