Add fixed-point evaluation script

scripts/eval_fixed.sh

+#!/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.                                   #
+#                                                                            #
+##############################################################################
+
+
+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_fixed_$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/}
+  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=$( { /usr/bin/time -f ", %e" \
+                                ./daisy $FILEPATH --certificate=$prv \
+                                --precision=Fixed16
+                                --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
+  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 "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
+  RESULT=${RESULT#*M1}
+  RESULT=${RESULT%%M2*}
+  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/certificate_*".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/certificate_*".txt" >>$2; } 2>&1)
+
+  echo $RESULT >>$1
+
+  mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/
+
+done