Revision c3bbc76e
Added by Pierre-Loïc Garoche over 9 years ago
| test/test-compile.sh | ||
|---|---|---|
| 1 | 1 |
#!/bin/bash |
| 2 | 2 |
|
| 3 |
eval set -- $(getopt -n $0 -o "-ciwh:" -- "$@") |
|
| 4 |
|
|
| 5 |
declare c i w h |
|
| 6 |
declare -a files |
|
| 7 |
|
|
| 3 | 8 |
NOW=`date "+%y%m%d%H%M"` |
| 9 |
report=`pwd`/report-$NOW |
|
| 4 | 10 |
#LUSTREC="../../_build/src/lustrec" |
| 5 | 11 |
LUSTREC=lustrec |
| 6 | 12 |
mkdir -p build |
| 7 | 13 |
build=`pwd`"/build" |
| 8 |
while IFS=, read -r file main opts |
|
| 9 |
do |
|
| 10 |
echo fichier:$file |
|
| 11 |
# echo main:$main |
|
| 12 |
# echo opts:$opts |
|
| 13 |
rm -f witness* |
|
| 14 |
name=`basename "$file" .lus` |
|
| 15 |
dir=`dirname "$file"` |
|
| 16 |
pushd $dir > /dev/null |
|
| 14 |
|
|
| 15 |
|
|
| 16 |
base_compile() {
|
|
| 17 |
while IFS=, read -r file main opts |
|
| 18 |
do |
|
| 19 |
name=`basename "$file" .lus` |
|
| 20 |
dir=`dirname "$file"` |
|
| 21 |
pushd $dir > /dev/null |
|
| 17 | 22 |
if [ "$main" != "" ]; then |
| 18 | 23 |
$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus; |
| 19 | 24 |
if [ $? -ne 0 ]; then |
| 20 |
rlustrec1="INVALID"; |
|
| 21 |
else |
|
| 22 |
rlustrec1="VALID" |
|
| 23 |
fi |
|
| 24 |
pushd $build > /dev/null |
|
| 25 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 26 |
popd > /dev/null |
|
| 27 |
if [ $? -ne 0 ]; then |
|
| 28 |
rgcc1="INVALID"; |
|
| 29 |
else |
|
| 30 |
rgcc1="VALID" |
|
| 31 |
fi |
|
| 32 |
# Removing Generated lusi file |
|
| 33 |
#grep generated ../${file}i > /dev/null
|
|
| 34 |
#if [ $? -ne 1 ];then |
|
| 35 |
# rm ../${file}i
|
|
| 36 |
#fi |
|
| 37 |
# Checking inlining |
|
| 38 |
$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus; |
|
| 39 |
if [ $? -ne 0 ]; then |
|
| 40 |
rlustrec2="INVALID"; |
|
| 25 |
rlustrec1="INVALID"; |
|
| 41 | 26 |
else |
| 42 |
rlustrec2="VALID"
|
|
| 27 |
rlustrec1="VALID"
|
|
| 43 | 28 |
fi |
| 44 | 29 |
pushd $build > /dev/null |
| 45 | 30 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
| 46 | 31 |
popd > /dev/null |
| 47 | 32 |
if [ $? -ne 0 ]; then |
| 48 |
rgcc2="INVALID";
|
|
| 33 |
rgcc1="INVALID";
|
|
| 49 | 34 |
else |
| 50 |
rgcc2="VALID"
|
|
| 35 |
rgcc1="VALID"
|
|
| 51 | 36 |
fi |
| 52 |
# Cheching witness |
|
| 53 |
pushd $build > /dev/null |
|
| 54 |
lustreh -horn -node check witness.lus 2>/dev/null |
|
| 55 |
popd > /dev/null |
|
| 56 |
z3="`z3 -t:10 witness.smt2 | xargs`" |
|
| 57 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
|
| 58 |
rinlining="VALID"; |
|
| 59 |
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then |
|
| 60 |
rinlining="ERROR"; |
|
| 61 |
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then |
|
| 62 |
rinlining="UNKNOWN"; |
|
| 63 |
else |
|
| 64 |
rinlining="INVALID" |
|
| 65 |
exit 1 |
|
| 66 |
fi |
|
| 67 |
# Checking horn backend |
|
| 68 |
$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus; |
|
| 69 |
echo z3 "$name".smt2 | grep unsat |
|
| 70 |
# TODO: This part of the script has to be optimized |
|
| 71 |
z3 -t:10 "$name".smt2 | grep unsat > /dev/null |
|
| 72 |
if [ $? -ne 0 ]; then |
|
| 73 |
rhorn="INVALID"; |
|
| 74 |
else |
|
| 75 |
rhorn="VALID" |
|
| 76 |
fi |
|
| 77 |
echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 78 | 37 |
else |
| 79 | 38 |
$LUSTREC -d $build -verbose 0 $opts "$name".lus; |
| 80 | 39 |
if [ $? -ne 0 ]; then |
| 81 |
rlustrec1="INVALID"; |
|
| 40 |
rlustrec1="INVALID";
|
|
| 82 | 41 |
else |
| 83 |
rlustrec1="VALID" |
|
| 42 |
rlustrec1="VALID"
|
|
| 84 | 43 |
fi |
| 85 | 44 |
pushd $build > /dev/null |
| 86 | 45 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
| 87 | 46 |
popd > /dev/null |
| 88 | 47 |
if [ $? -ne 0 ]; then |
| 89 |
rgcc1="INVALID"; |
|
| 48 |
rgcc1="INVALID";
|
|
| 90 | 49 |
else |
| 91 |
rgcc1="VALID" |
|
| 50 |
rgcc1="VALID"
|
|
| 92 | 51 |
fi |
| 93 |
$LUSTREC -horn -d $build -verbose 0 $opts ../$file |
|
| 94 |
echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 95 | 52 |
fi |
| 96 | 53 |
popd > /dev/null |
| 97 |
done < tests_ok.list |
|
| 54 |
echo "lustrec ($rlustrec1), gcc($rgcc1), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 55 |
done < $file_list |
|
| 56 |
} |
|
| 57 |
|
|
| 58 |
inline_compile () {
|
|
| 59 |
while IFS=, read -r file main opts |
|
| 60 |
do |
|
| 61 |
name=`basename "$file" .lus` |
|
| 62 |
dir=`dirname "$file"` |
|
| 63 |
|
|
| 64 |
pushd $dir > /dev/null |
|
| 65 |
|
|
| 66 |
# Checking inlining |
|
| 67 |
$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus; |
|
| 68 |
if [ $? -ne 0 ]; then |
|
| 69 |
rlustrec2="INVALID"; |
|
| 70 |
else |
|
| 71 |
rlustrec2="VALID" |
|
| 72 |
fi |
|
| 73 |
pushd $build > /dev/null |
|
| 74 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 75 |
popd > /dev/null |
|
| 76 |
if [ $? -ne 0 ]; then |
|
| 77 |
rgcc2="INVALID"; |
|
| 78 |
else |
|
| 79 |
rgcc2="VALID" |
|
| 80 |
fi |
|
| 81 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 82 |
popd > /dev/null |
|
| 83 |
done < $file_list |
|
| 84 |
} |
|
| 85 |
|
|
| 86 |
inline_compile_with_check () {
|
|
| 87 |
# Checking inlining |
|
| 88 |
while IFS=, read -r file main opts |
|
| 89 |
do |
|
| 90 |
name=`basename "$file" .lus` |
|
| 91 |
dir=`dirname "$file"` |
|
| 92 |
pushd $dir > /dev/null |
|
| 93 |
$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus; |
|
| 94 |
if [ $? -ne 0 ]; then |
|
| 95 |
rlustrec2="INVALID"; |
|
| 96 |
else |
|
| 97 |
rlustrec2="VALID" |
|
| 98 |
fi |
|
| 99 |
pushd $build > /dev/null |
|
| 100 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null |
|
| 101 |
popd > /dev/null |
|
| 102 |
if [ $? -ne 0 ]; then |
|
| 103 |
rgcc2="INVALID"; |
|
| 104 |
else |
|
| 105 |
rgcc2="VALID" |
|
| 106 |
fi |
|
| 107 |
# Cheching witness |
|
| 108 |
pushd $build > /dev/null |
|
| 109 |
lustrec -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
|
|
| 110 |
popd > /dev/null |
|
| 111 |
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
|
|
| 112 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
|
| 113 |
rinlining="VALID"; |
|
| 114 |
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then |
|
| 115 |
rinlining="ERROR"; |
|
| 116 |
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then |
|
| 117 |
rinlining="UNKNOWN"; |
|
| 118 |
else |
|
| 119 |
rinlining="INVALID" |
|
| 120 |
exit 1 |
|
| 121 |
fi |
|
| 122 |
echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 123 |
popd > /dev/null |
|
| 124 |
done < $file_list |
|
| 125 |
|
|
| 126 |
} |
|
| 127 |
|
|
| 128 |
check_prop () {
|
|
| 129 |
while IFS=, read -r file main opts |
|
| 130 |
do |
|
| 131 |
name=`basename "$file" .lus` |
|
| 132 |
dir=`dirname "$file"` |
|
| 133 |
pushd $dir > /dev/null |
|
| 134 |
|
|
| 135 |
# Checking horn backend |
|
| 136 |
if [ "$main" != "" ]; then |
|
| 137 |
$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus; |
|
| 138 |
else |
|
| 139 |
$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus |
|
| 140 |
fi |
|
| 141 |
# echo "z3 $build/$name".smt2 |
|
| 142 |
# TODO: This part of the script has to be optimized |
|
| 143 |
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null |
|
| 144 |
if [ $? -ne 0 ]; then |
|
| 145 |
rhorn="INVALID"; |
|
| 146 |
else |
|
| 147 |
rhorn="VALID" |
|
| 148 |
fi |
|
| 149 |
echo "horn-pdr ($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN" |
|
| 150 |
popd > /dev/null |
|
| 151 |
done < $file_list |
|
| 152 |
} |
|
| 153 |
|
|
| 154 |
usage () {
|
|
| 155 |
echo "usage: $0 [-aciwh] file_list" |
|
| 156 |
echo "-a: perform all steps" |
|
| 157 |
echo "-c: basic compilation" |
|
| 158 |
echo "-i: compile with inline mode" |
|
| 159 |
echo "-w: compile with inline mode. Check the inlining with z3" |
|
| 160 |
echo "-h: check files with the horn-pdf backend (requires z3)" |
|
| 161 |
} |
|
| 162 |
|
|
| 163 |
nobehavior=1 |
|
| 164 |
|
|
| 165 |
while [ $# -gt 0 ] ; do |
|
| 166 |
case "$1" in |
|
| 167 |
-v) shift ; verbose="$1"; shift ;; |
|
| 168 |
-a) nobehavior=0; c=1 ; w=1; h=1; shift ;; |
|
| 169 |
-c) nobehavior=0; c=1 ; shift ;; |
|
| 170 |
-i) nobehavior=0; i=1 ; shift ;; |
|
| 171 |
-w) nobehavior=0; w=1 ; shift ;; |
|
| 172 |
-h) nobehavior=0; h=1 ; shift ;; |
|
| 173 |
--) shift ;; |
|
| 174 |
-*) echo "bad option '$1'" ; exit 1 ;; |
|
| 175 |
*) files=("${files[@]}" "$1") ; shift ;;
|
|
| 176 |
esac |
|
| 177 |
done |
|
| 178 |
|
|
| 179 |
file_list=${files[0]}
|
|
| 180 |
|
|
| 181 |
|
|
| 182 |
if [ ${#files} -eq 0 ] ; then
|
|
| 183 |
echo input list required |
|
| 184 |
usage |
|
| 185 |
exit 1 |
|
| 186 |
fi |
|
| 187 |
|
|
| 188 |
[ ! -z "$c" ] && base_compile |
|
| 189 |
[ ! -z "$i" ] && inline_compile |
|
| 190 |
[ ! -z "$w" ] && inline_compile_with_check |
|
| 191 |
[ ! -z "$h" ] && check_prop |
|
| 192 |
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage |
|
| 193 |
|
|
| 194 |
|
|
| 195 |
# Removing Generated lusi file |
|
| 196 |
#grep generated ../${file}i > /dev/null
|
|
| 197 |
#if [ $? -ne 1 ];then |
|
| 198 |
# rm ../${file}i
|
|
| 199 |
#fi |
|
| 200 |
|
|
Also available in: Unified diff
Updated script. Does not seem to be fully functional yet.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@174 041b043f-8d7c-46b2-b46e-ef0dd855326e