Skip to content
This repository was archived by the owner on Feb 3, 2020. It is now read-only.

Commit 823ca86

Browse files
Expr: fixed hash computation
Since expressions are immutable, this can be done on expression creation Signed-off-by: Vitaly Chipounov <vitaly@cyberhaven.io>
1 parent 391f09e commit 823ca86

File tree

3 files changed

+66
-53
lines changed

3 files changed

+66
-53
lines changed

include/klee/Expr.h

Lines changed: 49 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ class Expr {
193193
protected:
194194
unsigned hashValue;
195195

196-
Expr() : refCount(0) {
196+
Expr() : refCount(0), hashValue(0) {
197197
}
198198

199199
public:
@@ -216,10 +216,6 @@ class Expr {
216216
return hashValue;
217217
}
218218

219-
/// (Re)computes the hash of the current expression.
220-
/// Returns the hash value.
221-
virtual unsigned computeHash();
222-
223219
/// Compares `b` to `this` Expr for structural equivalence.
224220
///
225221
/// This method effectively defines a total order over all Expr.
@@ -374,7 +370,6 @@ class ConstantExpr : public Expr {
374370

375371
for (uint64_t j = 0; j < max; ++j) {
376372
ref<ConstantExpr> r(new ConstantExpr(llvm::APInt(i, j)));
377-
r->computeHash();
378373
_const_table[i][j] = r;
379374
}
380375
}
@@ -391,7 +386,6 @@ class ConstantExpr : public Expr {
391386
}
392387

393388
ref<ConstantExpr> r(new ConstantExpr(v));
394-
r->computeHash();
395389
return r;
396390
}
397391

@@ -400,6 +394,11 @@ class ConstantExpr : public Expr {
400394
};
401395

402396
ConstantExpr(const llvm::APInt &v) : Expr(), value(v) {
397+
if (v.getBitWidth() <= 64) {
398+
hashValue = v.getZExtValue();
399+
} else {
400+
hashValue = *v.getRawData();
401+
}
403402
}
404403

405404
public:
@@ -610,6 +609,7 @@ class BinaryExpr : public NonConstantExpr {
610609

611610
protected:
612611
BinaryExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {
612+
hashValue = (left->hash() ^ right->hash()) * MAGIC_HASH_CONSTANT;
613613
}
614614

615615
protected:
@@ -749,11 +749,12 @@ class UpdateNode {
749749
private:
750750
UpdateNode(const UpdateNodePtr &_next, const ref<Expr> &_index, const ref<Expr> &_value);
751751

752-
UpdateNode() : m_refCount(0) {
752+
UpdateNode() : m_refCount(0), hashValue(0) {
753753
}
754+
754755
~UpdateNode();
755756

756-
unsigned computeHash();
757+
void computeHash();
757758

758759
friend void intrusive_ptr_add_ref(UpdateNode *ptr);
759760
friend void intrusive_ptr_release(UpdateNode *ptr);
@@ -891,8 +892,12 @@ class UpdateList {
891892

892893
std::atomic<unsigned> m_refCount;
893894

895+
unsigned m_hashValue;
896+
894897
UpdateList(ArrayPtr _root, UpdateNodePtr _head);
895898

899+
void computeHash();
900+
896901
public:
897902
static UpdateListPtr create(ArrayPtr _root, UpdateNodePtr _head) {
898903
return UpdateListPtr(new UpdateList(_root, _head));
@@ -906,7 +911,9 @@ class UpdateList {
906911
void extend(const ref<Expr> &index, const ref<Expr> &value);
907912

908913
int compare(const UpdateListPtr &b) const;
909-
unsigned hash() const;
914+
unsigned hash() const {
915+
return m_hashValue;
916+
}
910917

911918
const ArrayPtr &getRoot() const {
912919
return root;
@@ -941,8 +948,11 @@ class ReadExpr : public NonConstantExpr {
941948
ref<Expr> index;
942949

943950
ReadExpr(const UpdateListPtr &_updates, const ref<Expr> &_index) : updates(_updates), index(_index) {
951+
computeHash();
944952
}
945953

954+
void computeHash();
955+
946956
public:
947957
virtual ~ReadExpr() {
948958
}
@@ -985,8 +995,6 @@ class ReadExpr : public NonConstantExpr {
985995
return create(updates, kids[0]);
986996
}
987997

988-
virtual unsigned computeHash();
989-
990998
static bool classof(const Expr *E) {
991999
return E->getKind() == Expr::Read;
9921000
}
@@ -1087,6 +1095,7 @@ class SelectExpr : public NonConstantExpr {
10871095

10881096
private:
10891097
SelectExpr(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) : cond(c), trueExpr(t), falseExpr(f) {
1098+
hashValue = c->hash() ^ t->hash() ^ f->hash() ^ getKind();
10901099
}
10911100

10921101
public:
@@ -1160,6 +1169,7 @@ class ConcatExpr : public NonConstantExpr {
11601169
private:
11611170
ConcatExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {
11621171
width = l->getWidth() + r->getWidth();
1172+
hashValue = l->hash() ^ r->hash() ^ getKind();
11631173
}
11641174

11651175
public:
@@ -1231,12 +1241,13 @@ class ExtractExpr : public NonConstantExpr {
12311241
return create(kids[0], offset, width);
12321242
}
12331243

1234-
virtual unsigned computeHash();
1235-
12361244
private:
12371245
ExtractExpr(const ref<Expr> &e, unsigned b, Width w) : expr(e), offset(b), width(w) {
1246+
computeHash();
12381247
}
12391248

1249+
void computeHash();
1250+
12401251
public:
12411252
static bool classof(const Expr *E) {
12421253
return E->getKind() == Expr::Extract;
@@ -1296,8 +1307,6 @@ class NotExpr : public NonConstantExpr {
12961307
return create(kids[0]);
12971308
}
12981309

1299-
virtual unsigned computeHash();
1300-
13011310
public:
13021311
static bool classof(const Expr *E) {
13031312
return E->getKind() == Expr::Not;
@@ -1308,7 +1317,10 @@ class NotExpr : public NonConstantExpr {
13081317

13091318
private:
13101319
NotExpr(const ref<Expr> &e) : expr(e) {
1320+
computeHash();
13111321
}
1322+
1323+
void computeHash();
13121324
};
13131325

13141326
// Casting
@@ -1318,10 +1330,14 @@ class CastExpr : public NonConstantExpr {
13181330
ref<Expr> src;
13191331
Width width;
13201332

1321-
public:
1333+
void computeHash();
1334+
1335+
protected:
13221336
CastExpr(const ref<Expr> &e, Width w) : src(e), width(w) {
1337+
computeHash();
13231338
}
13241339

1340+
public:
13251341
Width getWidth() const {
13261342
return width;
13271343
}
@@ -1348,8 +1364,6 @@ class CastExpr : public NonConstantExpr {
13481364
return 0;
13491365
}
13501366

1351-
virtual unsigned computeHash();
1352-
13531367
static bool classof(const Expr *E) {
13541368
Expr::Kind k = E->getKind();
13551369
return Expr::CastKindFirst <= k && k <= Expr::CastKindLast;
@@ -1365,11 +1379,14 @@ class CastExpr : public NonConstantExpr {
13651379
static const Kind kind = _class_kind; \
13661380
static const unsigned numKids = 1; \
13671381
\
1382+
protected: \
1383+
_class_kind##Expr(const ref<Expr> &e, Width w) : CastExpr(e, w) { \
1384+
hashValue ^= getKind(); \
1385+
} \
1386+
\
13681387
public: \
13691388
virtual ~_class_kind##Expr() { \
13701389
} \
1371-
_class_kind##Expr(const ref<Expr> &e, Width w) : CastExpr(e, w) { \
1372-
} \
13731390
static ref<Expr> alloc(const ref<Expr> &e, Width w) { \
13741391
return ref<Expr>(new _class_kind##Expr(e, w)); \
13751392
} \
@@ -1400,11 +1417,15 @@ CAST_EXPR_CLASS(ZExt)
14001417
static const Kind kind = _class_kind; \
14011418
static const unsigned numKids = 2; \
14021419
\
1420+
protected: \
1421+
_class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r) : BinaryExpr(l, r) { \
1422+
hashValue ^= getKind(); \
1423+
} \
1424+
\
14031425
public: \
14041426
virtual ~_class_kind##Expr() { \
14051427
} \
1406-
_class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r) : BinaryExpr(l, r) { \
1407-
} \
1428+
\
14081429
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
14091430
return ref<Expr>(new _class_kind##Expr(l, r)); \
14101431
} \
@@ -1450,11 +1471,14 @@ ARITHMETIC_EXPR_CLASS(AShr)
14501471
static const Kind kind = _class_kind; \
14511472
static const unsigned numKids = 2; \
14521473
\
1474+
protected: \
1475+
_class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r) : CmpExpr(l, r) { \
1476+
hashValue ^= getKind(); \
1477+
} \
1478+
\
14531479
public: \
14541480
virtual ~_class_kind##Expr() { \
14551481
} \
1456-
_class_kind##Expr(const ref<Expr> &l, const ref<Expr> &r) : CmpExpr(l, r) { \
1457-
} \
14581482
static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
14591483
return ref<Expr>(new _class_kind##Expr(l, r)); \
14601484
} \

lib/Expr/Expr.cpp

Lines changed: 7 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -278,47 +278,33 @@ void Expr::printKind(llvm::raw_ostream &os, Kind k) {
278278
//
279279
///////
280280

281-
unsigned Expr::computeHash() {
282-
unsigned res = getKind() * Expr::MAGIC_HASH_CONSTANT;
283-
284-
int n = getNumKids();
285-
for (int i = 0; i < n; i++) {
286-
res <<= 1;
287-
res ^= getKid(i)->hash() * Expr::MAGIC_HASH_CONSTANT;
288-
}
289-
290-
hashValue = res;
291-
return hashValue;
292-
}
293-
294281
unsigned ConstantExpr::computeHash() {
295282
hashValue = hash_value(value) ^ (getWidth() * MAGIC_HASH_CONSTANT);
296283
return hashValue;
297284
}
298285

299-
unsigned CastExpr::computeHash() {
286+
void CastExpr::computeHash() {
300287
unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT;
301288
hashValue = res ^ src->hash() * Expr::MAGIC_HASH_CONSTANT;
302-
return hashValue;
303289
}
304290

305-
unsigned ExtractExpr::computeHash() {
291+
void ExtractExpr::computeHash() {
306292
unsigned res = offset * Expr::MAGIC_HASH_CONSTANT;
307293
res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT;
294+
res ^= getKind();
308295
hashValue = res ^ expr->hash() * Expr::MAGIC_HASH_CONSTANT;
309-
return hashValue;
310296
}
311297

312-
unsigned ReadExpr::computeHash() {
298+
void ReadExpr::computeHash() {
313299
unsigned res = index->hash() * Expr::MAGIC_HASH_CONSTANT;
314300
res ^= updates->hash();
301+
res ^= getKind();
315302
hashValue = res;
316-
return hashValue;
317303
}
318304

319-
unsigned NotExpr::computeHash() {
305+
void NotExpr::computeHash() {
320306
hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
321-
return hashValue;
307+
hashValue ^= getKind();
322308
}
323309

324310
void Expr::printWidth(llvm::raw_ostream &os, Width width) {

lib/Expr/Updates.cpp

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -36,17 +36,18 @@ int UpdateNode::compare(const UpdateNodePtr &b) const {
3636
return value.compare(b->value);
3737
}
3838

39-
unsigned UpdateNode::computeHash() {
39+
void UpdateNode::computeHash() {
4040
hashValue = index->hash() ^ value->hash();
4141
if (next) {
4242
hashValue ^= next->hash();
4343
}
44-
return hashValue;
4544
}
4645

4746
///
4847

49-
UpdateList::UpdateList(ArrayPtr _root, const UpdateNodePtr _head) : root(_root), head(_head), m_refCount(0) {
48+
UpdateList::UpdateList(ArrayPtr _root, const UpdateNodePtr _head)
49+
: root(_root), head(_head), m_refCount(0), m_hashValue(0) {
50+
computeHash();
5051
}
5152

5253
void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
@@ -85,15 +86,17 @@ int UpdateList::compare(const UpdateListPtr &b) const {
8586
return 0;
8687
}
8788

88-
unsigned UpdateList::hash() const {
89+
void UpdateList::computeHash() {
8990
unsigned res = 0;
90-
for (unsigned i = 0, e = root->getName().size(); i != e; ++i) {
91-
res = (res * Expr::MAGIC_HASH_CONSTANT) + root->getName()[i];
91+
if (root) {
92+
for (unsigned i = 0, e = root->getName().size(); i != e; ++i) {
93+
res = (res * Expr::MAGIC_HASH_CONSTANT) + root->getName()[i];
94+
}
9295
}
9396

9497
if (head) {
9598
res ^= head->hash();
9699
}
97100

98-
return res;
101+
m_hashValue = res;
99102
}

0 commit comments

Comments
 (0)