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

Create proof trace event for tail call information #1179

Merged
merged 10 commits into from
Dec 12, 2024
Merged

Conversation

theo25
Copy link
Collaborator

@theo25 theo25 commented Dec 9, 2024

This PR adds a new event that provides information on the way a function exits control, specifically whether it exits via a tail call or a conventional return statement. This event is added to assist in computing the call stack of the various simplifications from the proof trace hint.

@rv-jenkins rv-jenkins changed the base branch from master to develop December 9, 2024 19:19
@theo25 theo25 force-pushed the func-exit-hint branch 3 times, most recently from 35e6e56 to b4c6344 Compare December 10, 2024 19:28
@theo25 theo25 marked this pull request as ready for review December 10, 2024 21:22
Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have a couple low-level comments that I highlighted in the diff, but also one higher level comment: tail call info feels like a weird name for the event when it is emitted even in functions with no tail call. What if we just call it a function exit event?

lib/codegen/ProofEvent.cpp Outdated Show resolved Hide resolved
include/kllvm/codegen/ProofEvent.h Outdated Show resolved Hide resolved
@theo25 theo25 requested a review from dwightguth December 11, 2024 23:51
@theo25
Copy link
Collaborator Author

theo25 commented Dec 11, 2024

@dwightguth I addressed your comments. Could you take another look?

Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good but please double check what I commented on and fix it if my suspicions are correct.

lib/codegen/CreateTerm.cpp Outdated Show resolved Hide resolved
@dwightguth dwightguth enabled auto-merge (squash) December 12, 2024 21:26
@dwightguth dwightguth merged commit 6df5ac5 into develop Dec 12, 2024
10 checks passed
@dwightguth dwightguth deleted the func-exit-hint branch December 12, 2024 21:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants