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

Check that tokens are non-empty after #Layout #4595

Open
Scott-Guest opened this issue Aug 20, 2024 · 0 comments
Open

Check that tokens are non-empty after #Layout #4595

Scott-Guest opened this issue Aug 20, 2024 · 0 comments
Assignees

Comments

@Scott-Guest
Copy link
Contributor

Related to #4592

Check that, after removing all tokens matching #Layout, every token is still a non-empty regular expression, preventing bugs like

syntax #Layout ::= r"([\\n \\ \\r\\t])"
syntax Stmt ::= List{Int, " "}

where the list separator will never actually be matched because #Layout strips all white-space.

Explicitly, let L be the #Layout regex and S a token. We must check that (~(*L*))&S is non-empty where ~ is negation, * is Kleene star, and & is intersection.

@Scott-Guest Scott-Guest self-assigned this Aug 20, 2024
rv-jenkins added a commit that referenced this issue Aug 22, 2024
Closes #4592

Previously, we trimmed list separators, presumably under the assumption
that `#Layout` deletes all whitespace and the user may end up including
redundant whitespace. This is hacky and a faulty assumption given that
we allow custom `#Layout`.

For now, we just remove the `trim()` call. This shouldn't cause issues
downstream - I've manually checked that all `List{...}` and
`NeList{...}` declarations in the EVM, C, and WASM semantics are already
correct. If anything was missed, it's an easy fix.

A proper solution is described in #4595

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
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

No branches or pull requests

1 participant