Skip to content
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.

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

Fixes pack #149

Merged
merged 7 commits into from
Nov 2, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
48 changes: 26 additions & 22 deletions include/klee/ADT/DisjointSetUnion.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,21 +24,29 @@ namespace klee {
using ExprEitherSymcrete = either<Expr, Symcrete>;

template <typename ValueType, typename SetType,
typename HASH = std::hash<ValueType>,
typename PRED = std::equal_to<ValueType>,
typename CMP = std::less<ValueType>>
class DisjointSetUnion {
public:
using internal_storage_ty = std::unordered_set<ValueType, HASH, PRED>;
using disjoint_sets_ty =
std::unordered_map<ValueType, ref<const SetType>, HASH, PRED>;
using iterator = typename internal_storage_ty::iterator;

protected:
PersistentMap<ValueType, ValueType, CMP> parent;
PersistentSet<ValueType, CMP> roots;
PersistentMap<ValueType, size_t, CMP> rank;
std::unordered_map<ValueType, ValueType, HASH, PRED> parent;
std::set<ValueType, CMP> roots;
std::unordered_map<ValueType, size_t, HASH, PRED> rank;

PersistentSet<ValueType, CMP> internalStorage;
PersistentMap<ValueType, ref<const SetType>, CMP> disjointSets;
std::unordered_set<ValueType, HASH, PRED> internalStorage;
std::unordered_map<ValueType, ref<const SetType>, HASH, PRED> disjointSets;

ValueType find(const ValueType &v) { // findparent
assert(parent.find(v) != parent.end());
if (v == parent.at(v))
return v;
parent.replace({v, find(parent.at(v))});
parent.insert_or_assign(v, find(parent.at(v)));
return parent.at(v);
}

Expand All @@ -60,26 +68,22 @@ class DisjointSetUnion {
if (rank.at(a) < rank.at(b)) {
std::swap(a, b);
}
parent.replace({b, a});
parent.insert_or_assign(b, a);
if (rank.at(a) == rank.at(b)) {
rank.replace({a, rank.at(a) + 1});
rank.insert_or_assign(a, rank.at(a) + 1);
}

roots.remove(b);
disjointSets.replace(
{a, SetType::merge(disjointSets.at(a), disjointSets.at(b))});
disjointSets.remove(b);
roots.erase(b);
disjointSets.insert_or_assign(
a, SetType::merge(disjointSets.at(a), disjointSets.at(b)));
disjointSets.erase(b);
}

bool areJoined(const ValueType &i, const ValueType &j) const {
return constFind(i) == constFind(j);
}

public:
using internalStorage_ty = PersistentSet<ValueType, CMP>;
using disjointSets_ty = ImmutableMap<ValueType, ref<const SetType>, CMP>;
using iterator = typename internalStorage_ty::iterator;

iterator begin() const { return internalStorage.begin(); }
iterator end() const { return internalStorage.end(); }

Expand Down Expand Up @@ -107,7 +111,7 @@ class DisjointSetUnion {
disjointSets.insert({value, new SetType(value)});

internalStorage.insert(value);
internalStorage_ty oldRoots = roots;
std::set<ValueType, CMP> oldRoots = roots;
for (ValueType v : oldRoots) {
if (!areJoined(v, value) &&
SetType::intersects(disjointSets.at(find(v)),
Expand All @@ -122,8 +126,8 @@ class DisjointSetUnion {
}

void add(const DisjointSetUnion &b) {
internalStorage_ty oldRoots = roots;
internalStorage_ty newRoots = b.roots;
std::set<ValueType, CMP> oldRoots = roots;
std::set<ValueType, CMP> newRoots = b.roots;
for (auto it : b.parent) {
parent.insert(it);
}
Expand Down Expand Up @@ -152,16 +156,16 @@ class DisjointSetUnion {

DisjointSetUnion() {}

DisjointSetUnion(const internalStorage_ty &is) {
DisjointSetUnion(const internal_storage_ty &is) {
for (ValueType v : is) {
addValue(v);
}
}

public:
internalStorage_ty is() const { return internalStorage; }
internal_storage_ty is() const { return internalStorage; }

disjointSets_ty ds() const { return disjointSets; }
disjoint_sets_ty ds() const { return disjointSets; }
};
} // namespace klee

Expand Down
23 changes: 21 additions & 2 deletions include/klee/ADT/Either.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@ template <class T1, class T2> class either {

/// @brief Required by klee::ref-managed objects
class ReferenceCounter _refCount;
unsigned hashValue;

static const unsigned MAGIC_HASH_CONSTANT = 39;

public:
using left = either_left<T1, T2>;
Expand All @@ -46,6 +49,8 @@ template <class T1, class T2> class either {
// virtual unsigned hash() = 0;
virtual int compare(const either<T1, T2> &b) = 0;
virtual bool equals(const either<T1, T2> &b) = 0;

unsigned hash() const { return hashValue; }
};

template <class T1, class T2> class either_left : public either<T1, T2> {
Expand All @@ -56,8 +61,15 @@ template <class T1, class T2> class either_left : public either<T1, T2> {
private:
ref<T1> value_;

unsigned computeHash() {
unsigned res = (unsigned)getKind();
res = (res * either<T1, T2>::MAGIC_HASH_CONSTANT) + value_->hash();
either<T1, T2>::hashValue = res;
return either<T1, T2>::hashValue;
}

public:
either_left(ref<T1> leftValue) : value_(leftValue){};
either_left(ref<T1> leftValue) : value_(leftValue) { computeHash(); };

ref<T1> value() const { return value_; }
operator ref<T1> const() { return value_; }
Expand Down Expand Up @@ -100,8 +112,15 @@ template <class T1, class T2> class either_right : public either<T1, T2> {
private:
ref<T2> value_;

unsigned computeHash() {
unsigned res = (unsigned)getKind();
res = (res * either<T1, T2>::MAGIC_HASH_CONSTANT) + value_->hash();
either<T1, T2>::hashValue = res;
return either<T1, T2>::hashValue;
}

public:
either_right(ref<T2> rightValue) : value_(rightValue){};
either_right(ref<T2> rightValue) : value_(rightValue) { computeHash(); };

ref<T2> value() const { return value_; }
operator ref<T2> const() { return value_; }
Expand Down
17 changes: 17 additions & 0 deletions include/klee/ADT/ImmutableList.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#ifndef KLEE_IMMUTABLELIST_H
#define KLEE_IMMUTABLELIST_H

#include <cassert>
#include <memory>
#include <vector>

Expand Down Expand Up @@ -96,6 +97,22 @@ template <typename T> class ImmutableList {
node->values.push_back(std::move(value));
}

void push_back(const T &value) {
if (!node) {
node = std::make_shared<ImmutableListNode>();
}
node->values.push_back(value);
}

bool empty() { return size() == 0; }

const T &back() {
assert(node && "requiers not empty list");
auto it = iterator(node.get());
it.get = size() - 1;
return *it;
}

ImmutableList() : node(){};
ImmutableList(const ImmutableList<T> &il)
: node(std::make_shared<ImmutableListNode>(il)) {}
Expand Down
3 changes: 2 additions & 1 deletion include/klee/Expr/Constraints.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@

#include "klee/ADT/Ref.h"

#include "klee/ADT/PersistentMap.h"
#include "klee/Expr/Assignment.h"
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprHashMap.h"
Expand Down Expand Up @@ -91,7 +92,7 @@ class ConstraintSet {
class PathConstraints {
public:
using ordered_constraints_ty =
std::map<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;
PersistentMap<Path::PathIndex, constraints_ty, Path::PathIndexCompare>;

void advancePath(KInstruction *ki);
void advancePath(const Path &path);
Expand Down
26 changes: 23 additions & 3 deletions include/klee/Expr/Expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -753,7 +753,14 @@ class SelectExpr : public NonConstantExpr {

static ref<Expr> create(ref<Expr> c, ref<Expr> t, ref<Expr> f);

Width getWidth() const { return trueExpr->getWidth(); }
Width getWidth() const {
if (trueExpr->height() < falseExpr->height()) {
return trueExpr->getWidth();
} else {
return falseExpr->getWidth();
}
}

Kind getKind() const { return Select; }

unsigned getNumKids() const { return numKids; }
Expand Down Expand Up @@ -1093,7 +1100,6 @@ FP_CAST_EXPR_CLASS(SIToFP)
return createCachedExpr(res); \
} \
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
Width getWidth() const { return left->getWidth(); } \
Kind getKind() const { return _class_kind; } \
virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
return create(kids[0], kids[1]); \
Expand All @@ -1103,6 +1109,13 @@ FP_CAST_EXPR_CLASS(SIToFP)
return E->getKind() == Expr::_class_kind; \
} \
static bool classof(const _class_kind##Expr *) { return true; } \
Width getWidth() const { \
if (left->height() < right->height()) { \
return left->getWidth(); \
} else { \
return right->getWidth(); \
} \
} \
\
protected: \
virtual int compareContents(const Expr &b) const { \
Expand Down Expand Up @@ -1145,7 +1158,14 @@ ARITHMETIC_EXPR_CLASS(AShr)
} \
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r, \
llvm::APFloat::roundingMode rm); \
Width getWidth() const { return left->getWidth(); } \
Width getWidth() const { \
if (left->height() < right->height()) { \
return left->getWidth(); \
} else { \
return right->getWidth(); \
} \
} \
\
Kind getKind() const { return _class_kind; } \
virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
return create(kids[0], kids[1], roundingMode); \
Expand Down
4 changes: 2 additions & 2 deletions include/klee/Expr/IndependentConstraintSetUnion.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@

namespace klee {
class IndependentConstraintSetUnion
: public DisjointSetUnion<ref<ExprEitherSymcrete>,
IndependentConstraintSet> {
: public DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet,
ExprEitherSymcreteHash, ExprEitherSymcreteCmp> {
public:
Assignment concretization;

Expand Down
16 changes: 15 additions & 1 deletion include/klee/Expr/IndependentSet.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,19 @@ DISABLE_WARNING_POP
namespace klee {
using ExprEitherSymcrete = either<Expr, Symcrete>;

struct ExprEitherSymcreteHash {
unsigned operator()(const ref<ExprEitherSymcrete> &e) const {
return e->hash();
}
};

struct ExprEitherSymcreteCmp {
bool operator()(const ref<ExprEitherSymcrete> &a,
const ref<ExprEitherSymcrete> &b) const {
return a == b;
}
};

template <class T> class DenseSet {
typedef std::set<T> set_ty;
set_ty s;
Expand Down Expand Up @@ -87,7 +100,8 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
class IndependentConstraintSet {
private:
using InnerSetUnion =
DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet>;
DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet,
ExprEitherSymcreteHash, ExprEitherSymcreteCmp>;

void initIndependentConstraintSet(ref<Expr> e);
void initIndependentConstraintSet(ref<Symcrete> s);
Expand Down
24 changes: 4 additions & 20 deletions include/klee/Expr/Path.h
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
#ifndef KLEE_PATH_H
#define KLEE_PATH_H

#include "klee/ADT/ImmutableList.h"

#include <stack>
#include <string>
#include <vector>
Expand All @@ -16,7 +18,7 @@ using stackframe_ty = std::pair<KInstruction *, KFunction *>;

class Path {
public:
using path_ty = std::vector<KBlock *>;
using path_ty = ImmutableList<KBlock *>;
enum class TransitionKind { StepInto, StepOut, None };

struct PathIndex {
Expand All @@ -38,23 +40,6 @@ class Path {

void advance(KInstruction *ki);

friend bool operator==(const Path &lhs, const Path &rhs) {
return lhs.KBlocks == rhs.KBlocks &&
lhs.firstInstruction == rhs.firstInstruction &&
lhs.lastInstruction == rhs.lastInstruction;
}
friend bool operator!=(const Path &lhs, const Path &rhs) {
return !(lhs == rhs);
}

friend bool operator<(const Path &lhs, const Path &rhs) {
return lhs.KBlocks < rhs.KBlocks ||
(lhs.KBlocks == rhs.KBlocks &&
(lhs.firstInstruction < rhs.firstInstruction ||
(lhs.firstInstruction == rhs.firstInstruction &&
lhs.lastInstruction < rhs.lastInstruction)));
}

unsigned KBlockSize() const;
const path_ty &getBlocks() const;
unsigned getFirstIndex() const;
Expand All @@ -64,7 +49,6 @@ class Path {

std::vector<stackframe_ty> getStack(bool reversed) const;

std::vector<std::pair<KFunction *, BlockRange>> asFunctionRanges() const;
std::string toString() const;

static Path concat(const Path &l, const Path &r);
Expand All @@ -73,7 +57,7 @@ class Path {

Path() = default;

Path(unsigned firstInstruction, std::vector<KBlock *> kblocks,
Path(unsigned firstInstruction, const path_ty &kblocks,
unsigned lastInstruction)
: KBlocks(kblocks), firstInstruction(firstInstruction),
lastInstruction(lastInstruction) {}
Expand Down
2 changes: 2 additions & 0 deletions include/klee/Expr/Symcrete.h
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,8 @@ class Symcrete {
return id < rhs.id ? -1 : 1;
}

unsigned hash() { return id; }

bool operator<(const Symcrete &rhs) const { return compare(rhs) < 0; };
};

Expand Down
5 changes: 0 additions & 5 deletions include/klee/Module/TargetHash.h
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,8 @@ struct TargetCmp {
bool operator()(const ref<Target> &a, const ref<Target> &b) const;
};

typedef std::pair<llvm::BasicBlock *, llvm::BasicBlock *> Transition;
typedef std::pair<llvm::BasicBlock *, unsigned> Branch;

struct TransitionHash {
std::size_t operator()(const Transition &p) const;
};

struct BranchHash {
std::size_t operator()(const Branch &p) const;
};
Expand Down
File renamed without changes.
Loading
Loading