Skip to content

Commit

Permalink
[wip] Add persistent list workaround
Browse files Browse the repository at this point in the history
  • Loading branch information
@ladisgin
ladisgin committed Aug 28, 2023
1 parent f68d97e commit 915e90a
Show file tree
Hide file tree
Showing 4 changed files with 121 additions and 31 deletions.
3 changes: 3 additions & 0 deletions CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,9 @@ else()
message(STATUS "TCMalloc support disabled")
endif()


list(APPEND KLEE_COMPONENT_CXX_FLAGS "-gdwarf-4")

################################################################################
# Detect SQLite3
################################################################################
Expand Down
17 changes: 8 additions & 9 deletions lib/Core/ExecutionState.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ InfoStackFrame::InfoStackFrame(const InfoStackFrame &s)
/***/
ExecutionState::ExecutionState()
: initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1),
depth(0), ptreeNode(nullptr), steppedInstructions(0),
depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
steppedMemoryInstructions(0), instsSinceCovNew(0),
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
forkDisabled(false), prevHistory_(TargetsHistory::create()),
Expand All @@ -133,7 +133,7 @@ ExecutionState::ExecutionState()

ExecutionState::ExecutionState(KFunction *kf)
: initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
depth(0), ptreeNode(nullptr), steppedInstructions(0),
depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
steppedMemoryInstructions(0), instsSinceCovNew(0),
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
forkDisabled(false), prevHistory_(TargetsHistory::create()),
Expand All @@ -144,7 +144,7 @@ ExecutionState::ExecutionState(KFunction *kf)

ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
: initPC(kb->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1),
depth(0), ptreeNode(nullptr), steppedInstructions(0),
depth(0), ptreeNode(nullptr), symbolics(std::make_shared<PList>()), steppedInstructions(0),
steppedMemoryInstructions(0), instsSinceCovNew(0),
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false),
forkDisabled(false), prevHistory_(TargetsHistory::create()),
Expand Down Expand Up @@ -194,8 +194,8 @@ ExecutionState *ExecutionState::branch() {
}

bool ExecutionState::inSymbolics(const MemoryObject *mo) const {
for (auto i : symbolics) {
if (mo->id == i.memoryObject->id) {
for (auto &symbolic : *symbolics) {
if (mo->id == symbolic.memoryObject->id) {
return true;
}
}
Expand Down Expand Up @@ -255,13 +255,12 @@ void ExecutionState::popFrame() {

void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array,
KType *type) {
symbolics.emplace_back(ref<const MemoryObject>(mo), array, type);
symbolics->emplace_back(mo, array, type);
}

ref<const MemoryObject>
ExecutionState::findMemoryObject(const Array *array) const {
for (unsigned i = 0; i != symbolics.size(); ++i) {
const auto &symbolic = symbolics[i];
for (const auto &symbolic : *symbolics) {
if (array == symbolic.array) {
return symbolic.memoryObject;
}
Expand Down Expand Up @@ -368,7 +367,7 @@ bool ExecutionState::resolveOnSymbolics(const ref<ConstantExpr> &addr,
IDType &result) const {
uint64_t address = addr->getZExtValue();

for (const auto &res : symbolics) {
for (const auto &res : *symbolics) {
const auto &mo = res.memoryObject;
// Check if the provided address is between start and end of the object
// [mo->address, mo->address + mo->size) or the object is a 0-sized object.
Expand Down
83 changes: 82 additions & 1 deletion lib/Core/ExecutionState.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ DISABLE_WARNING_POP
#include <utility>
#include <vector>

#include <list>

namespace klee {
class Array;
class CallPathNode;
Expand Down Expand Up @@ -223,6 +225,85 @@ struct Symbolic {
}
};

struct PList {
private:
std::shared_ptr<const PList> prev;
size_t prev_len;
std::vector<Symbolic> curr;

public:
size_t size() const { return prev_len + curr.size(); }

struct iterator {
const PList *curr;
std::unique_ptr<iterator> it;
size_t get;

public:
explicit iterator(const PList *p) : curr(p), it(nullptr), get(0) {
if (curr->prev.get()) {
it = std::make_unique<iterator>(curr->prev.get());
}
}

bool operator==(const iterator &b) const {
return curr == b.curr && get == b.get;
}
bool operator!=(const iterator &b) const { return !(*this == b); }

iterator &operator++() {
++get;
if (get < curr->prev_len) {
return it->operator++();
}
return *this;
}

const Symbolic &operator*() const {
if (get < curr->prev_len) {
return it->operator*();
}
return curr->curr[get - curr->prev_len];
}

const Symbolic &operator->() const { return **this; }
};

[[nodiscard]] iterator begin() const { return iterator(this); }

[[nodiscard]] iterator end() const {
auto it = iterator(this);
it.get = size();
return it;
}

[[nodiscard]] iterator begin() { return iterator(this); }

[[nodiscard]] iterator end() {
auto it = iterator(this);
it.get = size();
return it;
}

void emplace_back(const MemoryObject *mo, const Array *array, KType *type) {
curr.emplace_back(ref<const MemoryObject>(mo), array, type);
}

PList() : prev(nullptr), prev_len(0), curr(){};
PList(std::shared_ptr<const PList> pr) : curr() {
while (pr && pr->prev && pr->prev_len == pr->prev->prev_len) {
pr = pr->prev;
}
if (pr && pr->size()) {
prev = pr;
prev_len = pr->size();
} else {
prev = nullptr;
prev_len = 0;
}
}
};

struct MemorySubobject {
ref<Expr> address;
unsigned size;
Expand Down Expand Up @@ -326,7 +407,7 @@ class ExecutionState {
/// @brief Ordered list of symbolics: used to generate test cases.
//
// FIXME: Move to a shared list structure (not critical).
std::vector<Symbolic> symbolics;
std::shared_ptr<PList> symbolics;

/// @brief map from memory accesses to accessed objects and access offsets.
ExprHashMap<std::set<IDType>> resolvedPointers;
Expand Down
49 changes: 28 additions & 21 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6900,10 +6900,10 @@ void Executor::logState(const ExecutionState &state, int id,
*f << "Address memory object: " << object.first->address << "\n";
*f << "Memory object size: " << object.first->size << "\n";
}
*f << state.symbolics.size() << " symbolics total. "
*f << state.symbolics->size() << " symbolics total. "
<< "Symbolics:\n";
size_t sc = 0;
for (auto &symbolic : state.symbolics) {
for (auto &symbolic : *state.symbolics) {
*f << "Symbolic number " << sc++ << "\n";
*f << "Associated memory object: " << symbolic.memoryObject.get()->id
<< "\n";
Expand All @@ -6924,12 +6924,12 @@ void Executor::setInitializationGraph(const ExecutionState &state,
ExprHashMap<std::pair<IDType, ref<Expr>>> resolvedPointers;

std::unordered_map<IDType, ref<const MemoryObject>> idToSymbolics;
for (const auto &symbolic : state.symbolics) {
for (const auto &symbolic : *state.symbolics) {
ref<const MemoryObject> mo = symbolic.memoryObject;
idToSymbolics[mo->id] = mo;
}

for (const auto &symbolic : state.symbolics) {
for (const auto &symbolic : *state.symbolics) {
KType *symbolicType = symbolic.type;
if (!symbolicType->getRawType()) {
continue;
Expand Down Expand Up @@ -6992,15 +6992,17 @@ void Executor::setInitializationGraph(const ExecutionState &state,
// The objects have to be symbolic
bool pointerFound = false, pointeeFound = false;
size_t pointerIndex = 0, pointeeIndex = 0;
for (size_t i = 0; i < state.symbolics.size(); i++) {
if (state.symbolics[i].memoryObject == pointerResolution.first) {
size_t i = 0;
for (auto &symbolic : *state.symbolics) {
if (symbolic.memoryObject == pointerResolution.first) {
pointerIndex = i;
pointerFound = true;
}
if (state.symbolics[i].memoryObject->id == pointer.second.first) {
if (symbolic.memoryObject->id == pointer.second.first) {
pointeeIndex = i;
pointeeFound = true;
}
++i;
}
if (pointerFound && pointeeFound) {
ref<ConstantExpr> offset = model.evaluate(pointerResolution.second);
Expand Down Expand Up @@ -7087,8 +7089,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {

std::vector<SparseStorage<unsigned char>> values;
std::vector<const Array *> objects;
for (unsigned i = 0; i != state.symbolics.size(); ++i)
objects.push_back(state.symbolics[i].array);
for (auto &symbolic : *state.symbolics) {
objects.push_back(symbolic.array);
}
bool success = solver->getInitialValues(extendedConstraints.cs(), objects,
values, state.queryMetaData);
solver->setTimeout(time::Span());
Expand All @@ -7099,19 +7102,23 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
return false;
}

res.objects = new KTestObject[state.symbolics.size()];
res.numObjects = state.symbolics.size();
res.numObjects = state.symbolics->size();
res.objects = new KTestObject[res.numObjects];

for (unsigned i = 0; i != state.symbolics.size(); ++i) {
auto mo = state.symbolics[i].memoryObject;
KTestObject *o = &res.objects[i];
o->name = const_cast<char *>(mo->name.c_str());
o->address = mo->address;
o->numBytes = values[i].size();
o->bytes = new unsigned char[o->numBytes];
std::copy(values[i].begin(), values[i].end(), o->bytes);
o->numPointers = 0;
o->pointers = nullptr;
{
size_t i = 0;
for (auto &symbolic : *state.symbolics) {
auto mo = symbolic.memoryObject;
KTestObject *o = &res.objects[i];
o->name = const_cast<char *>(mo->name.c_str());
o->address = mo->address;
o->numBytes = values[i].size();
o->bytes = new unsigned char[o->numBytes];
std::copy(values[i].begin(), values[i].end(), o->bytes);
o->numPointers = 0;
o->pointers = nullptr;
++i;
}
}

Assignment model = Assignment(objects, values, true);
Expand Down

0 comments on commit 915e90a

Please sign in to comment.