feat!: replace the analysis engine with a sound object model - #40
Merged
Merged
Conversation
Replaces the path-based engine behind the RFC 0030 seam with an engine whose facts live on abstract objects and symbolic values, so every alias sees every fact by construction (docs/rfcs/0031-object-engine.md). - Core: the heap domain (objects, cells, element ranges, focus objects, dead copies), a sparse zone of difference bounds, persistent maps. - Analysis: the object engine behind SafetyEngine (lib/Analysis/Engine*), format-30 summaries with cases, recursion widening and incomplete summaries, alias contexts, owning slots, carried-value and local liveness, loop budgets. - Frontend: unit record format 29, the link step and --whole-program over the new engine, the computed-goto edge split. - The old engine (FunctionDataflow and its trackers) and its tests are removed. - Tests: object-domain, alias-probe and held-out repro cases; eleven held-out corpus configs; the corpus ratchet re-recorded. BREAKING CHANGE: summary format 30 and unit record format 29 replace formats 29 and 28; objects built by earlier versions must be rebuilt. RFC 0030 and RFC 0031 are marked Implemented. Three numeric targets of RFC 0031 were not met and are carried forward as future work, with the measured values kept as ratchets (RFC 0031, "Gates carried forward"): the unresolved shares of G6, the build-cost bound of G12 and G4's count of possible temporal warnings.
…nd-trips; Linux corpus ratchet re-recorded
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
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.
What
Implements RFC 0031: the path-based engine behind the RFC 0030 seam is replaced by an engine whose facts live on abstract objects and symbolic values, so every alias sees every fact by construction. Summary format 30 and unit record format 29 replace formats 29 and 28 (breaking: objects built by earlier versions must be rebuilt). The old engine and its tests are removed.
RFC 0030 and RFC 0031 are marked Implemented. Every design decision made while implementing is recorded in RFC 0031's Implementation amendments.
Gates (reference machine, final tree)
--asanand--checks verify; no proven facet trapped in any corpus test suite built in verify modeunsafe-operationerrors triaged true (RFC 0004)make -j81.7 ssqlite3.c486 s / 2.3 GB;mujs/one.c12 sH1 (CI timings) is measured by this PR's CI.
Targets not met, carried forward
Three numeric targets set before the engine existed are not met. By the owner's decision they leave this RFC's acceptance, the measured values become ratchets, and the targets move to Future work (RFC 0031, Gates carried forward):
lua_CFunctionslot and collector, sqlite's allocator/mutex/VFS) and by extents the code does not state. Goes to RFC 0032.Known caveat
lz4's fuzz test (
frametest) can trap depending on its random seed: on a corrupt frameLZ4_memcpy_using_offset_basecallsmemcpy(dst, dst, 2)(overlapping, undefined in C; lz4's comment notes offset 0 happens in testing). The check is a true report, but the gate script still counts it as a trap, so a full held-out run can fail G5 on an unlucky seed.Testing
ctest --preset devsuites: Core 176, Analysis 388, Frontend 127 unit tests; 160 lit tests; 481 cases.scripts/corpus-gate.py --full --held-out(trap and verify modes),--inject,--bench;scripts/codegen-identity.py;scripts/check-hygiene.py;npm test && npm run buildindocs/.test/corpus/expected.jsonis re-recorded on the new engine for darwin-arm64 only; the linux-x86_64 record still needs--updatefrom a CI run.