Merge pull request #35 from peterschrammel/jbmc-wrapper-source-list

Accept multiple source files

Author: tautschnig

2ls.inc

@@ -2,14 +2,15 @@
 
 TOOL_BINARY=./2ls-binary
 TOOL_NAME=2LS
+FIND_OPTIONS=""
 
 # function to run the tool
 
 run()
 {
   gmon_suffix=$GMON_OUT_PREFIX
   export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
-  ./goto-cc -m$BIT_WIDTH --function $ENTRY $BM -o $LOG.bin
+  ./goto-cc -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
 
   export GMON_OUT_PREFIX="2ls_$gmon_suffix"
   # add property-specific options

cbmc.inc

@@ -2,6 +2,7 @@
 
 TOOL_BINARY=./cbmc-binary
 TOOL_NAME=CBMC
+FIND_OPTIONS=""
 
 # function to run the tool
 
@@ -13,7 +14,7 @@ run()
 
   gmon_suffix=$GMON_OUT_PREFIX
   export GMON_OUT_PREFIX="goto-cc_$gmon_suffix"
-  ./goto-cc -m$BIT_WIDTH --function $ENTRY $BM -o $LOG.bin
+  ./goto-cc -m$BIT_WIDTH --function $ENTRY "${BM[@]}" -o $LOG.bin
 
   export GMON_OUT_PREFIX="cbmc_$gmon_suffix"
 timeout 875 bash -c ' \

jbmc.inc

@@ -2,14 +2,16 @@
 
 TOOL_BINARY=./jbmc-binary
 TOOL_NAME=JBMC
+FIND_OPTIONS="-name '*.java'"
 
 # function to run the tool
 
 run()
 {
-  unzip $BM -d $BM_DIR
-  make -C $BM_DIR
-  BM=$BM_DIR/target/task.jar
+  mkdir -p $BM_DIR/classes
+  javac -g -cp $BM_DIR/classes -d $BM_DIR/classes "${BM[@]}"
+  jar -cfe $BM_DIR/task.jar Main -C $BM_DIR/classes .
+  export TASK="$BM_DIR/task.jar"
 
   MORE_OPTIONS="--throw-runtime-exceptions --max-nondet-string-length 100 --classpath core-models.jar"
 
@@ -24,11 +26,11 @@ 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 ; \
-./jbmc-binary $MORE_OPTIONS --graphml-witness $LOG.witness --unwind $c --stop-on-fail --$BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM >> $LOG.latest 2>&1 ; \
+./jbmc-binary $MORE_OPTIONS --graphml-witness $LOG.witness --unwind $c --stop-on-fail --$BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $TASK >> $LOG.latest 2>&1 ; \
 ec=$? ; \
 if [ $ec -eq 0 ] ; then \
 if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION SUCCESSFUL$" ; then ec=1 ; else \
-./jbmc-binary $MORE_OPTIONS --unwinding-assertions --unwind $c --stop-on-fail --$BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM > /dev/null 2>&1 || ec=42 ; \
+./jbmc-binary $MORE_OPTIONS --unwinding-assertions --unwind $c --stop-on-fail --$BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $TASK > /dev/null 2>&1 || ec=42 ; \
 fi ; \
 fi ; \
 if [ $ec -eq 10 ] ; then \

tool-wrapper.inc

@@ -72,15 +72,16 @@ process_graphml()
       <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=\"programfile\">$(echo ${BM[0]} | sed 's8/8\\/8g')<\/data>
+      <data key=\"programhash\">$(sha1sum ${BM[0]} | awk '{print $1}')<\/data>
       <data key=\"architecture\">${BIT_WIDTH}bit<\/data>\\Q/"
   fi
 }
 
 OBJ_BITS="11"
 BIT_WIDTH="64"
-BM=""
+declare -a BM
+BM=()
 PROP_FILE=""
 WITNESS_FILE=""
 
@@ -90,16 +91,16 @@ while [ -n "$1" ] ; do
     --propertyfile) PROP_FILE="$2" ; shift 2 ;;
     --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
     --version) $TOOL_BINARY --version ; exit 0 ;;
-    *) BM="$1" ; shift 1 ;;
+    *) SRC=(`eval "find $1 $FIND_OPTIONS"`) ; BM=("${BM[@]}" "${SRC[@]}") ; shift 1 ;;
   esac
 done
 
-if [ -z "$BM" ] || [ -z "$PROP_FILE" ] ; then
+if [ -z "${BM[0]}" ] || [ -z "$PROP_FILE" ] ; then
   echo "Missing benchmark or property file"
   exit 1
 fi
 
-if [ ! -s "$BM" ] || [ ! -s "$PROP_FILE" ] ; then
+if [ ! -s "${BM[0]}" ] || [ ! -s "$PROP_FILE" ] ; then
   echo "Empty benchmark or property file"
   exit 1
 fi
@@ -122,7 +123,7 @@ export BM
 export PROP
 export OBJ_BITS
 
-export GMON_OUT_PREFIX=`basename $BM`.gmon.out
+export GMON_OUT_PREFIX=`basename ${BM[0]}`.gmon.out
 
 export BM_DIR=`mktemp -d -t ${TOOL_NAME}-benchmark.XXXXXX`