Skip to content

Commit

Permalink
Fix comparison of pointers
Browse files Browse the repository at this point in the history 
This commit is a squash of the following commits changing the same piece of
code so that the tests still pass:

* Fix the comparison of object pointers

  We must use the symbolic address when we compare to a number.

  Fixes staticafi#12.

* Fix comparing to freed pointers

* Fix comparing pointers

* For pointers into the same memory object, compare their offsets,
  do not compare their symbolic addresses.

* Fix comparison of pointers to null

* Fix comparison of pointers for equality

  If we know the segments, we do not need to use the addresses
  (since we do not assume the inequality to other objects it would
  introduce false positives).

* Fix comparing freed pointers

* Freed pointers are usually concrete, so we must make them an exception
  in the code.

* Allow comparing symbolic pointers for (in)equality

  That can be derived without using symbolic addresses.

* Executor: fix handling freed pointers

  There was missing the "else" branch, so we overwrote
  the pointer in the case it was not resolved.

  Fixes staticafi/symbiotic#89
  • Loading branch information
@mchalupa @lzaoral
mchalupa authored and lzaoral committed Oct 4, 2022
1 parent 0301f18 commit 8d59086
Show file tree
Hide file tree
Showing 4 changed files with 87 additions and 84 deletions.
5 changes: 3 additions & 2 deletions lib/Core/AddressSpace.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ namespace klee {
typedef ImmutableMap<uint64_t, const MemoryObject*> SegmentMap;
typedef std::map</*address*/ const uint64_t, /*segment*/ const uint64_t> ConcreteAddressMap;
typedef std::map</*segment*/ const uint64_t, /*address*/ const uint64_t> SegmentAddressMap;
typedef std::map</*segment*/ const uint64_t, /*symbolic array*/ const Array*> RemovedObjectsMap;
typedef std::map</*segment*/ const uint64_t, /*symbolic array*/ ref<Expr>> RemovedObjectsMap;

class AddressSpace {
friend class ExecutionState;
Expand Down Expand Up @@ -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.
Expand Down
155 changes: 77 additions & 78 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2196,6 +2196,13 @@ ref<Expr> Executor::getSizeForAlloca(ExecutionState& state, KInstruction *ki) co
return size;
}

static inline bool segmentIsDeleted(ExecutionState& state,
ref<klee::ConstantExpr> 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()) {
Expand Down Expand Up @@ -2763,88 +2770,80 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
ICmpInst *ii = cast<ICmpInst>(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<ConstantExpr>(leftOriginal.getSegment().get());
const auto rightSegment =
dyn_cast<ConstantExpr>(rightOriginal.getSegment().get());
const auto leftValue =
dyn_cast<ConstantExpr>(leftOriginal.getValue().get());
const auto rightValue =
dyn_cast<ConstantExpr>(rightOriginal.getValue().get());

ref<Expr> leftArray;
ref<Expr> 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<MemoryObject *>(op.first)->getSymbolicAddress(
arrayCache);
auto *leftSegment = dyn_cast<ConstantExpr>(left.getSegment());
auto *rightSegment = dyn_cast<ConstantExpr>(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<MemoryObject *>(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<KValue>(leftOriginal);
right = static_cast<KValue>(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<MemoryObject*>(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<MemoryObject*>(lookupResult.first)->getSymbolicAddress(arrayCache));
}
}
}
}
}

Expand Down Expand Up @@ -4606,8 +4605,8 @@ void Executor::executeFree(ExecutionState &state,
StateTerminationType::Free,
getKValueInfo(*it->second, addressOptim));
} else {
const_cast<MemoryObject*>(mo)->initializeSymbolicArray(arrayCache);
it->second->addressSpace.removedObjectsMap.emplace(mo->segment, mo->symbolicAddress.getValue());
it->second->addressSpace.removedObjectsMap.emplace(
mo->segment, const_cast<MemoryObject*>(mo)->getSymbolicAddress(arrayCache));
it->second->addressSpace.unbindObject(mo);
if (target)
bindLocal(target, *it->second, KValue(Expr::createPointer(0)));
Expand Down
9 changes: 6 additions & 3 deletions lib/Core/Memory.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,16 +72,19 @@ 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());
}
}

ref<Expr> MemoryObject::getSymbolicAddress(klee::ArrayCache &array) {
if (!symbolicAddress) {
initializeSymbolicArray(array);
}
return Expr::createTempRead(symbolicAddress.getValue(),
Context::get().getPointerWidth());
return symbolicAddress.getValue();
}

/***/
Expand Down
2 changes: 1 addition & 1 deletion lib/Core/Memory.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ class MemoryObject {
const llvm::Value *allocSite;

/// Symbolic address for poiner comparison
llvm::Optional<const Array*> symbolicAddress;
llvm::Optional<ref<Expr>> symbolicAddress;

// DO NOT IMPLEMENT
MemoryObject(const MemoryObject &b);
Expand Down

0 comments on commit 8d59086

Please sign in to comment.