#!/usr/bin/env bash
# Optional source-confirmation smoke for Fold's KLEE adapter prototype.
# Skips cleanly when KLEE is not installed.
set -euo pipefail

ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../../.." && pwd)"
SRC="$ROOT/tests/confirmation/klee/oob_overwrite.c"
OUT="$ROOT/build/klee-smoke"
TASK="$OUT/oob_overwrite.task.json"
RESULT="$OUT/oob_overwrite.result.json"

mkdir -p "$OUT"
cat >"$TASK" <<EOF
{
  "version": "1",
  "task_id": "klee:oob-overwrite-smoke",
  "finding_id": "oob-access:oob_overwrite.c:10:5",
  "hazard": "oob-access",
  "backend": "source",
  "lane": "clang",
  "adapter": "klee",
  "target": {
    "artifact": "$SRC",
    "function": "vulnerable_copy",
    "source_location": {
      "file": "$SRC",
      "line": 10,
      "column": 5,
      "function": "vulnerable_copy"
    }
  },
  "input_channel": "harness",
  "controlled_values": ["idx"],
  "path_predicate": "idx >= 8 && idx < 16",
  "expected_violation": "out-of-bounds write",
  "artifacts": [],
  "partial": false
}
EOF

CLANG="${CLANG:-clang}"
python3 "$ROOT/tests/confirmation/klee/klee_confirm.py" \
	--task "$TASK" \
	--output "$RESULT" \
	--work-dir "$OUT" \
	--clang "$CLANG"

STATUS="$(
	python3 - <<PY
import json
from pathlib import Path
print(json.loads(Path('$RESULT').read_text()).get('status', ''))
PY
)"

case "$STATUS" in
confirmed)
	echo "ok: KLEE confirmed smoke task"
	;;
unsupported)
	echo "skip: KLEE adapter unsupported in this environment"
	;;
*)
	echo "fail: unexpected KLEE smoke status: $STATUS"
	cat "$RESULT"
	exit 1
	;;
esac