Skip to content

Commit 09b8cf7

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#2014 from tautschnig/cadical-experiment
Performance test extensions and updates
2 parents f50237b + a47941d commit 09b8cf7

File tree

5 files changed

+107
-162
lines changed

5 files changed

+107
-162
lines changed

‎scripts/perf-test/codebuild-glucose.yaml

Lines changed: 0 additions & 129 deletions
This file was deleted.

‎scripts/perf-test/codebuild.yaml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,8 @@ Resources:
6262
phases:
6363
install:
6464
commands:
65-
- apt-get update -y
66-
- apt-get install -y software-properties-common
67-
- add-apt-repository ppa:ubuntu-toolchain-r/test
65+
- echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
66+
- apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
6867
- apt-get update -y
6968
- apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk
7069
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
@@ -74,11 +73,12 @@ Resources:
7473
- echo ${Repository} > COMMIT_INFO
7574
- git rev-parse --short HEAD >> COMMIT_INFO
7675
- git log HEAD^..HEAD >> COMMIT_INFO
77-
- make -C src minisat2-download glucose-download
76+
- make -C src minisat2-download glucose-download cadical-download
7877
- make -C src -j8
7978
artifacts:
8079
files:
8180
- src/cbmc/cbmc
81+
- src/goto-cc/goto-cc
8282
- COMMIT_INFO
8383
discard-paths: yes
8484
Type: !Ref RepoType
@@ -104,9 +104,8 @@ Resources:
104104
phases:
105105
install:
106106
commands:
107-
- apt-get update -y
108-
- apt-get install -y software-properties-common
109-
- add-apt-repository ppa:ubuntu-toolchain-r/test
107+
- echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
108+
- apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
110109
- apt-get update -y
111110
- apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk
112111
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
@@ -116,11 +115,12 @@ Resources:
116115
- echo ${Repository} > COMMIT_INFO
117116
- git rev-parse --short HEAD >> COMMIT_INFO
118117
- git log HEAD^..HEAD >> COMMIT_INFO
119-
- make -C src minisat2-download glucose-download
118+
- make -C src minisat2-download glucose-download cadical-download
120119
- make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg"
121120
artifacts:
122121
files:
123122
- src/cbmc/cbmc
123+
- src/goto-cc/goto-cc
124124
- COMMIT_INFO
125125
discard-paths: yes
126126
Type: !Ref RepoType

‎scripts/perf-test/ebs.yaml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,8 @@ Resources:
3636
https://github.com/sosy-lab/cpachecker.git
3737
git clone --depth 1 \
3838
https://github.com/diffblue/cprover-sv-comp.git
39+
git clone --depth 1 \
40+
https://github.com/tautschnig/fshell-w2t.git
3941
halt
4042
4143
BaseVolume:

‎scripts/perf-test/ec2.yaml

Lines changed: 73 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@ Parameters:
3838
SSHKeyName:
3939
Type: String
4040

41+
WitnessCheck:
42+
Type: String
43+
4144
Conditions:
4245
UseSpot: !Not [!Equals [!Ref MaxPrice, ""]]
4346

@@ -153,6 +156,7 @@ Resources:
153156
apt-get install -y git time wget binutils awscli make jq
154157
apt-get install -y zip unzip
155158
apt-get install -y gcc libc6-dev-i386
159+
apt-get install -y ant python3-tempita python
156160

157161
# cgroup set up for benchexec
158162
chmod o+wt '/sys/fs/cgroup/cpuset/'
@@ -212,7 +216,7 @@ Resources:
212216
cd /mnt
213217
cd cprover-sv-comp
214218
git pull
215-
mkdir -p src/cbmc/
219+
mkdir -p src/cbmc src/goto-cc
216220
touch LICENSE
217221
cd ..
218222
mkdir -p run
@@ -223,6 +227,27 @@ Resources:
223227
mkdir -p tmp
224228
export TMPDIR=/mnt/tmp
225229

230+
if [ x${WitnessCheck} = xTrue ]
231+
then
232+
cd cpachecker
233+
ant
234+
235+
cd ../run
236+
for def in \
237+
cpa-seq-validate-correctness-witnesses \
238+
cpa-seq-validate-violation-witnesses \
239+
fshell-witness2test-validate-violation-witnesses
240+
do
241+
wget -O $def.xml https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/$def.xml
242+
sed -i 's#[\./]*/results-verified/LOGDIR/sv-comp18.\${!inputfile_name}.files/witness.graphml#witnesses/sv-comp18.${!inputfile_name}-witness.graphml#' $def.xml
243+
done
244+
245+
ln -s ../cpachecker/scripts/cpa.sh cpa.sh
246+
ln -s ../cpachecker/config/ config
247+
248+
cp ../fshell-w2t/* .
249+
fi
250+
226251
# reduce the likelihood of multiple hosts processing the
227252
# same message (in addition to SQS's message hiding)
228253
sleep $(expr $RANDOM % 30)
@@ -292,10 +317,12 @@ Resources:
292317
--receipt-handle $msg
293318

294319
cd /mnt/cprover-sv-comp
295-
rm -f src/cbmc/cbmc
320+
rm -f src/cbmc/cbmc src/goto-cc/goto-cc
296321
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \
297322
src/cbmc/cbmc
298-
chmod a+x src/cbmc/cbmc
323+
aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/goto-cc \
324+
src/goto-cc/goto-cc
325+
chmod a+x src/cbmc/cbmc src/goto-cc/goto-cc
299326
make CBMC=. cbmc.zip
300327
cd ../run
301328
unzip ../cprover-sv-comp/cbmc.zip
@@ -332,11 +359,26 @@ Resources:
332359
tar czf witnesses.tar.gz cbmc.*.logfiles
333360
rm -rf cbmc.*.logfiles
334361
cd ..
362+
363+
if [ x${WitnessCheck} = xTrue ]
364+
then
365+
for wc in *-witnesses.xml
366+
do
367+
wcp=$(echo $wc | sed 's/-witnesses.xml$//')
368+
mkdir witnesses
369+
tar -C witnesses --strip-components=1 -xzf \
370+
logs-$t/witnesses.tar.gz
371+
../benchexec/bin/benchexec --no-container \
372+
$wc --task $t -T 90s -M 15GB \
373+
-o $wcp-logs-$t/ -N $max_par -c 1
374+
rm -rf witnesses
375+
done
376+
fi
335377
fi
336-
if [ -f logs-$t/*.xml.bz2 ]
337-
then
338-
start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
339-
cd logs-$t
378+
start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
379+
for l in *logs-$t/*.xml.bz2
380+
do
381+
cd $(dirname $l)
340382
bunzip2 *.xml.bz2
341383
perl -p -i -e \
342384
"s/^(<result.*version=\"[^\"]*)/\$1:${PerfTestId}/" *.xml
@@ -346,22 +388,45 @@ Resources:
346388
"s/^(<result.*date=)\"[^\"]*/\$1\"$start_date/" *.xml
347389
bzip2 *.xml
348390
cd ..
391+
done
392+
393+
if [ x${WitnessCheck} = xTrue ]
394+
then
395+
../benchexec/bin/table-generator \
396+
logs-$t/*xml.bz2 *-logs-$t/*.xml.bz2 -o logs-$t/
397+
else
398+
../benchexec/bin/table-generator \
399+
logs-$t/*xml.bz2 -o logs-$t/
349400
fi
350401
aws s3 cp logs-$t \
351402
s3://${S3Bucket}/${PerfTestId}/$cfg/logs-$t/ \
352403
--recursive
404+
for wc in *-witnesses.xml
405+
do
406+
[ -s $wc ] || break
407+
wcp=$(echo $wc | sed 's/-witnesses.xml$//')
408+
rm -rf $wcp-logs-$t/*.logfiles
409+
aws s3 cp $wcp-logs-$t \
410+
s3://${S3Bucket}/${PerfTestId}/$cfg/$wcp-logs-$t/ \
411+
--recursive
412+
done
353413
else
354414
rm -f gmon.sum gmon.out *.gmon.out.*
355415
../benchexec/bin/benchexec cbmc.xml --no-container \
356416
--task $t -T 600s -M 7GB -o logs-$t/ \
357417
-N $max_par -c 1
358418
if ls *.gmon.out.* >/dev/null 2>&1
359419
then
360-
gprof --sum ./cbmc-binary *.gmon.out.*
420+
gprof --sum ./cbmc-binary cbmc*.gmon.out.*
361421
gprof ./cbmc-binary gmon.sum > sum.profile-$t
422+
rm -f gmon.sum
423+
gprof --sum ./goto-cc goto-cc*.gmon.out.*
424+
gprof ./goto-cc gmon.sum > sum.goto-cc-profile-$t
362425
rm -f gmon.sum gmon.out *.gmon.out.*
363426
aws s3 cp sum.profile-$t \
364427
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t
428+
aws s3 cp sum.goto-cc-profile-$t \
429+
s3://${S3Bucket}/${PerfTestId}/$cfg/sum.goto-cc-profile-$t
365430
fi
366431
fi
367432
rm -rf logs-$t sum.profile-$t

0 commit comments

Comments
 (0)