search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Reference evaluator crashes when using `Float`'s `Literal` instance #1715

Closed RyanGlScott closed 3 months ago

RyanGlScott commented 3 months ago

Currently, the Cryptol reference evaluator can evaluate a Float value when using its FLiteral instance:

Float> :m Float
Loading module Cryptol
Loading module Float
Float> :eval 1.0 : Float64
0x1.0

But if you use Float's Literal instance, then the reference evaluator crashes:

Float> :eval 1 : Float64
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  65397a491bddc3b4e8f41053106ce8859387d662
  Branch:    release-3.1.0 (uncommited files present)
  Location:  [Reference Evaluator]literal
  Message:   TCon (TC TCFloat) [TCon (TC (TCNum 11)) [],TCon (TC (TCNum 53)) []] cannot represent literals
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Eval/Reference.lhs:1804:19 in cryptol-3.1.0-inplace:Cryptol.Eval.Reference
%< ---------------------------------------------------

Fixing this should be a simple matter of adding another case to the literal function.