diff --git a/examples/pkg_resolver/abi/.gitignore b/examples/pkg_resolver/abi/.gitignore new file mode 100644 index 000000000..65b2c4210 --- /dev/null +++ b/examples/pkg_resolver/abi/.gitignore @@ -0,0 +1,3 @@ +# Generated stores, built fixtures and verification artifacts (rebuild via +# run_abi_verify.sh). Never commit machine-specific ingested data. +.out/ diff --git a/examples/pkg_resolver/abi/README.md b/examples/pkg_resolver/abi/README.md new file mode 100644 index 000000000..8afb8701c --- /dev/null +++ b/examples/pkg_resolver/abi/README.md @@ -0,0 +1,188 @@ + + + +# Symbol-level ABI-compatibility lane (`pkg_resolver/abi`) + +This lane refines the coarse package resolver's `provides` (`libc6 (>= 2.34)`) +to **ABI compatibility at the exact versioned-symbol level**: for a binary and +a shared library it answers *compatible / incompatible / unknown* per candidate +release, and computes the `[min, max]` compatible release range that `ldd` +cannot tell you. It is a driver **above** the frozen resolver: `resolver.pl` +and `resolver_store.pl` are not edited; the Debian-version comparison is +delegated to `resolver:version_lt/2` on `deb/3` terms from +`debian/deb_parse.pl`. + +The lane was redesigned after the PR #4262 review and revised after Sol's +re-review; `REVIEW_NOTES.md` maps each review point to the code and the +fixture that proves it. + +## The model + +Identity is the exact **(soname, symbol, version-node)** triple. Two axes are +kept strictly apart: + +| Axis | Values | Ordering | Used for | +|------|--------|----------|----------| +| ELF version node | `GLIBC_2.34`, `LIBSELINUX_1.0`, `COMMON_1`, `PUBLIC`, `Base` | **none** — opaque labels matched by string equality | *Does release R export `Sym@Node`?* A requirement `foo@LIB_1` is satisfied only by a provider row `foo@LIB_1` on the same soname. `foo@LIB_2` is not a match (the loader agrees: `undefined symbol: foo, version LIB_1`). `Base` is dpkg's spelling of "unversioned". An **unversioned requirement** binds, as the loader does, only to a `Base` export or a **default** (`@@`) export — never to a hidden (`@`) one. | +| Debian package version | `2.34`, `3.1~`, `1:2.3-1`, `2.35-0ubuntu3.15` | `resolver:version_lt/2` over `deb(Epoch, Upstream, Revision)` (epoch, `~`, revision, any number of components) | the `.symbols` minimum-version field (a curated **lower bound**, not an introduction date) and the **release candidates**. | + +Evidence is explicit, and every provider bound is tied to the evidence row it +came from: + +- `prov_evidence(So, symbols|elf, R0, complete|curated)` — `complete` (readelf, + or a `.symbols` file cross-checked against the ELF with `--elf`) means the + export set is fully observed at `R0`, so **absence from it is a fact**; + `curated` (a plain `.symbols` lower-bound list, no `--elf`) means **presence + is evidence but absence proves nothing** — an omitted symbol is `unknown`, + never `missing`/`below_floor` (Sol re-review 2, P1). +- `req_evidence(Bin, readelf, complete | missing_file | readelf_failed | inconsistent, Detail)`. +- Provider bounds: `since(Min, MinAtom, R0, Bind)` from the `.symbols` evidence + taken at `R0` (exported at `R0` and, by the curated bound, at every release + `>= Min`); `at(R0, Bind)` from readelf at `R0`. `Bind` is the + default-version binding: `default` (an unversioned reference binds to it: + `@@`, `Base`, or the oldest version node which the loader also accepts), + `nondefault` (hidden `@`), or `unproven` (a `.symbols` row not cross-checked + against the ELF with `--elf`). + +Per identity and release, **all** evidence rows are aggregated: evidence +taken *at* the release decides (readelf before `.symbols`); otherwise the +nearest evidence below (presence extrapolates upward) and the nearest +evidence above (absence *from a complete export set* propagates downward; a +curated floor covers `Rel >= Min`) are combined. A release satisfied by any +evidence row is never vetoed by another row's floor, and a curated `.symbols` +list never vetoes by absence — only a `complete` observation does. + +Verdict for `(Bin, So, Rel)`: + +``` +compatible(exact | curated | extrapolated) presence — defeasible "structurally possible" + exact every requirement observed by readelf at exactly Rel + curated some requirement rests on .symbols metadata only + extrapolated some requirement rests on the monotone-export assumption +incompatible([missing(Sym@Node) | missing(Sym@Node, observed_absent(Src, R1)) + | missing(Sym, no_default_export(So, Node)) | below_floor(Sym@Node, Min) + | soname_mismatch(offered(So), needed(N))]) + HARD veto — only reachable with complete, attributed evidence +unknown([no_requires_evidence | requires_evidence(Status,_) | no_provider_evidence(So) + | unknown(Sym@Node, evidence_release(R0) | absent_at(Src, R1) | dropped_between(R0, Src, R1)) + | unknown(Sym, default_binding_unproven(So, Node)) | ...]) +not_needed(So) not in DT_NEEDED and not a declared replacement +``` + +Documented defeasible assumption: within a soname, exports do not disappear +(removing one is an ABI break that requires a soname bump), so presence at +`R0` extrapolates to later releases and absence from a complete export set at +`R1` is a veto for every release `<= R1` (later releases may add symbols: +unknown). `drop(Sym, Node, At)` models a violation of that assumption to +exercise the upper bound; an *observed* violation (present at `R0`, absent +at a later `R1`) makes the releases in between `unknown(dropped_between(...))`. +`soname_mismatch` needs a declared `replaces(New, Old)` relation +(`replaces.jsonl`); there is no name-stem heuristic. + +## Files + +| File | Role | +|------|------| +| `ingest_symbols.mjs` | Ingest: `.symbols` (since bounds, optionally cross-checked against the ELF with `--elf`), `readelf` provides (`at` bounds with default-version binding), `readelf` requires (attributed via the ELF version **index**), NEEDED, evidence, release axis, declared soname succession (`replaces`). Loud, atomic failures (exit 3), never an empty or partial success. | +| `abi_resolve.pl` | Resolver: store loading, the two axes, per-identity evidence aggregation, per-requirement status, verdicts, floor, range over the real release axis. | +| `abi_cli.pl` | Driver: `verdict` / `status` / `floor` / `axis` / `range`. | +| `crosscheck.mjs` | readelf-vs-`.symbols` cross-check on exact identity + per-name node sets (no node-name parsing or ordering); fails on empty input. | +| `test_abi.pl` | Assertions: real data (A), version axes (B), model fixtures (C), gcc-built ELF fixtures + `.symbols` template fixtures (D). | +| `run_abi_verify.sh` | End-to-end: build the real store, cross-check (+ negatives), build/ingest fixtures with the loader as ground truth, run the tests. | +| `fixtures/` | C sources + version scripts for the ELF fixtures (incl. the hidden-version `libhid`); `.symbols` fixtures (simple cases, template rejects, arch selectors, `(optional)`, unknown tag, batch atomicity); `crosscheck/` static regression pair. | + +Generated stores land in `./.out` (gitignored). + +## Store shape (P/2 JSONL, `[key, value]`) + +``` +symprov.jsonl ["|@", ["since", "", "", ]] # .symbols tier + ["|@", ["at", "", ]] # readelf tier + = "default" | "nondefault" | "unproven" +symreq.jsonl ["|@", ["", "GLOBAL"|"WEAK"]] + ["|", ["", "GLOBAL"|"WEAK"]] # unversioned reference +needed.jsonl ["", ""] +evidence.jsonl ["provides|", ["symbols"|"elf", "", "complete"|"curated", ""]] + ["requires|", ["readelf", "complete"|"missing_file"|"readelf_failed"|"inconsistent", ""]] +releases.jsonl ["", ""] # the candidate axis (actual releases) +replaces.jsonl ["", ""] # declared soname succession +``` + +## The three provider tiers (cheapest first) + +1. **`Packages` `Depends:`** — the coarse floor (`libc6 (>= 2.34)`), consumed + by the coarse resolver. This lane's `abi_floor/3` recomputes it from the + symbols and, on this machine, matches coreutils' declared + `libc6 (>= 2.34), libselinux1 (>= 3.1~)` exactly. +2. **`.symbols` control member** (`ingest_symbols.mjs symbols-file`) — every + exported `sym@node` with a curated minimum package version. Already on disk + under `/var/lib/dpkg/info/*.symbols`; a few KB per package, no binary + download. Binary-form files are fully supported. Source-template tags are + **whitelisted**: `(arch=...)` / `(arch-bits=...)` / `(arch-endian=...)` + with `--arch`, `(ignore-blacklist)`, and `(optional)` **only with + `--elf `** (dpkg lets an optional symbol stay in the template after + it left the binary, so the row counts only if the ELF exports it); + every other tag, `(symver)`, `(regex)`, quoted C++ patterns, `#include`, + an unknown evidence release or a non-Debian `--release` **rejects the whole + file** (exit 3, nothing partial, also in batch mode). With `--elf` the + file is cross-checked against the ELF and each row's default-version + binding is taken from it; without it rows are `unproven` for unversioned + references. +3. **`readelf`** (`ingest_symbols.mjs elf` / `requires`) — any ELF. Provides + are exact for the file's own release and carry the default-version binding + (`.gnu.version` hidden bit, cross-checked against the `@`/`@@` spelling); + requires are joined to their soname through `.gnu.version` -> + `.gnu.version_r` by index, so two libraries using the same node name never + collide. + +## Verify on this machine + +``` +./run_abi_verify.sh +``` + +Real-data results (Ubuntu 22.04.5, libc6 2.35-0ubuntu3.15, libselinux1 3.3-1build2, `/bin/ls`): + +- Ingest: libc6 `.symbols` cross-checked against `libc.so.6` with `--elf` + -> **4827** `symprov` rows over 20 sonames (**3006** for `libc.so.6`, 0 + optional rows dropped, 0 disagreements, **115** hidden `@` exports recorded + `nondefault`, `memcpy@GLIBC_2.2.5` at verdef index 2 recorded `default`); + libselinux1 -> 238; `/bin/ls` -> **112 versioned + 3 unversioned (weak)** + requirements, `NEEDED = [libselinux.so.1, libc.so.6]`. +- Cross-check `readelf(libc.so.6)` vs `.symbols`: **3006/3006 exact + `sym@node` identities agree (100%)**; per-name node sets **2763/2763 + (100%)**. The earlier 91.7% was an aggregation bug (last curated row vs + earliest ELF row), not a glibc 2.34 merge effect; `fixtures/crosscheck/` + pins that case. Empty inputs fail the cross-check. +- `floor /bin/ls libc.so.6` = **2.34**; `floor /bin/ls libselinux.so.1` = + **3.1~** — equal to coreutils' declared Pre-Depends. +- Release axis (from `apt-cache madison` + dpkg): `[2.35-0ubuntu3, + 2.35-0ubuntu3.15]`; `range /bin/ls libc.so.6` = **[2.35-0ubuntu3, + 2.35-0ubuntu3.15]**, both ends `compatible(curated)` (the evidence is + `.symbols` metadata; `exact` needs readelf at that release). +- Hypothetical older release `2.31-0ubuntu9.9` -> + `incompatible([below_floor(__libc_start_main@GLIBC_2.34, 2.34), below_floor(lstat@GLIBC_2.33, 2.33)])`; + an axis extended below the floor yields min `2.34-0ubuntu3`, never the + lowest release. Adding readelf evidence for that release turns the verdict + into `compatible(exact)` — a curated floor never vetoes a release another + evidence row satisfies. +- Hypothetical removal of `getenv@GLIBC_2.2.5` at `2.35-0ubuntu3.15` caps the + range at `[2.35-0ubuntu3, 2.35-0ubuntu3]`; removing + `__libc_start_main@GLIBC_2.34` at the oldest release -> `no_candidate`. +- Offering `libc.so.7` -> `incompatible([soname_mismatch(...)])` because the + store declares `replaces(libc.so.7, libc.so.6)`; `libselinux.so.10` (same + stem, no declaration) -> `not_needed`; a binary with no requirement + evidence -> `unknown([no_requires_evidence(...)])`. +- ELF fixtures (gcc): `foo@LIB_1` required vs `foo@LIB_2` exported under the + same soname -> `incompatible([missing(foo@LIB_1)])`, and the loader agrees + (`undefined symbol: foo, version LIB_1`); `hid_fn` exported only at a + hidden `@HID_1` (verdef index 3) does **not** satisfy an unversioned + requirement -> `incompatible([missing(hid_fn, no_default_export(...))])`, + and the loader agrees (`undefined symbol: hid_fn`), while the same hidden + export at verdef index 2 binds (loader and lane agree); `COMMON_1` in two + libraries attributed correctly; `pub_fn@PUBLIC` + unversioned `plain_fn` + preserved; missing ELF -> `unknown([requires_evidence(missing_file, _)])`; + `(optional)` row absent from the ELF dropped, present rows kept. + +`test_abi.pl`: 92 checks, all passing; `run_abi_verify.sh` additionally +asserts the exit-3 rejections, batch atomicity and the cross-check negatives. diff --git a/examples/pkg_resolver/abi/REVIEW_NOTES.md b/examples/pkg_resolver/abi/REVIEW_NOTES.md new file mode 100644 index 000000000..70e7be169 --- /dev/null +++ b/examples/pkg_resolver/abi/REVIEW_NOTES.md @@ -0,0 +1,307 @@ + + + +# Review notes — redesign of the symbol-level ABI lane (PR #4262 follow-up) + +Astra's REQUEST-CHANGES review found the first implementation too lossy: it +collapsed `sym@node` to bare names with a numeric "intro", dropped non-numeric +and unversioned obligations, attributed requirements by version-*name*, mixed +the Debian package-version axis with the ELF node axis, computed an +unsatisfiable lower bound, mis-aggregated the cross-check (91.7%), and +silently mis-ingested `.symbols` templates. The model and ingest were +redesigned; the direction (three evidence tiers, a driver above the frozen +resolver) is unchanged. Sol's re-review of that redesign (REQUEST-CHANGES, +eight points) is addressed in the second section below. Frozen `resolver.pl` +/ `resolver_store.pl` / `debian/` are untouched (`git diff origin/main -- +examples/pkg_resolver/{resolver.pl,resolver_store.pl,debian}` is empty). + +Run `./run_abi_verify.sh` (needs node, readelf, swipl, gcc). Expected tail: +`== 122 passed, 0 failed, 0 skipped ==`. Check names in `test_abi.pl` carry the +review point they prove: `(#n)` for Astra's points, `(sol-...)` for Sol's. +The shell script's own assertions (exit codes, files not written, expected +cross-check failures) abort the run with `FAIL:` before the Prolog section. + +## Sol re-review — fixes + +Each row: Sol's point -> what changed -> the fixture that fails if the fix is +reverted. Sol judged the extrapolated/monotone-export disclosure adequate; it +is unchanged. + +| Sol point | Fix (location) | Proving fixture(s) | +|-----------|----------------|--------------------| +| **P1a** `->` committed to the first `symprov/4`; `since(2.0)` + `at(1.0)` vetoed release 1.0 as `below_floor` | `abi_resolve.pl`: every bound now carries its evidence release (`since(Min, MinAtom, R0, Bind)`, `at(R0, Bind)`) and is usable only through its own complete `prov_evidence` row (`bound_evidence/4`). `ident_status/5` collects what EVERY evidence row says about the identity (`ev_says/5`) and combines them: evidence AT the release decides (readelf before `.symbols`); otherwise the nearest evidence BELOW (presence extrapolates upward) and ABOVE (absence propagates downward under monotone exports; a curated floor covers `Rel >= Min`) are combined in `combine/4`. A release satisfied by any row is never vetoed by another row's floor. Ingest (`ingest_symbols.mjs`) writes the evidence release into every `since` row. | **C7** (`since(2.0)` asserted first, `at(1.0)` second; release 1.0 -> `compatible(exact)`), C7b (1.5 extrapolated, 2.5/3.0 curated, 4.0 extrapolated), C7c (0.5 -> unknown, not a veto), C7d (range min is the observed release), C7e (a bound without its evidence row does not count), C7f (absence propagates down, not up), C7g (present-then-absent -> `unknown(dropped_between)`), **A25** (real `/bin/ls`: ELF evidence at 2.31-0ubuntu9.9 turns the below_floor veto into `compatible(exact)`), D7 (rows tied to the evidence release). | +| **P1b** `@` (non-default) vs `@@` (default) discarded; a non-default-only export satisfied an unversioned reference | Ingest `elfProvides()` records a binding per row from the `.gnu.version` hidden bit, cross-checked against the `@`/`@@` spelling (`inconsistent` -> exit 3): `default` = non-hidden **or verdef index 2** (the loader binds legacy unversioned references to the oldest node even when hidden — verified with the loader, see D10c), `nondefault` = hidden at index >= 3. `.symbols` rows are `unproven` unless cross-checked with `--elf` (then the ELF's binding is copied); `Base` always binds. Store: `["at", rel, binding]`, `["since", minver, rel, binding]`. Resolver `unversioned_status/7`: satisfied only by a `Base` or `default` export (`unversioned_in/5`); an `unproven` row yields `unknown(Sym, default_binding_unproven(So, Node))`; a `nondefault`-only export yields the hard `missing(Sym, no_default_export(So, Node))`. | **D10** (gcc `libhid.so.1` exporting `hid_fn` only at hidden `@HID_1`, verdef index 3: unversioned require -> `incompatible([missing(hid_fn, no_default_export(...))])`; `run_abi_verify.sh` runs the loader: `undefined symbol: hid_fn`), D10b (`@Base` -> compatible), **D10c** (hidden at index 2 -> recorded `default`, compatible; loader binds), **C8** (model: nondefault-only -> hard veto), C8b (adding a default node -> compatible), **C8c** (`.symbols`-only -> `unknown(default_binding_unproven)`), C8d (`Base` row -> compatible(curated)), C8e/C8f (versioned requirements unaffected), A7b/A7c (real libc6: every `libc.so.6` row ELF-proven; `memcpy@GLIBC_2.2.5` index 2 -> default, 115 hidden rows -> nondefault), D4b. | +| **P1c** `(optional)` template rows emitted as complete exports (D8 asserted the unsafe behaviour) | Ingest: an `(optional)` row is not an export fact by itself. With `--elf ` the file is cross-checked against the ELF: an optional row the ELF does not export is **dropped** (stderr notice), a non-optional row the ELF does not export or an ELF export absent from the file **rejects** the file; without `--elf` any `(optional)` row rejects the file (exit 3). Binary-form `.symbols` under `/var/lib/dpkg/info` carry no tags, so the real path is unaffected; `run_abi_verify.sh` now ingests libc6's `.symbols` with `--elf libc.so.6` (0 dropped, 0 disagreements). | **D8 inverted** (`tmpl_optional.symbols` + `--elf libtmpl.so.1` which lacks `maybe_fn`: only `plain_fn` stored, evidence complete, `\+ symprov(maybe_fn)`), **D8b** (no `--elf` -> file rejected, no store), D8d (non-optional row absent from the ELF -> rejected), `run_abi_verify.sh` asserts the exit-3 and the dropped-row notice. `tmpl_arch.symbols` no longer carries the optional row (D8c keeps the arch checks: 3 rows). | +| **P2a** batch mode skipped a block with an unknown evidence release but counted the file as success and exited 0 | `cmdSymbolsFile()` collects every problem of every block and returns `null` (nothing added to the sink) if any exists — single-file and batch alike; `symbols-dir` counts it as rejected and exits 3. | **D11** + `run_abi_verify.sh` (`fixtures/batch/mixed.symbols`: block 1 resolvable via installed `libc6`, block 2 `#PACKAGE#`: exit 3, stderr `files=0 rejected=1 symprov=0`, `symprov.jsonl` and `evidence.jsonl` empty — no `good_fn` row). | +| **P2b** only a fixed tag list rejected; unknown tags silently stripped; `--release` unvalidated | `SUPPORTED_TAGS` whitelist (`optional`, `arch`, `arch-bits`, `arch-endian`, `ignore-blacklist`); every other tag rejects the file. `validRelease()` is the single Debian-version gate: `--release` is validated up front for every command, dpkg-guessed releases and the `releases` axis pass through the same regex. | **D9 tmpl_unknown_tag** (`(frobnicate)` -> exit 3, no store), **D9 bad_release** (`--release definitely-not-a-debian-version` -> exit 3, no store; also asserted for the `elf` path), `run_abi_verify.sh` `expect_reject` for both. | +| **P2c** `crosscheck.mjs` passed `/dev/null` vs `/dev/null` (`NaN < 100` is false) | Both symbol sets and the per-name denominator must be nonzero; `fail()` exits 1 otherwise; the pass conditions are `=== 100`, never `< 100`. | `run_abi_verify.sh` (sol-P2c): `/dev/null` vs `/dev/null` and `sym` vs `/dev/null` must fail with `FAIL: empty symbol set`. | +| **P2d** `soname_mismatch` from a stem heuristic (`libfoo.so.2` vs unrelated NEEDED `libfoo.so.1-extra`) | `so_stem/2` removed. `soname_offer/3` reports `mismatch(N)` only under a declared `replaces(Offered, N)` with `needed(Bin, N)`; anything else not NEEDED is `not_needed`. New store file `replaces.jsonl` (`ingest_symbols.mjs replaces ...`); `run_abi_verify.sh` declares `libc.so.7 replaces libc.so.6` for the real store. | **C9** (offer `libfoo.so.2`, NEEDED `libfoo.so.1-extra` -> `not_needed`), C9b (still not_needed with `libfoo.so.1` NEEDED but no relation), C9c (declared relation -> `soname_mismatch`), **A19b** (real: `libselinux.so.10` -> `not_needed`), A19 (real: `libc.so.7` mismatch only because declared). | +| **P3** local dotted-version comparator over node names in the legacy per-name figure | `nodeNum()`/`cmpDotted()`/`earliest()` removed. The per-name figure is now "per-name node-SET agreement" (sets compared, nothing parsed or ordered). Real data: 3006/3006 exact, 2763/2763 per-name. | `fixtures/crosscheck/` (sol-P3): a two-node symbol, a `GLIBC_PRIVATE` node, a `Base` node, another soname to be ignored -> 5/5 and 4/4; `elf_dropnode` must fail on both checks; asserted in `run_abi_verify.sh`. | +| **Residual** `.symbols`-derived verdicts labelled `compatible(exact)` | New basis `curated`: presence resting on `.symbols` metadata (at or below its evidence release, `Min =< Rel`) is `provided(_, curated)`; `exact` is reserved for readelf at exactly the release. The verdict basis is the weakest among the requirements (`exact < curated < extrapolated`). | A12 (real: `compatible(curated)` at the `.symbols` evidence release), C1b, C7b, C8d; `exact` still on ELF fixtures (D2, D3b, D4b, D10b/c, C7). | + +Changes that fell out of the P1a restructuring (documented, not requested): + +- **Absence propagates down, not up.** Before, a missing provider row was a + veto for *every* release of the soname; now absence from complete evidence + at `R1` is `missing` for `Rel =< R1` (reported as `missing(Sym@Node)` at + `R1` itself and `missing(Sym@Node, observed_absent(Src, R1))` when + inferred) and `unknown(absent_at(Src, R1))` for `Rel > R1` — later releases + add symbols. C7f, A17. +- **Observed drop.** Present at `R0`, absent at a later `R1`: a release in + between is `unknown(dropped_between(R0, Src, R1))`, neither extrapolated + nor vetoed. C7g. +- `abi_floor/3` takes the highest minimum over all `since` rows of an + identity (several `.symbols` evidence releases may coexist). + +## Sol's checklist (first review) + +### (a) Exact version-node identity end-to-end — Astra #1 + +- **Ingest** (`ingest_symbols.mjs`): `.symbols` rows are split at the last + `@` into `(sym, node)` and stored as `"|@"` with the minimum + version *verbatim* (`["since", "", "", ]`). + readelf provides carry the node from `.gnu.version_d` by index + (`["at", "", ]`). Nothing is parsed out of a node name. +- **Store** (`abi_resolve.pl`): `symprov(So, Sym, Node, Bound)`, + `symreq(Bin, Sym, Node, So, Bind)`. Loading rejects an empty node. +- **Match** (`versioned_status/7` -> `ident_status/5`): same soname, same + symbol, same node, by unification. No fallback to `symprov(So, Sym, _, _)` + for versioned requirements. +- **Fixtures**: C1/C1b, **D1** (gcc-built `libfoo.so.1` v1/v2; the loader + must print `undefined symbol: foo, version LIB_1`), A17/A18 on real libc, + A7, B8. + +### (b) verneed attribution via version INDEX — Astra #3 + +- `elfTables()` parses `readelf -W -V`: `.gnu.version` (per-dynsym index, + hidden bit `h`), `.gnu.version_d` (index -> name) and `.gnu.version_r` + (index -> `{file, name, weak}`). `elfRequires()` joins each UND symbol by + its **index** to `(file, node)`; the `name@VER` text is only a consistency + assertion (mismatch -> `inconsistent` evidence, exit 3). +- **Fixture D3**: `libalpha.so.1` / `libbeta.so.1` both define `COMMON_1`; + attribution asserted both ways. A4/A5 on `/bin/ls`. + +### (c) Two axes separate; deb parsing reused — Astra #4 + +- Package versions are parsed once at load by `debian/deb_parse:parse_deb_version/2` + and ordered by the frozen `resolver:version_lt/2` on `deb/3`. No local + version arithmetic exists in the lane (the last one, in `crosscheck.mjs`, + went with Sol P3). +- **Fixtures**: B1–B8, D7, **A8–A10** (computed floors `2.34` / `3.1~` equal + coreutils' declared dependency read from dpkg). + +### (d) Incomplete evidence never becomes a false veto or false compat — Astra #2 + +- Every successful ingest emits an `evidence` row; a missing/unreadable ELF + makes `requires` exit 3 **and** record an incomplete evidence row. +- `abi_verdict/5` short-circuits to `unknown(...)` without complete + requirement evidence or complete provider evidence; `at(R0)` evidence + yields `unknown(Sym@Node, evidence_release(R0))` for older releases; an + unversioned obligation is `unknown` while any NEEDED object lacks evidence + or while its only providers are `unproven`. +- **Fixtures**: C3/C3b, C4–C4e, C5/C5b, C6, C8c, **D4–D6**, A1–A3, A6, + A20–A22. + +### (e) `[min, max]` satisfiable at both ends — Astra #5 + +- `abi_range/5` evaluates **every** release of the actual axis and takes + min/max from the compatible ones (`range_min_max/3`). +- **Fixtures**: **C2** (`range(5.0, 5.0)`, not `range(1,5)`), C2c/C2d, C3b, + C7d, A13, **A15**, A23/A24, D2. + +### (f) Cross-check aggregation fixed; false 2.34-merge claim removed — Astra #6 + +- `crosscheck.mjs`: exact `sym@node` sets 3006/3006 and per-name node sets + 2763/2763 on Ubuntu 22.04 libc6; `fixtures/crosscheck/` pins the two-node + case that produced the old 91.7%. Docs no longer claim a glibc 2.34 merge + divergence. + +### (g) Frozen files untouched + +`git diff origin/main -- examples/pkg_resolver/resolver.pl +examples/pkg_resolver/resolver_store.pl examples/pkg_resolver/debian/` is +empty. The lane only *imports* `resolver:version_lt/2` and +`deb_parse:parse_deb_version/2`. + +### Astra #7 — `.symbols` templates handled or rejected loudly + +- Whitelisted tags are processed (`(arch=…)`, `(arch-bits=…)`, + `(arch-endian=…)` with `--arch`; `(ignore-blacklist)`; `(optional)` only + with `--elf`), everything else rejects the whole file with line numbers; + nothing partial is written, also in batch mode. `#PACKAGE#` headers make + `--release` mandatory. +- **Fixtures**: D7, D8/D8b/D8c/D8d, D9 x5, D11. + +## Things worth a second look + +- `default` for a hidden export at verdef index 2 encodes glibc's legacy + rule for unversioned references (`dl-lookup.c`: index < 3 is accepted + before the hidden test; D10c and `run_abi_verify.sh` verify it with the + loader). `dlsym()` lookups (`DL_LOOKUP_RETURN_NEWEST`) do not use that rule; + the lane models link-time/`DT_NEEDED` references only. +- With `--elf`, the ELF is used to prove bindings and to cross-check the + `.symbols` rows, but no `at()` rows are emitted from it, so the verdict + basis stays `curated`; ingest the ELF with `elf` (as `run_abi_verify.sh` + does for the fixture stores) to get `exact`. +- `unknown(dropped_between(R0, Src, R1))` and `unknown(absent_at(Src, R1))` + are new reasons callers may want to distinguish from the evidence-gap + reasons. +- `abi_floor/3` fails (rather than guessing) when a requirement has no + `since()` row — readelf-only provider evidence has no package floor. + +## Sol re-review pass 2 — fixes + +Sol's re-review CLOSED five of the eight original findings (P1b, P1c, P2a, P2c, +P2d) and returned REQUEST-CHANGES on four more, all rooted in one principle: a +`.symbols` file is a curated LOWER-BOUND list, not a complete export set, so its +ABSENCE proves nothing. Each fix is proven by a fixture whose check name carries +its point and that fails if the fix is reverted. `run_abi_verify.sh`: +`== 98 passed, 0 failed, 0 skipped ==`. + +| Sol finding | Fix (file) | Proving fixture(s) | +|---|---|---| +| P1 `abi_resolve.pl:289` curated absence = false hard veto | Ingest tags a plain `.symbols` (no `--elf`) as `curated`; only an `--elf` cross-check is `complete` (`ingest_symbols.mjs` `cmdSymbolsFile`). The resolver's `prov_usable/4` + `ev_says/5` let curated evidence establish PRESENCE but never ABSENCE (a curated omission yields no `Says` row → `unknown(absent_from_incomplete_evidence)`, never `missing`); `complete` absence still vetoes. **Unversioned path** (`unversioned_status/7`): the `missing` veto is gated on `\+ prov_evidence(S,_,_,complete)` for the NEEDED object, so a curated-only NEEDED library also yields `unknown` — a Fable re-verify caught an earlier over-widening to `prov_usable` here | **C10/C10b/C10c** (versioned: curated omission → unknown; present-in-curated → `provided(curated)`; the SAME store tagged `complete` DOES veto), **C12/C12b** (unversioned: curated-only omission → unknown; complete omission → missing), **A26** (real libselinux1, ingested without `--elf`, is curated: an absent symbol → unknown), **D7** (simple.symbols without `--elf` → `curated`) | +| P1 `abi_resolve.pl:311` contradictory curated floor overrides presence | A curated minimum ABOVE its evidence release is contradictory: rejected at ingest (`debLe`, exit 3) and at load (`assert_symprov` `rel_le(Deb,R0)` → the store fails to load). The existing evidence-tied aggregation (C7) already lets direct presence beat a floor | **C11/C11b** (`assert_symprov` rejects min 2.0 > release 1.0; accepts 1.0 ⩽ 1.0), **contradictory.symbols** (ingest exit 3, nothing written) | +| P2 `ingest_symbols.mjs:114` `DEB_VERSION_RE` not a real validator | `validDebVersion()` parses `[epoch:]upstream[-revision]` the way `dpkg --validate-version` does; `1:`, `1-`, `1::2` are rejected; one gate for every version/`--release` | **run_abi_verify** `bad_release_{1:,1-,1::2}` (exit 3), D9 `bad_release` | +| P3 `crosscheck.mjs` fixture cannot detect comparator restoration | Added `numnode@LIBX_2.1` / `numnode@LIBX_2.10` (opaque labels that a numeric parser would collapse) to the crosscheck pair, plus a negative `elf_numcollapse` fixture that FAILS under the correct opaque comparison but would PASS only if a numeric node comparator were reintroduced (2.10 == 2.1) | **run_abi_verify** `(sol2-P3)` numeric-collapse pair must FAIL; equal pair now 7/7 identity, 5/5 per-name | + +### Deliberate model points (documented, not requested) + +- After the P1(289) fix, `unknown(absent_at)` / `unknown(dropped_between)` treat + only DIRECT (`complete`) absence as a real absent endpoint; a curated omission + is `unknown`, never an absent observation. +- The verdict basis is the WEAKEST contributing basis; `compatible(curated)` (any + `.symbols`-only requirement) is kept distinct from `compatible(exact)` (readelf + at that release), and curated evidence can never be laundered into `exact`. +- `below_floor` remains a hard veto only as a DECLARED minimum (dpkg-shlibdeps' + floor), never from mere absence, and never overriding a direct presence + observation. +- Pre-existing, noted for awareness (unchanged this pass): if a COMPLETE ELF row + observes a symbol ABSENT at R and a curated row claims `since` ≤ R, `combine/4` + extrapolates the curated presence over the contradicting complete absence + between the two evidence releases. It needs genuinely contradictory tiers and + is not a contract violation (`Min` is documented as defeasible), but a future + pass could treat a complete absence as authoritative over a curated floor. +- Robustness: `debLe` `die()`s with a clear message if `dpkg` is not on PATH + (rather than silently rejecting every row); `load_abi_store/1` clears the + partial store if a row throws; the now-unused `bound_evidence/4` was removed. + +## Astra review — fixes + +Astra (the original reviewer) re-reviewed and confirmed original findings +#1/#3/#5/#6 CLOSED but returned REQUEST-CHANGES with new issues, the most +important found by ingesting live `libstdc++.so.6`. All real findings are fixed +and fixture-proven; `run_abi_verify.sh`: `== 108 passed, 0 failed, 0 skipped ==`. + +| Astra finding | Fix | Proving fixture(s) | +|---|---|---| +| P1 `ingest:378` STB_GNU_UNIQUE exports dropped (elfProvides kept only GLOBAL/WEAK) → false `missing` veto; live libstdc++ dropped 106 | `elfProvides` now keeps `UNIQUE` too | **run_abi_verify (astra)** ingests libstdc++.so.6 and asserts a real UNIQUE export (`_ZNSt10moneypunctIcLb0EE4intlE@GLIBCXX_3.4`) is stored | +| P1 `abi_resolve:461` unversioned historical-completeness false veto (complete evidence only BELOW Rel vetoed) | `unversioned_status/7` now vetoes `missing` only when absence is ESTABLISHED at Rel (`absence_established/2`: complete evidence at a release ≥ Rel); otherwise `unknown(absence_unestablished(...))` | **C14/C14b** (complete only at 1.0, query 2.0 → unknown; query 1.0 → missing) | +| P1 `abi_resolve:474` default binding detached from evidence (any/orphaned row's binding used) → false `compatible(exact)` for unversioned | `binding_at/6` ties the default-version binding to the evidence APPLICABLE at Rel; `unversioned_in`/`unproven`/`nondefault` use it | **C15/C15b/C15c** (default@1.0 + nondefault@2.0: query 2.0 → no_default_export; query 1.0 → compatible; orphaned default ignored) | +| P2 `ingest:201` arch selectors ≠ dpkg-architecture (`linux-any`/`any-arm` mis-matched) | `archSelects` supports only exact names (± `!`); wildcard patterns are REJECTED (exit 3), not mis-selected | **tmpl_arch_wild.symbols** rejected; **D9** asserts no store written | +| P2 `ingest:128` `validDebVersion` epoch unbounded (`2147483648:1` accepted) | epoch capped at 2147483647 (dpkg's limit) | **run_abi_verify** `bad_release_form` includes `2147483648:1` (exit 3) | +| P2 `abi_resolve:448` hypothetical unversioned drop ignored node + release | `unversioned_in` checks `\+ hyp_dropped(Hyp, Sym, Node, Rel)` per candidate export (node + release aware), like the versioned path | **C13/C13b** (drop of a different node/later release leaves the export; dropping the exact node at the release removes it) | + +### Deliberate dispositions (Astra P3, not changed) + +- `crosscheck.mjs` per-name mutation sensitivity: the negative `elf_numcollapse` + fixture guards the EXACT-IDENTITY path against a restored numeric node + comparator. The per-name figure is mathematically redundant with exact identity + when the `sym@node` key sets match (identical keys ⇒ identical per-name node + sets), so a per-name-only numeric mutation cannot be isolated by a fixture with + matching identity; the identity guard is the one the model relies on. +- `debLe` uses `dpkg --compare-versions` (the reference implementation, as the + ingest already does for `dpkg-query`/`dpkg -S`). The FROZEN-predicate boundary + governs the RESOLVER, which orders exclusively via `resolver:version_lt/2`; the + authoritative contradictory-floor rejection is the Prolog `assert_symprov` + `rel_le/2` check (frozen path), with the JS `debLe` only a loud early guard. + +### Fable re-verify of the Astra fixes — two regressions caught and fixed + +A Fable re-verification of the Astra-fix commit caught two regressions the +`binding_at` rework introduced (the harness missed them because every unversioned +`.symbols` test queries AT the evidence release): + +- **R1** (false `missing` veto): `binding_at` took the binding only from the row + AT Rel or BELOW, but `ident_status` can credit a curated `.symbols` floor row + ABOVE Rel (`combine/4`, `Min =< Rel`). Fixed: `binding_at` now also selects that + above curated row (mirroring `combine`). Fixture **C16/C16b** (unversioned ref + BELOW a curated floor, query 1.5/1.0 → `compatible(curated)`, not `missing`). +- **R2** (cross-axis false unknown): the missing-veto coverage gate compared So's + query release with a sibling's evidence release. Fixed: the gate applies to the + queried `So` only; siblings are evaluated at their own release (a sibling + lacking complete evidence is already handled earlier). Fixture **C17**. + +Also cleaned a stray NUL byte in the `debLe` cache-key string (now `\u0000` as +source text). `run_abi_verify.sh`: `== 111 passed, 0 failed, 0 skipped ==`. + +## Astra re-review 2 — unversioned-path unification + arch hardening + +Astra re-reviewed again and found more unversioned-path issues, all rooted in +`binding_at` being a SEPARATE re-derivation from `ident_status` and the veto +branches not being uniformly release-gated. Rather than patch case-by-case, the +binding was UNIFIED into the aggregation. `run_abi_verify.sh`: +`== 118 passed, 0 failed, 0 skipped ==`. + +- **Unification (fixes P1 522):** `ident_status` now returns `provided(Basis, + Binding)`; `says_status`/`combine` carry the binding from the SAME row that + establishes presence, so binding and presence can never diverge. When a + present-below row and a covering curated-above row disagree on the binding it is + `ambiguous`. `binding_at` is deleted; `unversioned_in`/`unproven`/`nondefault` + and a new `unversioned_ambiguous` read the binding straight from `ident_status`. + An `ambiguous` binding → `unknown(default_binding_conflict(...))`, never a veto + or a confident compatible. Fixture **C19**. +- **P1 470 (no_default_export release-gated):** the coverage gate + (`\+ absence_established(So, Rel)` → unknown) now precedes BOTH veto branches + (`no_default_export` and `missing`), so a nondefault export seen only in + complete evidence BELOW the query release yields `unknown`, not a veto (a + default export could be added later). Fixtures **C18/C18b**. +- **P2 arch (208):** `archSelects` validates EVERY term first (an early match or + negation can no longer skip a later unsupported term), and rejects any term + containing `any`, a tuple/GNU form (`gnu-any-amd64`), a comma-list + (`amd64,arm64`), or anything not a clean exact arch name. Fixtures + **tmpl_arch_tuple / tmpl_arch_list** (D9). +- **P2 arch attributes (285):** `arch-bits`/`arch-endian` use explicit + `ARCH_BITS`/`ARCH_ENDIAN` tables (verified vs dpkg-architecture, incl. + kfreebsd-amd64=64, mips64=big); a non-tabulated `--arch` REJECTS the row rather + than guessing. Fixture **arch_bits_unknown**. +- **P2 (test isolation):** the epoch cap is now proven through the `releases` + command (**epoch_releases**), which has no `debLe` floor check to mask it; the + hypothetical-drop node- and release-matching are isolated by **C13c** (same + release, different node) and **C13d** (same node, future release). + +### Fable re-verify of the unification — two pre-existing false verdicts fixed + +A Fable re-verification confirmed the refactor introduced NO regression but found +two PRE-EXISTING false verdicts (present on earlier commits too), now fixed. +`run_abi_verify.sh`: `== 120 passed, 0 failed, 0 skipped ==`. + +- **M2 (false compatible — mode bug):** `ident_status/5` was mode-dependent — + `combine/4` and `says_status/3` carry their cut AFTER head unification, so a + caller passing a bound `Status` (e.g. `provided(_, default)`) could skip the + clause the unbound call fires and match a later one, yielding + `compatible(extrapolated)` for a symbol observed DROPPED. Fixed: `ident_status` + computes into a fresh variable via `ident_status_/5`, then unifies, so every + caller sees the single mode-independent status (closes the whole class, not + just this case). Fixture **C20**. +- **M3 (false no_default_export):** `combine` clause 3 extrapolated the below-row + binding and ignored a disagreeing above row, so a nondefault-below + default- + above (floor not covering Rel) vetoed instead of reporting the binding as + changing. Fixed: `merge_binding/3` marks two conflicting DEFINITE bindings + `ambiguous` (→ `unknown`); `unproven` is treated as no-info, never a conflict. + Fixture **C21**. + +### Astra re-review 3 — one regression from the M3 fix, fixed + +Astra re-reviewed the unification+M2/M3 commit and confirmed everything closed +except a regression the M3 change introduced: `combine` clause 3 (extrapolating a +present-below row past a NON-covering above row) used `merge_binding`, which +promoted an `unproven` below binding to a future definite above binding — a false +`compatible` where it should stay `unknown(default_binding_unproven)`. Fixed: +clause 3 now uses `extrapolate_binding/3` (KEEP the below binding; flag +`ambiguous` only when both are definite and differ; never import the above +binding). Clause 2 (the COVERING-curated case, where the above floor does apply +at Rel) keeps `merge_binding`. Fixtures **C22** (curated-unproven below + complete +default-since-above → unknown, not compatible) and **C22b** (ELF default above +variant); C19/C21 still pass (definite conflicts → `ambiguous`). Also fixed a +stray NUL byte in this file. `run_abi_verify.sh`: `== 122 passed, 0 failed, 0 skipped ==`. diff --git a/examples/pkg_resolver/abi/SYMBOL_ABI_HOWTO.md b/examples/pkg_resolver/abi/SYMBOL_ABI_HOWTO.md new file mode 100644 index 000000000..88bf5a1a2 --- /dev/null +++ b/examples/pkg_resolver/abi/SYMBOL_ABI_HOWTO.md @@ -0,0 +1,237 @@ + + + +# Symbol-level ABI resolution — how it works, with real examples + +This extends the package resolver from coarse version constraints +(`libfoo (>= 2.0)`) to ABI compatibility at the *exact versioned symbol* level, +so we can compute the real `[min, max]` compatible release range for a binary. + +## The model + +- A **library release PROVIDES** a set of exported `sym@node` identities under + a `soname` (its ABI generation, e.g. `libc.so.6`). +- A **binary REQUIRES** a set of `sym@node` identities, each attributed to the + soname its ELF verneed table names, plus the sonames it links (`DT_NEEDED`), + plus any unversioned references. +- **Compatible(bin, release)** ⟺ every NEEDED soname is offered under its exact + name AND every required `sym@node` is exported by that soname at that + release (unversioned references: exported as `Base` or as the **default** + version — `@@`, or the oldest version node — by some NEEDED object; a + hidden `@` export does not count, exactly as in the loader). + +Two axes, never mixed: + +1. **ELF version nodes** are labels. `GLIBC_2.34` is not the number 2.34 — + it is the name of a node in `.gnu.version_d`. A requirement `foo@LIB_1` is + satisfied by `foo@LIB_1` and by nothing else; in particular not by + `foo@LIB_2` on the same soname (the loader fails with + `undefined symbol: foo, version LIB_1`). Non-numeric nodes (`PUBLIC`, + `GLIBC_PRIVATE`) and unversioned symbols (`Base`) are first-class identities. +2. **Debian package versions** order the release candidates and the `.symbols` + minimum-version field, through the frozen resolver's `deb/3` comparison + (`debian/deb_parse.pl` + `resolver:version_lt/2`): epochs (`1:2.3-1`), + tildes (`3.1~ < 3.1`), revisions (`2.35 < 2.35-0ubuntu3`), any number of + components. + +## Where the evidence comes from (three tiers, cheapest first) + +1. **`Packages` `Depends:`** — `libc6 (>= 2.34)` was computed by + `dpkg-shlibdeps` from the symbols at build time. Zero download; the coarse + resolver consumes it. `abi_floor/3` recomputes it from tier 2 and, on this + machine, reproduces coreutils' `libc6 (>= 2.34), libselinux1 (>= 3.1~)`. +2. **`.symbols` control member** — one row per `sym@node` with a curated + minimum package version: + ``` + libc.so.6 libc6 #MINVER# + | libc6 (>> 2.35), libc6 (<< 2.36) + getenv@GLIBC_2.2.5 2.2.5 + pthread_setname_np@GLIBC_2.12 2.12 + pthread_setname_np@GLIBC_2.34 2.34 + __libc_enable_secure@GLIBC_PRIVATE 0 1 + ``` + The minimum version is a **lower bound** a dependent must declare, *not* a + ground-truth introduction date: Debian policy lets a maintainer raise it + after a compatible behaviour change. The lane therefore stores it as + `since(Min, ..., R0, Bind)` tied to the evidence release `R0` the file was + taken at, and reports a release below it as `below_floor` (the same + conservative floor `dpkg-shlibdeps` emits), never as proof the symbol was + absent — and never when another evidence row (e.g. readelf at that + release) shows the symbol present. A `.symbols` file says nothing about + `@` vs `@@`, so its rows are `unproven` for unversioned references unless + the file is cross-checked against the library with `--elf lib.so` + (`run_abi_verify.sh` does this for libc6: 3006 rows, 0 disagreements). + Source-template tags are whitelisted (`(arch…)` with `--arch`, + `(ignore-blacklist)`, `(optional)` only with `--elf`); anything else, or a + block whose evidence release is unknown, rejects the whole file (exit 3), + also in `symbols-dir` batch mode. +3. **`readelf`** on the ELF itself — exact for that file's release + (`at(R0, Bind)`, with the default-version binding from `.gnu.version`), + unknown for older releases, extrapolated for newer ones. + +## Worked examples (real output, Ubuntu 22.04.5, after `./run_abi_verify.sh`) + +### 1. Requirements attributed through the version index + +``` +$ node ingest_symbols.mjs requires /bin/ls --stdout | grep -E 'start_main|freecon|gmon' +["/bin/ls|__libc_start_main@GLIBC_2.34",["libc.so.6","GLOBAL"]] +["/bin/ls|freecon@LIBSELINUX_1.0",["libselinux.so.1","GLOBAL"]] +["/bin/ls|__gmon_start__",["","WEAK"]] +``` +Each undefined symbol's `.gnu.version` index is looked up in `.gnu.version_r`, +giving *(file, node)*. Two libraries that both define a node called `COMMON_1` +therefore cannot be confused (fixture `usecommon`: `alpha_fn@COMMON_1 -> +libalpha.so.1`, `beta_fn@COMMON_1 -> libbeta.so.1`). Unversioned and weak +references are kept, flagged, and never silently dropped. + +### 2. The curated floor equals the declared dependency + +``` +$ swipl -q -g main -t halt abi_cli.pl -- .out/store floor /bin/ls libc.so.6 +floor /bin/ls libc.so.6: 2.34 +$ swipl -q -g main -t halt abi_cli.pl -- .out/store floor /bin/ls libselinux.so.1 +floor /bin/ls libselinux.so.1: 3.1~ +$ dpkg-query -W -f '${Pre-Depends}\n' coreutils +libacl1 (>= 2.2.23), libattr1 (>= 1:2.4.44), libc6 (>= 2.34), libgmp10 (>= 2:6.2.1+dfsg), libselinux1 (>= 3.1~) +``` + +### 3. Verdicts on the actual release axis + +``` +$ ... axis libc.so.6 +axis libc.so.6: [2.35-0ubuntu3,2.35-0ubuntu3.15] # apt-cache madison + dpkg +$ ... range /bin/ls libc.so.6 +range /bin/ls libc.so.6: [2.35-0ubuntu3, 2.35-0ubuntu3.15] + 2.35-0ubuntu3: compatible(curated) + 2.35-0ubuntu3.15: compatible(curated) +$ ... verdict /bin/ls libc.so.6 2.31-0ubuntu9.9 +verdict /bin/ls libc.so.6 2.31-0ubuntu9.9: incompatible([below_floor('__libc_start_main'@'GLIBC_2.34','2.34'),below_floor(lstat@'GLIBC_2.33','2.33')]) +``` +The candidates are releases, not symbol-introduction points; `range/3` reports +a `[min, max]` whose ends both carry `compatible` verdicts. With an axis +extended below the floor (`2.31-0ubuntu9.9, 2.34-0ubuntu3, ...`) the min is +`2.34-0ubuntu3` — the first release that actually satisfies the requirements. +The basis is `curated` because the only evidence is the `.symbols` file; +`exact` is reserved for readelf observations at that very release. Bounds +from several evidence rows are aggregated, never taken first-match: if +readelf evidence for `2.31-0ubuntu9.9` were ingested and showed every +required identity, that release would be `compatible(exact)` despite the +curated floor of 2.34 (test A25 does exactly that). + +### 4. Exact node identity (the case the old model got wrong) + +Fixture: `libfoo.so.1` v1 exports `foo@LIB_1`; v2 keeps a `LIB_1` node but +exports `foo` only as `foo@LIB_2`. `usefoo` is linked against v1. +``` +$ LD_LIBRARY_PATH=.out/fx/v2 .out/fx/usefoo +usefoo: symbol lookup error: usefoo: undefined symbol: foo, version LIB_1 +$ ... .out/fx/store_foo_v2 verdict .out/fx/usefoo libfoo.so.1 2.0-1 +verdict ... libfoo.so.1 2.0-1: incompatible([missing(foo@'LIB_1')]) +``` +A name-level model with a numeric intro would have said "compatible" here. + +### 5. Where a real MAX comes from — a removal (hypothetical) + +``` +$ ... range /bin/ls libc.so.6 getenv GLIBC_2.2.5 2.35-0ubuntu3.15 +range /bin/ls libc.so.6: [2.35-0ubuntu3, 2.35-0ubuntu3] + 2.35-0ubuntu3: compatible(exact) + 2.35-0ubuntu3.15: incompatible([missing(getenv@'GLIBC_2.2.5',hypothetical_drop)]) +$ ... range /bin/ls libc.so.6 __libc_start_main GLIBC_2.34 2.35-0ubuntu3 +range /bin/ls libc.so.6: no_candidate +``` + +### 6. Incomplete evidence is "unknown", not "compatible" + +``` +$ node ingest_symbols.mjs requires /nonexistent/bin --out .out/x ; echo exit=$? +ingest_symbols: requires /nonexistent/bin: missing_file; recorded INCOMPLETE evidence, no requirement rows +exit=3 +$ ... verdict /nonexistent/bin libc.so.6 2.35-0ubuntu3 +verdict /nonexistent/bin libc.so.6 2.35-0ubuntu3: unknown([no_requires_evidence('/nonexistent/bin')]) +``` +Likewise a NEEDED soname with no provider evidence yields +`unknown([no_provider_evidence(So)])`, and readelf-only evidence yields +`unknown` for releases older than the file's own. + +### 7. Cross-check: the two provider tiers agree exactly + +``` + exact sym@node identity: .symbols=3006 readelf=3006 shared=3006 only-readelf=0 only-.symbols=0 + identity agreement: 3006/3006 (100.0%) + per-name node-set agreement: 2763/2763 (100.0%) +``` +The earlier "91.7% agreement, explained by the glibc 2.34 pthread/rt merge" +was an aggregation bug: the last curated row of a symbol was compared with the +earliest ELF node of that symbol, so any symbol with two nodes +(`pthread_setname_np@GLIBC_2.12` + `@GLIBC_2.34`) "disagreed". Compared +consistently, everything agrees; the merge explanation was false. The +per-name figure now compares the *set* of nodes per name — nothing is parsed +out of a node name and nothing is ordered — and `fixtures/crosscheck/` pins +the two-node case (plus a `GLIBC_PRIVATE` node and a `Base` node) as a static +regression. Two empty inputs fail the check instead of passing on `NaN`. + +### 8. An unversioned reference vs a non-default-only export + +Fixture `libhid.so.1`: `hid_fn` is exported only as hidden `hid_fn@HID_1` +(`.symver` with a single `@`); `usehid` was linked against an unversioned +build and so references `hid_fn` without a version. +``` +$ LD_LIBRARY_PATH=.out/fx/hid_idx3 .out/fx/usehid +usehid: symbol lookup error: usehid: undefined symbol: hid_fn +$ grep hid_fn .out/fx/store_hid_idx3/symprov.jsonl +["libhid.so.1|hid_fn@HID_1",["at","1.0-1","nondefault"]] +$ ... .out/fx/store_hid_idx3 status .out/fx/usehid libhid.so.1 1.0-1 + missing(hid_fn,no_default_export('libhid.so.1','HID_1')) +``` +The same hidden export at verdef index 2 (the oldest node, `hid_idx2`) is +bound by the loader for legacy unversioned references, runs, and is recorded +`default`. A `.symbols`-only store cannot tell `@` from `@@`, so there the +answer is `unknown([unknown(hid_fn, default_binding_unproven(...))])`, never +`compatible`. + +## Epistemics + +- **Absence / soname mismatch = hard veto** (`incompatible`) — valid only + when requirement evidence is complete and provider evidence for that soname + is complete and attributed by index. Otherwise the answer is `unknown`. + A plain `.symbols` file is `curated`, not `complete` (only readelf or an + `--elf` cross-check observes the export set fully), so **a symbol's absence + from a `.symbols` list is `unknown`, never a veto** (Sol re-review 2, P1); + its presence is still evidence (`compatible(curated)`). +- **Presence = defeasible "structurally possible"** (`compatible(exact | + curated | extrapolated)`) — necessary, not sufficient; semantics are + unverified. It never outranks a declared or tested dependency; it widens + the candidate set with a low-confidence maybe. +- **`curated`** means the presence rests on `.symbols` metadata (a curated + export list), not on a direct readelf observation at that release; it is + reported distinctly from `exact`. +- **`below_floor`** is a curated floor, not proof of absence, and is reported + distinctly so a caller can choose to treat it as declared-dependency + strength rather than ELF-hard strength. It never overrides another evidence + row that shows the identity present at the release. +- **`extrapolated`** relies on the in-soname monotone-export assumption and is + reported distinctly from `exact`. Absence propagates the other way: absent + from complete evidence at `R1` means absent at every `Rel <= R1` + (`missing(..., observed_absent(Src, R1))`), but says nothing about later + releases (`unknown(..., absent_at(Src, R1))`). Present at `R0` and absent + at a later `R1` is an observed drop: the releases in between are + `unknown(..., dropped_between(R0, Src, R1))`. + +Confidence order: `tested > declared repo dep > ELF hard veto / ELF maybe > +soname default`. + +## Limits + +- The unversioned-reference rule follows `ld.so` for `DT_NEEDED`-driven + binding: `Base`, the `@@` default, or the oldest version node (verdef + index 2, accepted by glibc for legacy binaries even when hidden). `dlsym()` + lookups use a different rule and are not modelled. +- `.symbols` source-template constructs that need the binary to expand + (`(symver)`, `(regex)`, quoted C++ patterns) and any unknown tag are + rejected, not interpreted; `(optional)` rows need `--elf`. +- `soname_mismatch` needs a declared `replaces(New, Old)` row; the lane does + not guess that `libfoo.so.2` succeeds `libfoo.so.1` from the name. +- The release axis is an input (from `apt-cache madison`, dpkg, a snapshot + store); the lane never invents candidates from symbol data. diff --git a/examples/pkg_resolver/abi/abi_cli.pl b/examples/pkg_resolver/abi/abi_cli.pl new file mode 100644 index 000000000..ff50cf29d --- /dev/null +++ b/examples/pkg_resolver/abi/abi_cli.pl @@ -0,0 +1,62 @@ +:- encoding(utf8). +% SPDX-License-Identifier: MIT OR Apache-2.0 +% Copyright (c) 2026 John William Creighton (@s243a) +% +% abi_cli.pl -- a small callable driver over the ABI resolver. +% +% swipl -q -g main -t halt examples/pkg_resolver/abi/abi_cli.pl -- \ +% +% +% Commands: +% verdict [DropSym DropNode DropAt] +% compatible(exact|curated|extrapolated) | incompatible([...]) | unknown([...]) | not_needed(_) +% status one line per requirement (provided / missing / ...) +% floor curated lower bound implied by `.symbols` (= dpkg-shlibdeps' dep) +% axis the ingested release candidates, ascending +% range [DropSym DropNode DropAt] +% range(Min, Max, ...) over the release axis (both ends compatible), or +% no_candidate / unknown / no_releases + +:- use_module(abi_resolve). + +main :- + current_prolog_flag(argv, Argv), + ( Argv = [Dir, Cmd | Args] -> true ; usage, halt(2) ), + load_abi_store(Dir), + atom_string(CmdA, Cmd), + run(CmdA, Args). + +usage :- + format(user_error, + "usage: abi_cli.pl -- verdict|status|floor|axis|range ~n", []). + +drop_of([], none). +drop_of([Sym, Node, At], drop(Sym, Node, At)). + +run(verdict, [Bin, So, Rel | DropArgs]) :- !, + drop_of(DropArgs, Drop), + abi_verdict(Bin, So, Rel, Drop, V), + format("verdict ~w ~w ~w: ~q~n", [Bin, So, Rel, V]). +run(status, [Bin, So, Rel]) :- !, + rel_term(Rel, R), + forall(req_status(Bin, So, R, none, S), format(" ~q~n", [S])). +run(floor, [Bin, So]) :- !, + ( abi_floor(Bin, So, F) + -> format("floor ~w ~w: ~w~n", [Bin, So, F]) + ; format("floor ~w ~w: none (a requirement has no since() provider row)~n", [Bin, So]) + ). +run(axis, [So]) :- !, + release_axis(So, Rels), + format("axis ~w: ~w~n", [So, Rels]). +run(range, [Bin, So | DropArgs]) :- !, + drop_of(DropArgs, Drop), + abi_range(Bin, So, Drop, R), + ( R = range(Min, Max, Pairs) + -> format("range ~w ~w: [~w, ~w]~n", [Bin, So, Min, Max]), + forall(member(A-V, Pairs), format(" ~w: ~q~n", [A, V])) + ; R =.. [Kind, Pairs], is_list(Pairs) + -> format("range ~w ~w: ~w~n", [Bin, So, Kind]), + forall(member(A-V, Pairs), format(" ~w: ~q~n", [A, V])) + ; format("range ~w ~w: ~q~n", [Bin, So, R]) + ). +run(_, _) :- usage, halt(2). diff --git a/examples/pkg_resolver/abi/abi_resolve.pl b/examples/pkg_resolver/abi/abi_resolve.pl new file mode 100644 index 000000000..6249441b0 --- /dev/null +++ b/examples/pkg_resolver/abi/abi_resolve.pl @@ -0,0 +1,695 @@ +:- encoding(utf8). +% SPDX-License-Identifier: MIT OR Apache-2.0 +% Copyright (c) 2026 John William Creighton (@s243a) +% +% abi_resolve.pl -- symbol-level ABI-compatibility resolver (redesigned after +% the PR #4262 review, revised after Sol's re-review; see REVIEW_NOTES.md for +% the point-by-point map). +% +% MODEL +% Two independent axes: +% * ELF version-node axis: a node (GLIBC_2.34, LIBSELINUX_1.0, COMMON_1, +% PUBLIC, Base) is an opaque label. A requirement `Sym@Node` on soname So +% is satisfied only by a provider row with the SAME (So, Sym, Node) -- +% string equality, never numeric ordering, never a bare-name fallback. +% `Base` = dpkg's spelling of "unversioned". An unversioned REQUIREMENT +% (no node) binds, as the loader does, only to a `Base` export or to a +% DEFAULT export (`@@`, or the oldest version node); a provider row whose +% default binding is unproven (a `.symbols` row not cross-checked against +% the ELF) yields unknown, never compatible. +% * Debian package-version axis: the `.symbols` minimum-version and the +% release candidates are deb/3 terms produced by debian/deb_parse.pl and +% ordered by the frozen resolver:version_lt/2 (epoch, ~, revision all +% handled there). A non-deb release id is kept as label(Atom) and only +% ever matches itself. +% Evidence is explicit and every provider bound is tied to the evidence row +% it rests on (Sol P1a): +% prov_evidence(So, Src, R0, Status) -- what is known about So's export +% set at evidence release R0 (Src = symbols | elf): +% complete -- the export set was OBSERVED completely: readelf on the +% ELF, or a `.symbols` file cross-checked against the ELF +% with --elf (the ingest rejects any difference). Absence +% from it is a fact. +% curated -- a `.symbols` file ingested WITHOUT --elf: a curated +% LOWER-BOUND list, not a complete export set. Presence in +% it is (curated) evidence; ABSENCE FROM IT PROVES NOTHING +% (Sol re-review 2, P1): an omitted identity is `unknown`, +% never missing / below_floor / dropped / absent_at. +% symprov(So, Sym, Node, since(Min, MinAtom, R0, Bind)) -- from the +% `.symbols` evidence at R0: exported at R0 and, by the curated lower +% bound, at every release >= Min. Min is NOT a ground-truth introduction +% date (Debian policy lets it be raised); R < Min is `below_floor` (the +% conservative floor dpkg-shlibdeps emits) unless direct evidence says +% otherwise. Min =< R0 always: a curated minimum cannot exceed the +% release the row was curated from; a row violating that is +% CONTRADICTORY, rejected by the ingest and by load_abi_store/1, and -- +% if asserted directly -- evidence for nothing (Sol re-review 2, P1). +% symprov(So, Sym, Node, at(R0, Bind)) -- from readelf at R0. +% Bind = default | nondefault | unproven (default-version binding) +% req_evidence(Bin, Src, Status, Detail) -- Bin's requirement set is +% complete, or why not (missing_file / readelf_failed / inconsistent). +% Per-identity status at release Rel aggregates EVERY usable evidence row +% of the soname (ident_status/5): evidence AT Rel decides directly; else the +% nearest evidence BELOW Rel (presence extrapolates upward) and the nearest +% evidence ABOVE Rel (absence propagates downward, a curated floor covers +% Rel >= Min) are combined. A release satisfied by ANY evidence row is +% never vetoed by another row's bound, and a direct presence observation at +% or below Rel prevents any below_floor veto at Rel. +% Extrapolation (defeasible, documented): within a soname, exports do not +% disappear (removing one is an ABI break that requires a soname bump), so +% presence at R0 extends to R > R0 with basis `extrapolated`, and absence +% from a COMPLETE export set at R1 is a veto for R =< R1. Absence at R1 says +% nothing about R > R1 (later releases add symbols): unknown. Presence never +% becomes a guarantee: compatible(_) is defeasible. A hypothetical +% drop(Sym, Node, At) models an in-soname removal to exercise the upper bound. +% +% VERDICTS abi_verdict(Bin, So, Rel, Verdict): +% compatible(exact | curated | extrapolated) +% exact -- every requirement observed by readelf at exactly Rel +% curated -- at least one rests on `.symbols` metadata only (Sol residual) +% extrapolated -- at least one rests on the monotone-export assumption +% incompatible([missing(Sym@Node) | missing(Sym@Node, Why) | below_floor(Sym@Node, MinAtom) +% | soname_mismatch(offered(So), needed(N)) ...]) -- HARD veto, +% only reachable when requirement AND provider evidence are complete +% unknown([no_requires_evidence(Bin) | requires_evidence(Status, Detail) +% | no_provider_evidence(So) | unknown(Sym@Node, Why) +% | unknown(Sym, Why) ...]) +% not_needed(So) -- Bin has no DT_NEEDED entry for So and So is not a +% declared replacement (replaces/2) of a NEEDED soname +% +% RANGE abi_range(Bin, So, Releases, Result): every release in the ACTUAL +% candidate axis is evaluated; range(Min, Max, Pairs) has compatible verdicts +% at BOTH ends by construction (Min/Max are drawn from the compatible set). +% +% Frozen resolver.pl / resolver_store.pl are NOT edited. + +:- module(abi_resolve, [ + op(200, xfx, @), + load_abi_store/1, + abi_store_clear/0, + symprov/4, + symreq/5, + needed/2, + replaces/2, + prov_evidence/4, + req_evidence/4, + release/3, + rel_term/2, + rel_le/2, + rel_lt/2, + ident_status/5, + provides_at/5, + req_status/5, + abi_verdict/4, + abi_verdict/5, + abi_floor/3, + soname_offer/3, + release_axis/2, + abi_range/3, + abi_range/4, + abi_range/5, + range_min_max/3 +]). + +:- op(200, xfx, @). % Sym@Node terms in statuses/verdicts + +:- use_module('../resolver', [version_lt/2]). +:- use_module('../debian/deb_parse', [parse_deb_version/2]). +:- use_module(library(http/json)). +:- use_module(library(lists)). +:- use_module(library(apply)). + +:- dynamic symprov/4. % symprov(SoName, Sym, Node, Bound) Bound = since(Deb, Atom, R0, Bind) | at(R0, Bind) +:- dynamic symreq/5. % symreq(Binary, Sym, Node, SoName, Bind) Node/SoName = none if unversioned +:- dynamic needed/2. % needed(Binary, SoName) +:- dynamic replaces/2. % replaces(NewSoName, OldSoName) declared soname succession +:- dynamic prov_evidence/4. % prov_evidence(SoName, Src, Rel, Status) +:- dynamic req_evidence/4. % req_evidence(Binary, Src, Status, Detail) +:- dynamic release/3. % release(SoName, Rel, Atom) + +% --------------------------------------------------------------------------- +% Store loading (P/2 JSONL: [Key, Value] per line; values may be JSON arrays) +% --------------------------------------------------------------------------- + +abi_store_clear :- + retractall(symprov(_, _, _, _)), + retractall(symreq(_, _, _, _, _)), + retractall(needed(_, _)), + retractall(replaces(_, _)), + retractall(prov_evidence(_, _, _, _)), + retractall(req_evidence(_, _, _, _)), + retractall(release(_, _, _)). + +load_abi_store(Dir) :- + abi_store_clear, + % A row that fails to parse/validate (e.g. a contradictory since(Min>R0)) + % throws; clear the partial store so callers never compute on half a load. + catch(load_abi_rows(Dir), E, ( abi_store_clear, throw(E) )). + +load_abi_rows(Dir) :- + load_rows(Dir, 'symprov.jsonl', assert_symprov), + load_rows(Dir, 'symreq.jsonl', assert_symreq), + load_rows(Dir, 'needed.jsonl', assert_needed), + load_rows(Dir, 'replaces.jsonl', assert_replaces), + load_rows(Dir, 'evidence.jsonl', assert_evidence), + load_rows(Dir, 'releases.jsonl', assert_release). + +load_rows(Dir, File, Handler) :- + atomic_list_concat([Dir, '/', File], Path), + ( exists_file(Path) + -> setup_call_cleanup(open(Path, read, S), + load_row_lines(S, Path, 1, Handler), + close(S)) + ; true + ). + +load_row_lines(S, Path, N, Handler) :- + read_line_to_string(S, Line), + ( Line == end_of_file + -> true + ; ( Line == "" + -> true + ; atom_string(Atom, Line), + ( catch(atom_json_term(Atom, [K, V], [value_string_as(atom)]), _, fail), + catch(call(Handler, K, V), _, fail) + -> true + ; throw(error(abi_store_row(Path, N, Line), load_abi_store/1)) + ) + ), + N1 is N + 1, + load_row_lines(S, Path, N1, Handler) + ). + +% "|@" -> +% ["since", MinVer, EvidenceRelease, Bind] -> since(Deb, MinVer, R0, Bind) +% ["at", EvidenceRelease, Bind] -> at(R0, Bind) +% The evidence release is part of the row so a bound is tied to the evidence +% it came from even when several evidence rows exist for one soname. +assert_symprov(K, [Kind | V]) :- + split_first(K, '|', So, Ident), + split_last(Ident, '@', Sym, Node), + Node \== '', + ( Kind == since + -> V = [Min, EvRel, Bind0], + parse_deb_version(Min, Deb), rel_term(EvRel, R0), + rel_le(Deb, R0), % Sol re-review 2, P1: a curated minimum cannot + % exceed the release it was curated from; a + % contradictory since(Min>R0) row is rejected + % (the whole store then fails to load). + binding(Node, Bind0, Bind), + Bound = since(Deb, Min, R0, Bind) + ; Kind == at + -> V = [EvRel, Bind0], + rel_term(EvRel, R0), + binding(Node, Bind0, Bind), + Bound = at(R0, Bind) + ), + assertz(symprov(So, Sym, Node, Bound)). + +% A `Base` (unversioned) export always binds an unversioned reference. +binding('Base', _, default) :- !. +binding(_, Bind, Bind) :- memberchk(Bind, [default, nondefault, unproven]). + +% "|[@]" -> symreq(Bin, Sym, Node, SoName, Bind) +assert_symreq(K, [So0, Bind]) :- + split_first(K, '|', Bin, Ident), + ( split_last(Ident, '@', Sym, Node) + -> Node \== '', So0 \== '', So = So0 + ; Sym = Ident, Node = none, So = none + ), + memberchk(Bind, ['GLOBAL', 'WEAK']), + assertz(symreq(Bin, Sym, Node, So, Bind)). + +assert_needed(Bin, So) :- + atom(So), + assertz(needed(Bin, So)). + +assert_replaces(New, Old) :- + atom(Old), + assertz(replaces(New, Old)). + +assert_evidence(K, V) :- + split_first(K, '|', Kind, Subject), + ( Kind == provides + -> V = [Src, RelAtom, Status, _Source], + memberchk(Src, [symbols, elf]), + rel_term(RelAtom, Rel), + assertz(prov_evidence(Subject, Src, Rel, Status)) + ; Kind == requires + -> V = [Src, Status, Detail], + assertz(req_evidence(Subject, Src, Status, Detail)) + ). + +assert_release(So, V) :- + rel_term(V, Rel), + ( release(So, Rel, _) -> true ; assertz(release(So, Rel, V)) ). + +split_first(Atom, Sep, Before, After) :- + sub_atom(Atom, B, _, A, Sep), !, + sub_atom(Atom, 0, B, _, Before), + sub_atom(Atom, _, A, 0, After). + +split_last(Atom, Sep, Before, After) :- + sub_atom(Atom, B, _, A, Sep), + \+ ( sub_atom(Atom, B2, _, _, Sep), B2 > B ), !, + sub_atom(Atom, 0, B, _, Before), + sub_atom(Atom, _, A, 0, After). + +% --------------------------------------------------------------------------- +% Release axis (Debian package versions; labels only match themselves) +% --------------------------------------------------------------------------- + +% rel_term(+Atom, -Rel): deb/3 via the frozen parser, else label(Atom). +rel_term(Atom, Rel) :- + ( catch(parse_deb_version(Atom, Deb), _, fail), + Deb = deb(_, [s([], _)|_], _) % upstream starts with a digit (Policy 5.6.12) + -> Rel = Deb + ; Rel = label(Atom) + ). + +rel_lt(deb(E1, U1, R1), deb(E2, U2, R2)) :- + version_lt(deb(E1, U1, R1), deb(E2, U2, R2)). + +rel_le(A, B) :- + ( A = deb(_, _, _), B = deb(_, _, _) + -> \+ version_lt(B, A) + ; A == B + ). + +rel_cmp(Order, A-_, B-_) :- + ( rel_lt(A, B) -> Order = (<) + ; rel_lt(B, A) -> Order = (>) + ; A = deb(_, _, _), B = label(_) -> Order = (<) + ; A = label(_), B = deb(_, _, _) -> Order = (>) + ; A == B -> Order = (=) + ; compare(Order, A, B) + ). + +% release_axis(SoName, AscendingAtoms): the actual release candidates known for +% the soname (ingested `releases` rows), ascending, deduplicated. +release_axis(So, Atoms) :- + findall(R-A, release(So, R, A), Pairs0), + predsort(rel_cmp, Pairs0, Pairs), + pairs_values(Pairs, Atoms). + +% --------------------------------------------------------------------------- +% Evidence rows and what each says about one identity (Sol P1a) +% --------------------------------------------------------------------------- + +% observed(So, Sym, Node, Src, R1, Bound): the identity is in the Src +% evidence taken at R1. +observed(So, Sym, Node, symbols, R1, B) :- B = since(_, _, R1, _), symprov(So, Sym, Node, B). +observed(So, Sym, Node, elf, R1, B) :- B = at(R1, _), symprov(So, Sym, Node, B). + +% prov_usable(So, Src, R0, Status): a provider evidence row the resolver can +% use -- `complete` (readelf, or a `.symbols` file cross-checked against the ELF +% with --elf: the export set is fully observed, so ABSENCE from it is a fact) or +% `curated` (a plain `.symbols` lower-bound list ingested WITHOUT --elf: +% PRESENCE in it is curated evidence, ABSENCE FROM IT PROVES NOTHING). +prov_usable(So, Src, R0, Status) :- + prov_evidence(So, Src, R0, Status), + memberchk(Status, [complete, curated]). + +% ev_says(So, Sym, Node, R1, Says): for every usable evidence row (Src, R1) of +% So, whether Sym@Node is present in it (and under which bound) or absent. Only +% a COMPLETE export set can assert absence; a curated row that omits the +% identity says nothing about it (Sol re-review 2, P1) -- it yields no Says row. +ev_says(So, Sym, Node, R1, Says) :- + prov_usable(So, Src, R1, Status), + ( observed(So, Sym, Node, Src, R1, Bound) + -> Says = present(Src, Bound) + ; Status == complete + -> Says = absent(Src) + ; fail + ). + +% ident_status(+So, +Sym, +Node, +Rel, -Status): the status of the exact +% identity Sym@Node on So at Rel, aggregated over ALL complete evidence rows. +% provided(exact | curated | extrapolated) +% missing(Why) absent from a complete export set at/above Rel +% below_floor(MinAtom) only a curated floor above Rel covers it, and Rel < Min +% unknown(Why) no evidence row speaks about Rel +% Rule: evidence AT Rel decides (readelf before .symbols). Otherwise the +% nearest evidence BELOW Rel (last known state) and the nearest evidence ABOVE +% Rel are combined: presence below extrapolates upward unless the row above +% observed absence (then the identity was dropped somewhere in between: +% unknown, not a false compat and not a false veto); absence above propagates +% downward (monotone exports); a curated floor above covers Rel >= Min. +% Mode-insensitive: compute the status into a FRESH variable, then unify with the +% caller's pattern. combine/4 and says_status/3 carry their cut AFTER head +% unification, so a caller passing a bound Status (e.g. provided(_, default)) +% must NOT be allowed to skip the clause the unbound call would fire and match a +% later one -- that gave a false compatible for a symbol observed dropped (Fable +% re-verify M2). Callers therefore always see the single, mode-independent status. +ident_status(So, Sym, Node, Rel, Status) :- + ident_status_(So, Sym, Node, Rel, S0), !, + Status = S0. + +ident_status_(So, Sym, Node, Rel, Status) :- + findall(R1-Says, ev_says(So, Sym, Node, R1, Says), Rows), + Rows \== [], + ( member(Rel1-_, Rows), Rel1 == Rel + -> says_at(Rows, Rel, Says), + says_status(Says, Rel, Status) + ; nearest_below(Rows, Rel, Below), + nearest_above(Rows, Rel, Above), + combine(Below, Above, Rel, Status) + ). + +% says_at(Rows, R, Says): what the evidence taken at exactly R says; when both +% tiers were taken at R, readelf (direct observation) decides. +says_at(Rows, R, Says) :- + ( member(R1-present(elf, B), Rows), R1 == R -> Says = present(elf, B) + ; member(R1-absent(elf), Rows), R1 == R -> Says = absent(elf) + ; member(R1-present(symbols, B), Rows), R1 == R -> Says = present(symbols, B) + ; Says = absent(symbols) + ). + +% provided(Basis, Binding): the default-version binding comes from the SAME +% evidence row that establishes presence, so an unversioned reference can never +% pick a binding ident_status did not credit (Astra re-review 2). Binding is +% default | nondefault | unproven, or `ambiguous` when two credited rows disagree. +says_status(present(elf, at(_, Bind)), _, provided(exact, Bind)). +says_status(present(symbols, since(Min, MinAtom, _, Bind)), Rel, Status) :- + ( rel_le(Min, Rel) -> Status = provided(curated, Bind) ; Status = below_floor(MinAtom) ). +says_status(absent(Src), Rel, missing(observed_absent(Src, Rel))). + +% Distinct evidence releases strictly below / above Rel; the nearest one wins. +nearest_below(Rows, Rel, Below) :- + findall(R-R, ( member(R-_, Rows), rel_lt(R, Rel) ), Bs0), + predsort(rel_cmp, Bs0, Bs), + ( Bs == [] -> Below = none + ; last(Bs, R0-_), says_at(Rows, R0, Says), Below = ev(R0, Says) + ). + +nearest_above(Rows, Rel, Above) :- + findall(R-R, ( member(R-_, Rows), rel_lt(Rel, R) ), As0), + predsort(rel_cmp, As0, As), + ( As == [] -> Above = none + ; As = [R1-_|_], says_at(Rows, R1, Says), Above = ev(R1, Says) + ). + +% combine(Below, Above, Rel, Status) -- provided carries (Basis, Binding); when +% a present-below row and a covering curated-above row disagree on the binding, +% the binding is `ambiguous` (Astra re-review 2: conflicting cross-tier bindings +% must not yield a confident veto or a confident compatible). +combine(ev(R0, present(_, _)), ev(R1, absent(Src)), _, unknown(dropped_between(R0, Src, R1))) :- !. +combine(ev(_, present(_, BoundB)), ev(_, present(symbols, since(Min, _, _, BindA))), Rel, provided(curated, Bind)) :- + rel_le(Min, Rel), !, + bound_binding(BoundB, BindB), + merge_binding(BindB, BindA, Bind). +% below present, extrapolated upward. If a present row ABOVE records a DEFINITE +% binding that conflicts with the below one, the binding is changing across Rel: +% mark it ambiguous rather than confidently extrapolate the below binding (Fable +% re-verify M3). `unproven` above is no-info, not a conflict. +combine(ev(_, present(_, BoundB)), Above, _, provided(extrapolated, Bind)) :- !, + bound_binding(BoundB, BindB), + ( above_binding(Above, BindA) -> extrapolate_binding(BindB, BindA, Bind) ; Bind = BindB ). +combine(_, ev(R1, absent(Src)), _, missing(observed_absent(Src, R1))) :- !. +combine(_, ev(_, present(symbols, since(Min, MinAtom, _, Bind))), Rel, Status) :- !, + ( rel_le(Min, Rel) -> Status = provided(curated, Bind) ; Status = below_floor(MinAtom) ). +combine(_, ev(R1, present(elf, _)), _, unknown(evidence_release(R1))) :- !. +combine(ev(R0, absent(Src)), none, _, unknown(absent_at(Src, R0))) :- !. +combine(none, none, _, unknown(no_evidence)). + +% above_binding(Above, Bind): the default-version binding a present ABOVE row +% records (fails for none / absent -- no binding to conflict with). +above_binding(ev(_, present(elf, at(_, Bind))), Bind). +above_binding(ev(_, present(symbols, since(_, _, _, Bind))), Bind). + +% merge_binding(BelowOrAt, Covering, Merged): for a COVERING curated row (its +% floor applies AT Rel), two DEFINITE bindings that differ -> ambiguous; otherwise +% the definite one wins (`unproven` is no-info, never a conflict). +merge_binding(B, B, B) :- !. +merge_binding(B1, B2, ambiguous) :- + memberchk(B1, [default, nondefault]), memberchk(B2, [default, nondefault]), !. +merge_binding(B1, _, B1) :- memberchk(B1, [default, nondefault]), !. +merge_binding(_, B2, B2). + +% extrapolate_binding(BindBelow, BindAbove, Bind): extrapolating a present-below +% row past a NON-covering above row -- the above binding does NOT apply at Rel, so +% KEEP the below binding; only flag `ambiguous` when both are definite and differ +% (the binding is changing across Rel). Never promote an unproven below to a +% future definite above (Astra re-review 3: that gave a false compatible). +extrapolate_binding(B1, B2, ambiguous) :- + memberchk(B1, [default, nondefault]), memberchk(B2, [default, nondefault]), B1 \== B2, !. +extrapolate_binding(B1, _, B1). + +% provides_at(So, Sym, Node, Rel, Basis): So exports exactly Sym@Node at Rel. +provides_at(So, Sym, Node, Rel, Basis) :- + ident_status(So, Sym, Node, Rel, provided(Basis, _)). + +% node_binding(So, Sym, Node, Bind): the default-version binding recorded for +% an export (default: an unversioned reference binds to it; nondefault: it +% does not; unproven: `.symbols` row not cross-checked against the ELF). +node_binding(So, Sym, Node, Bind) :- + symprov(So, Sym, Node, Bound), + ( Bound = since(_, _, _, B) -> Bind = B ; Bound = at(_, B) -> Bind = B ). + +hyp_dropped(drop(Sym, Node, At), Sym, Node, Rel) :- + rel_term(At, AtRel), + rel_le(AtRel, Rel). + +% --------------------------------------------------------------------------- +% Per-requirement status +% --------------------------------------------------------------------------- + +% req_status(Bin, So, Rel, Hyp, Status) enumerates one Status per requirement +% of Bin that concerns So (versioned requirements attributed to So via the +% version index, plus Bin's unversioned requirements, which the loader +% resolves against any NEEDED object). +req_status(Bin, So, Rel, Hyp, Status) :- + symreq(Bin, Sym, Node, So, Bind), + Node \== none, + versioned_status(So, Sym, Node, Bind, Rel, Hyp, Status). +req_status(Bin, So, Rel, Hyp, Status) :- + symreq(Bin, Sym, none, none, Bind), + unversioned_status(Bin, So, Sym, Bind, Rel, Hyp, Status). + +% missing(Sym@Node) = absent from the complete export set observed AT Rel; +% missing(Sym@Node, observed_absent(Src, R1)) = absent at a LATER release R1, +% hence absent at Rel under monotone exports (the inference is visible). +versioned_status(So, Sym, Node, Bind, Rel, Hyp, Status) :- + ( hyp_dropped(Hyp, Sym, Node, Rel) + -> Status = missing(Sym@Node, hypothetical_drop) + ; ident_status(So, Sym, Node, Rel, S) + -> ( S = provided(Basis, _) -> Status = provided(Sym@Node, Basis) + ; S = below_floor(MinAtom) -> Status = below_floor(Sym@Node, MinAtom) + ; S = missing(_), Bind == 'WEAK' -> Status = weak_unresolved(Sym@Node) + ; S = missing(observed_absent(_, R1)), R1 == Rel -> Status = missing(Sym@Node) + ; S = missing(Why) -> Status = missing(Sym@Node, Why) + ; S = unknown(Why) -> Status = unknown(Sym@Node, Why) + ) + ; prov_usable(So, _, _, _) % So has (curated) evidence, but not for + -> Status = unknown(Sym@Node, absent_from_incomplete_evidence(So)) % this identity: unknown, not missing (Sol re-review 2, P1) + ; Status = unknown(Sym@Node, no_provider_evidence(So)) + ). + +% An unversioned reference binds (Sol P1b) to a `Base` export or a DEFAULT export +% of Sym in any NEEDED object -- never a non-default (`@`) one. The binding comes +% from ident_status (provided(Basis, Binding)), so it always reflects the row that +% established presence at the queried release; binding and presence never diverge +% (Astra re-review 2). A curated row's binding is `unproven`, and conflicting +% cross-tier bindings are `ambiguous`; both yield unknown, never a veto or a +% confident compatible. Against the queried So we evaluate at Rel; against other +% NEEDED objects at their own evidence release. A hard veto (missing OR +% no_default_export) needs absence -- of the symbol, or of a default export -- +% ESTABLISHED at Rel for So (complete evidence at a release >= Rel). Complete +% evidence only BELOW Rel says nothing (a later release may add the symbol or a +% default export) -> unknown (Astra re-review 2). +unversioned_status(Bin, So, Sym, Bind, Rel, Hyp, Status) :- + ( ( unversioned_in(So, Sym, Rel, Hyp, Node, Basis) + -> Status = provided(Sym, default_node(So, Node, Basis)) + ; needed(Bin, S), S \== So, prov_usable(S, _, R0, _), + unversioned_in(S, Sym, R0, Hyp, Node, Basis) + -> Status = provided(Sym, default_node(S, Node, Basis)) + ; fail + ) + -> true + ; Bind == 'WEAK' + -> Status = weak_unresolved(Sym) % a weak ref never vetoes, so missing evidence is moot + ; unversioned_unproven(Bin, So, Sym, Rel, S1, N1) + -> Status = unknown(Sym, default_binding_unproven(S1, N1)) + ; unversioned_ambiguous(Bin, So, Sym, Rel, S2, N2) + -> Status = unknown(Sym, default_binding_conflict(S2, N2)) + ; needed(Bin, S), \+ prov_evidence(S, _, _, complete) + -> ( prov_usable(S, _, _, _) % a curated NEEDED object cannot prove + -> Status = unknown(Sym, absent_from_incomplete_evidence(S)) % absence -> unknown, never a veto (Sol re-review 2, P1) + ; Status = unknown(Sym, no_provider_evidence(S)) ) + ; unversioned_unknown(Bin, So, Sym, Rel, _, Why) + -> Status = unknown(Sym, Why) + ; \+ absence_established(So, Rel) % So's complete evidence is only BELOW Rel: a later release + -> Status = unknown(Sym, absence_unestablished(So, Rel)) % may add the symbol OR a default export (Astra re-review 2, gates BOTH vetoes) + ; unversioned_nondefault(Bin, So, Sym, Rel, S3, N3) + -> Status = missing(Sym, no_default_export(S3, N3)) + ; Status = missing(Sym) + ). + +% absence_established(S, Rel): S has complete evidence at a release >= Rel, so a +% symbol -- or a default export -- absent from it is absent at Rel too (monotone). +absence_established(S, Rel) :- + prov_evidence(S, _, R0, complete), + rel_le(Rel, R0). + +% Per-object classification of an unversioned Sym at the relevant release, using +% the binding ident_status credits (so binding and presence never diverge): +% unversioned_in -> present with a DEFAULT (bindable) export, not dropped +% unversioned_unproven -> present, binding only from a curated .symbols row +% unversioned_ambiguous -> present, but the credited rows disagree on the binding +% unversioned_nondefault -> present only at a non-default node +unversioned_in(S, Sym, Rel, Hyp, Node, Basis) :- + symprov(S, Sym, Node, _), + \+ hyp_dropped(Hyp, Sym, Node, Rel), + ident_status(S, Sym, Node, Rel, provided(Basis, default)). + +unversioned_unproven(Bin, So, Sym, Rel, S, Node) :- + needed_at(Bin, So, Rel, S, R), + symprov(S, Sym, Node, _), + ident_status(S, Sym, Node, R, provided(_, unproven)). + +unversioned_ambiguous(Bin, So, Sym, Rel, S, Node) :- + needed_at(Bin, So, Rel, S, R), + symprov(S, Sym, Node, _), + ident_status(S, Sym, Node, R, provided(_, ambiguous)). + +unversioned_unknown(Bin, So, Sym, Rel, S, Why) :- + needed_at(Bin, So, Rel, S, R), + node_binding(S, Sym, Node, B), B \== nondefault, + ident_status(S, Sym, Node, R, unknown(Why)). + +unversioned_nondefault(Bin, So, Sym, Rel, S, Node) :- + needed_at(Bin, So, Rel, S, R), + symprov(S, Sym, Node, _), + ident_status(S, Sym, Node, R, provided(_, nondefault)). + +bound_binding(since(_, _, _, B), B). +bound_binding(at(_, B), B). + +% needed_at(Bin, So, Rel, S, R): the queried So at Rel, other NEEDED objects +% at their own evidence release(s). +needed_at(_, So, Rel, So, Rel). +needed_at(Bin, So, _, S, R) :- needed(Bin, S), S \== So, prov_usable(S, _, R, _). + +% --------------------------------------------------------------------------- +% Verdict +% --------------------------------------------------------------------------- + +abi_verdict(Bin, So, RelAtom, Verdict) :- + abi_verdict(Bin, So, RelAtom, none, Verdict). + +abi_verdict(Bin, So, RelAtom, Hyp, Verdict) :- + rel_term(RelAtom, Rel), + ( \+ req_evidence(Bin, _, _, _) + -> Verdict = unknown([no_requires_evidence(Bin)]) + ; req_evidence(Bin, _, Status, Detail), Status \== complete + -> Verdict = unknown([requires_evidence(Status, Detail)]) + ; soname_offer(Bin, So, mismatch(N)) + -> Verdict = incompatible([soname_mismatch(offered(So), needed(N))]) + ; \+ needed(Bin, So) + -> Verdict = not_needed(So) + ; \+ prov_usable(So, _, _, _) + -> Verdict = unknown([no_provider_evidence(So)]) + ; findall(S, req_status(Bin, So, Rel, Hyp, S), Ss), + aggregate_statuses(Ss, Verdict) + ). + +% The verdict basis is the WEAKEST basis among the provided requirements: +% exact < curated < extrapolated. +aggregate_statuses(Ss, Verdict) :- + include(hard_veto, Ss, Hard), + include(is_unknown, Ss, Unk), + ( Hard \== [] + -> Verdict = incompatible(Hard) + ; Unk \== [] + -> Verdict = unknown(Unk) + ; has_basis(Ss, extrapolated) + -> Verdict = compatible(extrapolated) + ; has_basis(Ss, curated) + -> Verdict = compatible(curated) + ; Verdict = compatible(exact) + ). + +has_basis(Ss, Basis) :- + ( memberchk(provided(_, Basis), Ss) -> true + ; memberchk(provided(_, default_node(_, _, Basis)), Ss) + ). + +hard_veto(missing(_)). +hard_veto(missing(_, _)). +hard_veto(below_floor(_, _)). +is_unknown(unknown(_, _)). + +% soname_offer(Bin, So, Offer): needed | mismatch(NeededSoName) | not_needed. +% Offering libfoo.so.2 to a binary whose DT_NEEDED says libfoo.so.1 is a hard +% veto ONLY under a declared succession relation replaces(libfoo.so.2, +% libfoo.so.1) (the loader matches DT_NEEDED by exact soname string). Without +% that declaration a name that is not NEEDED is simply not_needed -- no stem +% heuristic (Sol P2d: libfoo.so.2 vs an unrelated NEEDED libfoo.so.1-extra). +soname_offer(Bin, So, Offer) :- + ( needed(Bin, So) + -> Offer = needed + ; replaces(So, N), needed(Bin, N) + -> Offer = mismatch(N) + ; Offer = not_needed + ). + +% --------------------------------------------------------------------------- +% Floor: the curated lower bound implied by `.symbols` (= dpkg-shlibdeps' dep) +% --------------------------------------------------------------------------- + +% abi_floor(Bin, So, FloorAtom): the highest `.symbols` minimum-version among +% the provider rows matched (exactly, by node) by Bin's requirements on So. +% Fails if any versioned requirement on So has no since() provider row +% (missing symbol, or readelf-only evidence). +abi_floor(Bin, So, Floor) :- + findall(Sym-Node, ( symreq(Bin, Sym, Node, So, _), Node \== none ), Reqs), + Reqs \== [], + maplist(req_floor(So), Reqs, Mins), + max_deb(Mins, _-Floor). + +req_floor(So, Sym-Node, Max) :- + findall(Deb-Atom, symprov(So, Sym, Node, since(Deb, Atom, _, _)), Ms), + Ms \== [], + max_deb(Ms, Max). + +max_deb([M|Ms], Max) :- foldl(max_deb_1, Ms, M, Max). +max_deb_1(D-A, D0-A0, Out) :- ( rel_lt(D0, D) -> Out = D-A ; Out = D0-A0 ). + +% --------------------------------------------------------------------------- +% Range over the actual release axis +% --------------------------------------------------------------------------- + +abi_range(Bin, So, Result) :- + release_axis(So, Rels), + abi_range(Bin, So, Rels, none, Result). + +% abi_range(Bin, So, Hyp, Result): store axis, hypothetical drop(Sym, Node, At). +abi_range(Bin, So, Hyp, Result) :- + release_axis(So, Rels), + abi_range(Bin, So, Rels, Hyp, Result). + +% abi_range(Bin, So, RelAtoms, Hyp, Result): +% range(Min, Max, Pairs) -- Min/Max are releases with compatible(_) verdicts +% no_candidate(Pairs) -- every release incompatible / not needed +% unknown(Pairs) -- no compatible release, some unknown +% no_releases -- empty axis +% Pairs = [RelAtom-Verdict ...] ascending. +abi_range(_Bin, _So, [], _Hyp, no_releases) :- !. +abi_range(Bin, So, RelAtoms, Hyp, Result) :- + maplist(rel_pair, RelAtoms, P0), + predsort(rel_cmp, P0, Sorted), + pairs_values(Sorted, Asc), + findall(A-V, ( member(A, Asc), abi_verdict(Bin, So, A, Hyp, V) ), Pairs), + range_min_max(Pairs, Pairs, Result). + +rel_pair(A, R-A) :- rel_term(A, R). + +range_min_max(Pairs, Detail, Result) :- + findall(A, member(A-compatible(_), Pairs), Compat), + ( Compat = [Min|_] + -> last(Compat, Max), + Result = range(Min, Max, Detail) + ; memberchk(_-unknown(_), Pairs) + -> Result = unknown(Detail) + ; Result = no_candidate(Detail) + ). diff --git a/examples/pkg_resolver/abi/crosscheck.mjs b/examples/pkg_resolver/abi/crosscheck.mjs new file mode 100644 index 000000000..b9a41ec8d --- /dev/null +++ b/examples/pkg_resolver/abi/crosscheck.mjs @@ -0,0 +1,80 @@ +#!/usr/bin/env node +// SPDX-License-Identifier: MIT OR Apache-2.0 +// Copyright (c) 2026 John William Creighton (@s243a) +// +// crosscheck.mjs -- compare the two provider tiers for one soname: +// readelf(lib.so) -> symprov rows ["so|sym@node", ["at", rel, binding]] +// .symbols file -> symprov rows ["so|sym@node", ["since", minver, rel, binding]] +// +// (1) EXACT IDENTITY: the sets of sym@node must be equal. This is the check +// the model actually relies on (a requirement matches a provider by the +// exact triple), and on Ubuntu 22.04 libc6 it is 3006/3006. +// (2) PER-NAME COMPARISON: for every symbol NAME the SET of nodes must agree +// on both sides. This is the corrected form of the legacy per-name figure +// (the original script compared the LAST curated row of a symbol against +// the EARLIEST ELF node, so every two-node symbol -- e.g. +// pthread_setname_np@GLIBC_2.12 + @GLIBC_2.34 -- "disagreed": 91.7%). +// Node names are opaque labels: nothing is parsed out of them and nothing +// is ordered (Sol P3 removed the local dotted-version comparator); the +// fixture fixtures/crosscheck/ keeps the regression pinned. +// Both figures must be 100% AND every denominator must be nonzero: two empty +// inputs (e.g. /dev/null vs /dev/null) FAIL instead of passing on NaN (Sol P2c). +// +// usage: crosscheck.mjs + +import { readFileSync } from "node:fs"; + +const [symFile, elfFile, so] = process.argv.slice(2); +if (!symFile || !elfFile || !so) { console.error("usage: crosscheck.mjs "); process.exit(2); } + +function loadRows(file, tag) { + const rows = []; // {sym, node} + for (const l of readFileSync(file, "utf8").split("\n")) { + if (!l) continue; + const [k, v] = JSON.parse(l); + if (!k.startsWith(so + "|") || v[0] !== tag) continue; + const ident = k.slice(so.length + 1); + const at = ident.lastIndexOf("@"); + rows.push({ sym: ident.slice(0, at), node: ident.slice(at + 1) }); + } + return rows; +} + +function fail(msg) { console.error(` FAIL: ${msg}`); process.exit(1); } + +const S = loadRows(symFile, "since"), E = loadRows(elfFile, "at"); +const sKeys = new Set(S.map((r) => `${r.sym}@${r.node}`)); +const eKeys = new Set(E.map((r) => `${r.sym}@${r.node}`)); +let both = 0; const onlyE = [], onlyS = []; +for (const k of eKeys) (sKeys.has(k) ? both++ : onlyE.push(k)); +for (const k of sKeys) if (!eKeys.has(k)) onlyS.push(k); +console.log(` exact sym@node identity: .symbols=${sKeys.size} readelf=${eKeys.size} shared=${both} only-readelf=${onlyE.length} only-.symbols=${onlyS.length}`); +if (onlyE.length) console.log(` only-readelf sample: ${onlyE.slice(0, 5).join(", ")}`); +if (onlyS.length) console.log(` only-.symbols sample: ${onlyS.slice(0, 5).join(", ")}`); +if (sKeys.size === 0 || eKeys.size === 0) fail(`empty symbol set for ${so} (.symbols=${sKeys.size} readelf=${eKeys.size}); nothing to compare`); +const denom = Math.max(sKeys.size, eKeys.size); +const identityPct = (100 * both) / denom; +console.log(` identity agreement: ${both}/${denom} (${identityPct.toFixed(1)}%)`); + +// Per-name node-set agreement (no ordering, no parsing of node names). +function nodeSets(rows) { + const m = new Map(); + for (const r of rows) { if (!m.has(r.sym)) m.set(r.sym, new Set()); m.get(r.sym).add(r.node); } + return m; +} +const sN = nodeSets(S), eN = nodeSets(E); +const names = new Set([...sN.keys(), ...eN.keys()]); +let agree = 0; const dis = []; +for (const sym of names) { + const a = sN.get(sym) || new Set(), b = eN.get(sym) || new Set(); + const same = a.size === b.size && [...a].every((n) => b.has(n)); + if (same) agree++; + else if (dis.length < 5) dis.push(`${sym} (.symbols={${[...a].join(",")}} readelf={${[...b].join(",")}})`); +} +if (names.size === 0) fail("no symbol names to compare"); +const pct = (100 * agree) / names.size; +console.log(` per-name node-set agreement: ${agree}/${names.size} (${pct.toFixed(1)}%)`); +if (dis.length) console.log(` disagreements: ${dis.join(", ")}`); +if (!(identityPct === 100)) fail("exact identity sets differ"); +if (!(pct === 100)) fail("per-name node sets differ"); +console.log(" PASS: readelf and .symbols agree on every exact sym@node identity"); diff --git a/examples/pkg_resolver/abi/fixtures/alpha.c b/examples/pkg_resolver/abi/fixtures/alpha.c new file mode 100644 index 000000000..1da6d417f --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/alpha.c @@ -0,0 +1,2 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +int alpha_fn(void) { return 1; } diff --git a/examples/pkg_resolver/abi/fixtures/batch/mixed.symbols b/examples/pkg_resolver/abi/fixtures/batch/mixed.symbols new file mode 100644 index 000000000..f35a5fa43 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/batch/mixed.symbols @@ -0,0 +1,7 @@ +# Batch-mode atomicity fixture (Sol P2a): the first block's package (libc6) is +# installed so its evidence release is known; the second block's is not +# (#PACKAGE#, no --release). The WHOLE file must be rejected: no good_fn row. +libbatchgood.so.1 libc6 #MINVER# + good_fn@Base 1.0 +libbatchbad.so.1 #PACKAGE# #MINVER# + bad_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/beta.c b/examples/pkg_resolver/abi/fixtures/beta.c new file mode 100644 index 000000000..cfc77ab98 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/beta.c @@ -0,0 +1,2 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +int beta_fn(void) { return 2; } diff --git a/examples/pkg_resolver/abi/fixtures/common.map b/examples/pkg_resolver/abi/fixtures/common.map new file mode 100644 index 000000000..5a5d2859b --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/common.map @@ -0,0 +1 @@ +COMMON_1 { global: alpha_fn; beta_fn; local: *; }; diff --git a/examples/pkg_resolver/abi/fixtures/contradictory.symbols b/examples/pkg_resolver/abi/fixtures/contradictory.symbols new file mode 100644 index 000000000..f80711b53 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/contradictory.symbols @@ -0,0 +1,6 @@ +# Contradictory-floor fixture (Sol re-review 2, P1): the minimum-version 2.0 is +# ABOVE the evidence release the file is ingested at (--release 1.0). A curated +# minimum cannot exceed the release it was curated from, so the WHOLE file is +# rejected (exit 3), nothing written. +libcontra.so.1 #PACKAGE# #MINVER# + contra_fn@Base 2.0 diff --git a/examples/pkg_resolver/abi/fixtures/crosscheck/elf.symprov.jsonl b/examples/pkg_resolver/abi/fixtures/crosscheck/elf.symprov.jsonl new file mode 100644 index 000000000..99d6f4278 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/crosscheck/elf.symprov.jsonl @@ -0,0 +1,7 @@ +["libx.so.1|pthread_setname_np@GLIBC_2.34",["at","2.35-1","default"]] +["libx.so.1|pthread_setname_np@GLIBC_2.12",["at","2.35-1","nondefault"]] +["libx.so.1|getenv@GLIBC_2.2.5",["at","2.35-1","default"]] +["libx.so.1|__libc_enable_secure@GLIBC_PRIVATE",["at","2.35-1","default"]] +["libx.so.1|plain_fn@Base",["at","2.35-1","default"]] +["libx.so.1|numnode@LIBX_2.1",["at","2.35-1","default"]] +["libx.so.1|numnode@LIBX_2.10",["at","2.35-1","nondefault"]] diff --git a/examples/pkg_resolver/abi/fixtures/crosscheck/elf_dropnode.symprov.jsonl b/examples/pkg_resolver/abi/fixtures/crosscheck/elf_dropnode.symprov.jsonl new file mode 100644 index 000000000..e33e5255c --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/crosscheck/elf_dropnode.symprov.jsonl @@ -0,0 +1,4 @@ +["libx.so.1|pthread_setname_np@GLIBC_2.34",["at","2.35-1","default"]] +["libx.so.1|getenv@GLIBC_2.2.5",["at","2.35-1","default"]] +["libx.so.1|__libc_enable_secure@GLIBC_PRIVATE",["at","2.35-1","default"]] +["libx.so.1|plain_fn@Base",["at","2.35-1","default"]] diff --git a/examples/pkg_resolver/abi/fixtures/crosscheck/elf_numcollapse.symprov.jsonl b/examples/pkg_resolver/abi/fixtures/crosscheck/elf_numcollapse.symprov.jsonl new file mode 100644 index 000000000..27c58878e --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/crosscheck/elf_numcollapse.symprov.jsonl @@ -0,0 +1,6 @@ +["libx.so.1|pthread_setname_np@GLIBC_2.34",["at","2.35-1","default"]] +["libx.so.1|pthread_setname_np@GLIBC_2.12",["at","2.35-1","nondefault"]] +["libx.so.1|getenv@GLIBC_2.2.5",["at","2.35-1","default"]] +["libx.so.1|__libc_enable_secure@GLIBC_PRIVATE",["at","2.35-1","default"]] +["libx.so.1|plain_fn@Base",["at","2.35-1","default"]] +["libx.so.1|numnode@LIBX_2.1",["at","2.35-1","default"]] diff --git a/examples/pkg_resolver/abi/fixtures/crosscheck/sym.symprov.jsonl b/examples/pkg_resolver/abi/fixtures/crosscheck/sym.symprov.jsonl new file mode 100644 index 000000000..6ca882770 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/crosscheck/sym.symprov.jsonl @@ -0,0 +1,8 @@ +["libx.so.1|pthread_setname_np@GLIBC_2.12",["since","2.12","2.35-1","unproven"]] +["libx.so.1|pthread_setname_np@GLIBC_2.34",["since","2.34","2.35-1","unproven"]] +["libx.so.1|getenv@GLIBC_2.2.5",["since","2.2.5","2.35-1","unproven"]] +["libx.so.1|__libc_enable_secure@GLIBC_PRIVATE",["since","0","2.35-1","unproven"]] +["libx.so.1|plain_fn@Base",["since","1.0","2.35-1","default"]] +["libx.so.1|numnode@LIBX_2.1",["since","2.1","2.35-1","unproven"]] +["libx.so.1|numnode@LIBX_2.10",["since","2.10","2.35-1","unproven"]] +["libother.so.9|not_this_soname@OTHER_1",["since","1.0","2.35-1","unproven"]] diff --git a/examples/pkg_resolver/abi/fixtures/foo.c b/examples/pkg_resolver/abi/fixtures/foo.c new file mode 100644 index 000000000..ce374cf29 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/foo.c @@ -0,0 +1,7 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* libfoo fixture: built twice under the SAME soname (libfoo.so.1) with two + * version scripts. v1 exports foo@LIB_1; v2 keeps the LIB_1 node (foo_legacy) + * but moves foo to LIB_2 only -- so a binary linked against v1 needs foo@LIB_1 + * and the loader rejects v2: "undefined symbol: foo, version LIB_1". */ +int foo(void) { return 1; } +int foo_legacy(void) { return 0; } diff --git a/examples/pkg_resolver/abi/fixtures/foo_v1.map b/examples/pkg_resolver/abi/fixtures/foo_v1.map new file mode 100644 index 000000000..4c55d00f6 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/foo_v1.map @@ -0,0 +1 @@ +LIB_1 { global: foo; foo_legacy; local: *; }; diff --git a/examples/pkg_resolver/abi/fixtures/foo_v2.map b/examples/pkg_resolver/abi/fixtures/foo_v2.map new file mode 100644 index 000000000..0c4f24e0d --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/foo_v2.map @@ -0,0 +1,2 @@ +LIB_1 { global: foo_legacy; local: *; }; +LIB_2 { global: foo; } LIB_1; diff --git a/examples/pkg_resolver/abi/fixtures/hid.c b/examples/pkg_resolver/abi/fixtures/hid.c new file mode 100644 index 000000000..2a9b17f8e --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/hid.c @@ -0,0 +1,13 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* libhid fixture (Sol P1b): hid_fn is exported ONLY at a NON-DEFAULT version + * node (`.symver` with a single `@` = hidden, readelf shows hid_fn@HID_1, not + * @@). Built twice under soname libhid.so.1: + * hid_idx3.map: HID_0 first (verdef index 2), HID_1 second (index 3) -- the + * loader refuses an unversioned reference: "undefined symbol: hid_fn" + * hid_idx2.map: HID_1 is the only node (verdef index 2) -- the loader binds a + * legacy unversioned reference to the oldest node even though it + * is hidden (glibc dl-lookup: index < 3 is accepted before the + * hidden test). Ingest records index 2 as "default" for that reason. */ +int other_fn(void) { return 9; } +int hid_fn_impl(void) { return 5; } +__asm__(".symver hid_fn_impl, hid_fn@HID_1"); diff --git a/examples/pkg_resolver/abi/fixtures/hid_idx2.map b/examples/pkg_resolver/abi/fixtures/hid_idx2.map new file mode 100644 index 000000000..fcb12d734 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/hid_idx2.map @@ -0,0 +1 @@ +HID_1 { global: hid_fn; other_fn; local: *; }; diff --git a/examples/pkg_resolver/abi/fixtures/hid_idx3.map b/examples/pkg_resolver/abi/fixtures/hid_idx3.map new file mode 100644 index 000000000..58f4e65a5 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/hid_idx3.map @@ -0,0 +1,2 @@ +HID_0 { global: other_fn; local: *; }; +HID_1 { global: hid_fn; } HID_0; diff --git a/examples/pkg_resolver/abi/fixtures/hid_plain.c b/examples/pkg_resolver/abi/fixtures/hid_plain.c new file mode 100644 index 000000000..9cb851ad0 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/hid_plain.c @@ -0,0 +1,5 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Unversioned build of libhid.so.1 (hid_fn@Base): usehid is linked against + * this one, so its reference to hid_fn is UNVERSIONED. */ +int other_fn(void) { return 9; } +int hid_fn(void) { return 5; } diff --git a/examples/pkg_resolver/abi/fixtures/plain.c b/examples/pkg_resolver/abi/fixtures/plain.c new file mode 100644 index 000000000..4beb0795d --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/plain.c @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Built WITHOUT a version script: an unversioned export (dpkg spells it @Base). */ +int plain_fn(void) { return 4; } diff --git a/examples/pkg_resolver/abi/fixtures/pub.c b/examples/pkg_resolver/abi/fixtures/pub.c new file mode 100644 index 000000000..19b7f83a5 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/pub.c @@ -0,0 +1,2 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +int pub_fn(void) { return 3; } diff --git a/examples/pkg_resolver/abi/fixtures/pub.map b/examples/pkg_resolver/abi/fixtures/pub.map new file mode 100644 index 000000000..e53c6468a --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/pub.map @@ -0,0 +1 @@ +PUBLIC { global: pub_fn; local: *; }; diff --git a/examples/pkg_resolver/abi/fixtures/simple.symbols b/examples/pkg_resolver/abi/fixtures/simple.symbols new file mode 100644 index 000000000..234e9f6cf --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/simple.symbols @@ -0,0 +1,11 @@ +# A binary-form .symbols with the simple cases: two sonames, an alt-dep line, +# a meta field, comments, a private (minimum 0) row, tilde and epoch minimums. +libsimple.so.1 libsimple1 #MINVER# +| libsimple1 (>> 1.2), libsimple1 (<< 1.3) +* Build-Depends-Package: libsimple-dev + SIMPLE_1.0@SIMPLE_1.0 1.0 + simple_new@SIMPLE_1.2 1.2~rc1 + simple_old@SIMPLE_1.0 1:0.9-2 + _private_thing@SIMPLE_PRIVATE 0 1 +libsimple-extra.so.0 libsimple1 #MINVER# + extra_fn@Base 1.1 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_arch.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_arch.symbols new file mode 100644 index 000000000..791ca6ed9 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_arch.symbols @@ -0,0 +1,5 @@ +libtmpl.so.1 #PACKAGE# #MINVER# + (arch=amd64)only_amd64@Base 1.0 + (arch=!amd64)not_amd64@Base 1.0 + (arch-bits=64)bits64@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_arch_list.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_arch_list.symbols new file mode 100644 index 000000000..b1c475c24 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_arch_list.symbols @@ -0,0 +1,5 @@ +# Architecture-list fixture (Astra re-review 2): (arch=amd64,arm64) uses a +# comma-list our whitespace parser does not handle; rejected, not mis-selected. +liblist.so.1 #PACKAGE# #MINVER# + (arch=amd64,arm64)list_fn@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_arch_tuple.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_arch_tuple.symbols new file mode 100644 index 000000000..1e2cc0e1a --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_arch_tuple.symbols @@ -0,0 +1,5 @@ +# Architecture-tuple fixture (Astra re-review 2): (arch=gnu-any-amd64) is a dpkg +# GNU tuple wildcard we do not match; the row is rejected, not mis-selected. +libtuple.so.1 #PACKAGE# #MINVER# + (arch=gnu-any-amd64)tuple_fn@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_arch_wild.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_arch_wild.symbols new file mode 100644 index 000000000..073e09af4 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_arch_wild.symbols @@ -0,0 +1,6 @@ +# Architecture-wildcard fixture (Astra P2): (arch=linux-any) needs +# dpkg-architecture matching semantics we do not reimplement, so the row is +# rejected rather than mis-selected. The whole file is refused (exit 3). +libwild.so.1 #PACKAGE# #MINVER# + (arch=linux-any)wild_fn@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_cxx.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_cxx.symbols new file mode 100644 index 000000000..62efeb085 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_cxx.symbols @@ -0,0 +1,3 @@ +libtmpl.so.1 #PACKAGE# #MINVER# + (c++)"Foo::bar(int)@Base" 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_optional.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_optional.symbols new file mode 100644 index 000000000..07bc62fd0 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_optional.symbols @@ -0,0 +1,3 @@ +libtmpl.so.1 #PACKAGE# #MINVER# + (optional)maybe_fn@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_symver.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_symver.symbols new file mode 100644 index 000000000..773b054d7 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_symver.symbols @@ -0,0 +1,3 @@ +libtmpl.so.1 #PACKAGE# #MINVER# + (symver)LIB_1 1.0 + plain_fn@LIB_1 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/tmpl_unknown_tag.symbols b/examples/pkg_resolver/abi/fixtures/tmpl_unknown_tag.symbols new file mode 100644 index 000000000..45c503b67 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/tmpl_unknown_tag.symbols @@ -0,0 +1,3 @@ +libtmpl.so.1 #PACKAGE# #MINVER# + (frobnicate)mystery_fn@Base 1.0 + plain_fn@Base 1.0 diff --git a/examples/pkg_resolver/abi/fixtures/usecommon.c b/examples/pkg_resolver/abi/fixtures/usecommon.c new file mode 100644 index 000000000..df82a9ae4 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/usecommon.c @@ -0,0 +1,7 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Needs alpha_fn@COMMON_1 from libalpha.so.1 AND beta_fn@COMMON_1 from + * libbeta.so.1: the same version-node NAME in two verneed files. Attribution + * must go through the per-symbol version INDEX, not the node name. */ +int alpha_fn(void); +int beta_fn(void); +int main(void) { return alpha_fn() + beta_fn() == 3 ? 0 : 1; } diff --git a/examples/pkg_resolver/abi/fixtures/usefoo.c b/examples/pkg_resolver/abi/fixtures/usefoo.c new file mode 100644 index 000000000..9a47301c6 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/usefoo.c @@ -0,0 +1,4 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Linked against libfoo v1: requires foo@LIB_1 from libfoo.so.1. */ +int foo(void); +int main(void) { return foo() == 1 ? 0 : 1; } diff --git a/examples/pkg_resolver/abi/fixtures/usehid.c b/examples/pkg_resolver/abi/fixtures/usehid.c new file mode 100644 index 000000000..bce8b199c --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/usehid.c @@ -0,0 +1,4 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Unversioned reference to hid_fn from libhid.so.1. */ +int hid_fn(void); +int main(void) { return hid_fn() == 5 ? 0 : 1; } diff --git a/examples/pkg_resolver/abi/fixtures/usepub.c b/examples/pkg_resolver/abi/fixtures/usepub.c new file mode 100644 index 000000000..10a6f5e79 --- /dev/null +++ b/examples/pkg_resolver/abi/fixtures/usepub.c @@ -0,0 +1,6 @@ +/* SPDX-License-Identifier: MIT OR Apache-2.0 */ +/* Needs pub_fn@PUBLIC (a non-numeric node) and plain_fn (unversioned). Both + * are real loader obligations and must survive ingestion. */ +int pub_fn(void); +int plain_fn(void); +int main(void) { return pub_fn() + plain_fn() == 7 ? 0 : 1; } diff --git a/examples/pkg_resolver/abi/ingest_symbols.mjs b/examples/pkg_resolver/abi/ingest_symbols.mjs new file mode 100644 index 000000000..9d7b01b61 --- /dev/null +++ b/examples/pkg_resolver/abi/ingest_symbols.mjs @@ -0,0 +1,687 @@ +#!/usr/bin/env node +// SPDX-License-Identifier: MIT OR Apache-2.0 +// Copyright (c) 2026 John William Creighton (@s243a) +// +// ingest_symbols.mjs -- ingest symbol-level ABI evidence into the store as P/2 +// JSONL rows (`[key, value]`, the load_p2_jsonl shape). +// +// DESIGN (post-review redesign; see REVIEW_NOTES.md): +// +// * Identity is the exact (soname, symbol, version-node) triple. A version +// node (`GLIBC_2.34`, `LIBSELINUX_1.0`, `COMMON_1`, `PUBLIC`, `Base`) is an +// opaque ELF label matched by string equality -- never parsed into a number, +// never collapsed to the bare symbol name. `Base` is dpkg's spelling of "no +// version" (an unversioned export); ELF unversioned exports are recorded +// under that same spelling so the two provider tiers agree. +// * The Debian PACKAGE-version axis (the `.symbols` minimum-version field, +// the release candidates) is a separate axis, carried verbatim as the deb +// version string and parsed/ordered on the Prolog side by the frozen +// resolver's deb/3 machinery (debian/deb_parse.pl + resolver:version_lt/2). +// * Every obligation is preserved: versioned requirements with non-numeric +// nodes, unversioned requirements, weak references (flagged, not dropped). +// * Requirements are attributed to their soname through the per-symbol +// version INDEX (.gnu.version -> .gnu.version_r), not through the version +// NAME, so two libraries sharing a node name (COMMON_1) never collide. +// * Evidence completeness is explicit: every successful ingest emits an +// `evidence` row; a missing / unreadable ELF is a loud failure (exit 3) +// that -- when --out is given -- records a failure evidence row instead +// of an empty "success". A `.symbols` file is ingested atomically: one +// unsupported row, one unknown tag, one block whose evidence release is +// unknown, or a bad --release rejects the WHOLE file (also in batch +// mode), nothing partial is written, and the run exits 3 (Sol P2). +// * Default-version binding is retained (Sol P1b): every provider row says +// whether an UNVERSIONED reference binds to it. From readelf that is the +// `.gnu.version` hidden bit (`@` = hidden = "nondefault", `@@` = +// "default"); the loader additionally binds legacy unversioned references +// to the OLDEST version node (verdef index 2) even when hidden, so index 2 +// is recorded as "default" too (verified with the loader, fixture D10c). +// A `.symbols` file carries no `@@` information: its rows are "unproven" +// unless cross-checked against the ELF with --elf, and the resolver then +// answers unknown -- never compatible -- for an unversioned reference. +// `Base` (unversioned export) always binds. +// +// Store rows (all JSON arrays `[key, value]`): +// symprov.jsonl ["|@", ["since", "", "", ]] (.symbols) +// ["|@", ["at", "", ]] (readelf) +// = "default" | "nondefault" | "unproven" +// symreq.jsonl ["|@", ["", "GLOBAL"|"WEAK"]] +// ["|", ["", "GLOBAL"|"WEAK"]] (unversioned) +// needed.jsonl ["", ""] +// evidence.jsonl ["provides|", ["symbols"|"elf", "", "complete"|"curated", ""]] +// ("elf" and --elf-cross-checked "symbols" are "complete" (absence is a fact); +// a plain "symbols" ingest is "curated" (a lower bound; absence proves nothing)) +// ["requires|", ["readelf", "complete"|"missing_file"|"readelf_failed"|"inconsistent", ""]] +// releases.jsonl ["", ""] (candidate axis) +// replaces.jsonl ["", ""] (declared soname succession) +// +// Usage: +// node ingest_symbols.mjs symbols-file [--release V] [--arch A] [--elf lib.so] [--out DIR] [--append] [--stdout] +// node ingest_symbols.mjs symbols-dir [--release V] [--arch A] --out DIR +// node ingest_symbols.mjs elf [--release V] [--out DIR] [--append] [--stdout] +// node ingest_symbols.mjs requires [--out DIR] [--append] [--stdout] +// node ingest_symbols.mjs releases ... [--out DIR] [--append] [--stdout] +// node ingest_symbols.mjs replaces ... [--out DIR] [--append] [--stdout] +// +// Exit codes: 0 ok; 2 usage; 3 evidence failure (missing file, readelf failure, +// unsupported/unknown .symbols template construct, unknown or invalid evidence +// release, (optional) row without ELF cross-check, ELF/.symbols disagreement). + +import { execFileSync } from "node:child_process"; +import { readFileSync, existsSync, appendFileSync, writeFileSync, mkdirSync, readdirSync } from "node:fs"; +import { join } from "node:path"; + +const EXIT_EVIDENCE = 3; + +function die(msg, code = EXIT_EVIDENCE) { + process.stderr.write(`ingest_symbols: ${msg}\n`); + process.exit(code); +} + +function pair(k, v) { + return JSON.stringify([k, v]); +} + +function run(cmd, args) { + return execFileSync(cmd, args, { encoding: "utf8", maxBuffer: 1 << 26, stdio: ["ignore", "pipe", "ignore"] }); +} + +// readelf: returns null (never "") on failure so callers cannot mistake a +// failed read for an empty section. +function readelf(args, file) { + if (!existsSync(file)) return null; + try { return run("readelf", [...args, file]); } catch { return null; } +} + +// --------------------------------------------------------------------------- +// Debian package-version helpers (ingestion edge only; ordering is Prolog's). +// --------------------------------------------------------------------------- +// The evidence release of a provider = the package version the evidence was +// taken from. For an installed .symbols file that is the installed package +// version (dpkg-query); for an ELF file it is the owning package's version +// (dpkg -S). Callers may override with --release. +function dpkgVersion(pkg) { + try { return run("dpkg-query", ["-W", "-f", "${Version}", pkg]).trim() || null; } catch { return null; } +} + +function dpkgOwner(path) { + try { + const out = run("dpkg", ["-S", path]).trim(); + const m = out.match(/^([^:\s]+(?::[^:\s]+)?):\s/); + return m ? m[1] : null; + } catch { return null; } +} + +// A syntactically valid Debian version: [epoch:]upstream[-revision] (Policy +// 5.6.12), validated the way `dpkg --validate-version` does -- a loose regex +// (the old DEB_VERSION_RE) accepted "1:", "1-" and "1::2", which dpkg rejects +// (Sol re-review 2, P2). Ordering is still Prolog's; this only validates syntax. +// * epoch (optional): digits before the FIRST colon, must be all digits +// * upstream: must start with a digit; alnum . + ~ - and ':' (':' only when +// an epoch is present); '-' only as the last-hyphen revision delimiter +// * revision (optional, after the LAST '-'): alnum . + ~ , no '-' or ':', +// and must be non-empty when a '-' is present +function validDebVersion(v) { + if (typeof v !== "string" || v.length === 0 || /\s/.test(v)) return false; + let rest = v, hasEpoch = false; + const colon = v.indexOf(":"); + if (colon >= 0) { + const ep = v.slice(0, colon); + // epoch must be all digits and within dpkg's int range (Astra: 2147483648:1 + // is rejected by dpkg --validate-version) + if (!/^\d+$/.test(ep) || Number(ep) > 2147483647) return false; + rest = v.slice(colon + 1); + hasEpoch = true; + } + let upstream = rest, revision = null; + const hy = rest.lastIndexOf("-"); + if (hy >= 0) { upstream = rest.slice(0, hy); revision = rest.slice(hy + 1); } + if (upstream.length === 0 || !/^[0-9]/.test(upstream)) return false; + const upstreamOk = hasEpoch ? /^[0-9A-Za-z.+~:-]+$/ : /^[0-9A-Za-z.+~-]+$/; + if (!upstreamOk.test(upstream)) return false; + if (revision !== null && !/^[0-9A-Za-z.+~]+$/.test(revision)) return false; // empty or bad revision + return true; +} + +// a <= b on the Debian version axis (dpkg is the reference implementation the +// Prolog resolver:version_lt/2 mirrors). Cached: a .symbols block has one +// evidence release and few distinct minimum versions. Used only to reject a +// curated minimum ABOVE its evidence release (Sol re-review 2, P1). +const _cmpCache = new Map(); +function debLe(a, b) { + const key = `${a}\u0000${b}`; + if (_cmpCache.has(key)) return _cmpCache.get(key); + let r; + try { execFileSync("dpkg", ["--compare-versions", a, "le", b], { stdio: "ignore" }); r = true; } + catch (e) { + if (e && e.code === "ENOENT") die(`dpkg not found on PATH; it is required to compare Debian versions (${a} vs ${b})`); + r = false; // exit 1 = a > b (both a and b are already syntactically valid here) + } + _cmpCache.set(key, r); + return r; +} + +// --------------------------------------------------------------------------- +// Tier: parse a Debian/Ubuntu `.symbols` file (binary control member form). +// --------------------------------------------------------------------------- +// Binary form (dpkg-gensymbols output, /var/lib/dpkg/info/*.symbols): +// #MINVER# header (no leading whitespace) +// | libc6 (>> 2.35), libc6 (<< 2.36) alternative dependency template +// * Build-Depends-Package: libc6-dev meta field +// @ [] symbol row (indented) +// +// SOURCE-TEMPLATE syntax (debian/*.symbols in source packages) differs and is +// only partially supportable without the binary at hand. Tags are WHITELISTED: +// the ones below are processed, EVERY other tag rejects the file (Sol P2). +// (optional) dpkg lets an optional symbol stay in the template +// after it disappeared from the binary, so the row is +// NOT an export fact by itself (Sol P1c). It is kept only +// when --elf is given and the ELF exports that exact +// sym@node; an optional row absent from the ELF is +// dropped (reported on stderr); without --elf the file +// is rejected. +// (arch=..)/(arch-bits=..)/(arch-endian=..) +// processed when --arch is given (row kept iff it +// selects the arch; arch-bits/endian derived from it); +// rejected otherwise +// (ignore-blacklist) processed (ignored; does not affect identity) +// (symver), (regex), (c++...), any unknown tag +// rejected: symver/regex/c++ need the binary to expand; +// an unknown tag has unknown semantics +// #include "file" rejected (template include) +// #PACKAGE# accepted in the header; the package name is then +// unknown so --release becomes mandatory +// Minimum-version semantics: a curated LOWER BOUND on the package version a +// dependent needs (Debian policy lets maintainers raise it after a compatible +// behaviour change), NOT a ground-truth introduction date. Stored verbatim. + +// Architecture bit-width and endianness, tabulated for the arches we are +// CONFIDENT about; an --arch not listed makes an (arch-bits=..)/(arch-endian=..) +// row REJECT the file rather than guess wrong (Astra re-review 2: the old +// positive-set-with-default guessed kfreebsd-amd64 as 32-bit and mips64 as +// little-endian). Values verified against dpkg-architecture. +const ARCH_BITS = { + amd64: 64, "kfreebsd-amd64": 64, i386: 32, "kfreebsd-i386": 32, x32: 32, + arm64: 64, armhf: 32, armel: 32, riscv64: 64, loong64: 64, ia64: 64, + ppc64: 64, ppc64el: 64, powerpc: 32, s390x: 64, alpha: 64, sparc64: 64, sparc: 32, + mips: 32, mipsel: 32, mips64: 64, mips64el: 64, m68k: 32, hppa: 32, sh4: 32, +}; +const ARCH_ENDIAN = { + amd64: "little", "kfreebsd-amd64": "little", i386: "little", "kfreebsd-i386": "little", x32: "little", + arm64: "little", armhf: "little", armel: "little", riscv64: "little", loong64: "little", ia64: "little", + ppc64el: "little", mipsel: "little", mips64el: "little", sh4: "little", alpha: "little", + ppc64: "big", powerpc: "big", s390x: "big", sparc64: "big", sparc: "big", + mips: "big", mips64: "big", m68k: "big", hppa: "big", +}; + +// Only EXACT Debian architecture names (optionally `!`-negated) are supported. +// dpkg wildcard/tuple patterns (any, linux-any, any-arm, gnu-any-amd64, ...) and +// comma-lists need dpkg-architecture's matching semantics, which we do NOT +// reimplement (the old ad-hoc matcher disagreed with dpkg), so a row using one is +// REJECTED by the caller. EVERY term is validated FIRST, so an early match or +// negation cannot skip a later unsupported term (Astra re-review 2). Returns +// true/false, or null for "unsupported selector". +function archSelects(spec, arch) { + const terms = spec.trim().split(/\s+/); + const cleanName = /^[a-z][a-z0-9]*(-[a-z0-9]+)?$/; // amd64, armhf, kfreebsd-amd64 + for (let t of terms) { + if (t.startsWith("!")) t = t.slice(1); + if (t.includes("any") || !cleanName.test(t)) return null; // wildcard / tuple / list / malformed + } + let selected = null; + for (let t of terms) { + let neg = false; + if (t.startsWith("!")) { neg = true; t = t.slice(1); } + const hit = (t === arch); + if (neg) { if (hit) return false; if (selected === null) selected = true; } + else if (hit) selected = true; + else if (selected === null) selected = false; + } + return selected === null ? true : selected; +} + +function parseTags(line) { + // Leading `(tag|tag=value|...)` group(s). Returns {tags: Map, rest}. + const tags = new Map(); + let rest = line; + while (rest[0] === "(") { + const close = rest.indexOf(")"); + if (close < 0) break; + for (const t of rest.slice(1, close).split("|")) { + const eq = t.indexOf("="); + if (eq < 0) tags.set(t.trim(), true); + else tags.set(t.slice(0, eq).trim(), t.slice(eq + 1).trim()); + } + rest = rest.slice(close + 1); + } + return { tags, rest }; +} + +// Whitelist (Sol P2): every tag not listed here rejects the file. +const SUPPORTED_TAGS = new Set(["optional", "arch", "arch-bits", "arch-endian", "ignore-blacklist"]); + +function parseSymbolsFile(path, { arch = null } = {}) { + if (!existsSync(path)) die(`symbols file not found: ${path}`); + const text = readFileSync(path, "utf8"); + const blocks = []; // {soname, package, rows: [{sym, node, minver, optional}]} + const errors = []; // unsupported template constructs (line numbers) + let cur = null; + let lineNo = 0; + for (const raw of text.split("\n")) { + lineNo++; + if (!raw.trim()) continue; + if (!/^[ \t]/.test(raw)) { + const c = raw[0]; + if (c === "|" || c === "*") continue; // alt-dep template / meta field + if (c === "#") { + if (/^#include\b/.test(raw)) errors.push(`${lineNo}: template #include`); + continue; // comment + } + const [soname, pkg] = raw.trim().split(/\s+/); + if (!soname) { errors.push(`${lineNo}: malformed header`); continue; } + cur = { soname, package: pkg && pkg !== "#PACKAGE#" ? pkg : null, rows: [] }; + blocks.push(cur); + continue; + } + if (!cur) { errors.push(`${lineNo}: symbol row before any soname header`); continue; } + let line = raw.trim(); + if (line[0] === "|" || line[0] === "*" || line[0] === "#") continue; + const { tags, rest } = parseTags(line); + line = rest.trimStart(); + // Whitelist: reject every tag whose semantics we do not implement. + const unknown = [...tags.keys()].filter((t) => !SUPPORTED_TAGS.has(t)); + if (unknown.length) { errors.push(`${lineNo}: unsupported template tag (${unknown.join("|")}): ${raw.trim()}`); continue; } + if (line[0] === '"') { errors.push(`${lineNo}: quoted (pattern) symbol needs the binary to expand: ${raw.trim()}`); continue; } + // Architecture selectors. + let archOk = true; + for (const key of ["arch", "arch-bits", "arch-endian"]) { + if (!tags.has(key)) continue; + if (!arch) { errors.push(`${lineNo}: (${key}=...) selector but no --arch given: ${raw.trim()}`); archOk = null; break; } + const v = String(tags.get(key)); + if (key === "arch") { + const sel = archSelects(v, arch); + if (sel === null) { errors.push(`${lineNo}: unsupported architecture wildcard in (arch=${v}); only exact names (optionally !negated) are supported: ${raw.trim()}`); archOk = null; break; } + archOk = archOk && sel; + } + else if (key === "arch-bits") { + const bits = ARCH_BITS[arch]; + if (bits === undefined) { errors.push(`${lineNo}: (arch-bits=..) but architecture ${arch} is not tabulated; refusing to guess: ${raw.trim()}`); archOk = null; break; } + archOk = archOk && (v === String(bits)); + } + else { // arch-endian + const end = ARCH_ENDIAN[arch]; + if (end === undefined) { errors.push(`${lineNo}: (arch-endian=..) but architecture ${arch} is not tabulated; refusing to guess: ${raw.trim()}`); archOk = null; break; } + archOk = archOk && (v === end); + } + } + if (archOk === null) continue; + if (!archOk) continue; // row does not apply to this arch + // "@ []" -- split at the LAST '@' (symbol + // names never contain '@'; node names never do either). + const parts = line.split(/\s+/); + const ident = parts[0], minver = parts[1]; + const at = ident.lastIndexOf("@"); + if (at <= 0 || minver === undefined) { errors.push(`${lineNo}: malformed symbol row: ${raw.trim()}`); continue; } + const sym = ident.slice(0, at), node = ident.slice(at + 1); + if (!node) { errors.push(`${lineNo}: empty version node: ${raw.trim()}`); continue; } + if (!validDebVersion(minver)) { errors.push(`${lineNo}: minimum-version is not a Debian version: ${raw.trim()}`); continue; } + cur.rows.push({ sym, node, minver, optional: tags.has("optional"), lineNo }); + } + return { blocks, errors }; +} + +// --------------------------------------------------------------------------- +// readelf: version-index-aware symbol tables (Tiers 2 & 3). +// --------------------------------------------------------------------------- +// readelf -W --dyn-syms rows: " 7: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34 (5)" +// readelf -W -V: +// Version symbols section '.gnu.version' ... +// 000: 0 (*local*) 2 (GLIBC_2.3) 3 (GLIBC_2.2.5) 5h (GLIBC_2.34) <- versym per .dynsym index; 'h' = hidden +// Version definition section '.gnu.version_d' ... +// 0x0000: Rev: 1 Flags: base Index: 1 Cnt: 1 Name: libc.so.6 +// 0x001c: Rev: 1 Flags: none Index: 2 Cnt: 1 Name: GLIBC_2.2.5 +// Version needs section '.gnu.version_r' ... +// 0x0000: Version: 1 File: libc.so.6 Cnt: 9 +// 0x0010: Name: GLIBC_2.28 Flags: none Version: 11 +function elfTables(file) { + const symOut = readelf(["-W", "--dyn-syms"], file); + const verOut = readelf(["-W", "-V"], file); + const dynOut = readelf(["-W", "-d"], file); + if (symOut === null || verOut === null || dynOut === null) return null; + + const syms = []; // {idx, bind, ndx, name, verName (from name@VER), defaultFromName (@@)} + for (const raw of symOut.split("\n")) { + const m = raw.match(/^\s*(\d+):\s+\S+\s+\S+\s+(\S+)\s+(\S+)\s+(\S+)\s+(\S+)\s+(\S+)?(?:\s+\((\d+)\))?\s*$/); + if (!m) continue; + const [, idx, , bind, , ndx, name0] = m; + if (!name0) continue; + let name = name0, verName = null, defaultFromName = null; + const dd = name0.indexOf("@@"), d = name0.indexOf("@"); + if (dd >= 0) { name = name0.slice(0, dd); verName = name0.slice(dd + 2); defaultFromName = true; } + else if (d > 0) { name = name0.slice(0, d); verName = name0.slice(d + 1); defaultFromName = false; } + syms.push({ idx: +idx, bind, ndx, name, verName, defaultFromName }); + } + + // .gnu.version: index -> {ver, hidden} + const versym = new Map(); + const verdef = new Map(); // verIdx -> name (definitions; Index 1 = base/unversioned) + const verneed = new Map(); // verIdx -> {file, name, weak} + let section = null, curFile = null; + for (const raw of verOut.split("\n")) { + if (/^Version symbols section/.test(raw)) { section = "sym"; continue; } + if (/^Version definition section/.test(raw)) { section = "def"; continue; } + if (/^Version needs section/.test(raw)) { section = "need"; continue; } + if (section === "sym") { + const m = raw.match(/^\s*([0-9a-f]+):\s+(.*)$/); + if (!m) continue; + const base = parseInt(m[1], 16); + const re = /([0-9a-f]+)(h?)\s*\(([^)]*)\)/g; // "23 (GLIBC_2.34)" or hidden "10h(GLIBC_2.12)" + let e, i = 0; + while ((e = re.exec(m[2]))) { versym.set(base + i, { ver: parseInt(e[1], 16), hidden: e[2] === "h" }); i++; } + } else if (section === "def") { + const m = raw.match(/Index:\s+(\d+)\s+Cnt:\s+\d+\s+Name:\s+(\S+)/); + if (m) verdef.set(+m[1], m[2]); + } else if (section === "need") { + let m; + if ((m = raw.match(/Version:\s+\d+\s+File:\s+(\S+)\s+Cnt:/))) { curFile = m[1]; continue; } + if ((m = raw.match(/Name:\s+(\S+)\s+Flags:\s+([^\s]+(?:\s+[^\s]+)*?)\s+Version:\s+(\d+)/)) && curFile) { + verneed.set(+m[3], { file: curFile, name: m[1], weak: /WEAK/.test(m[2]) }); + } + } + } + + let soname = null; + const needed = []; + for (const raw of dynOut.split("\n")) { + let m; + if ((m = raw.match(/\(SONAME\)\s+Library soname: \[([^\]]+)\]/))) soname = m[1]; + else if ((m = raw.match(/\(NEEDED\)\s+Shared library: \[([^\]]+)\]/))) needed.push(m[1]); + } + return { syms, versym, verdef, verneed, soname, needed, hasVersioning: versym.size > 0 }; +} + +// Provides: defined dynamic symbols with their exact version node and their +// default-version binding (Sol P1b): +// binding = "default" an unversioned reference binds to it: the `@@` +// default (versym hidden bit clear), or the oldest +// version node (verdef index 2), which the loader +// accepts for legacy unversioned references even +// when hidden (glibc dl-lookup: index < 3 is taken +// before the hidden test; fixture D10c proves it) +// = "nondefault" hidden (`@`) at verdef index >= 3: an unversioned +// reference does NOT bind to it (fixture D10) +// `Base` is always "default". +function elfProvides(t) { + const rows = []; // {sym, node, binding} + const problems = []; + for (const s of t.syms) { + if (s.ndx === "UND" || s.ndx === "Ndx") continue; + // GLOBAL, WEAK, and STB_GNU_UNIQUE (readelf: "UNIQUE") are all exported and + // resolved by the loader; LOCAL is not. Dropping UNIQUE (e.g. ~100 in + // libstdc++.so.6) would let a real requirement produce a false missing veto. + if (s.bind !== "GLOBAL" && s.bind !== "WEAK" && s.bind !== "UNIQUE") continue; + let node, binding = "default"; + if (!t.hasVersioning) node = "Base"; + else { + const v = t.versym.get(s.idx); + if (!v) { problems.push(`no versym entry for dynsym ${s.idx} (${s.name})`); continue; } + if (v.ver === 0) continue; // *local* + if (v.ver === 1) node = "Base"; // *global* = unversioned + else { + node = t.verdef.get(v.ver); + if (!node) { problems.push(`dynsym ${s.idx} (${s.name}) versym ${v.ver} has no verdef entry`); continue; } + if (s.verName && s.verName !== node) problems.push(`dynsym ${s.idx}: name says @${s.verName} but verdef index says ${node}`); + if (s.defaultFromName !== null && s.defaultFromName === v.hidden) + problems.push(`dynsym ${s.idx} (${s.name}@${node}): name says ${s.defaultFromName ? "@@ default" : "@ hidden"} but versym hidden bit says ${v.hidden ? "hidden" : "default"}`); + binding = (!v.hidden || v.ver === 2) ? "default" : "nondefault"; + } + } + rows.push({ sym: s.name, node, binding }); + } + return { rows, problems }; +} + +// Exact export map of an ELF: "sym@node" -> binding. Used to cross-check a +// `.symbols` file against the binary it describes (Sol P1c). +function elfExportMap(path, what) { + const t = elfTables(path); + if (!t) die(`${what}: --elf ${path}: cannot read (missing file or readelf failure)`); + const { rows, problems } = elfProvides(t); + if (problems.length) die(`${what}: --elf ${path}: inconsistent version tables:\n ${problems.slice(0, 10).join("\n ")}`); + const map = new Map(); + for (const { sym, node, binding } of rows) { + const k = `${sym}@${node}`; + if (!map.has(k) || binding === "default") map.set(k, binding); + } + return { soname: t.soname || path, map }; +} + +// Requires: undefined dynamic symbols, each attributed to (file, node) via its +// version INDEX. Never keyed by node name. +function elfRequires(t) { + const rows = []; // {sym, node|null, soname|"", bind} + const problems = []; + for (const s of t.syms) { + if (s.ndx !== "UND" || !s.name) continue; + if (s.bind !== "GLOBAL" && s.bind !== "WEAK") continue; + let bind = s.bind; + if (!t.hasVersioning) { rows.push({ sym: s.name, node: null, soname: "", bind }); continue; } + const v = t.versym.get(s.idx); + if (!v) { problems.push(`no versym entry for dynsym ${s.idx} (${s.name})`); continue; } + if (v.ver <= 1) { rows.push({ sym: s.name, node: null, soname: "", bind }); continue; } // unversioned reference + const need = t.verneed.get(v.ver); + if (!need) { problems.push(`dynsym ${s.idx} (${s.name}) versym ${v.ver} has no verneed entry`); continue; } + if (s.verName && s.verName !== need.name) problems.push(`dynsym ${s.idx}: name says @${s.verName} but verneed index ${v.ver} says ${need.name}`); + if (!t.needed.includes(need.file)) problems.push(`verneed file ${need.file} (for ${s.name}@${need.name}) is not in DT_NEEDED`); + if (need.weak) bind = "WEAK"; + rows.push({ sym: s.name, node: need.name, soname: need.file, bind }); + } + return { rows, problems }; +} + +// --------------------------------------------------------------------------- +// Output sink. +// --------------------------------------------------------------------------- +const STORES = ["symprov", "symreq", "needed", "evidence", "releases", "replaces"]; + +function makeSink(outDir, toStdout) { + const buffers = Object.fromEntries(STORES.map((s) => [s, []])); + return { + add(store, k, v) { buffers[store].push(pair(k, v)); }, + flush(append) { + if (outDir) mkdirSync(outDir, { recursive: true }); + for (const store of STORES) { + const lines = buffers[store]; + if (!lines.length) continue; + if (outDir) { + const f = join(outDir, store + ".jsonl"); + const body = lines.join("\n") + "\n"; + if (append) appendFileSync(f, body); else writeFileSync(f, body); + } + if (toStdout) for (const l of lines) process.stdout.write(l + "\n"); + } + }, + }; +} + +function parseArgs(rest) { + const opts = { out: null, stdout: false, append: false, release: null, arch: null, elf: null, positional: [] }; + for (let i = 0; i < rest.length; i++) { + const a = rest[i]; + if (a === "--out") opts.out = rest[++i]; + else if (a === "--stdout") opts.stdout = true; + else if (a === "--append") opts.append = true; + else if (a === "--release") opts.release = rest[++i]; + else if (a === "--arch") opts.arch = rest[++i]; + else if (a === "--elf") opts.elf = rest[++i]; + else opts.positional.push(a); + } + if (!opts.out && !opts.stdout) opts.stdout = true; + return opts; +} + +// One Debian-version gate for every evidence release, whichever command +// supplied it (Sol P2): --release, dpkg-query, or the `releases` axis. +function validRelease(rel, what) { + if (!rel) die(`${what}: evidence release unknown (not owned by an installed package); pass --release `); + if (!validDebVersion(rel)) die(`${what}: release '${rel}' is not a Debian version`); + return rel; +} + +function requireRelease(opts, guess, what) { + return validRelease(opts.release || guess, what); +} + +// --------------------------------------------------------------------------- +// Commands. +// --------------------------------------------------------------------------- +// A `.symbols` file is ingested ATOMICALLY: any error in any block returns +// null (nothing is added to the sink), in single-file and batch mode alike. +function cmdSymbolsFile(opts, path, sink, elf = null) { + const { blocks, errors } = parseSymbolsFile(path, { arch: opts.arch }); + if (!blocks.length && !errors.length) errors.push("no soname blocks"); + const rows = []; // deferred until the whole file is clean + const sonames = []; + let dropped = 0; + for (const b of blocks) { + const guess = b.package ? dpkgVersion(b.package) : null; + const rel = opts.release || guess; + if (!rel) { errors.push(`${b.soname}: evidence release unknown (package ${b.package || "#PACKAGE#"} not installed); pass --release`); continue; } + if (!validDebVersion(rel)) { errors.push(`${b.soname}: release '${rel}' is not a Debian version`); continue; } + const xcheck = elf && elf.soname === b.soname ? elf.map : null; + const seen = new Set(); + for (const { sym, node, minver, optional, lineNo } of b.rows) { + const k = `${sym}@${node}`; + // A curated minimum cannot exceed the release the file was curated from + // (Sol re-review 2, P1): such a row is contradictory. Reject the file. + if (!debLe(minver, rel)) { errors.push(`${lineNo}: minimum-version ${minver} is above the evidence release ${rel} (contradictory): ${k}`); continue; } + if (xcheck) { + const binding = xcheck.get(k); + if (binding === undefined) { + if (optional) { dropped++; process.stderr.write(`ingest_symbols: ${path}:${lineNo}: (optional) ${k} not exported by ${opts.elf}; row dropped\n`); continue; } + errors.push(`${lineNo}: ${k} is in the .symbols file but not exported by --elf ${opts.elf}`); + continue; + } + seen.add(k); + rows.push([`${b.soname}|${k}`, ["since", minver, rel, binding]]); + } else { + if (optional) { errors.push(`${lineNo}: (optional) ${k} needs an ELF cross-check (--elf ) to count as an export`); continue; } + rows.push([`${b.soname}|${k}`, ["since", minver, rel, node === "Base" ? "default" : "unproven"]]); + } + } + if (xcheck) for (const k of xcheck.keys()) if (!seen.has(k)) errors.push(`${b.soname}: ${k} is exported by --elf ${opts.elf} but absent from the .symbols file (evidence would not be complete)`); + // A plain .symbols file is CURATED (a lower-bound list); only an --elf + // cross-check observes the export set completely (Sol re-review 2, P1). + // Curated presence is evidence; curated absence proves nothing. + rows.push([`provides|${b.soname}`, ["symbols", rel, xcheck ? "complete" : "curated", path], "evidence"]); + sonames.push(b.soname); + } + if (errors.length) { + process.stderr.write(`ingest_symbols: ${path}: ${errors.length} problem(s) -- rejecting the whole file, nothing written:\n`); + for (const e of errors.slice(0, 20)) process.stderr.write(` ${e}\n`); + if (errors.length > 20) process.stderr.write(` ... ${errors.length - 20} more\n`); + return null; + } + let n = 0; + for (const [k, v, store] of rows) { sink.add(store || "symprov", k, v); if (!store) n++; } + return { n, sonames, dropped }; +} + +const [cmd, ...rest] = process.argv.slice(2); +const opts = parseArgs(rest); +if (opts.release !== null) validRelease(opts.release, cmd); + +if (cmd === "symbols-file") { + const path = opts.positional[0]; + if (!path) die("symbols-file: missing path", 2); + const elf = opts.elf ? elfExportMap(opts.elf, `symbols-file ${path}`) : null; + const sink = makeSink(opts.out, opts.stdout); + const r = cmdSymbolsFile(opts, path, sink, elf); + if (!r) process.exit(EXIT_EVIDENCE); + sink.flush(opts.append); + process.stderr.write(`symbols-file ${path}: symprov=${r.n} sonames=${r.sonames.length} [${r.sonames.slice(0, 6).join(", ")}${r.sonames.length > 6 ? ", ..." : ""}]${elf ? ` cross-checked=${elf.soname} optional-dropped=${r.dropped}` : ""}\n`); +} else if (cmd === "symbols-dir") { + const dir = opts.positional[0]; + if (!dir || !opts.out) die("symbols-dir: needs and --out DIR", 2); + if (opts.elf) die("symbols-dir: --elf applies to a single file; use symbols-file", 2); + const files = readdirSync(dir).filter((f) => f.endsWith(".symbols")).map((f) => join(dir, f)); + mkdirSync(opts.out, { recursive: true }); + for (const s of ["symprov", "evidence"]) writeFileSync(join(opts.out, s + ".jsonl"), ""); + let total = 0, ok = 0, rejected = 0; + for (const f of files) { + const sink = makeSink(opts.out, false); + const r = cmdSymbolsFile(opts, f, sink); + if (!r) { rejected++; continue; } // atomic: no block of a rejected file is written + sink.flush(true); + total += r.n; ok++; + } + process.stderr.write(`symbols-dir ${dir}: files=${ok} rejected=${rejected} symprov=${total}\n`); + if (rejected) process.exit(EXIT_EVIDENCE); +} else if (cmd === "elf") { + const path = opts.positional[0]; + if (!path) die("elf: missing path", 2); + const t = elfTables(path); + if (!t) die(`elf: cannot read ${path} (missing file or readelf failure); no evidence emitted`); + const so = t.soname || path; + const owner = dpkgOwner(path); + const rel = requireRelease(opts, owner ? dpkgVersion(owner) : null, `elf ${path}`); + const { rows, problems } = elfProvides(t); + if (problems.length) die(`elf ${path}: inconsistent version tables:\n ${problems.slice(0, 10).join("\n ")}`); + const sink = makeSink(opts.out, opts.stdout); + const seen = new Map(); // one identity per sym@node; "default" wins if both appear + for (const { sym, node, binding } of rows) { + const k = `${so}|${sym}@${node}`; + if (!seen.has(k) || binding === "default") seen.set(k, binding); + } + let nd = 0; + for (const [k, binding] of seen) { sink.add("symprov", k, ["at", rel, binding]); if (binding === "nondefault") nd++; } + sink.add("evidence", `provides|${so}`, ["elf", rel, "complete", path]); + sink.flush(opts.append); + process.stderr.write(`elf ${path}: soname=${so} release=${rel} symprov=${seen.size} (nondefault=${nd})\n`); +} else if (cmd === "requires") { + const path = opts.positional[0]; + if (!path) die("requires: missing path", 2); + const t = elfTables(path); + const sink = makeSink(opts.out, opts.stdout); + if (!t) { + const status = existsSync(path) ? "readelf_failed" : "missing_file"; + sink.add("evidence", `requires|${path}`, ["readelf", status, path]); + sink.flush(opts.append); + die(`requires ${path}: ${status}; recorded INCOMPLETE evidence, no requirement rows`); + } + const { rows, problems } = elfRequires(t); + if (problems.length) { + sink.add("evidence", `requires|${path}`, ["readelf", "inconsistent", problems[0]]); + sink.flush(opts.append); + die(`requires ${path}: inconsistent version tables:\n ${problems.slice(0, 10).join("\n ")}`); + } + let nv = 0, nu = 0; + for (const { sym, node, soname, bind } of rows) { + if (node === null) { sink.add("symreq", `${path}|${sym}`, ["", bind]); nu++; } + else { sink.add("symreq", `${path}|${sym}@${node}`, [soname, bind]); nv++; } + } + for (const so of t.needed) sink.add("needed", path, so); + sink.add("evidence", `requires|${path}`, ["readelf", "complete", path]); + sink.flush(opts.append); + process.stderr.write(`requires ${path}: symreq=${nv} versioned + ${nu} unversioned; needed=[${t.needed.join(", ")}]\n`); +} else if (cmd === "releases") { + const [so, ...vers] = opts.positional; + if (!so || !vers.length) die("releases: needs ...", 2); + for (const v of vers) validRelease(v, `releases ${so}`); + const sink = makeSink(opts.out, opts.stdout); + for (const v of vers) sink.add("releases", so, v); + sink.flush(opts.append); + process.stderr.write(`releases ${so}: ${vers.length} candidate(s)\n`); +} else if (cmd === "replaces") { + // Declared soname succession (Sol P2d): offering to a binary whose + // DT_NEEDED names is a soname_mismatch only under this relation; any + // other name that is not NEEDED is simply not_needed (no stem heuristic). + const [so, ...olds] = opts.positional; + if (!so || !olds.length) die("replaces: needs ...", 2); + const sink = makeSink(opts.out, opts.stdout); + for (const o of olds) sink.add("replaces", so, o); + sink.flush(opts.append); + process.stderr.write(`replaces ${so}: ${olds.join(", ")}\n`); +} else { + process.stderr.write("usage: ingest_symbols.mjs symbols-file|symbols-dir|elf|requires|releases|replaces [--release V] [--arch A] [--elf lib.so] [--out DIR] [--append] [--stdout]\n"); + process.exit(2); +} diff --git a/examples/pkg_resolver/abi/run_abi_verify.sh b/examples/pkg_resolver/abi/run_abi_verify.sh new file mode 100755 index 000000000..ed73f4e69 --- /dev/null +++ b/examples/pkg_resolver/abi/run_abi_verify.sh @@ -0,0 +1,272 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MIT OR Apache-2.0 +# Copyright (c) 2026 John William Creighton (@s243a) +# +# run_abi_verify.sh -- build the symbol-level ABI store from THIS machine's +# real Ubuntu/Debian data plus the review fixtures, then verify. +# +# 1. Real data: libc6 + libselinux1 `.symbols` -> symprov (since bounds; +# libc6 cross-checked against libc.so.6 with --elf so default-version +# binding is proven); /bin/ls -> symreq (attributed via the ELF version +# index) + NEEDED; the release axis from `apt-cache madison` + dpkg (real +# candidates); a declared soname succession (libc.so.7 replaces libc.so.6). +# 2. Cross-check: readelf(libc.so.6) vs `.symbols` on EXACT sym@node +# identity (must be 100%) and per-name node sets (must be 100%); the +# empty-input and dropped-node negatives must FAIL (Sol P2c/P3). +# 3. ELF fixtures (gcc): foo@LIB_1 vs foo@LIB_2 under one soname (with the +# loader as ground truth), COMMON_1 cross-attribution, PUBLIC + +# unversioned obligations, a missing ELF, non-default-only exports (Sol +# P1b, loader as ground truth), `.symbols` template accept/reject cases +# including (optional) with and without an ELF cross-check (Sol P1c), +# unknown tags, bad --release, and batch-mode atomicity (Sol P2). +# 4. test_abi.pl: the Prolog assertions over all of the above. +# +# Everything lands in ./.out (gitignored). Requires: node, readelf, swipl; +# gcc for the ELF fixtures (ABI_ALLOW_SKIP=1 tolerates a missing gcc). +set -euo pipefail + +HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +OUT="$HERE/.out" +STORE="$OUT/store" +FX="$OUT/fx" +SRC="$HERE/fixtures" +INGEST="$HERE/ingest_symbols.mjs" +BINARY="${ABI_BINARY:-/bin/ls}" +LIBSO="${ABI_LIBSO:-/lib/x86_64-linux-gnu/libc.so.6}" +ARCH="$(dpkg --print-architecture 2>/dev/null || echo amd64)" + +fail() { echo "FAIL: $*" >&2; exit 1; } + +# expect_reject