Commit 346ce385 authored by Joachim Bard's avatar Joachim Bard

adjusting eval script for fixed-point arith

parent 99599a8b
...@@ -11,8 +11,19 @@ ...@@ -11,8 +11,19 @@
# # # #
############################################################################## ##############################################################################
TIMECMD=""
PROVERS=(coq hol4 binary) 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=() arr=()
while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
...@@ -24,10 +35,13 @@ DATE=`date +%H%M%d%m%y` ...@@ -24,10 +35,13 @@ DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_fixed_$DATE mkdir /tmp/artifact_fixed_$DATE
echo "Creating HOL4 heap for evaluation" >>$2 #echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/ #cd ./hol4/output/
Holmake heap >>$2 #Holmake heap >>$2
cd ../../ #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[@]}" for file in "${arr[@]}"
do do
...@@ -43,10 +57,14 @@ do ...@@ -43,10 +57,14 @@ do
cd ./daisy cd ./daisy
for prv in "${PROVERS[@]}" for prv in "${PROVERS[@]}"
do do
RESULT=$( { /usr/bin/time -f ", %e" \ RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \ ./daisy $FILEPATH --certificate=$prv \
--precision=Fixed32 \ --precision=Fixed32 \
--rangeMethod=smt \
--errorMethod=interval \ --errorMethod=interval \
--subdiv \
--divLimit=5 \
--totalOpt=150 \
--results-csv=$FILENAME.csv \ --results-csv=$FILENAME.csv \
>>$2 \ >>$2 \
; } 2>&1 ) ; } 2>&1 )
...@@ -59,80 +77,81 @@ do ...@@ -59,80 +77,81 @@ do
#run coq checker 3 times #run coq checker 3 times
echo "Working on Coq $CERTNAME" >>$2 echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \ RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1 echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \ RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1 echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \ RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1 echo -n $RESULT >>$1
#run HOL4 checker 3 times # #run HOL4 checker 3 times
cp ./daisy/output/*Script.sml ./hol4/output/ # cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/ # cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2 # echo "Working on $CERTNAME Theory.sig" >>$2
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1) # RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1} # RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*} # RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
rm ./certificate_*Theory* # rm ./certificate_*Theory*
#
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1) # RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1} # RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*} # RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
rm ./certificate_*Theory* # rm ./certificate_*Theory*
#
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1) # RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1} # RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*} # RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
cd ../../ # cd ../../
#
#run HOL4 binary 3 times # #run HOL4 binary 3 times
echo "Working on CakeML $CERTNAME" # echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \ # RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \ # RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \ # RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
# #run Coq binary 3 times # # #run Coq binary 3 times
echo "Working on Coq binary $CERTNAME" # echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \ # RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \ # RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
echo -n $RESULT >>$1 # echo -n $RESULT >>$1
#
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \ # RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1) # ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
echo $RESULT >>$1 # echo $RESULT >>$1
echo "" >>$1
mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/ mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/
done done
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment