lustrec / test / test-compile.sh.in @ 66e25f0f
History | View | Annotate | Download (7.29 KB)
| 1 |
#!/bin/bash |
|---|---|
| 2 |
|
| 3 |
eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@") |
| 4 |
|
| 5 |
declare c i w h a v |
| 6 |
declare -a files |
| 7 |
|
| 8 |
SRC_PREFIX=@SRC_PATH@-tests/ |
| 9 |
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler |
| 10 |
NOW=`date "+%y%m%d%H%M"` |
| 11 |
report=`pwd`/report-@PACKAGE_VERSION@-$NOW |
| 12 |
LUSTREC=lustrec |
| 13 |
mkdir -p build |
| 14 |
build=`pwd`"/build" |
| 15 |
|
| 16 |
gcc_compile() {
|
| 17 |
if [ $verbose -gt 1 ]; then |
| 18 |
echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null" |
| 19 |
fi |
| 20 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null; |
| 21 |
if [ $? -ne 0 ]; then |
| 22 |
rgcc="INVALID"; |
| 23 |
else |
| 24 |
rgcc="VALID" |
| 25 |
fi |
| 26 |
} |
| 27 |
|
| 28 |
lustrec_compile() {
|
| 29 |
if [ $verbose -gt 1 ]; then |
| 30 |
echo "$LUSTREC $@" |
| 31 |
fi |
| 32 |
$LUSTREC "$@"; |
| 33 |
if [ $? -ne 0 ]; then |
| 34 |
rlustrec="INVALID"; |
| 35 |
else |
| 36 |
rlustrec="VALID" |
| 37 |
fi |
| 38 |
} |
| 39 |
|
| 40 |
base_compile() {
|
| 41 |
while IFS=, read -r file main opts |
| 42 |
do |
| 43 |
name=`basename "$file" .lus` |
| 44 |
ext=".lus" |
| 45 |
if [ `dirname "$file"`/"$name" = "$file" ]; then |
| 46 |
name=`basename "$file" .lusi` |
| 47 |
ext=".lusi" |
| 48 |
fi |
| 49 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 50 |
pushd $dir > /dev/null |
| 51 |
|
| 52 |
if [ "$main" != "" ]; then |
| 53 |
lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext; |
| 54 |
else |
| 55 |
lustrec_compile -d $build -verbose 0 $opts $name$ext |
| 56 |
fi |
| 57 |
pushd $build > /dev/null |
| 58 |
|
| 59 |
if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
| 60 |
gcc_compile "$name"; |
| 61 |
else |
| 62 |
rgcc="NONE" |
| 63 |
fi |
| 64 |
popd > /dev/null |
| 65 |
popd > /dev/null |
| 66 |
|
| 67 |
if [ $verbose -gt 0 ]; then |
| 68 |
echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
|
| 69 |
else |
| 70 |
echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
| 71 |
fi; |
| 72 |
done < $file_list |
| 73 |
} |
| 74 |
|
| 75 |
inline_compile () {
|
| 76 |
while IFS=, read -r file main opts |
| 77 |
do |
| 78 |
name=`basename "$file" .lus` |
| 79 |
ext=".lus" |
| 80 |
if [ `dirname "$file"`/"$name" = "$file" ]; then |
| 81 |
name=`basename "$file" .lusi` |
| 82 |
ext=".lusi" |
| 83 |
fi |
| 84 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 85 |
pushd $dir > /dev/null |
| 86 |
|
| 87 |
if [ "$main" != "" ]; then |
| 88 |
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext; |
| 89 |
else |
| 90 |
if [ "$ext" = ".lusi" ]; then |
| 91 |
lustrec_compile -d $build -verbose 0 $opts $name$ext; |
| 92 |
else |
| 93 |
rlustrec="NONE" |
| 94 |
rgcc="NONE" |
| 95 |
fi |
| 96 |
fi |
| 97 |
pushd $build > /dev/null |
| 98 |
|
| 99 |
if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
| 100 |
gcc_compile "$name"; |
| 101 |
else |
| 102 |
rgcc="NONE" |
| 103 |
fi |
| 104 |
popd > /dev/null |
| 105 |
popd > /dev/null |
| 106 |
|
| 107 |
if [ $verbose -gt 0 ]; then |
| 108 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
|
| 109 |
else |
| 110 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
| 111 |
fi; |
| 112 |
done < $file_list |
| 113 |
} |
| 114 |
|
| 115 |
inline_compile_with_check () {
|
| 116 |
# Checking inlining |
| 117 |
while IFS=, read -r file main opts |
| 118 |
do |
| 119 |
name=`basename "$file" .lus` |
| 120 |
ext=".lus" |
| 121 |
if [ `dirname "$file"`/"$name" = "$file" ]; then |
| 122 |
name=`basename "$file" .lusi` |
| 123 |
ext=".lusi" |
| 124 |
fi |
| 125 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 126 |
pushd $dir > /dev/null |
| 127 |
|
| 128 |
if [ "$main" != "" ]; then |
| 129 |
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext; |
| 130 |
else |
| 131 |
if [ "$ext" = ".lusi" ]; then |
| 132 |
lustrec_compile -d $build -verbose 0 $opts $name$ext; |
| 133 |
else |
| 134 |
rlustrec="NONE" |
| 135 |
rgcc="NONE" |
| 136 |
fi |
| 137 |
fi |
| 138 |
popd > /dev/null |
| 139 |
pushd $build > /dev/null |
| 140 |
|
| 141 |
if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
| 142 |
gcc_compile "$name"; |
| 143 |
else |
| 144 |
rgcc="NONE" |
| 145 |
fi |
| 146 |
# Cheching witness |
| 147 |
|
| 148 |
if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
| 149 |
mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus
|
| 150 |
lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus
|
| 151 |
z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"
|
| 152 |
if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then |
| 153 |
rinlining="VALID"; |
| 154 |
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then |
| 155 |
rinlining="ERROR"; |
| 156 |
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then |
| 157 |
rinlining="UNKNOWN"; |
| 158 |
elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then |
| 159 |
rinlining="TIMEOUT" |
| 160 |
else |
| 161 |
rinlining="INVALID" |
| 162 |
fi |
| 163 |
else |
| 164 |
rinlining="NONE" |
| 165 |
fi |
| 166 |
popd > /dev/null |
| 167 |
|
| 168 |
if [ $verbose -gt 0 ]; then |
| 169 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
|
| 170 |
else |
| 171 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
|
| 172 |
fi |
| 173 |
done < $file_list |
| 174 |
|
| 175 |
} |
| 176 |
|
| 177 |
check_prop () {
|
| 178 |
while IFS=, read -r file main opts |
| 179 |
do |
| 180 |
name=`basename "$file" .lus` |
| 181 |
if [ "$name" = "$file" ]; then |
| 182 |
return 0 |
| 183 |
fi |
| 184 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 185 |
pushd $dir > /dev/null |
| 186 |
|
| 187 |
# Checking horn backend |
| 188 |
if [ "$main" != "" ]; then |
| 189 |
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus"; |
| 190 |
else |
| 191 |
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus" |
| 192 |
fi |
| 193 |
|
| 194 |
# echo "z3 $build/$name".smt2 |
| 195 |
# TODO: This part of the script has to be optimized |
| 196 |
z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"
|
| 197 |
if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then |
| 198 |
rhorn="VALID"; |
| 199 |
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then |
| 200 |
rhorn="ERROR"; |
| 201 |
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then |
| 202 |
rhorn="UNKNOWN"; |
| 203 |
elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then |
| 204 |
rhorn="TIMEOUT" |
| 205 |
else |
| 206 |
rhorn="INVALID" |
| 207 |
fi |
| 208 |
if [ $verbose -gt 0 ]; then |
| 209 |
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
|
| 210 |
else |
| 211 |
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
| 212 |
fi |
| 213 |
popd > /dev/null |
| 214 |
done < $file_list |
| 215 |
} |
| 216 |
|
| 217 |
usage () {
|
| 218 |
echo "usage: $0 [-aciwh] file_list" |
| 219 |
echo "-a: perform all steps" |
| 220 |
echo "-c: basic compilation" |
| 221 |
echo "-i: compile with inline mode" |
| 222 |
echo "-w: compile with inline mode. Check the inlining with z3" |
| 223 |
echo "-h: check files with the horn-pdf backend (requires z3)" |
| 224 |
echo "-v <int>: verbose level" |
| 225 |
} |
| 226 |
|
| 227 |
verbose=0 |
| 228 |
nobehavior=1 |
| 229 |
|
| 230 |
while [ $# -gt 0 ] ; do |
| 231 |
case "$1" in |
| 232 |
-v) shift ; verbose="$1"; shift ;; |
| 233 |
-a) nobehavior=0; c=1 ; w=1; h=1; shift ;; |
| 234 |
-c) nobehavior=0; c=1 ; shift ;; |
| 235 |
-i) nobehavior=0; i=1 ; shift ;; |
| 236 |
-w) nobehavior=0; w=1 ; shift ;; |
| 237 |
-h) nobehavior=0; h=1 ; shift ;; |
| 238 |
--) shift ;; |
| 239 |
-*) echo "bad option '$1'" ; exit 1 ;; |
| 240 |
*) files=("${files[@]}" "$1") ; shift ;;
|
| 241 |
esac |
| 242 |
done |
| 243 |
|
| 244 |
file_list=${files[0]}
|
| 245 |
|
| 246 |
|
| 247 |
if [ ${#files} -eq 0 ] ; then
|
| 248 |
echo input list required |
| 249 |
usage |
| 250 |
exit 1 |
| 251 |
fi |
| 252 |
|
| 253 |
# cleaning directory $build |
| 254 |
|
| 255 |
rm -f "$build"/* 2> /dev/null |
| 256 |
|
| 257 |
# executing tests |
| 258 |
|
| 259 |
[ ! -z "$c" ] && base_compile |
| 260 |
[ ! -z "$i" ] && inline_compile |
| 261 |
[ ! -z "$w" ] && inline_compile_with_check |
| 262 |
[ ! -z "$h" ] && check_prop |
| 263 |
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage |
| 264 |
|
| 265 |
|
| 266 |
# Removing Generated lusi file |
| 267 |
#grep generated ../${file}i > /dev/null
|
| 268 |
#if [ $? -ne 1 ];then |
| 269 |
# rm ../${file}i
|
| 270 |
#fi |
| 271 |
|