Project

General

Profile

Revision c3bbc76e test/test-compile.sh

View differences:

test/test-compile.sh
1 1
#!/bin/bash
2 2

  
3
eval set -- $(getopt -n $0 -o "-ciwh:" -- "$@")
4

  
5
declare c i w h
6
declare -a files
7

  
3 8
NOW=`date "+%y%m%d%H%M"`
9
report=`pwd`/report-$NOW
4 10
#LUSTREC="../../_build/src/lustrec"
5 11
LUSTREC=lustrec
6 12
mkdir -p build
7 13
build=`pwd`"/build"
8
while IFS=, read -r file main opts
9
do
10
  echo fichier:$file
11
#   echo main:$main
12
#   echo opts:$opts
13
    rm -f witness*
14
    name=`basename "$file" .lus`
15
    dir=`dirname "$file"`
16
    pushd $dir > /dev/null
14
    
15

  
16
base_compile() {
17
    while IFS=, read -r file main opts
18
    do
19
	name=`basename "$file" .lus`
20
	dir=`dirname "$file"`
21
	pushd $dir > /dev/null
17 22
    if [ "$main" != "" ]; then
18 23
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
19 24
        if [ $? -ne 0 ]; then
20
          rlustrec1="INVALID";
21
        else
22
          rlustrec1="VALID"
23
	fi
24
	pushd $build > /dev/null
25
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
26
	popd > /dev/null
27
        if [ $? -ne 0 ]; then
28
          rgcc1="INVALID";
29
        else
30
          rgcc1="VALID"
31
	fi	
32
	# Removing Generated lusi file
33
	#grep generated ../${file}i > /dev/null
34
	#if [ $? -ne 1 ];then
35
	#  rm ../${file}i
36
	#fi
37
	# Checking inlining
38
	$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
39
	if [ $? -ne 0 ]; then
40
          rlustrec2="INVALID";
25
            rlustrec1="INVALID";
41 26
        else
42
          rlustrec2="VALID"
27
            rlustrec1="VALID"
43 28
	fi
44 29
	pushd $build > /dev/null
45 30
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
46 31
	popd > /dev/null
47 32
        if [ $? -ne 0 ]; then
48
          rgcc2="INVALID";
33
            rgcc1="INVALID";
49 34
        else
50
          rgcc2="VALID"
35
            rgcc1="VALID"
51 36
	fi	
52
	# Cheching witness
53
	pushd $build > /dev/null
54
	lustreh -horn -node check witness.lus 2>/dev/null
55
	popd > /dev/null
56
    	z3="`z3 -t:10 witness.smt2 | xargs`"
57
    	if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
58
	  rinlining="VALID";
59
	elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
60
	  rinlining="ERROR";
61
	elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
62
	 rinlining="UNKNOWN";
63
	else
64
	 rinlining="INVALID"
65
	 exit 1
66
        fi  
67
	# Checking horn backend
68
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
69
	echo z3 "$name".smt2 | grep unsat
70
	# TODO: This part of the script has to be optimized
71
	z3 -t:10 "$name".smt2 | grep unsat > /dev/null
72
	if [ $? -ne 0 ]; then
73
         rhorn="INVALID";
74
        else
75
         rhorn="VALID"
76
        fi
77
	echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
78 37
    else
79 38
	$LUSTREC -d $build -verbose 0 $opts "$name".lus;
80 39
        if [ $? -ne 0 ]; then
81
          rlustrec1="INVALID";
40
            rlustrec1="INVALID";
82 41
        else
83
          rlustrec1="VALID"
42
            rlustrec1="VALID"
84 43
        fi
85 44
	pushd $build > /dev/null
86 45
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
87 46
	popd > /dev/null
88 47
        if [ $? -ne 0 ]; then
89
          rgcc1="INVALID";
48
            rgcc1="INVALID";
90 49
        else
91
          rgcc1="VALID"
50
            rgcc1="VALID"
92 51
        fi
93
	$LUSTREC -horn -d $build -verbose 0 $opts ../$file 
94
	echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
95 52
    fi
96 53
    popd > /dev/null
97
done < tests_ok.list
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
55
    done < $file_list
56
}
57

  
58
inline_compile () {
59
    while IFS=, read -r file main opts
60
    do
61
	name=`basename "$file" .lus`
62
	dir=`dirname "$file"`
63

  
64
	pushd $dir > /dev/null
65

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

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

  
126
}
127

  
128
check_prop () {
129
    while IFS=, read -r file main opts
130
    do
131
	name=`basename "$file" .lus`
132
	dir=`dirname "$file"`
133
	pushd $dir > /dev/null
134
	
135
    # Checking horn backend
136
    if [ "$main" != "" ]; then
137
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
138
    else
139
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
140
    fi
141
    # echo "z3 $build/$name".smt2 
142
    # TODO: This part of the script has to be optimized
143
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
144
    if [ $? -ne 0 ]; then
145
        rhorn="INVALID";
146
    else
147
        rhorn="VALID"
148
    fi
149
    echo "horn-pdr ($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
150
    popd > /dev/null
151
done < $file_list
152
}
153

  
154
usage () {
155
echo "usage: $0 [-aciwh] file_list"
156
echo "-a: perform all steps"
157
echo "-c: basic compilation"
158
echo "-i: compile with inline mode"
159
echo "-w: compile with inline mode. Check the inlining with z3"
160
echo "-h: check files with the horn-pdf backend (requires z3)"
161
}
162

  
163
nobehavior=1
164

  
165
while [ $# -gt 0 ] ; do
166
        case "$1" in
167
	        -v) shift ; verbose="$1"; shift ;;
168
	        -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
169
                -c) nobehavior=0; c=1 ; shift ;;
170
                -i) nobehavior=0; i=1 ; shift ;;
171
                -w) nobehavior=0; w=1 ; shift ;;
172
                -h) nobehavior=0; h=1 ; shift ;;
173
                --) shift ;;
174
                -*) echo "bad option '$1'" ; exit 1 ;;
175
                *) files=("${files[@]}" "$1") ; shift ;;
176
         esac
177
done
178

  
179
file_list=${files[0]}
180

  
181

  
182
if [ ${#files} -eq 0 ] ; then
183
    echo input list required
184
    usage
185
    exit 1
186
fi
187

  
188
[ ! -z "$c" ] && base_compile
189
[ ! -z "$i" ] && inline_compile
190
[ ! -z "$w" ] && inline_compile_with_check
191
[ ! -z "$h" ] && check_prop
192
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
193

  
194

  
195
	# Removing Generated lusi file
196
	#grep generated ../${file}i > /dev/null
197
	#if [ $? -ne 1 ];then
198
	#  rm ../${file}i
199
	#fi
200

  

Also available in: Unified diff