Skip to content

Compare expressions by height in simplifier #138

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
misonijnik merged 1 commit into from
Oct 21, 2023
Merged

Compare expressions by height in simplifier #138

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
25 changes: 25 additions & 0 deletions include/klee/Expr/Expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,6 +260,7 @@ class Expr {

protected:
unsigned hashValue;
unsigned heightValue;

/// Compares `b` to `this` Expr and determines how they are ordered
/// (ignoring their kid expressions - i.e. those returned by `getKid()`).
Expand Down Expand Up @@ -304,10 +305,12 @@ class Expr {

/// Returns the pre-computed hash of the current expression
virtual unsigned hash() const { return hashValue; }
virtual unsigned height() const { return heightValue; }

/// (Re)computes the hash of the current expression.
/// Returns the hash value.
virtual unsigned computeHash();
virtual unsigned computeHeight();

/// Compares `b` to `this` Expr for structural equivalence.
///
Expand Down Expand Up @@ -522,6 +525,7 @@ class NotOptimizedExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &src) {
ref<Expr> r(new NotOptimizedExpr(src));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}

Expand Down Expand Up @@ -557,6 +561,7 @@ class UpdateNode {

// cache instead of recalc
unsigned hashValue;
unsigned heightValue;

public:
const ref<UpdateNode> next;
Expand All @@ -578,11 +583,13 @@ class UpdateNode {
int compare(const UpdateNode &b) const;
bool equals(const UpdateNode &b) const;
unsigned hash() const { return hashValue; }
unsigned height() const { return heightValue; }

UpdateNode() = delete;
~UpdateNode() = default;

unsigned computeHash();
unsigned computeHeight();
};

class Array {
Expand Down Expand Up @@ -677,6 +684,7 @@ class UpdateList {
bool operator<(const UpdateList &rhs) const { return compare(rhs) < 0; }

unsigned hash() const;
unsigned height() const;
};

/// Class representing a one byte read from an array.
Expand All @@ -693,6 +701,7 @@ class ReadExpr : public NonConstantExpr {
static ref<Expr> alloc(const UpdateList &updates, const ref<Expr> &index) {
ref<Expr> r(new ReadExpr(updates, index));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}

Expand All @@ -714,6 +723,7 @@ class ReadExpr : public NonConstantExpr {
}

virtual unsigned computeHash();
virtual unsigned computeHeight();

private:
ReadExpr(const UpdateList &_updates, const ref<Expr> &_index)
Expand All @@ -740,6 +750,7 @@ class SelectExpr : public NonConstantExpr {
const ref<Expr> &f) {
ref<Expr> r(new SelectExpr(c, t, f));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}

Expand Down Expand Up @@ -804,6 +815,7 @@ class ConcatExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {
ref<Expr> c(new ConcatExpr(l, r));
c->computeHash();
c->computeHeight();
return createCachedExpr(c);
}

Expand Down Expand Up @@ -874,6 +886,7 @@ class ExtractExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) {
ref<Expr> r(new ExtractExpr(e, o, w));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}

Expand Down Expand Up @@ -924,6 +937,7 @@ class NotExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &e) {
ref<Expr> r(new NotExpr(e));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}

Expand Down Expand Up @@ -997,6 +1011,7 @@ class CastExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &e, Width w) { \
ref<Expr> r(new _class_kind##Expr(e, w)); \
r->computeHash(); \
r->computeHeight(); \
return createCachedExpr(r); \
} \
static ref<Expr> create(const ref<Expr> &e, Width w); \
Expand Down Expand Up @@ -1030,6 +1045,7 @@ CAST_EXPR_CLASS(FPExt)
llvm::APFloat::roundingMode rm) { \
ref<Expr> r(new _class_kind##Expr(e, w, rm)); \
r->computeHash(); \
r->computeHeight(); \
return createCachedExpr(r); \
} \
static ref<Expr> create(const ref<Expr> &e, Width w, \
Expand Down Expand Up @@ -1076,6 +1092,7 @@ FP_CAST_EXPR_CLASS(SIToFP)
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
ref<Expr> res(new _class_kind##Expr(l, r)); \
res->computeHash(); \
res->computeHeight(); \
return createCachedExpr(res); \
} \
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
Expand Down Expand Up @@ -1126,6 +1143,7 @@ ARITHMETIC_EXPR_CLASS(AShr)
const llvm::APFloat::roundingMode rm) { \
ref<Expr> res(new _class_kind##Expr(l, r, rm)); \
res->computeHash(); \
res->computeHeight(); \
return createCachedExpr(res); \
} \
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r, \
Expand Down Expand Up @@ -1172,6 +1190,7 @@ FLOAT_ARITHMETIC_EXPR_CLASS(FMin)
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
ref<Expr> res(new _class_kind##Expr(l, r)); \
res->computeHash(); \
res->computeHeight(); \
return createCachedExpr(res); \
} \
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
Expand Down Expand Up @@ -1218,6 +1237,7 @@ COMPARISON_EXPR_CLASS(FOGe)
static ref<Expr> alloc(const ref<Expr> &e) { \
ref<Expr> r(new _class_kind##Expr(e)); \
r->computeHash(); \
r->computeHeight(); \
return createCachedExpr(r); \
} \
static ref<Expr> create(const ref<Expr> &e); \
Expand Down Expand Up @@ -1263,6 +1283,7 @@ FP_PRED_EXPR_CLASS(IsSubnormal)
const llvm::APFloat::roundingMode rm) { \
ref<Expr> r(new _class_kind##Expr(e, rm)); \
r->computeHash(); \
r->computeHeight(); \
return createCachedExpr(r); \
} \
static ref<Expr> create(const ref<Expr> &e, \
Expand Down Expand Up @@ -1309,6 +1330,7 @@ class FAbsExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &e) {
ref<Expr> r(new FAbsExpr(e));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}
static ref<Expr> create(const ref<Expr> &e);
Expand Down Expand Up @@ -1341,6 +1363,7 @@ class FNegExpr : public NonConstantExpr {
static ref<Expr> alloc(const ref<Expr> &e) {
ref<Expr> r(new FNegExpr(e));
r->computeHash();
r->computeHeight();
return createCachedExpr(r);
}
static ref<Expr> create(const ref<Expr> &e);
Expand Down Expand Up @@ -1447,12 +1470,14 @@ class ConstantExpr : public Expr {
static ref<ConstantExpr> alloc(const llvm::APInt &v) {
ref<ConstantExpr> r(new ConstantExpr(v));
r->computeHash();
r->computeHeight();
return r;
}

static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
ref<ConstantExpr> r(new ConstantExpr(f));
r->computeHash();
r->computeHeight();
return r;
}

Expand Down
2 changes: 1 addition & 1 deletion lib/Expr/Constraints.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,7 @@ Simplificator::simplifyExpr(const constraints_ty &constraints,
if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
ref<Expr> left = ee->left;
ref<Expr> right = ee->right;
if (right < left) {
if (right->height() < left->height()) {
left = ee->right;
right = ee->left;
}
Expand Down
17 changes: 17 additions & 0 deletions lib/Expr/Expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,6 +260,18 @@ unsigned Expr::computeHash() {
return hashValue;
}

unsigned Expr::computeHeight() {
unsigned maxKidHeight = 0;

int n = getNumKids();
for (int i = 0; i < n; i++) {
maxKidHeight = std::max(maxKidHeight, getKid(i)->height());
}

heightValue = maxKidHeight + 1;
return heightValue;
}

unsigned ConstantExpr::computeHash() {
Expr::Width w = getWidth();
if (w <= 64)
Expand Down Expand Up @@ -290,6 +302,11 @@ unsigned ReadExpr::computeHash() {
return hashValue;
}

unsigned ReadExpr::computeHeight() {
heightValue = std::max(index->height(), updates.height()) + 1;
return heightValue;
}

unsigned NotExpr::computeHash() {
hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
return hashValue;
Expand Down
11 changes: 11 additions & 0 deletions lib/Expr/Updates.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
"Update value should be 8-bit wide.");
*/
computeHash();
computeHeight();
size = next ? next->size + 1 : 1;
}

Expand All @@ -45,6 +46,14 @@ unsigned UpdateNode::computeHash() {
return hashValue;
}

unsigned UpdateNode::computeHeight() {
unsigned maxHeight = next ? next->height() : 0;
maxHeight = std::max(maxHeight, index->height());
maxHeight = std::max(maxHeight, value->height());
heightValue = maxHeight;
return heightValue;
}

///

UpdateList::UpdateList(const Array *_root, const ref<UpdateNode> &_head)
Expand Down Expand Up @@ -95,3 +104,5 @@ unsigned UpdateList::hash() const {
res = (res * Expr::MAGIC_HASH_CONSTANT) + head->hash();
return res;
}

unsigned UpdateList::height() const { return head ? head->height() : 0; }