Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ b3f91fdb

History | View | Annotate | Download (6.33 KB)

1 0cbf0839 ploc
#!/bin/bash
2
3 1699b8ff ploc
eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
4 626e6f03 ploc
5 1699b8ff ploc
declare c i w h a v
6 626e6f03 ploc
declare -a files
7
8 6cf31814 xthirioux
#SRC_PREFIX="../.."
9
SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10 0cbf0839 ploc
NOW=`date "+%y%m%d%H%M"`
11 626e6f03 ploc
report=`pwd`/report-$NOW
12 b8ae1bbc ploc
#LUSTREC="../../_build/src/lustrec"
13
LUSTREC=lustrec
14 0cbf0839 ploc
mkdir -p build
15 8b3afe43 xthirioux
build=`pwd`"/build"
16 3f823d04 xthirioux
17 b3f91fdb xthirioux
gcc_compile() {
18
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
19
    if [ $? -ne 0 ]; then
20
	rgcc="INVALID";
21
    else
22
	rgcc="VALID"
23
    fi
24
}
25
26
lustrec_compile() {
27
    $LUSTREC "$@";
28
    if [ $? -ne 0 ]; then
29
        rlustrec="INVALID";
30
    else
31
        rlustrec="VALID"
32
    fi
33
}
34 626e6f03 ploc
35
base_compile() {
36
    while IFS=, read -r file main opts
37
    do
38
	name=`basename "$file" .lus`
39 3f823d04 xthirioux
        ext=".lus"
40
	if [ `dirname "$file"`/"$name" = "$file" ]; then
41
	    name=`basename "$file" .lusi`
42
	    ext=".lusi"
43
	fi
44
        dir=${SRC_PREFIX}/`dirname "$file"`
45 626e6f03 ploc
	pushd $dir > /dev/null
46 b3f91fdb xthirioux
47
	if [ "$main" != "" ]; then
48
	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
49 3f823d04 xthirioux
	else
50 b3f91fdb xthirioux
	    lustrec_compile -d $build -verbose 0 $opts $name$ext
51 3f823d04 xthirioux
	fi
52 8b3afe43 xthirioux
	pushd $build > /dev/null
53 b3f91fdb xthirioux
54 7dd90f72 xthirioux
	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
55 b3f91fdb xthirioux
            gcc_compile "$name";
56 3f823d04 xthirioux
	else
57 b3f91fdb xthirioux
	    rgcc="NONE"
58 3f823d04 xthirioux
	fi
59 8b3afe43 xthirioux
	popd > /dev/null
60 b3f91fdb xthirioux
	popd > /dev/null
61
62
	if [ $verbose -gt 0 ]; then
63
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
64
	else
65
	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
66
	fi;
67 626e6f03 ploc
    done < $file_list
68
}
69
70
inline_compile () {
71
    while IFS=, read -r file main opts
72
    do
73
	name=`basename "$file" .lus`
74 b3f91fdb xthirioux
	ext=".lus"
75 3f823d04 xthirioux
	if [ `dirname "$file"`/"$name" = "$file" ]; then
76 b3f91fdb xthirioux
	    name=`basename "$file" .lusi`
77
	    ext=".lusi"
78 3f823d04 xthirioux
	fi
79 1699b8ff ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
80 626e6f03 ploc
	pushd $dir > /dev/null
81
82 b3f91fdb xthirioux
	if [ "$main" != "" ]; then
83
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
84
	else
85
	    if [ "$ext" = ".lusi" ]; then
86
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
87
	    else
88
		rlustrec="NONE"
89
		rgcc="NONE"
90
	    fi
91
	fi
92
	pushd $build > /dev/null
93
94
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
95
	    gcc_compile "$name";
96
	else
97
	    rgcc="NONE"
98
	fi
99
	popd > /dev/null
100
	popd > /dev/null
101
102
	if [ $verbose -gt 0 ]; then
103
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
104
	else
105
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
106
	fi;
107
    done < $file_list
108 626e6f03 ploc
}
109
110
inline_compile_with_check () {
111
# Checking inlining
112
    while IFS=, read -r file main opts
113
    do
114
	name=`basename "$file" .lus`
115 3f823d04 xthirioux
	if [ "$name" = "$file" ]; then
116
	    return 0
117
	fi
118 1699b8ff ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
119 626e6f03 ploc
	pushd $dir > /dev/null
120 b3f91fdb xthirioux
    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
121
122 626e6f03 ploc
    pushd $build > /dev/null
123 b3f91fdb xthirioux
    gcc_compile "$name"
124
	
125 3f823d04 xthirioux
    popd > /dev/null
126 626e6f03 ploc
	# Cheching witness
127
    pushd $build > /dev/null
128 b3f91fdb xthirioux
    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
129 626e6f03 ploc
    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 839ca600 ploc
	rinlining="INVALID/TIMEOUT"
139 626e6f03 ploc
    fi  
140 1699b8ff ploc
    if [ $verbose -gt 0 ]; then
141 b3f91fdb xthirioux
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
142 1699b8ff ploc
    else
143 b3f91fdb xthirioux
	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 1699b8ff ploc
    fi
145 626e6f03 ploc
    popd > /dev/null
146
done < $file_list
147
148
}
149
150
check_prop () {
151
    while IFS=, read -r file main opts
152
    do
153
	name=`basename "$file" .lus`
154 3f823d04 xthirioux
	if [ "$name" = "$file" ]; then
155
	    return 0
156
	fi
157 1699b8ff ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
158 626e6f03 ploc
	pushd $dir > /dev/null
159
	
160
    # Checking horn backend
161
    if [ "$main" != "" ]; then
162 b3f91fdb xthirioux
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
163 626e6f03 ploc
    else
164 b3f91fdb xthirioux
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
165 36454535 ploc
    fi
166 b3f91fdb xthirioux
167 626e6f03 ploc
    # echo "z3 $build/$name".smt2 
168
    # 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";
172
    else
173
        rhorn="VALID"
174
    fi
175 1699b8ff ploc
    if [ $verbose -gt 0 ]; then
176 36454535 ploc
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
177 1699b8ff ploc
    else
178 36454535 ploc
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
179 1699b8ff ploc
    fi
180 626e6f03 ploc
    popd > /dev/null
181
done < $file_list
182
}
183
184
usage () {
185
echo "usage: $0 [-aciwh] file_list"
186
echo "-a: perform all steps"
187
echo "-c: basic compilation"
188
echo "-i: compile with inline mode"
189
echo "-w: compile with inline mode. Check the inlining with z3"
190
echo "-h: check files with the horn-pdf backend (requires z3)"
191 1699b8ff ploc
echo "-v <int>: verbose level"
192 626e6f03 ploc
}
193
194 1699b8ff ploc
verbose=0
195 626e6f03 ploc
nobehavior=1
196
197
while [ $# -gt 0 ] ; do
198
        case "$1" in
199
	        -v) shift ; verbose="$1"; shift ;;
200
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
201
                -c) nobehavior=0; c=1 ; shift ;;
202
                -i) nobehavior=0; i=1 ; shift ;;
203
                -w) nobehavior=0; w=1 ; shift ;;
204
                -h) nobehavior=0; h=1 ; shift ;;
205
                --) shift ;;
206
                -*) echo "bad option '$1'" ; exit 1 ;;
207
                *) files=("${files[@]}" "$1") ; shift ;;
208
         esac
209
done
210
211
file_list=${files[0]}
212
213
214
if [ ${#files} -eq 0 ] ; then
215
    echo input list required
216
    usage
217
    exit 1
218
fi
219
220 b3f91fdb xthirioux
# cleaning directory $build
221
222
rm -f "$build"/* 2> /dev/null
223
224
# executing tests
225
226 626e6f03 ploc
[ ! -z "$c" ] && base_compile
227
[ ! -z "$i" ] && inline_compile
228
[ ! -z "$w" ] && inline_compile_with_check
229
[ ! -z "$h" ] && check_prop
230
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
231
232
233
	# Removing Generated lusi file
234
	#grep generated ../${file}i > /dev/null
235
	#if [ $? -ne 1 ];then
236
	#  rm ../${file}i
237
	#fi