Project

General

Profile

« Previous | Next » 

Revision 3b2bd83d

Added by Teme Kahsai about 8 years ago

updating to onera version 30f766a:2016-12-04

View differences:

test/test-compile.sh
5 5
declare c i w h a v
6 6
declare -a files
7 7

  
8
#SRC_PREFIX="../.."
9
SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
8
SRC_PREFIX=/Users/Teme/Documents/GitHub/onera_lustrec-tests/
9
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10 10
NOW=`date "+%y%m%d%H%M"`
11
report=`pwd`/report-$NOW
12
#LUSTREC="../../_build/src/lustrec"
11
report=`pwd`/report-1.3-     459-$NOW
13 12
LUSTREC=lustrec
14 13
mkdir -p build
15 14
build=`pwd`"/build"
16 15

  
17 16
gcc_compile() {
17
    if [ $verbose -gt 1 ]; then
18
	echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
19
    fi
18 20
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
19 21
    if [ $? -ne 0 ]; then
20 22
	rgcc="INVALID";
......
24 26
}
25 27

  
26 28
lustrec_compile() {
29
    if [ $verbose -gt 1 ]; then
30
       echo "$LUSTREC $@"
31
    fi
27 32
    $LUSTREC "$@";
28 33
    if [ $? -ne 0 ]; then
29 34
        rlustrec="INVALID";
......
112 117
    while IFS=, read -r file main opts
113 118
    do
114 119
	name=`basename "$file" .lus`
115
	if [ "$name" = "$file" ]; then
116
	    return 0
120
	ext=".lus"
121
	if [ `dirname "$file"`/"$name" = "$file" ]; then
122
	    name=`basename "$file" .lusi`
123
	    ext=".lusi"
117 124
	fi
118 125
	dir=${SRC_PREFIX}/`dirname "$file"`
119 126
	pushd $dir > /dev/null
120
    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
121 127

  
122
    pushd $build > /dev/null
123
    gcc_compile "$name"
128
	if [ "$main" != "" ]; then
129
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
130
	else
131
	    if [ "$ext" = ".lusi" ]; then
132
		lustrec_compile -d $build -verbose 0 $opts $name$ext;
133
	    else
134
		rlustrec="NONE"
135
		rgcc="NONE"
136
	    fi
137
	fi
138
	popd > /dev/null
139
	pushd $build > /dev/null
124 140
	
125
    popd > /dev/null
141
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
142
	    gcc_compile "$name";
143
	else
144
	    rgcc="NONE"
145
	fi
126 146
	# Cheching witness
127
    pushd $build > /dev/null
128
    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
129
    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
	rinlining="INVALID/TIMEOUT"
139
    fi  
140
    if [ $verbose -gt 0 ]; then
141
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
142
    else
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"
144
    fi
145
    popd > /dev/null
147
       
148
	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
149
	    mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus
150
	    lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus
151
	    z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"
152
	    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
153
		rinlining="VALID";
154
	    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
155
		rinlining="ERROR";
156
	    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
157
		rinlining="UNKNOWN";
158
	    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
159
		rinlining="TIMEOUT"
160
	    else
161
		rinlining="INVALID"
162
	    fi
163
	else
164
	    rinlining="NONE"
165
	fi
166
	popd > /dev/null
167

  
168
	if [ $verbose -gt 0 ]; then
169
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
170
	else
171
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
172
	fi
146 173
done < $file_list
147 174

  
148 175
}
......
159 186
	
160 187
    # Checking horn backend
161 188
    if [ "$main" != "" ]; then
162
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
189
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
163 190
    else
164
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
191
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
165 192
    fi
166 193

  
167 194
    # echo "z3 $build/$name".smt2 
168 195
    # 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";
196
    z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"
197
    if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
198
	rhorn="VALID";
199
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
200
	rhorn="ERROR";
201
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
202
	rhorn="UNKNOWN";
203
    elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
204
	rhorn="TIMEOUT"
172 205
    else
173
        rhorn="VALID"
206
	rhorn="INVALID"
174 207
    fi
175 208
    if [ $verbose -gt 0 ]; then
176 209
	echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;

Also available in: Unified diff