Commit fc02e1b5 authored by Heiko Becker's avatar Heiko Becker

Add more sophisticated cpp script such that I need not do all the dirty work by hand

parent 16e2b87a
#!/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 #
# #
####################################################################################
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find ./testcases/cpp2018/ -name "*.scala" -print0)
echo "################################################
Daisy analysis and generation phase
################################################" >$1
for file in "${arr[@]}"
do
#echo $file
#echo "Coq certificate"
FILEPRE=${file/.scala/}
FILENAME=${FILEPRE/.\/testcases\/cpp2018\//}
/usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=coq --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/${file/scala/txt} >/dev/null
#echo "HOL4 Certificate"
/usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=hol4 --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/${file/scala/txt} >/dev/null
#echo "HOL4 Binary Certificate"
/usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=binary --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/${file/scala/txt} >/dev/null
#echo ""
done
echo "################################################
Certificate test - Coq
################################################" >$1
cd coq
arrCoq=()
while IFS= read -r -d $'\0'; do
arrCoq+=("$REPLY")
done < <(find ./output/ -name "*.v" -print0)
for file in "${arrCoq[@]}"
do
$FILEPRE = ${file/.v/}
$FILENAME=${FILEPRE/output/}
/usr/bin/time -o $1 -a -f "| $FILENAME | %e |" coqc -R ./ Daisy $file
done
echo "################################################
Certificate test - HOL4
################################################" >$1
cd ./hol4/output
arrHOL=()
while IFS= read -r -d $'\0'; do
arrHOL+=("$REPLY")
done < <(find ./ -name "*Script.sml" -print0)
for file in "${arrHOL[@]}"
do
$FILEPRE = ${file/Script.sml/}
$FILENAME=$FILEPRE
/usr/bin/time -o $1 -a -f "| $FILENAME | %e" Holmake ${file/Script.sml/Theory.sig}
done
# echo ""
# echo "[Certificate Test - HOL4]"
# echo ""
# arrHOL=()
# while IFS= read -r -d $'\0'; do
# arrHOL+=("$REPLY")
# done < <(find ./output/ -name "*.sml" -print0)
# for file in "${arrHOL[@]}"
# do
# echo $file
# echo ""
# /usr/bin/time -o $1 -a -f "%C %e" $HOLDIR/bin/Holmake ${file/Script.sml/Theory.sig}
# done
echo "################################################
Certificate test - HOL4 Binary
################################################" >$1
cd ../../output/
arrBinary=()
while IFS= read -r -d $'\0'; do
arrBinary+=("$REPLY")
done < <(find ./ -name "*.txt" -print0)
for file in "${arrBinary[@]}"
do
$FILEPRE=${file/.txt/}
$FILENAME=$FILEPRE
/usr/bin/time -f "| $FILENAME | %e |" sh -c "../hol4/binary/cake_checker <$file"
echo $?
done
echo "################################################"
echo " Certificate test - Coq Binary"
echo "################################################"
for file in "${arrBinary[@]}"
do
$FILEPRE=${file/.txt/}
$FILENAME=$FILEPRE
/usr/bin/time -a -o $1 -f "| $FILENAME | %e |" sh -c "../coq/binary/coq_checker_native $file"
echo $?
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