Commit f9f05d48 authored by Heiko Becker's avatar Heiko Becker

Add affine arithmetic evaluation script, add comments to scripts

parent a3663215
#!/bin/bash
##########################################################################
# #
# Affine Arithmetic Experiments for FMCAD 2018 paper #
# First run Daisy on all files found in the folder fmcad2018 to generate #
# certificates and log roundoff errors in a csv file. #
# Then benchmark each of the FloVer implementations by measuring runtime #
# when checking the generated certificate. #
# #
##########################################################################
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_affine_$DATE
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" >>$2
RESULT=$( { /usr/bin/time -f ", %e" \
./daisy $FILEPATH --certificate=coq \
--rangeMethod=affine \
--errorMethod=interval \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1 )
echo -n $RESULT >> $1
else
echo "Doing mixed-precision eval for $FILENAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" \
./daisy $FILEPATH --certificate=coq \
--rangeMethod=affine \
--errorMethod=interval \
--mixed-precision=testcases/mixed-precision-maps/$PMAP \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1)
echo -n $RESULT >> $1
fi
mv ./output/$FILENAME.csv /tmp/artifact_$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 $RESULT >>$1
mv ./daisy/output/certificate_* /tmp/artifact_affine_$DATE/
done
#!/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 #
# #
####################################################################################
##########################################################################
# #
# Interval Arithmetic Experiments for FMCAD 2018 paper #
# First run Daisy on all files found in the folder fmcad2018 to generate #
# 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)
......
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