Merge pull request #56 from peterschrammel/dynamic-pre-analysis

Dynamic pre-analysis used in Java track of SV-COMP'20

Author: peterschrammel

jbmc.inc

@@ -3,29 +3,85 @@
 TOOL_BINARY=./jbmc-binary
 TOOL_NAME=JBMC
 FIND_OPTIONS="-name '*.java'"
+JVM_HOME=/usr/lib/jvm/java-8-openjdk-amd64
 
 # function to run the tool
 
 run()
 {
   mkdir -p $BM_DIR/classes
-  /usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp $BM_DIR/classes -d $BM_DIR/classes "${BM[@]}"
-  rm $BM_DIR/classes/org/sosy_lab/sv_benchmarks/Verifier.class
-  jar -cfe $BM_DIR/task.jar Main -C $BM_DIR/classes .
-  export TASK="$BM_DIR/task.jar"
+  mkdir -p $BM_DIR/src/org/sosy_lab/sv_benchmarks
+  HAS_NONDET=0
+  # We have to patch the Verifier interface.
+  # Should be upstreamed to sv-benchmarks to make witness checking easier.
+  # Make a copy of Verifier.java.
+  for f in "${!BM[@]}"; do
+    echo "${BM[$f]}" | grep Verifier.java > /dev/null
+    if [ $? -eq 0 ] ; then
+      VERIFIER_FILE="$BM_DIR/src/org/sosy_lab/sv_benchmarks/Verifier.java"
+      cp "${BM[$f]}" $VERIFIER_FILE
+      BM[$f]="$VERIFIER_FILE"
+    else
+      grep "Verifier.nondet" "${BM[$f]}" > /dev/null
+      if [ $? -eq 0 ] ; then
+        HAS_NONDET=1
+      fi
+    fi
+  done
+  # We have to distinguish assumption from assertion failures.
+  sed -i 's/Runtime.getRuntime().halt(1);/Runtime.getRuntime().halt(2);/g' $VERIFIER_FILE
+  # Let's determinize (uses same inputs for all benchmarks).
+  sed -i 's/new Random().nextInt()/11/g' $VERIFIER_FILE
+  sed -i 's/new Random().nextBoolean()/false/g' $VERIFIER_FILE
+  sed -i 's/new Random().nextLong()/11/g' $VERIFIER_FILE
+  sed -i 's/new Random().nextFloat()/11.0f/g' $VERIFIER_FILE
+  sed -i 's/new Random().nextDouble()/11.0/g' $VERIFIER_FILE
+  sed -i 's/int size = random.nextInt();/int size = 1;/g' $VERIFIER_FILE
+  sed -i 's/return new String(bytes);/return "JBMC at SV-COMP 2020";/g' $VERIFIER_FILE
+  # Compile
+  $JVM_HOME/bin/javac -g -cp $BM_DIR/classes -d $BM_DIR/classes "${BM[@]}"
+  # Check whether the file runs
+  timeout 10 $JVM_HOME/bin/java -ea -cp $BM_DIR/classes Main >> $LOG.latest 2>&1
+  ECR=$?
+  EC=42
+  # Filter out memouts and other errors
+  if [ $ECR -eq 1 ] ; then
+    grep -E "java\.lang\.StackOverflowError|java\.lang\.OutOfMemoryError|Error: Could not find or load main class|Error: Main method not found in class" $LOG.latest > /dev/null
+    if [ $? -eq 0 ] ; then
+      ECR=42
+    fi
+  fi
+  # Assertion failure found
+  if [ $ECR -eq 1 ] ; then
+    EC=10
+    mv $LOG.latest $LOG.ok
+    echo "EC=$EC" >> $LOG.ok
+  fi
+  # No assertion failure, but deterministic
+  if [ $ECR -eq 0 ] ; then
+    if [ $HAS_NONDET -eq 0 ] ; then
+      EC=0
+      mv $LOG.latest $LOG.ok
+      echo "EC=$EC" >> $LOG.ok
+    fi
+  fi
+  if [ $EC -eq 42 ]; then
+    rm $BM_DIR/classes/org/sosy_lab/sv_benchmarks/Verifier.class
+    jar -cfe $BM_DIR/task.jar Main -C $BM_DIR/classes .
+    export TASK="$BM_DIR/task.jar"
 
-  export MORE_OPTIONS="--java-threading --throw-runtime-exceptions --max-nondet-string-length 100 --classpath core-models.jar"
+    export MORE_OPTIONS="--java-threading --throw-runtime-exceptions --max-nondet-string-length 100 --classpath core-models.jar"
 
-  if [ "$PROP" = "termination" ] ; then
-    PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"
-  fi
+    if [ "$PROP" = "termination" ] ; then
+      PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"
+    fi
 
-timeout 875 bash -c ' \
+    timeout 875 bash -c ' \
 \
 ulimit -v 15000000 ; \
 \
 EC=42 ; \
-for c in 2 6 12 17 21 40 200 400 1025 2049 268435456 ; do \
+for c in 2 6 10 15 20 25 30 35 45 60 100 150 200 300 400 500 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 $TASK >> $LOG.latest 2>&1 ; \
 ec=$? ; \
@@ -47,8 +103,9 @@ esac ; \
 \
 done \
 '
-  if [ ! -s $LOG.ok ] ; then
-    mv $LOG.latest $LOG.ok ; echo "EC=42" >> $LOG.ok
+    if [ ! -s $LOG.ok ] ; then
+      mv $LOG.latest $LOG.ok ; echo "EC=42" >> $LOG.ok
+    fi
   fi
   eval `tail -n 1 $LOG.ok`
 }