diff --git a/continuous-benchmarking/README.md b/continuous-benchmarking/README.md new file mode 100644 index 0000000..a45080b --- /dev/null +++ b/continuous-benchmarking/README.md @@ -0,0 +1,14 @@ +# CBMC Continuous Benchmarking + +## Setting up a machine + +`./setup.sh` +`screen -S www` +`cd www; ./server.sh` +Ctrl+A+D + +Add commits to analyze to the list of commits in `run-cbmc.sh` respectively `run-jbmc.sh` + +`screen -S run` +`./run-cbmc.sh; ./run-jbmc.sh` +Ctrl+A+D diff --git a/continuous-benchmarking/rename.sh b/continuous-benchmarking/rename.sh new file mode 100755 index 0000000..4d70065 --- /dev/null +++ b/continuous-benchmarking/rename.sh @@ -0,0 +1,28 @@ +TIMESTAMP_FILE=$1 +TIMESTAMP_TEXT="$2" + +for f in *.zip +do + unzip $f > /dev/null + rm $f + D=`echo $f | rev | cut -c5- | rev` + #echo "old dir: $D" + NEWD="cbmc.${TIMESTAMP_FILE}.logfiles" + #echo "new dir: $NEWD" + mv $D $NEWD + zip -r ${NEWD}.zip $NEWD > /dev/null + rm -rf $NEWD +done +for f in *.bz2 +do + bunzip2 $f + F=`echo $f | rev | cut -c5- | rev` + SUFFIX=`echo $F | cut -c22-` + NEWF="cbmc.${TIMESTAMP_FILE}.${SUFFIX}" + #echo "new file: $NEWF" + mv $F $NEWF + sed -i.bak "s/[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\} [0-9]\{2\}:[0-9]\{2\}:[0-9]\{2\} UTC/${TIMESTAMP_TEXT}/g" $NEWF + bzip2 $NEWF + rm *.bak +done + diff --git a/continuous-benchmarking/run-cbmc.sh b/continuous-benchmarking/run-cbmc.sh new file mode 100755 index 0000000..cec4204 --- /dev/null +++ b/continuous-benchmarking/run-cbmc.sh @@ -0,0 +1,74 @@ +#!/bin/bash +set -e + +sudo chmod o+wt '/sys/fs/cgroup/cpuset/' +sudo chmod o+wt '/sys/fs/cgroup/cpu,cpuacct/user.slice' +sudo chmod o+wt '/sys/fs/cgroup/freezer/' +sudo chmod o+wt '/sys/fs/cgroup/memory/user.slice' + +LOG=~/www/public/log.txt +PROGRESS=~/www/public/log + +PUBLIC_DIR=~/www/public/svcomp19 + +REPO=https://github.com/diffblue/cbmc.git + +cd cprover-sv-comp >> $LOG 2>&1 +make cbmc-wrapper >> $LOG 2>&1 +cd ../benchexec >> $LOG 2>&1 +cp ../cprover-sv-comp/cbmc-wrapper cbmc >> $LOG 2>&1 +cp ../sv-comp/benchmark-defs/cbmc.xml . >> $LOG 2>&1 +echo "`date` Benchexec wrappers set up" | tee -a $PROGRESS $LOG +for v in 5594db641 e743f02fc eca9b599e +do +echo "`date` Updating CBMC" | tee -a $PROGRESS $LOG +rm -Rf ../cbmc >> $LOG 2>&1 +git clone $REPO ../cbmc >> $LOG 2>&1 +cd ../cbmc/src >> $LOG 2>&1 +git checkout $v >> $LOG 2>&1 +rm -f sha.txt +git log | head -n 1 | cut -c 8- > sha.txt +SHA=`cat sha.txt` +echo "`date` CBMC commit $SHA" | tee -a $PROGRESS $LOG +echo "`date` Compiling CBMC" | tee -a $PROGRESS $LOG +make clean >> $LOG 2>&1 +make minisat2-download >> $LOG 2>&1 +make -j4 >> $LOG 2>&1 +rm -f version.txt +cbmc/cbmc --version | cut -c-4 | tr -d '[:space:]' > version.txt +CDATE=`git show -s --format=%ci | cut -c-10` +TIMESTAMP_FILE="${CDATE}_0000" +TIMESTAMP_TEXT="${CDATE} 00:00:00 UTC" +echo "`date` CBMC version `cat version.txt`" | tee -a $PROGRESS $LOG +echo "`date` Preparing CBMC for benchexec" | tee -a $PROGRESS $LOG +cd ../../benchexec >> $LOG 2>&1 +cp ../cbmc/src/cbmc/cbmc cbmc-binary >> $LOG 2>&1 +cp ../cbmc/src/goto-cc/goto-cc goto-cc >> $LOG 2>&1 +VERSION=`cat ../cbmc/src/version.txt` +cp ../cprover-sv-comp/cbmc-wrapper cbmc >> $LOG 2>&1 +sed -i.bak "s/\$TOOL_BINARY --version/echo ${VERSION}-${SHA}/g" cbmc +for TASK in ReachSafety-Arrays ReachSafety-BitVectors ReachSafety-ControlFlow ReachSafety-Floats ReachSafety-Heap ReachSafety-Loops MemSafety-Arrays MemSafety-Heap MemSafety-LinkedLists +do +OUTPUT_DIR="results-$TASK" +echo "`date` Starting evaluation for $TASK $TIMESTAMP_TEXT" | tee -a $PROGRESS $LOG +rm -f results/* >> $LOG 2>&1 +bin/benchexec cbmc.xml --no-container -t $TASK >> $LOG 2>&1 +echo "`date` Evaluation finished, updating tables" | tee -a $PROGRESS $LOG +cd results +../../rename.sh "$TIMESTAMP_FILE" "$TIMESTAMP_TEXT" >> $LOG 2>&1 +cd .. +mkdir -p $OUTPUT_DIR >> $LOG 2>&1 +mv results/*.zip $OUTPUT_DIR/ >> $LOG 2>&1 +mv results/*.xml.bz2 $OUTPUT_DIR/ >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.html >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.csv >> $LOG 2>&1 +bin/table-generator $OUTPUT_DIR/*.xml.bz2 >> $LOG 2>&1 +pwd >> $LOG 2>&1 +ls $OUTPUT_DIR >> $LOG 2>&1 +mkdir -p $PUBLIC_DIR/benchexec/$OUTPUT_DIR >> $LOG 2>&1 +for f in `find $OUTPUT_DIR -name '*.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/index.html >> $LOG 2>&1; done +for f in `find $OUTPUT_DIR -name '*table.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/index.html >> $LOG 2>&1; done +for f in `find $OUTPUT_DIR -name '*diff.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/diff.html >> $LOG 2>&1; done +echo "`date` Done" | tee -a $PROGRESS $LOG +done +done diff --git a/continuous-benchmarking/run-jbmc.sh b/continuous-benchmarking/run-jbmc.sh new file mode 100755 index 0000000..9d2040d --- /dev/null +++ b/continuous-benchmarking/run-jbmc.sh @@ -0,0 +1,78 @@ +#!/bin/bash +set -e + +sudo chmod o+wt '/sys/fs/cgroup/cpuset/' +sudo chmod o+wt '/sys/fs/cgroup/cpu,cpuacct/user.slice' +sudo chmod o+wt '/sys/fs/cgroup/freezer/' +sudo chmod o+wt '/sys/fs/cgroup/memory/user.slice' + +LOG=~/www/public/log.txt +PROGRESS=~/www/public/log + +PUBLIC_DIR=~/www/public/svcomp19 + +REPO=https://github.com/diffblue/cbmc.git + +cd cprover-sv-comp >> $LOG 2>&1 +make cbmc-wrapper >> $LOG 2>&1 +cd ../benchexec >> $LOG 2>&1 +cp ../cprover-sv-comp/jbmc-wrapper jbmc >> $LOG 2>&1 +cp ../sv-comp/benchmark-defs/jbmc.xml . >> $LOG 2>&1 +for v in 34df81a09b57a62df58c76eb2f08c244735ba969 90d0de91b0918c9e5d5ed250cae62241ae38392a baaabc80e5ce72aaba4649869b2de1d2a04c2b25 f02417343fbb22ff258b5e9c96876a53f28b718e f5483b20162945273e62d68917dde72f08341710 +do +echo "`date` Updating CBMC" | tee -a $PROGRESS $LOG +rm -Rf ../cbmc >> $LOG 2>&1 +git clone $REPO ../cbmc >> $LOG 2>&1 +cd ../cbmc/src >> $LOG 2>&1 +git checkout $v >> $LOG 2>&1 +git submodule update --init --recursive +rm -f sha.txt +git log | head -n 1 | cut -c 8- > sha.txt +SHA=`cat sha.txt` +echo "`date` CBMC commit $SHA" | tee -a $PROGRESS $LOG +echo "`date` Compiling JBMC" | tee -a $PROGRESS $LOG +make clean >> $LOG 2>&1 +make minisat2-download >> $LOG 2>&1 +make -j4 >> $LOG 2>&1 +cd ../jbmc/src >> $LOG 2>&1 +make -j4 >> $LOG 2>&1 +rm -f version.txt +jbmc/jbmc --version | cut -c-4 | tr -d '[:space:]' > version.txt +CDATE=`git show -s --format=%ci | cut -c-10` +TIMESTAMP_FILE="${CDATE}_0000" +TIMESTAMP_TEXT="${CDATE} 00:00:00 UTC" +echo "`date` CBMC version `cat version.txt`" | tee -a $PROGRESS $LOG +echo "`date` Preparing CBMC for benchexec" | tee -a $PROGRESS $LOG +cd ../../../benchexec >> $LOG 2>&1 +cp ../cbmc/jbmc/src/jbmc/jbmc jbmc-binary >> $LOG 2>&1 +cp ../cbmc/jbmc/lib/java-models-library/target/core-models.jar core-models.jar >> $LOG 2>&1 +cp ../cbmc/src/goto-cc/goto-cc goto-cc >> $LOG 2>&1 +VERSION=`cat ../cbmc/jbmc/src/version.txt` +cp ../cprover-sv-comp/jbmc-wrapper jbmc >> $LOG 2>&1 +sed -i.bak "s/\$TOOL_BINARY --version/echo ${VERSION}-${SHA}/g" jbmc +for TASK in ReachSafety-Java +do +OUTPUT_DIR="results-$TASK" +echo "`date` Starting evaluation for $TASK $TIMESTAMP_TEXT" | tee -a $PROGRESS $LOG +rm -f results/* >> $LOG 2>&1 +bin/benchexec jbmc.xml --no-container -t $TASK >> $LOG 2>&1 +echo "`date` Evaluation finished, updating tables" | tee -a $PROGRESS $LOG +cd results +../../rename.sh "$TIMESTAMP_FILE" "$TIMESTAMP_TEXT" >> $LOG 2>&1 +cd .. +mkdir -p $OUTPUT_DIR >> $LOG 2>&1 +mv results/*.zip $OUTPUT_DIR/ >> $LOG 2>&1 +mv results/*.xml.bz2 $OUTPUT_DIR/ >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.html >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.csv >> $LOG 2>&1 +bin/table-generator $OUTPUT_DIR/*.xml.bz2 >> $LOG 2>&1 +pwd >> $LOG 2>&1 +ls $OUTPUT_DIR >> $LOG 2>&1 +mkdir -p $PUBLIC_DIR/benchexec/$OUTPUT_DIR >> $LOG 2>&1 +cp $OUTPUT_DIR/*.zip $PUBLIC_DIR/benchexec/$OUTPUT_DIR/ >> $LOG 2>&1 +for f in `find $OUTPUT_DIR -name '*.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/index.html >> $LOG 2>&1; done +for f in `find $OUTPUT_DIR -name '*table.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/index.html >> $LOG 2>&1; done +for f in `find $OUTPUT_DIR -name '*diff.html'`; do cp $f $PUBLIC_DIR/benchexec/$OUTPUT_DIR/diff.html >> $LOG 2>&1; done +echo "`date` Done" | tee -a $PROGRESS $LOG +done +done diff --git a/continuous-benchmarking/setup.sh b/continuous-benchmarking/setup.sh new file mode 100755 index 0000000..a58a98a --- /dev/null +++ b/continuous-benchmarking/setup.sh @@ -0,0 +1,6 @@ +#!/bin/bash +set -e + +git clone -b 1.17 https://github.com/sosy-lab/benchexec --depth=1 +git clone -b svcomp19 https://github.com/sosy-lab/sv-comp --depth=1 +git clone -b svcomp19 https://github.com/diffblue/cprover-sv-comp --depth=1 diff --git a/continuous-benchmarking/utils/bulkrename.sh b/continuous-benchmarking/utils/bulkrename.sh new file mode 100755 index 0000000..e6dfaf8 --- /dev/null +++ b/continuous-benchmarking/utils/bulkrename.sh @@ -0,0 +1,14 @@ +for d in results-* +do +cd $d +#../../rename2.sh cbmc.2018-01-31 2018-11-07_0000 "2018-11-07 00:00:00" 8640288 8640288-minisat-enhanced +../../rename2.sh cbmc.2018-11-06 2018-11-06_0001 "2018-11-06 00:00:00" 9494ebe92f6f98ddb7bdc9f32bcbb04adcf6e191 8640288-minisat-base +../../rename2.sh cbmc.2018-11-06 2018-11-06_0000 "2018-11-06 00:00:00" 9494ebe92f6f98ddb7bdc9f32bcbb04adcf6e191 8640288-minisat-base +cd .. +bin/table-generator $d/*.xml.bz2 +for f in $d/*table.html; do cp $f ~/www/public/benchexec/$d/index.html; done +for f in $d/*diff.html; do cp $f ~/www/public/benchexec/$d/diff.html; done +cp $d/*.zip ~/www/public/benchexec/$d/ +cp $d/*.xml.bz2 ~/www/public/benchexec/$d/ +rm $d/*.html $d/*.csv +done diff --git a/continuous-benchmarking/utils/rename2.sh b/continuous-benchmarking/utils/rename2.sh new file mode 100755 index 0000000..ff58cc4 --- /dev/null +++ b/continuous-benchmarking/utils/rename2.sh @@ -0,0 +1,29 @@ +PREFIX=$1 +TIMESTAMP_FILE=$2 +TIMESTAMP_TEXT="$3" + +for f in $PREFIX*.zip +do + unzip $f > /dev/null + rm $f + D=`echo $f | rev | cut -c5- | rev` + #echo "old dir: $D" + NEWD="cbmc.${TIMESTAMP_FILE}.logfiles" + #echo "new dir: $NEWD" + mv $D $NEWD + zip -r ${NEWD}.zip $NEWD > /dev/null + rm -rf $NEWD +done +for f in $PREFIX*.bz2 +do + bunzip2 $f + F=`echo $f | rev | cut -c5- | rev` + SUFFIX=`echo $F | cut -c22-` + NEWF="cbmc.${TIMESTAMP_FILE}.${SUFFIX}" + #echo "new file: $NEWF" + mv $F $NEWF + sed -i.bak "s/[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\} [0-9]\{2\}:[0-9]\{2\}:[0-9]\{2\} UTC/${TIMESTAMP_TEXT}/g" $NEWF + sed -i.bak "s/$4/$5/g" $NEWF + bzip2 $NEWF + rm *.bak +done diff --git a/continuous-benchmarking/utils/rename3.sh b/continuous-benchmarking/utils/rename3.sh new file mode 100755 index 0000000..f31c5b7 --- /dev/null +++ b/continuous-benchmarking/utils/rename3.sh @@ -0,0 +1,28 @@ +TIMESTAMP_FILE=$1 +TIMESTAMP_TEXT="$2" + +for f in *.zip +do + unzip $f > /dev/null + rm $f + D=`echo $f | rev | cut -c5- | rev` + #echo "old dir: $D" + NEWD="cbmc.${TIMESTAMP_FILE}.logfiles" + #echo "new dir: $NEWD" + mv $D $NEWD + zip -r ${NEWD}.zip $NEWD > /dev/null + rm -rf $NEWD +done +for f in *.bz2 +do + bunzip2 $f + F=`echo $f | rev | cut -c5- | rev` + SUFFIX=`echo $F | cut -c22-` + NEWF="cbmc.${TIMESTAMP_FILE}.${SUFFIX}" + #echo "new file: $NEWF" + mv $F $NEWF + sed -i.bak "s/[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\} [0-9]\{2\}:[0-9]\{2\}:[0-9]\{2\} UTC/${TIMESTAMP_TEXT}/g" $NEWF + sed -i.bak "s/$3/$4/g" $NEWF + bzip2 $NEWF + rm *.bak +done diff --git a/continuous-benchmarking/utils/run-binary.sh b/continuous-benchmarking/utils/run-binary.sh new file mode 100755 index 0000000..2d2bf6f --- /dev/null +++ b/continuous-benchmarking/utils/run-binary.sh @@ -0,0 +1,104 @@ +#!/bin/bash +set -e + +sudo chmod o+wt '/sys/fs/cgroup/cpuset/' +sudo chmod o+wt '/sys/fs/cgroup/cpu,cpuacct/user.slice' +sudo chmod o+wt '/sys/fs/cgroup/freezer/' +sudo chmod o+wt '/sys/fs/cgroup/memory/user.slice' + +LOG=~/www/public/log.txt +PROGRESS=~/www/public/log + +PUBLIC_DIR=~/www/public + +REPO=https://github.com/nmanthey/cbmc +#https://github.com/diffblue/cbmc.git + +#CBMC versions: +# cbmc-5.8 +# 2017/09 02ed3bf4337d4e40491c34f01fe8d081b4d3d8c6 +# 2017/10 897aaf640ef97d9e09b2073e02eac93a7a452ff7 +# 2017/11 b67d6e80fd66619e4bc0bf400de1e3c5beec30d8 +# cbmc-sv-comp-2018 +# 2017/12 b9372f1ae399b2636c60597510a4d08ff16d8038 +# 2018/01 2d67e42572f2d4d1966466edb8613245ea8d94b6 +# 2018/02 4a93a29a10f43dc27766c8d785b85e772127e254 +# 2018/03 4dd0f29734d7d5d1a08f426ccf88883cc375096c +# 2018/04 988b81841441afb8c3eb1d4cdfb72d7e501297ff +# 2018/05 e0bc5fd941d497ad6f55dcdac90fee8f841aa36f +# 2018/06 3f951dd60532c63b72eb878931dd2c3119d56b0f +# cbmc-5.9 +# 2018/07 ffbb83fdce4c4ba10b3ec916d91b9c9b32cc5be8 +# 2018/08 80331d8a57e526ab09d0c108617f831e69a4aba8 +# cbmc-5.10 +# 2018/09 d733fe34e1ce270738468d00e30bc16849f9a640 +# 2018/10 22e9fa80c3305944ff94f085361d8a1c4eeba074 +# 2018/11 25d5bff49bdba335bbc124b3c2a333338456edd1 +# manthey-minisat-base 9494ebe92f6f98ddb7bdc9f32bcbb04adcf6e191 +# manthey-minisat-enhanced 8640288 +# manthey-glucose-enhanced +# mantehy-glucose-fully-enhanced + +cd cprover-sv-comp >> $LOG 2>&1 +make cbmc-wrapper >> $LOG 2>&1 +cd ../benchexec >> $LOG 2>&1 +cp ../cprover-sv-comp/cbmc-wrapper cbmc >> $LOG 2>&1 +cp ../sv-comp/benchmark-defs/cbmc.xml . >> $LOG 2>&1 +#echo "`date` Benchexec wrappers set up" | tee -a $PROGRESS $LOG +for v in 8640288-glucose-fully-enhanced +#22e9fa80c3305944ff94f085361d8a1c4eeba074 25d5bff49bdba335bbc124b3c2a333338456edd1 +# 02ed3bf4337d4e40491c34f01fe8d081b4d3d8c6 897aaf640ef97d9e09b2073e02eac93a7a452ff7 b67d6e80fd66619e4bc0bf400de1e3c5beec30d8 b9372f1ae399b2636c60597510a4d08ff16d8038 2d67e42572f2d4d1966466edb8613245ea8d94b6 4a93a29a10f43dc27766c8d785b85e772127e254 4dd0f29734d7d5d1a08f426ccf88883cc375096c 988b81841441afb8c3eb1d4cdfb72d7e501297ff e0bc5fd941d497ad6f55dcdac90fee8f841aa36f 3f951dd60532c63b72eb878931dd2c3119d56b0f ffbb83fdce4c4ba10b3ec916d91b9c9b32cc5be8 80331d8a57e526ab09d0c108617f831e69a4aba8 22e9fa80c3305944ff94f085361d8a1c4eeba074 +do +#echo "`date` Updating CBMC" | tee -a $PROGRESS $LOG +#rm -Rf ../cbmc >> $LOG 2>&1 +#git clone $REPO ../cbmc >> $LOG 2>&1 +#cd ../cbmc/src >> $LOG 2>&1 +#git checkout $v >> $LOG 2>&1 +#rm -f sha.txt +#git log | head -n 1 | cut -c 8- > sha.txt +#SHA=`cat sha.txt` +SHA=$v +echo "`date` CBMC commit $SHA" | tee -a $PROGRESS $LOG +#echo "`date` Compiling CBMC" | tee -a $PROGRESS $LOG +#make clean >> $LOG 2>&1 +#make minisat2-download >> $LOG 2>&1 +#make -j4 >> $LOG 2>&1 +rm -f version.txt +#cbmc/cbmc --version | cut -c-4 | tr -d '[:space:]' > version.txt +./cbmc --version | cut -c-4 | tr -d '[:space:]' > version.txt +#CDATE=`git show -s --format=%ci | cut -c-10` +CDATE="2018-11-09" +TIMESTAMP_FILE="${CDATE}_0000" +TIMESTAMP_TEXT="${CDATE} 00:00:00 UTC" +echo "`date` CBMC version `cat version.txt`" | tee -a $PROGRESS $LOG +echo "`date` Preparing CBMC for benchexec" | tee -a $PROGRESS $LOG +#cd ../../benchexec >> $LOG 2>&1 +#cp ../cbmc/src/cbmc/cbmc cbmc-binary >> $LOG 2>&1 +VERSION=`cat ../cbmc/src/version.txt` +VERSION=`cat version.txt` +cp ../cprover-sv-comp/cbmc-wrapper cbmc >> $LOG 2>&1 +sed -i.bak "s/\$TOOL_BINARY --version/echo ${VERSION}-${SHA}/g" cbmc +for TASK in ReachSafety-Arrays ReachSafety-BitVectors ReachSafety-ControlFlow ReachSafety-Loops MemSafety-Arrays MemSafety-Heap MemSafety-LinkedLists ReachSafety-Floats ReachSafety-Heap +do +OUTPUT_DIR="results-$TASK" +echo "`date` Starting evaluation for $TASK $TIMESTAMP_TEXT" | tee -a $PROGRESS $LOG +rm -f results/* >> $LOG 2>&1 +bin/benchexec cbmc.xml --no-container -t $TASK >> $LOG 2>&1 +echo "`date` Evaluation finished, updating tables" | tee -a $PROGRESS $LOG +cd results +../../rename.sh "$TIMESTAMP_FILE" "$TIMESTAMP_TEXT" >> $LOG 2>&1 +cd .. +mv results/*.zip $OUTPUT_DIR/ >> $LOG 2>&1 +mv results/*.xml.bz2 $OUTPUT_DIR/ >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.html >> $LOG 2>&1 +rm -f $OUTPUT_DIR/*.csv >> $LOG 2>&1 +bin/table-generator $OUTPUT_DIR/*.xml.bz2 >> $LOG 2>&1 +pwd >> $LOG 2>&1 +ls $OUTPUT_DIR >> $LOG 2>&1 +cp $OUTPUT_DIR/*.zip $PUBLIC_DIR/benchexec/$OUTPUT_DIR/ >> $LOG 2>&1 +cp $OUTPUT_DIR/*.xml.bz2 $PUBLIC_DIR/benchexec/$OUTPUT_DIR/ >> $LOG 2>&1 +cp $OUTPUT_DIR/*table.html $PUBLIC_DIR/benchexec/$OUTPUT_DIR/index.html >> $LOG 2>&1 +cp $OUTPUT_DIR/*diff.html $PUBLIC_DIR/benchexec/$OUTPUT_DIR/diff.html >> $LOG 2>&1 +echo "`date` Done" | tee -a $PROGRESS $LOG +done +done diff --git a/continuous-benchmarking/www/server.js b/continuous-benchmarking/www/server.js new file mode 100644 index 0000000..481a411 --- /dev/null +++ b/continuous-benchmarking/www/server.js @@ -0,0 +1,75 @@ +'use strict'; + +const readline = require('readline'); +const fs = require('fs'); +const express = require('express'); +const app = express(); + +//app.use(express.static('public')); + +app.get('/', (req, res) => { + res.write(''); + res.write('CBMC Continuous Benchmarking'); + res.write(''); + res.write(''); + res.write('

CBMC Continuous Benchmarking

'); + res.write('

SV-COMP 2019 Benchmarks Results

'); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write('
ReachSafety-Arraystablediff
ReachSafety-BitVectorstablediff
ReachSafety-ControlFlowtablediff
ReachSafety-Floatstablediff
ReachSafety-Heaptablediff
ReachSafety-Loopstablediff
MemSafety-Arraystablediff
MemSafety-Heaptablediff
MemSafety-LinkedListstablediff
ReachSafety-Javatablediff
'); + + var analyses = ['n/a', 'n/a', 'n/a', 'n/a']; + var lineReader = readline.createInterface({ + input: fs.createReadStream('public/log') + }); + lineReader.on('line', function (line) { + if(line.includes('Starting evaluation')) { + analyses.push(line.substring(52)); + } + }).on('close', () => { + res.write('

Current Analysis

'); + res.write(analyses[analyses.length-1]+'
'); + res.write('

Recent Analyses

'); + res.write(analyses[analyses.length-2]+'
'); + res.write(analyses[analyses.length-3]+'
'); + res.write(analyses[analyses.length-4]+'
'); + res.write('

SV-COMP 2018 Benchmarks Results

'); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write(''); + res.write('
ReachSafety-Arraystablediff
ReachSafety-BitVectorstablediff
ReachSafety-ControlFlowtablediff
ReachSafety-Floatstablediff
ReachSafety-Heaptablediff
ReachSafety-Loopstablediff
MemSafety-Arraystablediff
MemSafety-Heaptablediff
MemSafety-LinkedListstablediff
'); + res.write(''); + res.write(''); + res.end(); + }); +}); + +app.use(express.static('public')); + +app.use(function(req, res, next) { + res.status(404).send("Sorry, that route doesn't exist."); +}); + +// Start the server +const PORT = process.env.PORT || 8080; +app.listen(PORT, () => { + console.log(`App listening on port ${PORT}`); + console.log('Press Ctrl+C to quit.'); +}); + diff --git a/continuous-benchmarking/www/server.sh b/continuous-benchmarking/www/server.sh new file mode 100755 index 0000000..f2f7019 --- /dev/null +++ b/continuous-benchmarking/www/server.sh @@ -0,0 +1,2 @@ +sudo iptables -t nat -I PREROUTING -p tcp --dport 80 -j REDIRECT --to-ports 8080 +nodejs server.js