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

Replacement parser kernel #2566

Merged
merged 20 commits into from
May 18, 2022
Merged

Replacement parser kernel #2566

merged 20 commits into from
May 18, 2022

Conversation

dwightguth
Copy link
Collaborator

@dwightguth dwightguth commented Apr 28, 2022

This PR essentially deletes the "parser" part of the parser kernel and replaces it with a new parser algorithm which is easier to understand and maintain. It also includes several smaller refactorings that arose during this process. Functionally, the old and new parser kernels behave identically. In terms of performance, on its own, the new parser kernel may be slower than the old one in a few cases, but in those cases which we have observed, there is usually a very massive nest of ambiguities, which we are able to postprocess faster due to the changes in the commit titled "move all priority filters into a single pass for performance". Overall the time spent parsing in large semantics is on par or faster with this branch on all the semantics I have tested.

I tried very hard to document the new algorithm so if anything is hard to follow, please let me know and I can add additional documentation. Bear in mind it's not likely to be completely understandable without reading the two papers I linked to in the javadoc of the EarleyParser class, though.

This has been tested against EVM, WASM, Michelson, and C in addition to the regression test suite.

@dwightguth dwightguth force-pushed the new-parser branch 6 times, most recently from 048fd1a to 4c7797f Compare May 2, 2022 21:51
@dwightguth dwightguth force-pushed the new-parser branch 3 times, most recently from f557283 to 3f2dfc5 Compare May 2, 2022 23:03
@dwightguth dwightguth marked this pull request as ready for review May 3, 2022 17:20
Copy link
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

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

This file can also be deleted: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/utils/algorithms/SCCTarjan.java

Overall pretty good. Indeed seems more straightforward. The previous implementation had other things in mind which didn't get implemented. The code seemed obfuscated because of that.

@dwightguth dwightguth requested a review from radumereuta May 17, 2022 23:54
@dwightguth dwightguth merged commit 8b2e215 into master May 18, 2022
@dwightguth dwightguth deleted the new-parser branch May 18, 2022 21:01
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