-#!/bin/bash
-#set -x
-TEMP=`getopt -o c:d:m: -- "$@"`
-libdir="`pwd`/library"
-matitac="`pwd`/matitac.opt"
-devel="library"
-matitadep="./matitadep.opt"
-eval set -- "$TEMP"
-while true ; do
- case "$1" in
- -d) libdir="$2"; shift 2 ;;
- -c) matitac="$2"; shift 2 ;;
- -m) devel="$2"; shift 2 ;;
- --) shift; break ;;
- *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
- esac
-done
-if ! [ -d "$libdir" ] ; then
- echo "Can't find library directory '$libdir'"
- exit 2
-fi
-if ! [ -x "$matitac" ] ; then
- echo "Can't find executable Matita compiler '$matitac'"
- exit 2
-fi
-
-ma_s=$(find $libdir -name "*.ma" -type f)
-sorted_ma_s=$($matitadep -order $ma_s)
-
-log="bench_disamberrors.txt"
-rm -f "$log"
-echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
-# format: tab-separated fields:
-# FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
-# field descriptions:
-# OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
-# EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
-# ERRORS, same format as above (FROM-TO)
-# SPURIOUS_ERRORS, same format as above (FROM-TO)
-log_outcome ()
-{
- echo -e "$1|$2|$3|$4|$5" >> "$log"
-}
-
-for ma in $sorted_ma_s ; do
- mo=`echo $ma | sed 's/\.ma$/.mo/'`
- make -C $libdir $mo # ensure deps for $mo have been built
- rotten_mas=$(ls $libdir/$ma.*.rottened)
- for rotten_ma in $rotten_mas ; do
- rotten_ma=$(echo $rotten_ma | sed s@^$(pwd)/@@) # prettier names
- echo "$rotten_ma ..."
- tmp="bench_disamberrors.tmp"
- $matitac $rotten_ma &> $tmp
- outcome=$?
- if [ "$outcome" = 3 ] ; then
- outcome="KO"
- elif [ "$outcome" = 0 ] ; then
- outcome="OK"
- else
- outcome="UNKNOWN($outcome)"
- fi
- supposed_error=$(grep ^error-at: $rotten_ma | cut -f 2 -d' ')
- errors=""
- spurious_errors=""
- error_pass=""
- error_loc=""
- while read e ; do
- if echo "$e" | grep -q "Error at" && [ -n "$error_pass" ] ; then
- # this is an error location line
- if echo "$e" | grep -q "Spurious" ; then
- loc=$(echo "$e" | sed 's/:.*$//' | cut -f 4 -d ' ')
- if ! echo "$spurious_errors" | grep -q "$loc"; then
- if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
- spurious_errors="$spurious_errors$loc"
- fi
- else
- loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ')
- if ! echo "$errors" | grep -q "$loc"; then
- if ! [ -z "$errors" ] ; then errors="$errors," ; fi
- errors="$errors$loc"
- fi
- fi
- fi
- error_pass=$(echo "$e" | grep "during phases " | sed 's/:.*$//' | cut -f 6 -d' ' | grep "4\|6")
- done < $tmp
- log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
- done
-done
-
-echo "See $log for benchmark results"