From 12e689ec29127679a1770ce6a56004abc73764c9 Mon Sep 17 00:00:00 2001 From: Aleksei Babushkin Date: Fri, 20 Oct 2023 19:27:39 +0300 Subject: [PATCH] [fix] Compare exprs by height in simplifier --- include/klee/Expr/Expr.h | 25 +++++++++++++++++++++++++ lib/Expr/Constraints.cpp | 2 +- lib/Expr/Expr.cpp | 17 +++++++++++++++++ lib/Expr/Updates.cpp | 11 +++++++++++ 4 files changed, 54 insertions(+), 1 deletion(-) diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index ab6826e25d..9fdc8c5b21 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -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()`). @@ -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. /// @@ -522,6 +525,7 @@ class NotOptimizedExpr : public NonConstantExpr { static ref alloc(const ref &src) { ref r(new NotOptimizedExpr(src)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } @@ -557,6 +561,7 @@ class UpdateNode { // cache instead of recalc unsigned hashValue; + unsigned heightValue; public: const ref next; @@ -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 { @@ -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. @@ -693,6 +701,7 @@ class ReadExpr : public NonConstantExpr { static ref alloc(const UpdateList &updates, const ref &index) { ref r(new ReadExpr(updates, index)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } @@ -714,6 +723,7 @@ class ReadExpr : public NonConstantExpr { } virtual unsigned computeHash(); + virtual unsigned computeHeight(); private: ReadExpr(const UpdateList &_updates, const ref &_index) @@ -740,6 +750,7 @@ class SelectExpr : public NonConstantExpr { const ref &f) { ref r(new SelectExpr(c, t, f)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } @@ -804,6 +815,7 @@ class ConcatExpr : public NonConstantExpr { static ref alloc(const ref &l, const ref &r) { ref c(new ConcatExpr(l, r)); c->computeHash(); + c->computeHeight(); return createCachedExpr(c); } @@ -874,6 +886,7 @@ class ExtractExpr : public NonConstantExpr { static ref alloc(const ref &e, unsigned o, Width w) { ref r(new ExtractExpr(e, o, w)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } @@ -924,6 +937,7 @@ class NotExpr : public NonConstantExpr { static ref alloc(const ref &e) { ref r(new NotExpr(e)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } @@ -997,6 +1011,7 @@ class CastExpr : public NonConstantExpr { static ref alloc(const ref &e, Width w) { \ ref r(new _class_kind##Expr(e, w)); \ r->computeHash(); \ + r->computeHeight(); \ return createCachedExpr(r); \ } \ static ref create(const ref &e, Width w); \ @@ -1030,6 +1045,7 @@ CAST_EXPR_CLASS(FPExt) llvm::APFloat::roundingMode rm) { \ ref r(new _class_kind##Expr(e, w, rm)); \ r->computeHash(); \ + r->computeHeight(); \ return createCachedExpr(r); \ } \ static ref create(const ref &e, Width w, \ @@ -1076,6 +1092,7 @@ FP_CAST_EXPR_CLASS(SIToFP) static ref alloc(const ref &l, const ref &r) { \ ref res(new _class_kind##Expr(l, r)); \ res->computeHash(); \ + res->computeHeight(); \ return createCachedExpr(res); \ } \ static ref create(const ref &l, const ref &r); \ @@ -1126,6 +1143,7 @@ ARITHMETIC_EXPR_CLASS(AShr) const llvm::APFloat::roundingMode rm) { \ ref res(new _class_kind##Expr(l, r, rm)); \ res->computeHash(); \ + res->computeHeight(); \ return createCachedExpr(res); \ } \ static ref create(const ref &l, const ref &r, \ @@ -1172,6 +1190,7 @@ FLOAT_ARITHMETIC_EXPR_CLASS(FMin) static ref alloc(const ref &l, const ref &r) { \ ref res(new _class_kind##Expr(l, r)); \ res->computeHash(); \ + res->computeHeight(); \ return createCachedExpr(res); \ } \ static ref create(const ref &l, const ref &r); \ @@ -1218,6 +1237,7 @@ COMPARISON_EXPR_CLASS(FOGe) static ref alloc(const ref &e) { \ ref r(new _class_kind##Expr(e)); \ r->computeHash(); \ + r->computeHeight(); \ return createCachedExpr(r); \ } \ static ref create(const ref &e); \ @@ -1263,6 +1283,7 @@ FP_PRED_EXPR_CLASS(IsSubnormal) const llvm::APFloat::roundingMode rm) { \ ref r(new _class_kind##Expr(e, rm)); \ r->computeHash(); \ + r->computeHeight(); \ return createCachedExpr(r); \ } \ static ref create(const ref &e, \ @@ -1309,6 +1330,7 @@ class FAbsExpr : public NonConstantExpr { static ref alloc(const ref &e) { ref r(new FAbsExpr(e)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } static ref create(const ref &e); @@ -1341,6 +1363,7 @@ class FNegExpr : public NonConstantExpr { static ref alloc(const ref &e) { ref r(new FNegExpr(e)); r->computeHash(); + r->computeHeight(); return createCachedExpr(r); } static ref create(const ref &e); @@ -1447,12 +1470,14 @@ class ConstantExpr : public Expr { static ref alloc(const llvm::APInt &v) { ref r(new ConstantExpr(v)); r->computeHash(); + r->computeHeight(); return r; } static ref alloc(const llvm::APFloat &f) { ref r(new ConstantExpr(f)); r->computeHash(); + r->computeHeight(); return r; } diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index f14d612379..241c1a329b 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -425,7 +425,7 @@ Simplificator::simplifyExpr(const constraints_ty &constraints, if (const EqExpr *ee = dyn_cast(constraint)) { ref left = ee->left; ref right = ee->right; - if (right < left) { + if (right->height() < left->height()) { left = ee->right; right = ee->left; } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index ccf6eab730..5d301e0d7c 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -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) @@ -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; diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 6b740e3a72..b7bbad8cbc 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -25,6 +25,7 @@ UpdateNode::UpdateNode(const ref &_next, const ref &_index, "Update value should be 8-bit wide."); */ computeHash(); + computeHeight(); size = next ? next->size + 1 : 1; } @@ -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 &_head) @@ -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; }