From 0a425613d5108efa5f623d075135f2e08d3dfde2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 24 May 2017 13:28:58 -0700 Subject: [PATCH] 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 --- src/proof/sat_proof_implementation.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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::registerResolution(ClauseId id, ResChain* res) { ResChain* 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); -- 2.30.2