From: Andres Noetzli <noetzli@stanford.edu>
Date: Wed, 24 May 2017 20:28:58 +0000 (-0700)
Subject: Fix use-after-free with ResChains
X-Git-Tag: cvc5-1.0.0~5790
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a425613d5108efa5f623d075135f2e08d3dfde2;p=cvc5.git

Fix use-after-free with ResChains

This commit fixes an issue where the ResChain in `d_resolutionChains` gets
deleted here:

https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729

The condition immediately after is false because the condition on line 727 is
true. Thus, `d_resolutionChains` now has a deleted entry for `id`.

When CVC4 afterwards gets the ResChain associated with `id` in
`checkResolution()`, it accesses the deleted entry:

https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
---

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index bcc849906..eb4e04d13 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -728,8 +728,8 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) {
     ResChain<Solver>* current = (*d_resolutionChains.find(id)).second;
     delete current;
   }
-  if (d_resolutionChains.find(id) == d_resolutionChains.end())
-    d_resolutionChains.insert(id, res);
+
+  d_resolutionChains.insert(id, res);
 
   if (Debug.isOn("proof:sat")) {
     printRes(id);