diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml new file mode 100644 index 0000000000..71ee425958 --- /dev/null +++ b/.github/workflows/cbmc.yml @@ -0,0 +1,46 @@ +# 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 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: + 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/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 | diff --git a/test/cbmc/README.md b/test/cbmc/README.md index 4b35154204..c4ad6e7684 100644 --- a/test/cbmc/README.md +++ b/test/cbmc/README.md @@ -55,11 +55,26 @@ 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` | - -`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). +| `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_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; 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..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 +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 +92,198 @@ 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 +## 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 (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`. + +### 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`) + +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 + +`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 counterexample (`VERIFICATION FAILED`). Investigation showed it is a **real @@ -85,7 +291,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 +341,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 +350,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_ackpolicy.c b/test/cbmc/harness_ackpolicy.c new file mode 100644 index 0000000000..74099afc08 --- /dev/null +++ b/test/cbmc/harness_ackpolicy.c @@ -0,0 +1,541 @@ +/*- + * Copyright (c) 2026 libdb contributors. All rights reserved. + * + * SPDX-License-Identifier: Sleepycat + * + * See the file LICENSE for redistribution information. + */ + +/* + * CBMC harness H4: the repmgr ack-policy durability decision -- + * got_acks (src/repmgr/repmgr_net.c:1117) and the needed/quorum computation + * in __repmgr_send (src/repmgr/repmgr_net.c, DB_REP_PERMANENT block, the + * "switch (policy)" at ~line 433 through the needed==0 / 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/harness_bt_decompress.c b/test/cbmc/harness_bt_decompress.c new file mode 100644 index 0000000000..b9e0ddcda2 --- /dev/null +++ b/test/cbmc/harness_bt_decompress.c @@ -0,0 +1,480 @@ +/*- + * 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 UINT32_MAX 4294967295U +#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; + +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 + * 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_int8_t sink = 0; + /* The real int32 decoder reads the leading `w` bytes of buf. */ + for (k = 0; k < w; k++) + 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 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) + 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. + * + * 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; + + /* Unmarshal prefix and suffix */ + 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); + + /* + * 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); + } + + /* 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); + 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); + + /* 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); +} +#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 + + +/* + * 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/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/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/harness_env_alloc_size.c b/test/cbmc/harness_env_alloc_size.c new file mode 100644 index 0000000000..3b392e0597 --- /dev/null +++ b/test/cbmc/harness_env_alloc_size.c @@ -0,0 +1,148 @@ +/*- + * 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..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. + */ + +#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 --- */ + +/* 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); + +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/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/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/harness_qam_recno.c b/test/cbmc/harness_qam_recno.c new file mode 100644 index 0000000000..a0f4459780 --- /dev/null +++ b/test/cbmc/harness_qam_recno.c @@ -0,0 +1,200 @@ +/*- + * 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); + /* 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); + + __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/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 1af21a288f..b48f4c0012 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 @@ -50,44 +54,120 @@ 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 +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 +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 +run b2-roundtrip harness_bt_roundtrip.c harness --unwind 6 # B2 compress/decompress round trip -# 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 $SOLVER --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" +# 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 +sabotage() { + local name=$1 file=$2 func=$3; shift 3 + printf '=== %-14s ' "$name" + local tmp; tmp=$(mktemp); SECONDS=0 + "$CBMC" "$file" -Istubs --function "$func" $SOLVER "$@" >"$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 +# 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 +# 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 \ + --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 +# 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 +# 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 +# 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" +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