Deprecate symbol and klabel
#4045
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
|
Baltoli
force-pushed
the
deprecate-symbol-klabel
branch
from
fec6c79 to
2495800
Compare
This was referenced Mar 15, 2024
rv-jenkins
pushed a commit
to runtimeverification/haskell-backend
that referenced
this pull request
Mar 20, 2024
) See #3742 for full context; this PR adds a backwards-compatible check for `symbol'Kywd` as well as `klabel` for the pseudo-builtin sorts `Endianness` and `Signedness`. When this is merged, I'll be able to finish working on runtimeverification/k#4045. Then, when that PR lands, the frontend will no longer emit `klabel(_)` to KORE, and we can safely remove the backwards-compatible part of this PR. The integration test suite's checked-in KORE files are all updated to use the new attribute rather than the old one, but the tests that use K to compile fresh KORE will still be using `klabel(_)` until the dependency update job induced by the changes above goes through. I have verified manually that building K with this HB commit allows the failing integration test in #3742 to pass. Thanks @jberthold for the suggestions! ~~The implementation here would ideally be made backwards-compatible; my version induces a dependency loop (hence failing tests, it would need an update to the K dependency to go through first for the integration test suite to pass).~~
|
|
rv-jenkins
pushed a commit
that referenced
this pull request
Mar 26, 2024
When working on #4045, I identified a case in the C Semantics where an overload set was flagged as being singletons (that is, that the productions in the set were not actually overloads of one another). Despite this warning, removing the `overload(_)` attributes broke compilation by producing a parsing ambiguity. It turns out that the issue was a difference between the main module and the _disambiguation module_ produced during the inner parsing process. The disambiguation module adds an additional production ``` Es ::= E ``` for user list sorts `Es` that subsorts the list element sort into the list sort. This means that two productions ``` S ::= f(Es) T ::= f(E) ``` can be overloads of one another. However, this check was only using the overloads induced by the main module and not those used by the disambiguation module. The fix is simply to compute the disambiguation module[^1] and use its overloads for the checks. Doing so requires some changes to the plumbing; the subsorting production is previously only added when `RULE-LISTS` is imported, but we need to short-circuit that code path in this context. This PR includes a regression test minimised from the original example. [^1]: I tried a cheaper fix that just checks parameters of overload-attributed productions to see if they appear in a user list, but this isn't sufficiently general in the case where the overload parameter is actually a sub-/supersort of the user list element, as happens in the C semantics.
rv-jenkins
pushed a commit
that referenced
this pull request
Mar 27, 2024
When working on #4045, I noticed that a pair of productions like: ```k syntax KItem ::= disambiguate(KItem, KItem) [overload(disambiguate)] | disambiguate(List, Set) [overload(disambiguate)] ``` were both being incorrectly flagged as singleton overloads, despite meeting the criteria for being an overload set. Some investigation reveals that this is due to the overload lattice checks being applied _before_ the compiler inserts subsorting productions into `KItem` for every sort; we therefore don't know that `List <: KItem` when constructing the overload lattice. The solution is to move the overload checks later in the compilation process, after the compilation pipeline has been run. This PR makes that change, along with some associated documentation and renaming for clarity. It also includes a regression test with the example above; I have verified that the test breaks before this PR.
Baltoli
force-pushed
the
deprecate-symbol-klabel
branch
from
0bf16a2 to
60ad675
Compare
tothtamas28
approved these changes
Jul 4, 2024
Merged
rv-jenkins
pushed a commit
that referenced
this pull request
Jul 10, 2024
Related: * #4045 * runtimeverification/kontrol#679 Changes: * Remove `Atts.KLABEL` * Make `Atts.SYMBOL` unary
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR implements @tothtamas28's warning messages for usages of the deprecated
klabel(_)andsymbolattributes (which can now be unambiguously replaced bysymbol(_)andoverload(_)).The actual code changes are pretty minimal, but we need to do a bunch of updates on test cases and related output to keep tests passing. Additionally, we have pre-merged downstream PRs to make sure other projects are not subjected to noisy compiler output as a result of making this change:
Downstream updates:
symbolandklabel(_)evm-semantics#2378klabelattribute wasm-semantics#666klabelattribute mx-semantics#298klabelattribute kasmer-multiversx#168klabel)klabelattribute blockchain-k-plugin#184