eval_interval.sh 3.35 KB
Newer Older
1 2
#!/bin/bash

Heiko Becker's avatar
Heiko Becker committed
3 4 5 6 7 8 9 10 11 12 13

##############################################################################
#                                                                            #
# Interval 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.                                   #
#                                                                            #
##############################################################################

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

PROVERS=(coq hol4 binary)

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_$DATE

echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/
Holmake heap >>$2
cd ../../

for file in "${arr[@]}"
do
  #Get the filename
  FILEPATH=${file/daisy\//.\/}
  FILE=${file/*\//}
  FILENAME=${FILE/.scala/}
  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
      for prv in "${PROVERS[@]}"
      do
          RESULT=$( { /usr/bin/time -f ", %e" \
                                    ./daisy $FILEPATH --certificate=$prv \
                                    --errorMethod=interval \
                                    --results-csv=$FILENAME \
                                    >>$2 \
                      ; } 2>&1 )
          echo -n $RESULT >> $1
      done
  else
      echo "Doing mixed-precision eval for $FILENAME" >>$2
      for prv in "${PROVERS[@]}"
      do
          RESULT=$( { /usr/bin/time -f ", %e" \
                                    ./daisy $FILEPATH --certificate=$prv \
                                    --errorMethod=interval \
                                    --mixed-precision=testcases/mixed-precision-maps/$PMAP \
                                    --results-csv=$FILENAME \
                                    >>$2 \
                      ; } 2>&1)
          echo -n $RESULT >> $1
      done
  fi

  mv ./output/$FILENAME.csv /tmp/artifact_$DATE

  cd ..

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

  #run HOL4 checker
  cp ./daisy/output/*Script.sml ./hol4/output/
  cd ./hol4/output/
  echo "Working on $CERTNAME Theory.sig" >>$2
  RESULT=$( { /usr/bin/time -f ", %e" Holmake $CERTNAME"Theory.sig" >>$2; } 2>&1)
  echo -n $RESULT >>$1

  cd ../../

  # #run HOL4 binary
  echo "Working on CakeML $CERTNAME"
  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
                            ./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)
  echo -n $RESULT >>$1

  # #run Coq binary
  echo "Working on Coq binary $CERTNAME"
  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
                            ./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)

  echo $RESULT >>$1

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

done