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