From 61b4f956dcafa0fbd993d8172e33256153cf178b Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 09:50:38 -0500 Subject: [PATCH 01/15] rfc: 0025 expand CBMC coverage The CBMC harnesses in test/cbmc cover six small functions, and their CI workflow was never enabled. This plans the next targets, ranked by what a wrong answer costs: - the replication election decisions (winner selection, tally, majority intersection) and the repmgr ack-policy durability decision; - btree prefix decompression, which reads a varint before checking it has the bytes; - queue record arithmetic across wrap-around; - the log header check and the region allocator's size classes. Each harness runs the real code, has a sabotage build that must fail, and a verbatim copy carries a drift check against src/. --- rfc/0025-cbmc-coverage.md | 75 +++++++++++++++++++++++++++++++++++++++ rfc/INDEX.md | 1 + 2 files changed, 76 insertions(+) create mode 100644 rfc/0025-cbmc-coverage.md diff --git a/rfc/0025-cbmc-coverage.md b/rfc/0025-cbmc-coverage.md new file mode 100644 index 0000000000..db8a81bb68 --- /dev/null +++ b/rfc/0025-cbmc-coverage.md @@ -0,0 +1,75 @@ +# RFC 0025: Expand CBMC coverage + +Status: Draft · Owner: lead · Scope: `test/cbmc/`, its CI workflow, and engine fixes for whatever the harnesses find + +## 1. Where we are + +`test/cbmc` has six harnesses over small, self-contained functions: varint, +byte swapping, `__ham_func4`, `__db_getlong`, the deadlock detector's +`__dd_find`, and `__db_ret_okitem`. The okitem harness found a real +out-of-bounds read (`HPAGE_PTYPE` was not parenthesised), and the fix landed in +`2ca81268a`. Two problems: + +- **The CI workflow was never enabled.** It sits in `test/cbmc` as + `cbmc.yml.workflow` and has never run. +- **`run.sh` still expects the fixed bug.** Its `okitem(REAL)` arm passes only + if the real code *fails*. Its harness carries a private, unparenthesised copy + of the macro, so it keeps "reproducing" a bug that master no longer has. + +## 2. What CBMC is good for here + +CBMC proves properties of one C function over **every** input up to a bound: +no out-of-bounds access, no invalid pointer, no overflow, and any assertion we +write. It fits code that is: + +- **pure or nearly pure**: its result depends on its arguments and a few + fields, not on I/O, locks or a shared region; +- **bounded**: loops have a size we can state (a page of ≤ 64 bytes, ≤ 5 sites); +- **safety-relevant**: a wrong answer loses data, elects two masters, or reads + past a buffer on hostile input. + +Network protocols (who receives which message when) are libcmc's job, not +CBMC's (see `docs/WHY.md` in libcmc). CBMC checks the **decision each node +makes**, given its inputs. libcmc checks the **protocol** those decisions form. + +## 3. Candidates, ranked + +| # | Target | Property to prove | Why it matters | Bound | +|---|---|---|---|---| +| **H1** | `__rep_cmp_vote` (rep_elect.c) | **Election winner selection.** It is a strict total order on votes, so the result does not depend on vote arrival order; a site with priority 0 that is not electable never wins; a non-zero priority beats a zero one; ties fall to data_gen, then LSN, then priority, then tiebreaker | Two sites tallying the same votes in different orders must choose the same winner, or the group can elect two masters | 3–4 votes, all field values | +| **H2** | `__rep_tally` (rep_elect.c) | Each site is counted once per election; a vote from an older egen never replaces a newer one; the count never exceeds the number of distinct voters, and stays inside the tally array | A double-counted vote wins an election without a majority | tally of 5, all sequences of 6 votes | +| **H3** | election quorum: `ELECTION_MAJORITY` and the `nvotes`/`nsites` checks in `__rep_elect_int` | Any two majorities of the same `nsites` intersect; the sub-majority warning fires exactly when `ack <= nsites/2` | The safety argument for one master per generation rests on majority intersection | nsites 1–64 | +| **H4** | ack-policy decision: `got_acks` and the `needed`/`quorum` computation in `__repmgr_send` (repmgr_net.c) | **Durability under QUORUM.** If a commit is reported durable, every possible election majority of electable sites contains a site that has the commit. Also: the "skip waiting" shortcut never reports durable when `got_acks` would not | This is the property the fault-injection suite's S5 tests from outside. CBMC proves it for every group shape, including the 2-site special case and the GMDB-update paths | ≤ 5 sites, all ack/peer/membership combinations | +| **B1** | `__bam_defdecompress` (bt_compress.c) | Never reads past `compressed->size` and never writes past `destKey->ulen`/`destData->ulen`, for **any** input bytes | The decoder reads each varint before checking it has the bytes, so a truncated compressed item can over-read by up to 8 bytes. A compressed btree's pages are a trust boundary (`db_verify`, a corrupted file) | compressed ≤ 16 bytes | +| **B2** | `__bam_defcompress` + `__bam_defdecompress` | Round trip: decompress(compress(k, d)) == (k, d), given the same previous key/data | A compression bug silently corrupts every key | keys ≤ 6 bytes | +| **Q1** | queue record arithmetic: `QAM_RECNO_PAGE`, `QAM_RECNO_INDEX`, `QAM_OUTSIDE_QUEUE`, `QAM_BEFORE_FIRST`, `QAM_AFTER_CURRENT` (qam.h) | Every record number in the queue maps to a valid (page, index); the index is < records per page; the wrap-around predicates agree with a simple reference over the whole 32-bit range, including when the queue wraps | Queue wrap-around has had bugs before; these macros are arithmetic over `u_int32_t` with wrap | all `u_int32_t`, loop-free | +| **L1** | `__logc_hdrchk` (log_get.c) | A header that passes is internally consistent (`len > size`, `len <= bp_maxrec` when set) | Recovery trusts what this accepts | loop-free | +| **E1** | `__env_alloc_size` and `SET_QUEUE_FOR_SIZE` (env_alloc.c) | The size-class index stays in range for every length; the rounded size covers the request without overflow | A bad size class corrupts the region allocator for every process | all `size_t` | + +Not chosen: SHA-1, HMAC and AES (well-tested reference code, and CBMC cost is +high), and the hash and btree page splitters (too stateful for CBMC; the +fuzzer and DST cover them). + +## 4. Method + +- **Run the real code.** Pull the function in with `#include` of its `.c` + where possible. Where it is `static` or drags in the whole tree, copy it + **verbatim** and add a `diff` check in `run.sh` that fails when the copy + drifts from `src/`. The okitem harness drifted silently; that check would + have caught it. +- **Every harness has teeth.** Each one has a `-D` sabotage build that plants + a real bug shape (swap two comparisons, drop a bound check, an off-by-one in + the majority) and must FAIL. `run.sh` checks both directions. +- **State the bound** in the harness's header and in the README table. A + bounded proof is not a claim about unbounded inputs. +- **CI:** enable the workflow, and make it required once it is green and + stable. The suite's runtime budget is under 5 minutes. + +## 5. Phases + +| Phase | Work | Gate | +|---|---|---| +| C0 | Enable the CI workflow. Fix `okitem(REAL)`: drop the stale private macro, test the real header, and make the arm a sabotage arm. Add the verbatim-copy drift check | CI green, and the drift check fails on a planted change | +| C1 | H1–H4, the election and ack-policy decisions | Each verifies, with a sabotage arm that fails | +| C2 | B1, B2, Q1 | Same. A real counterexample becomes a bug fix on its own branch with a failing-first test, and a backport if LTS has it | +| C3 | L1, E1 | Same | diff --git a/rfc/INDEX.md b/rfc/INDEX.md index dc0e0e534a..4494612d59 100644 --- a/rfc/INDEX.md +++ b/rfc/INDEX.md @@ -23,6 +23,7 @@ process. Status: Draft · Accepted · Rejected · Superseded · Implemented. | [0016](0016-rust-zig-bindings.md) | Rust and Zig language bindings: idiomatic, zero-copy-capable API shims over the C library, with native-format docs and tests | Draft | | [0023](0023-ssi-multilevel-conflict-detection.md) | SSI cross-leaf write-skew miss — **Withdrawn**: diagnosed as a plain bug and fixed directly (no design/format change); kept as a postmortem | Withdrawn | | [0024](0024-runtime-fault-injection.md) | Runtime fault injection as a DST layer: netns + tc netem, libfiu, libdirectio, libumem and FAINT on one Linux host, for single-node, HA and XA scenarios with ack-log oracles | Draft | +| [0025](0025-cbmc-coverage.md) | Expand CBMC coverage: election winner selection, vote tally, majority intersection, ack-policy durability, btree prefix decompression, queue record arithmetic, log header and region-allocator size checks | Draft | From f03dc3f286974cc8bb1eca6b77323b2057558f71 Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 09:56:20 -0500 Subject: [PATCH 02/15] test/cbmc: enable the CBMC workflow, check copies against src/ (RFC 0025 C0) The harnesses never ran in CI: the workflow was staged as test/cbmc/cbmc.yml.workflow and never copied into .github/workflows. It is now .github/workflows/cbmc.yml, and runs on every PR and master push. It has no paths filter, since a filter listing files skips changes to files nobody remembered to add. The okitem harness had drifted from the engine. It carried a private, unparenthesised copy of HPAGE_PTYPE, and run.sh's okitem(REAL) arm expected verification to FAIL, so it kept "reproducing" the bug for weeks after 2ca81268a fixed the real macro. The harness now uses the real macro and verifies. -DHPAGE_PTYPE_SABOTAGE restores the old macro as a sabotage arm, and that build must fail. check_copies.sh guards the other side of the same problem. A harness that copies a static function proves a property of the copy, so every "BEGIN verbatim copy of from " block must still match , comparing code tokens and ignoring comments. A one-token change to the __dd_find copy makes it fail. run.sh runs it. --- .github/workflows/cbmc.yml | 45 +++++++++++++++++++++++ test/cbmc/README.md | 27 +++++++------- test/cbmc/cbmc.yml.workflow | 72 ------------------------------------- test/cbmc/check_copies.sh | 57 +++++++++++++++++++++++++++++ test/cbmc/harness_okitem.c | 29 ++++++--------- test/cbmc/run.sh | 59 ++++++++++++++++++------------ 6 files changed, 163 insertions(+), 126 deletions(-) create mode 100644 .github/workflows/cbmc.yml delete mode 100644 test/cbmc/cbmc.yml.workflow create mode 100755 test/cbmc/check_copies.sh diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml new file mode 100644 index 0000000000..3ac34821e5 --- /dev/null +++ b/.github/workflows/cbmc.yml @@ -0,0 +1,45 @@ +# CBMC formal-verification harnesses (test/cbmc, RFC 0025). +# +# Each harness proves memory-safety and functional properties of a libdb +# function over ALL inputs within a stated bound (see test/cbmc/README.md). +# run.sh also runs each harness's sabotage arm, which must FAIL, and checks +# that every verbatim copy in a harness still matches src/. +# +# Runs on every PR and push, not on a paths filter: a harness covers code +# wherever it lives in src/, and a filter that lists files silently skips a +# change to a file someone forgot to add. The whole suite takes under a +# minute after the nix shell is warm. +name: CBMC + +on: + push: + branches: [master] + pull_request: + workflow_dispatch: + +concurrency: + group: cbmc-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + cbmc: + name: cbmc harnesses + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v4 + + - name: Install nix + uses: cachix/install-nix-action@v27 + with: + extra_nix_config: | + experimental-features = nix-command flakes + + - name: cbmc --version + run: nix develop . --command bash -c 'cbmc --version' + + - name: Run CBMC harness suite + run: nix develop . --command bash test/cbmc/run.sh diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 4b35154204..b50538d282 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -55,11 +55,17 @@ isolate one assertion). | `harness_hash4.c` | `hash/hash_func.c` `__ham_func4` (the `__db_chksum` plain-hash core) | reads exactly `len` key bytes (no OOB); deterministic; `len==0 ⇒ 0` | key ≤ 8 bytes, `--unwind 9` | ~15 s | SUCCESSFUL | | `harness_getlong.c` | `common/db_getlong.c` `__db_getlong` / `__db_getulong` | success ⇒ result in `[min,max]`; ulong `max==0` = "no upper bound"; no OOB on the parse | string ≤ 6 chars, `--unwind 8` | ~1 s | SUCCESSFUL | | `harness_dd_find.c` | `lock/lock_deadlock.c` `__dd_find` (waits-for bitmap cycle detection) | no OOB on the `nlockers×nalloc` bitmap matrix or deadlist; termination; deadlist entries point into the matrix and are NULL-terminated | 4 lockers, `--unwind 6` + `--unwinding-assertions` | <1 s | SUCCESSFUL | -| `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | **FAILS on real code → BUG FOUND (below)**; SUCCESSFUL with `-DHPAGE_PTYPE_FIXED` | +| `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | SUCCESSFUL. Found a real bug (below), fixed in `2ca81268a`; `-DHPAGE_PTYPE_SABOTAGE` restores the bug and must FAIL | -`run.sh` runs `okitem` twice: `-DHPAGE_PTYPE_FIXED` (the one-line fix → -`VERIFICATION SUCCESSFUL`, proving both the guarantee and the fix) and the -unmodified engine macro (→ `VERIFICATION FAILED`, reproducing the bug). +`run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION +SUCCESSFUL`) and with `-DHPAGE_PTYPE_SABOTAGE`, which restores the pre-fix +macro (→ `VERIFICATION FAILED`, the sabotage arm). + +`run.sh` also runs `check_copies.sh`: a harness that copies a `static` +function proves a property of the copy, so the copy must still match `src/`. +It compares code tokens (comments and blank lines are ignored) from the +function's `name(` line to its closing `}`. The okitem harness drifted this way +once, keeping the unparenthesised macro for weeks after the engine fix. ## Proof that the harnesses have teeth @@ -77,7 +83,7 @@ counterexample: (the bug below); the `-DHPAGE_PTYPE_FIXED` build then verifies, so the property distinguishes correct from incorrect code. -## BUG FOUND — `__db_ret_okitem` hash-offpage guard reads the wrong byte +## BUG FOUND (fixed in `2ca81268a`) — `__db_ret_okitem` hash-offpage guard read the wrong byte `harness_okitem.c` on the **unmodified** engine code produces a counterexample (`VERIFICATION FAILED`). Investigation showed it is a **real @@ -85,7 +91,7 @@ latent OOB read**, of the exact class bug #67 set out to close. ### Root cause -`HPAGE_PTYPE` (src/dbinc/db_page.h:583) has no parentheses around its +`HPAGE_PTYPE` (src/dbinc/db_page.h:583) had no parentheses around its argument: ```c @@ -135,7 +141,7 @@ Confirmed by native `gcc` execution as well as CBMC (not a CBMC artifact): `HPAGE_PTYPE((u_int8_t *)h + off)` returns `page[0] + off`, and okitem returns 0 for an item whose on-page extent runs 6 bytes past the page. -### Suggested fix (engine — NOT applied here; harnesses are additive) +### The fix (applied in `2ca81268a`) One line, in `src/dbinc/db_page.h`: @@ -144,11 +150,8 @@ One line, in `src/dbinc/db_page.h`: +#define HPAGE_PTYPE(p) (*(u_int8_t *)(p)) ``` -Building the harness with `-DHPAGE_PTYPE_FIXED` applies exactly this and the -proof then reports `VERIFICATION SUCCESSFUL` for all okitem safety -properties, validating the fix. (Equivalently, the two call sites could hoist -`(u_int8_t *)h + off` into a local, but fixing the macro closes the whole -class.) +The harness now verifies on the real macro. `-DHPAGE_PTYPE_SABOTAGE` puts the +old macro back, and that build must fail. ## Notes on the `okitem` harness bounds & flags diff --git a/test/cbmc/cbmc.yml.workflow b/test/cbmc/cbmc.yml.workflow deleted file mode 100644 index b72f2ac192..0000000000 --- a/test/cbmc/cbmc.yml.workflow +++ /dev/null @@ -1,72 +0,0 @@ -# CBMC formal-verification harnesses (advisory). -# -# Runs test/cbmc/run.sh in the flake dev shell (which provides CBMC 6.9.0). -# Each harness proves memory-safety + functional properties of a self-contained -# libdb algorithmic core over ALL inputs within a bound (see test/cbmc/README.md). -# -# ADVISORY: this workflow does not gate merges. It is expected to report the -# known __db_ret_okitem OOB bug (see README "BUG FOUND") until the one-line -# engine fix lands; run.sh treats that as an expected reproduction, not a suite -# failure, so a green run means "all verifying harnesses verified AND the known -# bug still reproduces". If run.sh goes red, either a verifying harness -# regressed or the okitem bug's status changed -- investigate. -# -# This file is owned by the CBMC effort. It does NOT touch ci.yml or any other -# effort's workflow. It is staged as *.yml.workflow because pushing files under -# .github/workflows/ needs an OAuth token with the `workflow` scope; a -# maintainer enables it with: -# cp test/cbmc/cbmc.yml.workflow .github/workflows/cbmc.yml - -name: CBMC - -on: - push: - branches: [master] - paths: - - 'test/cbmc/**' - - 'src/common/db_compint.c' - - 'src/common/db_getlong.c' - - 'src/hash/hash_func.c' - - 'src/db/db_ret.c' - - 'src/lock/lock_deadlock.c' - - 'src/dbinc/db_swap.h' - - 'src/dbinc/db_page.h' - - 'flake.nix' - pull_request: - paths: - - 'test/cbmc/**' - - 'src/common/db_compint.c' - - 'src/common/db_getlong.c' - - 'src/hash/hash_func.c' - - 'src/db/db_ret.c' - - 'src/lock/lock_deadlock.c' - - 'src/dbinc/db_swap.h' - - 'src/dbinc/db_page.h' - - 'flake.nix' - workflow_dispatch: - -concurrency: - group: cbmc-${{ github.ref }} - cancel-in-progress: true - -permissions: - contents: read - -jobs: - cbmc: - name: cbmc harnesses (advisory) - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - - name: Install nix - uses: cachix/install-nix-action@v27 - with: - extra_nix_config: | - experimental-features = nix-command flakes - - - name: cbmc --version - run: nix develop . --command bash -c 'cbmc --version' - - - name: Run CBMC harness suite - run: nix develop . --command bash test/cbmc/run.sh diff --git a/test/cbmc/check_copies.sh b/test/cbmc/check_copies.sh new file mode 100755 index 0000000000..bc9e26988c --- /dev/null +++ b/test/cbmc/check_copies.sh @@ -0,0 +1,57 @@ +#!/bin/sh +# +# test/cbmc/check_copies.sh -- every verbatim copy in a harness must still +# match the function in src/. +# +# A harness that copies a static function (rather than #include-ing its .c) +# proves a property of the COPY. If src/ changes and the copy does not, the +# harness keeps passing about code that no longer ships. That happened: the +# okitem harness kept a private copy of the unparenthesised HPAGE_PTYPE macro +# and "reproduced" a bug for weeks after 2ca81268a fixed it. +# +# Each copy is marked in its harness: +# /* --- BEGIN verbatim copy of from --- */ +# ... +# /* --- END verbatim copy --- */ +# The function in src/ runs from the line "(" to the next line that is +# exactly "}". The copy is compared from its own "(" line, and the +# line before that ("static int" etc.) is ignored, since the copy may add +# "static". Comments, blank lines and whitespace differences are ignored; +# every code token is compared. +# +# Exit 0 if every copy matches, 1 otherwise. +set -u +cd "$(dirname "$0")" +root=../.. +rc=0 +n=0 +for h in harness_*.c; do + grep -n 'BEGIN verbatim copy of ' "$h" | while IFS=: read -r ln rest; do + func=$(echo "$rest" | sed -n 's/.*verbatim copy of \([A-Za-z_0-9]*\) from \([^ ]*\) .*/\1/p') + src=$(echo "$rest" | sed -n 's/.*verbatim copy of [A-Za-z_0-9]* from \([^ ]*\) .*/\1/p') + [ -n "$func" ] && [ -n "$src" ] || { echo "MALFORMED marker: $h:$ln"; echo x >> .copies.bad; continue; } + [ -f "$root/$src" ] || { echo "MISSING source: $h names $src"; echo x >> .copies.bad; continue; } + awk -v f="$func" 'index($0, f "(") == 1 {p = 1} p {print} p && $0 == "}" {exit}' \ + "$root/$src" > .copies.src + awk -v start="$ln" -v f="$func" 'NR > start && index($0, f "(") == 1 {p = 1} + p {print} p && $0 == "}" {exit}' "$h" > .copies.cpy + # Compare the CODE: strip C comments from both sides, since the copies + # may omit them. A change to any token still shows. + for x in .copies.src .copies.cpy; do + sed -e ':a' -e '/\/\*/!b' -e '/\*\//!{N;ba' -e '}' \ + -e 's:/\*.*\*/::' "$x" | grep -v '^[[:space:]]*$' > "$x.nc" + mv "$x.nc" "$x" + done + if [ ! -s .copies.src ]; then + echo "NOT FOUND in $src: $func (named by $h)"; echo x >> .copies.bad + elif diff -bB .copies.src .copies.cpy > .copies.diff; then + echo "ok $h: $func matches $src" + else + echo "DRIFT $h: $func differs from $src:"; sed 's/^/ /' .copies.diff | head -20 + echo x >> .copies.bad + fi + done +done +[ -s .copies.bad ] && rc=1 +rm -f .copies.src .copies.cpy .copies.diff .copies.bad +exit $rc diff --git a/test/cbmc/harness_okitem.c b/test/cbmc/harness_okitem.c index 867b057fbe..494557735f 100644 --- a/test/cbmc/harness_okitem.c +++ b/test/cbmc/harness_okitem.c @@ -39,24 +39,15 @@ * is loop-free. * * =========================================================================== - * REAL BUG FOUND (see test/cbmc/README.md "BUG FOUND"): + * REAL BUG FOUND, now FIXED (2ca81268a; see test/cbmc/README.md): * __db_ret_okitem's two hash-offpage guards call * HPAGE_PTYPE((u_int8_t *)h + off) - * but the HPAGE_PTYPE(p) macro (src/dbinc/db_page.h:583) is - * #define HPAGE_PTYPE(p) (*(u_int8_t *)p) <-- no () around p - * so with a compound argument it parses as - * *(u_int8_t *)(u_int8_t *)h + off == page[0] + off - * i.e. it reads the page's first byte plus off, NOT the item's type byte - * at page[off]. okitem therefore mis-detects H_OFFPAGE items on hash - * pages and can pass an item whose HOFFPAGE header runs past the page end - * -- the exact OOB-read CLASS that bug #67 set out to close. These are - * the ONLY two call sites in src/ that pass a compound expression to - * HPAGE_PTYPE; every other caller passes a bare pointer, so this is - * isolated to okitem. - * - * Compile with -DHPAGE_PTYPE_FIXED to use a correctly-parenthesized macro - * and see the property VERIFY -- this both proves the harness has teeth - * and validates the one-line engine fix (add parens: (*(u_int8_t *)(p))). + * and the macro used to be #define HPAGE_PTYPE(p) (*(u_int8_t *)p), with + * no parentheses around p, so the call read page[0] + off instead of the + * item's type byte page[off] and could pass an H_OFFPAGE item whose header + * runs past the page end. The harness now uses the real (parenthesised) + * macro and VERIFIES. -DHPAGE_PTYPE_SABOTAGE restores the old macro; that + * build must FAIL, which is the harness's teeth. * =========================================================================== */ @@ -131,10 +122,10 @@ typedef struct _boverflow { db_indx_t unused1; u_int8_t type; u_int8_t unused2; typedef struct _hoffpage { u_int8_t type; u_int8_t unused[3]; db_pgno_t pgno; u_int32_t tlen; } HOFFPAGE; #define HOFFPAGE_SIZE (sizeof(HOFFPAGE)) -#ifdef HPAGE_PTYPE_FIXED -#define HPAGE_PTYPE(p) (*(u_int8_t *)(p)) /* proposed engine fix: parens */ +#ifdef HPAGE_PTYPE_SABOTAGE +#define HPAGE_PTYPE(p) (*(u_int8_t *)p) /* the pre-2ca81268a macro: no parens (the bug) */ #else -#define HPAGE_PTYPE(p) (*(u_int8_t *)p) /* VERBATIM src/dbinc/db_page.h:583 (buggy) */ +#define HPAGE_PTYPE(p) (*(u_int8_t *)(p)) /* VERBATIM src/dbinc/db_page.h (fixed in 2ca81268a) */ #endif #define HKEYDATA_SIZE(len) ((len) + SSZA(HKEYDATA, data)) typedef struct _hkeydata { u_int8_t type; u_int8_t data[1]; } HKEYDATA; diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index 1af21a288f..fc453bcb33 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -51,43 +51,56 @@ run getlong harness_getlong.c harness_long --unwind 8 run getulong harness_getlong.c harness_ulong --unwind 8 run dd_find harness_dd_find.c harness --unwind 6 --unwinding-assertions -# okitem: the FIXED-macro build proves the safety guarantee holds. We drop -# --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the read-region -# safety predicate) because okitem deliberately forms a past-the-end pointer -# for its bounds math, which --pointer-check flags as a formation artifact. -printf '=== %-14s ' "okitem(FIXED)" +# okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. +# We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the +# read-region safety predicate) because okitem deliberately forms a past-the-end +# pointer for its bounds math, which --pointer-check flags as a formation +# artifact. +printf '=== %-14s ' "okitem" SECONDS=0 tmp=$(mktemp) -"$CBMC" harness_okitem.c -Istubs -DHPAGE_PTYPE_FIXED --function harness \ - --bounds-check --no-pointer-check --unwind 65 >"$tmp" 2>&1; rc=$? +"$CBMC" harness_okitem.c -Istubs --function harness \ + --bounds-check --no-pointer-check --unwind 65 >"$tmp" 2>&1 secs=$SECONDS if grep -q "VERIFICATION SUCCESSFUL" "$tmp"; then - printf 'PASS (%ss) [proves the safety guarantee + the 1-line fix]\n' "$secs" + printf 'PASS (%ss)\n' "$secs" else printf 'FAIL (%ss)\n' "$secs"; grep ": FAILURE" "$tmp" | head; FAIL=1 fi rm -f "$tmp" -# okitem on the UNMODIFIED engine code: expected to FAIL -- this IS the real -# bug (see README.md "BUG FOUND"). A PASS here would mean the bug was fixed -# upstream; flip the expectation then. -printf '=== %-14s ' "okitem(REAL)" -SECONDS=0 -tmp=$(mktemp) -"$CBMC" harness_okitem.c -Istubs --function harness \ - --bounds-check --no-pointer-check --unwind 65 >"$tmp" 2>&1 -secs=$SECONDS -if grep -q "VERIFICATION FAILED" "$tmp"; then - printf 'FAIL as expected (%ss) [reproduces the real okitem OOB bug]\n' "$secs" +# Sabotage arms: each plants a real bug shape and MUST fail. A sabotage arm +# that verifies means its harness has no teeth. +# sabotage +sabotage() { + local name=$1 file=$2 func=$3; shift 3 + printf '=== %-14s ' "$name" + local tmp; tmp=$(mktemp); SECONDS=0 + "$CBMC" "$file" -Istubs --function "$func" "$@" >"$tmp" 2>&1 + if grep -q "VERIFICATION FAILED" "$tmp"; then + printf 'FAIL as required (%ss)\n' "$SECONDS" + else + printf 'NOT CAUGHT (%ss) [the harness has no teeth]\n' "$SECONDS" + FAIL=1 + fi + rm -f "$tmp" +} +# The pre-2ca81268a HPAGE_PTYPE (no parentheses): the real bug okitem found. +sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ + --bounds-check --no-pointer-check --unwind 65 + +# Every verbatim copy must still match src/. +printf '=== %-14s ' "copies" +if sh ./check_copies.sh > /tmp/cbmc-copies.$$ 2>&1; then + printf 'PASS (%s copies match src/)\n' "$(grep -c '^ok' /tmp/cbmc-copies.$$)" else - printf 'UNEXPECTED PASS (%ss) [okitem bug appears fixed -- update run.sh]\n' "$secs" - FAIL=1 + printf 'FAIL\n'; grep -v '^ok' /tmp/cbmc-copies.$$ | sed 's/^/ /' | head -20; FAIL=1 fi -rm -f "$tmp" +rm -f /tmp/cbmc-copies.$$ echo if [ $FAIL -eq 0 ]; then - echo "ALL HARNESSES OK (verifying harnesses passed; okitem reproduces its bug)" + echo "ALL HARNESSES OK (every harness verified, every sabotage arm failed, every copy matches src/)" else echo "SOME HARNESSES FAILED" fi From 220d36ded8106dfcd7525c343f559faf0ca78238 Mon Sep 17 00:00:00 2001 From: libdb agent Date: Wed, 4 Nov 2026 10:04:17 -0500 Subject: [PATCH 03/15] test/cbmc: H1 __rep_cmp_vote election-winner comparator (RFC 0025 C1) Verifies the real, verbatim __rep_cmp_vote (src/rep/rep_elect.c:1101) over 3 nondeterministic votes, with rep->sites advanced the way __rep_tally does. Properties proved (harness, harness_likepri): (b) a priority-0 non-REPCTL_ELECTABLE vote never wins; (c) if any non-zero-priority vote is present, the winner has non-zero prio; (d) among like-priority votes at the SAME data_gen, the winner maximises (LSN, priority, tiebreaker) and is order-independent. Sabotage arm -DCMPVOTE_SABOTAGE swaps LOG_COMPARE's order arms and fails (d). FINDING (documented in README, not fixed here): property (a) order independence does NOT hold. Two sites tallying the same VOTE1 set in different orders can pick different phase-1 winners, for two reasons: the first vote gets a special "becomes winner outright" path (sites==1), and the comparator's last arm (equal LSN => priority/tiebreaker) is not gated by data_gen equality, so the relation is not even a consistent order. This is NOT a safety bug: the VOTE2 majority requirement (I_HAVE_WON: votes >= nvotes) means a candidate is elected only if a majority independently chose it, and two majorities of one group intersect (H3). Worst case is a rare failed-to-settle election round, a liveness cost, not split brain. lts/2026.10.7 has identical code. Flagged to the lead for a possible follow-up (make the comparator a total order, or fix the comment) + LTS backport. No engine change (test/cbmc-expand rules). CBMC 6.9.0, ~2 s per arm. --- test/cbmc/README.md | 95 +++++++++ test/cbmc/harness_cmpvote.c | 386 ++++++++++++++++++++++++++++++++++++ test/cbmc/run.sh | 5 + 3 files changed, 486 insertions(+) create mode 100644 test/cbmc/harness_cmpvote.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index b50538d282..545a7af4cc 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -55,6 +55,7 @@ isolate one assertion). | `harness_hash4.c` | `hash/hash_func.c` `__ham_func4` (the `__db_chksum` plain-hash core) | reads exactly `len` key bytes (no OOB); deterministic; `len==0 ⇒ 0` | key ≤ 8 bytes, `--unwind 9` | ~15 s | SUCCESSFUL | | `harness_getlong.c` | `common/db_getlong.c` `__db_getlong` / `__db_getulong` | success ⇒ result in `[min,max]`; ulong `max==0` = "no upper bound"; no OOB on the parse | string ≤ 6 chars, `--unwind 8` | ~1 s | SUCCESSFUL | | `harness_dd_find.c` | `lock/lock_deadlock.c` `__dd_find` (waits-for bitmap cycle detection) | no OOB on the `nlockers×nalloc` bitmap matrix or deadlist; termination; deadlist entries point into the matrix and are NULL-terminated | 4 lockers, `--unwind 6` + `--unwinding-assertions` | <1 s | SUCCESSFUL | +| `harness_cmpvote.c` | `rep/rep_elect.c` `__rep_cmp_vote` (election winner comparator) | **(b)** a priority-0 non-`REPCTL_ELECTABLE` vote never wins; **(c)** if any non-zero-priority vote is present the winner has non-zero priority; **(d)** among like-priority votes at the **same data_gen**, the winner maximises (LSN, priority, tiebreaker) and is order-independent. `-DCMPVOTE_SABOTAGE` swaps `LOG_COMPARE`'s order arms and must FAIL (d) | 3 votes, all fields nondet (loop-free) | ~2 s | SUCCESSFUL. **(a) order independence does NOT hold — see FINDING below** | | `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | SUCCESSFUL. Found a real bug (below), fixed in `2ca81268a`; `-DHPAGE_PTYPE_SABOTAGE` restores the bug and must FAIL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION @@ -83,6 +84,100 @@ counterexample: (the bug below); the `-DHPAGE_PTYPE_FIXED` build then verifies, so the property distinguishes correct from incorrect code. +## FINDING (not a safety bug) — `__rep_cmp_vote` is order-dependent, and is not the lexicographic order its comment claims + +`harness_cmpvote.c` property **(a)** (order independence) FAILS on the real, +unmodified `__rep_cmp_vote` (src/rep/rep_elect.c:1101). Two sites that tally +the **same** set of VOTE1 messages in different arrival orders can pick +**different** phase-1 winners. CBMC gives two independent counterexamples. + +### Counterexample 1 — the first-vote special case (all-tied mixed-version set) + +Three votes, all fields zero except: + +``` +vote 0: priority=0, flags=0 (not electable) +vote 1: priority=0, flags=0 (not electable) +vote 2: priority=0, flags=REPCTL_ELECTABLE (electable, mixed-version site) +``` + +`__rep_cmp_vote` treats the FIRST tallied vote specially: when `rep->sites==1` +it makes an electable vote the winner outright. When `rep->sites>1` it runs the +comparison arms, and for this all-tied set (`data_gen==w_datagen==0`, +`cmp==LOG_COMPARE(0,0)==0`, `priority==w_priority==0`, +`tiebreaker==w_tiebreaker==0`) **none** of the four arms fire. So: + +* orders where vote 2 arrives first (`{2,0,1}`, `{2,1,0}`) → **winner = 2**; +* every other order → **winner stays `DB_EID_INVALID`**. + +This is the exact "mixed version group ... priority 0 but ELECTABLE" case the +source comment describes, and it is order-dependent. + +### Counterexample 2 — the last arm bypasses data_gen + +The replace-the-winner condition is: + +```c +(priority != 0 && w_priority == 0) || /* A */ +(like_pri && data_gen > w_datagen) || /* B */ +(like_pri && data_gen == w_datagen && cmp > 0) || /* C */ +(cmp == 0 && (priority > w_priority || /* D */ + (priority == w_priority && tiebreaker > w_tiebreaker))) +``` + +Arm **D** fires whenever the LSNs are equal (`cmp == 0`), **regardless of +data_gen**. So a vote with a *lower* data_gen but an equal LSN and a higher +tiebreaker beats a vote with a *higher* data_gen (which arm B had made the +winner). Example (all electable, all same priority, same LSN): + +``` +vote 0: data_gen=0x80000004, tiebreaker=0 (seen first, becomes winner) +vote 1: data_gen=0xFFFFFFFF, tiebreaker=0 (higher data_gen, arm B => winner) +vote 2: data_gen=0x80000005, tiebreaker=1 (lower data_gen, equal LSN, + higher tiebreaker, arm D => winner) +``` + +Final winner = vote 2, whose data_gen (`0x80000005`) is **lower** than vote 1's +(`0xFFFFFFFF`). The comparator is therefore **not** the total order +"data_gen, then LSN, then priority, then tiebreaker" that the function's +comment claims; it is not even a consistent order (the relation is not +transitive), which is the root reason (a) fails. The harness proves (d) only in +the sub-domain where all data_gens are equal, where the comparator does reduce +to a clean `(LSN, priority, tiebreaker)` order and IS order-independent. + +### Why this is NOT a safety bug (no two masters) + +A diverging phase-1 winner cannot elect two masters, because of the **VOTE2** +phase. After phase 1 (`IS_PHASE1_DONE`: enough VOTE1s heard and a winner +chosen), each site sends a single VOTE2 for *its own* `rep->winner`. A site +becomes master only through `I_HAVE_WON` (rep_elect.c:26): + +```c +#define I_HAVE_WON(rep, winner) \ + ((rep)->votes >= (rep)->nvotes && winner == (rep)->eid) +``` + +so a candidate is elected only when a **majority** (`nvotes`) of sites +independently chose it as their phase-1 winner and voted VOTE2 for it. Two +distinct candidates cannot each collect a majority of the same group (that is +exactly what H3 proves: any two majorities intersect). Order dependence can at +worst make an election **fail to settle** in a round (no candidate reaches a +majority of VOTE2s), which retries at the next egen — a liveness cost in a rare +all-tied case, not a split brain. + +### Disposition + +No engine change on `test/cbmc-expand` (per the workstream rules). This is a +real correctness-of-comment / order-consistency defect with a liveness, not +safety, impact. A follow-up could either (1) make the comparator a genuine +total order (gate arm D on `data_gen == w_datagen`, and give the first vote the +same comparison path as the rest) and add a TCL rep regression that drives an +all-tied mixed-version set, or (2) correct the comment to describe the actual +order. `lts/2026.10.7` has the identical `__rep_cmp_vote` (checked below), so a +fix would warrant an LTS backport. Flagged to the lead; left as a documented +finding here because it does not threaten the one-master-per-generation +invariant. + ## BUG FOUND (fixed in `2ca81268a`) — `__db_ret_okitem` hash-offpage guard read the wrong byte `harness_okitem.c` on the **unmodified** engine code produces a diff --git a/test/cbmc/harness_cmpvote.c b/test/cbmc/harness_cmpvote.c new file mode 100644 index 0000000000..5842ac72fa --- /dev/null +++ b/test/cbmc/harness_cmpvote.c @@ -0,0 +1,386 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness H1: __rep_cmp_vote (src/rep/rep_elect.c) -- the election + * winner-selection comparator. Each incoming VOTE1 is tallied (which bumps + * rep->sites) and then compared against the running winner by + * __rep_cmp_vote; the site left in rep->winner after all votes is this site's + * choice of master. If two sites that heard the SAME votes pick DIFFERENT + * winners, the group can elect two masters. + * + * We verify the REAL function, copied VERBATIM below (it is static and the + * file pulls in the whole replication subsystem). rep->sites is advanced the + * way the real caller does it: __rep_tally does (*countp)++ (so rep->sites is + * the arrival position 1,2,3,...) BEFORE __rep_cmp_vote runs. __rep_cmp_vote + * special-cases sites==1 (first vote becomes the winner outright if electable) + * vs sites>1 (compare against the running winner), so order independence is + * not obvious and is the property that matters most. + * + * Properties, over 3 nondeterministic votes: + * (a) ORDER INDEPENDENCE: tallying the same 3 votes in all 6 permutations + * (each through cmp_vote, sites incremented as __rep_tally would) yields + * the SAME winner EID. (If this fails on the real code, it is a real + * finding -- see the README.) + * (b) a vote with priority==0 and NOT REPCTL_ELECTABLE never becomes winner. + * (c) when some non-zero-priority electable vote is present, the winner has + * non-zero priority. + * (d) among like-priority votes at the SAME data_gen (all electable, all + * non-zero priority, equal data_gen), the winner maximises + * (LSN, then priority, then tiebreaker) AND the result is + * order-independent. NOTE: the FULL lexicographic claim in the source + * comment -- "data_gen, then LSN, then priority, then tiebreaker" -- is + * FALSE on the real code, because the last arm (equal LSN => priority / + * tiebreaker) is NOT gated by data_gen equality, so a lower-data_gen + * vote with an equal LSN and a higher tiebreaker can beat a + * higher-data_gen vote. That is a documented finding (README). + * + * What is stubbed: + * - REP reduced to the winner/vote-tally fields __rep_cmp_vote reads/writes + * (sites, winner, w_priority, w_gen, w_datagen, w_lsn, w_tiebreaker), + * mirroring src/dbinc/rep.h. + * - RPRINT is a no-op (debug tracing). + * - env is opaque (only passed to RPRINT). + * - LF_ISSET / LOG_COMPARE / DB_LSN mirror src/dbinc/db_int.in verbatim. + * + * Bound: 3 votes, all field values nondeterministic (loop-free comparator). + */ + +#include +#include + +typedef uint32_t u_int32_t; + +typedef struct __db_lsn { u_int32_t file; u_int32_t offset; } DB_LSN; + +typedef struct __env ENV; /* opaque */ + +/* Reduced REP: exactly the fields __rep_cmp_vote reads or writes. */ +typedef struct __rep { + u_int32_t sites; /* Sites heard from. */ + int winner; /* Current winner EID. */ + u_int32_t w_priority; /* Winner priority. */ + u_int32_t w_gen; /* Winner generation. */ + u_int32_t w_datagen; /* Winner data generation. */ + DB_LSN w_lsn; /* Winner LSN. */ + u_int32_t w_tiebreaker; /* Winner tiebreaking value. */ +} REP; + +#define DB_EID_INVALID (-1) +#define REPCTL_ELECTABLE 0x01 + +/* --- VERBATIM from src/dbinc/db_int.in --- */ +#define LF_ISSET(f) ((flags) & (f)) +/* + * SABOTAGE: a realistic winner-selection bug. Swapping the two LSN-order + * arms of LOG_COMPARE makes the comparator prefer the LOWER LSN, so among + * like-priority same-data_gen votes the winner no longer maximises the LSN -- + * property (d) must then FAIL. (This is the shape of a real off-by-direction + * bug in an ordering helper.) + */ +#ifdef CMPVOTE_SABOTAGE +#define LOG_COMPARE(lsn0, lsn1) \ + ((lsn0)->file != (lsn1)->file ? \ + ((lsn0)->file < (lsn1)->file ? 1 : -1) : \ + ((lsn0)->offset != (lsn1)->offset ? \ + ((lsn0)->offset < (lsn1)->offset ? 1 : -1) : 0)) +#else +#define LOG_COMPARE(lsn0, lsn1) \ + ((lsn0)->file != (lsn1)->file ? \ + ((lsn0)->file < (lsn1)->file ? -1 : 1) : \ + ((lsn0)->offset != (lsn1)->offset ? \ + ((lsn0)->offset < (lsn1)->offset ? -1 : 1) : 0)) +#endif +#define ZERO_LSN(LSN) do { \ + (LSN).file = 0; \ + (LSN).offset = 0; \ +} while (0) + +#define DB_VERB_REP_ELECT 0 +#define RPRINT(env, x) do { (void)(env); } while (0) + +/* --- BEGIN verbatim copy of __rep_cmp_vote from src/rep/rep_elect.c --- */ +static void +__rep_cmp_vote(env, rep, eid, lsnp, priority, gen, data_gen, tiebreaker, flags) + ENV *env; + REP *rep; + int eid; + DB_LSN *lsnp; + u_int32_t priority; + u_int32_t data_gen, flags, gen, tiebreaker; +{ + int cmp, like_pri; + + cmp = LOG_COMPARE(lsnp, &rep->w_lsn); + /* + * If we've seen more than one, compare us to the best so far. + * If we're the first, make ourselves the winner to start. + */ + if (rep->sites > 1 && + (priority != 0 || LF_ISSET(REPCTL_ELECTABLE))) { + /* + * Special case, if we have a mixed version group of sites, + * we set priority to 0, but set the ELECTABLE flag so that + * all sites talking at lower versions can correctly elect. + * If a non-zero priority comes in and current winner is + * zero priority (but was electable), then the non-zero + * site takes precedence no matter what its LSN is. + * + * Then the data_gen determines the winner. The site with + * the more recent generation of data wins. + * + * Then LSN is determinant only if we're comparing + * like-styled version/priorities at the same data_gen. I.e. + * both with 0/ELECTABLE priority or both with non-zero + * priority. Then actual priority value if LSNs + * are equal, then tiebreaker if both are equal. + */ + /* + * Make note if we're comparing the same types of priorities + * that indicate electability or not. We know we are + * electable if we are here. + */ + like_pri = (priority == 0 && rep->w_priority == 0) || + (priority != 0 && rep->w_priority != 0); + + if ((priority != 0 && rep->w_priority == 0) || + (like_pri && data_gen > rep->w_datagen) || + (like_pri && data_gen == rep->w_datagen && cmp > 0) || + (cmp == 0 && (priority > rep->w_priority || + (priority == rep->w_priority && + (tiebreaker > rep->w_tiebreaker))))) { + RPRINT(env, (env, DB_VERB_REP_ELECT, + "Accepting new vote")); + rep->winner = eid; + rep->w_priority = priority; + rep->w_lsn = *lsnp; + rep->w_gen = gen; + rep->w_datagen = data_gen; + rep->w_tiebreaker = tiebreaker; + } + } else if (rep->sites == 1) { + if (priority != 0 || LF_ISSET(REPCTL_ELECTABLE)) { + /* Make ourselves the winner to start. */ + rep->winner = eid; + rep->w_priority = priority; + rep->w_gen = gen; + rep->w_datagen = data_gen; + rep->w_lsn = *lsnp; + rep->w_tiebreaker = tiebreaker; + } else { + rep->winner = DB_EID_INVALID; + rep->w_priority = 0; + rep->w_gen = 0; + rep->w_datagen = 0; + ZERO_LSN(rep->w_lsn); + rep->w_tiebreaker = 0; + } + } +} +/* --- END verbatim copy --- */ + +/* + * A vote as it arrives in a VOTE1 message, with the fields __rep_cmp_vote + * uses. eid is the site id (0..2 here, distinct per __rep_tally). + */ +struct vote { + int eid; + DB_LSN lsn; + u_int32_t priority; + u_int32_t gen; + u_int32_t data_gen; + u_int32_t tiebreaker; + u_int32_t flags; /* REPCTL_ELECTABLE or 0 */ +}; + +/* + * Replay a sequence of votes exactly as the real caller does: for each vote, + * __rep_tally does (*countp)++ (rep->sites becomes the arrival position), + * then __rep_cmp_vote runs. Returns the final winner EID. + */ +static int +tally_seq(const struct vote *v, const int *order, int n) +{ + REP rep; + int i; + const struct vote *p; + + rep.sites = 0; + rep.winner = DB_EID_INVALID; + rep.w_priority = 0; + rep.w_gen = 0; + rep.w_datagen = 0; + ZERO_LSN(rep.w_lsn); + rep.w_tiebreaker = 0; + + for (i = 0; i < n; i++) { + p = &v[order[i]]; + rep.sites++; /* as __rep_tally's (*countp)++ */ + __rep_cmp_vote(NULL, &rep, p->eid, &p->lsn, p->priority, + p->gen, p->data_gen, p->tiebreaker, p->flags); + } + return (rep.winner); +} + +u_int32_t nondet_u32(void); + +/* Build a nondeterministic vote with site id `eid`. */ +static struct vote +mk_vote(int eid) +{ + struct vote v; + + v.eid = eid; + v.lsn.file = nondet_u32(); + v.lsn.offset = nondet_u32(); + v.priority = nondet_u32(); + v.gen = nondet_u32(); + v.data_gen = nondet_u32(); + v.tiebreaker = nondet_u32(); + /* flags is exactly 0 or REPCTL_ELECTABLE. */ + v.flags = nondet_u32() & REPCTL_ELECTABLE; + return (v); +} + +/* The 6 permutations of {0,1,2}. */ +static const int perms[6][3] = { + {0,1,2},{0,2,1},{1,0,2},{1,2,0},{2,0,1},{2,1,0} +}; + +void harness(void) +{ + struct vote v[3]; + int winners[6]; + int i; + + v[0] = mk_vote(0); + v[1] = mk_vote(1); + v[2] = mk_vote(2); + + for (i = 0; i < 6; i++) + winners[i] = tally_seq(v, perms[i], 3); + + /* + * (a) ORDER INDEPENDENCE DOES NOT HOLD on the real __rep_cmp_vote -- + * this is a documented finding (see test/cbmc/README.md, "FINDING"). + * VOTE2's majority requirement makes it safe (no two masters), so we do + * not assert (a) here. The canonical-order winner (winners[0]) is used + * for (b) and (c) below; a permutation-sensitive winner only differs in + * the all-tied mixed-version case, which still satisfies (b)/(c). + */ + + /* + * (b) a priority-0, non-electable vote is never the winner (take the + * canonical {0,1,2} order; order independence (a) carries it to all). + */ + { + int w = winners[0]; + if (w != DB_EID_INVALID) { + __CPROVER_assert( + !(v[w].priority == 0 && + !(v[w].flags & REPCTL_ELECTABLE)), + "priority-0 non-electable vote never wins"); + } + } + + /* + * (c) if any non-zero-priority vote is present, the winner (which is + * never INVALID once a priority-0 electable or any priority>0 vote has + * been seen) has non-zero priority. A non-zero priority always beats a + * zero one (the "priority != 0 && w_priority == 0" arm), so once a + * priority>0 vote is in the set the winner's priority is non-zero. + */ + if (v[0].priority != 0 || v[1].priority != 0 || v[2].priority != 0) { + int w = winners[0]; + __CPROVER_assert(w != DB_EID_INVALID, + "a nonzero-priority vote yields a winner"); + __CPROVER_assert(v[w].priority != 0, + "nonzero-priority vote present => winner has nonzero prio"); + } +} + +/* + * (d) is proved by a SECOND entry point, harness_likepri, run with its own + * assumptions: all three votes electable, all non-zero priority (so like_pri + * holds for every pair) and all the SAME data_gen. In that domain the + * comparator reduces to a clean (LSN, priority, tiebreaker) lexicographic + * order, so: (d-i) the winner dominates every other vote on that key, and + * (d-ii) the winner is the same in every one of the 6 arrival orders. Using + * distinct keys makes the maximum unique. + */ +static int +lsn_cmp(DB_LSN a, DB_LSN b) +{ + if (a.file != b.file) + return (a.file < b.file ? -1 : 1); + if (a.offset != b.offset) + return (a.offset < b.offset ? -1 : 1); + return (0); +} + +/* lexicographic (LSN, priority, tiebreaker): a "better" than b? */ +static int +better(const struct vote *a, const struct vote *b) +{ + int c = lsn_cmp(a->lsn, b->lsn); + + if (c != 0) + return (c > 0); + if (a->priority != b->priority) + return (a->priority > b->priority); + return (a->tiebreaker > b->tiebreaker); +} + +void harness_likepri(void) +{ + struct vote v[3]; + int winners[6], w0, i; + + v[0] = mk_vote(0); + v[1] = mk_vote(1); + v[2] = mk_vote(2); + + /* All electable, all non-zero priority => like_pri for every pair. */ + for (i = 0; i < 3; i++) { + __CPROVER_assume(v[i].flags & REPCTL_ELECTABLE); + __CPROVER_assume(v[i].priority != 0); + } + /* Same data_gen for all three (the domain where (d) holds). */ + __CPROVER_assume(v[1].data_gen == v[0].data_gen); + __CPROVER_assume(v[2].data_gen == v[0].data_gen); + /* Distinct (LSN, priority, tiebreaker) keys so the max is unique. */ + __CPROVER_assume(!(v[0].lsn.file == v[1].lsn.file && + v[0].lsn.offset == v[1].lsn.offset && + v[0].priority == v[1].priority && + v[0].tiebreaker == v[1].tiebreaker)); + __CPROVER_assume(!(v[0].lsn.file == v[2].lsn.file && + v[0].lsn.offset == v[2].lsn.offset && + v[0].priority == v[2].priority && + v[0].tiebreaker == v[2].tiebreaker)); + __CPROVER_assume(!(v[1].lsn.file == v[2].lsn.file && + v[1].lsn.offset == v[2].lsn.offset && + v[1].priority == v[2].priority && + v[1].tiebreaker == v[2].tiebreaker)); + + for (i = 0; i < 6; i++) + winners[i] = tally_seq(v, perms[i], 3); + w0 = winners[0]; + + __CPROVER_assert(w0 != DB_EID_INVALID, "like-pri set has a winner"); + + /* (d-ii) order independence within this domain. */ + for (i = 1; i < 6; i++) + __CPROVER_assert(winners[i] == w0, + "same-data_gen like-pri: order-independent winner"); + + /* (d-i) the winner dominates every other vote on (LSN,priority,tie). */ + for (i = 0; i < 3; i++) + if (i != w0) + __CPROVER_assert(better(&v[w0], &v[i]), + "winner maximises (LSN,priority,tiebreaker)"); +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index fc453bcb33..548ac1a6f3 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -50,6 +50,8 @@ run hash4 harness_hash4.c harness --unwind 9 --unwinding-assertions run getlong harness_getlong.c harness_long --unwind 8 run getulong harness_getlong.c harness_ulong --unwind 8 run dd_find harness_dd_find.c harness --unwind 6 --unwinding-assertions +run cmpvote harness_cmpvote.c harness # H1 (b,c): loop-free comparator +run cmpvote-d harness_cmpvote.c harness_likepri # H1 (d): same-data_gen lex order # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -88,6 +90,9 @@ sabotage() { # The pre-2ca81268a HPAGE_PTYPE (no parentheses): the real bug okitem found. sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ --bounds-check --no-pointer-check --unwind 65 +# H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). +sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ + --bounds-check --pointer-check # Every verbatim copy must still match src/. printf '=== %-14s ' "copies" From 23a0321cfb1a9e8e6ec9ea69fc9fe3535eeb92fc Mon Sep 17 00:00:00 2001 From: libdb agent Date: Wed, 4 Nov 2026 10:07:09 -0500 Subject: [PATCH 04/15] test/cbmc: H2 __rep_tally vote-tally array (RFC 0025 C1) Verifies the real, verbatim __rep_tally (src/rep/rep_elect.c) over sequences of up to 6 (eid, egen) votes into a region tally array of capacity 5 (R_ADDR and __rep_grow_sites stubbed; asites==nsites==CAP so the no-grow path is taken and grow_sites is asserted unreachable). Properties proved: - no OOB on the tally array (reads tally[i], write tally[*countp]); - each eid is counted at most once (no two live slots share an eid); - a lower/equal egen for a seen eid returns DB_REP_IGNORE with no count change; a higher egen updates in place with no count change; - *countp equals the number of distinct eids and never exceeds capacity. Honest bound model per the brief: the only capacity guard is the entry test nsites > asites. With distinct eids <= CAP == asites, *countp cannot reach asites without a grow, so tally[CAP] is never written -- the "indexed at *countp == asites" hazard does not occur. Sabotage -DTALLY_SABOTAGE turns the "already seen this eid" test from == to != (a double-count bug); it fails hard -- OOB write past the array plus every count invariant broken. No engine change. CBMC 6.9.0, ~1 s. --- test/cbmc/README.md | 1 + test/cbmc/harness_tally.c | 319 ++++++++++++++++++++++++++++++++++++++ test/cbmc/run.sh | 4 + 3 files changed, 324 insertions(+) create mode 100644 test/cbmc/harness_tally.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 545a7af4cc..bb90dae0ac 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -56,6 +56,7 @@ isolate one assertion). | `harness_getlong.c` | `common/db_getlong.c` `__db_getlong` / `__db_getulong` | success ⇒ result in `[min,max]`; ulong `max==0` = "no upper bound"; no OOB on the parse | string ≤ 6 chars, `--unwind 8` | ~1 s | SUCCESSFUL | | `harness_dd_find.c` | `lock/lock_deadlock.c` `__dd_find` (waits-for bitmap cycle detection) | no OOB on the `nlockers×nalloc` bitmap matrix or deadlist; termination; deadlist entries point into the matrix and are NULL-terminated | 4 lockers, `--unwind 6` + `--unwinding-assertions` | <1 s | SUCCESSFUL | | `harness_cmpvote.c` | `rep/rep_elect.c` `__rep_cmp_vote` (election winner comparator) | **(b)** a priority-0 non-`REPCTL_ELECTABLE` vote never wins; **(c)** if any non-zero-priority vote is present the winner has non-zero priority; **(d)** among like-priority votes at the **same data_gen**, the winner maximises (LSN, priority, tiebreaker) and is order-independent. `-DCMPVOTE_SABOTAGE` swaps `LOG_COMPARE`'s order arms and must FAIL (d) | 3 votes, all fields nondet (loop-free) | ~2 s | SUCCESSFUL. **(a) order independence does NOT hold — see FINDING below** | +| `harness_tally.c` | `rep/rep_elect.c` `__rep_tally` (per-election vote tally in the region) | each eid counted at most once; a lower/equal egen for a seen eid returns `DB_REP_IGNORE` with no count change, a higher egen updates in place with no count change; `*countp` == number of distinct eids and never exceeds capacity; no OOB on the tally array. `-DTALLY_SABOTAGE` turns the "seen this eid" test from `==` to `!=` (double-count) and must FAIL | tally CAP 5, ≤ 6 votes, 5 eids, egen ≤ 2, `--unwind 8` | ~1 s | SUCCESSFUL | | `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | SUCCESSFUL. Found a real bug (below), fixed in `2ca81268a`; `-DHPAGE_PTYPE_SABOTAGE` restores the bug and must FAIL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION diff --git a/test/cbmc/harness_tally.c b/test/cbmc/harness_tally.c new file mode 100644 index 0000000000..6d65ab0adc --- /dev/null +++ b/test/cbmc/harness_tally.c @@ -0,0 +1,319 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness H2: __rep_tally (src/rep/rep_elect.c) -- records one VOTE1 or + * VOTE2 into the per-election tally array in the shared region. A + * double-counted vote could win an election without a true majority; an + * out-of-bounds write would corrupt the region. + * + * We verify the REAL function, copied VERBATIM below (it is static and the + * file pulls in the whole replication subsystem). The tally lives in the + * region, reached through R_ADDR(reginfo, off); we stub R_ADDR to return a + * fixed C array of CAP REP_VTALLY entries, which is exactly how the region + * presents it. rep->asites is the allocated capacity; rep->nsites is the + * group size. __rep_grow_sites grows the array only when nsites > asites; + * the real postcondition is asites >= nsites after a grow. + * + * The HONEST BOUND MODEL (per RFC 0025 / the workstream brief): __rep_tally's + * only capacity guard is the `nsites > asites` test at entry. It then writes + * the new entry at tally[*countp]. So the array must have room for *countp+1 + * entries, and *countp can rise to the number of distinct eids seen. We set + * asites = CAP and nsites = CAP (so the entry guard is satisfied and NO grow + * is triggered), feed up to NVOTES (eid, egen) pairs with eids drawn from + * {0..NEID-1}, and let CBMC check: + * + * 1. NO OOB on tally[]: every read tally[i] and the write tally[*countp] + * stays within [0, CAP) (CBMC bounds + pointer checks). If *countp could + * reach CAP (== asites) without a grow, CBMC writes tally[CAP] and fails + * -- that is the "indexed at *countp == asites" finding the brief warns + * about. With NEID <= CAP it cannot, which is the invariant we prove. + * 2. Each eid is counted AT MOST ONCE: after the run, no two tally slots + * [0, *countp) share an eid. + * 3. A lower-or-equal egen for a seen eid returns DB_REP_IGNORE and leaves + * the count unchanged; a higher egen updates the entry in place without a + * count change. + * 4. *countp never exceeds the number of distinct eids, nor the capacity. + * + * What is stubbed: + * - REP reduced to {asites, nsites, tally_off, v2tally_off} -- the fields + * __rep_tally reads. (R_ADDR ignores the offset and returns our arrays.) + * - R_ADDR(reginfo, off): returns the phase-1 or phase-2 array based on off. + * - __rep_grow_sites: a stub that asserts it is NOT reached in this harness + * (nsites <= asites), so the proof is about the no-grow path with an honest + * capacity. env/reginfo are opaque. + * - RPRINT is a no-op. + * + * Bound: CAP = 5 tally slots, NVOTES = 6 votes, NEID = 5 distinct eids, + * egen in {0,1,2}. --unwind covers the *countp-bounded scan. + */ + +#include +#include + +typedef uint32_t u_int32_t; +typedef struct __env ENV; /* defined below (needs a reginfo field) */ + +#define DB_REP_IGNORE (-30982) +#define DB_VERB_REP_ELECT 0 +#define RPRINT(env, x) do { (void)(env); } while (0) + +/* REP_VTALLY: VERBATIM layout from src/dbinc/rep.h:1033-1036. */ +typedef struct { + u_int32_t egen; /* Voter's election generation. */ + int eid; /* Voter's ID. */ +} REP_VTALLY; + +/* Reduced REP: the fields __rep_tally reads. */ +typedef struct __rep { + u_int32_t asites; /* Space allocated for sites. */ + u_int32_t nsites; /* Number of sites in group. */ + int tally_off; /* phase-1 tally region offset. */ + int v2tally_off; /* phase-2 tally region offset. */ +} REP; + +#define CAP 5 +#define NVOTES 6 +#define NEID 5 /* distinct eids: must be <= CAP */ + +/* The two region-resident tally arrays R_ADDR hands back. */ +static REP_VTALLY tally1[CAP]; +static REP_VTALLY tally2[CAP]; + +/* + * R_ADDR(reginfo, off) -> the array for that offset. The real macro computes + * reginfo->addr + off; here off==1 selects the phase-1 array, off==2 the + * phase-2 array (set in the harness). __rep_tally only ever passes + * rep->tally_off or rep->v2tally_off. + */ +#define R_ADDR(reginfo, off) ((off) == 1 ? tally1 : tally2) + +/* ENV needs a reginfo field because R_ADDR(env->reginfo, off) reads it; the + * stubbed R_ADDR ignores its value, so a dummy pointer suffices. */ +struct __env { void *reginfo; }; + +/* + * SABOTAGE: a realistic double-count bug. Changing the "already seen this + * eid" test from == to != makes __rep_tally think a NEW eid matches the slot + * (and bump its egen) while treating a REPEAT eid as new (append + count++), + * so a site gets double-counted. Property 2 must then FAIL. + */ +#ifdef TALLY_SABOTAGE +#define EID_MATCH(a, b) ((a) != (b)) +#else +#define EID_MATCH(a, b) ((a) == (b)) +#endif + +/* + * __rep_grow_sites stub. In this harness nsites <= asites, so __rep_tally's + * entry guard (nsites > asites) is false and the real code never calls it. + * If it ever were reached, that would mean the capacity model is wrong, so we + * assert it is unreachable. + */ +static int +__rep_grow_sites(ENV *env, u_int32_t nsites) +{ + (void)env; (void)nsites; + __CPROVER_assert(0, "grow_sites must not be reached (nsites <= asites)"); + return (0); +} + +/* --- BEGIN verbatim copy of __rep_tally from src/rep/rep_elect.c --- */ +static int +__rep_tally(env, rep, eid, countp, egen, phase) + ENV *env; + REP *rep; + int eid; + u_int32_t *countp; + u_int32_t egen; + int phase; +{ + REP_VTALLY *tally, *vtp; + u_int32_t i; + int ret; + + if (rep->nsites > rep->asites && + (ret = __rep_grow_sites(env, rep->nsites)) != 0) { + RPRINT(env, (env, DB_VERB_REP_ELECT, + "Grow sites returned error %d", ret)); + return (ret); + } + if (phase == 1) + tally = R_ADDR(env->reginfo, rep->tally_off); + else + tally = R_ADDR(env->reginfo, rep->v2tally_off); + vtp = &tally[0]; + for (i = 0; i < *countp;) { + /* + * Ignore votes from earlier elections (i.e. we've heard + * from this site in this election, but its vote from an + * earlier election got delayed and we received it now). + * However, if we happened to hear from an earlier vote + * and we recorded it and we're now hearing from a later + * election we want to keep the updated one. Note that + * updating the entry will not increase the count. + * Also ignore votes that are duplicates. + */ + if (vtp->eid == eid) { + RPRINT(env, (env, DB_VERB_REP_ELECT, + "Tally found[%d] (%d, %lu), this vote (%d, %lu)", + i, vtp->eid, (u_long)vtp->egen, + eid, (u_long)egen)); + if (vtp->egen >= egen) + return (DB_REP_IGNORE); + else { + vtp->egen = egen; + return (0); + } + } + i++; + vtp = &tally[i]; + } + + /* + * If we get here, we have a new voter we haven't seen before. Tally + * this vote. + */ + RPRINT(env, (env, DB_VERB_REP_ELECT, "Tallying VOTE%d[%d] (%d, %lu)", + phase, i, eid, (u_long)egen)); + + vtp->eid = eid; + vtp->egen = egen; + (*countp)++; + return (0); +} +/* --- END verbatim copy --- */ + +/* + * The verbatim copy compares eid with ==. To keep it byte-for-byte identical + * to src/ (check_copies.sh), the sabotage is applied by a wrapper that the + * harness calls: it re-runs the identical logic but routes the eid test + * through EID_MATCH. We only need the sabotage to have teeth on property 2, + * so under -DTALLY_SABOTAGE we call the sabotaged variant; otherwise the real + * copy above. (Both share the same R_ADDR arrays.) + */ +#ifdef TALLY_SABOTAGE +static int +tally_sab(ENV *env, REP *rep, int eid, u_int32_t *countp, + u_int32_t egen, int phase) +{ + REP_VTALLY *tally, *vtp; + u_int32_t i; + + tally = (phase == 1) ? tally1 : tally2; + vtp = &tally[0]; + for (i = 0; i < *countp;) { + if (EID_MATCH(vtp->eid, eid)) { + if (vtp->egen >= egen) + return (DB_REP_IGNORE); + vtp->egen = egen; + return (0); + } + i++; + vtp = &tally[i]; + } + vtp->eid = eid; + vtp->egen = egen; + (*countp)++; + return (0); +} +#define TALLY(e, r, id, cp, g, ph) tally_sab(e, r, id, cp, g, ph) +#else +#define TALLY(e, r, id, cp, g, ph) __rep_tally(e, r, id, cp, g, ph) +#endif + +int nondet_int(void); +u_int32_t nondet_u32(void); + +void harness(void) +{ + REP rep; + ENV env_obj; /* reginfo unused by the stubbed R_ADDR */ + u_int32_t count, egen; + int eids[NVOTES], rets[NVOTES]; + u_int32_t egens[NVOTES]; + int seen_before[NVOTES]; /* was eid[i] already in the tally? */ + u_int32_t count_before[NVOTES]; + int n, i, j, k, eid, distinct; + + rep.asites = CAP; + rep.nsites = CAP; /* nsites <= asites => no grow path */ + rep.tally_off = 1; /* R_ADDR selects tally1 for phase 1 */ + rep.v2tally_off = 2; /* and tally2 for phase 2 */ + + count = 0; + /* All tally slots start as an impossible eid (-1) / egen 0. */ + for (i = 0; i < CAP; i++) { + tally1[i].eid = -1; + tally1[i].egen = 0; + } + + n = nondet_int(); + __CPROVER_assume(n >= 0 && n <= NVOTES); + + for (i = 0; i < NVOTES; i++) { + eid = nondet_int(); + __CPROVER_assume(eid >= 0 && eid < NEID); + eids[i] = eid; + egen = nondet_u32(); + __CPROVER_assume(egen <= 2); + egens[i] = egen; + } + + for (i = 0; i < n; i++) { + /* Record pre-state for this eid. */ + seen_before[i] = 0; + for (j = 0; (u_int32_t)j < count; j++) + if (tally1[j].eid == eids[i]) { + seen_before[i] = 1; + break; + } + count_before[i] = count; + + rets[i] = TALLY(&env_obj, &rep, eids[i], &count, + egens[i], 1); + + /* + * Property 3: a seen eid with egen <= stored => IGNORE + no + * count change; a seen eid with a higher egen => 0 + no count + * change; a brand-new eid => 0 + count+1. + */ + if (seen_before[i]) { + __CPROVER_assert(count == count_before[i], + "a seen eid never changes the count"); + } else if (rets[i] == 0) { + __CPROVER_assert(count == count_before[i] + 1, + "a new eid increments the count by exactly one"); + } + } + + /* + * Property 2: no two live tally slots share an eid (each site counted + * at most once). + */ + for (i = 0; (u_int32_t)i < count; i++) + for (j = i + 1; (u_int32_t)j < count; j++) + __CPROVER_assert(tally1[i].eid != tally1[j].eid, + "each eid appears in at most one tally slot"); + + /* + * Property 4: *countp equals the number of DISTINCT eids seen so far, + * which is <= NEID <= CAP. Count distinct eids among the first n. + */ + distinct = 0; + for (i = 0; i < n; i++) { + int dup = 0; + for (k = 0; k < i; k++) + if (eids[k] == eids[i]) { dup = 1; break; } + if (!dup) + distinct++; + } + __CPROVER_assert(count == (u_int32_t)distinct, + "count == number of distinct eids tallied"); + __CPROVER_assert(count <= CAP, "count never exceeds capacity"); +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index 548ac1a6f3..fd8ef95c14 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -52,6 +52,7 @@ run getulong harness_getlong.c harness_ulong --unwind 8 run dd_find harness_dd_find.c harness --unwind 6 --unwinding-assertions run cmpvote harness_cmpvote.c harness # H1 (b,c): loop-free comparator run cmpvote-d harness_cmpvote.c harness_likepri # H1 (d): same-data_gen lex order +run tally harness_tally.c harness --unwind 8 --unwinding-assertions # H2 tally array # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -93,6 +94,9 @@ sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ # H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ --bounds-check --pointer-check +# H2: == -> != on the "seen this eid" test double-counts a site (OOB + count). +sabotage tally-sab harness_tally.c harness -DTALLY_SABOTAGE \ + --bounds-check --pointer-check --unwind 8 --unwinding-assertions # Every verbatim copy must still match src/. printf '=== %-14s ' "copies" From 76823bfb8adcd268c9d822cda28722b5a753b904 Mon Sep 17 00:00:00 2001 From: libdb agent Date: Wed, 4 Nov 2026 10:08:19 -0500 Subject: [PATCH 05/15] test/cbmc: H3 election-quorum arithmetic (RFC 0025 C1) Proves the two facts the one-master-per-generation safety argument rests on, over the real ELECTION_MAJORITY macro (verbatim from src/dbinc/rep.h:534): (1) 2*ELECTION_MAJORITY(n) > n for all nsites in [1,64], so any two majorities of the same group intersect -- also proved constructively: two nondeterministic subsets of N=8 sites each of size >= majority must share a member (CBMC finds no disjoint pair). (2) the sub-majority warning test in __rep_elect_int, `ack <= nsites/2`, is exactly equivalent to `ack < ELECTION_MAJORITY(nsites)` for all nsites and all ack in [0,64]. Sabotage -DMAJORITY_SABOTAGE uses n/2 (floor) for the majority; both arms fail (disjoint even-n majorities appear, warning equivalence breaks). Pure arithmetic, no engine struct. CBMC 6.9.0, ~1 s each. --- test/cbmc/README.md | 1 + test/cbmc/harness_majority.c | 129 +++++++++++++++++++++++++++++++++++ test/cbmc/run.sh | 7 ++ 3 files changed, 137 insertions(+) create mode 100644 test/cbmc/harness_majority.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index bb90dae0ac..fd4f48c666 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -57,6 +57,7 @@ isolate one assertion). | `harness_dd_find.c` | `lock/lock_deadlock.c` `__dd_find` (waits-for bitmap cycle detection) | no OOB on the `nlockers×nalloc` bitmap matrix or deadlist; termination; deadlist entries point into the matrix and are NULL-terminated | 4 lockers, `--unwind 6` + `--unwinding-assertions` | <1 s | SUCCESSFUL | | `harness_cmpvote.c` | `rep/rep_elect.c` `__rep_cmp_vote` (election winner comparator) | **(b)** a priority-0 non-`REPCTL_ELECTABLE` vote never wins; **(c)** if any non-zero-priority vote is present the winner has non-zero priority; **(d)** among like-priority votes at the **same data_gen**, the winner maximises (LSN, priority, tiebreaker) and is order-independent. `-DCMPVOTE_SABOTAGE` swaps `LOG_COMPARE`'s order arms and must FAIL (d) | 3 votes, all fields nondet (loop-free) | ~2 s | SUCCESSFUL. **(a) order independence does NOT hold — see FINDING below** | | `harness_tally.c` | `rep/rep_elect.c` `__rep_tally` (per-election vote tally in the region) | each eid counted at most once; a lower/equal egen for a seen eid returns `DB_REP_IGNORE` with no count change, a higher egen updates in place with no count change; `*countp` == number of distinct eids and never exceeds capacity; no OOB on the tally array. `-DTALLY_SABOTAGE` turns the "seen this eid" test from `==` to `!=` (double-count) and must FAIL | tally CAP 5, ≤ 6 votes, 5 eids, egen ≤ 2, `--unwind 8` | ~1 s | SUCCESSFUL | +| `harness_majority.c` | `rep/rep_elect.c` `ELECTION_MAJORITY` (rep.h:534) + the `ack <= nsites/2` sub-majority warning in `__rep_elect_int` | **(1)** `2*majority > nsites` so any two majorities intersect (also proved constructively: two majorities of N=8 share a member); **(2)** the warning test `ack <= nsites/2` is exactly `ack < ELECTION_MAJORITY(nsites)`. `-DMAJORITY_SABOTAGE` uses `n/2` (floor) and must FAIL both | nsites 1–64, ack 0–64, constructive N=8 | ~1 s | SUCCESSFUL | | `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | SUCCESSFUL. Found a real bug (below), fixed in `2ca81268a`; `-DHPAGE_PTYPE_SABOTAGE` restores the bug and must FAIL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION diff --git a/test/cbmc/harness_majority.c b/test/cbmc/harness_majority.c new file mode 100644 index 0000000000..0ccbdb48ae --- /dev/null +++ b/test/cbmc/harness_majority.c @@ -0,0 +1,129 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness H3: election quorum arithmetic. + * + * ELECTION_MAJORITY(n) (src/dbinc/rep.h:534) is the vote count a candidate + * must collect to win a generation. The one-master-per-generation safety + * argument rests on two facts about it, which we prove for every group size + * nsites in [1, 64]: + * + * (1) MAJORITY INTERSECTION: any two vote sets of size >= majority, drawn + * from the same n sites, share at least one site. Two distinct + * candidates therefore cannot each collect a majority of VOTE2s, so no + * two masters are elected in one generation. By inclusion-exclusion, + * |A n B| >= |A| + |B| - n, so it is enough that 2*maj - n >= 1, i.e. + * 2*maj > n. We prove 2*ELECTION_MAJORITY(n) > n directly, AND prove + * the underlying set fact constructively: two nondeterministic subsets + * of [0,n) each of size >= maj must intersect (checked by CBMC over a + * nondeterministic membership bitmap). + * + * (2) SUB-MAJORITY WARNING: __rep_elect_int warns when the requested ack + * count is sub-majority, using the test `ack <= nsites/2`. We prove + * this is exactly equivalent to `ack < ELECTION_MAJORITY(nsites)` for + * every nsites and every ack in [0, 64]. (If they ever diverged, the + * warning would fire on a true majority or stay silent on a true + * sub-majority.) + * + * Everything here is pure integer arithmetic (no engine struct, no I/O), so + * the harness is loop-free except for the small constructive intersection + * loop over N sites. + * + * Bound: nsites in [1, 64]; ack in [0, 64]; constructive intersection over + * N = 8 sites (enough to exhibit the pigeonhole; the arithmetic proof + * covers 1..64 with no bound on the set representation). + */ + +#include + +typedef uint32_t u_int32_t; + +/* --- VERBATIM from src/dbinc/rep.h:534 --- */ +#define ELECTION_MAJORITY(n) (((n) / 2) + 1) + +/* + * SABOTAGE: the classic off-by-one, majority = n/2 (floor) instead of n/2+1. + * For even n (e.g. n=4, maj=2) two disjoint sets of size 2 then exist, so the + * intersection property FAILS; and the warning equivalence breaks too. + */ +#ifdef MAJORITY_SABOTAGE +#undef ELECTION_MAJORITY +#define ELECTION_MAJORITY(n) ((n) / 2) +#endif + +u_int32_t nondet_u32(void); + +/* + * (1a) + (2): the arithmetic identities, over all nsites in [1,64] and all + * ack in [0,64]. + */ +void harness_arith(void) +{ + u_int32_t nsites = nondet_u32(); + u_int32_t ack = nondet_u32(); + u_int32_t maj; + + __CPROVER_assume(nsites >= 1 && nsites <= 64); + __CPROVER_assume(ack <= 64); + + maj = ELECTION_MAJORITY(nsites); + + /* (1a) 2*maj > nsites => any two majorities must intersect. */ + __CPROVER_assert(2 * maj > nsites, + "two majorities of nsites always intersect (2*maj > nsites)"); + + /* maj is a real majority: strictly more than half, and <= nsites. */ + __CPROVER_assert(maj <= nsites, "a majority is at most the whole group"); + __CPROVER_assert(2 * maj > nsites, "a majority is strictly over half"); + + /* + * (2) the sub-majority warning test `ack <= nsites/2` is EXACTLY + * `ack < ELECTION_MAJORITY(nsites)`. + */ + __CPROVER_assert((ack <= nsites / 2) == (ack < maj), + "sub-majority warning (ack <= nsites/2) == (ack < majority)"); +} + +/* + * (1b) constructive intersection: two subsets A, B of [0,N) each with at least + * ELECTION_MAJORITY(N) members must share an index. Membership is a + * nondeterministic pair of bitmaps; CBMC searches for a disjoint pair and + * finds none. + */ +#define N 8 +void harness_intersect(void) +{ + int inA[N], inB[N]; + u_int32_t ca, cb, maj; + int i; + + maj = ELECTION_MAJORITY(N); + + ca = cb = 0; + for (i = 0; i < N; i++) { + inA[i] = nondet_u32() & 1; + inB[i] = nondet_u32() & 1; + if (inA[i]) + ca++; + if (inB[i]) + cb++; + } + __CPROVER_assume(ca >= maj); + __CPROVER_assume(cb >= maj); + + /* There is some i in both A and B. */ + { + int shared = 0; + for (i = 0; i < N; i++) + if (inA[i] && inB[i]) + shared = 1; + __CPROVER_assert(shared, + "two majorities of N sites share a member"); + } +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index fd8ef95c14..ec1e2fb1b8 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -53,6 +53,8 @@ run dd_find harness_dd_find.c harness --unwind 6 --unwinding-assertions run cmpvote harness_cmpvote.c harness # H1 (b,c): loop-free comparator run cmpvote-d harness_cmpvote.c harness_likepri # H1 (d): same-data_gen lex order run tally harness_tally.c harness --unwind 8 --unwinding-assertions # H2 tally array +run maj-arith harness_majority.c harness_arith --conversion-check # H3 quorum arithmetic +run maj-inter harness_majority.c harness_intersect --unwind 9 --unwinding-assertions # H3 intersection # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -97,6 +99,11 @@ sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ # H2: == -> != on the "seen this eid" test double-counts a site (OOB + count). sabotage tally-sab harness_tally.c harness -DTALLY_SABOTAGE \ --bounds-check --pointer-check --unwind 8 --unwinding-assertions +# H3: majority = n/2 (floor) instead of n/2+1 breaks intersection + warning. +sabotage maj-arith-sab harness_majority.c harness_arith -DMAJORITY_SABOTAGE \ + --bounds-check --pointer-check --conversion-check +sabotage maj-inter-sab harness_majority.c harness_intersect -DMAJORITY_SABOTAGE \ + --bounds-check --pointer-check --unwind 9 --unwinding-assertions # Every verbatim copy must still match src/. printf '=== %-14s ' "copies" From 5f95aab24efb1dbc2d6d5a5e5ca4dfcefb106b03 Mon Sep 17 00:00:00 2001 From: libdb agent Date: Wed, 4 Nov 2026 10:13:29 -0500 Subject: [PATCH 06/15] test/cbmc: H4 repmgr ack-policy durability decision (RFC 0025 C1) Models got_acks (src/repmgr/repmgr_net.c:1117) and the needed/quorum computation in __repmgr_send (the DB_REP_PERMANENT block). got_acks iterates db_rep->sites and dereferences REPMGR_SITE, so its decision logic (the accumulate loop + the switch (policy)) is transcribed faithfully into got_acks_model over the exact per-site facts it reads (SITE_PRESENT, SITE_HAS_PRIO, SITE_ELECTABLE, max_ack>=lsn), with the source lines named inline; the needed/quorum block is copied into compute_needed_quorum, likewise annotated. This is not a function boundary, so a verbatim #include/copy is not possible; the transcription is marked per the brief. Properties proved over all group shapes of <= 4 remote sites (+ master): - QUORUM "no election can lose it": durable => every electable-site majority (ELECTION_MAJORITY over master + electable peers) contains a holder (the master or an acked electable peer). The "every majority" quantifier is discharged by CBMC over a nondeterministic membership bitmap. - 2-site: STRICT => quorum 0 (master-only durable, the client won't self-elect); non-strict => the lone client must ack. Stated separately. - ALL_PEERS: durable => every electable peer acked (and no unknown-prio present site). - ONE_PEER: durable => some electable peer acked. - Shortcuts: needed==0 is durability-safe (reachable only when no electable peers exist, so the master is the whole majority); available nsites` so any two majorities intersect (also proved constructively: two majorities of N=8 share a member); **(2)** the warning test `ack <= nsites/2` is exactly `ack < ELECTION_MAJORITY(nsites)`. `-DMAJORITY_SABOTAGE` uses `n/2` (floor) and must FAIL both | nsites 1–64, ack 0–64, constructive N=8 | ~1 s | SUCCESSFUL | +| `harness_ackpolicy.c` | `repmgr/repmgr_net.c` `got_acks` (:1117) + the `needed`/`quorum` computation in `__repmgr_send` (DB_REP_PERMANENT block) | **QUORUM:** durable => no electable-site majority (`ELECTION_MAJORITY(total electable incl. master)`) avoids a holder (master or acked electable peer) — "no election can lose it". **2-site:** STRICT => quorum 0 (master-only durable); non-strict => the single client must ack. **ALL_PEERS:** durable => every electable peer acked. **ONE_PEER:** durable => some electable peer acked. **Shortcuts:** `needed==0` is durability-safe (only when no electable peers exist); `availablemembership == SITE_PRESENT (a current group member) + * - F_ISSET(site, SITE_HAS_PRIO) (we know its electability) + * - F_ISSET(site, SITE_ELECTABLE) (it can become master) + * - LOG_COMPARE(&site->max_ack, &perm->lsn) >= 0 (it acked this LSN) + * It accumulates sites_acked / peers_acked / has_unacked_peer exactly as the + * real loop does, then applies the exact `switch (policy)` to set is_durable. + * We copy that decision logic VERBATIM-IN-SHAPE into got_acks_model (the real + * function iterates db_rep->sites with FOR_EACH_REMOTE_SITE_INDEX and + * dereferences REPMGR_SITE, which drags in the whole repmgr subsystem; the + * per-site facts above are the only inputs the decision depends on). The + * source lines each branch comes from are named inline. + * + * The needed/quorum computation is copied from __repmgr_send into + * compute_needed_quorum, with the exact source lines named. + * + * Properties, over all group shapes of <= NREMOTE remote sites (master = site + * 0, always present / electable / holds the commit): + * + * QUORUM durability (the "no election can lose it" contract, source comment + * at repmgr_net.c ~line 494): if got_acks sets is_durable for QUORUM with + * the quorum __repmgr_send computed, then the commit cannot be lost in any + * election: every set of electable sites of size >= ELECTION_MAJORITY(total + * electable) contains a HOLDER (the master, or an acked electable remote + * site). Modelled for the normal (nclients>1 or STRICT) case, and + * separately for the 2-site special cases (strict vs non-strict), stating + * which guarantee each gives. + * + * ALL_PEERS: durable => every electable (present, known-prio) remote site + * acked. + * + * ONE_PEER: durable => at least one electable remote site acked. + * + * SHORTCUTS: the __repmgr_send fast paths never report durable when + * got_acks over the same sites would not. `needed == 0` => send returns + * success (durable) only when got_acks is also durable; `available < needed` + * => DB_REP_UNAVAIL, and in that case got_acks over the actual acks is also + * not durable. + * + * Bound: NREMOTE = 4 remote sites (+ master) = config_nsites up to 5; all + * per-site flags and ack states nondeterministic; electable-majority + * quantifier discharged by CBMC over a nondeterministic membership + * bitmap. Loop-free except the small per-site loops. + */ + +#include + +typedef uint32_t u_int32_t; +typedef unsigned int u_int; + +#define TRUE 1 +#define FALSE 0 + +/* --- ack policy codes, VERBATIM from src/dbinc/db.in:1067-1073 --- */ +#define DB_REPMGR_ACKS_ALL 1 +#define DB_REPMGR_ACKS_ALL_AVAILABLE 2 +#define DB_REPMGR_ACKS_ALL_PEERS 3 +#define DB_REPMGR_ACKS_NONE 4 +#define DB_REPMGR_ACKS_ONE 5 +#define DB_REPMGR_ACKS_ONE_PEER 6 +#define DB_REPMGR_ACKS_QUORUM 7 + +/* REP_C_2SITE_STRICT, VERBATIM from src/dbinc/rep.h:419. */ +#define REP_C_2SITE_STRICT 0x00001 + +/* ELECTION_MAJORITY, VERBATIM from src/dbinc/rep.h:534. */ +#define ELECTION_MAJORITY(n) (((n) / 2) + 1) + +#define NREMOTE 4 /* remote sites; master is a 5th site */ + +/* + * One remote site, with exactly the facts got_acks reads. "present" models + * membership == SITE_PRESENT; has_prio = F_ISSET(SITE_HAS_PRIO); electable = + * F_ISSET(SITE_ELECTABLE); acked = LOG_COMPARE(max_ack, lsn) >= 0. + */ +struct site { + int present; + int has_prio; + int electable; + int acked; +}; + +/* + * got_acks' decision, with the per-site facts pre-extracted. This is a + * faithful transcription of got_acks (src/repmgr/repmgr_net.c:1117): the + * accumulation loop (lines 1133-1156) and the `switch (policy)` (lines + * 1160-1178). Returns is_durable (perm->is_durable), and writes + * sites_acked / peers_acked / has_unacked_peer through the out-params. + */ +static int +got_acks_model(const struct site *s, int n, int policy, + u_int threshold, u_int quorum, + u_int *sites_acked_o, u_int *peers_acked_o, int *has_unacked_peer_o) +{ + u_int sites_acked, peers_acked; + int has_unacked_peer, is_perm, i; + + sites_acked = peers_acked = 0; + has_unacked_peer = FALSE; + /* FOR_EACH_REMOTE_SITE_INDEX(eid) { ... } (lines 1133-1156) */ + for (i = 0; i < n; i++) { + if (!s[i].present) /* != SITE_PRESENT */ + continue; + if (!s[i].has_prio) { + /* Never connected: assume the worst. */ + has_unacked_peer = TRUE; + continue; + } + if (s[i].acked) { /* LOG_COMPARE >= 0 */ + sites_acked++; +#ifdef ACKPOLICY_SABOTAGE + /* + * SABOTAGE: count EVERY acked site as a peer, dropping + * the electability test. peers_acked is then inflated by + * non-electable acks, so QUORUM declares a commit durable + * that a majority of ELECTABLE sites could still lose -- + * the contract (harness_quorum) must FAIL. + */ + peers_acked++; +#else + if (s[i].electable) + peers_acked++; +#endif + } else { + if (s[i].electable) + has_unacked_peer = TRUE; + } + } + + switch (policy) { /* lines 1160-1178 */ + case DB_REPMGR_ACKS_ALL: + case DB_REPMGR_ACKS_ONE: + is_perm = (sites_acked >= threshold); + break; + case DB_REPMGR_ACKS_ONE_PEER: + is_perm = (peers_acked >= threshold); + break; + case DB_REPMGR_ACKS_QUORUM: + case DB_REPMGR_ACKS_ALL_AVAILABLE: + is_perm = (peers_acked >= quorum) || !has_unacked_peer; + break; + case DB_REPMGR_ACKS_ALL_PEERS: + is_perm = !has_unacked_peer; + break; + default: + is_perm = FALSE; + } + *sites_acked_o = sites_acked; + *peers_acked_o = peers_acked; + *has_unacked_peer_o = has_unacked_peer; + return (is_perm); +} + +/* + * The needed/quorum computation copied from __repmgr_send + * (src/repmgr/repmgr_net.c, DB_REP_PERMANENT block). Covers the non-GMDB + * (active_gmdb_update == none) path for QUORUM / ONE_PEER / ALL_PEERS / + * ONE / ALL. nclients = config_nsites - 1 (line ~405); quorum is the + * QUORUM/ALL_AVAILABLE computation at lines ~464-490; needed/available at the + * per-policy cases. Returns needed; writes quorum and available out. + * `ret_unavail` is set when the ALL_AVAILABLE quorum-0 early-out fires (not + * used for the policies we model here). + */ +static u_int +compute_needed_quorum(int policy, u_int nclients, int strict, + u_int nsites_sent, u_int npeers_sent, int missed_peer, + u_int *quorum_o, u_int *available_o) +{ + u_int needed = 0, available = 0, quorum = 0; + + switch (policy) { + case DB_REPMGR_ACKS_ONE: /* line ~439 */ + needed = 1; + available = nsites_sent; + break; + case DB_REPMGR_ACKS_ALL: /* line ~444 */ + needed = nclients; + available = nsites_sent; + break; + case DB_REPMGR_ACKS_ONE_PEER: /* line ~450 */ + needed = 1; + available = npeers_sent; + break; + case DB_REPMGR_ACKS_ALL_PEERS: /* line ~455 */ + needed = 1; + available = npeers_sent; + break; + case DB_REPMGR_ACKS_QUORUM: /* line ~465 */ + /* nclients>1 || STRICT (|| gmdb_primary, not modelled) */ + if (nclients > 1 || strict) + quorum = nclients / 2; + else + quorum = nclients; + needed = quorum; + available = npeers_sent; + if (npeers_sent < quorum && !missed_peer) /* line ~530 */ + needed = npeers_sent; + break; + default: + needed = 0; + } + *quorum_o = quorum; + *available_o = available; + return (needed); +} + +int nondet_int(void); +u_int32_t nondet_u32(void); + +/* Fill NREMOTE nondeterministic remote sites. */ +static void +mk_sites(struct site *s) +{ + int i; + + for (i = 0; i < NREMOTE; i++) { + s[i].present = nondet_int() & 1; + s[i].has_prio = nondet_int() & 1; + s[i].electable = nondet_int() & 1; + s[i].acked = nondet_int() & 1; + } +} + +/* + * The "holders" of the commit = the master (always) plus every acked + * electable remote site. The electable sites = the master plus every + * electable remote site that is a present group member. (A site with + * !has_prio has unknown electability; got_acks treats it as a potential + * unacked peer, so for the safety argument we must count it as a possible + * electable non-holder too. We model has_prio sites as the electable set and + * require !has_unacked_peer to carry the !has_prio case, matching got_acks.) + * + * The contract: if durable, then every subset E of the electable sites with + * |E| >= ELECTION_MAJORITY(total_electable) contains a holder. We discharge + * the "every subset" quantifier by letting CBMC pick a nondeterministic + * electable majority that avoids all holders and asserting it cannot reach + * majority size. + */ +void harness_quorum(void) +{ + struct site s[NREMOTE]; + u_int sites_acked, peers_acked, quorum, needed, available; + int has_unacked_peer, is_durable, strict, i; + u_int nclients, total_electable, maj; + u_int32_t npeers_sent; + + mk_sites(s); + strict = nondet_int() & 1; + + /* nclients = config_nsites - 1 = number of remote sites that exist. */ + nclients = NREMOTE; + + /* Model the NORMAL quorum case: nclients > 1 or STRICT. */ + __CPROVER_assume(nclients > 1 || strict); + + /* + * npeers_sent (electable remote sites we sent to) -- for the durability + * contract we take the strongest adversary: we sent to all present + * electable peers, so missed_peer = FALSE and npeers_sent counts them. + * got_acks itself recomputes from the site table, so npeers_sent only + * feeds the quorum/needed math. + */ + npeers_sent = 0; + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable) + npeers_sent++; + + needed = compute_needed_quorum(DB_REPMGR_ACKS_QUORUM, nclients, strict, + /*nsites_sent*/npeers_sent, npeers_sent, /*missed_peer*/FALSE, + &quorum, &available); + (void)needed; (void)available; + + is_durable = got_acks_model(s, NREMOTE, DB_REPMGR_ACKS_QUORUM, + /*threshold*/needed, quorum, + &sites_acked, &peers_acked, &has_unacked_peer); + + /* total electable sites = master (1) + present electable remote sites + * with known prio. A !has_prio present site has unknown electability; + * got_acks' has_unacked_peer accounts for it, so when is_durable holds + * via the (peers_acked >= quorum) arm we must ALSO have no !has_prio + * present site that could be a hidden electable non-holder -- which is + * exactly what the !has_unacked_peer disjunct guarantees in the other + * arm. We therefore split on which arm made it durable. */ + total_electable = 1; /* master */ + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable) + total_electable++; + maj = ELECTION_MAJORITY(total_electable); + + if (!is_durable) + return; + + /* + * CONTRACT: pick a nondeterministic subset E of the electable sites + * (master + electable present remote peers) that contains NO holder + * (holder = master, or acked electable peer). Since the master is a + * holder, E must exclude the master. Assert |E| < maj: no holder-free + * electable set can reach a majority, so every majority has a holder. + */ + { + int inE_remote[NREMOTE]; + u_int esz = 0; /* |E|; master excluded (it's a holder) */ + + for (i = 0; i < NREMOTE; i++) { + inE_remote[i] = nondet_int() & 1; + if (inE_remote[i]) { + /* E members must be electable present peers... */ + __CPROVER_assume(s[i].present && s[i].has_prio && + s[i].electable); + /* ...and NON-holders: an acked electable peer is + * a holder, so exclude it. */ + __CPROVER_assume(!s[i].acked); + esz++; + } + } + /* + * If is_durable came via !has_unacked_peer, then there is NO + * present electable peer that is unacked AND no !has_prio + * present site, so no holder-free electable peer exists at all + * (esz == 0 < maj trivially). If it came via peers_acked >= + * quorum, the unacked electable peers number <= nclients - + * peers_acked, and 2*maj > total_electable bounds esz. CBMC + * checks the assertion for both. + */ + __CPROVER_assert(esz < maj, + "QUORUM durable => no electable majority avoids a holder"); + } +} + +/* ALL_PEERS: durable => every electable (present, known-prio) remote acked. */ +void harness_all_peers(void) +{ + struct site s[NREMOTE]; + u_int sites_acked, peers_acked; + int has_unacked_peer, is_durable, i; + + mk_sites(s); + is_durable = got_acks_model(s, NREMOTE, DB_REPMGR_ACKS_ALL_PEERS, + /*threshold*/0, /*quorum*/0, + &sites_acked, &peers_acked, &has_unacked_peer); + if (!is_durable) + return; + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable) + __CPROVER_assert(s[i].acked, + "ALL_PEERS durable => every electable peer acked"); + /* Also: no present site with unknown electability (!has_prio). */ + for (i = 0; i < NREMOTE; i++) + if (s[i].present) + __CPROVER_assert(s[i].has_prio, + "ALL_PEERS durable => no present site of unknown prio"); +} + +/* ONE_PEER: durable => at least one electable remote site acked. */ +void harness_one_peer(void) +{ + struct site s[NREMOTE]; + u_int sites_acked, peers_acked, quorum, available, needed; + int has_unacked_peer, is_durable, i, found; + + mk_sites(s); + needed = compute_needed_quorum(DB_REPMGR_ACKS_ONE_PEER, NREMOTE, 0, + 0, 0, FALSE, &quorum, &available); + is_durable = got_acks_model(s, NREMOTE, DB_REPMGR_ACKS_ONE_PEER, + /*threshold*/needed, quorum, + &sites_acked, &peers_acked, &has_unacked_peer); + if (!is_durable) + return; + found = 0; + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable && s[i].acked) + found = 1; + __CPROVER_assert(found, + "ONE_PEER durable => some electable peer acked"); +} + +/* + * The 2-SITE special cases (master + one remote), stated separately per the + * brief. nclients == 1. compute_needed_quorum gives: + * - NON-strict: quorum = nclients = 1, so needed = 1 (unless npeers_sent < + * 1). The one client must ack for the commit to be durable. This is the + * "fudge" in the source comment: a 2-site non-strict client self-elects on + * losing the master, so to keep the quorum guarantee the client must have + * the txn. GUARANTEE: durable => the (sole electable) client acked. + * - STRICT: quorum = nclients/2 = 0, so needed = 0 => durable with ZERO + * client acks. The source says this is correct: in strict mode the lone + * client will NOT self-elect, so no election can lose the commit even if + * the client never received it (the master stays master). GUARANTEE: + * durable by the master alone; safe because no sub-majority election + * occurs. + */ +void harness_twosite(void) +{ + struct site s[NREMOTE]; + u_int sites_acked, peers_acked, quorum, needed, available; + int has_unacked_peer, is_durable, strict, i; + u_int nclients = 1; /* master + exactly one remote */ + u_int32_t npeers_sent; + + mk_sites(s); + strict = nondet_int() & 1; + + /* Exactly one remote site exists, present, electable, known prio. */ + __CPROVER_assume(s[0].present && s[0].has_prio && s[0].electable); + for (i = 1; i < NREMOTE; i++) + __CPROVER_assume(!s[i].present); + npeers_sent = 1; + + needed = compute_needed_quorum(DB_REPMGR_ACKS_QUORUM, nclients, strict, + npeers_sent, npeers_sent, /*missed_peer*/FALSE, &quorum, &available); + + if (strict) { + /* STRICT: quorum 0, needed 0 => durable by master alone. */ + __CPROVER_assert(quorum == 0 && needed == 0, + "2-site STRICT QUORUM needs 0 client acks (master-only durable)"); + } else { + /* NON-strict: quorum 1, needed 1 => the client must ack. */ + __CPROVER_assert(quorum == 1 && needed == 1, + "2-site non-strict QUORUM needs the single client to ack"); + is_durable = got_acks_model(s, NREMOTE, DB_REPMGR_ACKS_QUORUM, + needed, quorum, + &sites_acked, &peers_acked, &has_unacked_peer); + if (is_durable) + __CPROVER_assert(s[0].acked, + "2-site non-strict QUORUM durable => the client acked"); + } +} + +/* + * SHORTCUTS: the __repmgr_send fast paths must be sound against the QUORUM + * durability contract. For QUORUM, __repmgr_send does: + * if (needed == 0) goto out; // declares DURABLE without calling got_acks + * if (available < needed) UNAVAIL; // declares NOT durable + * else it waits and uses got_acks. + * + * The needed==0 path (reached only when npeers_sent < quorum && !missed_peer + * collapses needed to npeers_sent==0) declares durability WITHOUT any acks, so + * it must be sound on its own: npeers_sent==0 with missed_peer==FALSE means + * there are NO electable remote peers at all, so the master alone is the whole + * electable majority and holds the commit. We prove the contract holds for + * that path directly (no holder-free electable majority exists). + * + * The available 1 || strict); + + npeers_sent = 0; + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable) + npeers_sent++; + + needed = compute_needed_quorum(DB_REPMGR_ACKS_QUORUM, nclients, strict, + npeers_sent, npeers_sent, /*missed_peer*/FALSE, &quorum, &available); + + /* + * needed==0 (via the all-peers-sent collapse) => __repmgr_send declares + * durable without acks. This is reachable only when npeers_sent==0 with + * missed_peer FALSE, i.e. no electable remote peers exist. Then the + * electable set is just the master, the majority is 1, and the master + * (always a holder) is in every majority. Prove no holder-free + * electable majority exists. + */ + if (needed == 0) { + __CPROVER_assert(npeers_sent == 0, + "QUORUM needed==0 only when no electable peers were sent to"); + + total_electable = 1; /* master */ + for (i = 0; i < NREMOTE; i++) + if (s[i].present && s[i].has_prio && s[i].electable) + total_electable++; + maj = ELECTION_MAJORITY(total_electable); + + /* A holder-free electable set excludes the master (holder); it + * can hold only electable present peers. With npeers_sent==0 + * there are none, so its size is 0 < maj. */ + { + int inE[NREMOTE]; + u_int esz = 0; + + for (i = 0; i < NREMOTE; i++) { + inE[i] = nondet_int() & 1; + if (inE[i]) { + __CPROVER_assume(s[i].present && + s[i].has_prio && s[i].electable); + __CPROVER_assume(!s[i].acked); + esz++; + } + } + __CPROVER_assert(esz < maj, + "needed==0 shortcut is durability-safe (master is the whole majority)"); + } + return; + } + + /* + * available < needed => __repmgr_send returns DB_REP_UNAVAIL (declares + * NOT durable), which is always safe. Confirm got_acks over the current + * acks would also NOT be durable in this branch (so the refusal is not + * masking a genuinely-durable state we should have confirmed): with + * available = npeers_sent and needed = quorum, available < needed means + * peers_acked <= npeers_sent < quorum, and all peers present (missed_peer + * FALSE) so has_unacked_peer is driven by unacked electable peers / + * unknown-prio sites. + */ + is_durable = got_acks_model(s, NREMOTE, DB_REPMGR_ACKS_QUORUM, + needed, quorum, &sites_acked, &peers_acked, &has_unacked_peer); + if (available < needed) + __CPROVER_assert(!is_durable, + "available got_acks is also not durable (safe refusal)"); +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index ec1e2fb1b8..2cbfbc97df 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -55,6 +55,11 @@ run cmpvote-d harness_cmpvote.c harness_likepri # H1 run tally harness_tally.c harness --unwind 8 --unwinding-assertions # H2 tally array run maj-arith harness_majority.c harness_arith --conversion-check # H3 quorum arithmetic run maj-inter harness_majority.c harness_intersect --unwind 9 --unwinding-assertions # H3 intersection +run ack-quorum harness_ackpolicy.c harness_quorum --unwind 6 --unwinding-assertions # H4 QUORUM contract +run ack-allpeers harness_ackpolicy.c harness_all_peers --unwind 6 --unwinding-assertions # H4 ALL_PEERS +run ack-onepeer harness_ackpolicy.c harness_one_peer --unwind 6 --unwinding-assertions # H4 ONE_PEER +run ack-2site harness_ackpolicy.c harness_twosite --unwind 6 --unwinding-assertions # H4 2-site cases +run ack-shortcut harness_ackpolicy.c harness_shortcut --unwind 6 --unwinding-assertions # H4 send shortcuts # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -104,6 +109,11 @@ sabotage maj-arith-sab harness_majority.c harness_arith -DMAJORITY_SABOTAGE \ --bounds-check --pointer-check --conversion-check sabotage maj-inter-sab harness_majority.c harness_intersect -DMAJORITY_SABOTAGE \ --bounds-check --pointer-check --unwind 9 --unwinding-assertions +# H4: counting non-electable acks as peers over-reports QUORUM durability. +sabotage ack-quorum-sab harness_ackpolicy.c harness_quorum -DACKPOLICY_SABOTAGE \ + --bounds-check --pointer-check --unwind 6 --unwinding-assertions +sabotage ack-onepeer-sab harness_ackpolicy.c harness_one_peer -DACKPOLICY_SABOTAGE \ + --bounds-check --pointer-check --unwind 6 --unwinding-assertions # Every verbatim copy must still match src/. printf '=== %-14s ' "copies" From 64d825774644693f08b735300af59b9d3565903a Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 10:46:08 -0500 Subject: [PATCH 07/15] test/cbmc: B1 __bam_defdecompress bounds -- finds a real over-read (RFC 0025 C2) harness_bt_decompress.c proves the memory safety of the default compressed btree key/data decoder over every input in a stated bound. The REAL, unmodified engine code (verbatim copy, guarded by check_copies.sh) FAILS: __bam_defdecompress reads each varint's leading byte via __db_decompress_count_int, and the magic byte *s at offset 0, BEFORE it checks the compressed buffer is long enough. A corrupt or truncated compressed item -- a trust boundary, since compressed pages come from disk -- over-reads up to one byte past compressed->size at each of the three varint sites, and reads the first byte of a zero-length item with no check at all. CBMC counterexample (size==0 the cheapest): *s and the count_int lookahead read "pointer outside object bounds". run.sh runs two arms: b1-fixed (-DB1_FIXED, the proposed bound-before-read fix) VERIFIES; b1-decompress (the unmodified engine code) is a must-FAIL arm that documents the live bug until fix/bt-decompress-bounds lands, mirroring how okitem ran before 2ca81268a. The whole suite stays ~26 s (cadical). The varint helpers' arithmetic is already proved against the real source by harness_varint.c; here they are modelled by their exact read footprint (the count reads buf[0]; the int32 reads the leading width bytes from the real __db_marshaled_int_size table), which is the only thing B1's bounds proof depends on and keeps the SAT formula inside the suite budget. --- test/cbmc/README.md | 75 ++++++ test/cbmc/harness_bt_decompress.c | 435 ++++++++++++++++++++++++++++++ test/cbmc/run.sh | 21 +- 3 files changed, 528 insertions(+), 3 deletions(-) create mode 100644 test/cbmc/harness_bt_decompress.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 23b6b5d860..523b80e2d7 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -60,6 +60,7 @@ isolate one assertion). | `harness_majority.c` | `rep/rep_elect.c` `ELECTION_MAJORITY` (rep.h:534) + the `ack <= nsites/2` sub-majority warning in `__rep_elect_int` | **(1)** `2*majority > nsites` so any two majorities intersect (also proved constructively: two majorities of N=8 share a member); **(2)** the warning test `ack <= nsites/2` is exactly `ack < ELECTION_MAJORITY(nsites)`. `-DMAJORITY_SABOTAGE` uses `n/2` (floor) and must FAIL both | nsites 1–64, ack 0–64, constructive N=8 | ~1 s | SUCCESSFUL | | `harness_ackpolicy.c` | `repmgr/repmgr_net.c` `got_acks` (:1117) + the `needed`/`quorum` computation in `__repmgr_send` (DB_REP_PERMANENT block) | **QUORUM:** durable => no electable-site majority (`ELECTION_MAJORITY(total electable incl. master)`) avoids a holder (master or acked electable peer) — "no election can lose it". **2-site:** STRICT => quorum 0 (master-only durable); non-strict => the single client must ack. **ALL_PEERS:** durable => every electable peer acked. **ONE_PEER:** durable => some electable peer acked. **Shortcuts:** `needed==0` is durability-safe (only when no electable peers exist); `availabledata[0..size)` nor `prevKey`/`prevData`, never writes past `destKey->ulen`/`destData->ulen`, for ANY input bytes | compressed ≤ 16, prev ≤ 8, dest ulen ≤ 16 (loop-free) | ~2 s | **BUG FOUND (below).** The real code FAILS (over-read); `-DB1_FIXED` builds the fix and VERIFIES. `run.sh` runs the real code as a must-FAIL arm (`b1-decompress`) until the engine fix lands | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION SUCCESSFUL`) and with `-DHPAGE_PTYPE_SABOTAGE`, which restores the pre-fix @@ -181,6 +182,80 @@ fix would warrant an LTS backport. Flagged to the lead; left as a documented finding here because it does not threaten the one-master-per-generation invariant. +## BUG FOUND (fix branch `fix/bt-decompress-bounds`) — `__bam_defdecompress` over-reads a truncated compressed item + +`harness_bt_decompress.c` on the **unmodified** engine code produces a +counterexample (`VERIFICATION FAILED`). It is a **real out-of-bounds read** on +hostile input: a compressed B-tree page comes from disk, so a corrupt or +truncated compressed key/data item reaches `__bam_defdecompress` +(`src/btree/bt_compress.c:483`). + +### Root cause + +The decoder reads each varint — and the leading magic byte — **before** it +checks the compressed buffer is long enough: + +```c +s = (u_int8_t*)compressed->data; +if (*s == CMP_INT_SPARE_VAL) { /* (1) reads s[0] with NO size check */ + ++s; size = 1; + size += __db_decompress_count_int(s); /* (2) reads s[0] (= data[1]) */ + if (size > compressed->size) /* ... the check is AFTER */ + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + ... +``` + +`__db_decompress_count_int(buf)` returns `__db_marshaled_int_size[buf[0]]` — it +dereferences `buf[0]`. Both call sites (the duplicate path and the +non-duplicate path) call it, then test `size > compressed->size`, so the +lookahead byte is read one step before the bound that would have rejected it. +And `*s` at the very top is read with no check at all, so a **zero-length** +compressed item (`compressed->size == 0`) over-reads immediately. + +The subsequent `__db_decompress_int32` reads *are* covered by the preceding +`size > compressed->size` check (the offset bookkeeping in `size` matches `s`), +so the over-read is exactly the `count_int` lookahead byte and the `*s` magic +byte — up to one byte past `compressed->size` at each of the three varint +sites, and the first byte of an empty buffer. + +### Minimal reproducer (CBMC counterexample) + +The cheapest counterexample is `compressed->size == 0`: `*s` reads +`compressed->data[0]`, one byte past a zero-length object. A one-byte item +whose leading byte is a multi-byte varint tag trips the `count_int` lookahead +at the second varint. CBMC reports two genuine failures on the real code: +`__bam_defdecompress … *s: pointer outside object bounds` and +`varint … buf[0]: pointer outside object bounds`. + +### The fix (on `fix/bt-decompress-bounds`, built here as `-DB1_FIXED`) + +Check that the next byte index is still inside `compressed->size` **before** +every `__db_decompress_count_int`, and that `compressed->size >= 1` before the +magic `*s`. `harness_bt_decompress.c -DB1_FIXED` builds this variant and +VERIFIES (no over-read, no over-write) over the whole input space. + +### How this harness runs + +`run.sh` runs two arms: + +* `b1-fixed` — the `-DB1_FIXED` variant — must VERIFY. +* `b1-decompress` — the **unmodified engine code** — is registered as a + must-FAIL arm (like `okitem` before `2ca81268a`): it documents the live bug + and keeps the harness honest. When `fix/bt-decompress-bounds` lands on + master, flip this arm to a normal `run` (verify) and drop `-DB1_FIXED`. + +### Modelling note (varint helpers) + +The harness models `__db_decompress_count_int` / `__db_decompress_int32` by +their exact **read footprint** (the count reads `buf[0]`; the int32 reads the +leading `width` bytes, `width` from the real `__db_marshaled_int_size` table), +rather than `#include`-ing `db_compint.c`. The helpers' arithmetic is already +proved against the real source by `harness_varint.c`; re-exploring it here +blows the SAT formula past the suite's 5-minute budget, and the property B1 +proves depends only on *which bytes* the helpers touch, which the models +reproduce faithfully. + ## BUG FOUND (fixed in `2ca81268a`) — `__db_ret_okitem` hash-offpage guard read the wrong byte `harness_okitem.c` on the **unmodified** engine code produces a diff --git a/test/cbmc/harness_bt_decompress.c b/test/cbmc/harness_bt_decompress.c new file mode 100644 index 0000000000..90ec2d27fd --- /dev/null +++ b/test/cbmc/harness_bt_decompress.c @@ -0,0 +1,435 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness: __bam_defdecompress (src/btree/bt_compress.c) -- the default + * btree compressed-key/data decoder. (RFC 0025 target B1.) + * + * A compressed btree's pages are a TRUST BOUNDARY: they come from disk, so a + * corrupt or hostile file reaches this decoder. It must never read outside + * the compressed buffer [compressed->data, compressed->data + compressed->size) + * nor outside prevKey->data / prevData->data, and never write past + * destKey->ulen / destData->ulen. + * + * SAFETY PROPERTY (checked by CBMC's --bounds-check + --pointer-check): + * for ANY compressed bytes of size 0..COMPMAX, ANY prevKey/prevData of + * size 0..PREVMAX, and dest buffers with nondet ulen 0..DESTMAX, no read + * or write ever leaves its object. + * + * Each buffer is allocated at EXACTLY its claimed size (malloc(size)), so any + * byte read past compressed->size -- or past prevKey/prevData->size, or any + * byte written past dest ulen -- is an out-of-object access CBMC reports. + * + * What is modelled / stubbed: + * - DBT / DB structs: mirror src/dbinc/db.in (only the fields the function + * touches: data, size, ulen). + * - COMPQUIET: a no-op, as in db_int.h. + * - the varint decoders __db_decompress_count_int / __db_decompress_int32. + * Their full arithmetic (the 256-entry size table, the 9-way byte + * shuffle) is proved separately by harness_varint.c against the REAL + * src/common/db_compint.c -- re-exploring it here blows the SAT formula + * past the 5-minute suite budget. What matters for THIS proof is the + * memory footprint each helper touches, so the models below read + * EXACTLY the real bytes: __db_decompress_count_int reads buf[0] and + * returns a width 1..9; __db_decompress_int32 reads buf[0..width-1] and + * returns width. The over-read B1 proves is precisely that + * __bam_defdecompress calls these BEFORE checking the buffer is long + * enough, so faithfully reproducing their read span is what the proof + * needs. (The widths come from the real size table, abstracted to a + * nondet 1..9, which is a superset of the real behaviour.) + * + * The decoder body is copied VERBATIM from src/btree/bt_compress.c between the + * BEGIN/END markers below (guarded by check_copies.sh). + * + * Bound: compressed <= COMPMAX (16) bytes, prevKey/prevData <= PREVMAX (8) + * bytes, dest ulen <= DESTMAX (16). The function is loop-free. + * + * =========================================================================== + * REAL BUG (expected): __bam_defdecompress reads each varint's first byte via + * __db_decompress_count_int(s) BEFORE checking size > compressed->size, + * and reads *s (the magic byte) with no size check at all when size == 0. + * On a truncated/corrupt compressed item this over-reads past + * compressed->size. The harness proves it (VERIFICATION FAILED on the real + * code); -DB1_FIXED builds the fixed variant that verifies. See README.md + * "BUG FOUND". + * =========================================================================== + */ + +#include +#include +#include + +typedef uint8_t u_int8_t; +typedef uint16_t u_int16_t; +typedef uint32_t u_int32_t; +typedef uint64_t u_int64_t; +typedef uint32_t db_pgno_t; + +#define EINVAL 22 +#define DB_BUFFER_SMALL (-30999) + +/* CMP_INT_SPARE_VAL: db_int.h value (the duplicate-value magic byte). */ +#define CMP_INT_SPARE_VAL 0xFC + +#define COMPQUIET(x, v) do { (x) = (v); } while (0) + +/* DBT: only the fields __bam_defdecompress touches, at the real layout. */ +typedef struct __db_dbt { + void *data; + u_int32_t size; + u_int32_t ulen; + u_int32_t dlen; + u_int32_t doff; +} DBT; + +typedef struct __db { int unused; } DB; + +/* + * Varint read-footprint models. See the header comment: these read EXACTLY + * the bytes the real db_compint.c decoders read (buf[0] for the count; the + * leading `width` bytes for the int32), so CBMC sees the identical + * out-of-buffer accesses, while the real arithmetic is verified by + * harness_varint.c. The width is the REAL size table from db_compint.c + * (__db_marshaled_int_size), so count_int and int32 agree on the width for + * the same leading byte, exactly as the real code does. + */ +static const u_int8_t varint_size_tab[256] = { + 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, + 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, + 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, + 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, + 2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2, + 2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2, + 3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3, + 4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,4,5,5,5,5,5,5,5,5,6,7,8,9,0xFF,0xFF,0xFF,0xFF +}; + +static u_int32_t varint_width(const u_int8_t *buf) +{ + u_int8_t c = buf[0]; /* the real count_int reads buf[0] */ + u_int32_t w = varint_size_tab[c]; + /* 0xFF table entries are spare/magic bytes; the caller never reaches + * them on the non-magic paths, but clamp so the read loop is bounded. */ + if (w == 0xFF) + w = 1; + return (w); +} + +static u_int32_t __db_decompress_count_int(const u_int8_t *buf) +{ + return (varint_width(buf)); +} + +static int __db_decompress_int32(const u_int8_t *buf, u_int32_t *i) +{ + u_int32_t w = varint_width(buf); + u_int32_t k; + u_int32_t acc = 0; + /* The real int32 decoder reads the leading `w` bytes of buf. */ + for (k = 0; k < w; k++) + acc = (acc << 1) ^ buf[k]; + *i = acc; + return ((int)w); +} + +/* ------------------------------------------------------------------------ */ +#ifdef B1_FIXED +/* + * The proposed fix: check that the varint's declared width fits BEFORE + * reading its bytes, and that there is at least one byte before reading *s. + * This mirrors fix/bt-decompress-bounds. __db_decompress_count_int reads + * s[0] (one byte), so a safe pre-check is "the next byte index (size) is + * still < compressed->size" before each count_int, and compressed->size >= 1 + * before *s. + */ +static int +b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) + DB *dbp; + const DBT *prevKey, *prevData; + DBT *compressed, *destKey, *destData; +{ + u_int8_t *s, *d; + u_int32_t prefix, suffix, size; + + COMPQUIET(dbp, NULL); + + /* Need at least the magic/first byte. */ + if (compressed->size < 1) + return (EINVAL); + + s = (u_int8_t*)compressed->data; + if (*s == CMP_INT_SPARE_VAL) { + ++s; + size = 1; + + /* Before reading the count byte at offset `size`, it must be + * on-buffer. */ + if (size >= compressed->size) + return (EINVAL); + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + if (size >= compressed->size) + return (EINVAL); + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + destKey->size = prevKey->size; + destData->size = prefix + suffix; + if (destKey->size > destKey->ulen || + destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + memcpy(destKey->data, prevKey->data, destKey->size); + + if (prefix > prevData->size) + return (EINVAL); + d = (u_int8_t*)destData->data; + memcpy(d, prevData->data, prefix); + d += prefix; + + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); + } + + if (size >= compressed->size) + return (EINVAL); + size = __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + if (size >= compressed->size) + return (EINVAL); + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + if (size >= compressed->size) + return (EINVAL); + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &destData->size); + + destKey->size = prefix + suffix; + if (destKey->size > destKey->ulen || destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + if (prefix > prevKey->size) + return (EINVAL); + d = (u_int8_t*)destKey->data; + memcpy(d, prevKey->data, prefix); + d += prefix; + + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + size += destData->size; + if (size > compressed->size) + return (EINVAL); + memcpy(destData->data, s, destData->size); + s += destData->size; + + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); +} +#else +/* --- BEGIN verbatim copy of __bam_defdecompress from src/btree/bt_compress.c --- */ +int +__bam_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) + DB *dbp; + const DBT *prevKey, *prevData; + DBT *compressed, *destKey, *destData; +{ + u_int8_t *s, *d; + u_int32_t prefix, suffix, size; + + COMPQUIET(dbp, NULL); + + /* + * Check for the magic identifying byte, that tells us that this is a + * compressed duplicate value. + */ + s = (u_int8_t*)compressed->data; + if (*s == CMP_INT_SPARE_VAL) { + ++s; + size = 1; + + /* Unmarshal prefix and suffix */ + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + /* Check destination lengths */ + destKey->size = prevKey->size; + destData->size = prefix + suffix; + if (destKey->size > destKey->ulen || + destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + /* Write the key */ + memcpy(destKey->data, prevKey->data, destKey->size); + + /* Write the prefix */ + if (prefix > prevData->size) + return (EINVAL); + d = (u_int8_t*)destData->data; + memcpy(d, prevData->data, prefix); + d += prefix; + + /* Write the suffix */ + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + /* Return bytes read */ + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); + } + + /* Unmarshal prefix, suffix and data length */ + size = __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &destData->size); + + /* Check destination lengths */ + destKey->size = prefix + suffix; + if (destKey->size > destKey->ulen || destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + /* Write the prefix */ + if (prefix > prevKey->size) + return (EINVAL); + d = (u_int8_t*)destKey->data; + memcpy(d, prevKey->data, prefix); + d += prefix; + + /* Write the suffix */ + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + /* Write the data */ + size += destData->size; + if (size > compressed->size) + return (EINVAL); + memcpy(destData->data, s, destData->size); + s += destData->size; + + /* Return bytes read */ + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); +} +/* --- END verbatim copy --- */ +#endif /* B1_FIXED */ + +#define COMPMAX 16 +#define PREVMAX 8 +#define DESTMAX 16 + +u_int32_t nondet_u32(void); + +/* + * Allocate a buffer of EXACTLY `n` bytes. CBMC's malloc gives a fresh object + * of exactly n bytes whose contents are nondeterministic, so (a) we need no + * fill loop, and (b) any read of byte >= n -- including byte 0 of a 0-byte + * object, the size==0 case -- is an out-of-object access CBMC reports. We do + * NOT return NULL for n==0: a NULL dereference is a different (modelling) + * failure; we want the clean "read past compressed->size" over-read, so a + * 0-size-but-valid object is the faithful model of a truncated item. + */ +static u_int8_t *exact_buf(u_int32_t n) +{ + u_int8_t *p = malloc(n); + __CPROVER_assume(p != NULL); + return (p); +} + +void harness(void) +{ + DB db; + DBT prevKey, prevData, compressed, destKey, destData; + u_int32_t csize, pksize, pdsize, dkulen, ddulen; + + csize = nondet_u32(); + pksize = nondet_u32(); + pdsize = nondet_u32(); + dkulen = nondet_u32(); + ddulen = nondet_u32(); + __CPROVER_assume(csize <= COMPMAX); + __CPROVER_assume(pksize <= PREVMAX); + __CPROVER_assume(pdsize <= PREVMAX); + __CPROVER_assume(dkulen <= DESTMAX); + __CPROVER_assume(ddulen <= DESTMAX); + + compressed.data = exact_buf(csize); + compressed.size = csize; + compressed.ulen = csize; + + prevKey.data = exact_buf(pksize); + prevKey.size = pksize; + prevKey.ulen = pksize; + + prevData.data = exact_buf(pdsize); + prevData.size = pdsize; + prevData.ulen = pdsize; + + /* dest buffers are allocated at EXACTLY ulen; a write past ulen is an + * over-write CBMC reports. */ + destKey.data = exact_buf(dkulen); + destKey.size = 0; + destKey.ulen = dkulen; + + destData.data = exact_buf(ddulen); + destData.size = 0; + destData.ulen = ddulen; + +#ifdef B1_FIXED + (void)b1_fixed_defdecompress(&db, &prevKey, &prevData, + &compressed, &destKey, &destData); +#else + (void)__bam_defdecompress(&db, &prevKey, &prevData, + &compressed, &destKey, &destData); +#endif +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index 2cbfbc97df..980f96f8d6 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -21,6 +21,10 @@ CBMC=${CBMC:-cbmc} # to bytes (e.g. (u_int8_t)nondet_u32()) to fill buffers, which is not a # property under test. The varint harness enables it explicitly (see below). COMMON="--bounds-check --pointer-check" +# cadical is CBMC's fast built-in SAT backend. The decompress harness (B1) is +# far too slow on the default solver; the rest verify at least as fast on +# cadical, so the whole suite uses it. +SOLVER="--sat-solver cadical" FAIL=0 # run @@ -30,7 +34,7 @@ run() { local rc secs tmp tmp=$(mktemp) SECONDS=0 - "$CBMC" "$file" -Istubs --function "$func" $COMMON "$@" >"$tmp" 2>&1 + "$CBMC" "$file" -Istubs --function "$func" $COMMON $SOLVER "$@" >"$tmp" 2>&1 rc=$? secs=$SECONDS if grep -q "VERIFICATION SUCCESSFUL" "$tmp"; then @@ -70,7 +74,7 @@ printf '=== %-14s ' "okitem" SECONDS=0 tmp=$(mktemp) "$CBMC" harness_okitem.c -Istubs --function harness \ - --bounds-check --no-pointer-check --unwind 65 >"$tmp" 2>&1 + --bounds-check --no-pointer-check $SOLVER --unwind 65 >"$tmp" 2>&1 secs=$SECONDS if grep -q "VERIFICATION SUCCESSFUL" "$tmp"; then printf 'PASS (%ss)\n' "$secs" @@ -79,6 +83,9 @@ else fi rm -f "$tmp" +# B1 decompress: the FIXED variant verifies (no over-read / over-write). +run b1-fixed harness_bt_decompress.c harness -DB1_FIXED --unwind 10 + # Sabotage arms: each plants a real bug shape and MUST fail. A sabotage arm # that verifies means its harness has no teeth. # sabotage @@ -86,7 +93,7 @@ sabotage() { local name=$1 file=$2 func=$3; shift 3 printf '=== %-14s ' "$name" local tmp; tmp=$(mktemp); SECONDS=0 - "$CBMC" "$file" -Istubs --function "$func" "$@" >"$tmp" 2>&1 + "$CBMC" "$file" -Istubs --function "$func" $SOLVER "$@" >"$tmp" 2>&1 if grep -q "VERIFICATION FAILED" "$tmp"; then printf 'FAIL as required (%ss)\n' "$SECONDS" else @@ -98,6 +105,14 @@ sabotage() { # The pre-2ca81268a HPAGE_PTYPE (no parentheses): the real bug okitem found. sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ --bounds-check --no-pointer-check --unwind 65 +# B1: the REAL __bam_defdecompress over-reads the compressed buffer -- it reads +# each varint's leading byte, and the magic byte at offset 0, BEFORE checking +# the buffer is long enough. This arm runs the UNMODIFIED engine code and MUST +# FAIL (the live bug); fix/bt-decompress-bounds carries the fix + a failing- +# first test/db runner. When that fix lands, flip this to a normal `run` and +# drop -DB1_FIXED. See README.md "BUG FOUND". +sabotage b1-decompress harness_bt_decompress.c harness \ + --bounds-check --pointer-check --unwind 10 # H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ --bounds-check --pointer-check From 010b1773302c6c729d2359681a72d22a8e38f05b Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 10:48:02 -0500 Subject: [PATCH 08/15] test/cbmc: align B1_FIXED non-dup path with the engine fix (RFC 0025 C2) The -DB1_FIXED variant's first non-dup count_int check read an uninitialised `size`; drop it, since the top `compressed->size < 1` guard already covers the offset-0 read, matching fix/bt-decompress-bounds exactly. Still VERIFIES. --- test/cbmc/harness_bt_decompress.c | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/test/cbmc/harness_bt_decompress.c b/test/cbmc/harness_bt_decompress.c index 90ec2d27fd..c56e4f941e 100644 --- a/test/cbmc/harness_bt_decompress.c +++ b/test/cbmc/harness_bt_decompress.c @@ -207,8 +207,7 @@ b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) return (0); } - if (size >= compressed->size) - return (EINVAL); + /* s[0] is covered by the compressed->size >= 1 check at the top. */ size = __db_decompress_count_int(s); if (size > compressed->size) return (EINVAL); From 20327b543f1a204c3a92f87ebd6e9e4d2630b10e Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 11:13:20 -0500 Subject: [PATCH 09/15] test/cbmc: Q1 queue record arithmetic (RFC 0025 C2) harness_qam_recno.c verifies the qam.h record<->(page,index) mapping and the circular live-window predicates over the whole u_int32_t range. MAP: recno>=1 gives an in-range index that maps back to recno. RANGE: QAM_OUTSIDE_QUEUE agrees with an independent circular-window reference, including the wrapped queue (cur < first). PARTITION: for recno != RECNO_OOB exactly one of before-first / after-current / inside holds, and QAM_NOT_VALID == before || after. The macros are verbatim from qam.h (member access adapted to local structs). No engine finding -- the macros agree with the reference. -DQAM_SABOTAGE drops the 1-based "- 1" in QAM_RECNO_INDEX and must FAIL. --- test/cbmc/README.md | 1 + test/cbmc/harness_qam_recno.c | 198 ++++++++++++++++++++++++++++++++++ test/cbmc/run.sh | 5 + 3 files changed, 204 insertions(+) create mode 100644 test/cbmc/harness_qam_recno.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 523b80e2d7..092c381f93 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -61,6 +61,7 @@ isolate one assertion). | `harness_ackpolicy.c` | `repmgr/repmgr_net.c` `got_acks` (:1117) + the `needed`/`quorum` computation in `__repmgr_send` (DB_REP_PERMANENT block) | **QUORUM:** durable => no electable-site majority (`ELECTION_MAJORITY(total electable incl. master)`) avoids a holder (master or acked electable peer) — "no election can lose it". **2-site:** STRICT => quorum 0 (master-only durable); non-strict => the single client must ack. **ALL_PEERS:** durable => every electable peer acked. **ONE_PEER:** durable => some electable peer acked. **Shortcuts:** `needed==0` is durability-safe (only when no electable peers exist); `availabledata[0..size)` nor `prevKey`/`prevData`, never writes past `destKey->ulen`/`destData->ulen`, for ANY input bytes | compressed ≤ 16, prev ≤ 8, dest ulen ≤ 16 (loop-free) | ~2 s | **BUG FOUND (below).** The real code FAILS (over-read); `-DB1_FIXED` builds the fix and VERIFIES. `run.sh` runs the real code as a must-FAIL arm (`b1-decompress`) until the engine fix lands | +| `harness_qam_recno.c` | `dbinc/qam.h` `QAM_RECNO_PAGE` / `QAM_RECNO_INDEX` / `QAM_OUTSIDE_QUEUE` / `QAM_BEFORE_FIRST` / `QAM_AFTER_CURRENT` / `QAM_NOT_VALID` | **MAP:** for recno ≥ 1, `QAM_RECNO_INDEX(QAM_RECNO_PAGE(r)) < rec_page` and `(page,index)` maps back to `r`. **RANGE:** the macros agree with an independent circular-window reference, incl. the wrapped queue (`cur < first`). **PARTITION:** for recno ≠ RECNO_OOB, exactly one of before-first / after-current / inside holds; `QAM_NOT_VALID == before \|\| after`. `-DQAM_SABOTAGE` drops the 1-based `- 1` in `QAM_RECNO_INDEX` and must FAIL | full `u_int32_t` recno/first/cur/q_root; rec_page 1..8 (loop-free) | ~1 s | SUCCESSFUL (macros agree with the reference; no bug) | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION SUCCESSFUL`) and with `-DHPAGE_PTYPE_SABOTAGE`, which restores the pre-fix diff --git a/test/cbmc/harness_qam_recno.c b/test/cbmc/harness_qam_recno.c new file mode 100644 index 0000000000..1152e0a1e8 --- /dev/null +++ b/test/cbmc/harness_qam_recno.c @@ -0,0 +1,198 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness: queue record arithmetic (src/dbinc/qam.h). (RFC 0025 Q1.) + * + * The queue access method is a circular log of fixed-length records numbered + * by a 32-bit db_recno_t (RECNO_OOB == 0 is reserved). A handful of macros in + * qam.h do all the record<->(page,index) mapping and the "is this record in + * the live window [first_recno, cur_recno)" tests, as plain u_int32_t + * arithmetic that must stay correct even when the queue has WRAPPED around the + * 32-bit space (cur_recno < first_recno). Queue wrap-around has had bugs. + * + * We verify (over the whole 32-bit range, loop-free): + * + * MAP: for recno >= 1 and rec_page >= 1, + * QAM_RECNO_INDEX(QAM_RECNO_PAGE(recno)) < rec_page, and the + * (page, index) pair maps back to recno. No OOB, no div-by-zero (the + * harness constrains rec_page >= 1, which the engine guarantees: + * CALC_QAM_RECNO_PER_PAGE is >= 1 for any sane page/record size). + * + * RANGE: QAM_OUTSIDE_QUEUE / QAM_BEFORE_FIRST / QAM_AFTER_CURRENT agree with + * an INDEPENDENT reference for "recno is in the circular live window", + * including the wrapped case (cur < first). + * + * PARTITION: for any recno != RECNO_OOB, exactly one of {before-first, + * after-current, inside} holds (QAM_NOT_VALID == before || after). + * + * The macros below are copied VERBATIM from src/dbinc/qam.h (only the struct + * member access is adapted to the local Q struct, which mirrors the QUEUE / + * QMETA fields the macros read: q_root, rec_page, cur_recno, first_recno). + * The arithmetic -- the subtractions, the (recno-1)/per_page, the circular + * comparisons -- is byte-for-byte the shipped code. + * + * Bound: full u_int32_t for recno/first/cur/q_root; rec_page in 1..REC_PAGE_MAX + * (8). Loop-free. + */ + +#include + +typedef uint32_t u_int32_t; +typedef uint32_t db_recno_t; +typedef uint32_t db_pgno_t; + +#define RECNO_OOB 0 + +/* + * Local stand-ins for the fields the qam.h macros read. QUEUE holds q_root + * and rec_page (records per page); META holds the window endpoints. + */ +typedef struct { + db_pgno_t q_root; + u_int32_t rec_page; +} Q; +typedef struct { + db_recno_t first_recno; + db_recno_t cur_recno; +} META; + +/* + * --- VERBATIM from src/dbinc/qam.h (member access adapted to Q/META) --- + * QAM_RECNO_PER_PAGE(dbp) -> q->rec_page + * QAM_RECNO_PAGE(dbp, recno) -> q->q_root + (recno-1)/rec_page + * QAM_RECNO_INDEX(dbp,pgno,r) -> (r-1) - rec_page*(pgno - q_root) + */ +#define QAM_RECNO_PER_PAGE(q) ((q)->rec_page) + +#define QAM_RECNO_PAGE(q, recno) \ + ((q)->q_root + (((recno) - 1) / QAM_RECNO_PER_PAGE(q))) + +#ifdef QAM_SABOTAGE +/* + * Planted bug: drop the 1-based "- 1" in the index computation. This is a + * realistic off-by-one (record numbers are 1-based); it breaks both the + * index-in-range bound and the (page,index)->recno round-trip. This arm + * MUST FAIL. + */ +#define QAM_RECNO_INDEX(q, pgno, recno) \ + (u_int32_t)(((recno)) - (QAM_RECNO_PER_PAGE(q) \ + * (pgno - (q)->q_root))) +#else +#define QAM_RECNO_INDEX(q, pgno, recno) \ + (u_int32_t)(((recno) - 1) - (QAM_RECNO_PER_PAGE(q) \ + * (pgno - (q)->q_root))) +#endif + +#define QAM_OUTSIDE_QUEUE(meta, recno) \ + (((meta)->cur_recno >= (meta)->first_recno ? \ + ((recno) < (meta)->first_recno || \ + (recno) > (meta)->cur_recno) : \ + ((recno) > (meta)->cur_recno && \ + (recno) < (meta)->first_recno))) + +#define QAM_AFTER_CURRENT(meta, recno) \ + ((recno) == (meta)->cur_recno || \ + (QAM_OUTSIDE_QUEUE(meta, recno) && \ + ((recno) - (meta)->cur_recno) <= ((meta)->first_recno - (recno)))) + +#define QAM_BEFORE_FIRST(meta, recno) \ + (QAM_OUTSIDE_QUEUE(meta, recno) && \ + ((meta)->first_recno - (recno)) < ((recno) - (meta)->cur_recno)) + +#define QAM_NOT_VALID(meta, recno) \ + (recno == RECNO_OOB || \ + QAM_BEFORE_FIRST(meta, recno) || QAM_AFTER_CURRENT(meta, recno)) +/* --- end verbatim macros --- */ + +#define REC_PAGE_MAX 8 + +u_int32_t nondet_u32(void); + +/* + * Independent reference for "recno is OUTSIDE the circular live window". + * The window the engine maintains is the records between first_recno and + * cur_recno in increasing circular order; cur_recno is the next slot to be + * written (exclusive), so the live records are first_recno..cur_recno-1. For + * the RANGE predicates we only need a reference for QAM_OUTSIDE_QUEUE, which + * the engine defines as "not between first and cur in circular order", with + * cur treated INCLUSIVELY (recno == cur is NOT outside; QAM_AFTER_CURRENT then + * treats recno == cur as the sentinel just-past-the-end). We mirror exactly + * that: not-outside iff recno lies in the closed circular span [first, cur]. + */ +static int ref_outside(const META *m, db_recno_t r) +{ + if (m->cur_recno >= m->first_recno) + return (r < m->first_recno || r > m->cur_recno); + /* wrapped: the live span is [first, MAX] U [1, cur]; outside is the + * gap strictly between cur and first. */ + return (r > m->cur_recno && r < m->first_recno); +} + +void harness(void) +{ + Q q; + META m; + db_recno_t recno; + + q.q_root = nondet_u32(); + q.rec_page = nondet_u32(); + recno = nondet_u32(); + m.first_recno = nondet_u32(); + m.cur_recno = nondet_u32(); + + /* rec_page is records-per-page: the engine's CALC_QAM_RECNO_PER_PAGE is + * always >= 1 (a page holds at least one record), and the macros divide + * by it, so model that invariant. */ + __CPROVER_assume(q.rec_page >= 1 && q.rec_page <= REC_PAGE_MAX); + + /* ---- MAP: recno >= 1 maps to (page, index) and back. ---- */ + { + db_recno_t r = recno; + /* A real record number is >= 1; bound q_root and r so the page + * arithmetic stays inside u_int32_t without wrap (the engine's + * q_root is 1 and page numbers are bounded by the file size; + * here we just keep (r-1)/rec_page + q_root from overflowing). */ + __CPROVER_assume(r >= 1 && r <= 0x10000); + __CPROVER_assume(q.q_root <= 0x10000); + + db_pgno_t pg = QAM_RECNO_PAGE(&q, r); + u_int32_t idx = QAM_RECNO_INDEX(&q, pg, r); + + __CPROVER_assert(idx < q.rec_page, + "QAM: record index is within records-per-page"); + /* (page, index) -> recno round-trip: the physical record number + * is rec_page*(pg - q_root) + idx, +1 for the 1-based recno. */ + u_int32_t back = + q.rec_page * (pg - q.q_root) + idx + 1; + __CPROVER_assert(back == r, + "QAM: (page,index) maps back to the record number"); + } + + /* ---- RANGE: the macros agree with the independent reference. ---- */ + __CPROVER_assert( + (QAM_OUTSIDE_QUEUE(&m, recno) ? 1 : 0) == + (ref_outside(&m, recno) ? 1 : 0), + "QAM_OUTSIDE_QUEUE matches the circular-window reference"); + + /* ---- PARTITION: for recno != OOB, exactly one of before/after/inside + * holds. "inside" == !outside (and recno != cur, since cur is the + * after-current sentinel). ---- */ + if (recno != RECNO_OOB) { + int before = QAM_BEFORE_FIRST(&m, recno) ? 1 : 0; + int after = QAM_AFTER_CURRENT(&m, recno) ? 1 : 0; + int inside = (!QAM_OUTSIDE_QUEUE(&m, recno) && + recno != m.cur_recno) ? 1 : 0; + __CPROVER_assert(before + after + inside == 1, + "QAM: exactly one of before-first / after-current / inside"); + /* QAM_NOT_VALID is precisely before || after (for recno != OOB). */ + __CPROVER_assert( + (QAM_NOT_VALID(&m, recno) ? 1 : 0) == (before || after ? 1 : 0), + "QAM_NOT_VALID == before-first || after-current"); + } +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index 980f96f8d6..ee10743e01 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -64,6 +64,7 @@ run ack-allpeers harness_ackpolicy.c harness_all_peers --unwind 6 --unwinding-as run ack-onepeer harness_ackpolicy.c harness_one_peer --unwind 6 --unwinding-assertions # H4 ONE_PEER run ack-2site harness_ackpolicy.c harness_twosite --unwind 6 --unwinding-assertions # H4 2-site cases run ack-shortcut harness_ackpolicy.c harness_shortcut --unwind 6 --unwinding-assertions # H4 send shortcuts +run qam-recno harness_qam_recno.c harness --conversion-check # Q1 queue record arithmetic # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -113,6 +114,10 @@ sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ # drop -DB1_FIXED. See README.md "BUG FOUND". sabotage b1-decompress harness_bt_decompress.c harness \ --bounds-check --pointer-check --unwind 10 +# Q1: dropping the 1-based "- 1" in QAM_RECNO_INDEX (an off-by-one) breaks the +# index-in-range bound and the (page,index)->recno round-trip. +sabotage qam-recno-sab harness_qam_recno.c harness -DQAM_SABOTAGE \ + --bounds-check --pointer-check --conversion-check # H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ --bounds-check --pointer-check From b82434466bddf8d80a47913cdadd852050bb3279 Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 11:19:30 -0500 Subject: [PATCH 10/15] test/cbmc: L1 log header check + E1 region size classes (RFC 0025 C3) L1 harness_logc_hdrchk.c: the verbatim static __logc_hdrchk (check_copies- guarded). Proves a header that passes with *eofp==0 is internally consistent (hdr->len > hdr->size, and hdr->len <= bp_maxrec when bp_maxrec != 0), with the __logc_set_maxrec re-read stubbed as both a no-op and a shrink. Sabotage (L1_SABOTAGE, a separate hand-written copy, like harness_tally's) uses < for <= and FAILs. E1 harness_env_alloc_size.c: __env_alloc_size/DB_ALLOC_SIZE and SET_QUEUE_FOR_SIZE (verbatim macros + DB_ALIGN). SIZE: the rounded allocation covers len and is 8-aligned with no size_t overflow (default + DIAGNOSTIC guard-byte). QUEUE: the size-class index stays in [0, DB_SIZE_Q_COUNT], is the smallest class covering the chunk, and the clamp of an over-range index is a valid subscript. Sabotage (E1_SABOTAGE) uses < for <= in the class test and FAILs at the boundary. No engine finding for either. Whole suite ~28 s (cadical); 6 verbatim copies match src/. --- test/cbmc/README.md | 2 + test/cbmc/harness_env_alloc_size.c | 151 ++++++++++++++++++ test/cbmc/harness_logc_hdrchk.c | 247 +++++++++++++++++++++++++++++ test/cbmc/run.sh | 12 ++ 4 files changed, 412 insertions(+) create mode 100644 test/cbmc/harness_env_alloc_size.c create mode 100644 test/cbmc/harness_logc_hdrchk.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 092c381f93..aba2444af1 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -62,6 +62,8 @@ isolate one assertion). | `harness_okitem.c` | `db/db_ret.c` `__db_ret_okitem` (the #67 guard) | **safety guarantee**: if okitem returns 0 ("safe"), the exact downstream `__db_ret`/`__db_retcopy` read stays on-page (`__CPROVER_r_ok`) | page ≤ 64 bytes (loop-free) | ~1 s | SUCCESSFUL. Found a real bug (below), fixed in `2ca81268a`; `-DHPAGE_PTYPE_SABOTAGE` restores the bug and must FAIL | | `harness_bt_decompress.c` | `btree/bt_compress.c` `__bam_defdecompress` | **safety**: never reads outside `compressed->data[0..size)` nor `prevKey`/`prevData`, never writes past `destKey->ulen`/`destData->ulen`, for ANY input bytes | compressed ≤ 16, prev ≤ 8, dest ulen ≤ 16 (loop-free) | ~2 s | **BUG FOUND (below).** The real code FAILS (over-read); `-DB1_FIXED` builds the fix and VERIFIES. `run.sh` runs the real code as a must-FAIL arm (`b1-decompress`) until the engine fix lands | | `harness_qam_recno.c` | `dbinc/qam.h` `QAM_RECNO_PAGE` / `QAM_RECNO_INDEX` / `QAM_OUTSIDE_QUEUE` / `QAM_BEFORE_FIRST` / `QAM_AFTER_CURRENT` / `QAM_NOT_VALID` | **MAP:** for recno ≥ 1, `QAM_RECNO_INDEX(QAM_RECNO_PAGE(r)) < rec_page` and `(page,index)` maps back to `r`. **RANGE:** the macros agree with an independent circular-window reference, incl. the wrapped queue (`cur < first`). **PARTITION:** for recno ≠ RECNO_OOB, exactly one of before-first / after-current / inside holds; `QAM_NOT_VALID == before \|\| after`. `-DQAM_SABOTAGE` drops the 1-based `- 1` in `QAM_RECNO_INDEX` and must FAIL | full `u_int32_t` recno/first/cur/q_root; rec_page 1..8 (loop-free) | ~1 s | SUCCESSFUL (macros agree with the reference; no bug) | +| `harness_logc_hdrchk.c` | `log/log_get.c` `__logc_hdrchk` (static) | a header that passes with `*eofp == 0` is internally consistent: `hdr->len > hdr->size`, and `hdr->len <= bp_maxrec` when `bp_maxrec != 0`. Checked with the `__logc_set_maxrec` re-read stubbed both as a no-op and as a shrink (`-DL1_SET_MAXREC_SHRINK`). `-DL1_SABOTAGE` uses `<` for `<=` and must FAIL | all field values nondet (loop-free) | ~1 s | SUCCESSFUL | +| `harness_env_alloc_size.c` | `env/env_alloc.c` `__env_alloc_size`/`DB_ALLOC_SIZE` + `SET_QUEUE_FOR_SIZE` | **SIZE:** the rounded allocation covers `len` (`>= len`) and is 8-aligned with no `size_t` overflow (default and `-DE1_DIAGNOSTIC` guard-byte builds). **QUEUE:** the size-class index is in `[0, DB_SIZE_Q_COUNT]`, is the smallest class covering the chunk when `< DB_SIZE_Q_COUNT`, and the engine's clamp of an over-range index yields a valid `sizeq[]` subscript. `-DE1_SABOTAGE` uses `<` for `<=` in the class test and must FAIL | `len` 0..64 MB (loop ≤ 11) | ~1 s | SUCCESSFUL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION SUCCESSFUL`) and with `-DHPAGE_PTYPE_SABOTAGE`, which restores the pre-fix diff --git a/test/cbmc/harness_env_alloc_size.c b/test/cbmc/harness_env_alloc_size.c new file mode 100644 index 0000000000..b42b059dcf --- /dev/null +++ b/test/cbmc/harness_env_alloc_size.c @@ -0,0 +1,151 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness: region allocator size classes (src/env/env_alloc.c). + * (RFC 0025 E1.) + * + * __env_alloc carves the shared region into chunks, bucketed into size queues + * by SET_QUEUE_FOR_SIZE and sized by DB_ALLOC_SIZE / __env_alloc_size. A bad + * size class or a size that does not cover the request corrupts the region + * allocator for every process attached to it. + * + * SIZE: __env_alloc_size(len) == DB_ALLOC_SIZE(len) rounds the request up to + * the alignment and ALWAYS covers len (result >= len), with no + * size_t overflow, for every len up to a stated bound. + * + * QUEUE: SET_QUEUE_FOR_SIZE produces an index i in [0, DB_SIZE_Q_COUNT]. + * When i < DB_SIZE_Q_COUNT it is the SMALLEST queue whose class + * (1024 << i) covers len. When i == DB_SIZE_Q_COUNT (len exceeds the + * largest class, 1 MB) the engine clamps it to DB_SIZE_Q_COUNT - 1 + * before indexing sizeq[]; that clamped index is in range. + * + * SET_QUEUE_FOR_SIZE and DB_ALLOC_SIZE / DB_ALIGN are copied VERBATIM from + * src/env/env_alloc.c (the queue head array access is replaced by a local + * array, since the macro only reads &head->sizeq[i]; the arithmetic that + * picks i and rounds the size is the shipped code). sizeof(ALLOC_ELEMENT) is + * modelled as ALLOC_ELEMENT_SIZE below (its real LP64 layout: two + * SH_TAILQ_ENTRY of two db_ssize_t each, plus two uintmax_t). + * + * Bound: len in 0..LEN_MAX (a region chunk, far below SIZE_MAX; the allocator + * is never asked for a size near the address-space limit, where the + * `len + overhead + align` sum would of course overflow). Loop-free + * apart from the <= 11-iteration SET_QUEUE_FOR_SIZE loop. + */ + +#include +#include + +typedef uint8_t u_int8_t; +typedef uint32_t u_int32_t; +typedef uint64_t u_int64_t; +typedef unsigned int u_int; + +/* --- VERBATIM constants / macros from src/env/env_alloc.c + db_int.h --- */ +#define DB_SIZE_Q_COUNT 11 + +/* DB_ALIGN from src/dbinc/db_int.in. */ +#define DB_ALIGN(v, bound) \ + (((v) + (bound) - 1) & ~(((uintmax_t)(bound)) - 1)) + +/* + * sizeof(ALLOC_ELEMENT): two SH_TAILQ_ENTRY (each two db_ssize_t) plus two + * uintmax_t. On the LP64 target db_ssize_t is 8 bytes and uintmax_t is 8, + * so 2*(2*8) + 2*8 = 48. The DIAGNOSTIC build adds a +1 guard byte before + * the alignment; we verify both. + */ +#define ALLOC_ELEMENT_SIZE 48 + +#ifdef E1_DIAGNOSTIC +#define DB_ALLOC_SIZE(len) \ + (size_t)DB_ALIGN((len) + ALLOC_ELEMENT_SIZE + 1, sizeof(uintmax_t)) +#else +#define DB_ALLOC_SIZE(len) \ + (size_t)DB_ALIGN((len) + ALLOC_ELEMENT_SIZE, sizeof(uintmax_t)) +#endif + +/* + * SET_QUEUE_FOR_SIZE from src/env/env_alloc.c, with the real head->sizeq[i] + * access replaced by a local array `sizeq` (the macro only takes its address). + */ +#ifdef E1_SABOTAGE +/* + * SABOTAGE: `<` for `<=` in the class test. A chunk whose length is exactly + * a class boundary (1024 << i) then falls through to the NEXT, larger queue + * (or past the last one), so the "i is the smallest class that covers len" + * property fails at the boundary. + */ +#define CLASS_FITS(len, i) ((len) < (u_int64_t)1024 << (i)) +#else +#define CLASS_FITS(len, i) ((len) <= (u_int64_t)1024 << (i)) +#endif +#define SET_QUEUE_FOR_SIZE(sizeq, q, i, len) do { \ + for (i = 0; i < DB_SIZE_Q_COUNT; ++i) { \ + q = &(sizeq)[i]; \ + if (CLASS_FITS(len, i)) \ + break; \ + } \ +} while (0) +/* --- end verbatim macros --- */ + +/* The largest size class is 1024 << 10 == 1 MB. Bound len well below + * SIZE_MAX (see header): a few MB covers every region-chunk request and + * keeps the overhead+alignment sum from overflowing size_t. */ +#define LEN_MAX ((size_t)0x4000000) /* 64 MB */ + +size_t nondet_size(void); + +void harness(void) +{ + size_t len, total, c; + /* A stand-in for head->sizeq[]; the macro takes &sizeq[i]. */ + u_int8_t sizeq[DB_SIZE_Q_COUNT]; + u_int8_t *q; + u_int i; + + len = nondet_size(); + __CPROVER_assume(len <= LEN_MAX); + + /* ---- SIZE: the rounded size covers len and does not overflow. ---- */ + total = DB_ALLOC_SIZE(len); + __CPROVER_assert(total >= len, + "env_alloc_size: rounded size covers the request"); + /* Alignment is to 8 bytes, so total is a multiple of 8. */ + __CPROVER_assert((total & (sizeof(uintmax_t) - 1)) == 0, + "env_alloc_size: result is aligned"); + + /* ---- QUEUE: the chosen index is in range and is the smallest class + * that covers the (rounded) chunk length. ---- */ + SET_QUEUE_FOR_SIZE(sizeq, q, i, total); + __CPROVER_assert(i <= DB_SIZE_Q_COUNT, + "SET_QUEUE_FOR_SIZE: index never exceeds the queue count"); + + if (i < DB_SIZE_Q_COUNT) { + /* class i covers total ... */ + c = (size_t)1024 << i; + __CPROVER_assert(total <= c, + "SET_QUEUE_FOR_SIZE: chosen class covers the chunk"); + /* ... and it is the SMALLEST such class (class i-1 does not). */ + if (i > 0) { + size_t cprev = (size_t)1024 << (i - 1); + __CPROVER_assert(total > cprev, + "SET_QUEUE_FOR_SIZE: no smaller class would fit"); + } + } + + /* The engine clamps an out-of-range index to the last queue before it + * indexes sizeq[] (env_alloc.c: `if (i >= DB_SIZE_Q_COUNT) i = + * DB_SIZE_Q_COUNT - 1`). The clamped index is always valid. */ + { + u_int ci = i; + if (ci >= DB_SIZE_Q_COUNT) + ci = DB_SIZE_Q_COUNT - 1; + __CPROVER_assert(ci < DB_SIZE_Q_COUNT, + "clamped queue index is a valid sizeq[] subscript"); + } +} diff --git a/test/cbmc/harness_logc_hdrchk.c b/test/cbmc/harness_logc_hdrchk.c new file mode 100644 index 0000000000..6cd377ac0f --- /dev/null +++ b/test/cbmc/harness_logc_hdrchk.c @@ -0,0 +1,247 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness: __logc_hdrchk (src/log/log_get.c). (RFC 0025 L1.) + * + * __logc_hdrchk is the guard recovery and DB_LOGC->get run over a log record + * header read from disk BEFORE trusting hdr->len to allocate a buffer and copy + * a record out. A header that passes must be internally consistent, or + * recovery over-allocates / over-copies on a corrupt log. + * + * PROPERTY: if __logc_hdrchk returns 0 and reports NOT end-of-file + * (*eofp == 0), then + * (1) hdr->len > hdr->size (the record is larger than its own + * header -- there is a body to read); + * (2) when bp_maxrec != 0 (we are reading from a log file), + * hdr->len <= bp_maxrec (not an impossibly large record). + * + * The function body below is copied VERBATIM from src/log/log_get.c between + * the BEGIN/END markers (guarded by check_copies.sh). What is stubbed (named + * in each stub's comment): + * - __logc_set_maxrec: the real one re-reads the max-record size from a + * growing last log file. The brief stubs it; here it returns 0 and leaves + * bp_maxrec unchanged, so the post-condition is checked against the value + * the function actually decided with. To keep the proof honest about the + * re-read, the harness ALSO runs a variant where the stub lowers bp_maxrec + * (it can only shrink what passes), which still must uphold the property. + * - __db_err / __db_errx: error reporting; no-ops (the err: path returns EIO, + * not 0, so it never reaches the success post-condition). + * - F_ISSET: the real bit test, over a nondet flags word. + * + * Bound: all field values nondet; loop-free. + */ + +#include +#include + +typedef uint8_t u_int8_t; +typedef uint32_t u_int32_t; +typedef unsigned long u_long; + +#define EIO 5 +#define DB_MAC_KEY 20 +#define DB_IV_BYTES 16 +#define DB_LOG_SILENT_ERR 0x04 + +#define F_ISSET(p, f) ((p)->flags & (f)) +#define DB_STR_A(id, msg, fmt) (msg) +#define COMPQUIET(x, v) do { (x) = (v); } while (0) + +typedef struct { u_int32_t file, offset; } DB_LSN; + +/* HDR: mirrors src/dbinc/log.h struct __hdr (the fields hdrchk reads). */ +typedef struct __hdr { + u_int32_t prev; + u_int32_t len; + u_int8_t chksum[DB_MAC_KEY]; + u_int8_t iv[DB_IV_BYTES]; + u_int32_t orig_size; + size_t size; +} HDR; + +typedef struct { int unused; } ENV; + +/* DB_LOGC: only the fields hdrchk reads (src/dbinc/db.in struct + * __db_log_cursor): env, bp_maxrec, flags. */ +typedef struct __db_log_cursor { + ENV *env; + u_int32_t bp_maxrec; + u_int32_t flags; +} DB_LOGC; + +/* __logc_set_maxrec stub: see header comment. SET_MAXREC_SHRINK lowers + * bp_maxrec (models the re-read finding a smaller max); otherwise it is a + * no-op. Either way it returns success. */ +u_int32_t nondet_u32(void); +static int +__logc_set_maxrec(DB_LOGC *logc, char *name) +{ + COMPQUIET(name, (char *)0); +#ifdef L1_SET_MAXREC_SHRINK + { + u_int32_t nv = nondet_u32(); + __CPROVER_assume(nv <= logc->bp_maxrec); + logc->bp_maxrec = nv; + } +#endif + return (0); +} + +/* Error reporting stubs: no-ops. The err: label returns EIO, so these are + * never on a path that returns 0. */ +static void __db_err(ENV *env, int ret, const char *fmt, ...) { (void)env; (void)ret; (void)fmt; } +static void __db_errx(ENV *env, const char *fmt, ...) { (void)env; (void)fmt; } + +/* --- BEGIN verbatim copy of __logc_hdrchk from src/log/log_get.c --- */ +static int +__logc_hdrchk(logc, lsn, hdr, eofp) + DB_LOGC *logc; + DB_LSN *lsn; + HDR *hdr; + int *eofp; +{ + ENV *env; + int ret; + + env = logc->env; + + /* + * Check EOF before we do any other processing. + */ + if (eofp != NULL) { + if (hdr->prev == 0 && hdr->chksum[0] == 0 && hdr->len == 0) { + *eofp = 1; + return (0); + } + *eofp = 0; + } + + /* + * Sanity check the log record's size. + * We must check it after "virtual" EOF above. + */ + if (hdr->len <= hdr->size) + goto err; + + /* + * If the cursor's max-record value isn't yet set, it means we aren't + * reading these records from a log file and no check is necessary. + */ + if (logc->bp_maxrec != 0 && hdr->len > logc->bp_maxrec) { + /* + * If we fail the check, there's the pathological case that + * we're reading the last file, it's growing, and our initial + * check information was wrong. Get it again, to be sure. + */ + if ((ret = __logc_set_maxrec(logc, NULL)) != 0) { + __db_err(env, ret, "DB_LOGC->get"); + return (ret); + } + if (logc->bp_maxrec != 0 && hdr->len > logc->bp_maxrec) + goto err; + } + return (0); + +err: if (!F_ISSET(logc, DB_LOG_SILENT_ERR)) + __db_errx(env, DB_STR_A("2580", + "DB_LOGC->get: LSN %lu/%lu: invalid log record header", + "%lu %lu"), (u_long)lsn->file, (u_long)lsn->offset); + return (EIO); +} +/* --- END verbatim copy --- */ + +/* + * SABOTAGE variant: the brief's planted bug -- `<` for `<=` in the record-size + * sanity check. With `<`, a header whose len EQUALS its size (a record with no + * body) passes, so property (1) -- hdr->len > hdr->size on a non-EOF OK -- must + * FAIL. The non-sabotage build uses the verbatim __logc_hdrchk above; this + * hand-written copy exists only so the sabotage has teeth, and is not guarded + * by check_copies.sh (it is deliberately different from src/). + */ +#ifdef L1_SABOTAGE +static int +__logc_hdrchk_sab(logc, lsn, hdr, eofp) + DB_LOGC *logc; + DB_LSN *lsn; + HDR *hdr; + int *eofp; +{ + ENV *env; + int ret; + + env = logc->env; + + if (eofp != NULL) { + if (hdr->prev == 0 && hdr->chksum[0] == 0 && hdr->len == 0) { + *eofp = 1; + return (0); + } + *eofp = 0; + } + + if (hdr->len < hdr->size) /* SABOTAGE: was <= */ + goto err; + + if (logc->bp_maxrec != 0 && hdr->len > logc->bp_maxrec) { + if ((ret = __logc_set_maxrec(logc, NULL)) != 0) { + __db_err(env, ret, "DB_LOGC->get"); + return (ret); + } + if (logc->bp_maxrec != 0 && hdr->len > logc->bp_maxrec) + goto err; + } + return (0); + +err: if (!F_ISSET(logc, DB_LOG_SILENT_ERR)) + __db_errx(env, DB_STR_A("2580", + "DB_LOGC->get: LSN %lu/%lu: invalid log record header", + "%lu %lu"), (u_long)lsn->file, (u_long)lsn->offset); + return (EIO); +} +#define HDRCHK(l, s, h, e) __logc_hdrchk_sab(l, s, h, e) +#else +#define HDRCHK(l, s, h, e) __logc_hdrchk(l, s, h, e) +#endif + +u_int8_t nondet_u8(void); +size_t nondet_size(void); + +void harness(void) +{ + DB_LOGC logc; + DB_LSN lsn; + HDR hdr; + int eof, rc; + unsigned i; + + logc.env = (ENV *)0; + logc.bp_maxrec = nondet_u32(); + logc.flags = nondet_u32(); + + lsn.file = nondet_u32(); + lsn.offset = nondet_u32(); + + hdr.prev = nondet_u32(); + hdr.len = nondet_u32(); + for (i = 0; i < DB_MAC_KEY; i++) + hdr.chksum[i] = nondet_u8(); + hdr.orig_size = nondet_u32(); + hdr.size = nondet_size(); + + eof = -1; + rc = HDRCHK(&logc, &lsn, &hdr, &eof); + + if (rc == 0 && eof == 0) { + __CPROVER_assert(hdr.len > hdr.size, + "hdrchk-OK non-EOF: record length exceeds its header size"); + if (logc.bp_maxrec != 0) + __CPROVER_assert(hdr.len <= logc.bp_maxrec, + "hdrchk-OK non-EOF: record length within bp_maxrec"); + } +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index ee10743e01..e403c5edbe 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -65,6 +65,10 @@ run ack-onepeer harness_ackpolicy.c harness_one_peer --unwind 6 --unwinding-as run ack-2site harness_ackpolicy.c harness_twosite --unwind 6 --unwinding-assertions # H4 2-site cases run ack-shortcut harness_ackpolicy.c harness_shortcut --unwind 6 --unwinding-assertions # H4 send shortcuts run qam-recno harness_qam_recno.c harness --conversion-check # Q1 queue record arithmetic +run logc-hdrchk harness_logc_hdrchk.c harness # L1 log header check +run logc-hdrchk2 harness_logc_hdrchk.c harness -DL1_SET_MAXREC_SHRINK # L1 w/ maxrec re-read that shrinks +run env-alloc harness_env_alloc_size.c harness --unwind 12 --unwinding-assertions # E1 region size classes +run env-alloc-d harness_env_alloc_size.c harness -DE1_DIAGNOSTIC --unwind 12 --unwinding-assertions # E1 DIAGNOSTIC size # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -118,6 +122,14 @@ sabotage b1-decompress harness_bt_decompress.c harness \ # index-in-range bound and the (page,index)->recno round-trip. sabotage qam-recno-sab harness_qam_recno.c harness -DQAM_SABOTAGE \ --bounds-check --pointer-check --conversion-check +# L1: `<` for `<=` in the record-size sanity check lets a body-less record +# (len == size) pass -- property (1) then fails. +sabotage logc-hdrchk-sab harness_logc_hdrchk.c harness -DL1_SABOTAGE \ + --bounds-check --pointer-check +# E1: `<` for `<=` in SET_QUEUE_FOR_SIZE sends a boundary-size chunk to the +# next, larger queue -- the chosen class is no longer the smallest that fits. +sabotage env-alloc-sab harness_env_alloc_size.c harness -DE1_SABOTAGE \ + --bounds-check --pointer-check --unwind 12 --unwinding-assertions # H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ --bounds-check --pointer-check From bd9575070a7af30d326bf9b7b304ed8a1e5318ed Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 11:44:05 -0500 Subject: [PATCH 11/15] test/cbmc: B2 compress/decompress round trip (RFC 0025 C2) harness_bt_roundtrip.c proves decompress(compress(key,data)) == (key,data) for the default compressed-btree codec, given the same prevKey/prevData. Both __bam_defcompress and __bam_defdecompress are verbatim copies (check_copies- guarded); the varint codec is the REAL db_compint.c (#include). -DB2_SABOTAGE drops the duplicate-path magic byte on compress, so decompress misreads a duplicate record and the round trip FAILs. No engine finding. Bound: key/data/prev <= 4 bytes -- at the brief's 6 the #include'd codec's full arithmetic pushes this one harness past the suite's 5-min budget; <= 4 still covers every structural path (empty/prefix/suffix/full/duplicate) and the multi-byte varint widths are already proved by harness_varint.c. Whole suite ~4.0 min on a fast host (B2's two arms are ~110 s + ~103 s), 8 copies match. --- test/cbmc/README.md | 1 + test/cbmc/harness_bt_roundtrip.c | 424 +++++++++++++++++++++++++++++++ test/cbmc/run.sh | 5 + 3 files changed, 430 insertions(+) create mode 100644 test/cbmc/harness_bt_roundtrip.c diff --git a/test/cbmc/README.md b/test/cbmc/README.md index aba2444af1..54bf187770 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -64,6 +64,7 @@ isolate one assertion). | `harness_qam_recno.c` | `dbinc/qam.h` `QAM_RECNO_PAGE` / `QAM_RECNO_INDEX` / `QAM_OUTSIDE_QUEUE` / `QAM_BEFORE_FIRST` / `QAM_AFTER_CURRENT` / `QAM_NOT_VALID` | **MAP:** for recno ≥ 1, `QAM_RECNO_INDEX(QAM_RECNO_PAGE(r)) < rec_page` and `(page,index)` maps back to `r`. **RANGE:** the macros agree with an independent circular-window reference, incl. the wrapped queue (`cur < first`). **PARTITION:** for recno ≠ RECNO_OOB, exactly one of before-first / after-current / inside holds; `QAM_NOT_VALID == before \|\| after`. `-DQAM_SABOTAGE` drops the 1-based `- 1` in `QAM_RECNO_INDEX` and must FAIL | full `u_int32_t` recno/first/cur/q_root; rec_page 1..8 (loop-free) | ~1 s | SUCCESSFUL (macros agree with the reference; no bug) | | `harness_logc_hdrchk.c` | `log/log_get.c` `__logc_hdrchk` (static) | a header that passes with `*eofp == 0` is internally consistent: `hdr->len > hdr->size`, and `hdr->len <= bp_maxrec` when `bp_maxrec != 0`. Checked with the `__logc_set_maxrec` re-read stubbed both as a no-op and as a shrink (`-DL1_SET_MAXREC_SHRINK`). `-DL1_SABOTAGE` uses `<` for `<=` and must FAIL | all field values nondet (loop-free) | ~1 s | SUCCESSFUL | | `harness_env_alloc_size.c` | `env/env_alloc.c` `__env_alloc_size`/`DB_ALLOC_SIZE` + `SET_QUEUE_FOR_SIZE` | **SIZE:** the rounded allocation covers `len` (`>= len`) and is 8-aligned with no `size_t` overflow (default and `-DE1_DIAGNOSTIC` guard-byte builds). **QUEUE:** the size-class index is in `[0, DB_SIZE_Q_COUNT]`, is the smallest class covering the chunk when `< DB_SIZE_Q_COUNT`, and the engine's clamp of an over-range index yields a valid `sizeq[]` subscript. `-DE1_SABOTAGE` uses `<` for `<=` in the class test and must FAIL | `len` 0..64 MB (loop ≤ 11) | ~1 s | SUCCESSFUL | +| `harness_bt_roundtrip.c` | `btree/bt_compress.c` `__bam_defcompress` + `__bam_defdecompress` | **round trip:** for any prevKey/prevData/key/data, `decompress(compress(…))` with the same prev returns exactly `(key, data)` — size and bytes. Uses the REAL `db_compint.c` codec. `-DB2_SABOTAGE` drops the duplicate-path magic byte on compress and must FAIL | key/data/prev ≤ 4 bytes (6 blows the 5-min budget; structural paths all covered, varint widths are harness_varint's job) | ~2 min/arm | SUCCESSFUL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION SUCCESSFUL`) and with `-DHPAGE_PTYPE_SABOTAGE`, which restores the pre-fix diff --git a/test/cbmc/harness_bt_roundtrip.c b/test/cbmc/harness_bt_roundtrip.c new file mode 100644 index 0000000000..843c29fad7 --- /dev/null +++ b/test/cbmc/harness_bt_roundtrip.c @@ -0,0 +1,424 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness: __bam_defcompress / __bam_defdecompress round trip + * (src/btree/bt_compress.c). (RFC 0025 B2.) + * + * The default compressed-btree codec prefix-compresses each key/data pair + * against the previous one. If a round trip ever loses information, every + * key in a compressed btree is silently corrupted. We prove: + * + * ROUND TRIP: for ANY prevKey/prevData/key/data (each <= 6 bytes), if + * __bam_defcompress succeeds, then __bam_defdecompress of that output -- + * given the SAME prevKey/prevData, and dest buffers sized from compress's + * reported size -- returns exactly (key, data). + * + * Both functions are copied VERBATIM from src/btree/bt_compress.c (guarded by + * check_copies.sh). The varint codec they call is the REAL + * src/common/db_compint.c, pulled in by #include (as harness_varint.c does); + * the small 6-byte bound keeps the real codec's full arithmetic inside the + * suite budget. __db_isbigendian() is stubbed to 0 (CBMC's little-endian + * target). + * + * SABOTAGE (-DB2_SABOTAGE): drop the duplicate-path magic byte on the COMPRESS + * side (write nothing instead of CMP_INT_SPARE_VAL). Decompress then mistakes + * a duplicate record for a normal one (or vice versa) and the round trip + * fails. + * + * Bound: key/data/prevKey/prevData each <= 4 bytes. (The brief's target is 6; + * at 6 the real varint codec's full #include'd arithmetic pushes this + * one harness past ~3.5 min, over the suite's 5-min budget. At <= 4 it + * is ~2 min and still exercises every structural path -- the empty, + * prefix-only, suffix-only, full and duplicate cases -- since record + * lengths <= 4 are all 1-byte length varints; the multi-byte varint + * widths are already proved exhaustively by harness_varint.c.) + * Loop-free apart from the codec's fixed shuffles and the <= 4-byte + * prefix-match loops. + */ + +#include +#include + +typedef uint8_t u_int8_t; +typedef uint16_t u_int16_t; +typedef uint32_t u_int32_t; +typedef uint64_t u_int64_t; + +#define EINVAL 22 +#define DB_BUFFER_SMALL (-30999) +#define CMP_INT_SPARE_VAL 0xFC + +#define COMPQUIET(x, v) do { (x) = (v); } while (0) + +typedef struct __db_dbt { + void *data; + u_int32_t size; + u_int32_t ulen; + u_int32_t dlen; + u_int32_t doff; +} DBT; + +typedef struct __db { int unused; } DB; + +/* Endianness stub: CBMC target is little-endian (see harness_varint.c). */ +int __db_isbigendian(void) { return 0; } + +/* Pull in the REAL varint codec (db_compint.c is #ifdef HAVE_COMPRESSION). */ +#define HAVE_COMPRESSION 1 +#include "../../src/common/db_compint.c" + +/* + * The compress side's duplicate magic byte. Normally CMP_INT_SPARE_VAL; the + * sabotage drops it (writes nothing and does not advance ptr), so the encoded + * duplicate is indistinguishable from a short normal record. + */ +#ifdef B2_SABOTAGE +#define WRITE_DUP_MAGIC(ptr) do { } while (0) +#else +#define WRITE_DUP_MAGIC(ptr) do { *(ptr) = CMP_INT_SPARE_VAL; ++(ptr); } while (0) +#endif + +/* --- BEGIN verbatim copy of __bam_defcompress from src/btree/bt_compress.c --- */ +int +__bam_defcompress(dbp, prevKey, prevData, key, data, dest) + DB *dbp; + const DBT *prevKey, *prevData, *key, *data; + DBT *dest; +{ + u_int8_t *ptr; + const u_int8_t *k, *p; + size_t len, prefix, suffix; + + COMPQUIET(dbp, NULL); + + k = (const u_int8_t*)key->data; + p = (const u_int8_t*)prevKey->data; + len = key->size > prevKey->size ? prevKey->size : key->size; + for (; len-- && *k == *p; ++k, ++p) + continue; + + prefix = (size_t)(k - (u_int8_t*)key->data); + suffix = key->size - prefix; + + if (prefix == prevKey->size && suffix == 0) { + /* It's a duplicate - do prefix compression on the value */ + k = (const u_int8_t*)data->data; + p = (const u_int8_t*)prevData->data; + len = data->size > prevData->size ? prevData->size : data->size; + for (; len-- && *k == *p; ++k, ++p) + continue; + + prefix = (size_t)(k - (u_int8_t*)data->data); + suffix = data->size - prefix; + + /* Check that we have enough space in dest */ + dest->size = (u_int32_t)(1 + __db_compress_count_int(prefix) + + __db_compress_count_int(suffix) + suffix); + if (dest->size > dest->ulen) + return (DB_BUFFER_SMALL); + + /* Magic identifying byte */ + ptr = (u_int8_t*)dest->data; + *ptr = CMP_INT_SPARE_VAL; + ++ptr; + + /* prefix length */ + ptr += __db_compress_int(ptr, prefix); + + /* suffix length */ + ptr += __db_compress_int(ptr, suffix); + + /* suffix */ + memcpy(ptr, k, suffix); + + return (0); + } + + /* Check that we have enough space in dest */ + dest->size = (u_int32_t)(__db_compress_count_int(prefix) + + __db_compress_count_int(suffix) + + __db_compress_count_int(data->size) + suffix + data->size); + if (dest->size > dest->ulen) + return (DB_BUFFER_SMALL); + + /* prefix length */ + ptr = (u_int8_t*)dest->data; + ptr += __db_compress_int(ptr, prefix); + + /* suffix length */ + ptr += __db_compress_int(ptr, suffix); + + /* data length */ + ptr += __db_compress_int(ptr, data->size); + + /* suffix */ + memcpy(ptr, k, suffix); + ptr += suffix; + + /* data */ + memcpy(ptr, data->data, data->size); + + return (0); +} +/* --- END verbatim copy --- */ + +/* --- BEGIN verbatim copy of __bam_defdecompress from src/btree/bt_compress.c --- */ +int +__bam_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) + DB *dbp; + const DBT *prevKey, *prevData; + DBT *compressed, *destKey, *destData; +{ + u_int8_t *s, *d; + u_int32_t prefix, suffix, size; + + COMPQUIET(dbp, NULL); + + /* + * Check for the magic identifying byte, that tells us that this is a + * compressed duplicate value. + */ + s = (u_int8_t*)compressed->data; + if (*s == CMP_INT_SPARE_VAL) { + ++s; + size = 1; + + /* Unmarshal prefix and suffix */ + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + /* Check destination lengths */ + destKey->size = prevKey->size; + destData->size = prefix + suffix; + if (destKey->size > destKey->ulen || + destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + /* Write the key */ + memcpy(destKey->data, prevKey->data, destKey->size); + + /* Write the prefix */ + if (prefix > prevData->size) + return (EINVAL); + d = (u_int8_t*)destData->data; + memcpy(d, prevData->data, prefix); + d += prefix; + + /* Write the suffix */ + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + /* Return bytes read */ + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); + } + + /* Unmarshal prefix, suffix and data length */ + size = __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &prefix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &suffix); + + size += __db_decompress_count_int(s); + if (size > compressed->size) + return (EINVAL); + s += __db_decompress_int32(s, &destData->size); + + /* Check destination lengths */ + destKey->size = prefix + suffix; + if (destKey->size > destKey->ulen || destData->size > destData->ulen) + return (DB_BUFFER_SMALL); + + /* Write the prefix */ + if (prefix > prevKey->size) + return (EINVAL); + d = (u_int8_t*)destKey->data; + memcpy(d, prevKey->data, prefix); + d += prefix; + + /* Write the suffix */ + size += suffix; + if (size > compressed->size) + return (EINVAL); + memcpy(d, s, suffix); + s += suffix; + + /* Write the data */ + size += destData->size; + if (size > compressed->size) + return (EINVAL); + memcpy(destData->data, s, destData->size); + s += destData->size; + + /* Return bytes read */ + compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); + return (0); +} +/* --- END verbatim copy --- */ + +/* + * A sabotaged compress: identical to __bam_defcompress except it drops the + * duplicate-path magic byte (via WRITE_DUP_MAGIC). Used only under + * -DB2_SABOTAGE; the real __bam_defcompress above stays verbatim for + * check_copies.sh. + */ +#ifdef B2_SABOTAGE +static int +sab_defcompress(dbp, prevKey, prevData, key, data, dest) + DB *dbp; + const DBT *prevKey, *prevData, *key, *data; + DBT *dest; +{ + u_int8_t *ptr; + const u_int8_t *k, *p; + size_t len, prefix, suffix; + + COMPQUIET(dbp, NULL); + + k = (const u_int8_t*)key->data; + p = (const u_int8_t*)prevKey->data; + len = key->size > prevKey->size ? prevKey->size : key->size; + for (; len-- && *k == *p; ++k, ++p) + continue; + prefix = (size_t)(k - (u_int8_t*)key->data); + suffix = key->size - prefix; + + if (prefix == prevKey->size && suffix == 0) { + k = (const u_int8_t*)data->data; + p = (const u_int8_t*)prevData->data; + len = data->size > prevData->size ? prevData->size : data->size; + for (; len-- && *k == *p; ++k, ++p) + continue; + prefix = (size_t)(k - (u_int8_t*)data->data); + suffix = data->size - prefix; + + /* SABOTAGE: size does NOT count the dropped magic byte. */ + dest->size = (u_int32_t)(__db_compress_count_int(prefix) + + __db_compress_count_int(suffix) + suffix); + if (dest->size > dest->ulen) + return (DB_BUFFER_SMALL); + ptr = (u_int8_t*)dest->data; + WRITE_DUP_MAGIC(ptr); /* writes nothing under sabotage */ + ptr += __db_compress_int(ptr, prefix); + ptr += __db_compress_int(ptr, suffix); + memcpy(ptr, k, suffix); + return (0); + } + + dest->size = (u_int32_t)(__db_compress_count_int(prefix) + + __db_compress_count_int(suffix) + + __db_compress_count_int(data->size) + suffix + data->size); + if (dest->size > dest->ulen) + return (DB_BUFFER_SMALL); + ptr = (u_int8_t*)dest->data; + ptr += __db_compress_int(ptr, prefix); + ptr += __db_compress_int(ptr, suffix); + ptr += __db_compress_int(ptr, data->size); + memcpy(ptr, k, suffix); + ptr += suffix; + memcpy(ptr, data->data, data->size); + return (0); +} +#define COMPRESS(dp, pk, pd, k, d, dst) sab_defcompress(dp, pk, pd, k, d, dst) +#else +#define COMPRESS(dp, pk, pd, k, d, dst) __bam_defcompress(dp, pk, pd, k, d, dst) +#endif + +#define KMAX 4 +#define DESTMAX 64 + +u_int32_t nondet_u32(void); + +static u_int8_t *nondet_bytes(u_int32_t n) +{ + u_int8_t *p; + u_int32_t i; + p = malloc(n == 0 ? 1 : n); + __CPROVER_assume(p != NULL); + for (i = 0; i < n; i++) + p[i] = (u_int8_t)nondet_u32(); + return (p); +} + +void harness(void) +{ + DB db; + DBT prevKey, prevData, key, data, dest; + DBT cmp, destKey, destData; + u_int32_t pks, pds, ks, ds; + u_int8_t destbuf[DESTMAX]; + u_int8_t okbuf[DESTMAX], odbuf[DESTMAX]; + int rc; + u_int32_t i; + + pks = nondet_u32(); pds = nondet_u32(); + ks = nondet_u32(); ds = nondet_u32(); + __CPROVER_assume(pks <= KMAX && pds <= KMAX); + __CPROVER_assume(ks <= KMAX && ds <= KMAX); + + prevKey.data = nondet_bytes(pks); prevKey.size = pks; prevKey.ulen = pks; + prevData.data = nondet_bytes(pds); prevData.size = pds; prevData.ulen = pds; + key.data = nondet_bytes(ks); key.size = ks; key.ulen = ks; + data.data = nondet_bytes(ds); data.size = ds; data.ulen = ds; + + /* dest buffer: generous (DESTMAX); compress sets dest.size. */ + memset(&dest, 0, sizeof(dest)); + dest.data = destbuf; + dest.ulen = DESTMAX; + + rc = COMPRESS(&db, &prevKey, &prevData, &key, &data, &dest); + if (rc != 0) + return; /* DB_BUFFER_SMALL => nothing to prove */ + + /* Decompress the compressed buffer (sized exactly from compress). */ + memset(&cmp, 0, sizeof(cmp)); + cmp.data = destbuf; + cmp.size = dest.size; + cmp.ulen = dest.size; + + memset(&destKey, 0, sizeof(destKey)); + memset(&destData, 0, sizeof(destData)); + destKey.data = okbuf; destKey.ulen = DESTMAX; + destData.data = odbuf; destData.ulen = DESTMAX; + + rc = __bam_defdecompress(&db, &prevKey, &prevData, + &cmp, &destKey, &destData); + __CPROVER_assert(rc == 0, + "B2 round trip: decompress of a successful compress succeeds"); + if (rc != 0) + return; + + __CPROVER_assert(destKey.size == key.size, + "B2 round trip: key size recovered"); + __CPROVER_assert(destData.size == data.size, + "B2 round trip: data size recovered"); + for (i = 0; i < KMAX; i++) { + if (i < key.size) + __CPROVER_assert(okbuf[i] == ((u_int8_t *)key.data)[i], + "B2 round trip: key bytes recovered"); + if (i < data.size) + __CPROVER_assert(odbuf[i] == ((u_int8_t *)data.data)[i], + "B2 round trip: data bytes recovered"); + } +} diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index e403c5edbe..00d9e00cb9 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -69,6 +69,7 @@ run logc-hdrchk harness_logc_hdrchk.c harness # run logc-hdrchk2 harness_logc_hdrchk.c harness -DL1_SET_MAXREC_SHRINK # L1 w/ maxrec re-read that shrinks run env-alloc harness_env_alloc_size.c harness --unwind 12 --unwinding-assertions # E1 region size classes run env-alloc-d harness_env_alloc_size.c harness -DE1_DIAGNOSTIC --unwind 12 --unwinding-assertions # E1 DIAGNOSTIC size +run b2-roundtrip harness_bt_roundtrip.c harness --unwind 6 # B2 compress/decompress round trip # okitem proves the safety guarantee on the real (parenthesised) HPAGE_PTYPE. # We drop --pointer-check here (keeping --bounds-check + __CPROVER_r_ok, the @@ -130,6 +131,10 @@ sabotage logc-hdrchk-sab harness_logc_hdrchk.c harness -DL1_SABOTAGE \ # next, larger queue -- the chosen class is no longer the smallest that fits. sabotage env-alloc-sab harness_env_alloc_size.c harness -DE1_SABOTAGE \ --bounds-check --pointer-check --unwind 12 --unwinding-assertions +# B2: dropping the duplicate-path magic byte on the compress side makes +# decompress misread a duplicate record, so the round trip fails. +sabotage b2-roundtrip-sab harness_bt_roundtrip.c harness -DB2_SABOTAGE \ + --bounds-check --pointer-check --unwind 6 # H1: swapping LOG_COMPARE's order arms breaks winner-maximises-LSN (d). sabotage cmpvote-sab harness_cmpvote.c harness_likepri -DCMPVOTE_SABOTAGE \ --bounds-check --pointer-check From 391d1a26055d8b4cd30fb04db55d13af43139edd Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 11:44:40 -0500 Subject: [PATCH 12/15] test/cbmc: refresh the workflow runtime note (RFC 0025 C2/C3) The B1 and B2 btree-compression harnesses run the real varint codec and take ~2 min each, so the suite is a few minutes now, not under one. The 30-min job timeout is unchanged. cadical (CBMC's built-in fast SAT backend, which run.sh now selects) ships inside the cbmc binary, so no flake change is needed. --- .github/workflows/cbmc.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml index 3ac34821e5..71ee425958 100644 --- a/.github/workflows/cbmc.yml +++ b/.github/workflows/cbmc.yml @@ -7,8 +7,9 @@ # # Runs on every PR and push, not on a paths filter: a harness covers code # wherever it lives in src/, and a filter that lists files silently skips a -# change to a file someone forgot to add. The whole suite takes under a -# minute after the nix shell is warm. +# change to a file someone forgot to add. The whole suite takes a few minutes +# after the nix shell is warm (the two btree-compression harnesses that run the +# real varint codec dominate at ~2 min each; everything else is seconds). name: CBMC on: From a431dc72572bc38d6e9326544f950b67d5627e44 Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 12:15:29 -0500 Subject: [PATCH 13/15] test/cbmc: B1 models the decoded varint value as any u32, add the wrap arm The varint model returned a value built from the bytes it read, at most about 2^17, so the proof could not see prefix + suffix wrap. The real decoder returns any u32 from a 5-byte varint. With the value nondet, the first fix (2e99a1f84) fails the proof; the fix plus e067d6507 verifies. The B1_FIXED arm is now a verbatim copy of the final fixed function, and a new b1-wrap arm (-DB1_NO_WRAP_CHECK) must fail. --- test/cbmc/README.md | 31 +++++++++++-- test/cbmc/harness_bt_decompress.c | 76 +++++++++++++++++++++++++------ test/cbmc/run.sh | 4 ++ 3 files changed, 92 insertions(+), 19 deletions(-) diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 54bf187770..a74ed5cd57 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -232,12 +232,35 @@ at the second varint. CBMC reports two genuine failures on the real code: `__bam_defdecompress … *s: pointer outside object bounds` and `varint … buf[0]: pointer outside object bounds`. +### A second hole: the decoded lengths wrap + +The first version of this harness modelled `__db_decompress_int32` as +returning a value built from the bytes it read, which never exceeded about +2^17. That hid a worse bug. The decoded prefix, suffix and data length come +from disk and can be any u32. With prefix 4 and suffix `0xFFFFFFFE`, +`prefix + suffix` wraps to 2, `size += suffix` wraps back under +`compressed->size`, every check passes, and `memcpy` copies about 4 GB. This +happens on both paths. The model now returns `nondet_u32()`, and the first fix +alone fails the proof (`b1-wrap` arm). + +`__bamc_start_decompress`, the caller that decodes each item's first record, +had the same hole one level up: it copied the decoded length out of the page +unchecked. `test/db/bt_decompress_bounds.c` case E corrupts one length byte in +a real compressed database and crashes a plain `DB->get` on master. + ### The fix (on `fix/bt-decompress-bounds`, built here as `-DB1_FIXED`) -Check that the next byte index is still inside `compressed->size` **before** -every `__db_decompress_count_int`, and that `compressed->size >= 1` before the -magic `*s`. `harness_bt_decompress.c -DB1_FIXED` builds this variant and -VERIFIES (no over-read, no over-write) over the whole input space. +1. Check that the next byte index is still inside `compressed->size` **before** + every `__db_decompress_count_int`, and that `compressed->size >= 1` before + the magic `*s` (`2e99a1f84`). +2. Bound prefix against the previous key or data, suffix and the data length + against what is left of the item, and `prefix + suffix` against + `UINT32_MAX`, before any sum. Check the first record's length in + `__bamc_start_decompress` (`e067d6507`). + +`-DB1_FIXED` builds a verbatim copy of the fixed function and VERIFIES (no +over-read, no over-write) over the whole bounded input space. +`-DB1_FIXED -DB1_NO_WRAP_CHECK` drops step 2 and must FAIL. ### How this harness runs diff --git a/test/cbmc/harness_bt_decompress.c b/test/cbmc/harness_bt_decompress.c index c56e4f941e..4cb0a82165 100644 --- a/test/cbmc/harness_bt_decompress.c +++ b/test/cbmc/harness_bt_decompress.c @@ -71,6 +71,7 @@ typedef uint64_t u_int64_t; typedef uint32_t db_pgno_t; #define EINVAL 22 +#define UINT32_MAX 4294967295U #define DB_BUFFER_SMALL (-30999) /* CMP_INT_SPARE_VAL: db_int.h value (the duplicate-value magic byte). */ @@ -89,6 +90,8 @@ typedef struct __db_dbt { typedef struct __db { int unused; } DB; +u_int32_t nondet_u32(void); + /* * Varint read-footprint models. See the header comment: these read EXACTLY * the bytes the real db_compint.c decoders read (buf[0] for the count; the @@ -129,23 +132,27 @@ static int __db_decompress_int32(const u_int8_t *buf, u_int32_t *i) { u_int32_t w = varint_width(buf); u_int32_t k; - u_int32_t acc = 0; + u_int8_t sink = 0; /* The real int32 decoder reads the leading `w` bytes of buf. */ for (k = 0; k < w; k++) - acc = (acc << 1) ^ buf[k]; - *i = acc; + sink ^= buf[k]; + (void)sink; + /* + * The decoded VALUE is any u32: a 5-byte varint reaches UINT32_MAX, + * and the bytes come from disk. An earlier model returned a value + * built from the bytes read, which never exceeded ~2^17, so the proof + * could not see prefix + suffix wrap. + */ + *i = nondet_u32(); return ((int)w); } /* ------------------------------------------------------------------------ */ #ifdef B1_FIXED /* - * The proposed fix: check that the varint's declared width fits BEFORE - * reading its bytes, and that there is at least one byte before reading *s. - * This mirrors fix/bt-decompress-bounds. __db_decompress_count_int reads - * s[0] (one byte), so a safe pre-check is "the next byte index (size) is - * still < compressed->size" before each count_int, and compressed->size >= 1 - * before *s. + * The fix on fix/bt-decompress-bounds (2e99a1f84 + e067d6507), copied + * verbatim. When it lands on master, drop this arm: the BEGIN/END copy + * below becomes the fixed code and check_copies.sh guards it. */ static int b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) @@ -158,17 +165,25 @@ b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) COMPQUIET(dbp, NULL); - /* Need at least the magic/first byte. */ + /* + * Check for the magic identifying byte, that tells us that this is a + * compressed duplicate value. + * + * A compressed item comes from a btree page, i.e. from disk, so it is a + * trust boundary: a corrupt or truncated item must be rejected, not + * over-read. Each __db_decompress_count_int/_int32 below dereferences + * the byte at the current offset, so that offset must be proven < the + * compressed buffer BEFORE the read -- otherwise a short item over-reads + * its lookahead byte (and *s over-reads a zero-length item). + */ if (compressed->size < 1) return (EINVAL); - s = (u_int8_t*)compressed->data; if (*s == CMP_INT_SPARE_VAL) { ++s; size = 1; - /* Before reading the count byte at offset `size`, it must be - * on-buffer. */ + /* Unmarshal prefix and suffix */ if (size >= compressed->size) return (EINVAL); size += __db_decompress_count_int(s); @@ -183,31 +198,49 @@ b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) return (EINVAL); s += __db_decompress_int32(s, &suffix); + /* + * prefix and suffix are from disk too: bound them before any + * sum, or prefix + suffix and size + suffix wrap and the copies + * below run with a huge length. + */ + #ifndef B1_NO_WRAP_CHECK + if (prefix > prevData->size || + suffix > compressed->size - size || + suffix > UINT32_MAX - prefix) + return (EINVAL); +#endif + + /* Check destination lengths */ destKey->size = prevKey->size; destData->size = prefix + suffix; if (destKey->size > destKey->ulen || destData->size > destData->ulen) return (DB_BUFFER_SMALL); + /* Write the key */ memcpy(destKey->data, prevKey->data, destKey->size); + /* Write the prefix */ if (prefix > prevData->size) return (EINVAL); d = (u_int8_t*)destData->data; memcpy(d, prevData->data, prefix); d += prefix; + /* Write the suffix */ size += suffix; if (size > compressed->size) return (EINVAL); memcpy(d, s, suffix); s += suffix; + /* Return bytes read */ compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); return (0); } - /* s[0] is covered by the compressed->size >= 1 check at the top. */ + /* Unmarshal prefix, suffix and data length (s[0] is covered by the + * compressed->size >= 1 check above). */ size = __db_decompress_count_int(s); if (size > compressed->size) return (EINVAL); @@ -227,28 +260,42 @@ b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) return (EINVAL); s += __db_decompress_int32(s, &destData->size); + /* As above: bound the on-disk lengths before any sum can wrap. */ +#ifndef B1_NO_WRAP_CHECK + if (prefix > prevKey->size || + suffix > compressed->size - size || + suffix > UINT32_MAX - prefix || + destData->size > compressed->size - size - suffix) + return (EINVAL); +#endif + + /* Check destination lengths */ destKey->size = prefix + suffix; if (destKey->size > destKey->ulen || destData->size > destData->ulen) return (DB_BUFFER_SMALL); + /* Write the prefix */ if (prefix > prevKey->size) return (EINVAL); d = (u_int8_t*)destKey->data; memcpy(d, prevKey->data, prefix); d += prefix; + /* Write the suffix */ size += suffix; if (size > compressed->size) return (EINVAL); memcpy(d, s, suffix); s += suffix; + /* Write the data */ size += destData->size; if (size > compressed->size) return (EINVAL); memcpy(destData->data, s, destData->size); s += destData->size; + /* Return bytes read */ compressed->size = (u_int32_t)(s - (u_int8_t*)compressed->data); return (0); } @@ -367,7 +414,6 @@ __bam_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) #define PREVMAX 8 #define DESTMAX 16 -u_int32_t nondet_u32(void); /* * Allocate a buffer of EXACTLY `n` bytes. CBMC's malloc gives a fresh object diff --git a/test/cbmc/run.sh b/test/cbmc/run.sh index 00d9e00cb9..b48f4c0012 100755 --- a/test/cbmc/run.sh +++ b/test/cbmc/run.sh @@ -119,6 +119,10 @@ sabotage okitem-sab harness_okitem.c harness -DHPAGE_PTYPE_SABOTAGE \ # drop -DB1_FIXED. See README.md "BUG FOUND". sabotage b1-decompress harness_bt_decompress.c harness \ --bounds-check --pointer-check --unwind 10 +# B1b: the first fix alone (varint reads bounded, decoded lengths not) must +# also fail: prefix + suffix wraps. Catches a revert of e067d6507. +sabotage b1-wrap harness_bt_decompress.c harness -DB1_FIXED -DB1_NO_WRAP_CHECK \ + --bounds-check --pointer-check --unwind 10 # Q1: dropping the 1-based "- 1" in QAM_RECNO_INDEX (an off-by-one) breaks the # index-in-range bound and the (page,index)->recno round-trip. sabotage qam-recno-sab harness_qam_recno.c harness -DQAM_SABOTAGE \ From 7345eb85d5500f2bd86968584b23cd35fc198e6f Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 12:26:50 -0500 Subject: [PATCH 14/15] test/cbmc: Q1 and E1 bounds widened to the real input range Q1 MAP bounded recno and q_root to 0x10000. Queue has no subdatabases, so q_root is always 1 (__qam_open sets base_pgno + 1 with base_pgno 0); with that fixed, the round trip verifies for every recno >= 1. E1 bounded len to 64 MB; it verifies up to SIZE_MAX - 64, where only the rounding itself must overflow. Both sabotage arms still fail. --- test/cbmc/README.md | 4 ++-- test/cbmc/harness_env_alloc_size.c | 11 ++++------- test/cbmc/harness_qam_recno.c | 6 ++++-- 3 files changed, 10 insertions(+), 11 deletions(-) diff --git a/test/cbmc/README.md b/test/cbmc/README.md index a74ed5cd57..c4ad6e7684 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -61,9 +61,9 @@ isolate one assertion). | `harness_ackpolicy.c` | `repmgr/repmgr_net.c` `got_acks` (:1117) + the `needed`/`quorum` computation in `__repmgr_send` (DB_REP_PERMANENT block) | **QUORUM:** durable => no electable-site majority (`ELECTION_MAJORITY(total electable incl. master)`) avoids a holder (master or acked electable peer) — "no election can lose it". **2-site:** STRICT => quorum 0 (master-only durable); non-strict => the single client must ack. **ALL_PEERS:** durable => every electable peer acked. **ONE_PEER:** durable => some electable peer acked. **Shortcuts:** `needed==0` is durability-safe (only when no electable peers exist); `availabledata[0..size)` nor `prevKey`/`prevData`, never writes past `destKey->ulen`/`destData->ulen`, for ANY input bytes | compressed ≤ 16, prev ≤ 8, dest ulen ≤ 16 (loop-free) | ~2 s | **BUG FOUND (below).** The real code FAILS (over-read); `-DB1_FIXED` builds the fix and VERIFIES. `run.sh` runs the real code as a must-FAIL arm (`b1-decompress`) until the engine fix lands | -| `harness_qam_recno.c` | `dbinc/qam.h` `QAM_RECNO_PAGE` / `QAM_RECNO_INDEX` / `QAM_OUTSIDE_QUEUE` / `QAM_BEFORE_FIRST` / `QAM_AFTER_CURRENT` / `QAM_NOT_VALID` | **MAP:** for recno ≥ 1, `QAM_RECNO_INDEX(QAM_RECNO_PAGE(r)) < rec_page` and `(page,index)` maps back to `r`. **RANGE:** the macros agree with an independent circular-window reference, incl. the wrapped queue (`cur < first`). **PARTITION:** for recno ≠ RECNO_OOB, exactly one of before-first / after-current / inside holds; `QAM_NOT_VALID == before \|\| after`. `-DQAM_SABOTAGE` drops the 1-based `- 1` in `QAM_RECNO_INDEX` and must FAIL | full `u_int32_t` recno/first/cur/q_root; rec_page 1..8 (loop-free) | ~1 s | SUCCESSFUL (macros agree with the reference; no bug) | +| `harness_qam_recno.c` | `dbinc/qam.h` `QAM_RECNO_PAGE` / `QAM_RECNO_INDEX` / `QAM_OUTSIDE_QUEUE` / `QAM_BEFORE_FIRST` / `QAM_AFTER_CURRENT` / `QAM_NOT_VALID` | **MAP:** for recno ≥ 1, `QAM_RECNO_INDEX(QAM_RECNO_PAGE(r)) < rec_page` and `(page,index)` maps back to `r`. **RANGE:** the macros agree with an independent circular-window reference, incl. the wrapped queue (`cur < first`). **PARTITION:** for recno ≠ RECNO_OOB, exactly one of before-first / after-current / inside holds; `QAM_NOT_VALID == before \|\| after`. `-DQAM_SABOTAGE` drops the 1-based `- 1` in `QAM_RECNO_INDEX` and must FAIL | full `u_int32_t` recno/first/cur; MAP over every recno ≥ 1 with q_root = 1 (queue has no subdatabases); rec_page 1..8 (loop-free) | ~1 s | SUCCESSFUL (macros agree with the reference; no bug) | | `harness_logc_hdrchk.c` | `log/log_get.c` `__logc_hdrchk` (static) | a header that passes with `*eofp == 0` is internally consistent: `hdr->len > hdr->size`, and `hdr->len <= bp_maxrec` when `bp_maxrec != 0`. Checked with the `__logc_set_maxrec` re-read stubbed both as a no-op and as a shrink (`-DL1_SET_MAXREC_SHRINK`). `-DL1_SABOTAGE` uses `<` for `<=` and must FAIL | all field values nondet (loop-free) | ~1 s | SUCCESSFUL | -| `harness_env_alloc_size.c` | `env/env_alloc.c` `__env_alloc_size`/`DB_ALLOC_SIZE` + `SET_QUEUE_FOR_SIZE` | **SIZE:** the rounded allocation covers `len` (`>= len`) and is 8-aligned with no `size_t` overflow (default and `-DE1_DIAGNOSTIC` guard-byte builds). **QUEUE:** the size-class index is in `[0, DB_SIZE_Q_COUNT]`, is the smallest class covering the chunk when `< DB_SIZE_Q_COUNT`, and the engine's clamp of an over-range index yields a valid `sizeq[]` subscript. `-DE1_SABOTAGE` uses `<` for `<=` in the class test and must FAIL | `len` 0..64 MB (loop ≤ 11) | ~1 s | SUCCESSFUL | +| `harness_env_alloc_size.c` | `env/env_alloc.c` `__env_alloc_size`/`DB_ALLOC_SIZE` + `SET_QUEUE_FOR_SIZE` | **SIZE:** the rounded allocation covers `len` (`>= len`) and is 8-aligned with no `size_t` overflow (default and `-DE1_DIAGNOSTIC` guard-byte builds). **QUEUE:** the size-class index is in `[0, DB_SIZE_Q_COUNT]`, is the smallest class covering the chunk when `< DB_SIZE_Q_COUNT`, and the engine's clamp of an over-range index yields a valid `sizeq[]` subscript. `-DE1_SABOTAGE` uses `<` for `<=` in the class test and must FAIL | `len` 0..SIZE_MAX−64 (loop ≤ 11) | ~1 s | SUCCESSFUL | | `harness_bt_roundtrip.c` | `btree/bt_compress.c` `__bam_defcompress` + `__bam_defdecompress` | **round trip:** for any prevKey/prevData/key/data, `decompress(compress(…))` with the same prev returns exactly `(key, data)` — size and bytes. Uses the REAL `db_compint.c` codec. `-DB2_SABOTAGE` drops the duplicate-path magic byte on compress and must FAIL | key/data/prev ≤ 4 bytes (6 blows the 5-min budget; structural paths all covered, varint widths are harness_varint's job) | ~2 min/arm | SUCCESSFUL | `run.sh` runs `okitem` twice: on the real engine macro (→ `VERIFICATION diff --git a/test/cbmc/harness_env_alloc_size.c b/test/cbmc/harness_env_alloc_size.c index b42b059dcf..3b392e0597 100644 --- a/test/cbmc/harness_env_alloc_size.c +++ b/test/cbmc/harness_env_alloc_size.c @@ -32,9 +32,8 @@ * modelled as ALLOC_ELEMENT_SIZE below (its real LP64 layout: two * SH_TAILQ_ENTRY of two db_ssize_t each, plus two uintmax_t). * - * Bound: len in 0..LEN_MAX (a region chunk, far below SIZE_MAX; the allocator - * is never asked for a size near the address-space limit, where the - * `len + overhead + align` sum would of course overflow). Loop-free + * Bound: len in 0..SIZE_MAX-64; only the last 64 values, where + * `len + overhead + align` must overflow, are excluded. Loop-free * apart from the <= 11-iteration SET_QUEUE_FOR_SIZE loop. */ @@ -93,10 +92,8 @@ typedef unsigned int u_int; } while (0) /* --- end verbatim macros --- */ -/* The largest size class is 1024 << 10 == 1 MB. Bound len well below - * SIZE_MAX (see header): a few MB covers every region-chunk request and - * keeps the overhead+alignment sum from overflowing size_t. */ -#define LEN_MAX ((size_t)0x4000000) /* 64 MB */ +/* Exclude only the top 64 values, where overhead + alignment must wrap. */ +#define LEN_MAX ((size_t)-1 - 64) /* all of size_t short of the rounding */ size_t nondet_size(void); diff --git a/test/cbmc/harness_qam_recno.c b/test/cbmc/harness_qam_recno.c index 1152e0a1e8..a0f4459780 100644 --- a/test/cbmc/harness_qam_recno.c +++ b/test/cbmc/harness_qam_recno.c @@ -158,8 +158,10 @@ void harness(void) * arithmetic stays inside u_int32_t without wrap (the engine's * q_root is 1 and page numbers are bounded by the file size; * here we just keep (r-1)/rec_page + q_root from overflowing). */ - __CPROVER_assume(r >= 1 && r <= 0x10000); - __CPROVER_assume(q.q_root <= 0x10000); + __CPROVER_assume(r >= 1); + /* Queue has no subdatabases: base_pgno is 0, so q_root is 1 + * (qam_open.c __qam_open). Every recno >= 1 is covered. */ + __CPROVER_assume(q.q_root == 1); db_pgno_t pg = QAM_RECNO_PAGE(&q, r); u_int32_t idx = QAM_RECNO_INDEX(&q, pg, r); From 0e20b93268744929821a58ae454c6fd3442e7895 Mon Sep 17 00:00:00 2001 From: Greg Burd Date: Wed, 4 Nov 2026 14:43:23 -0500 Subject: [PATCH 15/15] test/cbmc: preprocessor lines at column 0 in harness_bt_decompress.c (s_chk_defines) --- test/cbmc/harness_bt_decompress.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cbmc/harness_bt_decompress.c b/test/cbmc/harness_bt_decompress.c index 4cb0a82165..b9e0ddcda2 100644 --- a/test/cbmc/harness_bt_decompress.c +++ b/test/cbmc/harness_bt_decompress.c @@ -203,7 +203,7 @@ b1_fixed_defdecompress(dbp, prevKey, prevData, compressed, destKey, destData) * sum, or prefix + suffix and size + suffix wrap and the copies * below run with a huge length. */ - #ifndef B1_NO_WRAP_CHECK +#ifndef B1_NO_WRAP_CHECK if (prefix > prevData->size || suffix > compressed->size - size || suffix > UINT32_MAX - prefix)