Commit | Line | Data |
---|---|---|
b02eb5b0 PM |
1 | #!/bin/sh |
2 | # SPDX-License-Identifier: GPL-2.0+ | |
3 | # | |
2024436d PM |
4 | # Given a .litmus test and the corresponding litmus output file, check |
5 | # the .litmus.out file against the "Result:" comment to judge whether the | |
6 | # test ran correctly. If the --hw argument is omitted, check against the | |
7 | # LKMM output, which is assumed to be in file.litmus.out. If this argument | |
8 | # is provided, this is assumed to be a hardware test, and the output is | |
ee542816 | 9 | # assumed to be in file.litmus.HW.out, where "HW" is the --hw argument. |
2024436d | 10 | # In addition, non-Sometimes verification results will be noted, but |
0838ba7e PM |
11 | # forgiven. Furthermore, if there is no "Result:" comment but there is |
12 | # an LKMM .litmus.out file, the observation in that file will be used | |
13 | # to judge the assembly-language verification. | |
b02eb5b0 PM |
14 | # |
15 | # Usage: | |
16 | # judgelitmus.sh file.litmus | |
17 | # | |
18 | # Run this in the directory containing the memory model, specifying the | |
19 | # pathname of the litmus test to check. | |
20 | # | |
21 | # Copyright IBM Corporation, 2018 | |
22 | # | |
61f615cc | 23 | # Author: Paul E. McKenney <paulmck@linux.ibm.com> |
b02eb5b0 PM |
24 | |
25 | litmus=$1 | |
26 | ||
27 | if test -f "$litmus" -a -r "$litmus" | |
28 | then | |
29 | : | |
30 | else | |
31 | echo ' --- ' error: \"$litmus\" is not a readable file | |
32 | exit 255 | |
33 | fi | |
2024436d PM |
34 | if test -z "$LKMM_HW_MAP_FILE" |
35 | then | |
36 | litmusout=$litmus.out | |
0838ba7e | 37 | lkmmout= |
2024436d PM |
38 | else |
39 | litmusout="`echo $litmus | | |
ee542816 | 40 | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out" |
0838ba7e | 41 | lkmmout=$litmus.out |
2024436d PM |
42 | fi |
43 | if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" | |
b02eb5b0 PM |
44 | then |
45 | : | |
46 | else | |
2024436d | 47 | echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file |
b02eb5b0 PM |
48 | exit 255 |
49 | fi | |
50 | if grep -q '^ \* Result: ' $litmus | |
51 | then | |
52 | outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` | |
0838ba7e PM |
53 | elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 |
54 | then | |
55 | outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` | |
b02eb5b0 PM |
56 | else |
57 | outcome=specified | |
58 | fi | |
59 | ||
2024436d PM |
60 | grep '^Observation' $LKMM_DESTDIR/$litmusout |
61 | if grep -q '^Observation' $LKMM_DESTDIR/$litmusout | |
b02eb5b0 PM |
62 | then |
63 | : | |
2024436d | 64 | elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
02484d82 | 65 | then |
2024436d | 66 | badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout | |
02484d82 PM |
67 | sed -e 's/^.*: Unknown macro //' | |
68 | sed -e 's/ (User error).*$//'` | |
69 | badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus" | |
70 | echo $badmsg | |
2024436d | 71 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
02484d82 | 72 | then |
2024436d | 73 | echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1 |
02484d82 PM |
74 | fi |
75 | exit 254 | |
2024436d | 76 | elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout |
2c644d3f PM |
77 | then |
78 | echo ' !!! Timeout' $litmus | |
2024436d | 79 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
2c644d3f | 80 | then |
2024436d | 81 | echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1 |
2c644d3f PM |
82 | fi |
83 | exit 124 | |
b02eb5b0 PM |
84 | else |
85 | echo ' !!! Verification error' $litmus | |
2024436d | 86 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
b02eb5b0 | 87 | then |
2024436d | 88 | echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1 |
b02eb5b0 PM |
89 | fi |
90 | exit 255 | |
91 | fi | |
92 | if test "$outcome" = DEADLOCK | |
93 | then | |
2024436d | 94 | if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' |
b02eb5b0 PM |
95 | then |
96 | ret=0 | |
97 | else | |
98 | echo " !!! Unexpected non-$outcome verification" $litmus | |
2024436d | 99 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
b02eb5b0 | 100 | then |
2024436d | 101 | echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 |
b02eb5b0 PM |
102 | fi |
103 | ret=1 | |
104 | fi | |
2024436d | 105 | elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' |
e253a403 PM |
106 | then |
107 | echo " !!! Unexpected non-$outcome deadlock" $litmus | |
2024436d | 108 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
e253a403 | 109 | then |
2024436d | 110 | echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1 |
e253a403 PM |
111 | fi |
112 | ret=1 | |
2024436d | 113 | elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe |
b02eb5b0 PM |
114 | then |
115 | ret=0 | |
116 | else | |
2024436d | 117 | if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes |
b02eb5b0 | 118 | then |
2024436d PM |
119 | flag="--- Forgiven" |
120 | ret=0 | |
121 | else | |
122 | flag="!!! Unexpected" | |
123 | ret=1 | |
124 | fi | |
125 | echo " $flag non-$outcome verification" $litmus | |
126 | if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout | |
127 | then | |
128 | echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 | |
b02eb5b0 | 129 | fi |
b02eb5b0 | 130 | fi |
2024436d | 131 | tail -2 $LKMM_DESTDIR/$litmusout | head -1 |
b02eb5b0 | 132 | exit $ret |