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.

diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index a54d72d3f6b359b0345afd6f9051194a927d2ea0..ccb288f6e4c6941dcb7f006886c0991f53b07483 100644 (file)
--- 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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a0939f4dbff2eb2dfe9c160d32bfe92d5089abef..6814ad5310bc4c2685236774510365a696294cf9 100644 (file)
--- 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;