edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

SegmentFault on String #379

Closed andylokandy closed 4 years ago

andylokandy commented 4 years ago

Steps to Reproduce

module Main

import Data.String.Extra

thisGoesWrong : String
thisGoesWrong = (join "a" []) ++ ""

main : IO ()
main = putStrLn $ thisGoesWrong

Expected Behavior

Output ""

Observed Behavior

If I eval thisGoesWrong in repl, the compiler will throw segment fault; if I execute main, the compiler throws Exception in substring: 1 and 0 are not valid start/end indices for "".

Both (join "a" []) and "" ++ "" are fine, but it breaks when they come together.

edwinb commented 4 years ago

It looks like the substring primitive doesn't check bounds properly, resulting in a dodgy string. Chez throws an exception in this case, and C crashes. The primitive should probably return an empty string in these cases rather than crash.