aboutsummaryrefslogtreecommitdiffstats
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
blob: d1545972a0fa431b4bb8e2cc75188142a105e6a6 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
#!/bin/sh

# This script expects a mode (either --should-pass or --should-fail) followed by
# an input file. The script uses the following environment variables. The test C
# source file is expected to be named test.c in the directory containing the
# input file.
#
# CBMC: The command to run CBMC. Default: cbmc
# CBMC_FLAGS: Additional flags to pass to CBMC
# NR_CPUS: Number of cpus to run tests with. Default specified by the test
# SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple.
#                 kernel: Version included in the linux kernel source.
#                 simple: Use try_check_zero directly.
#
# The input file is a script that is sourced by this file. It can define any of
# the following variables to configure the test.
#
# test_cbmc_options: Extra options to pass to CBMC.
# min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail.
#                The test is expected to pass if it is run with fewer. (Only
#                useful for .fail files)
# default_cpus: Quantity of CPUs to use for the test, if not specified on the
#               command line. Default: Larger of 2 and MIN_CPUS_FAIL.

set -e

if test "$#" -ne 2; then
	echo "Expected one option followed by an input file" 1>&2
	exit 99
fi

if test "x$1" = "x--should-pass"; then
	should_pass="yes"
elif test "x$1" = "x--should-fail"; then
	should_pass="no"
else
	echo "Unrecognized argument '$1'" 1>&2

	# Exit code 99 indicates a hard error.
	exit 99
fi

CBMC=${CBMC:-cbmc}

SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple}

case ${SYNC_SRCU_MODE} in
kernel) sync_srcu_mode_flags="" ;;
simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;;

*)
	echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2
	exit 99
	;;
esac

min_cpus_fail=1

c_file=`dirname "$2"`/test.c

# Source the input file.
. $2

if test ${min_cpus_fail} -gt 2; then
	default_default_cpus=${min_cpus_fail}
else
	default_default_cpus=2
fi
default_cpus=${default_cpus:-${default_default_cpus}}
cpus=${NR_CPUS:-${default_cpus}}

# Check if there are two few cpus to make the test fail.
if test $cpus -lt ${min_cpus_fail:-0}; then
	should_pass="yes"
fi

cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}"

echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}"
if ${CBMC} ${cbmc_opts} "${c_file}"; then
	# Verification successful. Make sure that it was supposed to verify.
	test "x${should_pass}" = xyes
else
	cbmc_exit_status=$?

	# An exit status of 10 indicates a failed verification.
	# (see cbmc_parse_optionst::do_bmc in the CBMC source code)
	if test ${cbmc_exit_status} -eq 10 && test "x${should_pass}" = xno; then
		:
	else
		echo "CBMC returned ${cbmc_exit_status} exit status" 1>&2

		# Parse errors have exit status 6. Any other type of error
		# should be considered a hard error.
		if test ${cbmc_exit_status} -ne 6 && \
		   test ${cbmc_exit_status} -ne 10; then
			exit 99
		else
			exit 1
		fi
	fi
fi