Skip to content

feat: Reintroduce concrete store #197

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 25, 2024
Merged

feat: Reintroduce concrete store #197

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 18 additions & 33 deletions lib/Core/AddressSpace.cpp
View file
Open in desktop
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
Open in desktop
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
40 changes: 28 additions & 12 deletions lib/Core/Executor.cpp
View file
Open in desktop
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,31 @@ 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) {
addConstraint(state, EqExpr::create(ce, arg));
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, op) &&
!op.second->readOnly) {
auto *os = state.addressSpace.getWriteable(op.first, op.second);
os->flushToConcreteStore(model);
}
if (ExternalCalls == ExternalCallPolicy::All) {
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]);
if (ExternalCalls == ExternalCallPolicy::All) {
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 +5312,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 +5380,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 +5390,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
Loading