From f70926fc27f350478806635309842396fa248937 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 28 Nov 2016 13:39:53 +0000 Subject: [PATCH 1/3] CBMC wrapper for SV-COMP --- sv-comp/cbmc | 116 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100755 sv-comp/cbmc diff --git a/sv-comp/cbmc b/sv-comp/cbmc new file mode 100755 index 00000000000..b8269853bf2 --- /dev/null +++ b/sv-comp/cbmc @@ -0,0 +1,116 @@ +#!/bin/bash + +parse_property_file() +{ + local fn=$1 + + cat $fn | sed 's/[[:space:]]//g' | perl -n -e ' +if(/^CHECK\(init\((\S+)\(\)\),LTL\(G(\S+)\)\)$/) { + print "ENTRY=$1\n"; + print "PROPERTY=\"--error-label $1\"\n" if($2 =~ /^!label\((\S+)\)$/); + print "PROPERTY=\" \"\n" if($2 =~ /^!call\(__VERIFIER_error\(\)\)$/); + print "PROPERTY=\"--pointer-check --memory-leak-check --bounds-check\"\n" if($2 =~ /^valid-(free|deref|memtrack)$/); + print "PROPERTY=\"--signed-overflow-check\"\n" if($2 =~ /^!overflow$/); +}' +} + +parse_result() +{ + if tail -n 50 $LOG.ok | grep -q "^[[:space:]]*__CPROVER_memory_leak == NULL$" ; then + echo 'FALSE(valid-memtrack)' + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*dereference failure:" ; then + echo 'FALSE(valid-deref)' + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*double free$" ; then + echo 'FALSE(valid-free)' + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*free argument has offset zero$" ; then + echo 'FALSE(valid-free)' + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*arithmetic overflow on signed" ; then + echo 'FALSE(no-overflow)' + else + echo FALSE + fi +} + +process_graphml() +{ + cat $LOG.cex | perl -p -e "s/()/\$1\\E + violation_witness<\/data> + CBMC<\/data> + $(<$PROP_FILE)<\/data> + $(echo $BM | sed 's8/8\\/8g')<\/data> + $(sha1sum $BM | awk '{print $1}')<\/data> + ${BIT_WIDTH##--}bit<\/data>\\Q/" +} + +BIT_WIDTH="--64" +BM="" +PROP_FILE="" +CEX_FILE="" + +while [ -n "$1" ] ; do + case "$1" in + --32|--64) BIT_WIDTH="$1" ; shift 1 ;; + --propertyfile) PROP_FILE="$2" ; shift 2 ;; + --graphml-cex) CEX_FILE="$2" ; shift 2 ;; + --version) ./cbmc-binary --version ; exit 0 ;; + *) BM="$1" ; shift 1 ;; + esac +done + +if [ -z "$BM" ] || [ -z "$PROP_FILE" ] ; then + echo "Missing benchmark or property file" + exit 1 +fi + +if [ ! -s "$BM" ] || [ ! -s "$PROP_FILE" ] ; then + echo "Empty benchmark or property file" + exit 1 +fi + +eval `parse_property_file $PROP_FILE` +export ENTRY +export PROPERTY +export BIT_WIDTH +export BM + +export LOG=`mktemp -t cbmc-log.XXXXXX` +trap "rm -f $LOG $LOG.latest $LOG.ok $LOG.cex" EXIT + +timeout 850 bash -c ' \ +\ +ulimit -v 15000000 ; \ +\ +EC=42 ; \ +for c in 2 6 12 17 21 40 200 400 1025 2049 268435456 ; do \ + echo "Unwind: $c" > $LOG.latest ; \ + ./cbmc-binary --graphml-cex $LOG.cex --unwind $c --stop-on-fail $BIT_WIDTH $PROPERTY --function $ENTRY $BM >> $LOG.latest 2>&1 ; \ + ec=$? ; \ + if [ $ec -eq 0 ] ; then \ + if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION SUCCESSFUL$" ; then ec=1 ; fi ; \ + fi ; \ + if [ $ec -eq 10 ] ; then \ + if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION FAILED$" ; then ec=1 ; fi ; \ + fi ; \ +\ + case $ec in \ + 0) EC=0 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ;; \ + 10) EC=10 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ; break ;; \ + *) if [ $EC -ne 0 ] ; then EC=$ec ; mv $LOG.latest $LOG.ok ; fi ; echo "EC=$EC" >> $LOG.ok ; break ;; \ + esac ; \ +\ +done \ +' + +if [ ! -s $LOG.ok ] ; then + exit 1 +fi + +eval `tail -n 1 $LOG.ok` +cat $LOG.ok +case $EC in + 0) echo "TRUE" ;; + 10) if [ "x$CEX_FILE" = x ] ; then process_graphml ; else process_graphml > $CEX_FILE ; fi ; parse_result ;; + *) echo "UNKNOWN" ;; +esac +exit $EC + From d967bc80c7b67dac0b024fa70043586439ec3a96 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 28 Nov 2016 13:49:29 +0000 Subject: [PATCH 2/3] README for SV-COMP scripts --- sv-comp/README.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 sv-comp/README.md diff --git a/sv-comp/README.md b/sv-comp/README.md new file mode 100644 index 00000000000..7a9de4a8b23 --- /dev/null +++ b/sv-comp/README.md @@ -0,0 +1,17 @@ +# SV-COMP Configuration and Wrappers + +#### Build package + +`make` + +#### Wrapper script + +`cbmc` + +#### Benchexec tool script + +https://github.com/sosy-lab/benchexec/blob/master/benchexec/tools/cbmc.py + +#### Benchexec benchmark configuration + +https://github.com/sosy-lab/sv-comp/blob/master/benchmark-defs/cbmc.xml \ No newline at end of file From 9b5005df902c4c03c05a8d1cda73321490bdb10c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 28 Nov 2016 13:55:39 +0000 Subject: [PATCH 3/3] Added a Makefile to build SV-COMP package --- sv-comp/Makefile | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 sv-comp/Makefile diff --git a/sv-comp/Makefile b/sv-comp/Makefile new file mode 100644 index 00000000000..662fc244796 --- /dev/null +++ b/sv-comp/Makefile @@ -0,0 +1,5 @@ +all: + mkdir -p tmp + cp ../LICENSE cbmc tmp/ + cp ../src/cbmc/cbmc tmp/cbmc-binary + cd tmp; tar cfz ../CBMC-sv-comp-2017.tar.gz *; rm cbmc cbmc-binary LICENSE; cd ..; rm -R tmp