/* SPDX-License-Identifier: GPL-2.0 */

/*
 * C implementation of Buchi automaton, automatically generated by
 * tools/verification/rvgen from the linear temporal logic specification.
 * For further information, see kernel documentation:
 *   Documentation/trace/rv/linear_temporal_logic.rst
 */

#include <linux/rv.h>

#define MONITOR_NAME sleep

enum ltl_atom {
	LTL_ABORT_SLEEP,
	LTL_BLOCK_ON_RT_MUTEX,
	LTL_CLOCK_NANOSLEEP,
	LTL_EPOLL_WAIT,
	LTL_FUTEX_LOCK_PI,
	LTL_FUTEX_WAIT,
	LTL_NANOSLEEP_CLOCK_REALTIME,
	LTL_NANOSLEEP_TIMER_ABSTIME,
	LTL_RT,
	LTL_SCHEDULE_IN,
	LTL_SLEEP,
	LTL_USER_THREAD,
	LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
	LTL_WOKEN_BY_HARDIRQ,
	LTL_WOKEN_BY_NMI,
	LTL_NUM_ATOM
};
static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);

static const char *ltl_atom_str(enum ltl_atom atom)
{
	static const char *const names[] = {
		"ab_sl",
		"bl_on_rt_mu",
		"cl_na",
		"ep_wa",
		"fu_lo_pi",
		"fu_wa",
		"na_cl_re",
		"na_ti_ab",
		"rt",
		"sch_in",
		"sle",
		"us_th",
		"wo_eq_hi_pr",
		"wo_ha",
		"wo_nm",
	};

	return names[atom];
}

enum ltl_buchi_state {
	S0,
	S1,
	S2,
	S3,
	S4,
	S5,
	S6,
	S7,
	RV_NUM_BA_STATES
};
static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);

static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
{
	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
	     mon->atoms);
	bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
	bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
	bool rt = test_bit(LTL_RT, mon->atoms);
	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
	bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
	bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
	bool val7 = block_on_rt_mutex || futex_lock_pi;
	bool val32 = woken_by_nmi || abort_sleep;
	bool val33 = woken_by_hardirq || val32;
	bool val14 = woken_by_equal_or_higher_prio || val33;
	bool val13 = !schedule_in;
	bool val25 = !nanosleep_clock_realtime;
	bool val26 = nanosleep_timer_abstime && val25;
	bool val18 = clock_nanosleep && val26;
	bool val20 = val18 || epoll_wait;
	bool val11 = futex_wait || val20;
	bool val3 = !user_thread;
	bool val2 = !sleep;
	bool val4 = val2 || val3;
	bool val1 = !rt;
	bool val5 = val1 || val4;

	if (val5)
		__set_bit(S0, mon->states);
	if (val11 && val13)
		__set_bit(S1, mon->states);
	if (val11 && val14)
		__set_bit(S4, mon->states);
	if (val7)
		__set_bit(S5, mon->states);
}

static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
	     mon->atoms);
	bool user_thread = test_bit(LTL_USER_THREAD, mon->atoms);
	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
	bool schedule_in = test_bit(LTL_SCHEDULE_IN, mon->atoms);
	bool rt = test_bit(LTL_RT, mon->atoms);
	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
	bool nanosleep_clock_realtime = test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms);
	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
	bool epoll_wait = test_bit(LTL_EPOLL_WAIT, mon->atoms);
	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
	bool val7 = block_on_rt_mutex || futex_lock_pi;
	bool val32 = woken_by_nmi || abort_sleep;
	bool val33 = woken_by_hardirq || val32;
	bool val14 = woken_by_equal_or_higher_prio || val33;
	bool val13 = !schedule_in;
	bool val25 = !nanosleep_clock_realtime;
	bool val26 = nanosleep_timer_abstime && val25;
	bool val18 = clock_nanosleep && val26;
	bool val20 = val18 || epoll_wait;
	bool val11 = futex_wait || val20;
	bool val3 = !user_thread;
	bool val2 = !sleep;
	bool val4 = val2 || val3;
	bool val1 = !rt;
	bool val5 = val1 || val4;

	switch (state) {
	case S0:
		if (val5)
			__set_bit(S0, next);
		if (val11 && val13)
			__set_bit(S1, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val7)
			__set_bit(S5, next);
		break;
	case S1:
		if (val11 && val13)
			__set_bit(S1, next);
		if (val13 && val5)
			__set_bit(S2, next);
		if (val14 && val5)
			__set_bit(S3, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val13 && val7)
			__set_bit(S6, next);
		if (val14 && val7)
			__set_bit(S7, next);
		break;
	case S2:
		if (val11 && val13)
			__set_bit(S1, next);
		if (val13 && val5)
			__set_bit(S2, next);
		if (val14 && val5)
			__set_bit(S3, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val13 && val7)
			__set_bit(S6, next);
		if (val14 && val7)
			__set_bit(S7, next);
		break;
	case S3:
		if (val5)
			__set_bit(S0, next);
		if (val11 && val13)
			__set_bit(S1, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val7)
			__set_bit(S5, next);
		break;
	case S4:
		if (val5)
			__set_bit(S0, next);
		if (val11 && val13)
			__set_bit(S1, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val7)
			__set_bit(S5, next);
		break;
	case S5:
		if (val5)
			__set_bit(S0, next);
		if (val11 && val13)
			__set_bit(S1, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val7)
			__set_bit(S5, next);
		break;
	case S6:
		if (val11 && val13)
			__set_bit(S1, next);
		if (val13 && val5)
			__set_bit(S2, next);
		if (val14 && val5)
			__set_bit(S3, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val13 && val7)
			__set_bit(S6, next);
		if (val14 && val7)
			__set_bit(S7, next);
		break;
	case S7:
		if (val5)
			__set_bit(S0, next);
		if (val11 && val13)
			__set_bit(S1, next);
		if (val11 && val14)
			__set_bit(S4, next);
		if (val7)
			__set_bit(S5, next);
		break;
	}
}