runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
36 stars 23 forks source link

Making `proof_trace_parser` and `llvm_rewrite_trace_iterator` use a shared_ptr of `kore_header` #1156

Closed Robertorosmaninho closed 1 month ago

Robertorosmaninho commented 1 month ago

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.