#!/usr/bin/bash

# create these files for a verification attempt
#
# proofs/
# ├── ast/
# │   └── program.sav             Serialized Abstract Syntax Tree
# ├── normalized/
# │   └── program.c               Frama-C normalized source
# ├── obligations/
# │   └── typed/
# │       ├── *.why               Why3 proof obligations
# │       └── *.smt2              Clean SMT-LIB2 files (optional)
# └── results/
#     ├── debug-summary.txt       LLM-friendly failure analysis
#     └── results.json            Structured verification results

PROGNAME=$(basename $1 .c)
if [ -z "$PROGNAME" ] || [ "$PROGNAME" = "." ] || [ "$PROGNAME" = ".." ]; then
    echo "Error: Invalid program name '$PROGNAME'"
    exit 1
fi

PROVER=${2:-alt-ergo}
rm -rf proofs/$PROGNAME
mkdir -p proofs/$PROGNAME/ast proofs/$PROGNAME/normalized proofs/$PROGNAME/obligations/typed proofs/$PROGNAME/results

frama-c -cpp-extra-args="-I inc" -save proofs/$PROGNAME/ast/$(basename $1).sav \
        -print -ocode proofs/$PROGNAME/normalized/program.c \
        -wp -wp-out proofs/$PROGNAME/obligations \
        -wp-prover $PROVER \
        -wp-report-json proofs/$PROGNAME/results/results.json \
        -wp-status \
        $1 > proofs/$PROGNAME/results/debug-summary.txt 2>&1

if [ $? -ne 0 ]; then
    echo "Frama-C failed. Check proofs/$PROGNAME/results/debug-summary.txt for details."
    exit 1
fi

for f in proofs/$PROGNAME/obligations/typed/*.why; do
	if [ -f "$f" ]; then
		base=$(basename "$f" .why)
		sed '1d' "$f" > "proofs/$PROGNAME/obligations/typed/${base}.smt2"
	fi
done

echo "========================================="
echo "VERIFICATION SUMMARY FOR $PROGNAME"
echo "========================================="

# Extract key metrics from debug summary
if [ -f "proofs/$PROGNAME/results/debug-summary.txt" ]; then
    PROVED=$(grep "Proved goals:" "proofs/$PROGNAME/results/debug-summary.txt" | sed 's/.*Proved goals: *\([0-9]*\) \/ \([0-9]*\).*/\1 \2/')
    PROVED_COUNT=$(echo $PROVED | cut -d' ' -f1)
    TOTAL_COUNT=$(echo $PROVED | cut -d' ' -f2)
    
    echo "Goals: $PROVED_COUNT/$TOTAL_COUNT proved"
    
    # Check for warnings and errors
    WARNINGS=0
    TIMEOUTS=0
    FAILURES=0
    
    if grep -q "Warning:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null; then
        WARNINGS=$(grep -c "Warning:" "proofs/$PROGNAME/results/debug-summary.txt")
    fi
    
    # Parse timeout count from "Timeout: N" line
    TIMEOUT_LINE=$(grep "Timeout:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null || echo "")
    if [ -n "$TIMEOUT_LINE" ]; then
        TIMEOUTS=$(echo "$TIMEOUT_LINE" | sed 's/.*Timeout: *\([0-9]*\).*/\1/')
    fi
    
    # Parse failure count from "Failure: N" or count "returns Failure" lines
    FAILURE_LINE=$(grep "Failure:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null || echo "")
    if [ -n "$FAILURE_LINE" ]; then
        FAILURES=$(echo "$FAILURE_LINE" | sed 's/.*Failure: *\([0-9]*\).*/\1/')
    else
        # Fallback: count individual failure lines
        if grep -q "returns Failure" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null; then
            FAILURES=$(grep -c "returns Failure" "proofs/$PROGNAME/results/debug-summary.txt")
        fi
    fi
    
    if [ "$WARNINGS" -gt 0 ]; then
        echo "Warnings: $WARNINGS"
    fi
    if [ "$TIMEOUTS" -gt 0 ]; then
        echo "Timeouts: $TIMEOUTS"
    fi
    if [ "$FAILURES" -gt 0 ]; then
        echo "Failures: $FAILURES"
    fi
    
    # Determine success/failure
    if [ "$PROVED_COUNT" = "$TOTAL_COUNT" ] && [ "$TIMEOUTS" -eq 0 ] && [ "$FAILURES" -eq 0 ]; then
        echo "Status: SUCCESS"
        echo "========================================="
        exit 0
    else
        echo "Status: FAILURE"
        echo "See proofs/$PROGNAME/results/debug-summary.txt for full details"
        echo "========================================="
        exit 1
    fi
else
    echo "Status: ERROR - No debug summary found"
    echo "========================================="
    exit 1
fi