Commit 8cd47ba2 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into affine_arithmetic

parents cdb5d093 ff37cc07
#!/bin/bash
####################################################################################
# #
# Experiments for CPP 2018 Paper. Run daisy on all testcases in the "cpp2018" #
# directory. Then use the provers to get the runtimes and check the certificates #
# #
####################################################################################
PROVERS=(coq hol4 binary)
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter?
done < <(find $2 -name "*.scala" -print0)
DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_$DATE
echo "Creating HOL4 heap for evaluation"
cd ./hol4/output/
Holmake heap
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"
for prv in "${PROVERS[@]}"
do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval
done
else
echo "Doing mixed-precision eval for $FILENAME"
for prv in "${PROVERS[@]}"
do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval \
--mixed-precision=testcases/mixed-precision-maps/$PMAP
done
fi
cd ..
#run coq checker
echo "Working on Coq $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" coqc -R ./coq Flover ./daisy/output/$CERTNAME.v
#run HOL4 checker
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig"
/usr/bin/time -o $1 -a -f ", %e" Holmake $CERTNAME"Theory.sig"
cd ../../
# #run HOL4 binary
echo "Working on CakeML $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" hol4/binary/cake_checker ./daisy/output/$CERTNAME".txt"
# #run Coq binary
echo "Working on Coq binary $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" coq/binary/coq_checker_native ./daisy/output/$CERTNAME".txt"
mv ./daisy/output/certificate_* /tmp/artifact_$DATE/
#Add a linebreak
echo "">>$1
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