Add selftest cases for BPF monitors generation. Signed-off-by: Gabriele Monaco --- .../tests/golden/da_bpf_cpu/da_bpf_cpu.c | 35 +++++++++++++ .../tests/golden/da_bpf_cpu/da_bpf_cpu.h | 47 ++++++++++++++++++ .../tests/golden/da_bpf_obj/da_bpf_obj.c | 49 +++++++++++++++++++ .../tests/golden/da_bpf_obj/da_bpf_obj.h | 47 ++++++++++++++++++ .../verification/rvgen/tests/rvgen_monitor.t | 11 +++++ 5 files changed, 189 insertions(+) create mode 100644 tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.c create mode 100644 tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.h create mode 100644 tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.c create mode 100644 tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.h diff --git a/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.c b/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.c new file mode 100644 index 000000000000..5a652ce9b461 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.c @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: GPL-2.0 + +#include "vmlinux.h" + +#define RV_MON_TYPE RV_MON_PER_CPU +#include "da_bpf_cpu.h" +#include + +/* + * 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. + */ +SEC(/* XXX: tracepoint or other probe */) +int BPF_PROG(handle_event_1, /* XXX: fill header */) +{ + da_handle_event(event_1_da_bpf_cpu); + return 0; +} + +SEC(/* XXX: tracepoint or other probe */) +int BPF_PROG(handle_event_2, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_da_bpf_cpu); + return 0; +} + +static struct rv_monitor rv_this = { + .enabled = 0, +}; + +char LICENSE[] SEC("license") = "GPL"; +char DESCRIPTION[] SEC(".rodata.description") = "auto-generated"; diff --git a/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.h b/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.h new file mode 100644 index 000000000000..fd8125118d81 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_bpf_cpu automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_bpf_cpu + +enum states_da_bpf_cpu { + state_a_da_bpf_cpu, + state_b_da_bpf_cpu, + state_max_da_bpf_cpu, +}; + +#define INVALID_STATE state_max_da_bpf_cpu + +enum events_da_bpf_cpu { + event_1_da_bpf_cpu, + event_2_da_bpf_cpu, + event_max_da_bpf_cpu, +}; + +struct automaton_da_bpf_cpu { + char state_names[state_max_da_bpf_cpu][32]; + char event_names[event_max_da_bpf_cpu][32]; + unsigned char function[state_max_da_bpf_cpu][event_max_da_bpf_cpu]; + unsigned char initial_state; + bool final_states[state_max_da_bpf_cpu]; +}; + +static const struct automaton_da_bpf_cpu automaton_da_bpf_cpu = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_da_bpf_cpu, state_a_da_bpf_cpu }, + { INVALID_STATE, state_a_da_bpf_cpu }, + }, + .initial_state = state_a_da_bpf_cpu, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.c b/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.c new file mode 100644 index 000000000000..a7d465f84f05 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.c @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: GPL-2.0 + +#include "vmlinux.h" + +#define RV_MON_TYPE RV_MON_PER_OBJ +typedef /* XXX: define the target type */ *monitor_target_bpf; +#include "da_bpf_obj.h" +#include + +/* + * 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. + */ +SEC(/* XXX: tracepoint or other probe */) +int BPF_PROG(handle_event_1, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + monitor_target_bpf t = /* XXX: how do I get t? */; + da_handle_event(id, t, event_1_da_bpf_obj); + return 0; +} + +SEC(/* XXX: tracepoint or other probe */) +int BPF_PROG(handle_event_2, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + int id = /* XXX: how do I get the id? */; + monitor_target_bpf t = /* XXX: how do I get t? */; + da_handle_start_event(id, t, event_2_da_bpf_obj); + return 0; +} + +/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */ +SEC(/* XXX: tracepoint or other probe */) +int BPF_PROG(handle_obj_cleanup, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + da_destroy_storage(id); + return 0; +} + +static struct rv_monitor rv_this = { + .enabled = 0, +}; + +char LICENSE[] SEC("license") = "GPL"; +char DESCRIPTION[] SEC(".rodata.description") = "auto-generated"; diff --git a/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.h b/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.h new file mode 100644 index 000000000000..385006098049 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_bpf_obj automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_bpf_obj + +enum states_da_bpf_obj { + state_a_da_bpf_obj, + state_b_da_bpf_obj, + state_max_da_bpf_obj, +}; + +#define INVALID_STATE state_max_da_bpf_obj + +enum events_da_bpf_obj { + event_1_da_bpf_obj, + event_2_da_bpf_obj, + event_max_da_bpf_obj, +}; + +struct automaton_da_bpf_obj { + char state_names[state_max_da_bpf_obj][32]; + char event_names[event_max_da_bpf_obj][32]; + unsigned char function[state_max_da_bpf_obj][event_max_da_bpf_obj]; + unsigned char initial_state; + bool final_states[state_max_da_bpf_obj]; +}; + +static const struct automaton_da_bpf_obj automaton_da_bpf_obj = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_da_bpf_obj, state_a_da_bpf_obj }, + { INVALID_STATE, state_a_da_bpf_obj }, + }, + .initial_state = state_a_da_bpf_obj, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/rvgen_monitor.t b/tools/verification/rvgen/tests/rvgen_monitor.t index 5f2562600bad..3d71685a7ad5 100644 --- a/tools/verification/rvgen/tests/rvgen_monitor.t +++ b/tools/verification/rvgen/tests/rvgen_monitor.t @@ -47,6 +47,17 @@ check_and_compare_folder "LTL per_task with parent and description (default name "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -p ltl_parent -D 'Simple description'" \ "test_ltl" "LTL_MON_EVENTS_ID" +# BPF monitor test +check_and_compare_folder "DA BPF per_cpu" \ + "$RVGEN monitor -b -c da -s tests/specs/test_da.dot -t per_cpu -n da_bpf_cpu" \ + "da_bpf_cpu" "Edit the da_bpf_cpu/da_bpf_cpu.c to add the instrumentation" \ + "Edit kernel/trace/rv/Makefile" + +check_and_compare_folder "DA BPF per_obj" \ + "$RVGEN monitor -b -c da -s tests/specs/test_da.dot -t per_obj -n da_bpf_obj" \ + "da_bpf_obj" "Edit the da_bpf_obj/da_bpf_obj.c to add the instrumentation" \ + "Edit kernel/trace/rv/Kconfig" + # Error handling tests check "missing required spec argument" \ "$RVGEN monitor -c da -t per_cpu" 2 \ -- 2.55.0