Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Making proof_trace_parser and llvm_rewrite_trace_iterator use a shared_ptr of kore_header #1156

Merged
merged 1 commit into from
Oct 11, 2024

Conversation

Robertorosmaninho
Copy link
Collaborator

@Robertorosmaninho Robertorosmaninho commented Oct 11, 2024

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.

@Robertorosmaninho Robertorosmaninho self-assigned this Oct 11, 2024
@rv-jenkins rv-jenkins changed the base branch from master to develop October 11, 2024 19:03
@Robertorosmaninho Robertorosmaninho merged commit a8704ec into develop Oct 11, 2024
10 checks passed
@Robertorosmaninho Robertorosmaninho deleted the fix-parse-proof-iterator-issue branch October 11, 2024 20:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants