Fix-Point opened a new pull request, #3985: URL: https://github.com/apache/nuttx-apps/pull/3985
## Summary **CI-breaking `uint128_t` typedef clash between NuttX `<stdint.h>` (`__INT128_DEFINED`) and the vendored HACL `krml/types.h`, fixed minimally: a single `#ifdef __INT128_DEFINED` block (hoist system-header parse + token redirect), +7/−0 in one file, upstream include order untouched, inert without `__INT128_DEFINED`.** Building the vendored HACL* hash code (`Modules/_hacl`) of interpreters/python currently fails on NuttX with `conflicting types for 'uint128_t'`: NuttX `<stdint.h>` typedefs `uint128_t` to the native `unsigned __int128` whenever `__INT128_DEFINED` is set (arch `types.h`, under `__SIZEOF_INT128__`), colliding with the `uint128_t` typedef of the vendored `krml/types.h` struct. The fix redirects the name instead of renaming its uses. One `#ifdef __INT128_DEFINED` block just before the typedef in `Modules/_hacl/include/krml/types.h`: 1. hoists the parse of `krml/internal/target.h` (the krml system-header dependency set; on NuttX `<stdio.h>` reaches `nuttx/lib/math32.h`, the only header using `uint128_t` natively) so platform headers keep their native typedef, and 2. redirects the `uint128_t` token to a private alias of the krml struct (`#define uint128_t __FStar_UInt128_uint128`), so the upstream typedef line and all HACL code keep the upstream spelling but bind to the struct. The redirect then stays in effect for the rest of the translation unit. Includes keep the upstream order (zero deleted lines); the whole block is a no-op where `__INT128_DEFINED` is not set. Shipped as patch 0022 of the existing interpreters/python patch series (plus one Makefile line applying it), following the established patch mechanism. ## Impact - **Build path only**: confined to the interpreters/python build (the patch series applied to the unpacked CPython tree); nothing outside `interpreters/python` changes. - **No API, ABI, or runtime behavior change**: every digest result stays byte-identical (see Testing). - **Zero effect on non-NuttX / non-`__INT128_DEFINED` platforms** (e.g. arm-none-eabi and AVR targets, glibc hosts): the entire block is `#ifdef`-guarded. - Known limit (documented in the patch comment): a platform macro whose body spells `uint128_t` (e.g. NuttX `FLS128`) must be used after `#undef uint128_t`. ## Testing Verification matrix (host: Ubuntu 22.04.5 LTS x86-64; gcc 13.1.0, clang 14.0.0, arm-none-eabi-gcc 10.3.1, avr-gcc 5.4.0; real NuttX headers with `__INT128_DEFINED` active, i.e. CI-faithful): **30 PASS / 0 FAIL**. - **Reverse reproduction**: pristine (unpatched) `Modules/_hacl` + NuttX `<stdint.h>` reproduces the CI error verbatim: `error: conflicting types for 'uint128_t'; have 'struct FStar_UInt128_uint128_s'`. - **Compile matrix** — all four `Modules/_hacl/*.c` (`Hacl_Hash_MD5/SHA1/SHA2/SHA3`) build clean: gcc x86-64 and clang x86-64 with the redirect active (`__INT128_DEFINED`), plus gcc `-m32`, `arm-none-eabi-gcc`, `avr-gcc`. - **Runtime semantics** (executed on host x86-64): MD5/SHA1/SHA2-224/256/384/512 — including the streaming multi-update 128-bit length path of SHA-384/512 — and SHA3-224/256/384/512 digests are byte-identical to Python `hashlib` in all four binding configurations (patched guard-off, patched guard-on, unpatched baseline, unpatched arch types). A `_Generic` probe confirms `uint128_t` binds to `FStar_UInt128_uint128` (size 16) inside `_hacl` TUs in every configuration. - **Mixed-TU stress** (`krml/types.h` + `nuttx/lib/math32.h` in one translation unit): compiles and runs correctly (native `umulh64` semantics + HACL struct semantics) on gcc x86-64, clang x86-64, gcc `-m32`; compiles on `arm-none-eabi-gcc` and `avr-gcc` (compile-only targets). - **Full patch series**: 0001..0022 apply in order to a freshly extracted CPython v3.13.0 tree; the resulting `types.h` is byte-identical to the verified reference and `fstar_uint128_struct_endianness.h` remains upstream-untouched. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
