eval_affine.sh 2.99 KB
Newer Older
1 2
#!/bin/bash

Heiko Becker's avatar
Heiko Becker committed
3 4 5 6 7 8 9 10 11
###############################################################################
#                                                                             #
# Affine Arithmetic Experiments for FMCAD 2018 paper                          #
# First run Daisy on all files found in the folder given as third argument    #
# certificates and log roundoff errors in a csv file.                         #
# Then benchmark each of the FloVer implementations by measuring runtime      #
# when checking the generated certificate.                                    #
#                                                                             #
###############################################################################
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

arr=()
while IFS=  read -r -d $'\0'; do
    arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter?
done < <(find $3 -name "*.scala" -print0)

DATE=`date +%H%M%d%m%y`

mkdir /tmp/artifact_affine_$DATE

for file in "${arr[@]}"
do
  #Get the filename
  FILEPATH=${file/daisy\//.\/}
  FILE=${file/*\//}
  FILENAME=${FILE/.scala/}
Heiko Becker's avatar
Heiko Becker committed
29
  FILENAME=${FILENAME/Let/}
30 31 32 33 34 35 36 37 38 39 40 41
  PMAP=${FILE/scala/txt}
  CERTNAME="certificate_$FILENAME"
  # Generate a certificate with Daisy
  echo -n $FILENAME >>$1
  cd ./daisy
  if [ ! -f testcases/mixed-precision-maps/$PMAP ];
  then
      echo "Doing single precision eval for $FILENAME" >>$2
      RESULT=$( { /usr/bin/time -f ", %e" \
                                ./daisy $FILEPATH --certificate=coq \
                                --rangeMethod=affine \
                                --errorMethod=interval \
Heiko Becker's avatar
Heiko Becker committed
42
                                --results-csv=$FILENAME.csv \
43 44 45 46 47 48 49 50 51 52
                                >>$2 \
                  ; } 2>&1 )
      echo -n $RESULT >> $1
  else
      echo "Doing mixed-precision eval for $FILENAME" >>$2
      RESULT=$( { /usr/bin/time -f ", %e" \
                                ./daisy $FILEPATH --certificate=coq \
                                --rangeMethod=affine \
                                --errorMethod=interval \
                                --mixed-precision=testcases/mixed-precision-maps/$PMAP \
Heiko Becker's avatar
Heiko Becker committed
53
                                --results-csv=$FILENAME.csv \
54 55 56 57 58
                                >>$2 \
                  ; } 2>&1)
      echo -n $RESULT >> $1
  fi

Heiko Becker's avatar
Heiko Becker committed
59
  mv ./output/$FILENAME.csv /tmp/artifact_affine_$DATE
60 61 62

  cd ..

63
  #run coq checker 3 times
64
  echo "Working on Coq $CERTNAME" >>$2
65 66 67 68 69 70 71 72 73 74 75 76 77 78
  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
                            ./daisy/output/$CERTNAME.v; } 2>&1)
  echo -n $RESULT >>$1

  rm ./daisy/output/$CERTNAME.vo
  rm ./daisy/output/$CERTNAME.glob

  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
                            ./daisy/output/$CERTNAME.v; } 2>&1)
  echo -n $RESULT >>$1

  rm ./daisy/output/$CERTNAME.vo
  rm ./daisy/output/$CERTNAME.glob

79 80 81 82 83 84 85
  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
                            ./daisy/output/$CERTNAME.v; } 2>&1)
  echo $RESULT >>$1

  mv ./daisy/output/certificate_* /tmp/artifact_affine_$DATE/

done