diff --git a/2ls.inc b/2ls.inc index d08b906..255ecef 100644 --- a/2ls.inc +++ b/2ls.inc @@ -7,17 +7,22 @@ TOOL_NAME=2LS 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 + + export GMON_OUT_PREFIX="2ls_$gmon_suffix" # add property-specific options if [[ "$PROP" == "termination" ]]; then PROPERTY1="$PROPERTY --termination --competition-mode" PROPERTY2="$PROPERTY --nontermination --competition-mode" # run the termination and nontermination analysis in parallel - $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY1 \ - --function $ENTRY $BM >> $LOG.ok1 2>&1 & + $TOOL_BINARY --graphml-witness $LOG.witness --object-bits $OBJ_BITS $PROPERTY1 \ + $LOG.bin >> $LOG.ok1 2>&1 & PID1="$!" - $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY2 \ - --function $ENTRY $BM >> $LOG.ok2 2>&1 & + $TOOL_BINARY --graphml-witness $LOG.witness --object-bits $OBJ_BITS $PROPERTY2 \ + $LOG.bin >> $LOG.ok2 2>&1 & PID2="$!" # this might not work in all environments wait -n &> /dev/null @@ -57,8 +62,8 @@ run() PROPERTY="$PROPERTY --heap-interval --k-induction --competition-mode" # run the tool - $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY \ - --function $ENTRY $BM >> $LOG.ok 2>&1 + $TOOL_BINARY --graphml-witness $LOG.witness --object-bits $OBJ_BITS $PROPERTY \ + $LOG.bin >> $LOG.ok 2>&1 # store the exit code EC=$? diff --git a/Makefile b/Makefile index 8eafc2d..21de904 100644 --- a/Makefile +++ b/Makefile @@ -18,26 +18,28 @@ jbmc: jbmc.zip cat $*.inc tool-wrapper.inc >> $@ chmod 755 $@ -cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc +cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc mkdir -p $(basename $@) $(MAKE) cbmc-wrapper mv cbmc-wrapper $(basename $@)/cbmc cp $(CBMC)/LICENSE $(basename $@)/ cp $(CBMC)/src/cbmc/cbmc $(basename $@)/cbmc-binary + cp $(CBMC)/src/goto-cc/goto-cc $(basename $@)/ chmod a+rX $(basename $@)/* zip -r $@ $(basename $@) - cd $(basename $@) && rm cbmc cbmc-binary LICENSE + cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE rmdir $(basename $@) -2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls +2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/src/goto-cc/goto-cc mkdir -p $(basename $@) $(MAKE) 2ls-wrapper mv 2ls-wrapper $(basename $@)/2ls cp $(2LS)/LICENSE $(basename $@)/ cp $(2LS)/src/2ls/2ls $(basename $@)/2ls-binary + cp $(2LS)/src/goto-cc/goto-cc $(basename $@)/ chmod a+rX $(basename $@)/* zip -r $@ $(basename $@) - cd $(basename $@) && rm 2ls 2ls-binary LICENSE + cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE rmdir $(basename $@) jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/src/jbmc/jbmc diff --git a/cbmc.inc b/cbmc.inc index ad2a089..cda5987 100644 --- a/cbmc.inc +++ b/cbmc.inc @@ -11,6 +11,11 @@ run() PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions" fi + gmon_suffix=$GMON_OUT_PREFIX + export GMON_OUT_PREFIX="goto-cc_$gmon_suffix" + ./goto-cc -m$BIT_WIDTH --function $ENTRY $BM -o $LOG.bin + + export GMON_OUT_PREFIX="cbmc_$gmon_suffix" timeout 875 bash -c ' \ \ ulimit -v 15000000 ; \ @@ -18,11 +23,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 ; \ -./cbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM >> $LOG.latest 2>&1 ; \ +./cbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail --object-bits $OBJ_BITS $PROPERTY $LOG.bin >> $LOG.latest 2>&1 ; \ ec=$? ; \ if [ $ec -eq 0 ] ; then \ if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION SUCCESSFUL$" ; then ec=1 ; else \ -./cbmc-binary --unwinding-assertions --unwind $c --stop-on-fail $BIT_WIDTH --object-bits $OBJ_BITS $PROPERTY --function $ENTRY $BM > /dev/null 2>&1 || ec=42 ; \ +./cbmc-binary --unwinding-assertions --unwind $c --stop-on-fail --object-bits $OBJ_BITS $PROPERTY $LOG.bin > /dev/null 2>&1 || ec=42 ; \ fi ; \ fi ; \ if [ $ec -eq 10 ] ; then \ diff --git a/jbmc.inc b/jbmc.inc index 529679d..060307a 100755 --- a/jbmc.inc +++ b/jbmc.inc @@ -18,11 +18,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 --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 --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 ; \ +./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 \ diff --git a/tool-wrapper.inc b/tool-wrapper.inc index ff9f716..330a093 100755 --- a/tool-wrapper.inc +++ b/tool-wrapper.inc @@ -74,19 +74,19 @@ process_graphml() $(<$PROP_FILE)<\/data> $(echo $BM | sed 's8/8\\/8g')<\/data> $(sha1sum $BM | awk '{print $1}')<\/data> - ${BIT_WIDTH##--}bit<\/data>\\Q/" + ${BIT_WIDTH}bit<\/data>\\Q/" fi } OBJ_BITS="11" -BIT_WIDTH="--64" +BIT_WIDTH="64" BM="" PROP_FILE="" WITNESS_FILE="" while [ -n "$1" ] ; do case "$1" in - --32|--64) BIT_WIDTH="$1" ; shift 1 ;; + --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 ;; @@ -125,7 +125,7 @@ export OBJ_BITS export GMON_OUT_PREFIX=`basename $BM`.gmon.out export LOG=`mktemp -t ${TOOL_NAME}-log.XXXXXX` -trap "rm -f $LOG $LOG.latest $LOG.ok $LOG.witness" EXIT +trap "rm -f $LOG $LOG.latest $LOG.ok $LOG.witness $LOG.bin" EXIT run