fix(t27c): gen-c arithmetic traps where t27 traps, with no C undefined behaviour

[gHashTag]

Summary

t27c gen-c emitted the bare C operators for + - * / % << >>. C leaves signed overflow, a shift amount outside [0, width), a zero divisor and MIN / -1 undefined, so the generated C gave different answers at different optimisation levels. The t27b differential test (#5905) found two cases: inc(INT_MAX) passed at -O0 and trapped at -O2, and shr(1024, 40) did the reverse. The language rule is #1659: plain + - * trap on overflow and +% -% *% wrap. Zig and t27b trap mode already follow it.

Inside fn, test, bench and invariant bodies, each arithmetic operator now becomes a call to a t27_* helper. The helpers live in one guarded block, C_ARITH_PRELUDE, which is emitted only when a module uses one:

• + - * use __builtin_*_overflow.
• Shifts check the amount.
• / and % check for a zero divisor and for MIN / -1.
• The wrapping operators compute in unsigned arithmetic.

Every failure calls __builtin_trap(). _Generic picks the width, and a GNU statement expression makes sure each operand is evaluated once.

Three cases keep the infix form on purpose:

• Module-scope initializers, because they must be C constant expressions.
• Arithmetic on literals only, which the C compiler folds and diagnoses.
• + with an array or string operand, which is concatenation.

A bare literal shifted by a runtime amount ((1 << n) - 1) takes the same width the Zig backend gives it: the declared type of the local it initializes, otherwise its suffix, otherwise u32 or u64 by magnitude.

Functions changed in bootstrap/src/compiler.rs:

• C_ARITH_PRELUDE, c_arith_helper
• CCodegen::{c_is_literal_arith, c_is_pure_lvalue, gen_c_macro_arg, c_scalar_int_type, c_shift_literal_base_type}
• gen_c_expr (ExprBinary), gen_c_stmt (StmtAssign compound and StmtLocal)
• gen_c_fn, gen_c_test, gen_c_bench, gen_c_invariant, gen_c

Before / after (t27b README reproducer)

test	zig test	clang -O0 before	clang -O2 before	clang -O0 after	clang -O2 after
inc_max (inc(2147483647))	trap	pass (UBSan: overflow)	trap	trap	trap
shr_big (shr(1024, 40))	trap	trap	pass (UBSan: shift)	trap	trap
rem_neg (rem(-7, 2) == -1)	pass (#5993)	pass	pass	pass	pass

After the change, -fsanitize=undefined reports nothing at -O0 or at -O2.

Corpus effect

Measured against the master this branch started from:

• 634 of 1186 specs change gen-c output.
• No spec that compiled cleanly with clang stops compiling, and no broken spec starts compiling. Clang error lines go from 18804 to 18841. All of the increase is in specs that were already broken: macro re-reports, and string or pointer + that _Generic now refuses.
• 229 specs compile both before and after. In those, every test gives the same answer at -O0 and at -O2, with three exceptions. Each exception moves C towards Zig:
  • gf_decode_param_fp64 test_decode_neg_inf now passes. Before, a 32-bit 1 << 52 was UB and made it fail.
  • ternary_memory test_ternary_word_write_read_trit now traps. Zig traps here too, on an @intCast of -1 to u32.
  • gf16_dot4 test_intermediate_structure now traps. Zig traps here too, on a u16 multiply overflow.

specs/igla/race/ternary_mac.t27 now accumulates with acc +% prod. This is a judgement call: tools/verify_igla_race.py models the accumulator as a wrapping i32 and drives it across the INT32 edges, so checked + trapped there, as the Zig output already did. verify_igla_race.py and check_duplicate_agreement.py now copy the prelude into the functions they extract.

Verifiers that pass:

• verify_igla_race, check_duplicate_agreement, verify_multitarget, verify_trainer_c.
• verify_exhaustive on maj3 tmul negate xor2 sign0 pack2: model == C == Rust on every input.

Seals

899 seal files (536 specs) carry the new gen_hash_c. check_seal_coverage.py and check_seal_currency.py both pass.

• 892 were resealed with t27c seal --save.
• ternary_shift (2 seal files) and gft_generalize_demo (1) were sealed with --force. Their Zig tests already fail with exactly the Zig output master seals (gen_hash_zig is unchanged). They are ledgered as tests-fail in tools/seal_baseline.txt.
• clock_domain_tb and gf16_accel_tb (4 seal files) had only gen_hash_c rewritten. Their own Zig test spins forever in while !sync_ready { tick_fast(); }, so seal --save never returns. The other four hashes were checked equal before the rewrite.

Tests

• New bootstrap/tests/c_checked_arith.rs has 5 tests:
  • two check the shape of the emitted code;
  • one checks that a module with no arithmetic gets no prelude;
  • one runs 15 tests at -O0 and -O2 and checks them against the Zig/t27b answers;
  • one repeats that under UBSan.
• Unit tests updated: test_tuple_literal_and_destructuring_c, and test_wrapping_ops_all_backends_1659, which now asserts the t27_w* lowering.
• cargo test --release -p t27c: every test binary passes except core_selfhost. See below.

Blocked: core_selfhost fixpoint (#6041)

#6041 landed on master while this PR was open. Its fixpoint requires specs/compiler/core/t27core.t27, the self-hosted core, to write exactly the bytes gen-c writes. With this change, gen-c(t27core.t27) lowers its 123 body operators to t27_* calls and emits the prelude. The core still writes infix C, so core(t27core.t27) != gen-c(t27core.t27). The core's own test blocks still pass when built from the new C. To make the fixpoint hold again, the core has to learn the same lowering:

• emit the prelude;
• choose the helper per operator;
• leave literal-only and module-scope arithmetic infix;
• apply the shift-literal width rule.

This PR does not edit the core. That work is a separate change to epic #5980. The PR is opened as a draft for that reason.

Not established

• Types narrower than int (i8, u8, i16, u16) are promoted by C, so they are checked at int width and truncated on store. That is defined behaviour, but a u16 overflow that Zig traps only traps in C if it also overflows int.
• Unary minus is not checked.
• Pointer + is not supported. With a pointer operand it is now a compile error, where before it was a pointer offset.
• verify_exhaustive was run on the subset above, not on the full target list, which did not finish under machine load.
• The branch includes master as of ec1d9a61c. Master has moved since, and a final merge and reseal is needed before landing.

Closes #5974. Part of #5905.

🤖 Generated with Claude Code