matita/bench_disamberrors

   1 #!/bin/bash
   2 #set -x
   3 TEMP=`getopt -o c:d:m: -- "$@"`
   4 libdir="`pwd`/library"
   5 matitac="`pwd`/matitac.opt"
   6 devel="library"
   7 matitadep="./matitadep.opt"
   8 eval set -- "$TEMP"
   9 while true ; do
  10   case "$1" in
  11     -d) libdir="$2"; shift 2 ;;
  12     -c) matitac="$2"; shift 2 ;;
  13     -m) devel="$2"; shift 2 ;;
  14     --) shift; break ;;
  15      *) echo "Usage: errors_bench [-c MATITAC_PATH] [-d LIBRARY_DIR] [-m MATITAMAKE_DEVEL]"; exit 1 ;;
  16   esac
  17 done
  18 if ! [ -d "$libdir" ] ; then
  19   echo "Can't find library directory '$libdir'"
  20   exit 2
  21 fi
  22 if ! [ -x "$matitac" ] ; then
  23   echo "Can't find executable Matita compiler '$matitac'"
  24   exit 2
  25 fi
  26
  27 ma_s=$(find $libdir -name "*.ma" -type f)
  28 sorted_ma_s=$($matitadep -order $ma_s)
  29
  30 log="bench_disamberrors.txt"
  31 rm -f "$log"
  32 echo -e "# FILENAME\tOUTCOME\tEXPECTED_ERROR\tERRORS\tSPURIOUS_ERRORS" > $log
  33 # format: tab-separated fields:
  34 #   FILENAME OUTCOME EXPECTED_ERROR ERRORS SPURIOUS_ERRORS
  35 # field descriptions:
  36 #   OUTCOME is one of {"OK","KO","UNKNOWN(n)"}, n is an exit code
  37 #   EXPECTED_ERROR is FROM-TO, where FROM and TO are character counts
  38 #   ERRORS, same format as above (FROM-TO)
  39 #   SPURIOUS_ERRORS, same format as above (FROM-TO)
  40 log_outcome ()
  41 {
  42   echo -e "$1|$2|$3|$4|$5" >> "$log"
  43 }
  44
  45 for ma in $sorted_ma_s ; do
  46   mo=`echo $ma | sed 's/\.ma$/.mo/'`
  47   make -C $libdir $mo # ensure deps for $mo have been built
  48   rotten_mas=$(ls $libdir/$ma.*.rottened)
  49   for rotten_ma in $rotten_mas ; do
  50     rotten_ma=$(echo $rotten_ma | sed s@^$(pwd)/@@)  # prettier names
  51     echo "$rotten_ma ..."
  52     tmp="bench_disamberrors.tmp"
  53     $matitac $rotten_ma &> $tmp
  54     outcome=$?
  55     if [ "$outcome" = 3 ] ; then
  56       outcome="KO"
  57     elif [ "$outcome" = 0 ] ; then
  58       outcome="OK"
  59     else
  60       outcome="UNKNOWN($outcome)"
  61     fi
  62     supposed_error=$(grep ^error-at: $rotten_ma | cut -f 2 -d' ')
  63     errors=""
  64     spurious_errors=""
  65     error_pass=""
  66     error_loc=""
  67     while read e ; do
  68       if echo "$e" | grep -q "Error at" && [ -n "$error_pass" ] ; then
  69         # this is an error location line
  70         if echo "$e" | grep -q "Spurious" ; then
  71           loc=$(echo "$e" | sed 's/:.*$//' | cut -f 4 -d ' ')
  72           if ! echo "$spurious_errors" | grep -q "$loc"; then
  73             if ! [ -z "$spurious_errors" ] ; then spurious_errors="$spurious_errors," ; fi
  74             spurious_errors="$spurious_errors$loc"
  75           fi
  76         else
  77           loc=$(echo "$e" | sed 's/:.*$//' | cut -f 3 -d ' ')
  78           if ! echo "$errors" | grep -q "$loc"; then
  79             if ! [ -z "$errors" ] ; then errors="$errors," ; fi
  80             errors="$errors$loc"
  81           fi
  82         fi
  83       fi
  84       error_pass=$(echo "$e" | grep "during phases " | sed 's/:.*$//' | cut -f 6 -d' ' | grep "4\|6")
  85     done < $tmp
  86     log_outcome $rotten_ma $outcome $supposed_error $errors $spurious_errors
  87   done
  88 done
  89
  90 echo "See $log for benchmark results"