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

SAW core import fails for modules with overlapping imports #1419

Open
eddywestbrook opened this issue Aug 17, 2021 · 0 comments
Open

SAW core import fails for modules with overlapping imports #1419

eddywestbrook opened this issue Aug 17, 2021 · 0 comments

Comments

@eddywestbrook
Copy link
Contributor

SAW core cannot currently handle a "module diamond", i.e., importing two modules which both import the same module. As a simplified example, if you start a SAW core file with

import Prelude; import Cryptol;

you will get the error

internal: Duplicate name "Array" being inserted into module linked_list

The issue appears to be that insImport in Verifier.SAW.Module calls insResolvedName on all names that are in scope in a module when that module is imported, including the names that module imports from other modules, and insResolvedName gets mad when the same name is inserted twice.

I think the easiest fix would be to make insResolvedName idempotent, so that two ResolvedNames with the same textual name can be added to the same module as long as they are equal. Another possibility would be to change either the calls to insImport or insImport itself to filter out ResolvedNames that are already in a module.

@brianhuffman brianhuffman removed their assignment Apr 28, 2022
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

2 participants