diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-01-05 15:46:30 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-01-05 15:46:30 +0000 |
commit | 34829f7444038a254449702082e7852f9ae1cad7 (patch) | |
tree | 31b17484596e08393cf74a33e99cf1398ed625df | |
parent | 3c5675731e3928ff0b96b8ab4b1ab2eed9031843 (diff) | |
parent | c8b3c00f1f15952ea4bcbeb9c633f9e8ebc8a6bf (diff) | |
download | klee-34829f7444038a254449702082e7852f9ae1cad7.tar.gz |
Merge pull request #325 from delcypher/fix_independence_solver_leak
Fix independence solver leak
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 82 |
1 files changed, 47 insertions, 35 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index a7685e46..78126ede 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -258,56 +258,66 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, // Breaks down a constraint into all of it's individual pieces, returning a // list of IndependentElementSets or the independent factors. -static -void getAllIndependentConstraintsSets(const Query& query, - std::list<IndependentElementSet> * &factors){ +// +// Caller takes ownership of returned std::list. +static std::list<IndependentElementSet>* +getAllIndependentConstraintsSets(const Query &query) { + std::list<IndependentElementSet> *factors = new std::list<IndependentElementSet>(); ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr); - if (CE){ - assert(CE && CE->isFalse() && - "the expr should always be false and therefore not included in factors"); + if (CE) { + assert(CE && CE->isFalse() && "the expr should always be false and " + "therefore not included in factors"); } else { ref<Expr> neg = Expr::createIsZero(query.expr); factors->push_back(IndependentElementSet(neg)); } for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) + ie = query.constraints.end(); + it != ie; ++it) { // iterate through all the previously separated constraints. Until we // actually return, factors is treated as a queue of expressions to be // evaluated. If the queue property isn't maintained, then the exprs // could be returned in an order different from how they came it, negatively // affecting later stages. factors->push_back(IndependentElementSet(*it)); - bool doneLoop = false; - do { - doneLoop = true; - std::list<IndependentElementSet> * done = new std::list<IndependentElementSet>; - while (factors->size() > 0){ - IndependentElementSet current = factors->front(); + } + + bool doneLoop = false; + do { + doneLoop = true; + std::list<IndependentElementSet> *done = + new std::list<IndependentElementSet>; + while (factors->size() > 0) { + IndependentElementSet current = factors->front(); + factors->pop_front(); + // This list represents the set of factors that are separate from current. + // Those that are not inserted into this list (queue) intersect with + // current. + std::list<IndependentElementSet> *keep = + new std::list<IndependentElementSet>; + while (factors->size() > 0) { + IndependentElementSet compare = factors->front(); factors->pop_front(); - // This list represents the set of factors that are separate from current. - // Those that are not inserted into this list (queue) intersect with current. - std::list<IndependentElementSet> *keep = new std::list<IndependentElementSet>; - while (factors->size() > 0){ - IndependentElementSet compare = factors->front(); - factors->pop_front(); - if (current.intersects(compare)){ - if (current.add(compare)){ - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - doneLoop = false; - } - } else { - keep->push_back(compare); - } - } - done->push_back(current); - delete factors; - factors = keep; + if (current.intersects(compare)) { + if (current.add(compare)) { + // Means that we have added (z=y)added to (x=y) + // Now need to see if there are any (z=?)'s + doneLoop = false; + } + } else { + keep->push_back(compare); + } } + done->push_back(current); + delete factors; + factors = keep; + } delete factors; factors = done; } while (!doneLoop); + + return factors; } static @@ -453,14 +463,14 @@ bool IndependentSolver::computeInitialValues(const Query& query, const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution){ - std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>; - // We assume the query has a solution except proven differently // This is important in case we don't have any constraints but // we need initial values for requested array objects. hasSolution = true; + // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't need + // to remember to manually call delete + std::list<IndependentElementSet> *factors = getAllIndependentConstraintsSets(query); - getAllIndependentConstraintsSets(query, factors); //Used to rearrange all of the answers into the correct order std::map<const Array*, std::vector<unsigned char> > retMap; for (std::list<IndependentElementSet>::iterator it = factors->begin(); @@ -477,9 +487,11 @@ bool IndependentSolver::computeInitialValues(const Query& query, if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor, tempValues, hasSolution)){ values.clear(); + delete factors; return false; } else if (!hasSolution){ values.clear(); + delete factors; return true; } else { assert(tempValues.size() == arraysInFactor.size() && |