#!/bin/sh if test -z "$EXPORT"; then set -e . util fi complain() { echo "### $@" > complaint } die() { test -f progress && cat progress rm progress complain "$@" exit 1 } report() { test -f report || return 0 if [ "$1" = '-q' ]; then shift; local QUIET=1 fi v=`grep "^$1:" report | cut -f2- -d: | cut -c2-` test -n "$3" && op="$3" || op="="; if test -n "$2" && ! test "$2" "$op" "$v"; then test "$QUIET" = 1 || complain "Expected $1 $op '$2' but got '$v' instead" return 1 fi echo "$v" > value; return 0 } report_print() { report "$@" cat value } ltl_algorithm() { report -q Algorithm OWCTY && return 0 report -q Algorithm "Nested DFS" && return 0 report -q Algorithm MAP && return 0 return 1 } reach_algorithm() { report -q Algorithm Reachability && return 0 report -q Algorithm "Weak Reachability" && return 0 report -q Algorithm CSDR && return 0 return 1 } ltl_valid() { report Finished Yes report -q Property-Type neverclaim || return 0 ltl_algorithm || return 0 report Property-Holds Yes } ltl_invalid() { report Finished Yes report -q Property-Type neverclaim || return 0 ltl_algorithm || return 0 report Property-Holds No } reachability_valid() { report Finished Yes reach_algorithm || return 0 report Property-Holds Yes } reachability_deadlock() { report Finished Yes report -q Property-Type deadlock || return 0 reach_algorithm || return 0 report Property-Holds No report CE-Type deadlock } reachability_goal() { report Finished Yes report -q Property-Type goal || return 0 reach_algorithm || return 0 report Property-Holds No report CE-Type goal } statespace() { test -f report || return 0 report Finished Yes op=-eq report -q Full-State-Space No && op=-le grep "^Transformations:.*POR" report && op=-le states=`report_print States-Visited` trans=`report_print Transition-Count` accept=`report_print States-Accepting` dead=`report_print Deadlock-Count` test $states $op $1 || die "States-Visited: $1 expected, $states got" test "$trans" = "-" || test $trans $op $2 || die "Transition-Count: $2 expected, $trans got" test $accept $op $3 || die "States-Accepting: $3 expected, $accept got" test "$dead" = "-" || test $dead $op $4 || die "Deadlock-Count: $4 expected, $dead got" } cleanup() { rm -f progress report testcase.{c,cpp,dve,dess} complaint *.core core* } clear() { cleanup echo "#### PASSED" echo } owcty_sizes() { test -f report || return 0 test -f progress || return 0 if ! grep -q "^Algorithm: OWCTY" report; then return 0; fi if grep -q "^Full-State-Space: No" report; then return 0; fi if grep -q "^Transformations:.*POR" report; then return 0; fi grep '|S| = ' progress | $esed -e 's,[^0-9]*([0-9]+).*,\1,' > numbers rm -f numbers-right for n in $@; do echo $n >> numbers-right; done diff -u numbers-right numbers } debris() { test -f progress && (cat progress; echo) || true for T in testcase.{c,cpp,dve}; do test -f $T && (nl -ba $T; echo) || true done if which gdb > /dev/null; then for core in $(ls *.core core* 2>/dev/null); do bin=$(gdb -batch -c "$core" 2>&1 | grep "generated by" | \ sed -e "s,.*generated by \`\([^ ']*\).*,\1,") if which lldb > /dev/null; then echo bt all | lldb -c "$core" $(which "$bin") else echo thread apply all bt full > gdb_commands.txt echo l >> gdb_commands.txt echo quit >> gdb_commands.txt gdb -batch -c "$core" -x gdb_commands.txt $(which "$bin") fi done fi || true test -f complaint && cat complaint || true cleanup } warn_table() { if test $((100 * $1)) -lt $((66 * $2)); then grep table verify.out echo WARNING: underutilized hash table $1/$2 touch warning fi } verify() { grep table verify.out | sed -re 's@.*\{ used: ([0-9]+), capacity: ([0-9]+) \}@\1 \2@' | \ while read used capacity; do case $capacity in 256) ;; # nothing 4096) warn_table $used 256 ;; 65536) warn_table $used 4096 ;; 524288) warn_table $used 65536 ;; *) warn_table $used $(($capacity / 4)) ;; esac done if fgrep -q '/* ERRSPEC:' "$1"; then spec=$(fgrep '/* ERRSPEC:' $1 | cut -d: -f2- | sed -e "s,^ *,," -e "s, *\*/,,") if test -n "$EXPORT"; then exit 1; fi echo spec: $spec if ! perl $TESTS/lib/check-errspec "$spec" verify.out; then echo "# expected error to be found in $spec, but it was not" exit 1 fi elif fgrep -q '/* ERROR' "$1"; then location=`fgrep -Hn '/* ERROR' "$1" | cut -d: -f1-2` if test -n "$EXPORT"; then echo "expect --result error --location $location"; exit 0 fi if ! grep -q "^ location: $location" verify.out; then nl -ba "$1" echo "# expected error to be found at $location, but it was not" exit 1 fi if fgrep -q '/* ERROR:' "$1"; then spec=$(fgrep '/* ERROR:' $1 | cut -d: -f2- | sed -e "s,^ *,," -e "s, *\*/,,") if ! grep -q "^ FAULT:.*$spec" verify.out; then echo "# expected FAULT: $spec in the output" exit 1 fi fi if test $(grep -c '^ FAULT:' verify.out) != 1 && ! grep -q '^property type: liveness' verify.out; then echo "# expected exactly one FAULT line in the trace" exit 1 fi if egrep -q "DOUBLE FAULT:" verify.out; then echo "# an unexpected double fault encountered" exit 1 fi if [ -s sim.out ] && ! grep -q "^ [{}a-zA-Z_].* at $location" sim.out; then cat sim.out nl -ba "$1" echo "# expected error to be found in divine sim at $location, but it was not" exit 1 fi elif fgrep -q '/* BOOT ERROR */' "$1"; then if test -n "$EXPORT"; then echo "expect --result boot-error"; exit 0; fi if ! grep -q "error found: boot" verify.out; then nl -ba "$1" echo "# boot error was expected but was not found" exit 1 fi else if test -n "$EXPORT"; then echo "expect --result valid"; exit 0; fi if ! grep -q "error found: no" verify.out; then nl -ba "$1" grep '^ location' verify.out || true echo "# no errors were expected but one was found anyway" exit 1 fi fi } sim() { cat > expected if ! ordgrep expected < sim.out; then exit 1; fi } "$@"