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

Add ogFromParam to Cryptol URI when importing Cryptol names #1915

Merged
merged 4 commits into from
Aug 24, 2023
Merged

Conversation

qsctr
Copy link
Contributor

@qsctr qsctr commented Aug 23, 2023

SAW currently constructs a unique Cryptol URI for each Cryptol name by using the components of the module path and the identifier, but this fails for instantiations of parameterized modules which import multiple interfaces containing parameters with the same name. We fix this by incorporating the identifier from ogFromParam in the OrigName if present, which identifies which interface the name came from.

Fixes #1892.

(This is my first SAW PR so let me know if I did anything wrong)

@qsctr qsctr self-assigned this Aug 23, 2023
Copy link
Contributor

@RyanGlScott RyanGlScott left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well spotted!

It would be worth adding an integration test under the intTests/ subdirectory to make sure that this actually fixes the issue (and moreover, that the issue stays fixed in the future).

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs Show resolved Hide resolved
@qsctr qsctr added the ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully. label Aug 24, 2023
@mergify mergify bot merged commit 128e8f8 into master Aug 24, 2023
38 checks passed
@mergify mergify bot deleted the T1892 branch August 24, 2023 06:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Attempted to register the following name twice: cryptol:
2 participants