Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ 9f77bff7

History | View | Annotate | Download (7.31 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=/Users/Teme/Documents/GitHub/lustrec-tests/
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-1.3-      55-$NOW
12
LUSTREC=lustrec
13
mkdir -p build
14
build=`pwd`"/build"
15

    
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
20
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
21
    if [ $? -ne 0 ]; then
22
	rgcc="INVALID";
23
    else
24
	rgcc="VALID"
25
    fi
26
}
27

    
28
lustrec_compile() {
29
    if [ $verbose -gt 1 ]; then
30
       echo "$LUSTREC $@"
31
    fi
32
    $LUSTREC "$@";
33
    if [ $? -ne 0 ]; then
34
        rlustrec="INVALID";
35
    else
36
        rlustrec="VALID"
37
    fi
38
}
39

    
40
base_compile() {
41
    while IFS=, read -r file main opts
42
    do
43
	name=`basename "$file" .lus`
44
        ext=".lus"
45
	if [ `dirname "$file"`/"$name" = "$file" ]; then
46
	    name=`basename "$file" .lusi`
47
	    ext=".lusi"
48
	fi
49
        dir=${SRC_PREFIX}/`dirname "$file"`
50
	pushd $dir > /dev/null
51

    
52
	if [ "$main" != "" ]; then
53
	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
54
	else
55
	    lustrec_compile -d $build -verbose 0 $opts $name$ext
56
	fi
57
	pushd $build > /dev/null
58

    
59
	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
60
            gcc_compile "$name";
61
	else
62
	    rgcc="NONE"
63
	fi
64
	popd > /dev/null
65
	popd > /dev/null
66

    
67
	if [ $verbose -gt 0 ]; then
68
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
69
	else
70
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
71
	fi;
72
    done < $file_list
73
}
74

    
75
inline_compile () {
76
    while IFS=, read -r file main opts
77
    do
78
	name=`basename "$file" .lus`
79
	ext=".lus"
80
	if [ `dirname "$file"`/"$name" = "$file" ]; then
81
	    name=`basename "$file" .lusi`
82
	    ext=".lusi"
83
	fi
84
	dir=${SRC_PREFIX}/`dirname "$file"`
85
	pushd $dir > /dev/null
86

    
87
	if [ "$main" != "" ]; then
88
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
89
	else
90
	    if [ "$ext" = ".lusi" ]; then
91
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
92
	    else
93
		rlustrec="NONE"
94
		rgcc="NONE"
95
	    fi
96
	fi
97
	pushd $build > /dev/null
98

    
99
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
100
	    gcc_compile "$name";
101
	else
102
	    rgcc="NONE"
103
	fi
104
	popd > /dev/null
105
	popd > /dev/null
106

    
107
	if [ $verbose -gt 0 ]; then
108
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
109
	else
110
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
111
	fi;
112
    done < $file_list
113
}
114

    
115
inline_compile_with_check () {
116
# Checking inlining
117
    while IFS=, read -r file main opts
118
    do
119
	name=`basename "$file" .lus`
120
	ext=".lus"
121
	if [ `dirname "$file"`/"$name" = "$file" ]; then
122
	    name=`basename "$file" .lusi`
123
	    ext=".lusi"
124
	fi
125
	dir=${SRC_PREFIX}/`dirname "$file"`
126
	pushd $dir > /dev/null
127

    
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
140
	
141
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
142
	    gcc_compile "$name";
143
	else
144
	    rgcc="NONE"
145
	fi
146
	# Cheching witness
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
173
done < $file_list
174

    
175
}
176

    
177
check_prop () {
178
    while IFS=, read -r file main opts
179
    do
180
	name=`basename "$file" .lus`
181
	if [ "$name" = "$file" ]; then
182
	    return 0
183
	fi
184
	dir=${SRC_PREFIX}/`dirname "$file"`
185
	pushd $dir > /dev/null
186
	
187
    # Checking horn backend
188
    if [ "$main" != "" ]; then
189
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
190
    else
191
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
192
    fi
193

    
194
    # echo "z3 $build/$name".smt2 
195
    # TODO: This part of the script has to be optimized
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"
205
    else
206
	rhorn="INVALID"
207
    fi
208
    if [ $verbose -gt 0 ]; then
209
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
210
    else
211
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
212
    fi
213
    popd > /dev/null
214
done < $file_list
215
}
216

    
217
usage () {
218
echo "usage: $0 [-aciwh] file_list"
219
echo "-a: perform all steps"
220
echo "-c: basic compilation"
221
echo "-i: compile with inline mode"
222
echo "-w: compile with inline mode. Check the inlining with z3"
223
echo "-h: check files with the horn-pdf backend (requires z3)"
224
echo "-v <int>: verbose level"
225
}
226

    
227
verbose=0
228
nobehavior=1
229

    
230
while [ $# -gt 0 ] ; do
231
        case "$1" in
232
	        -v) shift ; verbose="$1"; shift ;;
233
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
234
                -c) nobehavior=0; c=1 ; shift ;;
235
                -i) nobehavior=0; i=1 ; shift ;;
236
                -w) nobehavior=0; w=1 ; shift ;;
237
                -h) nobehavior=0; h=1 ; shift ;;
238
                --) shift ;;
239
                -*) echo "bad option '$1'" ; exit 1 ;;
240
                *) files=("${files[@]}" "$1") ; shift ;;
241
         esac
242
done
243

    
244
file_list=${files[0]}
245

    
246

    
247
if [ ${#files} -eq 0 ] ; then
248
    echo input list required
249
    usage
250
    exit 1
251
fi
252

    
253
# cleaning directory $build
254

    
255
rm -f "$build"/* 2> /dev/null
256

    
257
# executing tests
258

    
259
[ ! -z "$c" ] && base_compile
260
[ ! -z "$i" ] && inline_compile
261
[ ! -z "$w" ] && inline_compile_with_check
262
[ ! -z "$h" ] && check_prop
263
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
264

    
265

    
266
	# Removing Generated lusi file
267
	#grep generated ../${file}i > /dev/null
268
	#if [ $? -ne 1 ];then
269
	#  rm ../${file}i
270
	#fi
271