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

not a sequence panic involving empty sequences #1749

Closed
RyanGlScott opened this issue Sep 10, 2024 · 0 comments · Fixed by #1750
Closed

not a sequence panic involving empty sequences #1749

RyanGlScott opened this issue Sep 10, 2024 · 0 comments · Fixed by #1750
Labels
bug Something not working correctly

Comments

@RyanGlScott
Copy link
Contributor

The following program causes Cryptol to panic when evaluated:

// Main.cry

f : [0] -> [inf][0]
f = split

main : [0]
main = (f []) @ 0
$ ~/Software/cryptol-3.2.0/bin/cryptol Main.cry -c 'main'
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  1bcb75c5be92034b7b29155ab1f5d72780838605
  Branch:    release-3.2.0 (uncommited files present)
  Location:  [Eval] fromSeq
  Message:   not a sequence
             splitV
             word:0
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.2.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.2.0-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:413:18 in cryptol-3.2.0-inplace:Cryptol.Eval.Value
%< ---------------------------------------------------
@RyanGlScott RyanGlScott added the bug Something not working correctly label Sep 10, 2024
@RyanGlScott RyanGlScott changed the title not a sequence panic involving empty lists not a sequence panic involving empty sequences Sep 10, 2024
RyanGlScott added a commit that referenced this issue Sep 10, 2024
Previously, `splitV` would assume that if you were splitting a value `val` into
something of type `[inf][each]`, then `val` must be a stream of type of `[inf *
each]` (i.e., of type `[inf]`). This is not true in the corner case where
`each` equals `0`, however. In that case, `val` is of type `[0]`, which is a
word, not a stream. As such, we need to ensure that we do not call `fromSeq` on
`val`, which crashes if `val` is not a stream or sequence.

Fixes #1749.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant