|
| 1 | + |
| 2 | +# main tool wrapper script |
| 3 | +# run "make <tool>-wrapper" to generate the wrapper script |
| 4 | + |
| 5 | +# map properties to tool options |
| 6 | + |
| 7 | +declare -A OPTIONS |
| 8 | +OPTIONS["label"]="--error-label" |
| 9 | +OPTIONS["unreach_call"]="" |
| 10 | +OPTIONS["termination"]="" |
| 11 | +OPTIONS["overflow"]="--signed-overflow-check" |
| 12 | +OPTIONS["memsafety"]="--pointer-check --memory-leak-check --bounds-check" |
| 13 | + |
| 14 | +parse_property_file() |
| 15 | +{ |
| 16 | + local fn=$1 |
| 17 | + |
| 18 | + cat $fn | sed 's/[[:space:]]//g' | perl -n -e ' |
| 19 | +if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) { |
| 20 | + print "ENTRY=$1\n"; |
| 21 | + print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/); |
| 22 | + print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(__VERIFIER_error\(\)\)$/); |
| 23 | + print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/); |
| 24 | + print "PROP=\"overflow\"\n" if($2 =~ /^G!overflow$/); |
| 25 | + print "PROP=\"termination\"\n" if($2 =~ /^Fend$/); |
| 26 | +}' |
| 27 | +} |
| 28 | + |
| 29 | +parse_result() |
| 30 | +{ |
| 31 | + if tail -n 50 $LOG.ok | grep -q "^[[:space:]]*__CPROVER_memory_leak == NULL$"\ |
| 32 | + ; then |
| 33 | + echo 'FALSE(valid-memtrack)' |
| 34 | + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*dereference failure:" ; then |
| 35 | + echo 'FALSE(valid-deref)' |
| 36 | + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*double free$" ; then |
| 37 | + echo 'FALSE(valid-free)' |
| 38 | + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*free argument has offset zero\ |
| 39 | +$" ; then |
| 40 | + echo 'FALSE(valid-free)' |
| 41 | + elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*arithmetic overflow on signed\ |
| 42 | +" ; then |
| 43 | + echo 'FALSE(no-overflow)' |
| 44 | + elif [[ "$PROP" == "termination" ]]; then |
| 45 | + echo 'FALSE(termination)' |
| 46 | + else |
| 47 | + echo FALSE |
| 48 | + fi |
| 49 | +} |
| 50 | + |
| 51 | +process_graphml() |
| 52 | +{ |
| 53 | + if [ -f $LOG.witness ]; then |
| 54 | + if [ $1 -eq 0 ]; then |
| 55 | + TYPE="correctness_witness" |
| 56 | + else |
| 57 | + TYPE="violation_witness" |
| 58 | + fi |
| 59 | + cat $LOG.witness | perl -p -e "s/(<graph edgedefault=\"directed\">)/\$1\\E |
| 60 | + <data key=\"witness-type\">$(echo $TYPE)<\/data> |
| 61 | + <data key=\"producer\">$(echo $TOOL_NAME)<\/data> |
| 62 | + <data key=\"specification\">$(<$PROP_FILE)<\/data> |
| 63 | + <data key=\"programfile\">$(echo $BM | sed 's8/8\\/8g')<\/data> |
| 64 | + <data key=\"programhash\">$(sha1sum $BM | awk '{print $1}')<\/data> |
| 65 | + <data key=\"architecture\">${BIT_WIDTH##--}bit<\/data>\\Q/" |
| 66 | + fi |
| 67 | +} |
| 68 | + |
| 69 | +BIT_WIDTH="--64" |
| 70 | +BM="" |
| 71 | +PROP_FILE="" |
| 72 | +WITNESS_FILE="" |
| 73 | + |
| 74 | +while [ -n "$1" ] ; do |
| 75 | + case "$1" in |
| 76 | + --32|--64) BIT_WIDTH="$1" ; shift 1 ;; |
| 77 | + --propertyfile) PROP_FILE="$2" ; shift 2 ;; |
| 78 | + --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;; |
| 79 | + --version) $TOOL_BINARY --version ; exit 0 ;; |
| 80 | + *) BM="$1" ; shift 1 ;; |
| 81 | + esac |
| 82 | +done |
| 83 | + |
| 84 | +if [ -z "$BM" ] || [ -z "$PROP_FILE" ] ; then |
| 85 | + echo "Missing benchmark or property file" |
| 86 | + exit 1 |
| 87 | +fi |
| 88 | + |
| 89 | +if [ ! -s "$BM" ] || [ ! -s "$PROP_FILE" ] ; then |
| 90 | + echo "Empty benchmark or property file" |
| 91 | + exit 1 |
| 92 | +fi |
| 93 | + |
| 94 | +eval `parse_property_file $PROP_FILE` |
| 95 | + |
| 96 | +if [[ "$PROP" == "" ]]; then |
| 97 | + echo "Unrecognized property specification" |
| 98 | + exit 1 |
| 99 | +elif [[ "$PROP" == "label" ]]; then |
| 100 | + PROPERTY="${OPTIONS[$PROP]} $LABEL" |
| 101 | +else |
| 102 | + PROPERTY=${OPTIONS[$PROP]} |
| 103 | +fi |
| 104 | + |
| 105 | +export ENTRY |
| 106 | +export PROPERTY |
| 107 | +export BIT_WIDTH |
| 108 | +export BM |
| 109 | +export PROP |
| 110 | + |
| 111 | +export LOG=`mktemp -t ${TOOL_NAME}-log.XXXXXX` |
| 112 | +trap "rm -f $LOG $LOG.latest $LOG.ok $LOG.witness" EXIT |
| 113 | + |
| 114 | +run |
| 115 | + |
| 116 | +if [ ! -s $LOG.ok ] ; then |
| 117 | + exit 1 |
| 118 | +fi |
| 119 | + |
| 120 | +eval `tail -n 1 $LOG.ok` |
| 121 | +cat $LOG.ok |
| 122 | +case $EC in |
| 123 | + 0) if [[ "$WITNESS_FILE" != "" ]]; then process_graphml $EC > $WITNESS_FILE; \ |
| 124 | +fi; echo "TRUE" ;; |
| 125 | + 10) if [[ "$WITNESS_FILE" != "" ]]; then process_graphml $EC > $WITNESS_FILE;\ |
| 126 | + fi; parse_result ;; |
| 127 | + *) echo "UNKNOWN" ;; |
| 128 | +esac |
| 129 | +exit $EC |
0 commit comments