From 273e8b58ce5f387b90b561407e4920141503dc57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 31 Mar 2018 09:30:31 +0100 Subject: [PATCH] Use goto-cc to compile once and establish sharing Writing goto binaries establishes sharing of equal irepts, which is beneficial to all subsequent stages of analysis. For CBMC this furthermore implies that compilation is only done once instead of doing so for every loop unwinding attempt. --- 2ls.inc | 17 +++++++++++------ Makefile | 10 ++++++---- cbmc.inc | 9 +++++++-- jbmc.inc | 4 ++-- tool-wrapper.inc | 8 ++++---- 5 files changed, 30 insertions(+), 18 deletions(-) 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