feat!: prove or trap every memory-safety operation - #37
Merged
Merged
Conversation
WeaveC now decides every memory-safety-relevant operation in the code it compiles. Each site gets an outcome on each facet it has -- spatial, null, temporal -- and that outcome is one of: proven safe, checked at runtime, a violation, unresolved with a reason, or trusted with a reason. Nothing is silently ignored, so "no diagnostics" means something: every operation was either proved or is guarded. What the compiler does with those outcomes: - A definite violation is a compile-time error. - A possible spatial or null violation becomes a runtime check, inserted into the code being compiled (-fweavec-mode=trap|report|verify|none). - A possible temporal violation is a warning: a use-after-free cannot be checked cheaply at runtime, so it is reported rather than guarded. - Anything the analysis cannot resolve is reported with the reason it could not, never dropped. The guarantee, its assumptions A1-A5 and the blame property are stated in docs/pages/reference/guarantees.md and in the RFC's Soundness section. WEAVEC_UNSAFE now means "trusted raw operation", recorded in the ledger as trusted(unsafe-block) rather than a suppression that hides a site, and WEAVEC_ASSUME is checked rather than believed. How it works: - One ledger holds every site, facet and outcome, and is the only thing that publishes diagnostics. The engine never touches a DiagnosticSink. - Checks are planned, then emitted from Sema-built AST rewrites behind a deferred CodeGen consumer, so guards are inserted without a second pass over the IR. - Pointer kinds (Single, Counted, Sized, EndedBy, NulTerminated, Unknown, nullable or not) are declared, inferred, or defaulted soundly, and carry the extents that checks are written against. - Library behaviour is a declarative table of 888 entries, not name tests in the engine. - Indirect calls resolve through function-pointer slots, replacing the RFC 0014 callback-global fixpoint. - Units publish self-delimiting format-28 records; the link step verifies declarations across units, decides exported requirements at cross-unit callers, and writes a program ledger. SARIF and JSON output carry stable fingerprints. Measured on the pinned corpus of eleven configurations: - One definite error across the whole corpus, and it is a true one: a pointer laundered through uintptr_t, which needs WEAVEC_UNSAFE. Every finding carries a triage entry with the source evidence for its verdict. - None of the 85 soundness probes is silent, 62 are reported, and no bug site ASan confirms has its matching facet proven. - 29 of 31 injected bugs are reported at the injected line. - Verify mode covers 95.4% of proven null facets; it monitored nothing before, because the planner required a witness nothing published. Three gates are not met, each amended in the RFC with the measurement and the next lever rather than a moved threshold: - G10: 671 possible temporal warnings against a budget of 60. 619 of them are one Lua family whose cause is now isolated to a `replaced` fact that does not survive a recursive call. - G14: Lua's runtime overhead is 1.4783 against 1.10, but checking costs exactly 1.10; the rest is LLVM declining to replicate a computed-goto dispatch once checks supply the edges into it. A reproducer and the fix are recorded. - G15: Lua's whole-program analysis takes 307 s against 214 s. The estimate behind that limit was never derived from the analysis this RFC specifies. A schedule change that met it by exhausting one function's budget and losing 61 findings was rejected: this gate may not be met by analysing less. Removals, since this is pre-1.0 and nothing is kept for compatibility: checked mode in full (--checked, WEAVEC_CHECKED, checkContracts, SafetyState, the checked sidecar and report formats), the per-RFC validation populations and their harnesses, and every component that became unreachable. RFCs 0018-0029 are superseded; RFCs 0002-0017 carry amendment notes where this RFC changes what they say. Diagnostic ids removed: analysis-incomplete, annotation-required, checking-incomplete, checking-failed. Added: contradicted-assumption, allocation-failure, unresolved-operation, unchecked-operation, unanalyzed-input.
The branch had only ever been built on macOS. Clang on Linux rejects comparing a three-way comparison result against literal 0 under -Wzero-as-null-pointer-constant, which is one line in Summary.h and is why the Linux Debug, Linux Release, clang-tidy and CodeQL jobs all failed: each of them builds the project. Also: an inefficient string concatenation and a non-ranges binary_search that clang-tidy rejects, and six files clang-format wanted reflowed. Six cases pinned expectations the implementation has outgrown. Five probes (05, 19, 39, c06, c11) now get a runtime check that traps at the bug line, which is what RFC 0030 asks for and what the missing TRAP markers never recorded; lowered-out-of-bounds expected an index check where a definite violation gets the facet-level violation check instead.
…rap rule The case tree is now 410/410 in trap, no-run, no-emission and verify modes, and CTest is 1260/1260. Engine fixes, each found by reducing the failing case: - IntegerRange::fromRanks collapsed a range of more than two pieces to the whole type instead of its hull, so two if/else joins erased every bound a value had. - applySummary released array elements after consuming arguments, so a callee that walks a container and then frees it was read against a state where the same call had already freed it. That was a use-after-free error on every correct caller. - A bypassed declaration is not zero-initialised, which §2.3 says makes its pointer unresolved(no-zero-init); the engine was calling it checked(nonnull), and a null check does not make an indeterminate pointer safe. The bypass predicate moves out of the Frontend into a shared Analysis component so the A5 count and the engine agree. - A disjoint witness built its length with no bound, so a strlen inside it failed and took the site's len check with it. - The alternative state of a symbolic array store reported a leak for every cell the store may have overwritten. The runner matched a TRAP without a run only against a `checked` facet. A definite violation §3.4 lowers to a warning is still guarded, but its row keeps the outcome `violation`, so the check it carries is what stands in for the run. That is what the ASan job, which runs --no-run, was failing on. Five cases keep a known-gap marker rather than a fix, each with its reason in the file and in test/cases/soundness/README.md: two ALLOW for a leak the loop-correlation gap reports on correct code, and three MISS where the defect is not caught (the same fill-loop shape, an array past MaxArrayCells, and a length term §10.3 rule 1 cannot spell).
LinkStep's local quoted() took a const std::string&, but site.callee is a string_view and building a string from a view is explicit, so the helper was not viable and ADL chose std::quoted, which returns a stream manipulator. That one line failed both Linux jobs, clang-tidy and CodeQL. The helper is now quotedName(std::string_view), the signature Ledger.cpp already uses. The rest is 125 clang-tidy findings this branch accumulated, which CI can only reveal one file at a time: it runs clang-tidy while compiling, so the build stops at the first file that fails. Found by sweeping locally. Fixed rather than suppressed: 38 functions in anonymous namespaces made static, which is the convention this project states it follows; 18 C arrays to std::array; 15 const_casts routed through one documented helper; and the usual run of ranges algorithms, designated initialisers, const correctness, nested conditionals, string building and std::move. Seven suppressions, each narrow and with its reason in the file. Three deserve mention: padding on FunctionDataflow, whose members are grouped by concern and which is built once per function analysed; a loop in ZeroInit whose container grows as it iterates, so the suggested range-for would walk invalidated iterators; and four arena allocations the ASTContext owns, where the alternative spelling changes codegen under -fprotect-parens. One suppression was already there and silently broken: clang-format had wrapped its NOLINTNEXTLINE onto two lines, so it pointed at its own continuation and suppressed nothing.
These had never run on Linux: the Linux jobs always died at the build, so the first green build exposed four platform assumptions. - The prelude runtime test used Darwin spellings. glibc's malloc_usable_size takes void * where Darwin's malloc_size takes const void *, and -std=c11 hides posix_memalign behind a POSIX feature test on glibc but not on Darwin. - The analysis dump and the summary line went to differently buffered streams, and the RUN line merges them. glibc sizes a pipe's buffer at 4 KiB, so the summary landed inside a dump line; Darwin held the whole dump in one buffer and never split. printSummary now flushes the dump first, and the test pins the ordering so this is catchable here. - The corpus gate harness passed -ferror-limit=0 through its fake compiler to the system cc, which is Apple Clang here and gcc there. gcc rejects it, the analysis counted as a tool failure, and --update declined to write expected.json, which surfaced as a missing file. The fake driver now consumes the flag as the real one does, and the test asserts the update happened with the gate's own log in the message. - Probe 25c expects a getenv result to dangle across a setenv. glibc never frees a published NAME=value string, precisely so that callers may hold one, so there is no defect there for the ASan oracle to find. The oracle requirement is dropped with the reason recorded; the BUG marker stays, because WeaveC cannot know which libc it will be linked against. Also four clang-tidy findings only the newer clang-tidy CI runs reports: an optional dereferenced and immediately rewrapped.
Every remaining Linux failure was the same thing: `run N: timed out`, on a different case each time. Not a logic bug — starvation. CI runs `ctest -j $(nproc)`, and each cases-* suite then forked another os.cpu_count() workers, so a four-core runner had up to sixteen workers compiling and running programs at once. A program that finishes in milliseconds missed a ten-second wall-clock timeout because it was waiting to be scheduled at all. The macOS runner is fast enough to hide it, and the ASan job never saw it because --no-run runs no programs. The suites and the lit test now declare PROCESSORS, so CTest's scheduler knows what they cost, and each suite is given the matching --jobs so the two numbers cannot drift apart. Both are cache variables. The per-run timeout goes from 10 s to 30 s as well. It exists to bound a hang, and a hang is still caught; being generous costs nothing on a machine that is not starved, and this is a shared runner.
The ratchet held only darwin-arm64, so the pinned-corpus step failed on Linux with "no expectations recorded for linux-x86_64" — the one thing left once the Linux tests all passed. Recorded with --update-from, using the results the CI job itself measured and uploaded, which is what that flag is for: these numbers cannot be produced here. The run they come from was healthy: 0 definite errors, 22 possible temporal findings against a budget of 60, no function over its analysis budget. The four configurations are the ones the PR job measures; the weekly --full run records the rest.
owenthcarey
changed the title
owenthcarey
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
WeaveC now decides every memory-safety-relevant operation in the code it compiles. Each site gets an outcome on each facet it has -- spatial, null, temporal -- and that outcome is one of: proven safe, checked at runtime, a violation, unresolved with a reason, or trusted with a reason. Nothing is silently ignored, so "no diagnostics" means something: every operation was either proved or is guarded.
What the compiler does with those outcomes:
The guarantee, its assumptions A1-A5 and the blame property are stated in docs/pages/reference/guarantees.md and in the RFC's Soundness section. WEAVEC_UNSAFE now means "trusted raw operation", recorded in the ledger as trusted(unsafe-block) rather than a suppression that hides a site, and WEAVEC_ASSUME is checked rather than believed.
How it works:
Measured on the pinned corpus of eleven configurations:
Three gates are not met, each amended in the RFC with the measurement and the next lever rather than a moved threshold:
replacedfact that does not survive a recursive call.Removals, since this is pre-1.0 and nothing is kept for compatibility: checked mode in full (--checked, WEAVEC_CHECKED, checkContracts, SafetyState, the checked sidecar and report formats), the per-RFC validation populations and their harnesses, and every component that became unreachable. RFCs 0018-0029 are superseded; RFCs 0002-0017 carry amendment notes where this RFC changes what they say.
Diagnostic ids removed: analysis-incomplete, annotation-required, checking-incomplete, checking-failed. Added: contradicted-assumption, allocation-failure, unresolved-operation, unchecked-operation, unanalyzed-input.
Summary
Design notes
Test plan
unittests/)test/)ninja check-weavecpasses locallyChecklist
scripts/format.sh) and passes clang-tidylib/Core