#!/usr/bin/env sh
set -eu

check_file() {
    file="$1"
    awk '
        BEGIN {
            failed = 0
        }
        /^#\[cfg\((test|kani)\)\]/ {
            exit failed
        }
        /^[[:space:]]*\/\/[!\/]/ {
            next
        }
        pending_encode_array_assert == 1 {
            if ($0 ~ /^[[:space:]]*required == OUTPUT_LEN,/) {
                pending_encode_array_assert = 2
                next
            }
            failed = 1
        }
        pending_encode_array_assert == 2 {
            if ($0 ~ /^[[:space:]]*"base64 output array has incorrect length"/) {
                pending_encode_array_assert = 0
                next
            }
            failed = 1
        }
        /debug_assert!\(|debug_assert_eq!\(|debug_assert_ne!\(/ {
            next
        }
        FILENAME == "src/engine/encode.rs" && $0 ~ /^[[:space:]]*assert!\($/ {
            pending_encode_array_assert = 1
            next
        }
        /panic!\(|unreachable!\(|\.unwrap\(|\.expect\(|assert!\(|assert_eq!\(|assert_ne!\(/ {
            allowed = 0
            if ($0 ~ /assert!\(line_len != 0, "base64 line wrap length must be non-zero"\)/) {
                allowed = 1
            }
            if ($0 ~ /assert!\(len <= CAP, "visible length exceeds array capacity"\)/) {
                allowed = 1
            }
            if ($0 ~ /unreachable!\("stream .* was already taken"\)/) {
                allowed = 1
            }
            if ($0 ~ /unreachable!\("tokio .* writer inner writer was already taken"\)/) {
                allowed = 1
            }
            if ($0 ~ /unreachable!\("base64 encoder produced non-UTF-8 output"\)/) {
                allowed = 1
            }
            if ($0 ~ /_ => unreachable!\(\),/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("encoded base64 length overflows usize"\)/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("SecretArrayFrame decoded capacity exceeds 1024-byte stack limit"\)/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("SecretArrayEncoder encoded capacity exceeds 1368-byte stack limit"\)/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("sanitization secret staging exceeds the 1024-byte stack limit"\)/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("Serde decoded capacity exceeds the supported 4096-byte stack limit"\)/) {
                allowed = 1
            }
            if ($0 ~ /panic!\("base64-ng-sanitization locked secret integrity failure: \{error\}"\)/) {
                allowed = 1
            }
            if ($0 ~ /\.expect\("base64-ng encode_vec failed for byte input"\)/) {
                allowed = 1
            }
            if ($0 ~ /\.expect\("base64-ng encode_string failed for byte input"\)/) {
                allowed = 1
            }
            if ($0 ~ /\.expect\("base64-ng profile encode_vec failed for byte input"\)/) {
                allowed = 1
            }
            if ($0 ~ /\.expect\("base64-ng profile encode_string failed for byte input"\)/) {
                allowed = 1
            }
            if (!allowed) {
                printf "panic policy: unreviewed panic-like site in %s:%d: %s\n", FILENAME, FNR, $0 > "/dev/stderr"
                failed = 1
            }
        }
        END {
            exit failed || pending_encode_array_assert
        }
    ' "$file"
}

test -s docs/PANIC_POLICY.md

for test_file in src/*_tests.rs; do
    test -e "$test_file" || continue
    module_name="$(basename "$test_file" .rs)"
    if ! awk -v module_name="$module_name" '
        /^#\[cfg\(test\)\]/ {
            saw_cfg_test = 1
            next
        }
        saw_cfg_test && /^[[:space:]]*$/ {
            next
        }
        saw_cfg_test {
            expected = "^[[:space:]]*mod " module_name ";"
            if ($0 ~ expected) {
                found = 1
            }
            saw_cfg_test = 0
        }
        END {
            exit found ? 0 : 1
        }
    ' src/lib.rs; then
        echo "panic policy: $test_file must be declared behind #[cfg(test)] in src/lib.rs" >&2
        exit 1
    fi
done

for test_file in src/v2/*_tests.rs src/v2/fixtures.rs src/v2/rfc4648_oracle.rs; do
    test -e "$test_file" || continue
    module_name="$(basename "$test_file" .rs)"
    if ! awk -v module_name="$module_name" '
        /^#\[cfg\(.*test.*\)\]$/ {
            saw_cfg_test = 1
            next
        }
        saw_cfg_test && /^[[:space:]]*$/ {
            next
        }
        saw_cfg_test {
            expected = "^[[:space:]]*mod " module_name ";"
            if ($0 ~ expected) {
                found = 1
            }
            saw_cfg_test = 0
        }
        END {
            exit found ? 0 : 1
        }
    ' src/v2/mod.rs; then
        echo "panic policy: $test_file must be declared behind #[cfg(test)] in src/v2/mod.rs" >&2
        exit 1
    fi
done

for test_file in src/*/tests.rs src/*/*/tests.rs; do
    test -e "$test_file" || continue
    parent_module="$(dirname "$test_file")/../$(basename "$(dirname "$test_file")").rs"
    if [ ! -f "$parent_module" ]; then
        parent_module="$(dirname "$test_file")/mod.rs"
    fi
    if ! awk '
        /^#\[cfg\(/ {
            in_cfg = 1
            cfg_has_test = ($0 ~ /(^|[^[:alnum:]_])test([^[:alnum:]_]|$)/)
            if ($0 ~ /\)\]$/) {
                saw_cfg_test = cfg_has_test
                in_cfg = 0
            }
            next
        }
        in_cfg {
            if ($0 ~ /(^|[^[:alnum:]_])test([^[:alnum:]_]|$)/) {
                cfg_has_test = 1
            }
            if ($0 ~ /\)\]$/) {
                saw_cfg_test = cfg_has_test
                in_cfg = 0
            }
            next
        }
        saw_cfg_test && /^[[:space:]]*$/ {
            next
        }
        saw_cfg_test {
            if ($0 ~ /^[[:space:]]*mod tests;/) {
                found = 1
            }
            saw_cfg_test = 0
        }
        END {
            exit found ? 0 : 1
        }
    ' "$parent_module"; then
        echo "panic policy: $test_file must be declared behind #[cfg(test)] in $parent_module" >&2
        exit 1
    fi
done

find src crates/*/src -name '*.rs' | sort | while IFS= read -r source_file; do
    case "$source_file" in
        src/*_tests.rs|src/kani_proofs.rs|src/kani_in_place_proofs.rs|src/kani_v2_core_proofs.rs|src/kani_simd_model_proofs.rs|src/kani_assurance_proofs.rs|src/kani_secret_proofs.rs|src/kani_secret_encode_proofs.rs|src/tests.rs|src/simd/tests.rs|src/simd/wasm.rs|src/simd/neon_decode_tests.rs|src/simd/neon_direct_tests.rs|src/simd/x86_decode_tests.rs|src/v2/*_tests.rs|src/v2/fixtures.rs|src/v2/rfc4648_oracle.rs|src/*/tests.rs|src/*/*/tests.rs|crates/*/src/tests.rs|crates/*/src/*_tests.rs)
            continue
            ;;
    esac
    check_file "$source_file"
done

echo "panic policy: ok"