Skip to content

Commit 96ed720

Browse files
misonijnikmisonijnik
committed
[fix] Fix assertion fail
1 parent 27e0a63 commit 96ed720

6 files changed

Lines changed: 33 additions & 56 deletions

File tree

‎include/klee/Expr/Constraints.h‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@
1717
#include "klee/Expr/Expr.h"
1818
#include "klee/Expr/ExprHashMap.h"
1919
#include "klee/Expr/ExprUtil.h"
20-
#include "klee/Expr/IndependentConstraintSetUnion.h"
2120
#include "klee/Expr/IndependentSet.h"
2221
#include "klee/Expr/Path.h"
2322
#include "klee/Expr/Symcrete.h"

‎include/klee/Expr/IndependentSet.h‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ DISABLE_WARNING_POP
2323

2424
namespace klee {
2525
using ExprOrSymcrete = either<Expr, Symcrete>;
26+
class IndependentConstraintSetUnion;
2627

2728
struct ExprOrSymcreteHash {
2829
unsigned operator()(const ref<ExprOrSymcrete> &e) const { return e->hash(); }
@@ -97,9 +98,7 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
9798

9899
class IndependentConstraintSet {
99100
private:
100-
using InnerSetUnion =
101-
DisjointSetUnion<ref<ExprOrSymcrete>, IndependentConstraintSet,
102-
ExprOrSymcreteHash, ExprOrSymcreteCmp>;
101+
using InnerSetUnion = IndependentConstraintSetUnion;
103102

104103
void initIndependentConstraintSet(ref<Expr> e);
105104
void initIndependentConstraintSet(ref<Symcrete> s);
@@ -119,7 +118,7 @@ class IndependentConstraintSet {
119118

120119
Assignment concretization;
121120

122-
InnerSetUnion concretizedSets;
121+
std::shared_ptr<InnerSetUnion> concretizedSets;
123122

124123
ref<const IndependentConstraintSet> addExpr(ref<Expr> e) const;
125124
ref<const IndependentConstraintSet>

‎lib/Expr/Constraints.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
#include "klee/Expr/ExprHashMap.h"
1616
#include "klee/Expr/ExprUtil.h"
1717
#include "klee/Expr/ExprVisitor.h"
18+
#include "klee/Expr/IndependentConstraintSetUnion.h"
1819
#include "klee/Expr/IndependentSet.h"
1920
#include "klee/Expr/Path.h"
2021
#include "klee/Expr/Symcrete.h"

‎lib/Expr/IndependentConstraintSetUnion.cpp‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
#include "klee/Expr/IndependentConstraintSetUnion.h"
22

3+
#include "klee/ADT/DisjointSetUnion.h"
4+
#include "klee/Expr/IndependentSet.h"
5+
36
namespace klee {
47

58
IndependentConstraintSetUnion::IndependentConstraintSetUnion() {}
@@ -152,10 +155,11 @@ IndependentConstraintSetUnion::getConcretizedVersion() {
152155
ref<const IndependentConstraintSet> root = disjointSets.at(i);
153156
if (root->concretization.bindings.empty()) {
154157
for (ref<Expr> expr : root->exprs) {
155-
icsu.addValue(new ExprOrSymcrete::left(expr));
158+
icsu.addExpr(expr);
156159
}
157160
} else {
158-
icsu.add(root->concretizedSets);
161+
root->concretizedSets->calculateQueue();
162+
icsu.add(*root->concretizedSets.get());
159163
}
160164
icsu.concretization.addIndependentAssignment(root->concretization);
161165
}
@@ -178,7 +182,15 @@ void IndependentConstraintSetUnion::calculateQueue() {
178182
calculateUpdateConcretizationQueue();
179183
calculateRemoveConcretizationQueue();
180184
while (!constraintQueue.empty()) {
181-
addValue(constraintQueue[constraintQueue.size() - 1]);
185+
auto constraint = constraintQueue[constraintQueue.size() - 1];
186+
if (auto expr = dyn_cast<ExprOrSymcrete::left>(constraint)) {
187+
if (auto ce = dyn_cast<ConstantExpr>(expr->value())) {
188+
assert(ce->isTrue() && "Attempt to add invalid constraint");
189+
constraintQueue.pop_back();
190+
continue;
191+
}
192+
}
193+
addValue(constraint);
182194
constraintQueue.pop_back();
183195
}
184196
calculateUpdateConcretizationQueue();

‎lib/Expr/IndependentSet.cpp‎

Lines changed: 13 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
#include "klee/Expr/Constraints.h"
66
#include "klee/Expr/ExprHashMap.h"
77
#include "klee/Expr/ExprUtil.h"
8+
#include "klee/Expr/IndependentConstraintSetUnion.h"
89
#include "klee/Expr/SymbolicSource.h"
910
#include "klee/Expr/Symcrete.h"
1011
#include "klee/Solver/Solver.h"
@@ -29,32 +30,20 @@ IndependentConstraintSet::updateConcretization(
2930
InnerSetUnion DSU;
3031
for (ref<Expr> i : exprs) {
3132
ref<Expr> e = ics->concretization.evaluate(i);
32-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
33-
assert(ce->isTrue() && "Attempt to add invalid constraint");
34-
continue;
35-
}
3633
concretizedExprs[i] = e;
37-
DSU.addValue(new ExprOrSymcrete::left(e));
34+
DSU.addExpr(e);
3835
}
3936
for (ref<Symcrete> s : symcretes) {
4037
ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
4138
s->symcretized);
42-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
43-
assert(ce->isTrue() && "Attempt to add invalid constraint");
44-
continue;
45-
}
46-
DSU.addValue(new ExprOrSymcrete::left(e));
39+
DSU.addExpr(e);
4740
}
4841
auto concretizationConstraints =
4942
ics->concretization.createConstraintsFromAssignment();
5043
for (ref<Expr> e : concretizationConstraints) {
51-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
52-
assert(ce->isTrue() && "Attempt to add invalid constraint");
53-
continue;
54-
}
55-
DSU.addValue(new ExprOrSymcrete::left(e));
44+
DSU.addExpr(e);
5645
}
57-
ics->concretizedSets = DSU;
46+
ics->concretizedSets.reset(new InnerSetUnion(DSU));
5847
return ics;
5948
}
6049

@@ -71,33 +60,21 @@ IndependentConstraintSet::removeConcretization(
7160
InnerSetUnion DSU;
7261
for (ref<Expr> i : exprs) {
7362
ref<Expr> e = ics->concretization.evaluate(i);
74-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
75-
assert(ce->isTrue() && "Attempt to add invalid constraint");
76-
continue;
77-
}
7863
concretizedExprs[i] = e;
79-
DSU.addValue(new ExprOrSymcrete::left(e));
64+
DSU.addExpr(e);
8065
}
8166
for (ref<Symcrete> s : symcretes) {
8267
ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
8368
s->symcretized);
84-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
85-
assert(ce->isTrue() && "Attempt to add invalid constraint");
86-
continue;
87-
}
88-
DSU.addValue(new ExprOrSymcrete::left(e));
69+
DSU.addExpr(e);
8970
}
9071
auto concretizationConstraints =
9172
ics->concretization.createConstraintsFromAssignment();
9273
for (ref<Expr> e : concretizationConstraints) {
93-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
94-
assert(ce->isTrue() && "Attempt to add invalid constraint");
95-
continue;
96-
}
97-
DSU.addValue(new ExprOrSymcrete::left(e));
74+
DSU.addExpr(e);
9875
}
9976

100-
ics->concretizedSets = DSU;
77+
ics->concretizedSets.reset(new InnerSetUnion(DSU));
10178
return ics;
10279
}
10380

@@ -346,32 +323,20 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
346323
InnerSetUnion DSU;
347324
for (ref<Expr> i : a->exprs) {
348325
ref<Expr> e = a->concretization.evaluate(i);
349-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
350-
assert(ce->isTrue() && "Attempt to add invalid constraint");
351-
continue;
352-
}
353-
DSU.addValue(new ExprOrSymcrete::left(e));
326+
DSU.addExpr(e);
354327
}
355328
for (ref<Symcrete> s : a->symcretes) {
356329
ref<Expr> e = EqExpr::create(a->concretization.evaluate(s->symcretized),
357330
s->symcretized);
358-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
359-
assert(ce->isTrue() && "Attempt to add invalid constraint");
360-
continue;
361-
}
362-
DSU.addValue(new ExprOrSymcrete::left(e));
331+
DSU.addExpr(e);
363332
}
364333
auto concretizationConstraints =
365334
a->concretization.createConstraintsFromAssignment();
366335
for (ref<Expr> e : concretizationConstraints) {
367-
if (auto ce = dyn_cast<ConstantExpr>(e)) {
368-
assert(ce->isTrue() && "Attempt to add invalid constraint");
369-
continue;
370-
}
371-
DSU.addValue(new ExprOrSymcrete::left(e));
336+
DSU.addExpr(e);
372337
}
373338

374-
a->concretizedSets = DSU;
339+
a->concretizedSets.reset(new InnerSetUnion(DSU));
375340
}
376341

377342
return a;

‎lib/Solver/ConcretizingSolver.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
#include "klee/Expr/Constraints.h"
44
#include "klee/Expr/Expr.h"
55
#include "klee/Expr/ExprUtil.h"
6+
#include "klee/Expr/IndependentConstraintSetUnion.h"
67
#include "klee/Expr/IndependentSet.h"
78
#include "klee/Expr/SymbolicSource.h"
89
#include "klee/Expr/Symcrete.h"

0 commit comments

Comments
 (0)