#!/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