Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ 8a5f633d

History | View | Annotate | Download (6.23 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=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
9
NOW=`date "+%y%m%d%H%M"`
10
report=`pwd`/report-$NOW
11
#LUSTREC="../../_build/src/lustrec"
12
LUSTREC=lustrec
13
mkdir -p build
14
build=`pwd`"/build"
15
    
16

    
17
base_compile() {
18
    while IFS=, read -r file main opts
19
    do
20
	name=`basename "$file" .lus`
21
	dir=${SRC_PREFIX}/`dirname "$file"`
22
	pushd $dir > /dev/null
23
    if [ "$main" != "" ]; then
24
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
25
        if [ $? -ne 0 ]; then
26
            rlustrec1="INVALID";
27
        else
28
            rlustrec1="VALID"
29
	fi
30
	pushd $build > /dev/null
31
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
32
	popd > /dev/null
33
        if [ $? -ne 0 ]; then
34
            rgcc1="INVALID";
35
        else
36
            rgcc1="VALID"
37
	fi	
38
    else
39
	$LUSTREC -d $build -verbose 0 $opts "$name".lus;
40
        if [ $? -ne 0 ]; then
41
            rlustrec1="INVALID";
42
        else
43
            rlustrec1="VALID"
44
        fi
45
	pushd $build > /dev/null
46
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
47
	popd > /dev/null
48
        if [ $? -ne 0 ]; then
49
            rgcc1="INVALID";
50
        else
51
            rgcc1="VALID"
52
        fi
53
    fi
54
    popd > /dev/null
55
    if [ $verbose -gt 0 ]; then
56
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
57
    else
58
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
59
    fi;
60
    done < $file_list
61
}
62

    
63
inline_compile () {
64
    while IFS=, read -r file main opts
65
    do
66
	name=`basename "$file" .lus`
67
	dir=${SRC_PREFIX}/`dirname "$file"`
68

    
69
	pushd $dir > /dev/null
70

    
71
# Checking inlining
72
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
73
    if [ $? -ne 0 ]; then
74
        rlustrec2="INVALID";
75
    else
76
        rlustrec2="VALID"
77
    fi
78
    pushd $build > /dev/null
79
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
80
    popd > /dev/null
81
    if [ $? -ne 0 ]; then
82
        rgcc2="INVALID";
83
    else
84
        rgcc2="VALID"
85
    fi	
86
    if [ $verbose -gt 0 ]; then
87
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
88
    else
89
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
90
    fi;
91
    popd > /dev/null
92
done < $file_list
93
}
94

    
95
inline_compile_with_check () {
96
# Checking inlining
97
    while IFS=, read -r file main opts
98
    do
99
	name=`basename "$file" .lus`
100
	dir=${SRC_PREFIX}/`dirname "$file"`
101
	pushd $dir > /dev/null
102
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
103
    if [ $? -ne 0 ]; then
104
        rlustrec2="INVALID";
105
    else
106
        rlustrec2="VALID"
107
    fi
108
    pushd $build > /dev/null
109
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
110
    popd > /dev/null
111
    if [ $? -ne 0 ]; then
112
        rgcc2="INVALID";
113
    else
114
        rgcc2="VALID"
115
    fi	
116
	# Cheching witness
117
    pushd $build > /dev/null
118
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
119
    popd > /dev/null
120
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
121
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
122
	rinlining="VALID";
123
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
124
	rinlining="ERROR";
125
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
126
	rinlining="UNKNOWN";
127
    else
128
	rinlining="INVALID"
129
	exit 1
130
    fi  
131
    if [ $verbose -gt 0 ]; then
132
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
133
    else
134
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
135
    fi
136
    popd > /dev/null
137
done < $file_list
138

    
139
}
140

    
141
check_prop () {
142
    while IFS=, read -r file main opts
143
    do
144
	name=`basename "$file" .lus`
145
	dir=${SRC_PREFIX}/`dirname "$file"`
146
	pushd $dir > /dev/null
147
	
148
    # Checking horn backend
149
    if [ "$main" != "" ]; then
150
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
151
    else
152
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
153
    fi
154
    # echo "z3 $build/$name".smt2 
155
    # TODO: This part of the script has to be optimized
156
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
157
    if [ $? -ne 0 ]; then
158
        rhorn="INVALID";
159
    else
160
        rhorn="VALID"
161
    fi
162
    if [ $verbose -gt 0 ]; then
163
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
164
    else
165
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
166
    fi
167
    popd > /dev/null
168
done < $file_list
169
}
170

    
171
usage () {
172
echo "usage: $0 [-aciwh] file_list"
173
echo "-a: perform all steps"
174
echo "-c: basic compilation"
175
echo "-i: compile with inline mode"
176
echo "-w: compile with inline mode. Check the inlining with z3"
177
echo "-h: check files with the horn-pdf backend (requires z3)"
178
echo "-v <int>: verbose level"
179
}
180

    
181
verbose=0
182
nobehavior=1
183

    
184
while [ $# -gt 0 ] ; do
185
        case "$1" in
186
	        -v) shift ; verbose="$1"; shift ;;
187
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
188
                -c) nobehavior=0; c=1 ; shift ;;
189
                -i) nobehavior=0; i=1 ; shift ;;
190
                -w) nobehavior=0; w=1 ; shift ;;
191
                -h) nobehavior=0; h=1 ; shift ;;
192
                --) shift ;;
193
                -*) echo "bad option '$1'" ; exit 1 ;;
194
                *) files=("${files[@]}" "$1") ; shift ;;
195
         esac
196
done
197

    
198
file_list=${files[0]}
199

    
200

    
201
if [ ${#files} -eq 0 ] ; then
202
    echo input list required
203
    usage
204
    exit 1
205
fi
206

    
207
[ ! -z "$c" ] && base_compile
208
[ ! -z "$i" ] && inline_compile
209
[ ! -z "$w" ] && inline_compile_with_check
210
[ ! -z "$h" ] && check_prop
211
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
212

    
213

    
214
	# Removing Generated lusi file
215
	#grep generated ../${file}i > /dev/null
216
	#if [ $? -ne 1 ];then
217
	#  rm ../${file}i
218
	#fi
219