Merge pull request #8 from tautschnig/sv-comp-fixes

Fix configuration bugs and change CBMC behaviour

Author: peterschrammel

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

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 ; \
@@ -17,7 +22,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 +33,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 ; \
 \

tool-wrapper.inc

@@ -8,21 +8,21 @@ 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()
 {
   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$/);
 }'
 }
 
@@ -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)'
@@ -58,12 +61,12 @@ process_graphml()
     else
       TYPE="violation_witness"
     fi
-    cat $LOG.witness | perl -p -e "s/(<graph edgedefault=\"directed\">)/\$1\\E  
-      <data key=\"witness-type\">$(echo $TYPE)<\/data>                          
-      <data key=\"producer\">$(echo $TOOL_NAME)<\/data>                         
-      <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>       
+    cat $LOG.witness | perl -p -e "s/(<graph edgedefault=\"directed\">)/\$1\\E
+      <data key=\"witness-type\">$(echo $TYPE)<\/data>
+      <data key=\"producer\">$(echo $TOOL_NAME)<\/data>
+      <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/"
   fi
 }