From c6856fe7dc181629404f1736443ae3abf60bf3fa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Nov 2016 14:21:20 +0000 Subject: [PATCH] RFC: tools for running SV-COMP benchmarks This is not meant to be merged as-is (unless we set up some folder old/), but just to publish what scripting is being used. --- utils/convert-to-regression-tests.sh | 142 +++++++++++++++++++++++++++ utils/run.sh | 135 +++++++++++++++++++++++++ 2 files changed, 277 insertions(+) create mode 100755 utils/convert-to-regression-tests.sh create mode 100755 utils/run.sh diff --git a/utils/convert-to-regression-tests.sh b/utils/convert-to-regression-tests.sh new file mode 100755 index 0000000..4eccb33 --- /dev/null +++ b/utils/convert-to-regression-tests.sh @@ -0,0 +1,142 @@ +#!/bin/bash + +# Translate SV-COMP tasks into CProver regression tests + +set -e + +warn() +{ + echo "$1" >&2 +} + + +die() +{ + warn "$1" + exit 1 +} + +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$/); +}' +} + +convert() +{ + local category=$1 + local sub_category=$2 + local fn=$3 + + ENTRY="" + PROPERTY="" + eval `parse_property_file $sub_category.prp` + + if [ "x$ENTRY" = "x" ] ; then + die "Failed to parse entry function of $fn" + elif [ "x$PROPERTY" = "x" ] ; then + warn "Unhandled property in $fn" + return + fi + + if [ "x$category" = "xConcurrency" ] ; then + fn="`echo $fn | sed 's/i$/c/'`" + if [ ! -s $fn ] ; then + die "Non-preprocessed file $fn in Concurrency category not found" + fi + fi + + local suffix="`echo $fn | sed 's/.*\.//'`" + if [ "x$suffix" != "xc" ] && [ "x$suffix" != "xi" ] ; then + die "Failed to determine suffix of $fn" + fi + + local expected_result="" + local expected_exitcode="" + local expect_more="" + case $fn in + *_true-valid*) expected_result=SUCCESSFUL ; expect_more=TRUE ; expected_exitcode=0 ;; + *_true-unreach-call*) expected_result=SUCCESSFUL ; expect_more=TRUE ; expected_exitcode=0 ;; + *_true-no-overflow*) expected_result=SUCCESSFUL ; expect_more=TRUE ; expected_exitcode=0 ;; + *_true-termination*) expected_result=SUCCESSFUL ; expect_more=TRUE ; expected_exitcode=0 ;; + *_false-valid*) expected_result=FAILED ; expect_more=FALSE ; expected_exitcode=10 ;; + *_false-unreach-call*) expected_result=FAILED ; expect_more=FALSE ; expected_exitcode=10 ;; + *_false-no-overflow*) expected_result=FAILED ; expect_more=FALSE ; expected_exitcode=10 ;; + *_false-termination*) expected_result=FAILED ; expect_more=FALSE ; expected_exitcode=10 ;; + esac + if [ "x$expected_result" = "x" ] ; then + warn "Failed to determine expected result of $fn" + return + fi + case $fn in + *_false-valid-memtrack.*) expect_more="$expect_more(valid-memtrack)" ;; + *_false-valid-deref.*) expect_more="$expect_more(valid-deref)" ;; + *_false-valid-free.*) expect_more="$expect_more(valid-free)" ;; + *_false-no-overflow.*) expect_more="$expect_more(no-overflow)" ;; + esac + + local bitwidth=`grep ^Architecture $sub_category.cfg | awk '{print $2}'` + + mkdir -p cprover-regr/$category/$fn + cp $fn cprover-regr/$category/$fn/main.$suffix + + cat > cprover-regr/$category/$fn/test.desc < $x/verify.log || \ + ## ec=$? + ## else + ## timeout -k15 90 cbmc --verify-cex $x/main.cex $x/main.[ci] > $x/verify.log || \ + ## ec=$? + ## fi + ## if [ $ec -eq 10 ] ; then + ## echo "$x: Witness confirmed by CBMC" + ## else + ## echo "$x: Witness NOT confirmed by CBMC" + ## fi + fi + done + + cd .. + ## continue + + ## rm -f tests.log + ## echo "Experimental configurations" + + ## for d in * ; do + ## sed -i '3s/^/--graphml-cex main.cex /' $d/test.desc + ## done + + ## echo "CBMC with GraphML counter examples" + ## mv ../../../bin/cbmc ../../../bin/cbmc-trunk + ## mv ../../../bin/cbmc-graphml-cex ../../../bin/cbmc + ## test.pl -j 4 -c "timeout 900 inc.sh" + ## mv ../../../bin/cbmc ../../../bin/cbmc-graphml-cex + ## mv ../../../bin/cbmc-trunk ../../../bin/cbmc + + ## rm -f tests.log + + ## for d in * ; do + ## sed -i '3s/^--graphml-cex main.cex //' $d/test.desc + ## done + + ## echo "Building goto binaries" + ## for d in * ; do + ## if grep -q -- --32 $d/test.desc ; then + ## goto-cc -m32 $d/main.[ci] -o $d/main.gb + ## else + ## goto-cc $d/main.[ci] -o $d/main.gb + ## fi + ## done + + ## for d in * ; do + ## ec=0 + ## /usr/bin/time -v timeout -k15 900 goto-instrument-slicing --add-library --full-slice $d/main.gb $d/main.slice.gb || ec=$? + ## if [ $ec -eq 124 ] || [ $ec -eq 137 ] ; then + ## rm -f $d/main.slice.gb + ## echo "TIMEOUT" + ## elif [ $ec -eq 11 ] ; then + ## # Out of memory + ## rm -f $d/main.slice.gb + ## elif [ $ec -ne 0 ] ; then + ## exit 1 + ## fi + ## if [ -f $d/main.slice.gb ] ; then + ## goto-instrument-slicing --count-eloc $d/main.gb + ## goto-instrument-slicing --count-eloc $d/main.slice.gb + ## fi + + ## ec=0 + ## ##/usr/bin/time -v timeout -k15 900 goto-instrument --accelerate --z3 $d/main.gb $d/main.accel.gb || ec=$? + ## if [ $ec -eq 124 ] || [ $ec -eq 137 ] ; then + ## rm -f $d/main.accel.gb + ## echo "TIMEOUT" + ## elif [ $ec -eq 11 ] ; then + ## # Out of memory + ## rm -f $d/main.accel.gb + ## elif [ $ec -ne 0 ] ; then + ## exit 1 + ## fi + ## done + + ## for d in * ; do + ## if [ -f $d/main.slice.gb ] ; then + ## sed -i '2s/main.[ci]/main.slice.gb/' $d/test.desc + ## else + ## sed -i '1s/CORE/KNOWNBUG/' $d/test.desc + ## fi + ## done + + ## test.pl -j 4 -c "timeout 900 inc.sh" + + ## cd .. + done +done +