vbpf / prevail / 24861555409

86%

push

github

Decompose Program::from_sequence into named preparation passes (#1081)

Extract the pipeline inside Program::from_sequence into individually
documented passes so the soundness-relevant transformations are easier
to audit. from_sequence now reads as orchestration.

Passes, in order:
  pass_validate_instruction_support, pass_resolve_kfunc_calls,
  pass_lower_pseudo_loads, pass_populate_nodes, pass_connect_edges,
  pass_inline_local_calls, pass_validate_tail_call_depth,
  pass_compute_callback_metadata, pass_insert_termination_counters,
  pass_extract_assertions.

Each pass has a header comment stating Reads / Writes / Throws /
Invariant. Ordering asserts guard pass_connect_edges and
pass_inline_local_calls against mis-sequencing.

Add src/test/test_cfg_builder_passes.cpp with 13 targeted tests for
invariants that were previously implicit (empty sequence rejection,
Assume materialization, jump-to-undefined / fallthrough rejection,
LoadPseudo VARIABLE_ADDR / CODE_ADDR / MAP_BY_IDX handling, callback
metadata filtering, loop-counter insertion, per-label assertions).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

223 of 224 new or added lines in 2 files covered. (99.55%)

13606 of 15251 relevant lines covered (89.21%)

4424424.55 hits per line