diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-06 15:23:00 -0800 |
---|---|---|
committer | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-06 15:23:00 -0800 |
commit | 63fb4e8c33db706589fe41476c4d3358fb47164e (patch) | |
tree | 75a4545317546c97d2578474ced2879b157f471c /src/proof | |
parent | 7145d0772794013fd6eb2f145a43a30be64aa557 (diff) |
Fix use-after-free due to destruction order (#2739)
A test for PR #2737 was failing even though the PR only added dead code.
This PR fixes the issue by fixing two use-after-free bugs:
- `ResolutionBitVectorProof` has a `Context` and a
`std::unique_ptr<BVSatProof>` member. The `BVSatProof` depends on the
`Context` and tries to access it (indirectly) in its constructor but
because the context was declared after the proof, the context was
destroyed before the proof, leading to a use-after-free in a method
called from the proof's destructor. This commit reorders the two
members.
- `TLazyBitblaster` was destroyed before the `LFSCCnfProof` in
`BitVectorProof` because `SmtEngine`'s destructor first destroyed the
theory engine and then the proof manager. This lead to a use-after-free
because `LFSCCnfProof` was using the `d_nullContext` of
`TLazyBitblaster`, which got indirectly accessed in `LFSCCnfProof`'s
destructor. This commit moves the destruction of `ProofManager` above
the destruction of the theory engine.
The issues were likely introduced by #2599. They went undetected because
our nightlies' ASAN check does not use proofs due to known memory leaks
in the proof module of CVC4.
I have tested this PR up to regression level 2 with ASAN with leak
detection disabled.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/resolution_bitvector_proof.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h index a54d72d3f..ccb288f6e 100644 --- a/src/proof/resolution_bitvector_proof.h +++ b/src/proof/resolution_bitvector_proof.h @@ -98,6 +98,8 @@ class ResolutionBitVectorProof : public BitVectorProof void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override; protected: + context::Context d_fakeContext; + // The CNF formula that results from bit-blasting will need a proof. // This is that proof. std::unique_ptr<BVSatProof> d_resolutionProof; @@ -105,7 +107,6 @@ class ResolutionBitVectorProof : public BitVectorProof bool d_isAssumptionConflict; theory::TheoryId getTheoryId() override; - context::Context d_fakeContext; }; class LFSCBitVectorProof : public ResolutionBitVectorProof |