Skip to content

Commit

Permalink
[fix] Compare exprs by height in simplifier
Browse files Browse the repository at this point in the history
  • Loading branch information
@ocelaiwo @misonijnik
ocelaiwo authored and misonijnik committed Oct 20, 2023
1 parent f1e8720 commit 12e689e
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 1 deletion.
25 changes: 25 additions & 0 deletions include/klee/Expr/Expr.h
View file
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
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
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
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; }

0 comments on commit 12e689e

Please sign in to comment.