From 3a6611feacbd171c4d48ddc4c59855c748082cf3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 11:27:03 +0000 Subject: [PATCH 1/5] Ensure proper permissions --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 62ed09a..984ce43 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ CBMC-sv-comp-$(YEAR).tar.gz: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/s mv cbmc-wrapper tmp/cbmc cp $(CBMC)/LICENSE tmp/ cp $(CBMC)/src/cbmc/cbmc tmp/cbmc-binary - cd tmp && tar cfz ../$@ * && rm cbmc cbmc-binary LICENSE + cd tmp && chmod a+rX * && tar cfz ../$@ * && rm cbmc cbmc-binary LICENSE rmdir tmp 2ls-sv-comp-$(YEAR).tar.gz: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/summarizer/2ls @@ -30,5 +30,5 @@ CBMC-sv-comp-$(YEAR).tar.gz: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/s mv 2ls-wrapper tmp/2ls cp $(2LS)/LICENSE tmp/ cp $(2LS)/src/summarizer/2ls tmp/2ls-binary - cd tmp && tar cfz ../$@ * && rm 2ls 2ls-binary LICENSE + cd tmp && chmod a+rX * && tar cfz ../$@ * && rm 2ls 2ls-binary LICENSE rmdir tmp From cf9c639512ca3f7731604482ecd0468b0142f174 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 11:28:13 +0000 Subject: [PATCH 2/5] Removed whitespace at end of line --- tool-wrapper.inc | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/tool-wrapper.inc b/tool-wrapper.inc index 9083239..ef5843b 100755 --- a/tool-wrapper.inc +++ b/tool-wrapper.inc @@ -15,14 +15,14 @@ parse_property_file() { local fn=$1 - cat $fn | sed 's/[[:space:]]//g' | perl -n -e ' -if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) { - print "ENTRY=$1\n"; - print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/); + cat $fn | sed 's/[[:space:]]//g' | perl -n -e ' +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=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/); - print "PROP=\"overflow\"\n" if($2 =~ /^G!overflow$/); - print "PROP=\"termination\"\n" if($2 =~ /^Fend$/); + 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$/); }' } @@ -58,12 +58,12 @@ process_graphml() else TYPE="violation_witness" fi - cat $LOG.witness | perl -p -e "s/()/\$1\\E - $(echo $TYPE)<\/data> - $(echo $TOOL_NAME)<\/data> - $(<$PROP_FILE)<\/data> - $(echo $BM | sed 's8/8\\/8g')<\/data> - $(sha1sum $BM | awk '{print $1}')<\/data> + cat $LOG.witness | perl -p -e "s/()/\$1\\E + $(echo $TYPE)<\/data> + $(echo $TOOL_NAME)<\/data> + $(<$PROP_FILE)<\/data> + $(echo $BM | sed 's8/8\\/8g')<\/data> + $(sha1sum $BM | awk '{print $1}')<\/data> ${BIT_WIDTH##--}bit<\/data>\\Q/" fi } From 3f42fcf817d1747906d72db13968c8951bcec12e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 16:02:43 +0000 Subject: [PATCH 3/5] Fix property parsing for out-of-bounds, disable assertions in overflow/memsafety --- tool-wrapper.inc | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/tool-wrapper.inc b/tool-wrapper.inc index ef5843b..566e74e 100755 --- a/tool-wrapper.inc +++ b/tool-wrapper.inc @@ -8,8 +8,8 @@ declare -A OPTIONS OPTIONS["label"]="--error-label" OPTIONS["unreach_call"]="" OPTIONS["termination"]="" -OPTIONS["overflow"]="--signed-overflow-check" -OPTIONS["memsafety"]="--pointer-check --memory-leak-check --bounds-check" +OPTIONS["overflow"]="--signed-overflow-check --no-assertions" +OPTIONS["memsafety"]="--pointer-check --memory-leak-check --bounds-check --no-assertions" parse_property_file() { @@ -34,6 +34,9 @@ parse_result() elif tail -n 50 $LOG.ok | \ grep -Eq "^(\[.*\] |[[:space:]]*)dereference failure:" ; then echo 'FALSE(valid-deref)' + elif tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)array.* upper bound in " ; then + echo 'FALSE(valid-deref)' elif tail -n 50 $LOG.ok | \ grep -Eq "^(\[.*\] |[[:space:]]*)double free$" ; then echo 'FALSE(valid-free)' From 017a2e91d68a0d1c137e24c96f32af40ee67e8b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 16:04:13 +0000 Subject: [PATCH 4/5] Only report TRUE when unwinding was sufficient --- cbmc.inc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/cbmc.inc b/cbmc.inc index 3fdb101..1b86f9b 100644 --- a/cbmc.inc +++ b/cbmc.inc @@ -17,7 +17,9 @@ echo "Unwind: $c" > $LOG.latest ; \ ./cbmc-binary --graphml-witness $LOG.witness --unwind $c --stop-on-fail $BIT_WIDTH $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 ; fi ; \ +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 $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 ; \ @@ -26,6 +28,7 @@ fi ; \ case $ec in \ 0) EC=0 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ;; \ 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 ; \ \ From ddf8fecccbd617a717652df339ac08458777b477 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Dec 2016 01:50:01 +0000 Subject: [PATCH 5/5] CBMC can't handle termination --- cbmc.inc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cbmc.inc b/cbmc.inc index 1b86f9b..5540af9 100644 --- a/cbmc.inc +++ b/cbmc.inc @@ -7,6 +7,11 @@ TOOL_NAME=CBMC run() { + if [ "$PROP" = "termination" ] ; then + EC=42 + return + fi + timeout 850 bash -c ' \ \ ulimit -v 15000000 ; \