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.

Author: tautschnig

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=$?

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

cbmc.inc

@@ -11,18 +11,23 @@ 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 ; \
 \
 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 \

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 \

tool-wrapper.inc

@@ -74,19 +74,19 @@ process_graphml()
       <data key=\"specification\">$(<$PROP_FILE)<\/data>
       <data key=\"programfile\">$(echo $BM | sed 's8/8\\/8g')<\/data>
       <data key=\"programhash\">$(sha1sum $BM | awk '{print $1}')<\/data>
-      <data key=\"architecture\">${BIT_WIDTH##--}bit<\/data>\\Q/"
+      <data key=\"architecture\">${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