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 |
|