Skip to content

Reject Bedrock2 C outputs built for the wrong word size - #2399

Draft
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2509-bedrock2-word-width
Draft

Reject Bedrock2 C outputs built for the wrong word size#2399
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2509-bedrock2-word-width

Conversation

@JasonGross

Copy link
Copy Markdown
Collaborator

Summary

  • emit an exact target-word-width assertion in the Bedrock2 C prelude
  • regenerate all checked-in Bedrock2 C outputs with the assertion
  • compile only native-width outputs in the generated-C test and verify that a mismatched output is rejected
  • document the Bedrock2 target-width requirement

Rationale

Bedrock2 uses uintptr_t for both addresses and arithmetic words. Previously, compiling a _32.c output for a 64-bit target made _br_load and _br_store access eight bytes while generated limb offsets advanced by four bytes. That caused overlapping limb accesses, a four-byte overrun at the end of caller buffers, and incorrect field arithmetic.

The generator already receives the synthesis word size. This change preserves Bedrock2’s pointer-sized word model and turns any mismatch into a compile-time error before the affected code can run. The checked-in generated artifacts now reject both 32-on-64 and 64-on-32 mismatches. This addresses Scrutineer finding #2509.

Testing

  • opam exec -- make src/Bedrock/Field/Stringification/Stringification.vo EXTERNAL_DEPENDENCIES=1 -j2
  • make -f Makefile.examples only-test-bedrock2-files CC=cc
  • make -f Makefile.examples only-test-bedrock2-files CC=clang
  • git diff --check

A genuine 32-bit compiler/sysroot was not available locally, so successful _32.c compilation on a 32-bit host was not executed. The generated assertion is symmetric, and its rejection path is covered on this 64-bit host.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.

@JasonGross
JasonGross force-pushed the codex/fix-2509-bedrock2-word-width branch from 7da00ff to f1f7a3d Compare September 2, 2026 04:09
@JasonGross

Copy link
Copy Markdown
Collaborator Author

The five platform-specific failures had the same cause: the checked-in Bedrock2 outputs contained one extra blank line before the new assertion compared with freshly generated output. The 31 artifacts now match the generator. GCC and Clang both compile the native-width corpus and reject the mismatched-width sample with the expected diagnostic. The Alpine failure was unrelated infrastructure trouble while setup-alpine downloaded apk-tools.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant