[PATCH v2 13/15] verification/rvgen: Add support for BPF monitors

[Gabriele Monaco <gmonaco@redhat.com>]

Add the -b flag to rvgen monitor to generate a bpf monitor.
By default the code is generated in a folder with the same name as the
model just like in-kernel monitors, although only the source and header
are meaningful here. Passing -a moves the sources to
tools/verification/rv/bpf_monitors/ where they can be built directly.

Currently BPF monitors are only supported for DA.

Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/__main__.py          | 15 ++++++++---
 tools/verification/rvgen/rvgen/dot2c.py       | 15 ++++++++---
 tools/verification/rvgen/rvgen/dot2k.py       | 22 +++++++++++++---
 tools/verification/rvgen/rvgen/generator.py   | 26 ++++++++++++++-----
 .../rvgen/rvgen/templates/dot2k/main_bpf.c    | 21 +++++++++++++++
 5 files changed, 80 insertions(+), 19 deletions(-)
 create mode 100644 tools/verification/rvgen/rvgen/templates/dot2k/main_bpf.c

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 246b43fa29f1..16ce9b512fbb 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -39,6 +39,8 @@ if __name__ == '__main__':
                                 help="Monitor specification file")
     monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True,
                                 help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
+    monitor_parser.add_argument('-b', "--bpf", dest="bpf", action="store_true",
+                                required=False, help="Generate a BPF monitor")
 
     container_parser = subparsers.add_parser("container", parents=[parent_parser])
     container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
@@ -50,6 +52,9 @@ if __name__ == '__main__':
 
     params = parser.parse_args()
 
+    if params.subcmd == "monitor" and params.bpf and params.monitor_class != "da":
+        parser.error("BPF monitors (-b/--bpf) are only supported for deterministic automaton (-c da)")
+
     try:
         if params.subcmd == "monitor":
             print(f"Opening and parsing the specification file {params.spec}")
@@ -80,7 +85,9 @@ if __name__ == '__main__':
     print("Almost done, checklist")
     if params.subcmd == "monitor":
         print(f"  - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation")
-        print(monitor.fill_tracepoint_tooltip())
-    print(monitor.fill_makefile_tooltip())
-    print(monitor.fill_kconfig_tooltip())
-    print(monitor.fill_monitor_tooltip())
+        if not params.bpf:
+            print(monitor.fill_tracepoint_tooltip())
+    if not params.subcmd == "monitor" or not params.bpf:
+        print(monitor.fill_makefile_tooltip())
+        print(monitor.fill_kconfig_tooltip())
+        print(monitor.fill_monitor_tooltip())
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 22938ce1bf6c..5be9fe44a19b 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -111,10 +111,17 @@ class Dot2c(Automata):
         min_type = self.get_minimun_type()
         buff = []
         buff.append(f"struct {self.struct_automaton_def} {{")
-        buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
-        buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
-        if self.is_hybrid_automata():
-            buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
+        if self.bpf:
+            # BPF struggles with non-fixed string pointers
+            buff.append(f"\tchar state_names[state_max{self.enum_suffix}][32];")
+            buff.append(f"\tchar event_names[event_max{self.enum_suffix}][32];")
+            if self.is_hybrid_automata():
+                buff.append(f"\tchar env_names[env_max{self.enum_suffix}][32];")
+        else:
+            buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
+            buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
+            if self.is_hybrid_automata():
+                buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
         buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];")
         buff.append(f"\t{min_type} initial_state;")
         buff.append(f"\tbool final_states[state_max{self.enum_suffix}];")
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index fd3254ea5b4d..6600bfa0f20f 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -30,14 +30,19 @@ class dot2k(Monitor, Dot2c):
         buff = [ self.monitor_type.upper() ]
         buff += self._fill_timer_type()
         if self.monitor_type == "per_obj":
-            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
+            pad = "_bpf" if self.bpf else ""
+            buff.append(f"typedef /* XXX: define the target type */ *monitor_target{pad};")
         return "\n".join(buff)
 
     def fill_tracepoint_handlers_skel(self) -> str:
         buff = []
         buff += self._fill_hybrid_definitions()
         for event in self.events:
-            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
+            if self.bpf:
+                buff.append("SEC(/* XXX: tracepoint or other probe */)")
+                buff.append(f"int BPF_PROG(handle_{event}, /* XXX: fill header */)")
+            else:
+                buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
             buff.append("{")
             handle = "handle_event"
             if self.is_start_event(event):
@@ -50,19 +55,28 @@ class dot2k(Monitor, Dot2c):
                 buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
                 buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
             elif self.monitor_type == "per_obj":
+                pad = "_bpf" if self.bpf else ""
                 buff.append("\tint id = /* XXX: how do I get the id? */;")
-                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
+                buff.append(f"\tmonitor_target{pad} t = /* XXX: how do I get t? */;")
                 buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
             else:
                 buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
+            if self.bpf:
+                buff.append("\treturn 0;")
             buff.append("}")
             buff.append("")
         if self.monitor_type == "per_obj":
             buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */")
-            buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)")
+            if self.bpf:
+                buff.append("SEC(/* XXX: tracepoint or other probe */)")
+                buff.append(f"int BPF_PROG(handle_{self.cleanup_marker}, /* XXX: fill header */)")
+            else:
+                buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)")
             buff.append("{")
             buff.append("\tint id = /* XXX: how do I get the id? */;")
             buff.append("\tda_destroy_storage(id);")
+            if self.bpf:
+                buff.append("\treturn 0;")
             buff.append("}")
             buff.append("")
         return '\n'.join(buff)
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 45e2bab26cb5..b7985ff84521 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -11,18 +11,22 @@ from pathlib import Path
 
 class RVGenerator:
     rv_dir = "kernel/trace/rv"
+    rv_tool_dir = "../../../tools/verification/rv/bpf_monitors/"
 
     def __init__(self, extra_params={}):
         self.name = extra_params.get("model_name")
         self.parent = extra_params.get("parent")
+        self.bpf = extra_params.get("bpf")
         self.abs_template_dir = \
             Path(__file__).resolve().parent / "templates" / self.template_dir
-        self.main_c = self._read_template_file("main.c")
+        self.main_c = self._read_template_file("main.c" if not self.bpf
+                                               else "main_bpf.c")
         self.kconfig = self._read_template_file("Kconfig")
         self.description = extra_params.get("description", self.name) or "auto-generated"
         self.auto_patch = extra_params.get("auto_patch")
         if self.auto_patch:
             self._fill_rv_kernel_dir()
+            self.rv_tool_dir = (Path(self.rv_dir) / self.rv_tool_dir).resolve()
 
     def _fill_rv_kernel_dir(self):
         # find the kernel tree root relative to this file's location
@@ -191,6 +195,9 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
     def __create_directory(self):
         path = Path(self.name)
         if self.auto_patch:
+            if self.bpf:
+                # no directory for BPF monitors
+                return
             path = Path(self.rv_dir) / "monitors" / path
         path.mkdir(exist_ok=True)
 
@@ -202,6 +209,8 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
         path = Path(self.name) / file_name
         if self.auto_patch:
             path = Path(self.rv_dir) / "monitors" / self.name / file_name
+            if self.bpf:
+                path = Path(self.rv_tool_dir) / file_name
         self.__write_file(path, content)
 
     def print_files(self):
@@ -216,8 +225,9 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
         path = f"{self.name}.h"
         self._create_file(path, model_h)
 
-        kconfig = self.fill_kconfig()
-        self._create_file("Kconfig", kconfig)
+        if not self.bpf:
+            kconfig = self.fill_kconfig()
+            self._create_file("Kconfig", kconfig)
 
 
 class Monitor(RVGenerator):
@@ -225,7 +235,8 @@ class Monitor(RVGenerator):
 
     def __init__(self, extra_params={}):
         super().__init__(extra_params)
-        self.trace_h = self._read_template_file("trace.h")
+        if not self.bpf:
+            self.trace_h = self._read_template_file("trace.h")
 
     def fill_trace_h(self):
         trace_h = self.trace_h
@@ -245,6 +256,7 @@ class Monitor(RVGenerator):
 
     def print_files(self):
         super().print_files()
-        trace_h = self.fill_trace_h()
-        path = f"{self.name}_trace.h"
-        self._create_file(path, trace_h)
+        if not self.bpf:
+            trace_h = self.fill_trace_h()
+            path = f"{self.name}_trace.h"
+            self._create_file(path, trace_h)
diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main_bpf.c b/tools/verification/rvgen/rvgen/templates/dot2k/main_bpf.c
new file mode 100644
index 000000000000..1a83f3a2159a
--- /dev/null
+++ b/tools/verification/rvgen/rvgen/templates/dot2k/main_bpf.c
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include "vmlinux.h"
+
+#define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%%
+#include "%%MODEL_NAME%%.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.
+ */
+%%TRACEPOINT_HANDLERS_SKEL%%
+static struct rv_monitor rv_this = {
+	.enabled = 0,
+};
+
+char LICENSE[] SEC("license") = "GPL";
+char DESCRIPTION[] SEC(".rodata.description") = "%%DESCRIPTION%%";
-- 
2.55.0