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

Use same register for variables with the same id #1363

Closed
wants to merge 2 commits into from

Conversation

bugarela
Copy link
Collaborator

@bugarela bugarela commented Feb 8, 2024

Hello :octocat:

This fixes a problem I found recently when using multiple modules and no instances. Currently, our registers (which store values for state variables) are indexed by both the variable name and variable id. We already had some code ensuring that, if two variables have the same name (but a different id), they'd have the same register - this is important for instances, and flattening ensures that no two different state variables can have the same name.

Now, I'm adding a very similar piece of code to ensure variables with the same id get the same register, even if they have different names. This part is important for imports, since qualified imports can make it so the same variable is referred by different names.

I'm not confident this will work for all combinations of imports and instances, but it definitely covers more ground than what we currently have.

For testing, I just updated the existing imports.qnt example to have the complexity needed to hit the problem (fixed by this).

  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

@bugarela bugarela requested a review from shonfeder February 8, 2024 13:10
@bugarela bugarela self-assigned this Feb 8, 2024
@bugarela
Copy link
Collaborator Author

bugarela commented Feb 8, 2024

Ok, even though I fixed the scenario in the compiler, it still won't work in apalache. In order to make it work in apalache, we have to fix this in the flattener, which seems like the right thing to do now that I think about it.

I'll close this for now, and open an issue for the flattening problem instead.

@bugarela bugarela closed this Feb 8, 2024
@bugarela bugarela deleted the gabriela/fix-compilation-imported-variables branch May 22, 2024 11:08
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.

2 participants