Skip to content

Commit

Permalink
[temp] Fix plist
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Sep 27, 2023
1 parent 7fd53da commit 12e2dff
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 14 deletions.
3 changes: 2 additions & 1 deletion lib/Core/ExecutionState.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,8 @@ ExecutionState::ExecutionState(const ExecutionState &state)
addressSpace(state.addressSpace), constraints(state.constraints),
targetForest(state.targetForest), pathOS(state.pathOS),
symPathOS(state.symPathOS), coveredLines(state.coveredLines),
symbolics(state.symbolics), resolvedPointers(state.resolvedPointers),
symbolics(std::make_shared<PList>(state.symbolics)),
resolvedPointers(state.resolvedPointers),
cexPreferences(state.cexPreferences), arrayNames(state.arrayNames),
steppedInstructions(state.steppedInstructions),
steppedMemoryInstructions(state.steppedMemoryInstructions),
Expand Down
35 changes: 22 additions & 13 deletions lib/Core/ExecutionState.h
Original file line number Diff line number Diff line change
Expand Up @@ -228,13 +228,22 @@ struct Symbolic {
};

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

public:
size_t size() const { return prev_len + curr.size(); }
[[nodiscard]] size_t size() const { return prev_len + values.size(); }
[[nodiscard]] size_t get_depth() const {
size_t depth = 1;
const PList* p = this;
while(p->prev) {
depth++;
p = p->prev.get();
}
return depth;
}

struct iterator {
const PList *curr;
Expand All @@ -256,16 +265,16 @@ struct PList {
iterator &operator++() {
++get;
if (get < curr->prev_len) {
return it->operator++();
it->operator++();
}
return *this;
}

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

const Symbolic &operator->() const { return **this; }
Expand All @@ -288,20 +297,19 @@ struct PList {
}

void emplace_back(const MemoryObject *mo, const Array *array, KType *type) {
curr.emplace_back(ref<const MemoryObject>(mo), array, type);
values.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) {
PList() : prev(nullptr), prev_len(0), values(){};
PList(std::shared_ptr<const PList> pr)
: prev_len(pr ? pr->size() : 0), values() {
while (pr && pr->values.empty()) {
pr = pr->prev;
}
if (pr && pr->size()) {
prev = pr;
prev_len = pr->size();
} else {
prev = nullptr;
prev_len = 0;
}
}
};
Expand Down Expand Up @@ -411,6 +419,7 @@ class ExecutionState {
//
// FIXME: Move to a shared list structure (not critical).
std::shared_ptr<PList> symbolics;
// std::list<Symbolic> symbolics;

/// @brief map from memory accesses to accessed objects and access offsets.
ExprHashMap<std::set<IDType>> resolvedPointers;
Expand Down

0 comments on commit 12e2dff

Please sign in to comment.