User Tools

Site Tools


sv-comp-utilities

The latest CBMC wrapper script:

#!/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)$/);
}'
}

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)'
  else
    echo FALSE
  fi
}

BIT_WIDTH="--64"
BM=""
PROP_FILE=""

while [ -n "$1" ] ; do
  case "$1" in
    --32|--64) BIT_WIDTH="$1" ; shift 1 ;;
    --propertyfile) PROP_FILE="$2" ; shift 2 ;;
    *) 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" EXIT

timeout 850 bash -c ' \
\
ulimit -v 15000000 ; \
\
EC=42 ; \
for c in 2 6 12 17 21 40 ; do \
  echo "Unwind: $c" > $LOG.latest ; \
  ./cbmc --graphml-cex /dev/stdout --unwind $c --no-unwinding-assertions $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) parse_result ;;
  *) echo "UNKNOWN" ;;
esac
exit $EC

Build regression tests from an SV-COMP check-out:

#!/bin/bash

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)$/);
}'
}

parse_property()
{
  local fn=$1
  local dn=`dirname $fn`

  if [ -s $fn.prp ] ; then
    parse_property_file $fn.prp
  elif [ -s $dn/ALL.prp ] ; then
    parse_property_file $dn/ALL.prp
  fi
}

convert()
{
  local category=$1
  local fn=$2

  ENTRY=""
  ERROR_LABEL=""
  eval `parse_property $fn`

  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 ;;
    *_false-valid*) expected_result=FAILED ; expect_more=FALSE ; expected_exitcode=10 ;;
    *_false-unreach-call*) 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)" ;;
  esac

  local bitwidth=64
  case $category in
    Arrays) bitwidth=32 ;;
    BitVectors) bitwidth=32 ;;
    Concurrency) bitwidth=32 ;;
    ControlFlowInteger) bitwidth=32 ;;
    DeviceDrivers64) bitwidth=64 ;;
    HeapManipulation) bitwidth=32 ;;
    MemorySafety) bitwidth=32 ;;
    Recursive) bitwidth=32 ;;
    Sequentialized) bitwidth=32 ;;
    Simple) bitwidth=32 ;;
    Floats) bitwidth=32 ;;
    Termination) bitwidth=64 ;;
    DriverChallenges) bitwidth=64 ;;
    Stateful) bitwidth=64 ;;
  esac

  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

  if [ "x$category" = "xConcurrency" ] && [ "`basename $fn`" = "scull_true-unreach-call.c" ] ; then
    cp pthread-atomic/scull_true-unreach-call.h cprover-regr/$category/$fn/scull_safe.h
  fi
}

rm -rf cprover-regr

category=$set
if [ "x$category" = "xProductLines" ] ; then
  category="ControlFlowInteger"
elif [ "x$category" = "xLoops" ] ; then
  category="ControlFlowInteger"
elif [ "x$category" = "xECA" ] ; then
  category="ControlFlowInteger"
elif [ "x$category" = "xStateful" ] ; then
  exit 1
elif [ "x$category" = "xDriverChallenges" ] ; then
  exit 1
elif [ "x$category" = "xTermination-crafted" ] ; then
  exit 1
fi

for f in `cat $set.set` ; do
  if [ ! -s "$f" ] ; then
    warn "File $f not found"
    continue
  fi
  convert $category $f
done
sv-comp-utilities.txt · Last modified: 2015/01/14 10:52 by mictau