Unified wrapper script for CPROVER tools

Run the Makefile to build the tool wrapper script from tool-wrapper.inc
and tool-specific includes which define tool and executable names
as well as a run function, currently provided for CBMC and 2LS.
tool-wrapper.inc contains a mapping from SV-COMP properties to the
CPROVER property instrumentation options.

Author: peterschrammel

2ls.inc

@@ -0,0 +1,23 @@
+# tool 
+
+TOOL_BINARY=./2ls-binary
+TOOL_NAME=2LS
+
+# function to run the tool
+
+run() 
+{
+  # add property-specific options
+  if [[ "$PROP" == "termination" ]]; then
+    PROPERTY="$PROPERTY --termination --competition-mode"
+  else
+    PROPERTY="$PROPERTY --k-induction --competition-mode"
+  fi
+
+  # run the tool
+  $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH $PROPERTY \
+    --function $ENTRY $BM >> $LOG.ok 2>&1
+
+  # store the exit code
+  EC=$?
+}

Makefile

@@ -1,7 +1,34 @@
 CBMC=../cbmc
+2LS=../2ls
+YEAR=2017
 
-all: 
+all: cbmc 2ls
+
+cbmc: CBMC-sv-comp-$(YEAR).tar.gz
+
+2ls: 2ls-sv-comp-$(YEAR).tar.gz
+
+.PHONY: cbmc 2ls
+
+%-wrapper: %.inc tool-wrapper.inc
+	echo "#!/bin/bash" > $@
+	cat $*.inc tool-wrapper.inc >> $@
+	chmod 755 $@
+
+CBMC-sv-comp-$(YEAR).tar.gz: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc
 	mkdir -p tmp
-	cp $(CBMC)/LICENSE cbmc tmp/
+	$(MAKE) cbmc-wrapper
+	mv cbmc-wrapper tmp/cbmc
+	cp $(CBMC)/LICENSE tmp/
 	cp $(CBMC)/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
+	cd tmp && tar cfz ../$@ * && rm cbmc cbmc-binary LICENSE
+	rmdir tmp
+
+2ls-sv-comp-$(YEAR).tar.gz: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/summarizer/2ls
+	mkdir -p tmp
+	$(MAKE) 2ls-wrapper
+	mv 2ls-wrapper tmp/2ls
+	cp $(2LS)/LICENSE tmp/
+	cp $(2LS)/src/summarizer/2ls tmp/2ls-binary
+	cd tmp && tar cfz ../$@ * && rm 2ls 2ls-binary LICENSE
+	rmdir tmp

README.md

@@ -4,17 +4,21 @@
 
 `make`
 
-#### Wrapper script
+#### Build wrapper script
 
-`cbmc`
+`make` tool`-wrapper`
+
+where tool is `cbmc` or `2ls`, for instance
 
 #### Benchexec tool script
 
-https://github.com/sosy-lab/benchexec/blob/master/benchexec/tools/cbmc.py
+* CBMC: https://github.com/sosy-lab/benchexec/blob/master/benchexec/tools/cbmc.py
+* 2LS: https://github.com/sosy-lab/benchexec/blob/master/benchexec/tools/two_ls.py
 
 #### Benchexec benchmark definition
 
-https://github.com/sosy-lab/sv-comp/blob/master/benchmark-defs/cbmc.xml
+* CBMC: https://github.com/sosy-lab/sv-comp/blob/master/benchmark-defs/cbmc.xml
+* 2LS: https://github.com/sosy-lab/sv-comp/blob/master/benchmark-defs/2ls.xml
 
 #### License
 

cbmc

@@ -0,0 +1,34 @@
+# tool 
+
+TOOL_BINARY=./cbmc-binary
+TOOL_NAME=CBMC
+
+# function to run the tool
+
+run() 
+{
+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-witness $LOG.witness --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 \
+'
+}

cbmc.inc

@@ -0,0 +1,129 @@
+
+# main tool wrapper script
+# run "make <tool>-wrapper" to generate the wrapper script
+
+# map properties to tool options
+
+declare -A OPTIONS
+OPTIONS["label"]="--error-label"
+OPTIONS["unreach_call"]=""
+OPTIONS["termination"]=""
+OPTIONS["overflow"]="--signed-overflow-check"
+OPTIONS["memsafety"]="--pointer-check --memory-leak-check --bounds-check"
+
+parse_property_file()
+{
+  local fn=$1
+
+  cat $fn | sed 's/[[:space:]]//g' | perl -n -e '                               
+if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {                               
+  print "ENTRY=$1\n";                                                           
+  print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/);        
+  print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(__VERIFIER_error\(\)\)$/);
+  print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/);      
+  print "PROP=\"overflow\"\n" if($2 =~ /^G!overflow$/);                         
+  print "PROP=\"termination\"\n" if($2 =~ /^Fend$/);                            
+}'
+}
+
+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)'
+  elif [[ "$PROP" == "termination" ]]; then
+    echo 'FALSE(termination)'
+  else
+    echo FALSE
+  fi
+}
+
+process_graphml()
+{
+  if [ -f $LOG.witness ]; then
+    if [ $1 -eq 0 ]; then
+      TYPE="correctness_witness"
+    else
+      TYPE="violation_witness"
+    fi
+    cat $LOG.witness | perl -p -e "s/(<graph edgedefault=\"directed\">)/\$1\\E  
+      <data key=\"witness-type\">$(echo $TYPE)<\/data>                          
+      <data key=\"producer\">$(echo $TOOL_NAME)<\/data>                         
+      <data key=\"specification\">$(<$PROP_FILE)<\/data>                        
+      <data key=\"programfile\">$(echo $BM | sed 's8/8\\/8g')<\/data>           
+      <data key=\"programhash\">$(sha1sum $BM | awk '{print $1}')<\/data>       
+      <data key=\"architecture\">${BIT_WIDTH##--}bit<\/data>\\Q/"
+  fi
+}
+
+BIT_WIDTH="--64"
+BM=""
+PROP_FILE=""
+WITNESS_FILE=""
+
+while [ -n "$1" ] ; do
+  case "$1" in
+    --32|--64) BIT_WIDTH="$1" ; shift 1 ;;
+    --propertyfile) PROP_FILE="$2" ; shift 2 ;;
+    --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
+    --version) $TOOL_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`
+
+if [[ "$PROP" == "" ]]; then
+  echo "Unrecognized property specification"
+  exit 1
+elif [[ "$PROP" == "label" ]]; then
+  PROPERTY="${OPTIONS[$PROP]} $LABEL"
+else
+  PROPERTY=${OPTIONS[$PROP]}
+fi
+
+export ENTRY
+export PROPERTY
+export BIT_WIDTH
+export BM
+export PROP
+
+export LOG=`mktemp -t ${TOOL_NAME}-log.XXXXXX`
+trap "rm -f $LOG $LOG.latest $LOG.ok $LOG.witness" EXIT
+
+run
+
+if [ ! -s $LOG.ok ] ; then
+  exit 1
+fi
+
+eval `tail -n 1 $LOG.ok`
+cat $LOG.ok
+case $EC in
+  0) if [[ "$WITNESS_FILE" != "" ]]; then process_graphml $EC > $WITNESS_FILE; \
+fi; echo "TRUE" ;;
+  10) if [[ "$WITNESS_FILE" != "" ]]; then process_graphml $EC > $WITNESS_FILE;\
+ fi; parse_result ;;
+  *) echo "UNKNOWN" ;;
+esac
+exit $EC