tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh

   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
  26 set -e
  27
  28 if test "$#" -ne 2; then
  29         echo "Expected one option followed by an input file" 1>&2
  30         exit 99
  31 fi
  32
  33 if test "x$1" = "x--should-pass"; then
  34         should_pass="yes"
  35 elif test "x$1" = "x--should-fail"; then
  36         should_pass="no"
  37 else
  38         echo "Unrecognized argument '$1'" 1>&2
  39
  40         # Exit code 99 indicates a hard error.
  41         exit 99
  42 fi
  43
  44 CBMC=${CBMC:-cbmc}
  45
  46 SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple}
  47
  48 case ${SYNC_SRCU_MODE} in
  49 kernel) sync_srcu_mode_flags="" ;;
  50 simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;;
  51
  52 *)
  53         echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2
  54         exit 99
  55         ;;
  56 esac
  57
  58 min_cpus_fail=1
  59
  60 c_file=`dirname "$2"`/test.c
  61
  62 # Source the input file.
  63 . $2
  64
  65 if test ${min_cpus_fail} -gt 2; then
  66         default_default_cpus=${min_cpus_fail}
  67 else
  68         default_default_cpus=2
  69 fi
  70 default_cpus=${default_cpus:-${default_default_cpus}}
  71 cpus=${NR_CPUS:-${default_cpus}}
  72
  73 # Check if there are two few cpus to make the test fail.
  74 if test $cpus -lt ${min_cpus_fail:-0}; then
  75         should_pass="yes"
  76 fi
  77
  78 cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}"
  79
  80 echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}"
  81 if ${CBMC} ${cbmc_opts} "${c_file}"; then
  82         # Verification successful. Make sure that it was supposed to verify.
  83         test "x${should_pass}" = xyes
  84 else
  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
 103 fi