1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0
3
4# This script expects a mode (either --should-pass or --should-fail) followed by
5# an input file. The script uses the following environment variables. The test C
6# source file is expected to be named test.c in the directory containing the
7# input file.
8#
9# CBMC: The command to run CBMC. Default: cbmc
10# CBMC_FLAGS: Additional flags to pass to CBMC
11# NR_CPUS: Number of cpus to run tests with. Default specified by the test
12# SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple.
13#                 kernel: Version included in the linux kernel source.
14#                 simple: Use try_check_zero directly.
15#
16# The input file is a script that is sourced by this file. It can define any of
17# the following variables to configure the test.
18#
19# test_cbmc_options: Extra options to pass to CBMC.
20# min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail.
21#                The test is expected to pass if it is run with fewer. (Only
22#                useful for .fail files)
23# default_cpus: Quantity of CPUs to use for the test, if not specified on the
24#               command line. Default: Larger of 2 and MIN_CPUS_FAIL.
25
26set -e
27
28if test "$#" -ne 2; then
29	echo "Expected one option followed by an input file" 1>&2
30	exit 99
31fi
32
33if test "x$1" = "x--should-pass"; then
34	should_pass="yes"
35elif test "x$1" = "x--should-fail"; then
36	should_pass="no"
37else
38	echo "Unrecognized argument '$1'" 1>&2
39
40	# Exit code 99 indicates a hard error.
41	exit 99
42fi
43
44CBMC=${CBMC:-cbmc}
45
46SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple}
47
48case ${SYNC_SRCU_MODE} in
49kernel) sync_srcu_mode_flags="" ;;
50simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;;
51
52*)
53	echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2
54	exit 99
55	;;
56esac
57
58min_cpus_fail=1
59
60c_file=`dirname "$2"`/test.c
61
62# Source the input file.
63. $2
64
65if test ${min_cpus_fail} -gt 2; then
66	default_default_cpus=${min_cpus_fail}
67else
68	default_default_cpus=2
69fi
70default_cpus=${default_cpus:-${default_default_cpus}}
71cpus=${NR_CPUS:-${default_cpus}}
72
73# Check if there are two few cpus to make the test fail.
74if test $cpus -lt ${min_cpus_fail:-0}; then
75	should_pass="yes"
76fi
77
78cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}"
79
80echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}"
81if ${CBMC} ${cbmc_opts} "${c_file}"; then
82	# Verification successful. Make sure that it was supposed to verify.
83	test "x${should_pass}" = xyes
84else
85	cbmc_exit_status=$?
86
87	# An exit status of 10 indicates a failed verification.
88	# (see cbmc_parse_optionst::do_bmc in the CBMC source code)
89	if test ${cbmc_exit_status} -eq 10 && test "x${should_pass}" = xno; then
90		:
91	else
92		echo "CBMC returned ${cbmc_exit_status} exit status" 1>&2
93
94		# Parse errors have exit status 6. Any other type of error
95		# should be considered a hard error.
96		if test ${cbmc_exit_status} -ne 6 && \
97		   test ${cbmc_exit_status} -ne 10; then
98			exit 99
99		else
100			exit 1
101		fi
102	fi
103fi
104