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

aslt changes + grammar + testing #53

Merged
merged 21 commits into from
Mar 18, 2024
Merged

aslt changes + grammar + testing #53

merged 21 commits into from
Mar 18, 2024

Conversation

katrinafyi
Copy link
Member

@katrinafyi katrinafyi commented Mar 11, 2024

This PR will aim to address some inconveniences in the current aslt format (i.e. that from the AST's pp_raw methods). This should make the syntax more similar to a regular programming language (in particular, Python) and hence easier to parse with a variety of generic tools.

In the format itself,

  • Format integer literals with a prefix (e.g. 0x) and without wrapping in Expr_Lit*.
    • Possibly, strip non-digit characters when emitting.
  • Wrap identifiers (e.g. function identifiers) in double quotes, denoting them as strings.
  • Format else branches consistently (done in match raw pretty printing of optional_else and indented_block #51).
  • Investigate unnecessary parentheses.
  • Investigate use of space and semicolon delimited lists.

In the ANTLR grammar,

In downstream projects,

@mmcloughlin
Copy link

In case it's of interest, I'm working on a Rust parser for ASLT (based on pest). It's a work in progress but it parses a reasonable subset right now.

@katrinafyi
Copy link
Member Author

@mmcloughlin, that is interesting! Do you have plans to make use of ASLp for a verification project?

@mmcloughlin
Copy link

Do you have plans to make use of ASLp for a verification project?

Potentially, yes. I'm trying to see if it will work for our use case at the moment. The ASLT format is quite convenient.

The other thing we'll probably need is symbolic opcodes #52.

@katrinafyi katrinafyi force-pushed the aslt-changes branch 6 times, most recently from 761e7d5 to 27ff528 Compare March 13, 2024 06:51
This was linked to issues Mar 13, 2024
@mmcloughlin
Copy link

I've updated my Rust parser to support these new changes. All works fine.

@katrinafyi katrinafyi marked this pull request as ready for review March 14, 2024 05:42
@katrinafyi katrinafyi mentioned this pull request Mar 15, 2024
@katrinafyi
Copy link
Member Author

katrinafyi commented Mar 15, 2024

With the go-ahead of the Basil PR, this is scheduled for merge next Monday.

@katrinafyi
Copy link
Member Author

@ncough Are the changes in this diff to be expected? It looks like some more CSE and some distributivity simplifications have been added?

@ncough
Copy link
Collaborator

ncough commented Mar 18, 2024

Yeah, these should correspond to some simplifications over mul_int and add_int that were necessary to reduce bitvector slices down to a constant width. Given the resulting CSE mess, I may consider an alternative approach down the line. Nice to have this testing!

@katrinafyi katrinafyi changed the title aslt format changes aslt changes + grammar + testing Mar 18, 2024
@katrinafyi katrinafyi merged commit 8828e86 into partial_eval Mar 18, 2024
1 of 2 checks passed
@katrinafyi katrinafyi deleted the aslt-changes branch March 19, 2024 02: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.

adopt aslt grammar into this repository testing of semantics output
3 participants