| #!/bin/sh |
| # SPDX-License-Identifier: GPL-2.0 |
| |
| # 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 |