#!/usr/bin/env bash
#
# Layered concurrency-correctness verification for frame-alloc:
#
#   1. unit + doc tests (stable)   — functional correctness, sequential + a few
#                                    threaded stress tests.
#   2. ThreadSanitizer             — runs the allocators over real pool memory and flags data
#                                    races on the schedules that actually execute.
#   3. Miri (UB / provenance)      — the only layer that checks the crate's core
#                                    unsafe contract: reinterpreting pool bytes as
#                                    AtomicUsize, the Provenance int<->ptr casts,
#                                    the builder's writes, and every base.add(idx)
#                                    being in-bounds / aligned / correctly
#                                    provenanced. Miri is ~100-1000x slow, so this runs
#                                    a curated subset; -Zmiri-permissive-provenance is
#                                    required because the *test harness* fakes
#                                    physical memory via exposed provenance.
#   4. Miri concurrent             — the same threaded tests the TSan layer runs,
#                                    executed under Miri's weak-memory emulation
#                                    across 16 scheduler seeds (-Zmiri-many-seeds).
#                                    This is the only layer that can surface wrong
#                                    atomic orderings: TSan only flags unsynchronised
#                                    accesses, and the x86 host's TSO model hides
#                                    acquire/release mistakes at runtime. cfg(miri)
#                                    shrinks iteration counts to keep this tractable.
#   5. audit (structural invariants) — compiles with --cfg audit, which enables
#                                    per-op assertions after every alloc/free,
#                                    across the unit tests and the external
#                                    randomised occupancy oracle. Concurrent
#                                    tests are skipped.
#
# Run all layers:   ./scripts/verify.sh
# Run one layer:    ./scripts/verify.sh tsan   (or: tests | miri | miri-concurrent | audit)
#
# Archiving a run:  ./scripts/verify.sh --log            (writes validation/<layer>.log)
#                   ./scripts/verify.sh --log=DIR miri
#
# --log tees each layer's combined output to its own file and prefixes it with a
# provenance header (commit, dirty flag, host, and the toolchain versions that
# layer actually used). The nightly a Miri log was produced with is not
# reconstructable later, so an archived log without it is of little use.
set -euo pipefail
cd "$(dirname "$0")/.."

LOG_DIR=""

usage() {
    echo "usage: $0 [--log[=DIR]] [all|tests|tsan|miri|miri-concurrent|audit]" >&2
}

while [[ "${1:-}" == -* ]]; do
    case "$1" in
        --log) LOG_DIR="validation" ;;
        --log=*) LOG_DIR="${1#--log=}" ;;
        -h | --help) usage; exit 0 ;;
        *) echo "unknown option: $1" >&2; usage; exit 2 ;;
    esac
    shift
done

run_tests() {
    echo "== unit + doc tests (stable) =="
    cargo test --features stats
}

run_tsan() {
    echo "== ThreadSanitizer — data-race check on the real allocators =="
    local target
    target=$(rustc -vV | sed -n 's/host: //p')
    # The allocator concurrency tests live in the external `conformance` suite; the substring
    # concurrent` restricts both the lib and that binary to the threaded tests.
    # `mutual_exclusion_under_contention` (lib) is the Lock primitive's own race test.
    RUSTFLAGS="-Zsanitizer=thread" \
        cargo +nightly test -Zbuild-std --target "$target" --features stats \
        --lib --test conformance -- concurrent mutual_exclusion_under_contention
}

# Curated white-box unit tests that exercise the crate's core unsafe. Miri is far
# too slow to run the whole suite, so this list is chosen for coverage of the
# unsafe categories rather than breadth.
MIRI_TESTS=(
    # In-pool bitmap: placement, split/merge arithmetic, and the guarantee that
    # metadata never writes into a frame that was handed out.
    managed_frames_not_written
    bitmap_hosted_past_span_start_hole
    free_stats_split_and_merge
    # Span geometry: unaligned phys_base prefix reservation and order rounding.
    phantom_prefix_reserved_for_unaligned_phys_base
    multi_frame_count_rounds_up_to_order
    # Cache tier: depot overflow with cross-CPU reuse, and sibling-magazine steal.
    frees_overflow_into_depot_and_other_cpu_reuses
    single_frame_oom_steals_from_sibling_magazine
    # Region routing: CPU-selected allocation and address-routed donation.
    default_selector_alloc_dealloc
    add_usable_routes_to_owning_region
)

run_miri() {
    echo "== Miri — UB / provenance check on the real allocators (curated subset) =="
    MIRIFLAGS="-Zmiri-permissive-provenance" \
        cargo +nightly miri test --lib --features stats -- "${MIRI_TESTS[@]}"
}

run_miri_concurrent() {
    echo "== Miri (concurrent) — weak-memory emulation + schedule exploration =="
    MIRIFLAGS="-Zmiri-permissive-provenance -Zmiri-many-seeds=0..16" \
        cargo +nightly miri test --features stats --lib --test conformance \
        -- concurrent mutual_exclusion_under_contention
}

run_audit() {
    echo "== audit — per-op structural invariant check (sequential tests) =="
    RUSTFLAGS="--cfg audit" cargo test --features stats
}

provenance_header() {
    local layer=$1
    echo "=== frame-alloc verify.sh — layer: $layer ==="
    echo "date (UTC) : $(date -u +%Y-%m-%dT%H:%M:%SZ)"
    echo "commit     : $(git rev-parse HEAD 2>/dev/null || echo unknown)"
    if [[ -n "$(git status --porcelain --untracked-files=no 2>/dev/null)" ]]; then
        echo "tree       : DIRTY — this log does not correspond to the commit above"
    fi
    echo "host       : $(uname -srm)"
    echo "rustc      : $(rustc -V 2>/dev/null || echo unknown)"
    echo "cargo      : $(cargo -V 2>/dev/null || echo unknown)"
    case "$layer" in
        tsan | miri | miri-concurrent)
            echo "nightly    : $(rustc +nightly -V 2>/dev/null || echo 'not installed')"
            ;;
    esac
    case "$layer" in
        miri | miri-concurrent)
            echo "miri       : $(cargo +nightly miri -V 2>/dev/null || echo 'not installed')"
            ;;
    esac
    echo
}

# Dispatch one layer, teeing it to $LOG_DIR/<layer>.log when --log is set. The
# tee runs inside the pipeline, so a failing layer still leaves its log behind
# (pipefail then propagates the failure and set -e aborts, as without --log).
run_layer() {
    local layer=$1 fn="run_${1//-/_}"
    if [[ -z "$LOG_DIR" ]]; then
        "$fn"
        return
    fi
    mkdir -p "$LOG_DIR"
    { provenance_header "$layer"; "$fn"; } 2>&1 | tee "$LOG_DIR/$layer.log"
}

case "${1:-all}" in
    tests | tsan | miri | miri-concurrent | audit) run_layer "$1" ;;
    all)
        for layer in tests tsan miri miri-concurrent audit; do
            run_layer "$layer"
        done
        echo "All verification layers passed."
        ;;
    *)
        usage
        exit 2
        ;;
esac