From a8704ec079af06bf10bd3389ef1bf54f51b96862 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Fri, 11 Oct 2024 17:12:03 -0300 Subject: [PATCH] Making `proof_trace_parser` and `llvm_rewrite_trace_iterator` use a shared_ptr of `kore_header` (#1156) The Math Proof Team has had an issue with `llvm_rewrite_trace_iterator` where they start iteration in one function, and finish in another function, passing the iterator as an argument to this second function. This second function also generates an Iterable object that is then returned in the first function. This complex workflow was raising a `Python Segmentation Fault` on the call of `get_next_event` inside our `class LLVMRewriteTraceIterator`. After many hours of debugging, I reached a point where I discovered that the `arities_` of the `kore_header` object were corrupted, and then the parser threw a Segmentation Fault when trying to execute `get_arity`. I believe the Pybind deleted the `kore_header` object when the function finishes, as it was the only const ref on the function, and then when we tried to access it lazily using the Iterable object created by the MPG team, the memory where kore_header lived was already freed. By making it a `shared_ptr`, we ensure it's only deleted when the whole object is deleted, sharing the ownership of it with the C++ code. --- bindings/python/ast.cpp | 5 +++-- include/kllvm/binary/ProofTraceParser.h | 9 +++++---- lib/binary/ProofTraceParser.cpp | 9 +++++---- tools/kore-proof-trace/main.cpp | 2 +- 4 files changed, 14 insertions(+), 11 deletions(-) diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index 99ee92de9..f53d8a867 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -459,7 +459,7 @@ void bind_proof_trace(py::module_ &m) { .def_property_readonly("trace", &llvm_rewrite_trace::get_trace) .def_static( "parse", - [](py::bytes const &bytes, kore_header const &header) { + [](py::bytes const &bytes, std::shared_ptr &header) { proof_trace_parser parser(false, false, header); auto str = std::string(bytes); return parser.parse_proof_trace(str, false); @@ -486,7 +486,8 @@ void bind_proof_trace(py::module_ &m) { .def("__repr__", print_repr_adapter(true)) .def_static( "from_file", - [](std::string const &filename, kore_header const &header) { + [](std::string const &filename, + std::shared_ptr const &header) { std::ifstream file(filename, std::ios_base::binary); return llvm_rewrite_trace_iterator( std::make_unique(std::move(file)), diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h index 72acf18d4..93912c4b9 100644 --- a/include/kllvm/binary/ProofTraceParser.h +++ b/include/kllvm/binary/ProofTraceParser.h @@ -328,7 +328,7 @@ class proof_trace_parser { private: bool verbose_; bool expand_terms_; - [[maybe_unused]] kore_header const &header_; + [[maybe_unused]] std::shared_ptr header_; [[maybe_unused]] std::optional kore_definition_ = std::nullopt; @@ -342,7 +342,7 @@ class proof_trace_parser { || magic[3] != '2') { return nullptr; } - auto result = detail::read_v2(buffer, header_, pattern_len); + auto result = detail::read_v2(buffer, *header_, pattern_len); pattern_len += 4; return result; } @@ -701,7 +701,7 @@ class proof_trace_parser { public: proof_trace_parser( - bool verbose, bool expand_terms, kore_header const &header, + bool verbose, bool expand_terms, std::shared_ptr header, std::optional kore_definition = std::nullopt); std::optional parse_proof_trace_from_file( @@ -723,7 +723,8 @@ class llvm_rewrite_trace_iterator { public: llvm_rewrite_trace_iterator( - std::unique_ptr buffer, kore_header const &header); + std::unique_ptr buffer, + std::shared_ptr header); [[nodiscard]] uint32_t get_version() const { return version_; } std::optional get_next_event(); void print( diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp index b0b42ddea..7e92a0219 100644 --- a/lib/binary/ProofTraceParser.cpp +++ b/lib/binary/ProofTraceParser.cpp @@ -130,9 +130,10 @@ void llvm_event::print( } llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator( - std::unique_ptr buffer, kore_header const &header) + std::unique_ptr buffer, + std::shared_ptr header) : buffer_(std::move(buffer)) - , parser_(false, false, header) { + , parser_(false, false, std::move(header)) { if (!proof_trace_parser::parse_header(*buffer_, kind_, version_)) { throw std::runtime_error("invalid header"); } @@ -250,11 +251,11 @@ void llvm_rewrite_trace::print( } proof_trace_parser::proof_trace_parser( - bool verbose, bool expand_terms, kore_header const &header, + bool verbose, bool expand_terms, std::shared_ptr header, std::optional kore_definition) : verbose_(verbose) , expand_terms_(expand_terms) - , header_(header) + , header_(std::move(header)) , kore_definition_(std::move(kore_definition)) { } std::optional proof_trace_parser::parse_proof_trace( diff --git a/tools/kore-proof-trace/main.cpp b/tools/kore-proof-trace/main.cpp index df5dfc7d5..68f10ed7a 100644 --- a/tools/kore-proof-trace/main.cpp +++ b/tools/kore-proof-trace/main.cpp @@ -51,7 +51,7 @@ int main(int argc, char **argv) { cl::ParseCommandLineOptions(argc, argv); FILE *in = fopen(header_path.getValue().c_str(), "r"); - kore_header header(in); + auto header = std::make_shared(in); fclose(in); if (use_streaming_parser) {