Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ 4437ddbc

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