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

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