verification/rvgen: Add selftests for rvgen kunit

The rvgen kunit command patches monitor files and adds necessary
definitions for kunit tests.

Add a test case validating its behaviour on dummy generated files and
comparing it against reference files, like it's done for rvgen monitor.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-11-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_BAK_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select LTL_MON_EVENTS_ID
+	bool "test_bak_kunit monitor"
+	help
+	  auto-generated

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c

@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_bak_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "test_bak_kunit.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_test_bak_kunit(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_test_bak_kunit(void)
+{
+	rv_detach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_bak_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_bak_kunit,
+	.disable = disable_test_bak_kunit,
+};
+
+static int __init register_test_bak_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_bak_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_bak_kunit);
+module_exit(unregister_test_bak_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_bak_kunit: auto-generated");

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h

@@ -0,0 +1,108 @@
+/* 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 test_bak_kunit
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	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[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	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 event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_bak_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_BAK_KUNIT)
+
+static void rv_test_test_bak_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_bak_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_bak_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_bak_kunit rv_test_stub
+#endif

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.bak

@@ -0,0 +1 @@
+DUMMY

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h

@@ -0,0 +1,22 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_BAK_KUNIT_KUNIT_H
+#define __TEST_BAK_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_bak_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_example_event)(void *data, /* XXX: fill header */);
+} rv_test_bak_kunit_ops;
+#endif
+
+#endif /* __TEST_BAK_KUNIT_KUNIT_H */

tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h

@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_BAK_KUNIT
+DEFINE_EVENT(event_ltl_monitor_id, event_test_bak_kunit,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_test_bak_kunit,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_TEST_BAK_KUNIT */

tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_DA_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select DA_MON_EVENTS_IMPLICIT
+	bool "test_da_kunit monitor"
+	help
+	  auto-generated

tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c

@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_da_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_CPU
+#include "test_da_kunit.h"
+#include <rv/da_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+static void handle_event_1(void *data, /* XXX: fill header */)
+{
+	da_handle_event(event_1_test_da_kunit);
+}
+
+static void handle_event_2(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	da_handle_start_event(event_2_test_da_kunit);
+}
+
+static int enable_test_da_kunit(void)
+{
+	int retval;
+
+	retval = da_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
+	rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
+
+	return 0;
+}
+
+static void disable_test_da_kunit(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1);
+	rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2);
+
+	da_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_da_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_da_kunit,
+	.disable = disable_test_da_kunit,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_da_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_da_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_da_kunit);
+module_exit(unregister_test_da_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_da_kunit: auto-generated");
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#include <kunit/visibility.h>
+#include "test_da_kunit_kunit.h"
+
+const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = {
+	.mon = RV_MON_OPS_INIT(),
+	.handle_event_1 = handle_event_1,
+	.handle_event_2 = handle_event_2,
+};
+EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops);
+#endif

tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h

@@ -0,0 +1,47 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_da_kunit automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_da_kunit
+
+enum states_test_da_kunit {
+	state_a_test_da_kunit,
+	state_b_test_da_kunit,
+	state_max_test_da_kunit,
+};
+
+#define INVALID_STATE state_max_test_da_kunit
+
+enum events_test_da_kunit {
+	event_1_test_da_kunit,
+	event_2_test_da_kunit,
+	event_max_test_da_kunit,
+};
+
+struct automaton_test_da_kunit {
+	char *state_names[state_max_test_da_kunit];
+	char *event_names[event_max_test_da_kunit];
+	unsigned char function[state_max_test_da_kunit][event_max_test_da_kunit];
+	unsigned char initial_state;
+	bool final_states[state_max_test_da_kunit];
+};
+
+static const struct automaton_test_da_kunit automaton_test_da_kunit = {
+	.state_names = {
+		"state_a",
+		"state_b",
+	},
+	.event_names = {
+		"event_1",
+		"event_2",
+	},
+	.function = {
+		{       state_b_test_da_kunit,       state_a_test_da_kunit },
+		{               INVALID_STATE,       state_a_test_da_kunit },
+	},
+	.initial_state = state_a_test_da_kunit,
+	.final_states = { 1, 0 },
+};

tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_da_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_DA_KUNIT)
+
+static void rv_test_test_da_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_da_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_da_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_da_kunit rv_test_stub
+#endif

tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h

@@ -0,0 +1,23 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_DA_KUNIT_KUNIT_H
+#define __TEST_DA_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_da_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_event_1)(void *data, /* XXX: fill header */);
+	void (*handle_event_2)(void *data, /* XXX: fill header */);
+} rv_test_da_kunit_ops;
+#endif
+
+#endif /* __TEST_DA_KUNIT_KUNIT_H */

tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h

@@ -0,0 +1,15 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_DA_KUNIT
+DEFINE_EVENT(event_da_monitor, event_test_da_kunit,
+	     TP_PROTO(char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor, error_test_da_kunit,
+	     TP_PROTO(char *state, char *event),
+	     TP_ARGS(state, event));
+#endif /* CONFIG_RV_MON_TEST_DA_KUNIT */

tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_HA_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select HA_MON_EVENTS_ID
+	bool "test_ha_kunit monitor"
+	help
+	  auto-generated

tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c

@@ -0,0 +1,243 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ha_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#define RV_MON_TYPE RV_MON_PER_TASK
+/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */
+#define HA_TIMER_TYPE HA_TIMER_HRTIMER
+#include "test_ha_kunit.h"
+#include <rv/ha_monitor.h>
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */
+
+#define FOO_NS /* XXX: what is FOO_NS? */
+
+static inline u64 bar_ns(struct ha_monitor *ha_mon)
+{
+	return /* XXX: what is bar_ns(ha_mon)? */;
+}
+
+static u64 foo_ns = /* XXX: default value */;
+module_param(foo_ns, ullong, 0644);
+
+/*
+ * These functions define how to read and reset the environment variable.
+ *
+ * Common environment variables like ns-based and jiffy-based clocks have
+ * pre-define getters and resetters you can use. The parser can infer the type
+ * of the environment variable if you supply a measure unit in the constraint.
+ * If you define your own functions, make sure to add appropriate memory
+ * barriers if required.
+ * Some environment variables don't require a storage as they read a system
+ * state (e.g. preemption count). Those variables are never reset, so we don't
+ * define a reset function on monitors only relying on this type of variables.
+ */
+static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
+{
+	if (env == clk_test_ha_kunit)
+		return ha_get_clk_ns(ha_mon, env, time_ns);
+	else if (env == env1_test_ha_kunit)
+		return /* XXX: how do I read env1? */
+	else if (env == env2_test_ha_kunit)
+		return /* XXX: how do I read env2? */
+	return ENV_INVALID_VALUE;
+}
+
+static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns)
+{
+	if (env == clk_test_ha_kunit)
+		ha_reset_clk_ns(ha_mon, env, time_ns);
+}
+
+/*
+ * These functions are used to validate state transitions.
+ *
+ * They are generated by parsing the model, there is usually no need to change them.
+ * If the monitor requires a timer, there are functions responsible to arm it when
+ * the next state has a constraint, cancel it in any other case and to check
+ * that it didn't expire before the callback run. Transitions to the same state
+ * without a reset never affect timers.
+ */
+static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
+					enum states curr_state, enum events event,
+					enum states next_state, u64 time_ns)
+{
+	if (curr_state == S0_test_ha_kunit)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, bar_ns(ha_mon));
+	else if (curr_state == S2_test_ha_kunit)
+		return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, BAR_NS(ha_mon));
+	return true;
+}
+
+static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
+				    enum states curr_state, enum events event,
+				    enum states next_state, u64 time_ns)
+{
+	bool res = true;
+
+	if (curr_state == S0_test_ha_kunit && event == event0_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S0_test_ha_kunit && event == event1_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S1_test_ha_kunit && event == event0_test_ha_kunit)
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	else if (curr_state == S1_test_ha_kunit && event == event2_test_ha_kunit) {
+		res = ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 0ull;
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	} else if (curr_state == S2_test_ha_kunit && event == event1_test_ha_kunit)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < foo_ns;
+	else if (curr_state == S3_test_ha_kunit && event == event0_test_ha_kunit)
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < FOO_NS &&
+		      ha_get_env(ha_mon, env2_test_ha_kunit, time_ns) == 0ull);
+	else if (curr_state == S3_test_ha_kunit && event == event1_test_ha_kunit) {
+		res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) ||
+		      (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < 5000ull &&
+		      ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 1ull);
+		ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns);
+	}
+	return res;
+}
+
+static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
+				       enum states curr_state, enum events event,
+				       enum states next_state, u64 time_ns)
+{
+	if (next_state == curr_state && event != event0_test_ha_kunit)
+		return;
+	if (next_state == S0_test_ha_kunit)
+		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, bar_ns(ha_mon), time_ns);
+	else if (next_state == S2_test_ha_kunit)
+		ha_start_timer_ns(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns);
+	else if (curr_state == S0_test_ha_kunit)
+		ha_cancel_timer(ha_mon);
+	else if (curr_state == S2_test_ha_kunit)
+		ha_cancel_timer(ha_mon);
+}
+
+static bool ha_verify_constraint(struct ha_monitor *ha_mon,
+				 enum states curr_state, enum events event,
+				 enum states next_state, u64 time_ns)
+{
+	if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
+		return false;
+
+	ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);
+
+	return true;
+}
+
+static void handle_event0(void *data, /* XXX: fill header */)
+{
+	/* XXX: validate that this event always leads to the initial state */
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_start_event(p, event0_test_ha_kunit);
+}
+
+static void handle_event1(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event1_test_ha_kunit);
+}
+
+static void handle_event2(void *data, /* XXX: fill header */)
+{
+	struct task_struct *p = /* XXX: how do I get p? */;
+	da_handle_event(p, event2_test_ha_kunit);
+}
+
+static int enable_test_ha_kunit(void)
+{
+	int retval;
+
+	retval = ha_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
+	rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
+
+	return 0;
+}
+
+static void disable_test_ha_kunit(void)
+{
+	rv_this.enabled = 0;
+
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0);
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1);
+	rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2);
+
+	ha_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ha_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_ha_kunit,
+	.disable = disable_test_ha_kunit,
+	.reset = da_monitor_reset_all,
+	.enabled = 0,
+};
+
+static int __init register_test_ha_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_ha_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ha_kunit);
+module_exit(unregister_test_ha_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ha_kunit: auto-generated");
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+#include <kunit/visibility.h>
+#include "test_ha_kunit_kunit.h"
+
+const struct rv_test_ha_kunit_ops rv_test_ha_kunit_ops = {
+	.mon = RV_MON_OPS_INIT(),
+	.handle_event0 = handle_event0,
+	.handle_event1 = handle_event1,
+	.handle_event2 = handle_event2,
+};
+EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops);
+#endif

tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h

@@ -0,0 +1,88 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Automatically generated C representation of test_ha_kunit automaton
+ * For further information about this format, see kernel documentation:
+ *   Documentation/trace/rv/deterministic_automata.rst
+ */
+
+#define MONITOR_NAME test_ha_kunit
+
+enum states_test_ha_kunit {
+	S0_test_ha_kunit,
+	S1_test_ha_kunit,
+	S2_test_ha_kunit,
+	S3_test_ha_kunit,
+	state_max_test_ha_kunit,
+};
+
+#define INVALID_STATE state_max_test_ha_kunit
+
+enum events_test_ha_kunit {
+	event0_test_ha_kunit,
+	event1_test_ha_kunit,
+	event2_test_ha_kunit,
+	event_max_test_ha_kunit,
+};
+
+enum envs_test_ha_kunit {
+	clk_test_ha_kunit,
+	env1_test_ha_kunit,
+	env2_test_ha_kunit,
+	env_max_test_ha_kunit,
+	env_max_stored_test_ha_kunit = env1_test_ha_kunit,
+};
+
+_Static_assert(env_max_stored_test_ha_kunit <= MAX_HA_ENV_LEN, "Not enough slots");
+#define HA_CLK_NS
+
+struct automaton_test_ha_kunit {
+	char *state_names[state_max_test_ha_kunit];
+	char *event_names[event_max_test_ha_kunit];
+	char *env_names[env_max_test_ha_kunit];
+	unsigned char function[state_max_test_ha_kunit][event_max_test_ha_kunit];
+	unsigned char initial_state;
+	bool final_states[state_max_test_ha_kunit];
+};
+
+static const struct automaton_test_ha_kunit automaton_test_ha_kunit = {
+	.state_names = {
+		"S0",
+		"S1",
+		"S2",
+		"S3",
+	},
+	.event_names = {
+		"event0",
+		"event1",
+		"event2",
+	},
+	.env_names = {
+		"clk",
+		"env1",
+		"env2",
+	},
+	.function = {
+		{
+			S0_test_ha_kunit,
+			S1_test_ha_kunit,
+			INVALID_STATE,
+		},
+		{
+			S0_test_ha_kunit,
+			INVALID_STATE,
+			S2_test_ha_kunit,
+		},
+		{
+			INVALID_STATE,
+			S2_test_ha_kunit,
+			S3_test_ha_kunit,
+		},
+		{
+			S0_test_ha_kunit,
+			S1_test_ha_kunit,
+			INVALID_STATE,
+		},
+	},
+	.initial_state = S0_test_ha_kunit,
+	.final_states = { 1, 0, 0, 0 },
+};

tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_ha_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_HA_KUNIT)
+
+static void rv_test_test_ha_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_ha_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_ha_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_ha_kunit rv_test_stub
+#endif

tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h

@@ -0,0 +1,24 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_HA_KUNIT_KUNIT_H
+#define __TEST_HA_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_ha_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_event0)(void *data, /* XXX: fill header */);
+	void (*handle_event1)(void *data, /* XXX: fill header */);
+	void (*handle_event2)(void *data, /* XXX: fill header */);
+} rv_test_ha_kunit_ops;
+#endif
+
+#endif /* __TEST_HA_KUNIT_KUNIT_H */

tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h

@@ -0,0 +1,19 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_HA_KUNIT
+DEFINE_EVENT(event_da_monitor_id, event_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state),
+	     TP_ARGS(id, state, event, next_state, final_state));
+
+DEFINE_EVENT(error_da_monitor_id, error_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event),
+	     TP_ARGS(id, state, event));
+
+DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha_kunit,
+	     TP_PROTO(int id, char *state, char *event, char *env),
+	     TP_ARGS(id, state, event, env));
+#endif /* CONFIG_RV_MON_TEST_HA_KUNIT */

tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: GPL-2.0-only
+#
+config RV_MON_TEST_LTL_KUNIT
+	depends on RV
+	# XXX: add dependencies if there
+	select LTL_MON_EVENTS_ID
+	bool "test_ltl_kunit monitor"
+	help
+	  auto-generated

tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c

@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+
+#define MODULE_NAME "test_ltl_kunit"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <rv_trace.h>
+
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "test_ltl_kunit.h"
+#include <rv/ltl_monitor.h>
+
+static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon)
+{
+	/*
+	 * This is called everytime the Buchi automaton is triggered.
+	 *
+	 * This function could be used to fetch the atomic propositions which
+	 * are expensive to trace. It is possible only if the atomic proposition
+	 * does not need to be updated at precise time.
+	 *
+	 * It is recommended to use tracepoints and ltl_atom_update() instead.
+	 */
+}
+
+static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation)
+{
+	/*
+	 * This should initialize as many atomic propositions as possible.
+	 *
+	 * @task_creation indicates whether the task is being created. This is
+	 * false if the task is already running before the monitor is enabled.
+	 */
+	ltl_atom_set(mon, LTL_EVENT_A, true/false);
+	ltl_atom_set(mon, LTL_EVENT_B, true/false);
+}
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ */
+static void handle_example_event(void *data, /* XXX: fill header */)
+{
+	ltl_atom_update(task, LTL_EVENT_A, true/false);
+}
+
+static int enable_test_ltl_kunit(void)
+{
+	int retval;
+
+	retval = ltl_monitor_init();
+	if (retval)
+		return retval;
+
+	rv_attach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	return 0;
+}
+
+static void disable_test_ltl_kunit(void)
+{
+	rv_detach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event);
+
+	ltl_monitor_destroy();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_this = {
+	.name = "test_ltl_kunit",
+	.description = "auto-generated",
+	.enable = enable_test_ltl_kunit,
+	.disable = disable_test_ltl_kunit,
+};
+
+static int __init register_test_ltl_kunit(void)
+{
+	return rv_register_monitor(&rv_this, NULL);
+}
+
+static void __exit unregister_test_ltl_kunit(void)
+{
+	rv_unregister_monitor(&rv_this);
+}
+
+module_init(register_test_ltl_kunit);
+module_exit(unregister_test_ltl_kunit);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("rvgen: auto-generated");
+MODULE_DESCRIPTION("test_ltl_kunit: auto-generated");

tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h

@@ -0,0 +1,108 @@
+/* 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 test_ltl_kunit
+
+enum ltl_atom {
+	LTL_EVENT_A,
+	LTL_EVENT_B,
+	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[] = {
+		"ev_a",
+		"ev_b",
+	};
+
+	return names[atom];
+}
+
+enum ltl_buchi_state {
+	S0,
+	S1,
+	S2,
+	S3,
+	S4,
+	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 event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	if (val1)
+		__set_bit(S0, mon->states);
+	if (true)
+		__set_bit(S1, mon->states);
+	if (event_b)
+		__set_bit(S4, mon->states);
+}
+
+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool event_b = test_bit(LTL_EVENT_B, mon->atoms);
+	bool event_a = test_bit(LTL_EVENT_A, mon->atoms);
+	bool val1 = !event_a;
+
+	switch (state) {
+	case S0:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S1:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S2:
+		if (true)
+			__set_bit(S1, next);
+		if (true && val1)
+			__set_bit(S2, next);
+		if (event_b && val1)
+			__set_bit(S3, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S3:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	case S4:
+		if (val1)
+			__set_bit(S0, next);
+		if (true)
+			__set_bit(S1, next);
+		if (event_b)
+			__set_bit(S4, next);
+		break;
+	}
+}

tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/kernel.h>
+#include <linux/rv.h>
+#include <rv/kunit.h>
+/*
+ * XXX: include required headers, e.g.,
+ * #include <linux/sched.h>
+ */
+#include "test_ltl_kunit_kunit.h"
+
+#if IS_REACHABLE(CONFIG_RV_MON_TEST_LTL_KUNIT)
+
+static void rv_test_test_ltl_kunit(struct kunit *test)
+{
+	struct rv_kunit_ctx *ctx = test->priv;
+	/*
+	 * If you need to create task_structs with rv_kunit_alloc_mock_task()
+	 * do it BEFORE preparing the test.
+	 */
+
+	prepare_test(test, &rv_test_ltl_kunit_ops.mon);
+
+	/*
+	 * XXX: write the test here
+	 * e.g.
+	 * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx)
+	 *	rv_test_ltl_kunit_ops.handle_event(args);
+	 */
+}
+
+#else
+#define rv_test_test_ltl_kunit rv_test_stub
+#endif

tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h

@@ -0,0 +1,22 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Automatically generated by rvgen kunit.
+ * May need manual intervention for function prototypes that couldn't be
+ * found (e.g. are in another file) or variables to be exported.
+ */
+
+#ifndef __TEST_LTL_KUNIT_KUNIT_H
+#define __TEST_LTL_KUNIT_KUNIT_H
+
+#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST)
+
+#include <linux/rv.h>
+#include <rv/kunit.h>
+
+extern const struct rv_test_ltl_kunit_ops {
+	struct rv_kunit_mon mon;
+	void (*handle_example_event)(void *data, /* XXX: fill header */);
+} rv_test_ltl_kunit_ops;
+#endif
+
+#endif /* __TEST_LTL_KUNIT_KUNIT_H */

tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h

@@ -0,0 +1,14 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+/*
+ * Snippet to be included in rv_trace.h
+ */
+
+#ifdef CONFIG_RV_MON_TEST_LTL_KUNIT
+DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl_kunit,
+	     TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next),
+	     TP_ARGS(task, states, atoms, next));
+DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl_kunit,
+	     TP_PROTO(struct task_struct *task),
+	     TP_ARGS(task));
+#endif /* CONFIG_RV_MON_TEST_LTL_KUNIT */

tools/verification/rvgen/tests/rvgen_kunit.t

@@ -0,0 +1,41 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+source ../tests/engine.sh
+test_begin
+
+set_timeout 30s
+
+# Help tests
+check "verify kunit subcommand help" \
+	"$RVGEN kunit -h" 0 "model_name" "spec"
+
+check_and_compare_folder "KUnit generation with local lookup and test_da_kunit" \
+	"$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu -n test_da_kunit && $RVGEN kunit -a -l -n test_da_kunit" \
+	"test_da_kunit" "Now complete the test and add it to rv_monitors_test.c" "RV_MON_OPS_INIT"
+
+check_and_compare_folder "KUnit generation with local lookup and test_ha_kunit" \
+	"$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task -n test_ha_kunit && $RVGEN kunit -a -l -n test_ha_kunit" \
+	"test_ha_kunit" "Successfully created KUnit" "Append the following to"
+
+check_and_compare_folder "KUnit generation with local lookup and test_ltl_kunit" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_ltl_kunit && $RVGEN kunit -l -n test_ltl_kunit" \
+	"test_ltl_kunit" "RV_MON_OPS_INIT"
+
+check_and_compare_folder "KUnit generation with backup file" \
+	"$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_bak_kunit && echo DUMMY > test_bak_kunit/test_bak_kunit_kunit.c && $RVGEN kunit -l -n test_bak_kunit" \
+	"test_bak_kunit" "KUnit file(s) already exist.*backing up existing files"
+
+# Error handling tests
+check "missing required model_name" \
+	"$RVGEN kunit" 2 "the following arguments are required: -n/--model_name"
+
+check "non-existent model_name with auto_patch" \
+	"$RVGEN kunit -a -n nonexistent" 1 \
+	"Could not find monitor C file" "Traceback (most recent call last)"
+
+check "monitor without handlers" \
+	"mkdir -p nohandler ; echo DUMMY > nohandler/nohandler.c ; $RVGEN kunit -l -n nohandler" 1 \
+	"No handlers found" "Traceback (most recent call last)"
+rm -rf nohandler
+
+test_end