Memory Safety Where It Is Needed: Proof-Guided Runtime Checking in a Toolchain Small Enough to Read

Abstract

Fil-C showed that C can be made memory-safe at run time by giving every pointer acapability and checking it on every access. We take its diagnostic ambitions and put themsomewhere else: in a compiler small enough for a person, or a language model, to hold inview at once, and with a different goal. Crust’s --mem-safe is a test-time tool rather thana deployment mitigation. The identical source builds with the flag for the test suite andwithout it for release, and the release binary carries no runtime at all.The difference in setting changes what is possible. Because the check is inserted by thecompiler on its own intermediate language, the compiler can also decide not to insert it.Three proof rules—redundancy by local value numbering, constant-offset bounds againsta statically known allocation, and loop-carried index ranges from a dominating guard—together with hoisting of the remaining shadow bookkeeping out of the loop, took a 2M-iteration array loop from 31× overhead under uniform instrumentation to 1.05×, with noruntime call left in the loop body. Fil-C cannot do this: its check is a per-pointer test withno whole-program view to prove anything away.Because the bounds live in a side table keyed by address rather than in the pointer,instrumented and uninstrumented translation units link freely. That is what makes a secondtier possible: --mem-safe=cpp checks only code lowered from the C++ subset and leavesalready-audited C at full speed, distinguishing the two by the file name on each IL command’ssource range.We then argue the larger point: that a memory-safety mechanism belongs in a toolchainthat can be modified and re-verified in the time a test run takes, and that a fork like Fil-C126,031 commits behind its upstream is not such a toolchain.