9db52c7fa6
This PR fixes a heap buffer overflow in `lean_io_prim_handle_read` that was triggered through an integer overflow in the size computation of an allocation. In addition it places several checked arithmetic operations on all relevant allocation paths to have potential future overflows be turned into crashes instead. The offending code now throws an out of memory error instead. Closes: #13388
14 lines
338 B
Text
14 lines
338 B
Text
/-!
|
|
This issue is a minimal reproducer for #13388 which now throws an out of memory error.
|
|
-/
|
|
|
|
def main : IO UInt32 := do
|
|
let (h, _) ← IO.FS.createTempFile
|
|
let n : USize := (0 : USize) - (1 : USize)
|
|
try
|
|
discard <| h.read n
|
|
return 1
|
|
catch e =>
|
|
match e with
|
|
| .resourceExhausted .. => return 0
|
|
| _ => return 1
|