search

NorfairKing / validity

Validity and validity-based testing
https://www.youtube.com/watch?v=eIs9qNh17SM
MIT License
156 stars 31 forks source link

Char should not be trivially valid #78

Closed lehins closed 4 years ago

lehins commented 4 years ago

Currently in validity Char is trivially valid. But if you check the chr function it is expected to be:

| isTrue# (int2Word# i# `leWord#` 0x10FFFF##) = C# (chr# i#)

While when read from memory only 31 bits are expected: readWideCharOffAddr#

In other words I can construct an invalid Char# that can mess things up:

λ> C# (chr# 2147483647#)
'\2147483647'
λ> chr 2147483647
*** Exception: Prelude.chr: bad argument: 2147483647

In fact it is possible to construct even larger 64bit Chars that are ven negative :slightly_smiling_face:

λ> C# (chr# 9223372036854775807#)
'\9223372036854775807'
λ> C# (chr# -9223372036854775808#)
'\-9223372036854775808'
NorfairKing commented 4 years ago

It looks like the maxBound is quite small:

ord (maxBound :: Char)
1114111

Certainly smaller than 31 bits:

logBase 2 $ fromIntegral $ ord (maxBound :: Char)
20.087461546321563

What happens if you pass a 2147483647 to readWideCharOffAddr#?

NorfairKing commented 4 years ago

@lehins I opened https://github.com/NorfairKing/validity/pull/79/files Could you have a look?

NorfairKing commented 4 years ago

This has been implemented in the layest release