User Tools

Site Tools


sv-comp-utilities

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sv-comp-utilities [2015/01/14 10:52] (current)
mictau created
Line 1: Line 1:
 +The latest CBMC wrapper script:
  
 +<​code>​
 +#!/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
 +</​code>​
 +
 +Build regression tests from an SV-COMP check-out:
 +
 +<​code>​
 +#!/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
 +</​code>​
sv-comp-utilities.txt ยท Last modified: 2015/01/14 10:52 by mictau