diffblue · tautschnig · Nov 30, 2016
diff --git a/utils/convert-to-regression-tests.sh 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 <<EOF
+CORE
+main.$suffix
+--function $ENTRY $PROPERTY --$bitwidth
+^EXIT=$expected_exitcode$
+^SIGNAL=0$
+^VERIFICATION $expected_result$
+^$expect_more$
+--
+^warning: ignoring
+EOF
+
+  if grep -q "^$category/$fn$" ../KNOWNBUG ; then
+    sed -i '1s/CORE/KNOWNBUG/' cprover-regr/$category/$fn/test.desc
+  fi
+}
+
+git clone --depth=1 https://github.com/sosy-lab/sv-benchmarks.git sv-benchmarks.git
+cd sv-benchmarks.git/c
+
+rm -rf cprover-regr
+
+for sub_category in *.set ; do
+  category=$sub_category
+  case $set in
+    ArraysMemSafety) category="Arrays" ;;
+    ArraysReach) category="Arrays" ;;
+    BitVectorsOverflows) category="BitVectors" ;;
+    BitVectorsReach) category="BitVectors" ;;
+    BusyBox) category="SoftwareSystems" ;;
+    ControlFlow) category="ControlFlowInteger" ;;
+    DeviceDriversLinux64) category="SoftwareSystems" ;;
+    ECA) category="ControlFlowInteger" ;;
+    HeapMemSafety) category="HeapManipulation" ;;
+    HeapReach) category="HeapManipulation" ;;
+    Loops) category="ControlFlowInteger" ;;
+    ProductLines) category="ControlFlowInteger" ;;
+    Recursive) category="ControlFlowInteger" ;;
+    Sequentialized) category="ControlFlowInteger" ;;
+    Simple) category="ControlFlowInteger" ;;
+    Termination-*) category="Termination" ;;
+  esac
+
+  for f in `cat $set.set` ; do
+    if [ ! -s "$f" ] ; then
+      warn "File $f not found"
+      continue
+    fi
+    convert $category $sub_category $f
+  done
+done
+
diff --git a/utils/run.sh b/utils/run.sh
@@ -0,0 +1,135 @@
+#!/bin/bash
+
+set -e
+
+export TMPDIR=$PWD
+ulimit -S -v 24000000
+
+# test.pl
+export PATH=$PWD/../cbmc/regression:$PATH
+export TOOL=$PWD/cbmc
+
+cd sv-benchmarks.git/c/cprover-regr/
+
+for category in * ; do
+  [ -d $category ] || continue
+
+  echo "Category: $category"
+
+  for d in * ; do
+    echo "Subset: $d"
+    cd $d
+
+    test.pl -j 8 -c "timeout 900 $TOOL"
+
+    #cd ..
+    #continue
+    cp -a /import/debian-mole/tools-from-svns/cpachecker/CPAchecker.svn/config/ .
+    for x in * ; do
+      if [ -s $x/main.cex ] ; then
+        sed -i "s/main.c/$x\/main.c/" $x/main.cex
+        if \
+        /import/debian-mole/tools-from-svns/cpachecker/CPAchecker.svn/scripts/cpa.sh -witness-validation \
+          -timelimit 90 \
+          -spec $x/main.cex \
+          -spec ../../../$d/ALL.prp \
+          $x/main.[ci] | \
+        grep "^Verification result: FALSE" ; then
+          echo "$x: Witness confirmed by CPAchecker"
+        else
+          echo "$x: Witness NOT confirmed by CPAchecker"
+        fi
+        continue
+
+        ## ec=0
+        ## if grep -q -- --32 $x/test.desc ; then
+        ##   timeout -k15 90 cbmc --32 --verify-cex $x/main.cex $x/main.[ci] > $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
+