Add selftest cases for BPF monitors generation.
Signed-off-by: Gabriele Monaco <[email protected]>
---
.../tests/golden/da_bpf_cpu/da_bpf_cpu.c | 40 ++++++++++++++
.../tests/golden/da_bpf_cpu/da_bpf_cpu.h | 47 ++++++++++++++++
.../tests/golden/da_bpf_obj/da_bpf_obj.c | 54 +++++++++++++++++++
.../tests/golden/da_bpf_obj/da_bpf_obj.h | 47 ++++++++++++++++
.../verification/rvgen/tests/rvgen_monitor.t | 11 ++++
5 files changed, 199 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..37659b2ebce2
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_bpf_cpu/da_bpf_cpu.c
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include "vmlinux.h"
+
+#define RV_MON_TYPE RV_MON_PER_CPU
+#include "da_bpf_cpu.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.
+ */
+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;
+}
+
+SEC(".struct_ops.link")
+struct rv_monitor rv_da_bpf_cpu_kern = {
+ .name = "da_bpf_cpu",
+ .description = "auto-generated",
+ .enable = da_monitor_enable_bpf,
+ .disable = da_monitor_disable_bpf,
+ .reset = da_monitor_reset_bpf,
+ .enabled = 0,
+};
+
+char LICENSE[] SEC("license") = "GPL";
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..bbd46615a1a5
--- /dev/null
+++ b/tools/verification/rvgen/tests/golden/da_bpf_obj/da_bpf_obj.c
@@ -0,0 +1,54 @@
+// 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 <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.
+ */
+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;
+}
+
+SEC(".struct_ops.link")
+struct rv_monitor rv_da_bpf_obj_kern = {
+ .name = "da_bpf_obj",
+ .description = "auto-generated",
+ .enable = da_monitor_enable_bpf,
+ .disable = da_monitor_disable_bpf,
+ .reset = da_monitor_reset_bpf,
+ .enabled = 0,
+};
+
+char LICENSE[] SEC("license") = "GPL";
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
