Skip to content

Commit c1ea510

Browse files
author
Pascal Kesseli
committed
Updated CEGIS danger experiment script for FM camera-ready.
1 parent 8b2d7b4 commit c1ea510

File tree

2 files changed

+76
-127
lines changed

2 files changed

+76
-127
lines changed

‎regression/cegis/cegis_danger_benchmark_01_19/run-cbmc-danger-benchmark.sh

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,31 @@
11
#!/bin/bash
2-
#export PATH=${PATH//cbmc-5190/cbmc-trunk-synth}
3-
tool=/users/pkesseli/software/cpp/cbmc/cbmc-trunk-diffblue/regression/cbmc-wrapper.sh
4-
#benchmark_dir=${regression_dir}/cegis-cbmc
5-
result_file=$1.cbmc.log
6-
export out_file=$1.cbmc.out
2+
tool=$1
3+
export out_file=$2.cbmc.out
74
rm ${out_file} 2>/dev/null
85
timeout_time=300
96

10-
start_time=$(date +%s.%N)
11-
timeout --kill-after=10 ${timeout_time} bash ${tool} --no-unwinding-assertions $1
12-
end_time=$(date +%s.%N)
13-
duration=$(echo "${end_time} - ${start_time}" | bc)
14-
grep "VERIFICATION FAILED" ${out_file} >/dev/null
15-
error_found=$?
16-
grep "VERIFICATION SUCCESSFUL" ${out_file} >/dev/null
17-
no_bugs=$?
18-
if [ ${error_found} -eq 0 ]; then
19-
echo -e "${benchmark}\tFALSE\t${duration}" >>"${result_file}"
20-
elif [ ${no_bugs} -eq 0 ]; then
21-
echo -e "${benchmark}\tTRUE\t${duration}" >>"${result_file}"
22-
else
23-
echo -e "${benchmark}\tUNKNOWN\t${duration}" >>"${result_file}"
24-
fi
7+
start_time=$(($(date +%s%N)/1000000))
8+
timeout --kill-after=10 ${timeout_time} bash ${tool} --no-unwinding-assertions $2
9+
if [ $? -eq 124 ]; then
10+
timed_out=0
11+
else
12+
timed_out=1
13+
fi
14+
end_time=$(($(date +%s%N)/1000000))
15+
duration=$(echo "${end_time} - ${start_time}" | bc)
16+
grep "VERIFICATION FAILED" ${out_file} >/dev/null
17+
error_found=$?
18+
grep "VERIFICATION SUCCESSFUL" ${out_file} >/dev/null
19+
no_bugs=$?
20+
if [ ${timed_out} -eq 0 ]; then
21+
echo -e "${benchmark}\tTIMEOUT\t${duration}" >>"${out_file}"
22+
elif [ ${error_found} -eq 0 ]; then
23+
echo -e "${benchmark}\tVER-FALSE\t${duration}" >>"${out_file}"
24+
elif [ ${no_bugs} -eq 0 ]; then
25+
echo -e "${benchmark}\tVER-TRUE\t${duration}" >>"${out_file}"
26+
else
27+
echo -e "${benchmark}\tUNKNOWN\t${duration}" >>"${out_file}"
28+
fi
29+
30+
echo "<full_time> ${duration}</full_time>" >>"${out_file}"
31+
echo "</stats>" >>"${out_file}"

‎regression/cegis/cegis_danger_benchmark_01_19/run-danger.sh

Lines changed: 49 additions & 107 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,24 @@
11
#!/bin/bash
22
# Experiment script. Copy to "<cbmc_workspace>/regression/". Use as follows:
3-
# ./run-danger.sh [cegis|cegis-no-ranking] [cegis/cegis_danger_benchmark_<benchmark_id>]
3+
# ./run-danger.sh [cegis|cegis-no-ranking]
44

55
defaultArgs='--cegis-statistics --cegis-genetic main.c'
6-
cegisOut='main.cegis.out'
7-
cegisHeadStartOut='main.cegis-symex-head-start.out'
8-
cegisTournamentOut='main.cegis-tournament-select.out'
9-
cegisHeadStartTournamentOut='main.cegis-symex-head-start-tournament-select.out'
10-
config5Out='main.cegis-config5.out'
11-
config6Out='main.cegis-config6.out'
12-
config7Out='main.cegis-config7.out'
13-
config8Out='main.cegis-config8.out'
6+
config1Out='main.cegis-config1.out'
7+
config2Out='main.cegis-config2.out'
8+
config3Out='main.cegis-config3.out'
9+
config4Out='main.cegis-config4.out'
1410
successValue='</stats>'
1511
baseDir=`pwd`
1612

1713
trap '' SIGTERM
1814

15+
config_input=$1
16+
if [ -z "$1" ]; then config_input='cegis'; fi
17+
1918
for config in $1; do
2019
resultFile="${baseDir}/${config}.txt"
2120
truncate -s 0 "${resultFile}"
22-
for benchmark in ${baseDir}/$2; do
21+
for benchmark in ${baseDir}/cegis/cegis_danger_benchmark_*; do
2322
echo "${benchmark}"
2423
cd "${benchmark}"
2524
echo -n `basename ${benchmark}` >>"${resultFile}"
@@ -33,113 +32,56 @@ for config in $1; do
3332
benchmarkArgs="--danger ${benchmarkArgs}"
3433
fi
3534

36-
truncate -s 0 ${cegisOut}
37-
truncate -s 0 ${cegisHeadStartOut}
38-
truncate -s 0 ${cegisTournamentOut}
39-
truncate -s 0 ${cegisHeadStartTournamentOut}
40-
truncate -s 0 ${config5Out}
41-
truncate -s 0 ${config6Out}
42-
truncate -s 0 ${config7Out}
43-
truncate -s 0 ${config8Out}
35+
truncate -s 0 ${config1Out}
36+
truncate -s 0 ${config2Out}
37+
truncate -s 0 ${config3Out}
38+
truncate -s 0 ${config4Out}
4439

45-
../../run-cbmc-danger-benchmark.sh ${benchmark}/main.c &
46-
cbmcPid=$!
47-
cegis ${benchmarkArgs} >${cegisOut} 2>main.cegis.err &
48-
#../../sleep-echo.sh 10 1>${cegisOut} &
49-
cegisPid=$!
50-
cegis ${benchmarkArgs} --die --cegis-tournament-select >${cegisHeadStartOut} 2>main.cegis-symex-head-start.err &
51-
#../../sleep-echo.sh 100 1>${cegisHeadStartOut} &
52-
cegisSymexHeadStartPid=$!
53-
cegis ${benchmarkArgs} --cegis-symex-head-start 2 >${cegisTournamentOut} 2>main.cegis-tournament-select.err &
54-
#../../sleep-echo.sh 100 1>${cegisTournamentOut} & # unnecessary
55-
cegisTournamentPid=$!
56-
cegis ${benchmarkArgs} --cegis-symex-head-start 2 --cegis-tournament-select >${cegisHeadStartTournamentOut} 2>main.cegis-symex-head-start-tournament-select.err & # unnecessary
57-
#../../sleep-echo.sh 100 1>${cegisHeadStartTournamentOut} &
58-
cegisSymexHeadStartTournamentPid=$!
59-
cegis ${benchmarkArgs} --cegis-symex-head-start 3 --cegis-tournament-select --cegis-parallel-verify >${config5Out} 2>main.cegis-config5.err &
60-
#../../sleep-echo.sh 100 1>${cegisHeadStartTournamentOut} & # unnecessary
61-
config5Pid=$!
62-
cegis ${benchmarkArgs} --cegis-symex-head-start 1 >${config6Out} 2>main.cegis-config6.err &
63-
#../../sleep-echo.sh 100 1>${cegisHeadStartTournamentOut} & # unnecessary
64-
config6Pid=$!
65-
cegis ${benchmarkArgs} --cegis-symex-head-start 3 --cegis-parallel-verify >${config7Out} 2>main.cegis-config7.err &
66-
#../../sleep-echo.sh 100 1>${cegisHeadStartTournamentOut} & # unnecessary
67-
config7Pid=$!
68-
cegis ${benchmarkArgs} --cegis-symex-head-start 1 --cegis-tournament-select >${config8Out} 2>main.cegis-config8.err &
69-
#../../sleep-echo.sh 100 1>${cegisHeadStartTournamentOut} &
70-
config8Pid=$!
40+
cegis ${benchmarkArgs} --cegis-parallel-verify >${config1Out} 2>main.cegis.err &
41+
config1Pid=$!
42+
cegis ${benchmarkArgs} --cegis-symex-head-start 2 >${config2Out} 2>main.cegis.err &
43+
config2Pid=$!
44+
cegis ${benchmarkArgs} --cegis-tournament-select >${config3Out} 2>main.cegis.err &
45+
config3Pid=$!
46+
cegis ${benchmarkArgs} --cegis-tournament-select --cegis-symex-head-start 2 >${config4Out} 2>main.cegis.err &
47+
config4Pid=$!
7148

72-
cegisStopped=0
73-
#while [ ${cegisStopped} -eq 0 ] || [ ${cegisSymexHeadStartStopped} -eq 0 ] || [ ${cegisTournamentStopped} -eq 0 ]; do
74-
while [ ${cegisStopped} -eq 0 ] || [ ${cegisSymexHeadStartStopped} -eq 0 ] || [ ${cegisTournamentStopped} -eq 0 ] || [ ${cegisSymexHeadStartTournamentStopped} -eq 0 ] || [ ${config5Stopped} -eq 0 ] || [ ${config6Stopped} -eq 0 ] || [ ${config7Stopped} -eq 0 ] || [ ${config8Stopped} -eq 0 ] || [ ${cbmcStopped} -eq 0 ]; do
75-
kill -0 ${cegisPid} >/dev/null 2>&1; cegisStopped=$?
76-
grep --quiet "${successValue}" ${cegisOut}; cegisSuccess=$?
77-
kill -0 ${cegisSymexHeadStartPid} >/dev/null 2>&1; cegisSymexHeadStartStopped=$?
78-
grep --quiet "${successValue}" ${cegisHeadStartOut}; cegisSymexHeadStartSuccess=$?
79-
kill -0 ${cegisTournamentPid} >/dev/null 2>&1; cegisTournamentStopped=$?
80-
grep --quiet "${successValue}" ${cegisTournamentOut}; cegisTournamentSuccess=$?
81-
kill -0 ${cegisSymexHeadStartTournamentPid} >/dev/null 2>&1; cegisSymexHeadStartTournamentStopped=$?
82-
grep --quiet "${successValue}" ${cegisHeadStartTournamentOut}; cegisSymexHeadStartTournamentSuccess=$?
83-
kill -0 ${config5Pid} >/dev/null 2>&1; config5Stopped=$?
84-
grep --quiet "${successValue}" ${config5Out}; config5Success=$?
85-
kill -0 ${config6Pid} >/dev/null 2>&1; config6Stopped=$?
86-
grep --quiet "${successValue}" ${config6Out}; config6Success=$?
87-
kill -0 ${config7Pid} >/dev/null 2>&1; config7Stopped=$?
88-
grep --quiet "${successValue}" ${config7Out}; config7Success=$?
89-
kill -0 ${config8Pid} >/dev/null 2>&1; config8Stopped=$?
90-
grep --quiet "${successValue}" ${config8Out}; config8Success=$?
91-
kill -0 ${cbmcPid} >/dev/null 2>&1; cbmcStopped=$?
92-
grep --quiet "VERIFICATION" ${config8Out}; cbmcSuccess=$?
49+
config1Stopped=0
50+
while [ ${config1Stopped} -eq 0 ] || [ ${config2Stopped} -eq 0 ] || [ ${config3Stopped} -eq 0 ] || [ ${config4Stopped} -eq 0 ]; do
51+
kill -0 ${config1Pid} >/dev/null 2>&1; config1Stopped=$?
52+
grep --quiet "${successValue}" ${config1Out}; config1Success=$?
53+
kill -0 ${config2Pid} >/dev/null 2>&1; config2Stopped=$?
54+
grep --quiet "${successValue}" ${config2Out}; config2Success=$?
55+
kill -0 ${config3Pid} >/dev/null 2>&1; config3Stopped=$?
56+
grep --quiet "${successValue}" ${config3Out}; config3Success=$?
57+
kill -0 ${config4Pid} >/dev/null 2>&1; config4Stopped=$?
58+
grep --quiet "${successValue}" ${config4Out}; config4Success=$?
9359

94-
#if [ ${cegisSuccess} -eq 0 ] || [ ${cegisSymexHeadStartSuccess} -eq 0 ] || [ ${cegisTournamentSuccess} -eq 0 ]; then
95-
if [ ${cegisSuccess} -eq 0 ] || [ ${cegisSymexHeadStartSuccess} -eq 0 ] || [ ${cegisTournamentSuccess} -eq 0 ] || [ ${cegisSymexHeadStartTournamentSuccess} -eq 0 ] || [ ${config5Success} -eq 0 ] || [ ${config6Success} -eq 0 ] || [ ${config7Success} -eq 0 ] || [ ${config8Success} -eq 0 ] || [ ${cbmcSuccess} -eq 0 ]; then
96-
#while [ ${cegisStopped} -eq 0 ] || [ ${cegisSymexHeadStartStopped} -eq 0 ] || [ ${cegisTournamentStopped} -eq 0 ]; do
97-
while [ ${cegisStopped} -eq 0 ] || [ ${cegisSymexHeadStartStopped} -eq 0 ] || [ ${cegisTournamentStopped} -eq 0 ] || [ ${cegisSymexHeadStartTournamentStopped} -eq 0 ] || [ ${config5Stopped} -eq 0 ] || [ ${config6Stopped} -eq 0 ] || [ ${config7Stopped} -eq 0 ] || [ ${config8Stopped} -eq 0 ] || [ ${cbmcStopped} -eq 0 ]; do
60+
if [ ${config1Success} -eq 0 ] || [ ${config2Success} -eq 0 ] || [ ${config3Success} -eq 0 ] || [ ${config4Success} -eq 0 ]; then
61+
while [ ${config1Stopped} -eq 0 ] || [ ${config2Stopped} -eq 0 ] || [ ${config3Stopped} -eq 0 ] || [ ${config4Stopped} -eq 0 ]; do
9862
killall -9 cegis >/dev/null 2>&1
99-
killall -9 cbmc >/dev/null 2>&1
100-
killall timeout >/dev/null 2>&1
101-
kill -0 ${cegisPid} >/dev/null 2>&1; cegisStopped=$?
102-
kill -0 ${cegisSymexHeadStartPid} >/dev/null 2>&1; cegisSymexHeadStartStopped=$?
103-
kill -0 ${cegisTournamentPid} >/dev/null 2>&1; cegisTournamentStopped=$?
104-
kill -0 ${cegisSymexHeadStartTournamentPid} >/dev/null 2>&1; cegisSymexHeadStartTournamentStopped=$?
105-
kill -0 ${config5Pid} >/dev/null 2>&1; config5Stopped=$?
106-
kill -0 ${config6Pid} >/dev/null 2>&1; config6Stopped=$?
107-
kill -0 ${config7Pid} >/dev/null 2>&1; config7Stopped=$?
108-
kill -0 ${config8Pid} >/dev/null 2>&1; config8Stopped=$?
109-
kill -0 ${cbmcPid} >/dev/null 2>&1; cbmcStopped=$?
63+
kill -0 ${config1Pid} >/dev/null 2>&1; config1Stopped=$?
64+
kill -0 ${config2Pid} >/dev/null 2>&1; config2Stopped=$?
65+
kill -0 ${config3Pid} >/dev/null 2>&1; config3Stopped=$?
66+
kill -0 ${config4Pid} >/dev/null 2>&1; config4Stopped=$?
11067
sleep 10
11168
done
11269
fi
11370
sleep 10
11471
done
11572

116-
if [ ${cegisSuccess} -eq 0 ]; then
117-
echo -n ' base' >>"${resultFile}"
118-
outFile=${cegisOut}
119-
elif [ ${cegisSymexHeadStartSuccess} -eq 0 ]; then
120-
echo -n ' symex-head-start' >>"${resultFile}"
121-
outFile=${cegisHeadStartOut}
122-
elif [ ${cegisTournamentSuccess} -eq 0 ]; then
123-
echo -n ' tournament' >>"${resultFile}"
124-
outFile=${cegisTournamentOut}
125-
elif [ ${cegisSymexHeadStartTournamentSuccess} -eq 0 ]; then
126-
echo -n ' tournament-symex-head-start' >>"${resultFile}"
127-
outFile=${cegisHeadStartTournamentOut}
128-
elif [ ${config5Success} -eq 0 ]; then
129-
echo -n ' config5' >>"${resultFile}"
130-
outFile=${config5Out}
131-
elif [ ${config6Success} -eq 0 ]; then
132-
echo -n ' config6' >>"${resultFile}"
133-
outFile=${config6Out}
134-
elif [ ${config7Success} -eq 0 ]; then
135-
echo -n ' config7' >>"${resultFile}"
136-
outFile=${config7Out}
137-
elif [ ${config8Success} -eq 0 ]; then
138-
echo -n ' config8' >>"${resultFile}"
139-
outFile=${config8Out}
140-
elif [ ${cbmcSuccess} -eq 0 ]; then
141-
echo -n ' cbmc' >>"${resultFile}"
142-
outFile='none'
73+
if [ ${config1Success} -eq 0 ]; then
74+
echo -n ' config1' >>"${resultFile}"
75+
outFile=${config1Out}
76+
elif [ ${config2Success} -eq 0 ]; then
77+
echo -n ' config2' >>"${resultFile}"
78+
outFile=${config2Out}
79+
elif [ ${config3Success} -eq 0 ]; then
80+
echo -n ' config3' >>"${resultFile}"
81+
outFile=${config3Out}
82+
elif [ ${config4Success} -eq 0 ]; then
83+
echo -n ' config4' >>"${resultFile}"
84+
outFile=${config4Out}
14385
else
14486
echo -n ' none' >>"${resultFile}"
14587
outFile='none'

0 commit comments

Comments
 (0)