begriffs open source - acsl-example/blob - scripts/prove.sh

   1 #!/usr/bin/bash
   2
   3 # create these files for a verification attempt
   4 #
   5 # proofs/
   6 # ├── ast/
   7 # │   └── program.sav             Serialized Abstract Syntax Tree
   8 # ├── normalized/
   9 # │   └── program.c               Frama-C normalized source
  10 # ├── obligations/
  11 # │   └── typed/
  12 # │       ├── *.why               Why3 proof obligations
  13 # │       └── *.smt2              Clean SMT-LIB2 files (optional)
  14 # └── results/
  15 #     ├── debug-summary.txt       LLM-friendly failure analysis
  16 #     └── results.json            Structured verification results
  17
  18 PROGNAME=$(basename $1 .c)
  19 if [ -z "$PROGNAME" ] || [ "$PROGNAME" = "." ] || [ "$PROGNAME" = ".." ]; then
  20     echo "Error: Invalid program name '$PROGNAME'"
  21     exit 1
  22 fi
  23
  24 PROVER=${2:-alt-ergo}
  25 rm -rf proofs/$PROGNAME
  26 mkdir -p proofs/$PROGNAME/ast proofs/$PROGNAME/normalized proofs/$PROGNAME/obligations/typed proofs/$PROGNAME/results
  27
  28 frama-c -cpp-extra-args="-I inc" -save proofs/$PROGNAME/ast/$(basename $1).sav \
  29         -print -ocode proofs/$PROGNAME/normalized/program.c \
  30         -wp -wp-out proofs/$PROGNAME/obligations \
  31         -wp-prover $PROVER \
  32         -wp-report-json proofs/$PROGNAME/results/results.json \
  33         -wp-status \
  34         $1 > proofs/$PROGNAME/results/debug-summary.txt 2>&1
  35
  36 if [ $? -ne 0 ]; then
  37     echo "Frama-C failed. Check proofs/$PROGNAME/results/debug-summary.txt for details."
  38     exit 1
  39 fi
  40
  41 for f in proofs/$PROGNAME/obligations/typed/*.why; do
  42         if [ -f "$f" ]; then
  43                 base=$(basename "$f" .why)
  44                 sed '1d' "$f" > "proofs/$PROGNAME/obligations/typed/${base}.smt2"
  45         fi
  46 done
  47
  48 echo "========================================="
  49 echo "VERIFICATION SUMMARY FOR $PROGNAME"
  50 echo "========================================="
  51
  52 # Extract key metrics from debug summary
  53 if [ -f "proofs/$PROGNAME/results/debug-summary.txt" ]; then
  54     PROVED=$(grep "Proved goals:" "proofs/$PROGNAME/results/debug-summary.txt" | sed 's/.*Proved goals: *\([0-9]*\) \/ \([0-9]*\).*/\1 \2/')
  55     PROVED_COUNT=$(echo $PROVED | cut -d' ' -f1)
  56     TOTAL_COUNT=$(echo $PROVED | cut -d' ' -f2)
  57
  58     echo "Goals: $PROVED_COUNT/$TOTAL_COUNT proved"
  59
  60     # Check for warnings and errors
  61     WARNINGS=0
  62     TIMEOUTS=0
  63     FAILURES=0
  64
  65     if grep -q "Warning:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null; then
  66         WARNINGS=$(grep -c "Warning:" "proofs/$PROGNAME/results/debug-summary.txt")
  67     fi
  68
  69     # Parse timeout count from "Timeout: N" line
  70     TIMEOUT_LINE=$(grep "Timeout:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null || echo "")
  71     if [ -n "$TIMEOUT_LINE" ]; then
  72         TIMEOUTS=$(echo "$TIMEOUT_LINE" | sed 's/.*Timeout: *\([0-9]*\).*/\1/')
  73     fi
  74
  75     # Parse failure count from "Failure: N" or count "returns Failure" lines
  76     FAILURE_LINE=$(grep "Failure:" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null || echo "")
  77     if [ -n "$FAILURE_LINE" ]; then
  78         FAILURES=$(echo "$FAILURE_LINE" | sed 's/.*Failure: *\([0-9]*\).*/\1/')
  79     else
  80         # Fallback: count individual failure lines
  81         if grep -q "returns Failure" "proofs/$PROGNAME/results/debug-summary.txt" 2>/dev/null; then
  82             FAILURES=$(grep -c "returns Failure" "proofs/$PROGNAME/results/debug-summary.txt")
  83         fi
  84     fi
  85
  86     if [ "$WARNINGS" -gt 0 ]; then
  87         echo "Warnings: $WARNINGS"
  88     fi
  89     if [ "$TIMEOUTS" -gt 0 ]; then
  90         echo "Timeouts: $TIMEOUTS"
  91     fi
  92     if [ "$FAILURES" -gt 0 ]; then
  93         echo "Failures: $FAILURES"
  94     fi
  95
  96     # Determine success/failure
  97     if [ "$PROVED_COUNT" = "$TOTAL_COUNT" ] && [ "$TIMEOUTS" -eq 0 ] && [ "$FAILURES" -eq 0 ]; then
  98         echo "Status: SUCCESS"
  99         echo "========================================="
 100         exit 0
 101     else
 102         echo "Status: FAILURE"
 103         echo "See proofs/$PROGNAME/results/debug-summary.txt for full details"
 104         echo "========================================="
 105         exit 1
 106     fi
 107 else
 108     echo "Status: ERROR - No debug summary found"
 109     echo "========================================="
 110     exit 1
 111 fi
 112