diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-05-24 13:28:58 -0700 |
|---|---|---|
| committer | Andres Nötzli <andres.noetzli@gmail.com> | 2017-05-26 01:47:00 -0700 |
| commit | 0a425613d5108efa5f623d075135f2e08d3dfde2 (patch) | |
| tree | 041568ac9d317a6672c81f730d6d7f512248cc83 | |
| parent | 97443967555b0e7fe6be4e6ab03b81383bc90430 (diff) | |
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
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 4 |
1 files 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<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); |