Skip to content

Built but never tested: 3 dead Renode targets, ~48 unrun probe binaries, and a gate of mine that is blind to one of them #387

Description

@avrabe

[fathom (gale) — audit: things we build and never test]

Verified by me after the audit reported them. Unverified items listed separately.

1. CONFIRMED — three renode_test targets point at ELFs that have never existed

renode/BUILD.bazel:19  stm32f4_sem_test     -> elfs/stm32f4_disco_sem.elf
renode/BUILD.bazel:32  stm32l552_sem_test   -> elfs/nucleo_l552ze_q_sem.elf
renode/BUILD.bazel:45  zynqmp_r5_sem_test   -> elfs/qemu_cortex_r5_sem.elf

$ git ls-files renode/elfs/
renode/elfs/.gitkeep

Referenced by 0 workflows each. Nothing in the repo builds those ELFs. They
would fail on invocation with a missing input label, not merely go unrun.

The risk is not the dead target, it is what it implies: anyone auditing "which
architectures are Bazel-gated" sees three extra boards covered. The real CI path
(renode-tests.yml) reaches those boards a completely different way — building a
fresh Zephyr+gale ELF with west build and invoking renode-test against the
.robot files directly. So the .robot files are live; this Bazel wrapper around
them is orphaned scaffolding from docs/research/renode-multi-arch-ci.md.

And my own gate does not catch it. cargo xtask check renode-targets (added
last week, #385) hardcodes a single path:

const BUILD: &str = "benches/gust/renode-test/BUILD.bazel";

It found the gust-iso-renode gap and is blind to this one. A gate scoped to one
file, auditing a defect class that exists in two. That is the same narrowing it
was written to prevent, in the gate itself.

2. CONFIRMED — benches/gust has 50 [[bin]] targets; CI runs 2

Only gust_iso_fault_probe and gust_iso_unpriv_probe are invoked, via
cargo run --bin in kill-criteria.yml's mpu-enforcement job. No workflow runs
cargo build/check/test against benches/gust/Cargo.toml as a whole.

The other ~48 include gust_hm_probe, gust_timer_probe, gust_exec_probe,
gust_switch_probe, gust_os_tl_probe, gust_os_ts_probe, gust_two_tenant,
and the whole gust_{adc,can,dac,dma,i2c,pwm,spi}_probe family. They are
documented as manual reproduction commands in RESULTS.md / DEMONSTRATOR.md /
wave reports — and several are cited as verification evidence in rivet artifacts
(gust_os_roadmap.yaml, gust_safety_release_line.yaml).

None is hardware-dependent, so nothing structurally prevents CI from at least
compiling them. A cargo check over that crate would catch bit-rot in ~48
pieces of cited evidence for the cost of one job.

3. Reported, NOT verified by me

  • fuzz/src/bin/precondition_erasure_smoke.rs — a separate bin from the
    libFuzzer target CI does run; cited in artifacts/verification.yaml (IV-PE-001,
    method: automated-test) with "2511 cases, 0 mismatches" from one historical
    commit, never re-run as a regression.
  • mutants_test (cargo-mutants, part of //:nightly) — invoked nowhere, and
    unlike Miri it is absent from docs/safety/verification-honesty.md's
    "What Exists But Does NOT Run in CI" table.
  • miri_test — also never run, but already disclosed in that table.

Checked and clean

The audit explicitly cleared: all other Bazel targets across the root,
proofs/, proofs/lean/ (//proofs/lean:all is a genuine Bazel wildcard, not a
gap), plain/, bzl/, tools/verus-strip/; the sanitizer rules (covered by
sanitizers.yml running cargo directly); committed .o under drivers (covered by
object-freshness); and renode-test/*.elf (all consumed via LoadELF, now
17/17 gated).

Activity

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions