From ae4089fb6ff60fd5af5a212d68b91928f94bb5f2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Andres=20N=C3=B6tzli?= Date: Fri, 30 Jun 2017 11:39:17 -0700 Subject: [PATCH] Fix use-after-free with unsat cores/proofs (#174) In TSatProof::finalizeProof(), we got a clause from the clause allocator, called resolveUnit() and then size() on the clause. The problem is that resolveUnit() can reallocate memory (and there is even a comment warning about that in finalizeProof()), which invalidates the clause. This commit gets the clause again from the clause allocator before calling size(). --- src/proof/sat_proof_implementation.h | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 6cb10450a..44d98e88e 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -903,13 +903,11 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { ResChain* res = new ResChain(conflict_id); // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. - size_t conflict_size = getClause(conflict_ref).size(); - for (size_t i = 0; i < conflict_size; ++i) { + for (size_t i = 0; i < getClause(conflict_ref).size(); ++i) { const typename Solver::TClause& conflict = getClause(conflict_ref); typename Solver::TLit lit = conflict[i]; ClauseId res_id = resolveUnit(~lit); res->addStep(lit, res_id, !sign(lit)); - conflict_size = conflict.size(); } registerResolution(d_emptyClauseId, res); -- 2.30.2