Skip to content

Commit d5ff4df

Browse files
ocelaiwomisonijnik
ocelaiwo
authored and
misonijnik
committed
[fix] Compare exprs by height in simplifier
1 parent 4d9ad3e commit d5ff4df

4 files changed

Lines changed: 54 additions & 1 deletion

File tree

‎include/klee/Expr/Expr.h‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -260,6 +260,7 @@ class Expr {
260260

261261
protected:
262262
unsigned hashValue;
263+
unsigned heightValue;
263264

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

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

308310
/// (Re)computes the hash of the current expression.
309311
/// Returns the hash value.
310312
virtual unsigned computeHash();
313+
virtual unsigned computeHeight();
311314

312315
/// Compares `b` to `this` Expr for structural equivalence.
313316
///
@@ -522,6 +525,7 @@ class NotOptimizedExpr : public NonConstantExpr {
522525
static ref<Expr> alloc(const ref<Expr> &src) {
523526
ref<Expr> r(new NotOptimizedExpr(src));
524527
r->computeHash();
528+
r->computeHeight();
525529
return createCachedExpr(r);
526530
}
527531

@@ -557,6 +561,7 @@ class UpdateNode {
557561

558562
// cache instead of recalc
559563
unsigned hashValue;
564+
unsigned heightValue;
560565

561566
public:
562567
const ref<UpdateNode> next;
@@ -578,11 +583,13 @@ class UpdateNode {
578583
int compare(const UpdateNode &b) const;
579584
bool equals(const UpdateNode &b) const;
580585
unsigned hash() const { return hashValue; }
586+
unsigned height() const { return heightValue; }
581587

582588
UpdateNode() = delete;
583589
~UpdateNode() = default;
584590

585591
unsigned computeHash();
592+
unsigned computeHeight();
586593
};
587594

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

679686
unsigned hash() const;
687+
unsigned height() const;
680688
};
681689

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

@@ -714,6 +723,7 @@ class ReadExpr : public NonConstantExpr {
714723
}
715724

716725
virtual unsigned computeHash();
726+
virtual unsigned computeHeight();
717727

718728
private:
719729
ReadExpr(const UpdateList &_updates, const ref<Expr> &_index)
@@ -740,6 +750,7 @@ class SelectExpr : public NonConstantExpr {
740750
const ref<Expr> &f) {
741751
ref<Expr> r(new SelectExpr(c, t, f));
742752
r->computeHash();
753+
r->computeHeight();
743754
return createCachedExpr(r);
744755
}
745756

@@ -804,6 +815,7 @@ class ConcatExpr : public NonConstantExpr {
804815
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {
805816
ref<Expr> c(new ConcatExpr(l, r));
806817
c->computeHash();
818+
c->computeHeight();
807819
return createCachedExpr(c);
808820
}
809821

@@ -874,6 +886,7 @@ class ExtractExpr : public NonConstantExpr {
874886
static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) {
875887
ref<Expr> r(new ExtractExpr(e, o, w));
876888
r->computeHash();
889+
r->computeHeight();
877890
return createCachedExpr(r);
878891
}
879892

@@ -924,6 +937,7 @@ class NotExpr : public NonConstantExpr {
924937
static ref<Expr> alloc(const ref<Expr> &e) {
925938
ref<Expr> r(new NotExpr(e));
926939
r->computeHash();
940+
r->computeHeight();
927941
return createCachedExpr(r);
928942
}
929943

@@ -997,6 +1011,7 @@ class CastExpr : public NonConstantExpr {
9971011
static ref<Expr> alloc(const ref<Expr> &e, Width w) { \
9981012
ref<Expr> r(new _class_kind##Expr(e, w)); \
9991013
r->computeHash(); \
1014+
r->computeHeight(); \
10001015
return createCachedExpr(r); \
10011016
} \
10021017
static ref<Expr> create(const ref<Expr> &e, Width w); \
@@ -1030,6 +1045,7 @@ CAST_EXPR_CLASS(FPExt)
10301045
llvm::APFloat::roundingMode rm) { \
10311046
ref<Expr> r(new _class_kind##Expr(e, w, rm)); \
10321047
r->computeHash(); \
1048+
r->computeHeight(); \
10331049
return createCachedExpr(r); \
10341050
} \
10351051
static ref<Expr> create(const ref<Expr> &e, Width w, \
@@ -1076,6 +1092,7 @@ FP_CAST_EXPR_CLASS(SIToFP)
10761092
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
10771093
ref<Expr> res(new _class_kind##Expr(l, r)); \
10781094
res->computeHash(); \
1095+
res->computeHeight(); \
10791096
return createCachedExpr(res); \
10801097
} \
10811098
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
@@ -1126,6 +1143,7 @@ ARITHMETIC_EXPR_CLASS(AShr)
11261143
const llvm::APFloat::roundingMode rm) { \
11271144
ref<Expr> res(new _class_kind##Expr(l, r, rm)); \
11281145
res->computeHash(); \
1146+
res->computeHeight(); \
11291147
return createCachedExpr(res); \
11301148
} \
11311149
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r, \
@@ -1172,6 +1190,7 @@ FLOAT_ARITHMETIC_EXPR_CLASS(FMin)
11721190
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
11731191
ref<Expr> res(new _class_kind##Expr(l, r)); \
11741192
res->computeHash(); \
1193+
res->computeHeight(); \
11751194
return createCachedExpr(res); \
11761195
} \
11771196
static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
@@ -1218,6 +1237,7 @@ COMPARISON_EXPR_CLASS(FOGe)
12181237
static ref<Expr> alloc(const ref<Expr> &e) { \
12191238
ref<Expr> r(new _class_kind##Expr(e)); \
12201239
r->computeHash(); \
1240+
r->computeHeight(); \
12211241
return createCachedExpr(r); \
12221242
} \
12231243
static ref<Expr> create(const ref<Expr> &e); \
@@ -1263,6 +1283,7 @@ FP_PRED_EXPR_CLASS(IsSubnormal)
12631283
const llvm::APFloat::roundingMode rm) { \
12641284
ref<Expr> r(new _class_kind##Expr(e, rm)); \
12651285
r->computeHash(); \
1286+
r->computeHeight(); \
12661287
return createCachedExpr(r); \
12671288
} \
12681289
static ref<Expr> create(const ref<Expr> &e, \
@@ -1309,6 +1330,7 @@ class FAbsExpr : public NonConstantExpr {
13091330
static ref<Expr> alloc(const ref<Expr> &e) {
13101331
ref<Expr> r(new FAbsExpr(e));
13111332
r->computeHash();
1333+
r->computeHeight();
13121334
return createCachedExpr(r);
13131335
}
13141336
static ref<Expr> create(const ref<Expr> &e);
@@ -1341,6 +1363,7 @@ class FNegExpr : public NonConstantExpr {
13411363
static ref<Expr> alloc(const ref<Expr> &e) {
13421364
ref<Expr> r(new FNegExpr(e));
13431365
r->computeHash();
1366+
r->computeHeight();
13441367
return createCachedExpr(r);
13451368
}
13461369
static ref<Expr> create(const ref<Expr> &e);
@@ -1447,12 +1470,14 @@ class ConstantExpr : public Expr {
14471470
static ref<ConstantExpr> alloc(const llvm::APInt &v) {
14481471
ref<ConstantExpr> r(new ConstantExpr(v));
14491472
r->computeHash();
1473+
r->computeHeight();
14501474
return r;
14511475
}
14521476

14531477
static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
14541478
ref<ConstantExpr> r(new ConstantExpr(f));
14551479
r->computeHash();
1480+
r->computeHeight();
14561481
return r;
14571482
}
14581483

‎lib/Expr/Constraints.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,7 @@ Simplificator::simplifyExpr(const constraints_ty &constraints,
425425
if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
426426
ref<Expr> left = ee->left;
427427
ref<Expr> right = ee->right;
428-
if (right < left) {
428+
if (right->height() < left->height()) {
429429
left = ee->right;
430430
right = ee->left;
431431
}

‎lib/Expr/Expr.cpp‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -260,6 +260,18 @@ unsigned Expr::computeHash() {
260260
return hashValue;
261261
}
262262

263+
unsigned Expr::computeHeight() {
264+
unsigned maxKidHeight = 0;
265+
266+
int n = getNumKids();
267+
for (int i = 0; i < n; i++) {
268+
maxKidHeight = std::max(maxKidHeight, getKid(i)->height());
269+
}
270+
271+
heightValue = maxKidHeight + 1;
272+
return heightValue;
273+
}
274+
263275
unsigned ConstantExpr::computeHash() {
264276
Expr::Width w = getWidth();
265277
if (w <= 64)
@@ -290,6 +302,11 @@ unsigned ReadExpr::computeHash() {
290302
return hashValue;
291303
}
292304

305+
unsigned ReadExpr::computeHeight() {
306+
heightValue = std::max(index->height(), updates.height()) + 1;
307+
return heightValue;
308+
}
309+
293310
unsigned NotExpr::computeHash() {
294311
hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
295312
return hashValue;

‎lib/Expr/Updates.cpp‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
2525
"Update value should be 8-bit wide.");
2626
*/
2727
computeHash();
28+
computeHeight();
2829
size = next ? next->size + 1 : 1;
2930
}
3031

@@ -45,6 +46,14 @@ unsigned UpdateNode::computeHash() {
4546
return hashValue;
4647
}
4748

49+
unsigned UpdateNode::computeHeight() {
50+
unsigned maxHeight = next ? next->height() : 0;
51+
maxHeight = std::max(maxHeight, index->height());
52+
maxHeight = std::max(maxHeight, value->height());
53+
heightValue = maxHeight;
54+
return heightValue;
55+
}
56+
4857
///
4958

5059
UpdateList::UpdateList(const Array *_root, const ref<UpdateNode> &_head)
@@ -95,3 +104,5 @@ unsigned UpdateList::hash() const {
95104
res = (res * Expr::MAGIC_HASH_CONSTANT) + head->hash();
96105
return res;
97106
}
107+
108+
unsigned UpdateList::height() const { return head ? head->height() : 0; }

0 commit comments

Comments
 (0)