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. Signed-off-by: Gabriele Monaco <[email protected]> --- .../rvgen/rvgen/templates/kunit.c | 2 +- .../rvgen/tests/golden/test_da_kunit/Kconfig | 9 + .../golden/test_da_kunit/test_da_kunit.c | 111 ++++++++ .../golden/test_da_kunit/test_da_kunit.h | 47 ++++ .../test_da_kunit/test_da_kunit_kunit.c | 29 ++ .../test_da_kunit/test_da_kunit_kunit.h | 23 ++ .../test_da_kunit/test_da_kunit_trace.h | 15 + .../rvgen/tests/golden/test_ha_kunit/Kconfig | 9 + .../golden/test_ha_kunit/test_ha_kunit.c | 264 ++++++++++++++++++ .../golden/test_ha_kunit/test_ha_kunit.h | 88 ++++++ .../test_ha_kunit/test_ha_kunit_kunit.c | 29 ++ .../test_ha_kunit/test_ha_kunit_kunit.h | 24 ++ .../test_ha_kunit/test_ha_kunit_trace.h | 19 ++ .../rvgen/tests/golden/test_ltl_kunit/Kconfig | 9 + .../golden/test_ltl_kunit/test_ltl_kunit.c | 107 +++++++ .../golden/test_ltl_kunit/test_ltl_kunit.h | 108 +++++++ .../test_ltl_kunit/test_ltl_kunit_kunit.c | 29 ++ .../test_ltl_kunit/test_ltl_kunit_kunit.h | 22 ++ .../test_ltl_kunit/test_ltl_kunit_trace.h | 14 + tools/verification/rvgen/tests/rvgen_kunit.t | 32 +++ 20 files changed, 989 insertions(+), 1 deletion(-) create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h create mode 100644 tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h create mode 100644 tools/verification/rvgen/tests/rvgen_kunit.t diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c index d29bbf2ea5..402b5c8575 100644 --- a/tools/verification/rvgen/rvgen/templates/kunit.c +++ b/tools/verification/rvgen/rvgen/templates/kunit.c @@ -8,7 +8,7 @@ */ #include "%%MODEL_NAME%%_kunit.h" -#if IS_ENABLED(CONFIG_RV_MON_%%MODEL_NAME_UP%%) +#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%) static void rv_test_%%MODEL_NAME%%(struct kunit *test) { diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig new file mode 100644 index 0000000000..6d664ba562 --- /dev/null +++ b/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 diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c new file mode 100644 index 0000000000..c2916c3e86 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c @@ -0,0 +1,111 @@ +// 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("dot2k: 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_this = &rv_this, + .monitor_init = da_monitor_init, + .monitor_destroy = da_monitor_destroy, + }, + .handle_event_1 = handle_event_1, + .handle_event_2 = handle_event_2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h new file mode 100644 index 0000000000..290a9454ca --- /dev/null +++ b/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 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c new file mode 100644 index 0000000000..06a280444b --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c @@ -0,0 +1,29 @@ +// 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; + + 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 diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h new file mode 100644 index 0000000000..0094215ff4 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h new file mode 100644 index 0000000000..16804a79e8 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig new file mode 100644 index 0000000000..6c48770ace --- /dev/null +++ b/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 diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c new file mode 100644 index 0000000000..69ca870ac2 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c @@ -0,0 +1,264 @@ +// 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. + * Due to the different representations between invariants and guards, there is + * a function to convert it in case invariants or guards are reachable from + * another invariant without reset. Those are not present if not required in + * the model. This is all automatic but is worth checking because it may show + * errors in the model (e.g. missing resets). + */ +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); + else if (curr_state == S2_test_ha_kunit) + return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns); + return true; +} + +static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == next_state) + return; + if (curr_state == S2_test_ha_kunit) + ha_inv_to_guard(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns); +} + +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; + + ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns); + + 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("dot2k: 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_this = &rv_this, + .monitor_init = ha_monitor_init, + .monitor_destroy = ha_monitor_destroy, + }, + .handle_event0 = handle_event0, + .handle_event1 = handle_event1, + .handle_event2 = handle_event2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h new file mode 100644 index 0000000000..5c428f818b --- /dev/null +++ b/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 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c new file mode 100644 index 0000000000..730a9a26a0 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c @@ -0,0 +1,29 @@ +// 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; + + 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 diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h new file mode 100644 index 0000000000..0b2030cb64 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h new file mode 100644 index 0000000000..6c13ee0068 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig new file mode 100644 index 0000000000..3e334c3442 --- /dev/null +++ b/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 diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c new file mode 100644 index 0000000000..5e95a0f462 --- /dev/null +++ b/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_sample_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(/* TODO */); +MODULE_DESCRIPTION("test_ltl_kunit: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h new file mode 100644 index 0000000000..acc503b56e --- /dev/null +++ b/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; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c new file mode 100644 index 0000000000..f64faef1b0 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c @@ -0,0 +1,29 @@ +// 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; + + 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 diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h new file mode 100644 index 0000000000..b2ca34be32 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h new file mode 100644 index 0000000000..a054d5b2c0 --- /dev/null +++ b/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 */ diff --git a/tools/verification/rvgen/tests/rvgen_kunit.t b/tools/verification/rvgen/tests/rvgen_kunit.t new file mode 100644 index 0000000000..174a6fac0b --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_kunit.t @@ -0,0 +1,32 @@ +#!/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" "monitor_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" "monitor_init = ltl_monitor_init" + +# 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)" + +test_end -- 2.54.0
