test_script.sh (2981B)
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