Commit b2c87128 authored by Joachim Bard's avatar Joachim Bard

adding eval scripts for interval subdivision

parent 7fb99487
#!/bin/bash
##############################################################################
# #
# SMT 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_$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
if [ ! -f testcases/daisy-mixed-precision-maps/$PMAP ];
then
echo "Doing single precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--rangeMethod=interval \
--errorMethod=interval \
--subdiv \
--divLimit=10 \
--totalOpt=1000 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
echo -n $RESULT >> $1
done
else
echo "Doing mixed-precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--rangeMethod=interval \
--errorMethod=interval \
--subdiv \
--divLimit=10 \
--totalOpt=1000 \
--mixed-precision=testcases/daisy-mixed-precision-maps/$PMAP \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1)
echo -n $RESULT >> $1
done
fi
mv ./output/$FILENAME.csv /tmp/artifact_$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=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*
# cd ../../
#
# #run HOL4 binary 3 times
# echo "Working on CakeML $CERTNAME"
# RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { $TIMECMD -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=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
#
# RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
#
# RESULT=$( { $TIMECMD -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_$DATE/
done
#!/bin/bash
##############################################################################
# #
# SMT 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_$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
if [ ! -f testcases/daisy-mixed-precision-maps/$PMAP ];
then
echo "Doing single precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--divLimit=3 \
--totalOpt=1000 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
echo -n $RESULT >> $1
done
else
echo "Doing mixed-precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--divLimit=3 \
--totalOpt=1000 \
--mixed-precision=testcases/daisy-mixed-precision-maps/$PMAP \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1)
echo -n $RESULT >> $1
done
fi
mv ./output/$FILENAME.csv /tmp/artifact_$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=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*
# cd ../../
#
# #run HOL4 binary 3 times
# echo "Working on CakeML $CERTNAME"
# RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { $TIMECMD -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=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
#
# RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
#
# RESULT=$( { $TIMECMD -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_$DATE/
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