From: Andres Nötzli <andres.noetzli@gmail.com>
Date: Fri, 30 Jun 2017 18:39:17 +0000 (-0700)
Subject: Fix use-after-free with unsat cores/proofs (#174)
X-Git-Tag: cvc5-1.0.0~5752
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae4089fb6ff60fd5af5a212d68b91928f94bb5f2;p=cvc5.git

Fix use-after-free with unsat cores/proofs (#174)

In TSatProof<Solver>::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().
---

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<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
   ResChain<Solver>* res = new ResChain<Solver>(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);