Repository navigation
Conversation
The CBMC harnesses in test/cbmc cover six small functions, and their CI workflow was never enabled. This plans the next targets, ranked by what a wrong answer costs: - the replication election decisions (winner selection, tally, majority intersection) and the repmgr ack-policy durability decision; - btree prefix decompression, which reads a varint before checking it has the bytes; - queue record arithmetic across wrap-around; - the log header check and the region allocator's size classes. Each harness runs the real code, has a sabotage build that must fail, and a verbatim copy carries a drift check against src/.
…025 C0) The harnesses never ran in CI: the workflow was staged as test/cbmc/cbmc.yml.workflow and never copied into .github/workflows. It is now .github/workflows/cbmc.yml, and runs on every PR and master push. It has no paths filter, since a filter listing files skips changes to files nobody remembered to add. The okitem harness had drifted from the engine. It carried a private, unparenthesised copy of HPAGE_PTYPE, and run.sh's okitem(REAL) arm expected verification to FAIL, so it kept "reproducing" the bug for weeks after 2ca8126 fixed the real macro. The harness now uses the real macro and verifies. -DHPAGE_PTYPE_SABOTAGE restores the old macro as a sabotage arm, and that build must fail. check_copies.sh guards the other side of the same problem. A harness that copies a static function proves a property of the copy, so every "BEGIN verbatim copy of <func> from <src>" block must still match <src>, comparing code tokens and ignoring comments. A one-token change to the __dd_find copy makes it fail. run.sh runs it.
Verifies the real, verbatim __rep_cmp_vote (src/rep/rep_elect.c:1101) over 3
nondeterministic votes, with rep->sites advanced the way __rep_tally does.
Properties proved (harness, harness_likepri):
(b) a priority-0 non-REPCTL_ELECTABLE vote never wins;
(c) if any non-zero-priority vote is present, the winner has non-zero prio;
(d) among like-priority votes at the SAME data_gen, the winner maximises
(LSN, priority, tiebreaker) and is order-independent.
Sabotage arm -DCMPVOTE_SABOTAGE swaps LOG_COMPARE's order arms and fails (d).
FINDING (documented in README, not fixed here): property (a) order
independence does NOT hold. Two sites tallying the same VOTE1 set in different
orders can pick different phase-1 winners, for two reasons: the first vote gets
a special "becomes winner outright" path (sites==1), and the comparator's last
arm (equal LSN => priority/tiebreaker) is not gated by data_gen equality, so
the relation is not even a consistent order. This is NOT a safety bug: the
VOTE2 majority requirement (I_HAVE_WON: votes >= nvotes) means a candidate is
elected only if a majority independently chose it, and two majorities of one
group intersect (H3). Worst case is a rare failed-to-settle election round, a
liveness cost, not split brain. lts/2026.10.7 has identical code. Flagged to
the lead for a possible follow-up (make the comparator a total order, or fix
the comment) + LTS backport.
No engine change (test/cbmc-expand rules). CBMC 6.9.0, ~2 s per arm.
Verifies the real, verbatim __rep_tally (src/rep/rep_elect.c) over sequences of
up to 6 (eid, egen) votes into a region tally array of capacity 5 (R_ADDR and
__rep_grow_sites stubbed; asites==nsites==CAP so the no-grow path is taken and
grow_sites is asserted unreachable).
Properties proved:
- no OOB on the tally array (reads tally[i], write tally[*countp]);
- each eid is counted at most once (no two live slots share an eid);
- a lower/equal egen for a seen eid returns DB_REP_IGNORE with no count
change; a higher egen updates in place with no count change;
- *countp equals the number of distinct eids and never exceeds capacity.
Honest bound model per the brief: the only capacity guard is the entry test
nsites > asites. With distinct eids <= CAP == asites, *countp cannot reach
asites without a grow, so tally[CAP] is never written -- the "indexed at
*countp == asites" hazard does not occur.
Sabotage -DTALLY_SABOTAGE turns the "already seen this eid" test from == to !=
(a double-count bug); it fails hard -- OOB write past the array plus every
count invariant broken.
No engine change. CBMC 6.9.0, ~1 s.
Proves the two facts the one-master-per-generation safety argument rests on,
over the real ELECTION_MAJORITY macro (verbatim from src/dbinc/rep.h:534):
(1) 2*ELECTION_MAJORITY(n) > n for all nsites in [1,64], so any two
majorities of the same group intersect -- also proved constructively:
two nondeterministic subsets of N=8 sites each of size >= majority must
share a member (CBMC finds no disjoint pair).
(2) the sub-majority warning test in __rep_elect_int, `ack <= nsites/2`, is
exactly equivalent to `ack < ELECTION_MAJORITY(nsites)` for all nsites
and all ack in [0,64].
Sabotage -DMAJORITY_SABOTAGE uses n/2 (floor) for the majority; both arms fail
(disjoint even-n majorities appear, warning equivalence breaks).
Pure arithmetic, no engine struct. CBMC 6.9.0, ~1 s each.
Models got_acks (src/repmgr/repmgr_net.c:1117) and the needed/quorum
computation in __repmgr_send (the DB_REP_PERMANENT block). got_acks iterates
db_rep->sites and dereferences REPMGR_SITE, so its decision logic (the
accumulate loop + the switch (policy)) is transcribed faithfully into
got_acks_model over the exact per-site facts it reads (SITE_PRESENT,
SITE_HAS_PRIO, SITE_ELECTABLE, max_ack>=lsn), with the source lines named
inline; the needed/quorum block is copied into compute_needed_quorum, likewise
annotated. This is not a function boundary, so a verbatim #include/copy is not
possible; the transcription is marked per the brief.
Properties proved over all group shapes of <= 4 remote sites (+ master):
- QUORUM "no election can lose it": durable => every electable-site majority
(ELECTION_MAJORITY over master + electable peers) contains a holder (the
master or an acked electable peer). The "every majority" quantifier is
discharged by CBMC over a nondeterministic membership bitmap.
- 2-site: STRICT => quorum 0 (master-only durable, the client won't
self-elect); non-strict => the lone client must ack. Stated separately.
- ALL_PEERS: durable => every electable peer acked (and no unknown-prio
present site).
- ONE_PEER: durable => some electable peer acked.
- Shortcuts: needed==0 is durability-safe (reachable only when no electable
peers exist, so the master is the whole majority); available<needed refuses
and got_acks would also refuse.
Sabotage -DACKPOLICY_SABOTAGE counts non-electable acks as peers, inflating
peers_acked; QUORUM and ONE_PEER contracts then fail.
No engine change, no finding. CBMC 6.9.0; full suite (all H1-H4 + prior) ~45 s.
Coccinelle convention checksNo new violations. ✅ Resolved since baseline (3) -- update dist/cocci/baseline.txt to lock these in. |
ABI diff vs
|
|
Lead on the H1 finding: Counterexample 2 may be a durability bug, not only liveness. Arm D, A history that could reach it, which is not yet constructed:
H3 proves that two masters cannot win the same egen. It says nothing about which site wins, and choosing a site with older data is how a durable commit is lost. Equal LSNs are a coincidence, so the window is narrow, but it is not zero. Disposition: not a confirmed bug until it reproduces against the real code. The follow-up is to drive this history in a TCL rep test with controlled message delivery, or a libcmc model of the election decision. If it reproduces, the fix is to gate arm D on H4 note: the ack-policy harness is a transcription of a block inside |
…FC 0025 C2) harness_bt_decompress.c proves the memory safety of the default compressed btree key/data decoder over every input in a stated bound. The REAL, unmodified engine code (verbatim copy, guarded by check_copies.sh) FAILS: __bam_defdecompress reads each varint's leading byte via __db_decompress_count_int, and the magic byte *s at offset 0, BEFORE it checks the compressed buffer is long enough. A corrupt or truncated compressed item -- a trust boundary, since compressed pages come from disk -- over-reads up to one byte past compressed->size at each of the three varint sites, and reads the first byte of a zero-length item with no check at all. CBMC counterexample (size==0 the cheapest): *s and the count_int lookahead read "pointer outside object bounds". run.sh runs two arms: b1-fixed (-DB1_FIXED, the proposed bound-before-read fix) VERIFIES; b1-decompress (the unmodified engine code) is a must-FAIL arm that documents the live bug until fix/bt-decompress-bounds lands, mirroring how okitem ran before 2ca8126. The whole suite stays ~26 s (cadical). The varint helpers' arithmetic is already proved against the real source by harness_varint.c; here they are modelled by their exact read footprint (the count reads buf[0]; the int32 reads the leading width bytes from the real __db_marshaled_int_size table), which is the only thing B1's bounds proof depends on and keeps the SAT formula inside the suite budget.
The -DB1_FIXED variant's first non-dup count_int check read an uninitialised `size`; drop it, since the top `compressed->size < 1` guard already covers the offset-0 read, matching fix/bt-decompress-bounds exactly. Still VERIFIES.
|
C2 added B1
Q1/L1/E1/B2 harnesses coming to this branch next. |
harness_qam_recno.c verifies the qam.h record<->(page,index) mapping and the circular live-window predicates over the whole u_int32_t range. MAP: recno>=1 gives an in-range index that maps back to recno. RANGE: QAM_OUTSIDE_QUEUE agrees with an independent circular-window reference, including the wrapped queue (cur < first). PARTITION: for recno != RECNO_OOB exactly one of before-first / after-current / inside holds, and QAM_NOT_VALID == before || after. The macros are verbatim from qam.h (member access adapted to local structs). No engine finding -- the macros agree with the reference. -DQAM_SABOTAGE drops the 1-based "- 1" in QAM_RECNO_INDEX and must FAIL.
L1 harness_logc_hdrchk.c: the verbatim static __logc_hdrchk (check_copies- guarded). Proves a header that passes with *eofp==0 is internally consistent (hdr->len > hdr->size, and hdr->len <= bp_maxrec when bp_maxrec != 0), with the __logc_set_maxrec re-read stubbed as both a no-op and a shrink. Sabotage (L1_SABOTAGE, a separate hand-written copy, like harness_tally's) uses < for <= and FAILs. E1 harness_env_alloc_size.c: __env_alloc_size/DB_ALLOC_SIZE and SET_QUEUE_FOR_SIZE (verbatim macros + DB_ALIGN). SIZE: the rounded allocation covers len and is 8-aligned with no size_t overflow (default + DIAGNOSTIC guard-byte). QUEUE: the size-class index stays in [0, DB_SIZE_Q_COUNT], is the smallest class covering the chunk, and the clamp of an over-range index is a valid subscript. Sabotage (E1_SABOTAGE) uses < for <= in the class test and FAILs at the boundary. No engine finding for either. Whole suite ~28 s (cadical); 6 verbatim copies match src/.
harness_bt_roundtrip.c proves decompress(compress(key,data)) == (key,data) for the default compressed-btree codec, given the same prevKey/prevData. Both __bam_defcompress and __bam_defdecompress are verbatim copies (check_copies- guarded); the varint codec is the REAL db_compint.c (#include). -DB2_SABOTAGE drops the duplicate-path magic byte on compress, so decompress misreads a duplicate record and the round trip FAILs. No engine finding. Bound: key/data/prev <= 4 bytes -- at the brief's 6 the #include'd codec's full arithmetic pushes this one harness past the suite's 5-min budget; <= 4 still covers every structural path (empty/prefix/suffix/full/duplicate) and the multi-byte varint widths are already proved by harness_varint.c. Whole suite ~4.0 min on a fast host (B2's two arms are ~110 s + ~103 s), 8 copies match.
The B1 and B2 btree-compression harnesses run the real varint codec and take ~2 min each, so the suite is a few minutes now, not under one. The 30-min job timeout is unchanged. cadical (CBMC's built-in fast SAT backend, which run.sh now selects) ships inside the cbmc binary, so no flake change is needed.
|
C2/C3 complete — all five RFC 0025 targets pushed to this branch:
Whole suite ~4 min (B1/B2 run the real varint codec; I added |
…p arm The varint model returned a value built from the bytes it read, at most about 2^17, so the proof could not see prefix + suffix wrap. The real decoder returns any u32 from a 5-byte varint. With the value nondet, the first fix (2e99a1f) fails the proof; the fix plus e067d65 verifies. The B1_FIXED arm is now a verbatim copy of the final fixed function, and a new b1-wrap arm (-DB1_NO_WRAP_CHECK) must fail.
Q1 MAP bounded recno and q_root to 0x10000. Queue has no subdatabases, so q_root is always 1 (__qam_open sets base_pgno + 1 with base_pgno 0); with that fixed, the round trip verifies for every recno >= 1. E1 bounded len to 64 MB; it verifies up to SIZE_MAX - 64, where only the rounding itself must overflow. Both sabotage arms still fail.
|
E1 resolved: the H1 finding ( The CBMC H1 finding (order dependence; "Counterexample 2", arm D bypassing Reproduced against the real engine (dev box). The precondition is reachable: Fix (#266, CBMC harness update (for this branch). A prepared patch updates Pre-existing, separate: under |
RFC 0025 — expand CBMC coverage
Branch for the CBMC coverage expansion (RFC 0025). This PR is a draft while the
phases land; each harness verifies on the real engine code and carries a
sabotage arm that must fail.
C1 (election + ack-policy decisions) — done
Four new harnesses over the replication election and the repmgr ack-policy
decisions. Each runs the real code (verbatim
staticcopies checked bycheck_copies.sh, or a faithful transcription with the source lines namedwhere the function is not a clean boundary), verifies with CBMC 6.9.0, and has
a
-D..._SABOTAGEarm that plants a realistic bug and must fail.harness_cmpvote.c__rep_cmp_vote(rep_elect.c)harness_tally.c__rep_tally(rep_elect.c)*countp== distinct eids, within capacity; no OOBharness_majority.cELECTION_MAJORITY+ sub-majority warning2*maj > n, also constructively);ack <= nsites/2==ack < majorityharness_ackpolicy.cgot_acks+__repmgr_sendneeded/quorumWhole suite (these + the prior six) runs in ~45 s.
FINDING (documented, not a safety bug):
__rep_cmp_voteis order-dependentharness_cmpvote.cproperty (a), order independence, fails on the real,unmodified code. Two sites tallying the same VOTE1 set in different arrival
orders can pick different phase-1 winners, for two reasons: the first vote gets
a special "becomes winner outright" path (
sites==1), and the comparator'slast arm (equal LSN => priority/tiebreaker) is not gated by
data_genequality, so the relation is not even a consistent order (its comment claims a
data_gen, LSN, priority, tiebreakertotal order it does not implement).This is not a safety bug: the VOTE2 phase requires a majority
(
I_HAVE_WON:votes >= nvotes) to elect, and two majorities of one groupintersect (proved in
harness_majority.c), so there is no split brain. Theworst case is a rare failed-to-settle election round — a liveness cost. The
__rep_cmp_voteinlts/2026.10.7is byte-identical, so a fix would warrantan LTS backport. Full write-up and both CBMC counterexamples in
test/cbmc/README.mdunder FINDING. Flagged to the lead; no engine changemade on this branch (per the workstream rules).
Later phases (C2/C3) land in follow-up commits on this branch.