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