Making proof_trace_parser and llvm_rewrite_trace_iterator use a s…

…hared_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

@@ -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<kore_header> &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<llvm_rewrite_trace_iterator>(true))
       .def_static(
           "from_file",
-          [](std::string const &filename, kore_header const &header) {
+          [](std::string const &filename,
+             std::shared_ptr<kore_header> const &header) {
             std::ifstream file(filename, std::ios_base::binary);
             return llvm_rewrite_trace_iterator(
                 std::make_unique<proof_trace_file_buffer>(std::move(file)),

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<kore_header> header_;
   [[maybe_unused]] std::optional<kore_definition> 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<kore_header> header,
       std::optional<kore_definition> kore_definition = std::nullopt);
 
   std::optional<llvm_rewrite_trace> parse_proof_trace_from_file(
@@ -723,7 +723,8 @@ class llvm_rewrite_trace_iterator {
 
 public:
   llvm_rewrite_trace_iterator(
-      std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header);
+      std::unique_ptr<proof_trace_buffer> buffer,
+      std::shared_ptr<kore_header> header);
   [[nodiscard]] uint32_t get_version() const { return version_; }
   std::optional<annotated_llvm_event> get_next_event();
   void print(

lib/binary/ProofTraceParser.cpp

@@ -130,9 +130,10 @@ void llvm_event::print(
 }
 
 llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
-    std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header)
+    std::unique_ptr<proof_trace_buffer> buffer,
+    std::shared_ptr<kore_header> 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<kore_header> header,
     std::optional<kore_definition> kore_definition)
     : verbose_(verbose)
     , expand_terms_(expand_terms)
-    , header_(header)
+    , header_(std::move(header))
     , kore_definition_(std::move(kore_definition)) { }
 
 std::optional<llvm_rewrite_trace> proof_trace_parser::parse_proof_trace(

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<kore_header>(in);
   fclose(in);
 
   if (use_streaming_parser) {