Revision b3f91fdb
Added by Xavier Thirioux almost 8 years ago
| test/test-compile.sh | ||
|---|---|---|
| 14 | 14 |
mkdir -p build |
| 15 | 15 |
build=`pwd`"/build" |
| 16 | 16 |
|
| 17 |
gcc_compile() {
|
|
| 18 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null; |
|
| 19 |
if [ $? -ne 0 ]; then |
|
| 20 |
rgcc="INVALID"; |
|
| 21 |
else |
|
| 22 |
rgcc="VALID" |
|
| 23 |
fi |
|
| 24 |
} |
|
| 25 |
|
|
| 26 |
lustrec_compile() {
|
|
| 27 |
$LUSTREC "$@"; |
|
| 28 |
if [ $? -ne 0 ]; then |
|
| 29 |
rlustrec="INVALID"; |
|
| 30 |
else |
|
| 31 |
rlustrec="VALID" |
|
| 32 |
fi |
|
| 33 |
} |
|
| 17 | 34 |
|
| 18 | 35 |
base_compile() {
|
| 19 | 36 |
while IFS=, read -r file main opts |
| ... | ... | |
| 26 | 43 |
fi |
| 27 | 44 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 28 | 45 |
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 |
|
| 46 |
|
|
| 47 |
if [ "$main" != "" ]; then |
|
| 48 |
lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext; |
|
| 44 | 49 |
else |
| 45 |
rgcc1="NONE"
|
|
| 50 |
lustrec_compile -d $build -verbose 0 $opts $name$ext
|
|
| 46 | 51 |
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 | 52 |
pushd $build > /dev/null |
| 53 |
|
|
| 56 | 54 |
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 |
|
| 55 |
gcc_compile "$name"; |
|
| 63 | 56 |
else |
| 64 |
rgcc1="NONE"
|
|
| 57 |
rgcc="NONE" |
|
| 65 | 58 |
fi |
| 66 | 59 |
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;
|
|
| 60 |
popd > /dev/null
|
|
| 61 |
|
|
| 62 |
if [ $verbose -gt 0 ]; then
|
|
| 63 |
echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
|
|
| 64 |
else
|
|
| 65 |
echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 66 |
fi;
|
|
| 74 | 67 |
done < $file_list |
| 75 | 68 |
} |
| 76 | 69 |
|
| ... | ... | |
| 78 | 71 |
while IFS=, read -r file main opts |
| 79 | 72 |
do |
| 80 | 73 |
name=`basename "$file" .lus` |
| 74 |
ext=".lus" |
|
| 81 | 75 |
if [ `dirname "$file"`/"$name" = "$file" ]; then |
| 82 |
return 0 |
|
| 76 |
name=`basename "$file" .lusi` |
|
| 77 |
ext=".lusi" |
|
| 83 | 78 |
fi |
| 84 | 79 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 85 |
|
|
| 86 | 80 |
pushd $dir > /dev/null |
| 87 | 81 |
|
| 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 |
|
| 82 |
if [ "$main" != "" ]; then |
|
| 83 |
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext; |
|
| 84 |
else |
|
| 85 |
if [ "$ext" = ".lusi" ]; then |
|
| 86 |
lustrec_compile -d $build -verbose 0 $opts $name$ext; |
|
| 87 |
else |
|
| 88 |
rlustrec="NONE" |
|
| 89 |
rgcc="NONE" |
|
| 90 |
fi |
|
| 91 |
fi |
|
| 92 |
pushd $build > /dev/null |
|
| 93 |
|
|
| 94 |
if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
|
| 95 |
gcc_compile "$name"; |
|
| 96 |
else |
|
| 97 |
rgcc="NONE" |
|
| 98 |
fi |
|
| 99 |
popd > /dev/null |
|
| 100 |
popd > /dev/null |
|
| 101 |
|
|
| 102 |
if [ $verbose -gt 0 ]; then |
|
| 103 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
|
|
| 104 |
else |
|
| 105 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 106 |
fi; |
|
| 107 |
done < $file_list |
|
| 110 | 108 |
} |
| 111 | 109 |
|
| 112 | 110 |
inline_compile_with_check () {
|
| ... | ... | |
| 119 | 117 |
fi |
| 120 | 118 |
dir=${SRC_PREFIX}/`dirname "$file"`
|
| 121 | 119 |
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 |
|
| 120 |
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus" |
|
| 121 |
|
|
| 128 | 122 |
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 |
|
| 123 |
gcc_compile "$name" |
|
| 124 |
|
|
| 135 | 125 |
popd > /dev/null |
| 136 | 126 |
# Cheching witness |
| 137 | 127 |
pushd $build > /dev/null |
| 138 |
$LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
|
|
| 128 |
lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
|
|
| 139 | 129 |
popd > /dev/null |
| 140 | 130 |
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
|
| 141 | 131 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
| ... | ... | |
| 148 | 138 |
rinlining="INVALID/TIMEOUT" |
| 149 | 139 |
fi |
| 150 | 140 |
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;
|
|
| 141 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
|
|
| 152 | 142 |
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"
|
|
| 143 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
|
|
| 154 | 144 |
fi |
| 155 | 145 |
popd > /dev/null |
| 156 | 146 |
done < $file_list |
| ... | ... | |
| 169 | 159 |
|
| 170 | 160 |
# Checking horn backend |
| 171 | 161 |
if [ "$main" != "" ]; then |
| 172 |
$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
|
|
| 162 |
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
|
|
| 173 | 163 |
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" |
|
| 164 |
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus" |
|
| 180 | 165 |
fi |
| 166 |
|
|
| 181 | 167 |
# echo "z3 $build/$name".smt2 |
| 182 | 168 |
# TODO: This part of the script has to be optimized |
| 183 | 169 |
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null |
| ... | ... | |
| 231 | 217 |
exit 1 |
| 232 | 218 |
fi |
| 233 | 219 |
|
| 220 |
# cleaning directory $build |
|
| 221 |
|
|
| 222 |
rm -f "$build"/* 2> /dev/null |
|
| 223 |
|
|
| 224 |
# executing tests |
|
| 225 |
|
|
| 234 | 226 |
[ ! -z "$c" ] && base_compile |
| 235 | 227 |
[ ! -z "$i" ] && inline_compile |
| 236 | 228 |
[ ! -z "$w" ] && inline_compile_with_check |
Also available in: Unified diff
LOTS of bug correction wrt inlining, still a work in progress...
- global constants were not accounted for
- no good avoidance of name capture when inlining
- static parameters (array sizes and clocks) not handled
- ill-typed generated expressions, when inlining array expressions