From 84ead159cfbb76c8a6195ed2a64102529a84bdac Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 13 Apr 2018 18:22:11 -0700 Subject: [PATCH] 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. --- src/theory/bv/bitblast/eager_bitblaster.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.h | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index d49c1f432..08776e60d 100644 --- 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(), + 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 8610d0181..bea275c67 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -55,11 +55,12 @@ class EagerBitblaster : public TBitblaster void setProofLog(BitVectorProof* bvp); private: + std::unique_ptr d_nullContext; + typedef std::unordered_set TNodeSet; // sat solver used for bitblasting and associated CnfStream std::unique_ptr d_satSolver; std::unique_ptr d_bitblastingRegistrar; - std::unique_ptr d_nullContext; std::unique_ptr d_cnfStream; TheoryBV* d_bv; -- 2.30.2