#!/bin/bash


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

TIMECMD=""

unameOut="$(uname -s)"
case "${unameOut}" in
    Linux*)     TIMECMD=/usr/bin/time;;
    Darwin*)    TIMECMD=/usr/local/bin/time;;
    # CYGWIN*)    machine=Cygwin;;
    # MINGW*)     machine=MinGw;;
    # *)          machine="UNKNOWN:${unameOut}"
esac

#PROVERS=(coq hol4 binary)
PROVERS=(coq)

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

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

#echo "Daisy Coq,  Daisy HOL4, Daisy Binary, Coq1, Coq2, Coq3, HOL4_1, HOL4_2, HOL4_3, CakeML1, CakeML2, CakeML3, Coqbin1, Coqbin2, Coqbin3" >>$1
echo "Daisy Coq, Coq1, Coq2, Coq3" >>$1

for file in "${arr[@]}"
do
  #Get the filename
  FILEPATH=${file/daisy\//.\/}
  FILE=${file/*\//}
  FILENAME=${FILE/.scala/}
  FILENAME=${FILENAME/Let/}
  PMAP=${FILE/scala/txt}
  CERTNAME="certificate_$FILENAME"
  # Generate a certificate with Daisy
  echo -n $FILENAME >>$1
  cd ./daisy
  for prv in "${PROVERS[@]}"
  do
      RESULT=$( { $TIMECMD -f ", %e" \
                                ./daisy $FILEPATH --certificate=$prv \
                                --precision=Fixed32 \
                                --rangeMethod=smt \
                                --errorMethod=interval \
                                --results-csv=$FILENAME.csv \
                                >>$2 \
                  ; } 2>&1 )
      echo -n $RESULT >> $1
  done

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

  cd ..

  #run coq checker 3 times
  echo "Working on Coq $CERTNAME" >>$2
  RESULT=$( { $TIMECMD -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=$( { $TIMECMD -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=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
                            ./daisy/output/$CERTNAME.v; } 2>&1)
  echo -n $RESULT >>$1

#  #run HOL4 checker 3 times
#  cp ./daisy/output/*Script.sml ./hol4/output/
#  cd ./hol4/output/
#  echo "Working on $CERTNAME Theory.sig" >>$2
#  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
#  RESULT=${RESULT#*M1}
#  RESULT=${RESULT%%M2*}
#  echo -n $RESULT >>$1
#
#  rm ./certificate_*Theory*
#
#  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
#  RESULT=${RESULT#*M1}
#  RESULT=${RESULT%%M2*}
#  echo -n $RESULT >>$1
#
#  rm ./certificate_*Theory*
#
#  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
#  RESULT=${RESULT#*M1}
#  RESULT=${RESULT%%M2*}
#  echo -n $RESULT >>$1
#
#  cd ../../
#
#  #run HOL4 binary 3 times
#  echo "Working on CakeML $CERTNAME"
#  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#  echo -n $RESULT >>$1
#
#  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#  echo -n $RESULT >>$1
#
#  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#  echo -n $RESULT >>$1
#
#  # #run Coq binary 3 times
#  echo "Working on Coq binary $CERTNAME"
#  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
#  echo -n $RESULT >>$1
#
#  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
#  echo -n $RESULT >>$1
#
#  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
#                            ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
#  echo $RESULT >>$1

  echo "" >>$1
  mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/

done