jpf-bmc/testBubble.sh at master · qsphan/jpf-bmc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
#!/bin/bash

TMPFILE=$(pwd)'/tmp.txt'
CLASSPATH=$(pwd)'/src/examples/classic'

# delete old results
if [ -f resultBubble.txt ]
  then
    rm  resultBubble.txt
fi

# replace $1 by $2 in file $3
replace()
{
	searchterm=$1
	replaceterm=$2
	sed -e "s/$searchterm/$replaceterm/ig" $3 > $TMPFILE
	mv $TMPFILE $3
}

runJPF()
{
	conf=$1
        step=$2
	# UNIX timestamp concatenated with nanoseconds
	T="$(date +%s%N)"
	jpf $conf
	T="$(($(date +%s%N)-T))"
        # Milliseconds
	M="$((T/1000000))"
	case $step in
	"1")
    		echo "SPF time in miliseconds: ${M}" >> resultBubble.txt
    		;;
	"2")
    		echo "JSBMC time in miliseconds: ${M}" >> resultBubble.txt
    		;;
	"3")
    		echo "JCBMC (D = 10) time in miliseconds: ${M}" >> resultBubble.txt
    		;;
	"4")
    		echo "JCBMC (D = 200) time in miliseconds: ${M}" >> resultBubble.txt
    		;;
	esac

}

# test a single .jpf file with SPF, JSBMC, JCBMC
testJPF()
{
	# This should be the .jpf file
	conf=$1

        echo $conf >> resultBubble.txt

	testSPF $conf

	replace 'symbolic.dp.*' 'symbolic.dp = no_solver' $conf
	replace 'search.multiple_errors.*' 'search.multiple_errors = true' $conf

	#Third step: test with JCBMC, bmc.batch=10
	replace '.*listener.*' 'listener = uk.ac.qmul.bmc.concur.BmcConcurListenerUsingSmtlib2' $conf
	replace 'bmc.batch.*' 'bmc.batch = 10' $conf
	runJPF $conf 3

	#Fourth step: test with JCBMC, bmc.batch=200
	replace 'bmc.batch.*' 'bmc.batch = 200' $conf
	runJPF $conf 4

	#Second step: test with JSBMC
	replace 'listener.*' 'listener = uk.ac.qmul.bmc.BmcListenerUsingSmtlib2' $conf
	runJPF $conf 2

	echo '' >> resultBubble.txt
}

testSPF()
{
	# This should be the .jpf file
	conf=$1

        #echo $conf >> resultBubble.txt

        # First step: test SPF with z3
        replace 'listener.*' '#listener' $conf
	replace 'symbolic.dp.*' 'symbolic.dp = z3' $conf
	replace 'search.multiple_errors.*' 'search.multiple_errors = false' $conf
	runJPF $conf 1
}

bubble=$CLASSPATH'/BubbleSort.java'
negated=$CLASSPATH'/BubbleSortAssertionNegated.java'

testAll()
{
	echo 'Test BubbleSort n = 5' >> resultBubble.txt
	replace 'static int N =.*;' 'static int N = 5;' $bubble
	./compile
	testJPF $CLASSPATH'/BubbleSort.jpf'
	echo '' >> resultBubble.txt

	echo 'Test BubbleSort n = 6' >> resultBubble.txt
	replace 'static int N =.*;' 'static int N = 6;' $bubble
	./compile
	testJPF $CLASSPATH'/BubbleSort.jpf'
	echo '' >> resultBubble.txt

	echo 'Test BubbleSortAssertionNegated n = 6' >> resultBubble.txt
	replace 'static int N =.*;' 'static int N = 6;' $negated
	./compile
	testJPF $CLASSPATH'/BubbleSortAssertionNegated.jpf'
	echo '' >> resultBubble.txt

	echo 'Test BubbleSortAssertionNegated n = 30' >> resultBubble.txt
	replace 'static int N =.*;' 'static int N = 30;' $negated
	./compile
	testJPF $CLASSPATH'/BubbleSortAssertionNegated.jpf'
	echo '' >> resultBubble.txt

	echo 'Test BubbleSortAssertionNegated n = 100' >> resultBubble.txt
	replace 'static int N =.*;' 'static int N = 100;' $negated
	./compile
	testJPF $CLASSPATH'/BubbleSortAssertionNegated.jpf'
	echo '' >> resultBubble.txt

}

testAll