Fix use-after-free in eager bitblaster (#1772)

There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.

Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.

diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index d49c1f43241563cb7615c2f2d24c484c012c1140..08776e60d385ef1d677dd512725241c15bc4b322 100644 (file)
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -32,9 +32,9 @@ namespace bv {
 
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
     : TBitblaster<Node>(),
+      d_nullContext(new context::Context()),
       d_satSolver(),
       d_bitblastingRegistrar(new BitblastingRegistrar(this)),
-      d_nullContext(new context::Context()),
       d_cnfStream(),
       d_bv(theory_bv),
       d_bbAtoms(),

diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 8610d018123cc8e4f7498ce8b4fd72d3912fabf8..bea275c67b383b306116918a326c53ab53d2ab23 100644 (file)
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -55,11 +55,12 @@ class EagerBitblaster : public TBitblaster<Node>
   void setProofLog(BitVectorProof* bvp);
 
  private:
+  std::unique_ptr<context::Context> d_nullContext;
+
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
-  std::unique_ptr<context::Context> d_nullContext;
   std::unique_ptr<prop::CnfStream> d_cnfStream;
 
   TheoryBV* d_bv;