From 795c8dfa2505f7c1a210d4534262b9f6eead7812 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 27 Aug 2018 12:17:55 +0100
Subject: [PATCH] Run script for Benchexec

Benchexec is the benchmarking framework used
by SV-COMP.
https://github.com/sosy-lab/benchexec

It can be run using the benchmark definition in
https://github.com/sosy-lab/sv-comp
and the benchmarks in
https://github.com/sosy-lab/sv-benchmarks
---
 bin/jpf-sv-comp | 76 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100755 bin/jpf-sv-comp

diff --git a/bin/jpf-sv-comp b/bin/jpf-sv-comp
new file mode 100755
index 0000000..7670dc0
--- /dev/null
+++ b/bin/jpf-sv-comp
@@ -0,0 +1,76 @@
+#!/bin/bash
+
+# This script allows JPF to run on Benchexec.
+# https://github.com/sosy-lab/benchexec
+
+# create site.properties
+SITE_PROPERTIES=site.properties
+echo "jpf-core = `pwd`/jpf-core" > $SITE_PROPERTIES
+echo "jpf-symbc = `pwd`/jpf-symbc" >> $SITE_PROPERTIES
+echo "extensions=\${jpf-core},\${jpf-symbc}" >> $SITE_PROPERTIES
+
+# parse arguments
+BENCHMARK=""
+PROPERTY_FILE=""
+WITNESS_FILE=""
+
+while [ -n "$1" ] ; do
+  case "$1" in
+    --propertyfile) PROPERTY_FILE="$2" ; shift 2 ;;
+    --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
+    --version) jpf-core/bin/jpf -version ; exit 0 ;;
+    *) BENCHMARK="$1" ; shift 1 ;;
+  esac
+done
+
+if [ -z "$BENCHMARK" ] ; then
+  echo "Missing benchmark file"
+  exit 1
+fi
+
+if [ -z "$PROPERTY_FILE" ] ; then
+  echo "Missing property file"
+  exit 1
+fi
+
+if [ ! -s "$BENCHMARK" ]  ; then
+  echo "Empty benchmark file"
+  exit 1
+fi
+
+if [ ! -s "$PROPERTY_FILE" ] ; then
+  echo "Empty property file"
+  exit 1
+fi
+
+LOG=`mktemp -t jpf-log.XXXXXX`
+DIR=`mktemp -d -t jpf-benchmark.XXXXXX`
+trap "rm -rf $DIR $LOG" EXIT
+
+# we ignore the property file (there is only one property at the moment)
+# we ignore the witness file (not used yet)
+# we unpack the benchmark zip file, build it and analyze it
+unzip $BENCHMARK -d $DIR
+make -C $DIR
+
+# create configuration file
+echo "target=Main" > $DIR/config.jpf
+echo "classpath=$DIR/target/classes" >> $DIR/config.jpf
+echo "symbolic.dp=z3" >> $DIR/config.jpf
+echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf
+
+LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH
+
+jpf-core/bin/jpf $DIR/config.jpf | tee $LOG
+
+grep "no errors detected" $LOG > /dev/null
+if [ $? -eq 0 ]; then
+  echo "SAFE"
+else
+  grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null
+  if [ $? -eq 0 ]; then
+    echo "UNSAFE"
+  else
+    echo "UNKNOWN"
+  fi
+fi
-- 
2.34.1