Lean 4 is a theorem prover. Its kernel is small, audited, and does no I/O by design. Its runtime segfaults if a signal arrives while you are reading a file.
$ strace --inject=read:error=EINTR:when=8 ./my-lean-program < input
--- SIGSEGV {si_signo=SIGSEGV, si_code=SEGV_MAPERR, si_addr=NULL} ---
+++ killed by SIGSEGV +++
src/runtime/io.cpp:259:
case UV_EINTR:
lean_assert(fname != nullptr); // compiled out in release builds
inc_ref(fname); // dereferences it anyway
Eleven call sites in that same file pass decode_io_error(errno, nullptr). The
very next case in the switch has the null check this one is missing. In a
debug build the assertion catches it; in the binary you ship, the assertion is
gone and only the dereference remains.
How reachable is this? Less than I first assumed, and I checked before publishing rather than after.
EINTR on a blocking read requires a signal that is caught — a handler
installed without SA_RESTART. Signals with default disposition ignore, like
SIGWINCH, do not interrupt anything. I sent SIGWINCH, SIGCONT, SIGUSR1
and SIGTSTP to a Lean binary mid-read:
WINCH rc=0 survived
CONT rc=0 survived
USR1 rc=0 survived
TSTP rc=0 survived
All four survived. A Lean binary installs handlers for exactly three
signals — SIGBUS, SIGPIPE, SIGSEGV — and all three are set with
SA_RESTART.
So the realistic triggers are narrower: a slow or interrupted device, an NFS
mount going away, a SIGALRM timeout in a program that installs one, ptrace
attaching, or any library in the process that installs a handler of its own. The
crash is real and the path to it is real; it is not a routine terminal
resize, and I should not have written that it was.
I reproduced it in five of my own Lean utilities. Their sources wrap the read in
try ... catch e. They were written to handle I/O errors, and the handler is
never reached — the runtime dies before the exception can be constructed.
And the same shape, in C, in binutils
binutils 2.42, strings.c:543:
c = getc_unlocked (stream);
if (c == EOF)
return EOF;
getc_unlocked returns EOF for end-of-file and for error. There is no
ferror check anywhere on that path. Measured on a 415-byte input:
baseline 415 bytes, rc 0
EINTR 0 bytes, rc 0, stderr empty
EIO 0 bytes, rc 0
ENOSPC 0 bytes, rc 0
Three different errnos, identical result — the signature of a return value that
is never inspected. GNU cat on the same fault delivers all its bytes. strings
delivers none and reports success.
The thesis
These are the same bug in two languages, and neither language could have stopped it.
An errno is a value that must be consumed, exactly once, in a way that
distinguishes its cases. read() has three outcomes and they need three
answers:
n > 0 data
n == 0 end of input
n < 0 error — and errno decides retry (EINTR) or give up
Every clean implementation I tested distinguishes all three. Every defect I found collapses two of them:
strings.c:543 if (c == EOF) return EOF; EOF and error merged
wc.c:336 if (bytes_read <= 0) EOF and error merged
cat.rs:455 while let Ok(n) = reader.read(...) error dropped entirely
io.cpp:259 EINTR routed to an error path retry treated as failure
Lean has linear types. It did not use them here, because the error came back
from C, through a switch on an int, into a constructor that assumed a
pointer. The type system stopped at the FFI boundary and the discipline stopped
with it.
That is the argument: POSIX error values want linear types. Not as an
academic flourish — as the only mechanism that makes “you have not handled
EINTR” a compile error rather than a segfault in someone’s resized terminal.
What else the survey found
Six projects came back clean, and the reason is identical every time: a wrapper does the checking.
sqlite seekAndRead splits EINTR, EOF, error AND partial reads
grep safe_read gnulib's retrying wrapper
sed ck_fread clearerr / ferror / panic
ripgrep std::io retries beneath the application
mawk ferror at every print site
Every confirmed defect is a place where a program read without one.
GNU coreutils is on both lists, which is the sharpest thing here. Version 9.4
uses safe_read and is clean. Upstream HEAD replaced it with a raw read in
commit 6b8b1f9e7, and five tools regressed. The diff only changed a declared
type — the retry loop lived in a file the diff never touched.
Nine build-chain tools exit 0 with stdout closed: tar, objdump, readelf,
nm, ar, ld, as, make, patch. tar produces 10 KB of output, writes
none of it, and returns success. A backup script cannot tell that from working.
The tools
sauron runs a program under
strace --inject, fails one syscall at a time, and sorts the outcome into
RECOVERED, DIAGNOSED, SILENT, or SUSPECT.
SILENT is the finding. SUSPECT is the honesty — a fault injector whose
probe misses will report a clean bill unless it separates measured clean from
not measured. Ten of its regression tests exist because it got that wrong
once, including the day it reported a 14x speedup that turned out to be a crash.
saruman freezes a live invocation — argv, stdin bytes, the entire working
directory, environment, exit code — into a case sauron can replay. GNU’s own test
suite cannot be injected into, because tests/init.sh calls cat, tr and wc
for its own setup. saruman lifted it into 1050 standalone cases.
nazgul scans source for shapes sauron has already confirmed at runtime. Every pattern records the file, line and measurement it came from. It finds candidates; it does not decide.
Four of this survey’s findings were bugs in nazgul, not in the software: a
discarded fprintf(stderr, ...) is correct, RwLock::read() is not I/O, feof
discriminates as well as ferror, and < 0 is the right idiom — only <= 0
conflates. Each is recorded in the pattern file where it happened. A scanner
that quietly patches its own false positives teaches its next user that the
coverage is complete.
Try it
git clone https://github.com/chadbrewbaker/sauron
cd sauron && make && make test
./sauron --cheap /usr/bin/strings
951 lines. sauron, saruman and nazgul are bash; shim.c is the only thing
compiled. MIT.
The Lean bug is unreported as of writing — the fix is one line, copied from the case immediately below it.