Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ 9603460e

History | View | Annotate | Download (6.78 KB)

1 22fe1c93 ploc
#!/bin/bash
2
3 1692756a ploc
eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
4 c3bbc76e ploc
5 1692756a ploc
declare c i w h a v
6 c3bbc76e ploc
declare -a files
7
8 8ea13d96 xthirioux
#SRC_PREFIX="../.."
9
SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10 22fe1c93 ploc
NOW=`date "+%y%m%d%H%M"`
11 c3bbc76e ploc
report=`pwd`/report-$NOW
12 71513f0e ploc
#LUSTREC="../../_build/src/lustrec"
13
LUSTREC=lustrec
14 22fe1c93 ploc
mkdir -p build
15 7291cb80 xthirioux
build=`pwd`"/build"
16 9603460e xthirioux
17 c3bbc76e ploc
18
base_compile() {
19
    while IFS=, read -r file main opts
20
    do
21
	name=`basename "$file" .lus`
22 9603460e xthirioux
        ext=".lus"
23
	if [ `dirname "$file"`/"$name" = "$file" ]; then
24
	    name=`basename "$file" .lusi`
25
	    ext=".lusi"
26
	fi
27
        dir=${SRC_PREFIX}/`dirname "$file"`
28 c3bbc76e ploc
	pushd $dir > /dev/null
29 22fe1c93 ploc
    if [ "$main" != "" ]; then
30 9603460e xthirioux
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
31 867595f2 ploc
        if [ $? -ne 0 ]; then
32 c3bbc76e ploc
            rlustrec1="INVALID";
33 867595f2 ploc
        else
34 c3bbc76e ploc
            rlustrec1="VALID"
35 867595f2 ploc
	fi
36 7291cb80 xthirioux
	pushd $build > /dev/null
37 9603460e xthirioux
	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
44
	else
45
	    rgcc1="NONE"
46
	fi
47 7291cb80 xthirioux
	popd > /dev/null
48 22fe1c93 ploc
    else
49 9603460e xthirioux
	$LUSTREC -d $build -verbose 0 $opts "$name""$ext";
50 c6f61bd7 ploc
        if [ $? -ne 0 ]; then
51 c3bbc76e ploc
            rlustrec1="INVALID";
52 c6f61bd7 ploc
        else
53 c3bbc76e ploc
            rlustrec1="VALID"
54 c6f61bd7 ploc
        fi
55 7291cb80 xthirioux
	pushd $build > /dev/null
56 9603460e xthirioux
	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
63
	else
64
	    rgcc1="NONE"
65
	fi
66 7291cb80 xthirioux
	popd > /dev/null
67 22fe1c93 ploc
    fi
68 7291cb80 xthirioux
    popd > /dev/null
69 1692756a ploc
    if [ $verbose -gt 0 ]; then
70 9603460e xthirioux
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
71 1692756a ploc
    else
72 9603460e xthirioux
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
73 1692756a ploc
    fi;
74 c3bbc76e ploc
    done < $file_list
75
}
76
77
inline_compile () {
78
    while IFS=, read -r file main opts
79
    do
80
	name=`basename "$file" .lus`
81 9603460e xthirioux
	if [ `dirname "$file"`/"$name" = "$file" ]; then
82
	    return 0
83
	fi
84 1692756a ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
85 c3bbc76e ploc
86
	pushd $dir > /dev/null
87
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 9603460e xthirioux
    fi
102
    popd > /dev/null
103 1692756a ploc
    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 c3bbc76e ploc
    popd > /dev/null
109
done < $file_list
110
}
111
112
inline_compile_with_check () {
113
# Checking inlining
114
    while IFS=, read -r file main opts
115
    do
116
	name=`basename "$file" .lus`
117 9603460e xthirioux
	if [ "$name" = "$file" ]; then
118
	    return 0
119
	fi
120 1692756a ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
121 c3bbc76e ploc
	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
128
    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	
135 9603460e xthirioux
    popd > /dev/null
136 c3bbc76e ploc
	# Cheching witness
137
    pushd $build > /dev/null
138 f01a1af8 ploc
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
139 c3bbc76e ploc
    popd > /dev/null
140
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
142
	rinlining="VALID";
143
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
144
	rinlining="ERROR";
145
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
146
	rinlining="UNKNOWN";
147
    else
148 f01a1af8 ploc
	rinlining="INVALID/TIMEOUT"
149 c3bbc76e ploc
    fi  
150 1692756a ploc
    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;
152
    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"
154
    fi
155 c3bbc76e ploc
    popd > /dev/null
156
done < $file_list
157
158
}
159
160
check_prop () {
161
    while IFS=, read -r file main opts
162
    do
163
	name=`basename "$file" .lus`
164 9603460e xthirioux
	if [ "$name" = "$file" ]; then
165
	    return 0
166
	fi
167 1692756a ploc
	dir=${SRC_PREFIX}/`dirname "$file"`
168 c3bbc76e ploc
	pushd $dir > /dev/null
169
	
170
    # Checking horn backend
171
    if [ "$main" != "" ]; then
172
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
173
    else
174
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
175
    fi
176 af5af1e8 ploc
    if [ $? -ne 0 ]; then
177
        rlustrec="INVALID";
178
    else
179
        rlustrec="VALID"
180
    fi
181 c3bbc76e ploc
    # echo "z3 $build/$name".smt2 
182
    # TODO: This part of the script has to be optimized
183
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
184
    if [ $? -ne 0 ]; then
185
        rhorn="INVALID";
186
    else
187
        rhorn="VALID"
188
    fi
189 1692756a ploc
    if [ $verbose -gt 0 ]; then
190 af5af1e8 ploc
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
191 1692756a ploc
    else
192 af5af1e8 ploc
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
193 1692756a ploc
    fi
194 c3bbc76e ploc
    popd > /dev/null
195
done < $file_list
196
}
197
198
usage () {
199
echo "usage: $0 [-aciwh] file_list"
200
echo "-a: perform all steps"
201
echo "-c: basic compilation"
202
echo "-i: compile with inline mode"
203
echo "-w: compile with inline mode. Check the inlining with z3"
204
echo "-h: check files with the horn-pdf backend (requires z3)"
205 1692756a ploc
echo "-v <int>: verbose level"
206 c3bbc76e ploc
}
207
208 1692756a ploc
verbose=0
209 c3bbc76e ploc
nobehavior=1
210
211
while [ $# -gt 0 ] ; do
212
        case "$1" in
213
	        -v) shift ; verbose="$1"; shift ;;
214
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
215
                -c) nobehavior=0; c=1 ; shift ;;
216
                -i) nobehavior=0; i=1 ; shift ;;
217
                -w) nobehavior=0; w=1 ; shift ;;
218
                -h) nobehavior=0; h=1 ; shift ;;
219
                --) shift ;;
220
                -*) echo "bad option '$1'" ; exit 1 ;;
221
                *) files=("${files[@]}" "$1") ; shift ;;
222
         esac
223
done
224
225
file_list=${files[0]}
226
227
228
if [ ${#files} -eq 0 ] ; then
229
    echo input list required
230
    usage
231
    exit 1
232
fi
233
234
[ ! -z "$c" ] && base_compile
235
[ ! -z "$i" ] && inline_compile
236
[ ! -z "$w" ] && inline_compile_with_check
237
[ ! -z "$h" ] && check_prop
238
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
239
240
241
	# Removing Generated lusi file
242
	#grep generated ../${file}i > /dev/null
243
	#if [ $? -ne 1 ];then
244
	#  rm ../${file}i
245
	#fi