Project

General

Profile

Revision a1daa793 test/test-compile.sh

View differences:

test/test-compile.sh
14 14
mkdir -p build
15 15
build=`pwd`"/build"
16 16

  
17
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
}
17 34

  
18 35
base_compile() {
19 36
    while IFS=, read -r file main opts
......
26 43
	fi
27 44
        dir=${SRC_PREFIX}/`dirname "$file"`
28 45
	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
46

  
47
	if [ "$main" != "" ]; then
48
	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
44 49
	else
45
	    rgcc1="NONE"
50
	    lustrec_compile -d $build -verbose 0 $opts $name$ext
46 51
	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 52
	pushd $build > /dev/null
56
	if [ $ext = ".lus" ]; 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
53

  
54
	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
55
            gcc_compile "$name";
63 56
	else
64
	    rgcc1="NONE"
57
	    rgcc="NONE"
65 58
	fi
66 59
	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;
60
	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;
74 67
    done < $file_list
75 68
}
76 69

  
......
78 71
    while IFS=, read -r file main opts
79 72
    do
80 73
	name=`basename "$file" .lus`
74
	ext=".lus"
81 75
	if [ `dirname "$file"`/"$name" = "$file" ]; then
82
	    return 0
76
	    name=`basename "$file" .lusi`
77
	    ext=".lusi"
83 78
	fi
84 79
	dir=${SRC_PREFIX}/`dirname "$file"`
85

  
86 80
	pushd $dir > /dev/null
87 81

  
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
82
	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
110 108
}
111 109

  
112 110
inline_compile_with_check () {
......
119 117
	fi
120 118
	dir=${SRC_PREFIX}/`dirname "$file"`
121 119
	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
120
    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
121

  
128 122
    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
123
    gcc_compile "$name"
124
	
135 125
    popd > /dev/null
136 126
	# Cheching witness
137 127
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
128
    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
139 129
    popd > /dev/null
140 130
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 131
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
146 136
	rinlining="UNKNOWN";
147 137
    else
148 138
	rinlining="INVALID/TIMEOUT"
149
    fi
139
    fi  
150 140
    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;
141
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
152 142
    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"
143
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
154 144
    fi
155 145
    popd > /dev/null
156 146
done < $file_list
......
166 156
	fi
167 157
	dir=${SRC_PREFIX}/`dirname "$file"`
168 158
	pushd $dir > /dev/null
169

  
159
	
170 160
    # Checking horn backend
171 161
    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";
162
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
178 163
    else
179
        rlustrec="VALID"
164
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
180 165
    fi
181
    # echo "z3 $build/$name".smt2
166

  
167
    # echo "z3 $build/$name".smt2 
182 168
    # TODO: This part of the script has to be optimized
183 169
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
184 170
    if [ $? -ne 0 ]; then
......
195 181
done < $file_list
196 182
}
197 183

  
198
check_horn () {
199
    while IFS=, read -r file main opts
200
    do
201
	name=`basename "$file" .lus`
202
	if [ "$name" = "$file" ]; then
203
	    return 0
204
	fi
205
	dir=${SRC_PREFIX}/`dirname "$file"`
206
	pushd $dir > /dev/null
207

  
208
    # Checking horn backend
209
    if [ "$main" != "" ]; then
210
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
211
    else
212
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
213
    fi
214
    if [ $? -ne 0 ]; then
215
        rlustrec="INVALID";
216
    else
217
        rlustrec="VALID"
218
    fi
219
    if [ $verbose -gt 0 ]; then
220
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
221
    else
222
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
223
    fi
224
    popd > /dev/null
225
done < $file_list
226
}
227

  
228 184
usage () {
229 185
echo "usage: $0 [-aciwh] file_list"
230 186
echo "-a: perform all steps"
......
232 188
echo "-i: compile with inline mode"
233 189
echo "-w: compile with inline mode. Check the inlining with z3"
234 190
echo "-h: check files with the horn-pdf backend (requires z3)"
235
echo "-r: regression test for horn backend"
236 191
echo "-v <int>: verbose level"
237 192
}
238 193

  
......
246 201
                -c) nobehavior=0; c=1 ; shift ;;
247 202
                -i) nobehavior=0; i=1 ; shift ;;
248 203
                -w) nobehavior=0; w=1 ; shift ;;
249
                -r) nobehavior=0; r=1 ; shift ;;
250 204
                -h) nobehavior=0; h=1 ; shift ;;
251 205
                --) shift ;;
252 206
                -*) echo "bad option '$1'" ; exit 1 ;;
......
263 217
    exit 1
264 218
fi
265 219

  
220
# cleaning directory $build
221

  
222
rm -f "$build"/* 2> /dev/null
223

  
224
# executing tests
225

  
266 226
[ ! -z "$c" ] && base_compile
267 227
[ ! -z "$i" ] && inline_compile
268 228
[ ! -z "$w" ] && inline_compile_with_check
269 229
[ ! -z "$h" ] && check_prop
270
[ ! -z "$r" ] && check_horn
271 230
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
272 231

  
273 232

  
......
276 235
	#if [ $? -ne 1 ];then
277 236
	#  rm ../${file}i
278 237
	#fi
238

  

Also available in: Unified diff