[SwayamInSync]

Plan item B10 (small frontend gaps), its builtins: a call of a bit-counting or byte-swapping builtin stopped its function, and a static_assert with a message crashed cpp-verify.

On the base

The example below:

bits.cpp:8:15: error: log2_floor: call to function without a verification contract: __builtin_clz
    8 |   return 31 - __builtin_clz(x);
      |               ^~~~~~~~~~~~~~~~
bits.cpp:14:15: error: top_bit: call to function without a verification contract: __builtin_clz
...
bits.cpp:20:10: error: one_bit: call to function without a verification contract: __builtin_popcount
...
Summary: 3 unresolved (construct.unsupported 3) in 0.0 s

and a function with static_assert(sizeof(int) == 4, "int is 32 bits");:

PLEASE submit a bug report to https://github.com/SwayamInSync/cpp-verify/issues/ ...
 #3 ... RecursiveASTVisitor<findUnsupportedType(...)::Finder>::TraversePackExpansionExpr(...)

The crash: the message of static_assert(c, "text") is a string literal with no type, and the scan for unsupported types in a body (findUnsupportedType) read the type of every expression before checking that it had one. static_assert(c) without a message worked.

The other constructs B10 lists were already supported, which this PR checked: character literals, __builtin_expect, default arguments, if constexpr, consteval, local type aliases, [[likely]], structured bindings of records, return Pt{a, b};, and default member initializers.

With this PR

int log2_floor(unsigned x)
  cv::pre(x != 0)
  cv::post(0 <= cv::result && cv::result < 32)
  cv::post(x >= 1u << cv::result)
{
  return 31 - __builtin_clz(x);
}

int top_bit(unsigned x)
  cv::post(cv::result >= 0)
{
  return 31 - __builtin_clz(x);
}

bool one_bit(unsigned x)
  cv::post(cv::result == (x != 0 && (x & (x - 1)) == 0))
{
  return __builtin_popcount(x) == 1;
}

Verified: log2_floor [backend=z3]
bits.cpp:14:15: error: verification failed: top_bit [builtin-argument] [backend=z3] [reason=counterexample]
   14 |   return 31 - __builtin_clz(x);
      |               ^~~~~~~~~~~~~~~~
bits.cpp:14:15: note: counterexample: x = 0
Verified: one_bit [backend=z3]
Summary: 2 verified, 1 failed in 0.2 s

Design, from the references

• CBMC models these builtins exactly, as operations on the operand's bits; Frama-C's libc gives them ACSL contracts (requires x != 0 for __builtin_clz); Verus states u32::leading_zeros through spec functions with axioms.
• A contract would make each call a modular call with an assumed postcondition. An exact definition needs nothing assumed, so the builtins are their definitions, as in CBMC, and the one undefined case is a requirement, as Frama-C's requires states it.

ASTConverter::convertBitBuiltin lowers a call to its definition over the operand, read as an unsigned machine value of the parameter's width (a mathematical argument in a contract converts to the parameter's type first, as a bitwise operand does):

• clz and ctz: a ladder of conditionals on x & 2^k != 0, with literal results;
• popcount and parity: a balanced sum of one-bit terms in a byte (the count is at most 64). Summed at the operand's width, parity of a popcount took 6 s; in a byte it takes 0.8 s;
• ffs: the ctz ladder plus one, and 0 for 0;
• bswap16/32/64: each bit at its new place, combined with |, since no two meet.

None of these operations has a check of its own: comparisons with constants, conditionals, sums without carries, and |. Constant shifts were avoided, since each would add a trivially true shift check.

GCC leaves __builtin_clz(0) and __builtin_ctz(0) undefined. That is an obligation of a new definedness kind, builtin-argument (archive tag 24, read from schema v6), where the call is evaluated: ite(Require(x != 0), v, v), as constant-table reads require their bounds. In an explicit spec, which is total, there is no check, and they count every bit of 0, as C++20's std::countl_zero does.

Two fixes to E15's places, found here

• A guard in a definedness check was passed into only when written !g || c; canonicalization folds !!c to c, so a check in a ?:'s else branch stayed at the ?:. Every disjunction in a definedness check is a guard the verifier builds, so it is passed into whatever its shape.
• A check that a postcondition is defined was anchored at the clause by overwriting its own location, so its focus was lost: cv::post(cv::result == __builtin_clz(x)) failed at the ==. An exit assert now carries its anchor (PassiveExitAssert::Anchor) apart from its condition, which keeps its location as the focus; a focus outside the function, in a lifted helper's body, still leaves the failure at the clause.

Mutants

Each mutant below, applied alone and rebuilt, is caught by bit_builtins.cpp (14 of 14):

Mutant	Change
K1	clz and ctz of 0 are not checked
K2	a spec checks clz of 0 too
K3	clz counts one fewer
K4	ctz is ffs
K5	ffs of 0 is the width
K6	a bit counts twice in popcount
K7	parity is the count
K8	bswap keeps the bytes in place
K9	a mathematical argument is not converted
K10	the bits of a signed argument are read signed
K11	the type scan reads an expression without a type
K12	builtins are not lowered
K13	a guard in a definedness check is passed into only when written !g || c
K14	a postcondition's definedness check is anchored at its operation

Tests

suite/bit_builtins.cpp (new), in the default encoding and in the integer one:

• properties: clz of a nonzero argument and its relation to the top bit; ctzll; popcount bounds and zero; bswap32 against a formula of shifts; ffs of int; parity against popcount;
• every variant at the ends of its width and at a value of mixed bits, including __builtin_ffs(INT_MIN) in a check;
• failures: clz(0) and ctz(0) (the second in a ?: branch, at its call), a postcondition calling __builtin_clz, a lifted helper's __builtin_clz in a postcondition (shown at the clause), and a wrong bound on popcount;
• a spec that counts the bits of 0;
• static_assert with a message;
• the JSON kind and obligation ID.

The definitions were also checked against values computed apart from cpp-verify (Python's integers) for 794 calls, every variant at random and edge arguments: all verify, and a wrong value fails. That table takes 103 s, so the test keeps the edges.

On the base the test stops at its first builtin, and the static_assert crashes.

On a release build of this branch, merged with main of today, the whole Verify suite (506 tests) and the unit tests pass.

Docs

Functions and loops (the builtins, with the example and its output), limitations, the kinds in tooling, chapter 18 (a builtin's argument), release notes, ARCHITECTURE, DESIGN.