AddKoreAttribute as a Frontend Kompiler Pass #3522

Robertorosmaninho · 2023-07-18T18:50:20Z

Part of #3444

This PR creates a new compiler pass that adds the Kore attributes to productions before ModuleToKore. This is part of the effort to refactor the ModuleToKore infrastructure to simplify it by decoupling functions and actions that can be done before the translation and that aren't related to (kore) code emission.

Besides extracting the AddKoreAttrubutes function from ModuleToKore.java, this PR also simplifies function calls such as isFunctional and isConstructor only to test if the attribute is present on the given production.

…eBackend.java`

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

Robertorosmaninho · 2023-07-18T18:57:46Z

I'm currently blocked on the two pending issues mentioned above.
I'm testing it with this test as it was one of the first from regression-new to fail within this implementation.

The definition.kore reflect the second issue, as the symbols don't contain the appropriate attributes inserted by the AddKoreAttributes pass.

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java

dwightguth · 2023-07-18T20:24:51Z

As far as the issue with the module transformer is concerned, it is a known issue that passes that only edit the attributes of sentences in a module get cached incorrectly by the code that helps cache module transformations, as a result of which the changes to the attribute get discarded.

You have two options:

In a separate PR, try to fix the issue with module attribute caching. I don't remember exactly why I had trouble doing this when I tried, but I remember it wasn't as easy as I hoped it would be.
Bundle this pass together in the same module transformer as another change that edits something other than the attributes of every module it edits attributes in. This will bypass the issue with caching and correctly give back the right info.

Robertorosmaninho · 2023-07-18T22:44:11Z

As far as the issue with the module transformer is concerned, it is a known issue that passes that only edit the attributes of sentences in a module get cached incorrectly by the code that helps cache module transformations, as a result of which the changes to the attribute get discarded.

You have two options:

In a separate PR, try to fix the issue with module attribute caching. I don't remember exactly why I had trouble doing this when I tried, but I remember it wasn't as easy as I hoped it would be.

That's interesting, could you provide me with more details about it?

When/how did you face this issue before?
What have you tried?
How do we cache these module transformations?

Robertorosmaninho · 2023-07-19T15:20:51Z

Blocked on #3523.
We need to fix the Transformation caching to update the modules when we only modify the sentence attributes!

… the uses if `isConstructor` and `isFunction`

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java

radumereuta

lgtm, but I would like it if someone else could have a look.

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java

Modifying function calls signatures Simplifying ModuleToKore

This reverts commit 4db2ccb.

* Revert "AddKoreAttribute as a Frontend Kompiler Pass (#3522)" This reverts commit 4db2ccb. * Update test-pr.yml Testing public runners * Update test-pr.yml

…3187) * haskell-backend/src/main/native/haskell-backend: 2c1ff15bd - Export z3 overlay alone in flake (#3519) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 93a705112 - [#3493] Add total attribute (#3505) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: bd61a0565 - kore-rpc Catch any runtime exception and send as error (#3522) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 2020ceb1b - Fixing new nix update breaking cachix installation (#3526) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 37f122964 - [#3493] Rename `Fl` (functional) by `T` (total) (#3521) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 1c184832b - [#3523] Put unserialized definition.kore in bug report (#3527) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 559424aa4 - InfoAttemptUnification to DebugAttemptUnification (#3525) * Sync flake inputs to submodules * Fix `Dockerfile` * Fix another `Dockerfile` * Update result for failing test The rename from functional to total changed these outputs --------- Co-authored-by: rv-jenkins <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: Tamas Toth <tamas.toth@runtimeverification.com> Co-authored-by: Radu Mereuta <headness13@gmail.com>

Create AddKoreAttribute class and add it as a compiler pass in `Kor…

53fc010

…eBackend.java`

Robertorosmaninho commented Jul 18, 2023

View reviewed changes

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java Outdated Show resolved Hide resolved

Robertorosmaninho commented Jul 18, 2023

View reviewed changes

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java Outdated Show resolved Hide resolved

dwightguth reviewed Jul 18, 2023

View reviewed changes

Robertorosmaninho self-assigned this Jul 19, 2023

Robertorosmaninho added enhancement module-to-kore labels Jul 19, 2023

Robertorosmaninho added 6 commits July 19, 2023 15:04

Cleaning comments and AddKoreAttributes call on KoreBackend

94ea928

Refactoring ModuleToKORE.java to delete unused functions and simplify…

0fb740e

… the uses if `isConstructor` and `isFunction`

Using old SentenceTransformer

da92ba0

Merge branch 'develop' into AddKoreAttributesPass

53f7918

Using new SentenceTransformerAtt

1510a40

Assing Copyright header

237d19c

Robertorosmaninho added refactor java Pull requests that update Java code labels Jul 21, 2023

Robertorosmaninho added 4 commits July 24, 2023 13:32

Applying pass only to mainModule

1fec618

Merge branch 'develop' into AddKoreAttributesPass

e20a90c

Fix Typo

15fe67f

Deleting unused sorted rules and creating new ModuleTransformer

005b15b

Robertorosmaninho marked this pull request as ready for review July 24, 2023 19:03

Robertorosmaninho requested review from dwightguth, radumereuta and Scott-Guest July 24, 2023 19:03

Robertorosmaninho commented Jul 24, 2023

View reviewed changes

kernel/src/main/java/org/kframework/compile/AddKoreAttributes.java Outdated Show resolved Hide resolved

radumereuta approved these changes Jul 25, 2023

View reviewed changes

Merge branch 'develop' into AddKoreAttributesPass

20e7335

dwightguth requested changes Jul 25, 2023

View reviewed changes

Robertorosmaninho added 5 commits July 25, 2023 14:15

Deleting dead functions

e8c18ba

Creating production functions and functionRules definition in Module

4e06280

Modifying function calls signatures Simplifying ModuleToKore

Defining isRealHook on module and deleting duplicated implementations

3a4e87e

Fixing Scala issue

a2e4ffc

Deleting unused imports in outer.scala

6304e53

Robertorosmaninho requested a review from dwightguth July 25, 2023 18:52

Robertorosmaninho added 2 commits July 25, 2023 16:38

Simplifying functions, if-conditions and deleting unused imports

9258dcb

Merge branch 'develop' into AddKoreAttributesPass

5c195fc

dwightguth approved these changes Jul 26, 2023

View reviewed changes

Robertorosmaninho added the automerge label Jul 26, 2023

rv-jenkins merged commit 4db2ccb into develop Jul 26, 2023

rv-jenkins deleted the AddKoreAttributesPass branch July 26, 2023 14:02

Robertorosmaninho added a commit that referenced this pull request Aug 1, 2023

Revert "AddKoreAttribute as a Frontend Kompiler Pass (#3522)"

6ad412b

This reverts commit 4db2ccb.

Robertorosmaninho mentioned this pull request Aug 1, 2023

Revert "AddKoreAttribute as a Frontend Kompiler Pass" #3554

Merged

Robertorosmaninho mentioned this pull request Aug 24, 2023

Ordering instance for Sentences #3590

Merged

Baltoli mentioned this pull request Dec 12, 2023

2023 Goals #3098

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

AddKoreAttribute as a Frontend Kompiler Pass #3522

AddKoreAttribute as a Frontend Kompiler Pass #3522

Robertorosmaninho commented Jul 18, 2023 •

edited

Loading

Robertorosmaninho commented Jul 18, 2023

dwightguth commented Jul 18, 2023

Robertorosmaninho commented Jul 18, 2023

Robertorosmaninho commented Jul 19, 2023

radumereuta left a comment

AddKoreAttribute as a Frontend Kompiler Pass #3522

AddKoreAttribute as a Frontend Kompiler Pass #3522

Conversation

Robertorosmaninho commented Jul 18, 2023 • edited Loading

Robertorosmaninho commented Jul 18, 2023

dwightguth commented Jul 18, 2023

Robertorosmaninho commented Jul 18, 2023

Robertorosmaninho commented Jul 19, 2023

radumereuta left a comment

Choose a reason for hiding this comment

Robertorosmaninho commented Jul 18, 2023 •

edited

Loading