Skip to content

Commit 8de31b5

Browse files
misonijnikmisonijnik
committed
[fix] Improve IndependentConstraintSetUnion 
1 parent aa7528b commit 8de31b5

File tree

8 files changed

+289
-101
lines changed

8 files changed

+289
-101
lines changed

‎include/klee/ADT/DisjointSetUnion.h‎

Lines changed: 27 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,27 @@
11
#ifndef KLEE_DISJOINEDSETUNION_H
22
#define KLEE_DISJOINEDSETUNION_H
3+
4+
#include "klee/ADT/Either.h"
35
#include "klee/ADT/PersistentMap.h"
46
#include "klee/ADT/PersistentSet.h"
57
#include "klee/ADT/Ref.h"
8+
#include "klee/Expr/Expr.h"
9+
#include "klee/Expr/Symcrete.h"
10+
11+
#include "klee/Support/CompilerWarning.h"
12+
DISABLE_WARNING_PUSH
13+
DISABLE_WARNING_DEPRECATED_DECLARATIONS
14+
#include "llvm/Support/raw_ostream.h"
15+
DISABLE_WARNING_POP
16+
17+
#include <map>
618
#include <set>
719
#include <unordered_map>
820
#include <unordered_set>
921
#include <vector>
1022

1123
namespace klee {
24+
using ExprEitherSymcrete = either<Expr, Symcrete>;
1225

1326
template <typename ValueType, typename SetType,
1427
typename CMP = std::less<ValueType>>
@@ -55,7 +68,7 @@ class DisjointSetUnion {
5568
roots.remove(b);
5669
disjointSets.replace(
5770
{a, SetType::merge(disjointSets.at(a), disjointSets.at(b))});
58-
disjointSets.replace({b, nullptr});
71+
disjointSets.remove(b);
5972
}
6073

6174
bool areJoined(const ValueType &i, const ValueType &j) const {
@@ -109,6 +122,8 @@ class DisjointSetUnion {
109122
}
110123

111124
void add(const DisjointSetUnion &b) {
125+
internalStorage_ty oldRoots = roots;
126+
internalStorage_ty newRoots = b.roots;
112127
for (auto it : b.parent) {
113128
parent.insert(it);
114129
}
@@ -124,6 +139,15 @@ class DisjointSetUnion {
124139
for (auto it : b.disjointSets) {
125140
disjointSets.insert(it);
126141
}
142+
for (ValueType nv : newRoots) {
143+
for (ValueType ov : oldRoots) {
144+
if (!areJoined(ov, nv) &&
145+
SetType::intersects(disjointSets.at(find(ov)),
146+
disjointSets.at(find(nv)))) {
147+
merge(ov, nv);
148+
}
149+
}
150+
}
127151
}
128152

129153
DisjointSetUnion() {}
@@ -140,4 +164,5 @@ class DisjointSetUnion {
140164
disjointSets_ty ds() const { return disjointSets; }
141165
};
142166
} // namespace klee
143-
#endif
167+
168+
#endif /* KLEE_DISJOINEDSETUNION_H */

‎include/klee/ADT/Either.h‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
//===-- Either.h ------------------------------------------------*- C++ -*-===//
2+
//
3+
// The KLEE Symbolic Virtual Machine
4+
//
5+
// This file is distributed under the University of Illinois Open Source
6+
// License. See LICENSE.TXT for details.
7+
//
8+
//===----------------------------------------------------------------------===//
9+
10+
#ifndef KLEE_EITHER_H
11+
#define KLEE_EITHER_H
12+
13+
#include "klee/ADT/Ref.h"
14+
15+
#include "klee/Support/Casting.h"
16+
17+
#include <cassert>
18+
19+
namespace llvm {
20+
class raw_ostream;
21+
} // namespace llvm
22+
23+
namespace klee {
24+
25+
template <class T1, class T2> class either_left;
26+
template <class T1, class T2> class either_right;
27+
28+
template <class T1, class T2> class either {
29+
protected:
30+
friend class ref<either<T1, T2>>;
31+
friend class ref<const either<T1, T2>>;
32+
33+
/// @brief Required by klee::ref-managed objects
34+
class ReferenceCounter _refCount;
35+
36+
public:
37+
using left = either_left<T1, T2>;
38+
using right = either_right<T1, T2>;
39+
40+
enum class EitherKind { Left, Right };
41+
42+
virtual ~either() {}
43+
virtual EitherKind getKind() const = 0;
44+
45+
static bool classof(const either<T1, T2> *) { return true; }
46+
// virtual unsigned hash() = 0;
47+
virtual int compare(const either<T1, T2> &b) = 0;
48+
virtual bool equals(const either<T1, T2> &b) = 0;
49+
};
50+
51+
template <class T1, class T2> class either_left : public either<T1, T2> {
52+
protected:
53+
friend class ref<either_left<T1, T2>>;
54+
friend class ref<const either_left<T1, T2>>;
55+
56+
private:
57+
ref<T1> value_;
58+
59+
public:
60+
either_left(ref<T1> leftValue) : value_(leftValue){};
61+
62+
ref<T1> value() const { return value_; }
63+
operator ref<T1> const() { return value_; }
64+
65+
virtual typename either<T1, T2>::EitherKind getKind() const override {
66+
return either<T1, T2>::EitherKind::Left;
67+
}
68+
69+
static bool classof(const either<T1, T2> *S) {
70+
return S->getKind() == either<T1, T2>::EitherKind::Left;
71+
}
72+
static bool classof(const either_left<T1, T2> *) { return true; }
73+
74+
// virtual unsigned hash() override { return value_->hash(); };
75+
virtual int compare(const either<T1, T2> &b) override {
76+
if (b.getKind() != getKind()) {
77+
return b.getKind() < getKind() ? -1 : 1;
78+
}
79+
const either_left<T1, T2> &el = static_cast<const either_left<T1, T2> &>(b);
80+
if (el.value() != value()) {
81+
return el.value() < value() ? -1 : 1;
82+
}
83+
return 0;
84+
}
85+
86+
virtual bool equals(const either<T1, T2> &b) override {
87+
if (b.getKind() != getKind()) {
88+
return false;
89+
}
90+
const either_left<T1, T2> &el = static_cast<const either_left<T1, T2> &>(b);
91+
return el.value() == value();
92+
}
93+
};
94+
95+
template <class T1, class T2> class either_right : public either<T1, T2> {
96+
protected:
97+
friend class ref<either_right<T1, T2>>;
98+
friend class ref<const either_right<T1, T2>>;
99+
100+
private:
101+
ref<T2> value_;
102+
103+
public:
104+
either_right(ref<T2> rightValue) : value_(rightValue){};
105+
106+
ref<T2> value() const { return value_; }
107+
operator ref<T2> const() { return value_; }
108+
109+
virtual typename either<T1, T2>::EitherKind getKind() const override {
110+
return either<T1, T2>::EitherKind::Right;
111+
}
112+
113+
static bool classof(const either<T1, T2> *S) {
114+
return S->getKind() == either<T1, T2>::EitherKind::Right;
115+
}
116+
static bool classof(const either_right<T1, T2> *) { return true; }
117+
118+
// virtual unsigned hash() override { return value_->hash(); };
119+
virtual int compare(const either<T1, T2> &b) override {
120+
if (b.getKind() != getKind()) {
121+
return b.getKind() < getKind() ? -1 : 1;
122+
}
123+
const either_right<T1, T2> &el =
124+
static_cast<const either_right<T1, T2> &>(b);
125+
if (el.value() != value()) {
126+
return el.value() < value() ? -1 : 1;
127+
}
128+
return 0;
129+
}
130+
131+
virtual bool equals(const either<T1, T2> &b) override {
132+
if (b.getKind() != getKind()) {
133+
return false;
134+
}
135+
const either_right<T1, T2> &el =
136+
static_cast<const either_right<T1, T2> &>(b);
137+
return el.value() == value();
138+
}
139+
};
140+
} // end namespace klee
141+
142+
#endif /* KLEE_EITHER_H */

‎include/klee/Expr/IndependentConstraintSetUnion.h‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
11
#ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H
22
#define KLEE_INDEPENDENTCONSTRAINTSETUNION_H
33

4+
#include "klee/ADT/Either.h"
5+
46
#include "klee/Expr/Assignment.h"
57
#include "klee/Expr/IndependentSet.h"
68

79
namespace klee {
810
class IndependentConstraintSetUnion
9-
: public DisjointSetUnion<ref<Expr>, IndependentConstraintSet> {
11+
: public DisjointSetUnion<ref<ExprEitherSymcrete>,
12+
IndependentConstraintSet> {
1013
public:
1114
Assignment concretization;
1215

@@ -43,4 +46,4 @@ class IndependentConstraintSetUnion
4346
};
4447
} // namespace klee
4548

46-
#endif
49+
#endif /* KLEE_INDEPENDENTCONSTRAINTSETUNION_H */

‎include/klee/Expr/IndependentSet.h‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
#define KLEE_INDEPENDENTSET_H
33

44
#include "klee/ADT/DisjointSetUnion.h"
5+
#include "klee/ADT/Either.h"
56
#include "klee/ADT/PersistentMap.h"
67
#include "klee/ADT/PersistentSet.h"
78
#include "klee/Expr/Assignment.h"
@@ -21,6 +22,7 @@ DISABLE_WARNING_POP
2122
#include <vector>
2223

2324
namespace klee {
25+
using ExprEitherSymcrete = either<Expr, Symcrete>;
2426

2527
template <class T> class DenseSet {
2628
typedef std::set<T> set_ty;
@@ -84,7 +86,11 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
8486

8587
class IndependentConstraintSet {
8688
private:
87-
using InnerSetUnion = DisjointSetUnion<ref<Expr>, IndependentConstraintSet>;
89+
using InnerSetUnion =
90+
DisjointSetUnion<ref<ExprEitherSymcrete>, IndependentConstraintSet>;
91+
92+
void initIndependentConstraintSet(ref<Expr> e);
93+
void initIndependentConstraintSet(ref<Symcrete> s);
8894

8995
public:
9096
// All containers need to become persistent to make fast copy and faster
@@ -117,11 +123,8 @@ class IndependentConstraintSet {
117123
Assignment &assign) const;
118124

119125
IndependentConstraintSet();
120-
IndependentConstraintSet(ref<Expr> e);
121-
IndependentConstraintSet(ref<Symcrete> s);
122-
IndependentConstraintSet(const ref<const IndependentConstraintSet> &ics);
123-
124-
IndependentConstraintSet &operator=(const IndependentConstraintSet &ies);
126+
explicit IndependentConstraintSet(ref<ExprEitherSymcrete> v);
127+
IndependentConstraintSet(const IndependentConstraintSet &ics);
125128

126129
void print(llvm::raw_ostream &os) const;
127130

‎lib/Core/ExecutionState.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ struct Symbolic {
228228
struct MemorySubobject {
229229
ref<Expr> address;
230230
unsigned size;
231-
MemorySubobject(ref<Expr> address, unsigned size)
231+
explicit MemorySubobject(ref<Expr> address, unsigned size)
232232
: address(address), size(size) {}
233233
MemorySubobject &operator=(const MemorySubobject &other) = default;
234234
};

‎lib/Expr/Constraints.cpp‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -207,12 +207,12 @@ ConstraintSet::ConstraintSet() {}
207207

208208
void ConstraintSet::addConstraint(ref<Expr> e, const Assignment &delta) {
209209
_constraints.insert(e);
210-
_independentElements.addExpr(e);
211210
// Update bindings
212211
for (auto i : delta.bindings) {
213212
_concretization.bindings.replace({i.first, i.second});
214213
}
215214
_independentElements.updateConcretization(delta);
215+
_independentElements.addExpr(e);
216216
}
217217

218218
IDType Symcrete::idCounter = 0;
@@ -252,8 +252,10 @@ ConstraintSet ConstraintSet::getConcretizedVersion() const {
252252
ConstraintSet cs;
253253
cs._independentElements = _independentElements.getConcretizedVersion();
254254

255-
for (ref<Expr> e : cs._independentElements.is()) {
256-
cs._constraints.insert(e);
255+
for (auto &e : cs._independentElements.is()) {
256+
if (isa<ExprEitherSymcrete::left>(e)) {
257+
cs._constraints.insert(cast<ExprEitherSymcrete::left>(e)->value());
258+
}
257259
}
258260
return cs;
259261
}
@@ -263,8 +265,8 @@ ConstraintSet ConstraintSet::getConcretizedVersion(
263265
ConstraintSet cs;
264266
cs._independentElements =
265267
_independentElements.getConcretizedVersion(newConcretization);
266-
for (ref<Expr> e : cs._independentElements.is()) {
267-
cs._constraints.insert(e);
268+
for (auto &e : cs._independentElements.is()) {
269+
cs._constraints.insert(cast<ExprEitherSymcrete::left>(e)->value());
268270
}
269271
return cs;
270272
}

0 commit comments

Comments
 (0)