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

[New module system] Attempt to import nonexistent interface submodule crashes #1440

Closed
WeeknightMVP opened this issue Sep 23, 2022 · 0 comments
Assignees
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules

Comments

@WeeknightMVP
Copy link

// T.cry
module T where
  submodule A where
    import interface submodule I
$ CRYPTOLPATH=../scratch ./cry run ../scratch/T.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99 (ddcc67b, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module T
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  bd55b9617dccb775134eaed5c2bcfca80fbad6ff
  Branch:    functors-merge (uncommited files present)
  Location:  getExternal
  Message:   Missing external name
             submodule Cryptol::I
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/ModuleSystem/Renamer/Monad.hs:432:34 in cryptol-2.13.0.99-inplace:Cryptol.ModuleSystem.Renamer.Monad

Similar errors for importing a nonexistent regular module or submodule within the top level module or a submodule are being caught, but importing a nonexistent interface causes a crash.

@yav yav added bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules labels Sep 23, 2022
@yav yav self-assigned this Sep 23, 2022
yav added a commit that referenced this issue Sep 24, 2022
When we find an undefined name we record an error,
but we also generate a fake name, so that we can continue
processing and report other errors.  It is important
that we don't try to use this fake name.

This commit corrects this behavior where we'd try to get
information about an undefined intrface submodule.

Fixes #1440
yav added a commit that referenced this issue Sep 29, 2022
@yav yav closed this as completed Oct 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

No branches or pull requests

2 participants