/* 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_FUTEX_LOCK_PI,
        LTL_FUTEX_WAIT,
        LTL_KERNEL_THREAD,
        LTL_KTHREAD_SHOULD_STOP,
        LTL_NANOSLEEP_CLOCK_MONOTONIC,
        LTL_NANOSLEEP_CLOCK_TAI,
        LTL_NANOSLEEP_TIMER_ABSTIME,
        LTL_RT,
        LTL_SLEEP,
        LTL_TASK_IS_MIGRATION,
        LTL_TASK_IS_RCU,
        LTL_WAKE,
        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",
                "fu_lo_pi",
                "fu_wa",
                "ker_th",
                "kth_sh_st",
                "na_cl_mo",
                "na_cl_ta",
                "na_ti_ab",
                "rt",
                "sl",
                "ta_mi",
                "ta_rc",
                "wak",
                "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 task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
        bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
        bool val40 = task_is_rcu || task_is_migration;
        bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
        bool val41 = futex_lock_pi || val40;
        bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
        bool val5 = block_on_rt_mutex || val41;
        bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
        bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
        bool val32 = abort_sleep || kthread_should_stop;
        bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
        bool val33 = woken_by_nmi || val32;
        bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
        bool val34 = woken_by_hardirq || val33;
        bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
             mon->atoms);
        bool val14 = woken_by_equal_or_higher_prio || val34;
        bool wake = test_bit(LTL_WAKE, mon->atoms);
        bool val13 = !wake;
        bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
        bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
        bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
        bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai;
        bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
        bool val25 = nanosleep_timer_abstime && val24;
        bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
        bool val18 = clock_nanosleep && val25;
        bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
        bool val9 = futex_wait || val18;
        bool val11 = val9 || kernel_thread;
        bool sleep = test_bit(LTL_SLEEP, mon->atoms);
        bool val2 = !sleep;
        bool rt = test_bit(LTL_RT, mon->atoms);
        bool val1 = !rt;
        bool val3 = val1 || val2;

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

static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
        bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
        bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
        bool val40 = task_is_rcu || task_is_migration;
        bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
        bool val41 = futex_lock_pi || val40;
        bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
        bool val5 = block_on_rt_mutex || val41;
        bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
        bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
        bool val32 = abort_sleep || kthread_should_stop;
        bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
        bool val33 = woken_by_nmi || val32;
        bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
        bool val34 = woken_by_hardirq || val33;
        bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
             mon->atoms);
        bool val14 = woken_by_equal_or_higher_prio || val34;
        bool wake = test_bit(LTL_WAKE, mon->atoms);
        bool val13 = !wake;
        bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
        bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
        bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
        bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai;
        bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
        bool val25 = nanosleep_timer_abstime && val24;
        bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
        bool val18 = clock_nanosleep && val25;
        bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
        bool val9 = futex_wait || val18;
        bool val11 = val9 || kernel_thread;
        bool sleep = test_bit(LTL_SLEEP, mon->atoms);
        bool val2 = !sleep;
        bool rt = test_bit(LTL_RT, mon->atoms);
        bool val1 = !rt;
        bool val3 = val1 || val2;

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