Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
test/test-compile.sh | ||
---|---|---|
5 | 5 |
declare c i w h a v |
6 | 6 |
declare -a files |
7 | 7 |
|
8 |
#SRC_PREFIX="../.."
|
|
9 |
SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler |
|
8 |
SRC_PREFIX=/Users/Teme/Documents/GitHub/onera_lustrec-tests/
|
|
9 |
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
|
|
10 | 10 |
NOW=`date "+%y%m%d%H%M"` |
11 |
report=`pwd`/report-$NOW |
|
12 |
#LUSTREC="../../_build/src/lustrec" |
|
11 |
report=`pwd`/report-1.3- 459-$NOW |
|
13 | 12 |
LUSTREC=lustrec |
14 | 13 |
mkdir -p build |
15 | 14 |
build=`pwd`"/build" |
16 | 15 |
|
17 | 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 |
|
18 | 20 |
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null; |
19 | 21 |
if [ $? -ne 0 ]; then |
20 | 22 |
rgcc="INVALID"; |
... | ... | |
24 | 26 |
} |
25 | 27 |
|
26 | 28 |
lustrec_compile() { |
29 |
if [ $verbose -gt 1 ]; then |
|
30 |
echo "$LUSTREC $@" |
|
31 |
fi |
|
27 | 32 |
$LUSTREC "$@"; |
28 | 33 |
if [ $? -ne 0 ]; then |
29 | 34 |
rlustrec="INVALID"; |
... | ... | |
112 | 117 |
while IFS=, read -r file main opts |
113 | 118 |
do |
114 | 119 |
name=`basename "$file" .lus` |
115 |
if [ "$name" = "$file" ]; then |
|
116 |
return 0 |
|
120 |
ext=".lus" |
|
121 |
if [ `dirname "$file"`/"$name" = "$file" ]; then |
|
122 |
name=`basename "$file" .lusi` |
|
123 |
ext=".lusi" |
|
117 | 124 |
fi |
118 | 125 |
dir=${SRC_PREFIX}/`dirname "$file"` |
119 | 126 |
pushd $dir > /dev/null |
120 |
lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus" |
|
121 | 127 |
|
122 |
pushd $build > /dev/null |
|
123 |
gcc_compile "$name" |
|
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 |
|
124 | 140 |
|
125 |
popd > /dev/null |
|
141 |
if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then |
|
142 |
gcc_compile "$name"; |
|
143 |
else |
|
144 |
rgcc="NONE" |
|
145 |
fi |
|
126 | 146 |
# Cheching witness |
127 |
pushd $build > /dev/null |
|
128 |
lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus |
|
129 |
popd > /dev/null |
|
130 |
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`" |
|
131 |
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then |
|
132 |
rinlining="VALID"; |
|
133 |
elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then |
|
134 |
rinlining="ERROR"; |
|
135 |
elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then |
|
136 |
rinlining="UNKNOWN"; |
|
137 |
else |
|
138 |
rinlining="INVALID/TIMEOUT" |
|
139 |
fi |
|
140 |
if [ $verbose -gt 0 ]; then |
|
141 |
echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
|
142 |
else |
|
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" |
|
144 |
fi |
|
145 |
popd > /dev/null |
|
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 |
|
146 | 173 |
done < $file_list |
147 | 174 |
|
148 | 175 |
} |
... | ... | |
159 | 186 |
|
160 | 187 |
# Checking horn backend |
161 | 188 |
if [ "$main" != "" ]; then |
162 |
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
|
|
189 |
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
|
|
163 | 190 |
else |
164 |
lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
|
|
191 |
lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
|
|
165 | 192 |
fi |
166 | 193 |
|
167 | 194 |
# echo "z3 $build/$name".smt2 |
168 | 195 |
# TODO: This part of the script has to be optimized |
169 |
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null |
|
170 |
if [ $? -ne 0 ]; then |
|
171 |
rhorn="INVALID"; |
|
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" |
|
172 | 205 |
else |
173 |
rhorn="VALID"
|
|
206 |
rhorn="INVALID"
|
|
174 | 207 |
fi |
175 | 208 |
if [ $verbose -gt 0 ]; then |
176 | 209 |
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report; |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04