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