From 63fb4e8c33db706589fe41476c4d3358fb47164e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 6 Dec 2018 15:23:00 -0800 Subject: [PATCH] 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` 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. --- src/proof/resolution_bitvector_proof.h | 3 ++- src/smt/smt_engine.cpp | 21 ++++++++++++--------- 2 files changed, 14 insertions(+), 10 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 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a0939f4db..6814ad531 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1071,6 +1071,18 @@ SmtEngine::~SmtEngine() //destroy all passes before destroying things that they refer to d_private->cleanupPreprocessingPasses(); + // d_proofManager is always created when proofs are enabled at configure + // time. Because of this, this code should not be wrapped in PROOF() which + // additionally checks flags such as options::proof(). + // + // Note: the proof manager must be destroyed before the theory engine. + // Because the destruction of the proofs depends on contexts owned be the + // theory solvers. +#ifdef CVC4_PROOF + delete d_proofManager; + d_proofManager = NULL; +#endif + delete d_theoryEngine; d_theoryEngine = NULL; delete d_propEngine; @@ -1078,15 +1090,6 @@ SmtEngine::~SmtEngine() delete d_decisionEngine; d_decisionEngine = NULL; - -// d_proofManager is always created when proofs are enabled at configure time. -// Becuase of this, this code should not be wrapped in PROOF() which -// additionally checks flags such as options::proof(). -#ifdef CVC4_PROOF - delete d_proofManager; - d_proofManager = NULL; -#endif - delete d_stats; d_stats = NULL; delete d_statisticsRegistry; -- 2.30.2