Merge pull request #29 from tautschnig/goto-cc

Use goto-cc to compile once and establish sharing

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