Skip to content

Commit

Permalink
feat: Reintroduce concrete store
Browse files Browse the repository at this point in the history
  • Loading branch information
@ocelaiwo
ocelaiwo committed Oct 23, 2024
1 parent e513fc3 commit fb08eb5
Show file tree
Hide file tree
Showing 5 changed files with 277 additions and 70 deletions.
51 changes: 18 additions & 33 deletions lib/Core/AddressSpace.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
#include "klee/Statistics/TimerStatIncrementer.h"

#include "CoreStats.h"
#include <cstring>

namespace klee {
llvm::cl::OptionCategory
Expand Down Expand Up @@ -384,15 +385,15 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
// transparently avoid screwing up symbolics (if the byte is symbolic
// then its concrete cache byte isn't being used) but is just a hack.

void AddressSpace::copyOutConcretes(const Assignment &assignment) {
void AddressSpace::copyOutConcretes() {
for (const auto &object : objects) {
auto &mo = object.first;
auto &os = object.second;
if (ref<ConstantExpr> sizeExpr =
dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
if (!mo->isUserSpecified && !os->readOnly &&
sizeExpr->getZExtValue() != 0) {
copyOutConcrete(mo, os.get(), assignment);
copyOutConcrete(mo, os.get());
}
}
}
Expand All @@ -407,27 +408,19 @@ ref<ConstantExpr> toConstantExpr(ref<Expr> expr) {
}

void AddressSpace::copyOutConcrete(const MemoryObject *mo,
const ObjectState *os,
const Assignment &assignment) const {
if (ref<ConstantExpr> addressExpr =
dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
auto address =
reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
AssignmentEvaluator evaluator(assignment, false);
if (ref<ConstantExpr> sizeExpr =
dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
size_t moSize = sizeExpr->getZExtValue();
std::vector<uint8_t> concreteStore(moSize);
for (size_t i = 0; i < moSize; i++) {
auto byte = evaluator.visit(os->readValue8(i));
concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(Expr::Int8);
}
std::memcpy(address, concreteStore.data(), moSize);
const ObjectState *os) const {

if (auto addressExpr = dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
if (auto sizeExpr = dyn_cast<ConstantExpr>(mo->getSizeExpr())) {
auto address =
reinterpret_cast<std::uint8_t *>(addressExpr->getZExtValue());
auto size = sizeExpr->getZExtValue();
std::memcpy(address, os->valueOS.concreteStore->data(), size);
}
}
}

bool AddressSpace::copyInConcretes(const Assignment &assignment) {
bool AddressSpace::copyInConcretes() {
for (auto &obj : objects) {
const MemoryObject *mo = obj.first;

Expand All @@ -436,8 +429,7 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {

if (ref<ConstantExpr> arrayConstantAddress =
dyn_cast<ConstantExpr>(mo->getBaseExpr())) {
if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue(),
assignment))
if (!copyInConcrete(mo, os.get(), arrayConstantAddress->getZExtValue()))
return false;
}
}
Expand All @@ -447,24 +439,17 @@ bool AddressSpace::copyInConcretes(const Assignment &assignment) {
}

bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os,
uint64_t src_address,
const Assignment &assignment) {
AssignmentEvaluator evaluator(assignment, false);
uint64_t src_address) {
auto address = reinterpret_cast<std::uint8_t *>(src_address);
size_t moSize =
cast<ConstantExpr>(evaluator.visit(mo->getSizeExpr()))->getZExtValue();
std::vector<uint8_t> concreteStore(moSize);
for (size_t i = 0; i < moSize; i++) {
auto byte = evaluator.visit(os->readValue8(i));
concreteStore[i] = cast<ConstantExpr>(byte)->getZExtValue(8);
}
if (memcmp(address, concreteStore.data(), moSize) != 0) {
size_t moSize = cast<ConstantExpr>(mo->getSizeExpr())->getZExtValue();

if (memcmp(address, os->valueOS.concreteStore->data(), moSize) != 0) {
if (os->readOnly) {
return false;
} else {
ObjectState *wos = getWriteable(mo, os);
for (size_t i = 0; i < moSize; i++) {
wos->write(i, ConstantExpr::create(address[i], Expr::Int8));
wos->write8(i, address[i]);
}
}
}
Expand Down
10 changes: 4 additions & 6 deletions lib/Core/AddressSpace.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@
#include "Memory.h"

#include "klee/ADT/ImmutableMap.h"
#include "klee/Expr/Assignment.h"
#include "klee/Expr/Expr.h"
#include "klee/System/Time.h"

Expand Down Expand Up @@ -139,10 +138,9 @@ class AddressSpace {
/// actual system memory location they were allocated at.
/// Returns the (hypothetical) number of pages needed provided each written
/// object occupies (at least) a single page.
void copyOutConcretes(const Assignment &assignment);
void copyOutConcretes();

void copyOutConcrete(const MemoryObject *mo, const ObjectState *os,
const Assignment &assignment) const;
void copyOutConcrete(const MemoryObject *mo, const ObjectState *os) const;

/// \brief Obtain an ObjectState suitable for writing.
///
Expand All @@ -164,7 +162,7 @@ class AddressSpace {
///
/// \retval true The copy succeeded.
/// \retval false The copy failed because a read-only object was modified.
bool copyInConcretes(const Assignment &assignment);
bool copyInConcretes();

/// Updates the memory object with the raw memory from the address
///
Expand All @@ -175,7 +173,7 @@ class AddressSpace {
/// externally
/// @return
bool copyInConcrete(const MemoryObject *mo, const ObjectState *os,
uint64_t src_address, const Assignment &assignment);
uint64_t src_address);
};
} // namespace klee

Expand Down
33 changes: 22 additions & 11 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1140,7 +1140,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
if (v.isConstant()) {
os->setReadOnly(true);
// initialise constant memory that may be used with external calls
state.addressSpace.copyOutConcrete(mo, os, {});
state.addressSpace.copyOutConcrete(mo, os);
}
}
}
Expand Down Expand Up @@ -5252,15 +5252,26 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
// uniqueness
ref<Expr> arg = *ai;
if (auto pointer = dyn_cast<PointerExpr>(arg)) {
arg = pointer->getValue();
}
arg = optimizer.optimizeExpr(arg, true);
ref<ConstantExpr> ce = evaluator.visit(arg);
ce->toMemory(&args[wordIndex]);
if (ExternalCalls == ExternalCallPolicy::All) {
ref<ConstantExpr> base = evaluator.visit(pointer->getBase());
ref<ConstantExpr> value = evaluator.visit(pointer->getValue());
value->toMemory(&args[wordIndex]);
ref<ConstantPointerExpr> const_pointer =
ConstantPointerExpr::create(base, value);
ObjectPair op;
if (state.addressSpace.resolveOne(const_pointer, nullptr, op) &&
!op.second->readOnly) {
auto *os = state.addressSpace.getWriteable(op.first, op.second);
os->flushToConcreteStore(model);
}
addConstraint(state, EqExpr::create(const_pointer->getValue(), arg));
wordIndex += (value->getWidth() + 63) / 64;
} else {
arg = optimizer.optimizeExpr(arg, true);
ref<ConstantExpr> ce = evaluator.visit(arg);
ce->toMemory(&args[wordIndex]);
addConstraint(state, EqExpr::create(ce, arg));
wordIndex += (ce->getWidth() + 63) / 64;
}
wordIndex += (ce->getWidth() + 63) / 64;
} else {
ref<Expr> arg = toUnique(state, *ai);
if (ConstantExpr *ce = dyn_cast<ConstantExpr>(arg)) {
Expand Down Expand Up @@ -5296,7 +5307,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
solver->getInitialValues(state.constraints.cs(), arrays, values,
state.queryMetaData);
Assignment assignment(arrays, values);
state.addressSpace.copyOutConcretes(assignment);
state.addressSpace.copyOutConcretes();
#ifndef WINDOWS
// Update external errno state with local state value
ObjectPair result;
Expand Down Expand Up @@ -5364,7 +5375,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
return;
}

if (!state.addressSpace.copyInConcretes(assignment)) {
if (!state.addressSpace.copyInConcretes()) {
terminateStateOnExecError(state, "external modified read-only object",
StateTerminationType::External);
return;
Expand All @@ -5374,7 +5385,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
// Update errno memory object with the errno value from the call
int error = externalDispatcher->getLastErrno();
state.addressSpace.copyInConcrete(result.first, result.second,
(uint64_t)&error, assignment);
(uint64_t)&error);
#endif

Type *resultType = target->inst()->getType();
Expand Down
Loading

0 comments on commit fb08eb5

Please sign in to comment.