search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
438 stars 63 forks source link

scCryptolType: unsupported type sort 0 #1248

Open msaaltink opened 4 years ago

msaaltink commented 4 years ago

Executing

let bv64 = parse_core "bitvector 32";

results in

[17:36:02.544] You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< --------------------------------------------------- 
  Revision:  cff300fce2caaf4be678bfdab8c8e3ade93d020f
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type sort 0
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-7NBapC0zhks5IhYxksTPfp:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1400:19 in cryptol-saw-core-0.1-7NBapC0zhks5IhYxksTPfp:Verifier.SAW.Cryptol
%< ---------------------------------------------------
ghost commented 3 years ago

Stumbled across this with Prelude.Nat as well:

$ saw
version 0.7 (670e349-dirty)

sawscript> parse_core "4"

You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< --------------------------------------------------- 
  Revision:  f61023ebbb34c2d6acbda9fc2eb2d0ba0884604c
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type Prelude.Nat
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-Bsnj23LjNlkEA2Ker1hOsY:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1540:19 in cryptol-saw-core-0.1-Bsnj23LjNlkEA2Ker1hOsY:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

sawscript>
RyanGlScott commented 3 years ago

I believe this is fixed now? On a recent checkout of master, neither of the following appear to crash:

sawscript> parse_core "Vec 32 Bool"
[15:37:21.828] Prelude.Vec 32 Prelude.Bool
sawscript> parse_core "4"
[15:37:23.726] 4

(I'm assuming that bitvector n is an alias for Vec n Bool.)

robdockins commented 3 years ago

Yes, this was fixed via #1336. It's probably worthwhile to keep this ticket open until we add a test case.