Merge pull request #28 from peterschrammel/jbmc

JBMC Tool wrapper

Author: peterschrammel

Makefile

@@ -1,14 +1,17 @@
 CBMC=../cbmc
 2LS=../2ls
+JBMC=../cbmc
 YEAR=2018
 
-all: cbmc 2ls
+all: cbmc 2ls jbmc
 
 cbmc: cbmc.zip
 
 2ls: 2ls.zip
 
-.PHONY: cbmc 2ls
+jbmc: jbmc.zip
+
+.PHONY: cbmc 2ls jbmc
 
 %-wrapper: %.inc tool-wrapper.inc
 	echo "#!/bin/bash" > $@
@@ -36,3 +39,14 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc
 	zip -r $@ $(basename $@)
 	cd $(basename $@) && rm 2ls 2ls-binary LICENSE
 	rmdir $(basename $@)
+
+jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/src/jbmc/jbmc
+	mkdir -p $(basename $@)
+	$(MAKE) jbmc-wrapper
+	mv jbmc-wrapper $(basename $@)/jbmc
+	cp $(JBMC)/LICENSE $(basename $@)/
+	cp $(JBMC)/src/jbmc/jbmc $(basename $@)/jbmc-binary
+	chmod a+rX $(basename $@)/*
+	zip -r $@ $(basename $@)
+	cd $(basename $@) && rm jbmc jbmc-binary LICENSE
+	rmdir $(basename $@)

jbmc.inc

@@ -0,0 +1,42 @@
+# tool
+
+TOOL_BINARY=./jbmc-binary
+TOOL_NAME=JBMC
+
+# function to run the tool
+
+run()
+{
+  if [ "$PROP" = "termination" ] ; then
+    PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"
+  fi
+
+timeout 875 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 ; \
+./jbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $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 ; else \
+./jbmc-binary --unwinding-assertions --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM > /dev/null 2>&1 || ec=42 ; \
+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 ; break ;; \
+10) EC=10 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ; break ;; \
+42) EC=42 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ;; \
+*) if [ $EC -ne 0 ] ; then EC=$ec ; mv $LOG.latest $LOG.ok ; fi ; echo "EC=$EC" >> $LOG.ok ; break ;; \
+esac ; \
+\
+done \
+'
+  eval `tail -n 1 $LOG.ok`
+}

tool-wrapper.inc

@@ -20,6 +20,7 @@ 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=\"unreach_call\"\n" if($2 =~ /^Gassert$/);
   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$/);