Skip to content

Parsing meta-issue #327

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

Closed
dkcumming opened this issue Feb 21, 2024 · 1 comment
Closed

Parsing meta-issue #327

dkcumming opened this issue Feb 21, 2024 · 1 comment
Labels
mir-parser MIR syntax in K

Comments

@dkcumming
Copy link
Collaborator

This issue is intended to categorise the issues that are occurring with parsing for KMIR. 'Parsing' here may refer to the parsing of either the LLVM parser, or the Haskell parser. However 'parsing' is distinct from 'extraction' which is the process of accessing the MIR from the rust compiler in some format (--emit mir for textual MIR, a rustc_driver program for a JSON dump). Currently the only extraction KMIR uses is --emit mir for textual MIR.

Discrepancies between bison-glr parser and java parser handling ambiguities

Depending on which parser is used to run a test, the test may produce a different result
#235

Claim parser will stall on any IdentifierToken that isn't explicitly listed in the verification module or spec file

#320

Syntax for project is based on Rust surface language reference which differs from MIR internal and stable mir

Progress was made on this in the branch refactor/smir-syntax, however some challenges were encountered which inhibited merging including passing the test suite and handling the introduced ambiguities.

Parser hits unexpected tokens on stale branches

#171
#209

Conflicts in textual MIR

#54

Other issues with parsing I'm unsure how to categorise

#85
#86
#87
#90
#91
#92
#93
#315

@dkcumming dkcumming added the mir-parser MIR syntax in K label Feb 21, 2024
@yanliu18
Copy link
Contributor

@dkcumming thank you. This issue summarises well.
I think for issue #85 - 87, #90-93, they are refering to the exisiting syntax implementation and bison-glr parser issue.
We might probaly ignore them (but reference to these suggestions when problem was encountered) if new parser is to be implemented or if the syntax is refactored.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
mir-parser MIR syntax in K
Projects
None yet
Development

No branches or pull requests

2 participants