s12-stm32-hal

Identical ANSI C99 business logic compiled for STM32 (ARM Cortex-M4) and S12/S12X (m68hc12).

One byte-identical copy of the same ANSI C99 business logic (app/), calling only a function-pointer "ops" struct HAL, compiles, links, and behaves identically on an STM32F405 (ARM Cortex-M4) and an S12/S12X (m68hc12), with no platform #ifdef in shared code. Verified with no real hardware.

This is proven by a triangulation with four independent legs:

1. Host (mock HAL + unit tests + a mutation gate that proves the tests can fail),
2. ARM emulators (QEMU and Renode run the real firmware image),
3. S12 execution (GNU m68hc11 simulator runs the real firmware),
4. Equivalence by construction (source trees are hashed and must be byte-identical).

Every gate is a Nix derivation whose checkPhase and all of them are wired into nix flake check.

Repo layout

hal/
├── flake.nix                  # packages, checks, devShell
├── README.md                  # this file
├── app/                       # business logic
├── hal/
│   ├── include/               # portable ops-struct HAL headers
│   ├── stm32/                 # ARM backend
│   └── s12/                   # S12 backend
├── platform/                  # wires shared app to cw/s12/stm32 peripherals
├── s12/                       # m68hc12 toolchain + firmware package + smoke firmware
└── tests/
    ├── vectors/               # vec1-3.{in,expected}: UART byte-stream goldens
    ├── host/                  # unit tests + vector_runner + mock HAL + host package
    ├── arm/                   # QEMU + Renode harnesses
    ├── s12/audit.sh           # S12 artifact audit
    └── tools/                 # test scripts

Setup

Install Nix with flakes enabled, then verify from the repo root:

# /etc/nix/nix.conf (or ~/.config/nix/nix.conf):
#   experimental-features = nix-command flakes
nix flake check

Docker is only needed for the optional CodeWarrior differential tier (cw/container.nix). Everything else is pure Nix, no other build system required.

Walkthrough

Toolchain

• Host gcc builds the host unit tests and vector runner (tests/host/default.nix).
• STM32 (ARM): arm-none-eabi gcc via nixpkgs pkgsCross.arm-embedded (platform/stm32/default.nix).
• m68hc12 toolchain, built from source: binutils 2.19.1a (s12/binutils.nix), gcc 4.3.6 patched for two m68hc12 codegen bugs (s12/gcc.nix), and gdb 17.2 built with --target=m68hc11-elf --enable-sim plus the repo's own S12 peripheral models spliced into the sim tree (s12/gdb.nix).
• CodeWarrior under Wine in Docker (cw/container.nix) for optional validation, not part of nix flake check.

Polymorphism in C via function-pointer tables

The ancient m68hc12 compiler generates poor code for virtual calls and the two compilers must agree on ABI. See contract headers in hal/include, for example hal/include/hal_uart.h. Note the static inline wrappers, which let the compiler inline the u->ops->fn() dispatch into callers. The business logic (app/app.c) sees only hal_* functions. No register, no vendor API, no platform token. Each backend then fills in a concrete ops table and instance. For example, on S12 (hal/s12/hal_s12_uart.c), the SCI1 driver is register-level bare metal.

Compile targets

nix build .#arm .#s12 .#host

This produces three bundles:

• result/bin/: ARM .bin and .elf files (+ app-qemu.* for 128 KB-RAM QEMU variant)
• result-1/bin/: S12 .elf and .s19 files
• result-2/bin/: host test and vector runner

Shared code checks

nix build .#checks.x86_64-linux.lint
nix build .#checks.x86_64-linux.cppcheck
nix build .#checks.x86_64-linux.fanalyzer

These checks print errors when encountering:

• lint (tests/tools/lint.sh): C++ virtuals, #ifdef STM32/#ifdef S12 in shared code, heap, #pragma pack
• cppcheck: dead stores, leaks, uninit reads, overflow paths
• fanalyzer: double-free, use-after-free, NULL-deref across calls

Test failure paths

nix build .#checks.x86_64-linux.host-tests
nix build .#checks.x86_64-linux.host-sanitize
nix build .#checks.x86_64-linux.mutation-gate

• host-tests: unit + vector suite on host via mock HAL, gated on >=90% gcov
• host-sanitize: same suite rebuilt with ASan/UBSan, halting on any finding
• mutation-gate: applies mutation patches and requires the suite to catch each one

tests/vectors/ holds three vecN.in/vecN.expected input/output pairs that all three checks feed to vector_runner:

• host-tests and host-sanitize: vector_runner.c is compiled (in both builds) and run with all three pairs. It drives the app through the mocked HAL feeding tick/bytes/fail uart.* commands, then comparing the mock UART's captured output byte-for-byte against .expected.
• mutation-gate: its HOST_BUILD_CMD embeds the same vector_runner invocation with all three pairs, so each mutation must not break vector conformance.

ARM emulators

These gates boot the real .#arm ELF and compare its output against the same goldens above.

nix build .#checks.x86_64-linux.qemu-vectors
nix build .#checks.x86_64-linux.renode-traces

• qemu-vectors (tests/arm/run_qemu.sh, tests/arm/run_qemu.py): qemu-system-arm (netduinoplus2, STM32F405, USART2) injects each vector's bytes into the serial line and diffs against the goldens. vec3 is mock-only.
• renode-traces (tests/arm/run_renode.sh, tests/arm/check_traces.py): independent STM32F4 implementation with same byte-diff, plus assertions on emulated peripheral state (LED toggle count == TIM2 tick count, tick period consistent with the model clock).

S12 artifact audit and execution

Checks on toolchain itself:

nix build .#checks.x86_64-linux.toolchain

Artifact audit

nix build .#checks.x86_64-linux.s12-audit # runs tests/s12/audit.sh
S12=$(nix build --no-link --print-out-paths .#s12)
B=$(nix build --no-link --print-out-paths .#m68hc12-binutils)

tests/s12/audit.sh checks: memory map, vectors in place, ops dispatch present, no C++ runtime, within the flash budget.

$B/bin/m68hc12-elf-readelf -S $S12/bin/app.elf

  [ 1] .text             PROGBITS        0000c000 001000 000b46 00  AX  0   0  1
  [ 2] .rodata           PROGBITS        0000cb46 001b46 000030 00   A  0   0  1
  [ 3] .data             PROGBITS        00000800 002800 00001b 00  WA  0   0  1
  [ 4] .bss              NOBITS          0000081b 00081b 000008 00  WA  0   0  1
  [ 5] .vectors          PROGBITS        0000ff80 002f80 000080 00   A  0   0  1

$B/bin/m68hc12-elf-nm $S12/bin/app.elf

0000c846 T TIM0_ch0_isr
0000c02a T app_init
0000c0d6 T app_poll
0000c347 T app_timer_tick
0000cb60 r hal_gpio_ops_s12
0000cb6a r hal_uart_ops_s12
0000cb70 r hal_timer_ops_s12
00000800 D led_portb
00000809 D uart_sci1

$B/bin/m68hc12-elf-size -A $S12/bin/app.elf

.text             2886   49152
.rodata             48   52038
.data               27    2048
.bss                 8    2075
.vectors           128   65408

$B/bin/m68hc12-elf-objdump -d $S12/bin/app.elf | sed -n '/<app_init>:/,/^$/p'
$B/bin/m68hc12-elf-objdump -d $S12/bin/app.elf | rg 'jsr.*(0,X|\[[0-9],X\]|\[[0-9],Y\])'
$B/bin/m68hc12-elf-objdump -s -j .vectors $S12/bin/app.elf | tail -2

    c051:	ed 06       	ldy	6,X
    c053:	ee eb 00 00 	ldx	[0,Y]      ; uart_sci1.ops
    c057:	b7 64       	tfr	Y,D
    c059:	15 00       	jsr	0,X        ; ops->init(u, baud)
    ...
    c0b1:	15 e3 00 04 	jsr	[4,X]      ; timer ops->set_callback
    c0c8:	15 e3 00 02 	jsr	[2,X]      ; uart ops->write (banner)

    c059:	15 00       	jsr	0,X
    c077:	15 00       	jsr	0,X
    c094:	15 00       	jsr	0,X
    c0b1:	15 e3 00 04 	jsr	[4,X]
    c0c8:	15 e3 00 02 	jsr	[2,X]
    c0fb:	15 eb 00 04 	jsr	[4,Y]
    c276:	15 eb 00 02 	jsr	[2,Y]
    c318:	15 eb 00 02 	jsr	[2,Y]
    c36f:	15 eb 00 06 	jsr	[6,Y]
    c891:	15 00       	jsr	0,X

 ffe0 c028c028 c028c028 c028c028 c028c846  .(.(.(.(.(.(.(.F
 fff0 c028c028 c028c028 c028c028 c028c000  .(.(.(.(.(.(.(..

S12 simulator boot

nix build .#checks.x86_64-linux.gdb-sim

.#m68hc12-gdb (gdb 17.2, --target=m68hc11-elf --enable-sim) boots the real ELF under target sim, breaks at main, and proves the startup .data ROM->RAM copy ran by byte-comparing __data_load (ROM image) against __data_start (RAM copy).

Interactive, from the devShell:

nix develop
m68hc11-elf-gdb result/bin/app.elf
(gdb) target sim
(gdb) load
(gdb) break main
(gdb) run

S12 peripheral models

nix build .#checks.x86_64-linux.s12-sim-model

The gdb sim has no SCI1/TIM0/GPIO peripherals. The repo writes them (s12/sim-model/s12_sci1.c, s12/sim-model/s12_tim0.c, s12/sim-model/s12_gpio.c) and copies them into the sim tree at gdb build time (s12/gdb.nix).

S12 vector byte-diff

nix build .#checks.x86_64-linux.s12-vectors

S12 firmware, executing on a 68HC12 core model, must produce the same bytesthe host and both ARM emulators produced, against the same tests/vectors/ goldens:

S12 timer trace

nix build .#checks.x86_64-linux.s12-timer-trace

Proves the vector 0xFFEE TIM0 ISR really toggled the LED once per timer match under the simulator, asserting the TIM0 ch0 tick counter equals the PORTB pin-0 toggle counter.

Equivalence gate

nix build .#checks.x86_64-linux.equivalence

Both .#arm and .#s12 consume the same source tree. The gate (tests/tools/equivalence.sh) hashes app/, hal/include/, hal/src inside each build's own filtered source store path and requires them byte-identical.

Known limitations

Limitation	Current state / Workaround
Renode timer model runs at 10 MHz, not 16 MHz	Firmware's own config is asserted (PSC/ARR = 15999/99 -> 100 ms), measured period asserted against the model-consistent value within 20 %.
QEMU USART single-byte RX race	Just retry
Renode .log artifacts not byte-reproducible under nix build --rebuild	wall-clock timestamps/tick-count jitter not resolved yet
gdb sim needs TFLG1 polling	gdb sim quirk: TIM0 compare hardware event never self-fires
S12 firmware has no float/long long (gcc 4.3.6 backend ICEs)	uint8/16/32 business logic is unaffected, but big oof