Skip to content

Commit

Permalink
[wip] revert path to non-persistent list
Browse files Browse the repository at this point in the history
  • Loading branch information
ocelaiwo committed Sep 30, 2024
1 parent d7ee0a9 commit c43bb04
Show file tree
Hide file tree
Showing 4 changed files with 23 additions and 22 deletions.
33 changes: 17 additions & 16 deletions include/klee/Expr/Path.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,17 +7,16 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
#include "llvm/Support/raw_ostream.h"
DISABLE_WARNING_POP

#include "klee/ADT/ImmutableList.h"

#include <stack>
#include <string>
#include <vector>

namespace klee {
struct CallStackFrame;
struct KBlock;
struct KCallBlock;
struct KFunction;
struct KInstruction;
struct KCallBlock;
class KModule;

class Path {
Expand All @@ -32,10 +31,6 @@ class Path {
return block == other.block && kind == other.kind;
}

bool operator!=(const entry &other) const {
return !(*this == other);
}

bool operator<(const entry &other) const {
return block < other.block || (block == other.block && kind < other.kind);
}
Expand All @@ -44,13 +39,19 @@ class Path {
std::vector<entry> getSuccessors();
};

using path_ty = ImmutableList<entry>;
using path_ty = std::vector<entry>;

struct PathIndex {
unsigned long block;
unsigned long instruction;
bool operator==(const PathIndex &rhs) const {
return block == rhs.block && instruction == rhs.instruction;

bool operator==(const PathIndex &other) const {
return block == other.block && instruction == other.instruction;
}

bool operator<(const PathIndex &other) const {
return block < other.block ||
(block == other.block && instruction < other.instruction);
}
};

Expand Down Expand Up @@ -87,18 +88,18 @@ class Path {
(lhs.last == rhs.last && lhs.next < rhs.next)))));
}

unsigned KBlockSize() const;
bool empty() const { return path.empty(); }
bool emptyWithNext() const { return path.empty() && next; }

std::pair<bool, KCallBlock *> fromOutTransition() const;

unsigned KBlockSize() const { return path.size(); }
const path_ty &getBlocks() const;
unsigned getFirstIndex() const;
KInstruction *getFirstInstruction() const;
unsigned getLastIndex() const;
KInstruction *getLastInstruction() const;
KInstruction *getNext() const { return next; }
unsigned getLastIndex() const;

bool blockCompleted(unsigned index) const;
KFunction *getCalledFunction(unsigned index) const;
Expand All @@ -114,15 +115,15 @@ class Path {

static Path concat(const Path &l, const Path &r);

// static Path parse(const std::string &str, const KModule &km);

// For proof obligations
Path() = default;

// For execution states
explicit Path(KInstruction *next) : next(next) {}

Path(unsigned first, ImmutableList<entry> path, unsigned last,
Path(unsigned first, std::vector<entry> path, unsigned last,
KInstruction *next)
: first(first), last(last), path(path), next(next) {}
: first(first), last(last), path(path), next(next) {}

private:
// The path is stored as:
Expand Down
1 change: 1 addition & 0 deletions lib/Core/EventRecorder.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#define KLEE_EVENT_RECORDER_H

#include "klee/Expr/Path.h"
#include <klee/ADT/ImmutableList.h>

namespace klee {

Expand Down
2 changes: 1 addition & 1 deletion lib/Expr/Parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -471,7 +471,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
Path ParserImpl::ParsePathDecl() {
unsigned first = 0;
unsigned last = 0;
ImmutableList<Path::entry> blocks;
std::vector<Path::entry> blocks;
KInstruction *next = nullptr;

ConsumeExpectedToken(Token::KWPath);
Expand Down
9 changes: 4 additions & 5 deletions lib/Expr/Path.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
DISABLE_WARNING_PUSH
DISABLE_WARNING_DEPRECATED_DECLARATIONS
#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/Casting.h"
DISABLE_WARNING_POP

using namespace klee;
Expand Down Expand Up @@ -116,7 +117,7 @@ std::vector<CallStackFrame> Path::getStack(bool reversed) const {
std::vector<CallStackFrame> stack;
for (unsigned i = 0; i < path.size(); i++) {
auto index = reversed ? path.size() - 1 - i : i;
auto current = path.at(index);
auto current = path[index];

if (i == 0) {
stack.push_back(CallStackFrame(nullptr, current.block->parent));
Expand Down Expand Up @@ -184,6 +185,8 @@ Path Path::concat(const Path &l, const Path &r) {
}
Path path;
auto leftWhole = l.blockCompleted(l.path.size() - 1);
path.path.reserve(leftWhole ? l.path.size() + r.path.size()
: l.path.size() + r.path.size() - 1);
for (unsigned i = 0; i < l.path.size(); i++) {
path.path.push_back(l.path.at(i));
}
Expand Down Expand Up @@ -266,10 +269,6 @@ void Path::print(llvm::raw_ostream &ss) const {
ss << ") @ " << (next ? next->toString() : "None");
}

unsigned Path::KBlockSize() const {
return path.size();
}

std::pair<bool, KCallBlock *> Path::fromOutTransition() const {
if (path.empty()) {
return {false, nullptr};
Expand Down

0 comments on commit c43bb04

Please sign in to comment.