[PATCH v2 00/20] rv/rvgen: Robustness, modernization, and fixes

[PATCH v2 00/20] rv/rvgen: Robustness, modernization, and fixes

[Wander Lairson Costa]

This patch series introduces fixes and improvements to the RV Generator
(rvgen) tool in tools/verification. The primary goal is to enhance the
tool's robustness, maintainability, and correctness by addressing
several latent bugs, modernizing the Python codebase, and improving its
overall structure and error handling.

The changes include fixing logic errors in DOT file validation,
resolving unbound variable errors that could lead to runtime crashes,
and improving exception handling by removing dangerous bare except
clauses. The codebase is updated to use contemporary Python idioms such
as f-strings and context managers. Additionally, type annotations are
added to resolve static analysis errors.

Changes in v2:
- Dropped patches related to the @not_implemented decorator and
  abstract method stubs (v1 patches 9, 18, 19) to address class
  hierarchy improvements in a separate series.
- Dropped trivial cleanup patches (boolean simplification, __contains__)
  as they were already fixed after rebasing from
  linux-trace/latency/for-next.
- Merged typo fix patches into a single patch.
- Changed the fix for the unbound loop variable warning in abbreviate_atoms
  pyright report.
- Reworked initial state validation to strictly enforce the presence of
  an initial state.

Wander Lairson Costa (20):
  rv/rvgen: introduce AutomataError exception class
  rv/rvgen: remove bare except clauses in generator
  rv/rvgen: replace % string formatting with f-strings
  rv/rvgen: replace __len__() calls with len()
  rv/rvgen: remove unnecessary semicolons
  rv/rvgen: use context managers for file operations
  rv/rvgen: fix typos in automata and generator docstring and comments
  rv/rvgen: fix PEP 8 whitespace violations
  rv/rvgen: fix DOT file validation logic error
  rv/rvgen: use class constant for init marker
  rv/rvgen: refactor automata.py to use iterator-based parsing
  rv/rvgen: remove unused sys import from dot2c
  rv/rvgen: remove unused __get_main_name method
  rv/rvgen: make monitor arguments required in rvgen
  rv/rvgen: fix isinstance check in Variable.expand()
  rv/rvgen: extract node marker string to class constant
  rv/rvgen: enforce presence of initial state
  rv/rvgen: fix unbound loop variable warning
  rv/rvgen: fix _fill_states() return type annotation
  rv/rvgen: add missing return type annotations

 tools/verification/rvgen/__main__.py        |  22 +--
 tools/verification/rvgen/dot2c              |   1 -
 tools/verification/rvgen/rvgen/automata.py  | 146 ++++++++++++--------
 tools/verification/rvgen/rvgen/dot2c.py     |  56 ++++----
 tools/verification/rvgen/rvgen/dot2k.py     |  32 ++---
 tools/verification/rvgen/rvgen/generator.py | 107 ++++++--------
 tools/verification/rvgen/rvgen/ltl2ba.py    |   2 +-
 tools/verification/rvgen/rvgen/ltl2k.py     |  46 +++---
 8 files changed, 216 insertions(+), 196 deletions(-)

-- 
2.52.0

[PATCH v2 01/20] rv/rvgen: introduce AutomataError exception class

[Wander Lairson Costa]

Replace the generic except Exception block with a custom AutomataError
class that inherits from Exception. This provides more precise exception
handling for automata parsing and validation errors while avoiding
overly broad exception catches that could mask programming errors like
SyntaxError or TypeError.

The AutomataError class is raised when DOT file processing fails due to
invalid format, I/O errors, or malformed automaton definitions. The
main entry point catches this specific exception and provides a
user-friendly error message to stderr before exiting.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/__main__.py        |  9 ++++++---
 tools/verification/rvgen/rvgen/automata.py  | 17 ++++++++++++-----
 tools/verification/rvgen/rvgen/dot2c.py     |  4 ++--
 tools/verification/rvgen/rvgen/generator.py |  7 ++-----
 4 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index fa6fc1f4de2f7..3bd438f8476ed 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -8,11 +8,15 @@
 # For further information, see:
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
+from sys import stderr
+
+
 if __name__ == '__main__':
     from rvgen.dot2k import dot2k
     from rvgen.generator import Monitor
     from rvgen.container import Container
     from rvgen.ltl2k import ltl2k
+    from rvgen.automata import AutomataError
     import argparse
     import sys
 
@@ -51,9 +55,8 @@ if __name__ == '__main__':
                 sys.exit(1)
         else:
             monitor = Container(vars(params))
-    except Exception as e:
-        print('Error: '+ str(e))
-        print("Sorry : :-(")
+    except AutomataError as e:
+        print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
         sys.exit(1)
 
     print("Writing the monitor into the directory %s" % monitor.name)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 3f06aef8d4fdc..6ecd5ccd8f3d3 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -10,6 +10,13 @@
 
 import ntpath
 
+class AutomataError(Exception):
+    """Exception raised for errors in automata parsing and validation.
+
+    Raised when DOT file processing fails due to invalid format, I/O errors,
+    or malformed automaton definitions.
+    """
+
 class Automata:
     """Automata class: Reads a dot file and part it as an automata.
 
@@ -32,11 +39,11 @@ class Automata:
         basename = ntpath.basename(self.__dot_path)
         if not basename.endswith(".dot") and not basename.endswith(".gv"):
             print("not a dot file")
-            raise Exception("not a dot file: %s" % self.__dot_path)
+            raise AutomataError("not a dot file: %s" % self.__dot_path)
 
         model_name = ntpath.splitext(basename)[0]
         if model_name.__len__() == 0:
-            raise Exception("not a dot file: %s" % self.__dot_path)
+            raise AutomataError("not a dot file: %s" % self.__dot_path)
 
         return model_name
 
@@ -45,8 +52,8 @@ class Automata:
         dot_lines = []
         try:
             dot_file = open(self.__dot_path)
-        except:
-            raise Exception("Cannot open the file: %s" % self.__dot_path)
+        except OSError as exc:
+            raise AutomataError(f"Cannot open the file: {self.__dot_path}") from exc
 
         dot_lines = dot_file.read().splitlines()
         dot_file.close()
@@ -55,7 +62,7 @@ class Automata:
         line = dot_lines[cursor].split()
 
         if (line[0] != "digraph") and (line[1] != "state_automaton"):
-            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
+            raise AutomataError("Not a valid .dot format: %s" % self.__dot_path)
         else:
             cursor += 1
         return dot_lines
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 06a26bf15a7e9..74147ae2942f9 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -13,7 +13,7 @@
 # For further information, see:
 #   Documentation/trace/rv/deterministic_automata.rst
 
-from .automata import Automata
+from .automata import Automata, AutomataError
 
 class Dot2c(Automata):
     enum_suffix = ""
@@ -71,7 +71,7 @@ class Dot2c(Automata):
             min_type = "unsigned int"
 
         if self.states.__len__() > 1000000:
-            raise Exception("Too many states: %d" % self.states.__len__())
+            raise AutomataError("Too many states: %d" % self.states.__len__())
 
         return min_type
 
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 3441385c11770..a7bee6b1ea70c 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -51,10 +51,7 @@ class RVGenerator:
         raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
 
     def _read_file(self, path):
-        try:
-            fd = open(path, 'r')
-        except OSError:
-            raise Exception("Cannot open the file: %s" % path)
+        fd = open(path, 'r')
 
         content = fd.read()
 
@@ -65,7 +62,7 @@ class RVGenerator:
         try:
             path = os.path.join(self.abs_template_dir, file)
             return self._read_file(path)
-        except Exception:
+        except OSError:
             # Specific template file not found. Try the generic template file in the template/
             # directory, which is one level up
             path = os.path.join(self.abs_template_dir, "..", file)
-- 
2.52.0

[PATCH v2 02/20] rv/rvgen: remove bare except clauses in generator

[Wander Lairson Costa]

Remove bare except clauses from the generator module that were
catching all exceptions including KeyboardInterrupt and SystemExit.
This follows the same exception handling improvements made in the
previous AutomataError commit and addresses PEP 8 violations.

The bare except clause in __create_directory was silently catching
and ignoring all errors after printing a message, which could mask
serious issues. For __write_file, the bare except created a critical
bug where the file variable could remain undefined if open() failed,
causing a NameError when attempting to write to or close the file.

These methods now let OSError propagate naturally, allowing callers
to handle file system errors appropriately. This provides clearer
error reporting and allows Python's exception handling to show
complete stack traces with proper error types and locations.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/generator.py | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index a7bee6b1ea70c..af1662e2c20a7 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -198,17 +198,10 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
             os.mkdir(path)
         except FileExistsError:
             return
-        except:
-            print("Fail creating the output dir: %s" % self.name)
 
     def __write_file(self, file_name, content):
-        try:
-            file = open(file_name, 'w')
-        except:
-            print("Fail writing to file: %s" % file_name)
-
+        file = open(file_name, 'w')
         file.write(content)
-
         file.close()
 
     def _create_file(self, file_name, content):
-- 
2.52.0

[PATCH v2 03/20] rv/rvgen: replace % string formatting with f-strings

[Wander Lairson Costa]

Replace all instances of percent-style string formatting with
f-strings across the rvgen codebase. This modernizes the string
formatting to use Python 3.6+ features, providing clearer and more
maintainable code while improving runtime performance.

The conversion handles all formatting cases including simple variable
substitution, multi-variable formatting, and complex format specifiers.
Dynamic width formatting is converted from "%*s" to "{var:>{width}}"
using proper alignment syntax. Template strings for generated C code
properly escape braces using double-brace syntax to produce literal
braces in the output.

F-strings provide approximately 2x performance improvement over percent
formatting and are the recommended approach in modern Python.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/__main__.py        |  6 +--
 tools/verification/rvgen/rvgen/automata.py  |  6 +--
 tools/verification/rvgen/rvgen/dot2c.py     | 38 ++++++-------
 tools/verification/rvgen/rvgen/dot2k.py     | 26 ++++-----
 tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++-----------
 tools/verification/rvgen/rvgen/ltl2k.py     | 30 +++++------
 6 files changed, 81 insertions(+), 84 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 3bd438f8476ed..50b7d4227fb16 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -45,7 +45,7 @@ if __name__ == '__main__':
 
     try:
         if params.subcmd == "monitor":
-            print("Opening and parsing the specification file %s" % params.spec)
+            print(f"Opening and parsing the specification file {params.spec}")
             if params.monitor_class == "da":
                 monitor = dot2k(params.spec, params.monitor_type, vars(params))
             elif params.monitor_class == "ltl":
@@ -59,11 +59,11 @@ if __name__ == '__main__':
         print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
         sys.exit(1)
 
-    print("Writing the monitor into the directory %s" % monitor.name)
+    print(f"Writing the monitor into the directory {monitor.name}")
     monitor.print_files()
     print("Almost done, checklist")
     if params.subcmd == "monitor":
-        print("  - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name))
+        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())
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 6ecd5ccd8f3d3..bd8c04526be3a 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -39,11 +39,11 @@ class Automata:
         basename = ntpath.basename(self.__dot_path)
         if not basename.endswith(".dot") and not basename.endswith(".gv"):
             print("not a dot file")
-            raise AutomataError("not a dot file: %s" % self.__dot_path)
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         model_name = ntpath.splitext(basename)[0]
         if model_name.__len__() == 0:
-            raise AutomataError("not a dot file: %s" % self.__dot_path)
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         return model_name
 
@@ -62,7 +62,7 @@ class Automata:
         line = dot_lines[cursor].split()
 
         if (line[0] != "digraph") and (line[1] != "state_automaton"):
-            raise AutomataError("Not a valid .dot format: %s" % self.__dot_path)
+            raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
         else:
             cursor += 1
         return dot_lines
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 74147ae2942f9..6a2ad4fbf7824 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -28,17 +28,17 @@ class Dot2c(Automata):
 
     def __get_enum_states_content(self) -> list[str]:
         buff = []
-        buff.append("\t%s%s," % (self.initial_state, self.enum_suffix))
+        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
         for state in self.states:
             if state != self.initial_state:
-                buff.append("\t%s%s," % (state, self.enum_suffix))
-        buff.append("\tstate_max%s," % (self.enum_suffix))
+                buff.append(f"\t{state}{self.enum_suffix},")
+        buff.append(f"\tstate_max{self.enum_suffix},")
 
         return buff
 
     def format_states_enum(self) -> list[str]:
         buff = []
-        buff.append("enum %s {" % self.enum_states_def)
+        buff.append(f"enum {self.enum_states_def} {{")
         buff += self.__get_enum_states_content()
         buff.append("};\n")
 
@@ -47,15 +47,15 @@ class Dot2c(Automata):
     def __get_enum_events_content(self) -> list[str]:
         buff = []
         for event in self.events:
-            buff.append("\t%s%s," % (event, self.enum_suffix))
+            buff.append(f"\t{event}{self.enum_suffix},")
 
-        buff.append("\tevent_max%s," % self.enum_suffix)
+        buff.append(f"\tevent_max{self.enum_suffix},")
 
         return buff
 
     def format_events_enum(self) -> list[str]:
         buff = []
-        buff.append("enum %s {" % self.enum_events_def)
+        buff.append(f"enum {self.enum_events_def} {{")
         buff += self.__get_enum_events_content()
         buff.append("};\n")
 
@@ -71,25 +71,25 @@ class Dot2c(Automata):
             min_type = "unsigned int"
 
         if self.states.__len__() > 1000000:
-            raise AutomataError("Too many states: %d" % self.states.__len__())
+            raise AutomataError(f"Too many states: {self.states.__len__()}")
 
         return min_type
 
     def format_automaton_definition(self) -> list[str]:
         min_type = self.get_minimun_type()
         buff = []
-        buff.append("struct %s {" % self.struct_automaton_def)
-        buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
-        buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
-        buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix))
-        buff.append("\t%s initial_state;" % min_type)
-        buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
+        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}];")
+        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}];")
         buff.append("};\n")
         return buff
 
     def format_aut_init_header(self) -> list[str]:
         buff = []
-        buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
+        buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{")
         return buff
 
     def __get_string_vector_per_line_content(self, entries: list[str]) -> str:
@@ -134,9 +134,9 @@ class Dot2c(Automata):
                     next_state = self.function[x][y] + self.enum_suffix
 
                 if linetoolong:
-                    line += "\t\t\t%s" % next_state
+                    line += f"\t\t\t{next_state}"
                 else:
-                    line += "%*s" % (maxlen, next_state)
+                    line += f"{next_state:>{maxlen}}"
                 if y != nr_events-1:
                     line += ",\n" if linetoolong else ", "
                 else:
@@ -180,7 +180,7 @@ class Dot2c(Automata):
 
     def format_aut_init_final_states(self) -> list[str]:
        buff = []
-       buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
+       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},")
 
        return buff
 
@@ -196,7 +196,7 @@ class Dot2c(Automata):
 
     def format_invalid_state(self) -> list[str]:
         buff = []
-        buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix))
+        buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n")
 
         return buff
 
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 6128fe2384308..6d4151acc9fe3 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -19,7 +19,7 @@ class dot2k(Monitor, Dot2c):
         self.monitor_type = MonitorType
         Monitor.__init__(self, extra_params)
         Dot2c.__init__(self, file_path, extra_params.get("model_name"))
-        self.enum_suffix = "_%s" % self.name
+        self.enum_suffix = f"_{self.name}"
 
     def fill_monitor_type(self) -> str:
         return self.monitor_type.upper()
@@ -27,7 +27,7 @@ class dot2k(Monitor, Dot2c):
     def fill_tracepoint_handlers_skel(self) -> str:
         buff = []
         for event in self.events:
-            buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event)
+            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
             buff.append("{")
             handle = "handle_event"
             if self.is_start_event(event):
@@ -38,9 +38,9 @@ class dot2k(Monitor, Dot2c):
                 handle = "handle_start_run_event"
             if self.monitor_type == "per_task":
                 buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;");
-                buff.append("\tda_%s(p, %s%s);" % (handle, event, self.enum_suffix));
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
             else:
-                buff.append("\tda_%s(%s%s);" % (handle, event, self.enum_suffix));
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
             buff.append("}")
             buff.append("")
         return '\n'.join(buff)
@@ -48,20 +48,20 @@ class dot2k(Monitor, Dot2c):
     def fill_tracepoint_attach_probe(self) -> str:
         buff = []
         for event in self.events:
-            buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
+            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
         return '\n'.join(buff)
 
     def fill_tracepoint_detach_helper(self) -> str:
         buff = []
         for event in self.events:
-            buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
+            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
         return '\n'.join(buff)
 
     def fill_model_h_header(self) -> list[str]:
         buff = []
         buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
         buff.append("/*")
-        buff.append(" * Automatically generated C representation of %s automaton" % (self.name))
+        buff.append(f" * Automatically generated C representation of {self.name} automaton")
         buff.append(" * For further information about this format, see kernel documentation:")
         buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
         buff.append(" */")
@@ -75,10 +75,10 @@ class dot2k(Monitor, Dot2c):
         #
         # Adjust the definition names
         #
-        self.enum_states_def = "states_%s" % self.name
-        self.enum_events_def = "events_%s" % self.name
-        self.struct_automaton_def = "automaton_%s" % self.name
-        self.var_automaton_def = "automaton_%s" % self.name
+        self.enum_states_def = f"states_{self.name}"
+        self.enum_events_def = f"events_{self.name}"
+        self.struct_automaton_def = f"automaton_{self.name}"
+        self.var_automaton_def = f"automaton_{self.name}"
 
         buff = self.fill_model_h_header()
         buff += self.format_model()
@@ -113,8 +113,8 @@ class dot2k(Monitor, Dot2c):
             tp_args.insert(0, tp_args_id)
         tp_proto_c = ", ".join([a+b for a,b in tp_args])
         tp_args_c = ", ".join([b for a,b in tp_args])
-        buff.append("	     TP_PROTO(%s)," % tp_proto_c)
-        buff.append("	     TP_ARGS(%s)" % tp_args_c)
+        buff.append(f"	     TP_PROTO({tp_proto_c}),")
+        buff.append(f"	     TP_ARGS({tp_args_c})")
         return '\n'.join(buff)
 
     def fill_main_c(self) -> str:
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index af1662e2c20a7..6d16fb68798a7 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -40,7 +40,7 @@ class RVGenerator:
         if platform.system() != "Linux":
             raise OSError("I can only run on Linux.")
 
-        kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
+        kernel_path = os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
 
         # if the current kernel is from a distro this may not be a full kernel tree
         # verify that one of the files we are going to modify is available
@@ -69,11 +69,11 @@ class RVGenerator:
             return self._read_file(path)
 
     def fill_parent(self):
-        return "&rv_%s" % self.parent if self.parent else "NULL"
+        return f"&rv_{self.parent}" if self.parent else "NULL"
 
     def fill_include_parent(self):
         if self.parent:
-            return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
+            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
         return ""
 
     def fill_tracepoint_handlers_skel(self):
@@ -119,7 +119,7 @@ class RVGenerator:
         buff = []
         buff.append("	# XXX: add dependencies if there")
         if self.parent:
-            buff.append("	depends on RV_MON_%s" % self.parent.upper())
+            buff.append(f"	depends on RV_MON_{self.parent.upper()}")
             buff.append("	default y")
         return '\n'.join(buff)
 
@@ -145,31 +145,30 @@ class RVGenerator:
         monitor_class_type = self.fill_monitor_class_type()
         if self.auto_patch:
             self._patch_file("rv_trace.h",
-                            "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
-                            "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
-            return "  - Patching %s/rv_trace.h, double check the result" % self.rv_dir
+                            f"// Add new monitors based on CONFIG_{monitor_class_type} here",
+                            f"#include <monitors/{self.name}/{self.name}_trace.h>")
+            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the result"
 
-        return """  - Edit %s/rv_trace.h:
-Add this line where other tracepoints are included and %s is defined:
-#include <monitors/%s/%s_trace.h>
-""" % (self.rv_dir, monitor_class_type, self.name, self.name)
+        return f"""  - Edit {self.rv_dir}/rv_trace.h:
+Add this line where other tracepoints are included and {monitor_class_type} is defined:
+#include <monitors/{self.name}/{self.name}_trace.h>
+"""
 
     def _kconfig_marker(self, container=None) -> str:
-        return "# Add new %smonitors here" % (container + " "
-                                              if container else "")
+        return f"# Add new {container + ' ' if container else ''}monitors here"
 
     def fill_kconfig_tooltip(self):
         if self.auto_patch:
             # monitors with a container should stay together in the Kconfig
             self._patch_file("Kconfig",
                              self._kconfig_marker(self.parent),
-                            "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
-            return "  - Patching %s/Kconfig, double check the result" % self.rv_dir
+                            f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
+            return f"  - Patching {self.rv_dir}/Kconfig, double check the result"
 
-        return """  - Edit %s/Kconfig:
+        return f"""  - Edit {self.rv_dir}/Kconfig:
 Add this line where other monitors are included:
-source \"kernel/trace/rv/monitors/%s/Kconfig\"
-""" % (self.rv_dir, self.name)
+source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
+"""
 
     def fill_makefile_tooltip(self):
         name = self.name
@@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\"
         if self.auto_patch:
             self._patch_file("Makefile",
                             "# Add new monitors here",
-                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
-            return "  - Patching %s/Makefile, double check the result" % self.rv_dir
+                            f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o")
+            return f"  - Patching {self.rv_dir}/Makefile, double check the result"
 
-        return """  - Edit %s/Makefile:
+        return f"""  - Edit {self.rv_dir}/Makefile:
 Add this line where other monitors are included:
-obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
-""" % (self.rv_dir, name_up, name, name)
+obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
+"""
 
     def fill_monitor_tooltip(self):
         if self.auto_patch:
-            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
-        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
+            return f"  - Monitor created in {self.rv_dir}/monitors/{self.name}"
+        return f"  - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
 
     def __create_directory(self):
         path = self.name
@@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
         file.close()
 
     def _create_file(self, file_name, content):
-        path = "%s/%s" % (self.name, file_name)
+        path = f"{self.name}/{file_name}"
         if self.auto_patch:
             path = os.path.join(self.rv_dir, "monitors", path)
         self.__write_file(path, content)
 
     def __get_main_name(self):
-        path = "%s/%s" % (self.name, "main.c")
+        path = f"{self.name}/main.c"
         if not os.path.exists(path):
             return "main.c"
         return "__main.c"
@@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
 
         self.__create_directory()
 
-        path = "%s.c" % self.name
+        path = f"{self.name}.c"
         self._create_file(path, main_c)
 
         model_h = self.fill_model_h()
-        path = "%s.h" % self.name
+        path = f"{self.name}.h"
         self._create_file(path, model_h)
 
         kconfig = self.fill_kconfig()
@@ -256,5 +255,5 @@ class Monitor(RVGenerator):
     def print_files(self):
         super().print_files()
         trace_h = self.fill_trace_h()
-        path = "%s_trace.h" % self.name
+        path = f"{self.name}_trace.h"
         self._create_file(path, trace_h)
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b075f98d50c47..fa9ea6d597095 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -73,7 +73,7 @@ class ltl2k(generator.Monitor):
         ]
 
         for node in self.ba:
-            buf.append("\tS%i," % node.id)
+            buf.append(f"\tS{node.id},")
         buf.append("\tRV_NUM_BA_STATES")
         buf.append("};")
         buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
@@ -82,7 +82,7 @@ class ltl2k(generator.Monitor):
     def _fill_atoms(self):
         buf = ["enum ltl_atom {"]
         for a in sorted(self.atoms):
-            buf.append("\tLTL_%s," % a)
+            buf.append(f"\tLTL_{a},")
         buf.append("\tLTL_NUM_ATOM")
         buf.append("};")
         buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
@@ -96,7 +96,7 @@ class ltl2k(generator.Monitor):
         ]
 
         for name in self.atoms_abbr:
-            buf.append("\t\t\"%s\"," % name)
+            buf.append(f"\t\t\"{name}\",")
 
         buf.extend([
             "\t};",
@@ -113,19 +113,19 @@ class ltl2k(generator.Monitor):
                 continue
 
             if isinstance(node.op, ltl2ba.AndOp):
-                buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
+                buf.append(f"\tbool {node} = {node.op.left} && {node.op.right};")
                 required_values |= {str(node.op.left), str(node.op.right)}
             elif isinstance(node.op, ltl2ba.OrOp):
-                buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
+                buf.append(f"\tbool {node} = {node.op.left} || {node.op.right};")
                 required_values |= {str(node.op.left), str(node.op.right)}
             elif isinstance(node.op, ltl2ba.NotOp):
-                buf.append("\tbool %s = !%s;" % (node, node.op.child))
+                buf.append(f"\tbool {node} = !{node.op.child};")
                 required_values.add(str(node.op.child))
 
         for atom in self.atoms:
             if atom.lower() not in required_values:
                 continue
-            buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom))
+            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);")
 
         buf.reverse()
 
@@ -153,7 +153,7 @@ class ltl2k(generator.Monitor):
         ])
 
         for node in self.ba:
-            buf.append("\tcase S%i:" % node.id)
+            buf.append(f"\tcase S{node.id}:")
 
             for o in sorted(node.outgoing):
                 line   = "\t\tif "
@@ -163,7 +163,7 @@ class ltl2k(generator.Monitor):
                 lines = break_long_line(line, indent)
                 buf.extend(lines)
 
-                buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
+                buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
             buf.append("\t\tbreak;")
         buf.extend([
             "\t}",
@@ -197,7 +197,7 @@ class ltl2k(generator.Monitor):
             lines = break_long_line(line, indent)
             buf.extend(lines)
 
-            buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
+            buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
         buf.append("}")
         return buf
 
@@ -205,23 +205,21 @@ class ltl2k(generator.Monitor):
         buff = []
         buff.append("static void handle_example_event(void *data, /* XXX: fill header */)")
         buff.append("{")
-        buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0])
+        buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);")
         buff.append("}")
         buff.append("")
         return '\n'.join(buff)
 
     def fill_tracepoint_attach_probe(self):
-        return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \
-                % self.name
+        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
 
     def fill_tracepoint_detach_helper(self):
-        return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \
-                % self.name
+        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_sample_event);"
 
     def fill_atoms_init(self):
         buff = []
         for a in self.atoms:
-            buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
+            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
         return '\n'.join(buff)
 
     def fill_model_h(self):
-- 
2.52.0

[PATCH v2 04/20] rv/rvgen: replace __len__() calls with len()

[Wander Lairson Costa]

Replace all direct calls to the __len__() dunder method with the
idiomatic len() built-in function across the rvgen codebase. This
change eliminates a Python anti-pattern where dunder methods are
called directly instead of using their corresponding built-in
functions.

The changes affect nine instances across two files. In automata.py,
the empty string check is further improved by using truthiness
testing instead of explicit length comparison. In dot2c.py, all
length checks in the get_minimun_type, __get_max_strlen_of_states,
and get_aut_init_function methods now use the standard len()
function. Additionally, spacing around keyword arguments has been
corrected to follow PEP 8 guidelines.

Direct calls to dunder methods like __len__() are discouraged in
Python because they bypass the language's abstraction layer and
reduce code readability. Using len() provides the same functionality
while adhering to Python community standards and making the code more
familiar to Python developers.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/automata.py |  2 +-
 tools/verification/rvgen/rvgen/dot2c.py    | 16 ++++++++--------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index bd8c04526be3a..07ae81e9a49fa 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -42,7 +42,7 @@ class Automata:
             raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         model_name = ntpath.splitext(basename)[0]
-        if model_name.__len__() == 0:
+        if not model_name:
             raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         return model_name
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 6a2ad4fbf7824..b3a49779d4cc5 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -64,14 +64,14 @@ class Dot2c(Automata):
     def get_minimun_type(self) -> str:
         min_type = "unsigned char"
 
-        if self.states.__len__() > 255:
+        if len(self.states) > 255:
             min_type = "unsigned short"
 
-        if self.states.__len__() > 65535:
+        if len(self.states) > 65535:
             min_type = "unsigned int"
 
-        if self.states.__len__() > 1000000:
-            raise AutomataError(f"Too many states: {self.states.__len__()}")
+        if len(self.states) > 1000000:
+            raise AutomataError(f"Too many states: {len(self.states)}")
 
         return min_type
 
@@ -114,12 +114,12 @@ class Dot2c(Automata):
         return buff
 
     def __get_max_strlen_of_states(self) -> int:
-        max_state_name = max(self.states, key = len).__len__()
-        return max(max_state_name, self.invalid_state_str.__len__())
+        max_state_name = len(max(self.states, key=len))
+        return max(max_state_name, len(self.invalid_state_str))
 
     def get_aut_init_function(self) -> str:
-        nr_states = self.states.__len__()
-        nr_events = self.events.__len__()
+        nr_states = len(self.states)
+        nr_events = len(self.events)
         buff = []
 
         maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix)
-- 
2.52.0

[PATCH v2 05/20] rv/rvgen: remove unnecessary semicolons

[Wander Lairson Costa]

Remove unnecessary semicolons from Python code in the rvgen tool.
Python does not require semicolons to terminate statements, and
their presence goes against PEP 8 style guidelines. These semicolons
were likely added out of habit from C-style languages.

This cleanup improves consistency with Python coding standards and
aligns with the recent improvements to remove other Python
anti-patterns from the codebase.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/dot2k.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 6d4151acc9fe3..c70a9812abbf6 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -37,10 +37,10 @@ class dot2k(Monitor, Dot2c):
                 buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
                 handle = "handle_start_run_event"
             if self.monitor_type == "per_task":
-                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;");
-                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
+                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
             else:
-                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
             buff.append("}")
             buff.append("")
         return '\n'.join(buff)
-- 
2.52.0

[PATCH v2 06/20] rv/rvgen: use context managers for file operations

[Wander Lairson Costa]

Replace manual file open and close operations with context managers
throughout the rvgen codebase. The previous implementation used
explicit open() and close() calls, which could lead to resource leaks
if exceptions occurred between opening and closing the file handles.

This change affects three file operations: reading DOT specification
files in the automata parser, reading template files in the generator
base class, and writing generated monitor files. All now use the with
statement to ensure proper resource cleanup even in error conditions.

Context managers provide automatic cleanup through the with statement,
which guarantees that file handles are closed when the with block
exits regardless of whether an exception occurred. This follows PEP
343 recommendations and is the standard Python idiom for resource
management. The change also reduces code verbosity while improving
safety and maintainability.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py  |  6 ++----
 tools/verification/rvgen/rvgen/generator.py | 12 ++++--------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 07ae81e9a49fa..1feb5f0c0bc3e 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -51,13 +51,11 @@ class Automata:
         cursor = 0
         dot_lines = []
         try:
-            dot_file = open(self.__dot_path)
+            with open(self.__dot_path) as dot_file:
+                dot_lines = dot_file.read().splitlines()
         except OSError as exc:
             raise AutomataError(f"Cannot open the file: {self.__dot_path}") from exc
 
-        dot_lines = dot_file.read().splitlines()
-        dot_file.close()
-
         # checking the first line:
         line = dot_lines[cursor].split()
 
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 6d16fb68798a7..ee75e111feef1 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -51,11 +51,8 @@ class RVGenerator:
         raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
 
     def _read_file(self, path):
-        fd = open(path, 'r')
-
-        content = fd.read()
-
-        fd.close()
+        with open(path, 'r') as fd:
+            content = fd.read()
         return content
 
     def _read_template_file(self, file):
@@ -199,9 +196,8 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
             return
 
     def __write_file(self, file_name, content):
-        file = open(file_name, 'w')
-        file.write(content)
-        file.close()
+        with open(file_name, 'w') as file:
+            file.write(content)
 
     def _create_file(self, file_name, content):
         path = f"{self.name}/{file_name}"
-- 
2.52.0

[PATCH v2 07/20] rv/rvgen: fix typos in automata and generator docstring and comments

[Wander Lairson Costa]

Fix two typos in the Automata class documentation that have been
present since the initial implementation. Fix the class
docstring: "part it" instead of "parses it". Additionally, a
comment describing transition labels contained the misspelling
"lables" instead of "labels".

Fix a typo in the comment describing the insertion of the initial
state into the states list: "bein og" should be "beginning of".

Fix typo in the module docstring: "Abtract" should be "Abstract".

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py  | 6 +++---
 tools/verification/rvgen/rvgen/generator.py | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 1feb5f0c0bc3e..0d7cbd0c634a9 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -18,7 +18,7 @@ class AutomataError(Exception):
     """
 
 class Automata:
-    """Automata class: Reads a dot file and part it as an automata.
+    """Automata class: Reads a dot file and parses it as an automata.
 
     Attributes:
         dot_file: A dot file with an state_automaton definition.
@@ -113,7 +113,7 @@ class Automata:
         states = sorted(set(states))
         states.remove(initial_state)
 
-        # Insert the initial state at the bein og the states
+        # Insert the initial state at the beginning of the states
         states.insert(0, initial_state)
 
         if not has_final_states:
@@ -134,7 +134,7 @@ class Automata:
                 line = self.__dot_lines[cursor].split()
                 event = line[-2].replace('"','')
 
-                # when a transition has more than one lables, they are like this
+                # when a transition has more than one labels, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
                 # so split them.
 
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index ee75e111feef1..a3fbb1ac74916 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -3,7 +3,7 @@
 #
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
 #
-# Abtract class for generating kernel runtime verification monitors from specification file
+# Abstract class for generating kernel runtime verification monitors from specification file
 
 import platform
 import os
-- 
2.52.0

[PATCH v2 08/20] rv/rvgen: fix PEP 8 whitespace violations

[Wander Lairson Costa]

Fix whitespace violations throughout the rvgen codebase to comply
with PEP 8 style guidelines. The changes address missing whitespace
after commas, around operators, and in collection literals that
were flagged by pycodestyle.

The fixes include adding whitespace after commas in string replace
chains and function arguments, adding whitespace around arithmetic
operators, removing extra whitespace in list comprehensions, and
fixing dictionary literal spacing. These changes improve code
readability and consistency with Python coding standards.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/automata.py  | 12 ++++++------
 tools/verification/rvgen/rvgen/dot2c.py     |  2 +-
 tools/verification/rvgen/rvgen/dot2k.py     |  4 ++--
 tools/verification/rvgen/rvgen/generator.py |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 0d7cbd0c634a9..deb1f09556c3c 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -95,7 +95,7 @@ class Automata:
             raw_state = line[-1]
 
             #  "enabled_fired"}; -> enabled_fired
-            state = raw_state.replace('"', '').replace('};', '').replace(',','_')
+            state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
             if state[0:7] == "__init_":
                 initial_state = state[7:]
             else:
@@ -132,7 +132,7 @@ class Automata:
             #  ------------ event is here ------------^^^^^
             if self.__dot_lines[cursor].split()[1] == "->":
                 line = self.__dot_lines[cursor].split()
-                event = line[-2].replace('"','')
+                event = line[-2].replace('"', '')
 
                 # when a transition has more than one labels, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
@@ -162,7 +162,7 @@ class Automata:
             nr_state += 1
 
         # declare the matrix....
-        matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
+        matrix = [[self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
 
         # and we are back! Let's fill the matrix
         cursor = self.__get_cursor_begin_events()
@@ -170,9 +170,9 @@ class Automata:
         while self.__dot_lines[cursor].lstrip()[0] == '"':
             if self.__dot_lines[cursor].split()[1] == "->":
                 line = self.__dot_lines[cursor].split()
-                origin_state = line[0].replace('"','').replace(',','_')
-                dest_state = line[2].replace('"','').replace(',','_')
-                possible_events = line[-2].replace('"','').replace("\\n", " ")
+                origin_state = line[0].replace('"', '').replace(',', '_')
+                dest_state = line[2].replace('"', '').replace(',', '_')
+                possible_events = line[-2].replace('"', '').replace("\\n", " ")
                 for event in possible_events.split():
                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
             cursor += 1
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index b3a49779d4cc5..6ab519b03789c 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -137,7 +137,7 @@ class Dot2c(Automata):
                     line += f"\t\t\t{next_state}"
                 else:
                     line += f"{next_state:>{maxlen}}"
-                if y != nr_events-1:
+                if y != nr_events - 1:
                     line += ",\n" if linetoolong else ", "
                 else:
                     line += ",\n\t\t}," if linetoolong else " },"
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index c70a9812abbf6..4bf0db52e6264 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -111,8 +111,8 @@ class dot2k(Monitor, Dot2c):
         tp_args = tp_args_event if tp_type == "event" else tp_args_error
         if self.monitor_type == "per_task":
             tp_args.insert(0, tp_args_id)
-        tp_proto_c = ", ".join([a+b for a,b in tp_args])
-        tp_args_c = ", ".join([b for a,b in tp_args])
+        tp_proto_c = ", ".join([a + b for a, b in tp_args])
+        tp_args_c = ", ".join([b for a, b in tp_args])
         buff.append(f"	     TP_PROTO({tp_proto_c}),")
         buff.append(f"	     TP_ARGS({tp_args_c})")
         return '\n'.join(buff)
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index a3fbb1ac74916..31c454329e8e1 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -228,7 +228,7 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
 
 
 class Monitor(RVGenerator):
-    monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
+    monitor_types = {"global": 1, "per_cpu": 2, "per_task": 3}
 
     def __init__(self, extra_params={}):
         super().__init__(extra_params)
-- 
2.52.0

[PATCH v2 09/20] rv/rvgen: fix DOT file validation logic error

[Wander Lairson Costa]

Fix incorrect boolean logic in automata DOT file format validation
that allowed malformed files to pass undetected. The previous
implementation used a logical AND operator where OR was required,
causing the validation to only reject files when both the first
token was not "digraph" AND the second token was not
"state_automaton". This meant a file starting with "digraph" but
having an incorrect second token would incorrectly pass validation.

The corrected logic properly rejects DOT files where either the
first token is not "digraph" or the second token is not
"state_automaton", ensuring that only properly formatted automaton
definition files are accepted for processing. Without this fix,
invalid DOT files could cause downstream parsing failures or
generate incorrect C code for runtime verification monitors.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index deb1f09556c3c..38035d59cdd51 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -59,7 +59,7 @@ class Automata:
         # checking the first line:
         line = dot_lines[cursor].split()
 
-        if (line[0] != "digraph") and (line[1] != "state_automaton"):
+        if (line[0] != "digraph") or (line[1] != "state_automaton"):
             raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
         else:
             cursor += 1
-- 
2.52.0

[PATCH v2 10/20] rv/rvgen: use class constant for init marker

[Wander Lairson Costa]

Replace hardcoded string literal and magic number with a class
constant for the initial state marker in DOT file parsing. The
previous implementation used the magic string "__init_" directly
in the code along with a hardcoded length of 7 for substring
extraction, which made the code less maintainable and harder to
understand.

This change introduces a class constant init_marker to serve as
a single source of truth for the initial state prefix. The code
now uses startswith() for clearer intent and calculates the
substring position dynamically using len(), eliminating the magic
number. If the marker value needs to change in the future, only
the constant definition requires updating rather than multiple
locations in the code.

The refactoring improves code readability and maintainability
while preserving the exact same runtime behavior.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 38035d59cdd51..035d0e8c12c9a 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -25,6 +25,7 @@ class Automata:
     """
 
     invalid_state_str = "INVALID_STATE"
+    init_marker = "__init_"
 
     def __init__(self, file_path, model_name=None):
         self.__dot_path = file_path
@@ -96,8 +97,8 @@ class Automata:
 
             #  "enabled_fired"}; -> enabled_fired
             state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
-            if state[0:7] == "__init_":
-                initial_state = state[7:]
+            if state.startswith(self.init_marker):
+                initial_state = state[len(self.init_marker):]
             else:
                 states.append(state)
                 if "doublecircle" in self.__dot_lines[cursor]:
-- 
2.52.0

[PATCH v2 11/20] rv/rvgen: refactor automata.py to use iterator-based parsing

[Wander Lairson Costa]

Refactor the DOT file parsing logic in automata.py to use Python's
iterator-based patterns instead of manual cursor indexing. The previous
implementation relied on while loops with explicit cursor management,
which made the code prone to off-by-one errors and would crash on
malformed input files containing empty lines.

The new implementation uses enumerate and itertools.islice to iterate
over lines, eliminating manual cursor tracking. Functions that search
for specific markers now use for loops with early returns and explicit
AutomataError exceptions for missing markers, rather than assuming the
markers exist. Additional bounds checking ensures that split line
arrays have sufficient elements before accessing specific indices,
preventing IndexError exceptions on malformed DOT files.

The matrix creation and event variable extraction methods now use
functional patterns with map combined with itertools.islice,
making the intent clearer while maintaining the same behavior. Minor
improvements include using extend instead of append in a loop, adding
empty file validation, and replacing enumerate with range where the
enumerated value was unused.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 109 +++++++++++++--------
 1 file changed, 67 insertions(+), 42 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 035d0e8c12c9a..17b012b868531 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -9,6 +9,7 @@
 #   Documentation/trace/rv/deterministic_automata.rst
 
 import ntpath
+from itertools import islice
 
 class AutomataError(Exception):
     """Exception raised for errors in automata parsing and validation.
@@ -49,37 +50,54 @@ class Automata:
         return model_name
 
     def __open_dot(self) -> list[str]:
-        cursor = 0
         dot_lines = []
         try:
             with open(self.__dot_path) as dot_file:
-                dot_lines = dot_file.read().splitlines()
+                dot_lines = dot_file.readlines()
         except OSError as exc:
             raise AutomataError(f"Cannot open the file: {self.__dot_path}") from exc
 
+        if not dot_lines:
+            raise AutomataError(f"{self.__dot_path} is empty")
+
         # checking the first line:
-        line = dot_lines[cursor].split()
+        line = dot_lines[0].split()
 
-        if (line[0] != "digraph") or (line[1] != "state_automaton"):
+        if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
             raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
-        else:
-            cursor += 1
+
         return dot_lines
 
     def __get_cursor_begin_states(self) -> int:
-        cursor = 0
-        while self.__dot_lines[cursor].split()[0] != "{node":
-            cursor += 1
-        return cursor
+        for cursor, line in enumerate(self.__dot_lines):
+            split_line = line.split()
+
+            if len(split_line) and split_line[0] == "{node":
+                return cursor
+
+        raise AutomataError("Could not find a beginning state")
 
     def __get_cursor_begin_events(self) -> int:
-        cursor = 0
-        while self.__dot_lines[cursor].split()[0] != "{node":
-            cursor += 1
-        while self.__dot_lines[cursor].split()[0] == "{node":
-            cursor += 1
-        # skip initial state transition
-        cursor += 1
+        state = 0
+        cursor = 0 # make pyright happy
+
+        for cursor, line in enumerate(self.__dot_lines):
+            line = line.split()
+            if not line:
+                continue
+
+            if state == 0:
+                if line[0] == "{node":
+                    state = 1
+            elif line[0] != "{node":
+                break
+        else:
+            raise AutomataError("Could not find beginning event")
+
+        cursor += 1 # skip initial state transition
+        if cursor == len(self.__dot_lines):
+            raise AutomataError("Dot file ended after event beginning")
+
         return cursor
 
     def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
@@ -91,9 +109,12 @@ class Automata:
         cursor = self.__get_cursor_begin_states()
 
         # process nodes
-        while self.__dot_lines[cursor].split()[0] == "{node":
-            line = self.__dot_lines[cursor].split()
-            raw_state = line[-1]
+        for line in islice(self.__dot_lines, cursor, None):
+            split_line = line.split()
+            if not split_line or split_line[0] != "{node":
+                break
+
+            raw_state = split_line[-1]
 
             #  "enabled_fired"}; -> enabled_fired
             state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
@@ -101,16 +122,14 @@ class Automata:
                 initial_state = state[len(self.init_marker):]
             else:
                 states.append(state)
-                if "doublecircle" in self.__dot_lines[cursor]:
+                if "doublecircle" in line:
                     final_states.append(state)
                     has_final_states = True
 
-                if "ellipse" in self.__dot_lines[cursor]:
+                if "ellipse" in line:
                     final_states.append(state)
                     has_final_states = True
 
-            cursor += 1
-
         states = sorted(set(states))
         states.remove(initial_state)
 
@@ -123,26 +142,27 @@ class Automata:
         return states, initial_state, final_states
 
     def __get_event_variables(self) -> list[str]:
+        events: list[str] = []
         # here we are at the begin of transitions, take a note, we will return later.
         cursor = self.__get_cursor_begin_events()
 
-        events = []
-        while self.__dot_lines[cursor].lstrip()[0] == '"':
+        for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
+            if not line.startswith('"'):
+                break
+
             # transitions have the format:
             # "all_fired" -> "both_fired" [ label = "disable_irq" ];
             #  ------------ event is here ------------^^^^^
-            if self.__dot_lines[cursor].split()[1] == "->":
-                line = self.__dot_lines[cursor].split()
-                event = line[-2].replace('"', '')
+            split_line = line.split()
+            if len(split_line) > 1 and split_line[1] == "->":
+                event = split_line[-2].replace('"', '')
 
                 # when a transition has more than one labels, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
                 # so split them.
 
                 event = event.replace("\\n", " ")
-                for i in event.split():
-                    events.append(i)
-            cursor += 1
+                events.extend(event.split())
 
         return sorted(set(events))
 
@@ -163,31 +183,36 @@ class Automata:
             nr_state += 1
 
         # declare the matrix....
-        matrix = [[self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
+        matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
 
         # and we are back! Let's fill the matrix
         cursor = self.__get_cursor_begin_events()
 
-        while self.__dot_lines[cursor].lstrip()[0] == '"':
-            if self.__dot_lines[cursor].split()[1] == "->":
-                line = self.__dot_lines[cursor].split()
-                origin_state = line[0].replace('"', '').replace(',', '_')
-                dest_state = line[2].replace('"', '').replace(',', '_')
-                possible_events = line[-2].replace('"', '').replace("\\n", " ")
+        for line in map(str.lstrip,
+                        islice(self.__dot_lines, cursor, None)):
+
+            if not line or line[0] != '"':
+                break
+
+            split_line = line.split()
+
+            if len(split_line) > 2 and split_line[1] == "->":
+                origin_state = split_line[0].replace('"', '').replace(',', '_')
+                dest_state = split_line[2].replace('"', '').replace(',', '_')
+                possible_events = split_line[-2].replace('"', '').replace("\\n", " ")
                 for event in possible_events.split():
                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
-            cursor += 1
 
         return matrix
 
     def __store_init_events(self) -> tuple[list[bool], list[bool]]:
         events_start = [False] * len(self.events)
         events_start_run = [False] * len(self.events)
-        for i, _ in enumerate(self.events):
+        for i in range(len(self.events)):
             curr_event_will_init = 0
             curr_event_from_init = False
             curr_event_used = 0
-            for j, _ in enumerate(self.states):
+            for j in range(len(self.states)):
                 if self.function[j][i] != self.invalid_state_str:
                     curr_event_used += 1
                 if self.function[j][i] == self.initial_state:
-- 
2.52.0

[PATCH v2 12/20] rv/rvgen: remove unused sys import from dot2c

[Wander Lairson Costa]

The sys module was imported in the dot2c frontend script but never
used. This import was likely left over from earlier development or
copied from a template that required sys for exit handling.

Remove the unused import to clean up the code and satisfy linters
that flag unused imports as errors.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/dot2c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c
index bf0c67c5b66c8..1012becc7fab6 100644
--- a/tools/verification/rvgen/dot2c
+++ b/tools/verification/rvgen/dot2c
@@ -16,7 +16,6 @@
 if __name__ == '__main__':
     from rvgen import dot2c
     import argparse
-    import sys
 
     parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
     parser.add_argument('dot_file',  help='The dot file to be converted')
-- 
2.52.0

[PATCH v2 13/20] rv/rvgen: remove unused __get_main_name method

[Wander Lairson Costa]

The __get_main_name() method in the generator module is never called
from anywhere in the codebase. Remove this dead code to improve
maintainability.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/generator.py | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 31c454329e8e1..ef6c9150f50c6 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -205,12 +205,6 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
             path = os.path.join(self.rv_dir, "monitors", path)
         self.__write_file(path, content)
 
-    def __get_main_name(self):
-        path = f"{self.name}/main.c"
-        if not os.path.exists(path):
-            return "main.c"
-        return "__main.c"
-
     def print_files(self):
         main_c = self.fill_main_c()
 
-- 
2.52.0

[PATCH v2 14/20] rv/rvgen: make monitor arguments required in rvgen

[Wander Lairson Costa]

Add required=True to the monitor subcommand arguments for class, spec,
and monitor_type in rvgen. These arguments are essential for monitor
generation and attempting to run without them would cause AttributeError
exceptions later in the code when the script tries to access them.

Making these arguments explicitly required provides clearer error
messages to users at parse time rather than cryptic exceptions during
execution. This improves the user experience by catching missing
arguments early with helpful usage information.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/__main__.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 50b7d4227fb16..c4c795c15e853 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -32,10 +32,11 @@ if __name__ == '__main__':
     monitor_parser.add_argument('-n', "--model_name", dest="model_name")
     monitor_parser.add_argument("-p", "--parent", dest="parent",
                                 required=False, help="Create a monitor nested to parent")
-    monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+    monitor_parser.add_argument('-c', "--class", dest="monitor_class", required=True,
                                 help="Monitor class, either \"da\" or \"ltl\"")
-    monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
-    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
+    monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
+                                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())}")
 
     container_parser = subparsers.add_parser("container")
-- 
2.52.0

[PATCH v2 15/20] rv/rvgen: fix isinstance check in Variable.expand()

[Wander Lairson Costa]

The Variable.expand() method in ltl2ba.py performs contradiction
detection by checking if a negated variable already exists in the
graph node's old set. However, the isinstance check was incorrectly
testing the ASTNode wrapper instead of the wrapped operator, causing
the check to always return False.

The old set contains ASTNode instances which wrap LTL operators via
their .op attribute. The fix changes isinstance(f, NotOp) to
isinstance(f.op, NotOp) to correctly examine the wrapped operator
type. This follows the established pattern used elsewhere in the
file, such as the iteration at lines 572-574 which accesses
o.op.is_temporal() on items from node.old.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/ltl2ba.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index f14e6760ac3db..28f9a5682c830 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -394,7 +394,7 @@ class Variable:
     @staticmethod
     def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
         for f in node.old:
-            if isinstance(f, NotOp) and f.op.child is n:
+            if isinstance(f.op, NotOp) and f.op.child is n:
                 return node_set
         node.old |= {n}
         return node.expand(node_set)
-- 
2.52.0

[PATCH v2 16/20] rv/rvgen: extract node marker string to class constant

[Wander Lairson Costa]

Add a node_marker class constant to the Automata class to replace the
hardcoded "{node" string literal used throughout the DOT file parsing
logic. This follows the existing pattern established by the init_marker
and invalid_state_str class constants in the same class.

The "{node" string is used as a marker to identify node declaration
lines in DOT files during state variable extraction and cursor
positioning. Extracting it to a named constant improves code
maintainability and makes the marker's purpose explicit.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 17b012b868531..270a3d0bf4ce7 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -27,6 +27,7 @@ class Automata:
 
     invalid_state_str = "INVALID_STATE"
     init_marker = "__init_"
+    node_marker = "{node"
 
     def __init__(self, file_path, model_name=None):
         self.__dot_path = file_path
@@ -72,7 +73,7 @@ class Automata:
         for cursor, line in enumerate(self.__dot_lines):
             split_line = line.split()
 
-            if len(split_line) and split_line[0] == "{node":
+            if len(split_line) and split_line[0] == self.node_marker:
                 return cursor
 
         raise AutomataError("Could not find a beginning state")
@@ -87,9 +88,9 @@ class Automata:
                 continue
 
             if state == 0:
-                if line[0] == "{node":
+                if line[0] == self.node_marker:
                     state = 1
-            elif line[0] != "{node":
+            elif line[0] != self.node_marker:
                 break
         else:
             raise AutomataError("Could not find beginning event")
@@ -111,7 +112,7 @@ class Automata:
         # process nodes
         for line in islice(self.__dot_lines, cursor, None):
             split_line = line.split()
-            if not split_line or split_line[0] != "{node":
+            if not split_line or split_line[0] != self.node_marker:
                 break
 
             raw_state = split_line[-1]
-- 
2.52.0

[PATCH v2 17/20] rv/rvgen: enforce presence of initial state

[Wander Lairson Costa]

The __get_state_variables() method parses DOT files to identify the
automaton's initial state. If the input file lacks a node with the
required initialization prefix, the initial_state variable is referenced
before assignment, causing an UnboundLocalError or a generic error
during the state removal step.

Initialize the variable explicitly and validate that a start node was
found after parsing. Raise a descriptive AutomataError if the definition
is missing to improve debugging and ensure the automaton is valid.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 270a3d0bf4ce7..cf82f04dbc661 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -105,6 +105,7 @@ class Automata:
         # wait for node declaration
         states = []
         final_states = []
+        initial_state = ""
 
         has_final_states = False
         cursor = self.__get_cursor_begin_states()
@@ -131,6 +132,9 @@ class Automata:
                     final_states.append(state)
                     has_final_states = True
 
+        if not initial_state:
+            raise AutomataError("The automaton doesn't have an initial state")
+
         states = sorted(set(states))
         states.remove(initial_state)
 
-- 
2.52.0

[PATCH v2 18/20] rv/rvgen: fix unbound loop variable warning

[Wander Lairson Costa]

Pyright static analysis reports a "possibly unbound variable" warning
for the loop variable `i` in the `abbreviate_atoms` function. The
variable is accessed after the inner loop terminates to slice the atom
string. While the loop logic currently ensures execution, the analyzer
flags the reliance on the loop variable persisting outside its scope.

Refactor the prefix length calculation into a nested `find_share_length`
helper function. This encapsulates the search logic and uses explicit
return statements, ensuring the length value is strictly defined. This
satisfies the type checker and improves code readability without
altering the runtime behavior.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index fa9ea6d597095..2c564cc937235 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -43,13 +43,17 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
         skip = ["is", "by", "or", "and"]
         return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip])
 
-    abbrs = []
-    for atom in atoms:
+    def find_share_length(atom: str) -> int:
         for i in range(len(atom), -1, -1):
             if sum(a.startswith(atom[:i]) for a in atoms) > 1:
-                break
-        share = atom[:i]
-        unique = atom[i:]
+                return i
+        return 0
+
+    abbrs = []
+    for atom in atoms:
+        share_len = find_share_length(atom)
+        share = atom[:share_len]
+        unique = atom[share_len:]
         abbrs.append((shorten(share) + shorten(unique)))
     return abbrs
 
-- 
2.52.0

[PATCH v2 19/20] rv/rvgen: fix _fill_states() return type annotation

[Wander Lairson Costa]

The _fill_states() method returns a list of strings, but the type
annotation incorrectly specified str. Update the annotation to
list[str] to match the actual return value.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index 2c564cc937235..de765b8486bd1 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -71,7 +71,7 @@ class ltl2k(generator.Monitor):
         if not self.name:
             self.name = Path(file_path).stem
 
-    def _fill_states(self) -> str:
+    def _fill_states(self) -> list[str]:
         buf = [
             "enum ltl_buchi_state {",
         ]
-- 
2.52.0

[PATCH v2 20/20] rv/rvgen: add missing return type annotations

[Wander Lairson Costa]

Add missing `-> str` return type annotations to code generation
methods in RVGenerator. These methods return strings, and the missing
hints caused errors with static analysis tools.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/rvgen/generator.py | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index ef6c9150f50c6..4b984869a7b3d 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -73,13 +73,13 @@ class RVGenerator:
             return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
         return ""
 
-    def fill_tracepoint_handlers_skel(self):
+    def fill_tracepoint_handlers_skel(self) -> str:
         return "NotImplemented"
 
-    def fill_tracepoint_attach_probe(self):
+    def fill_tracepoint_attach_probe(self) -> str:
         return "NotImplemented"
 
-    def fill_tracepoint_detach_helper(self):
+    def fill_tracepoint_detach_helper(self) -> str:
         return "NotImplemented"
 
     def fill_main_c(self):
@@ -100,19 +100,19 @@ class RVGenerator:
 
         return main_c
 
-    def fill_model_h(self):
+    def fill_model_h(self) -> str:
         return "NotImplemented"
 
-    def fill_monitor_class_type(self):
+    def fill_monitor_class_type(self) -> str:
         return "NotImplemented"
 
-    def fill_monitor_class(self):
+    def fill_monitor_class(self) -> str:
         return "NotImplemented"
 
-    def fill_tracepoint_args_skel(self, tp_type):
+    def fill_tracepoint_args_skel(self, tp_type) -> str:
         return "NotImplemented"
 
-    def fill_monitor_deps(self):
+    def fill_monitor_deps(self) -> str:
         buff = []
         buff.append("	# XXX: add dependencies if there")
         if self.parent:
-- 
2.52.0

Re: [PATCH v2 01/20] rv/rvgen: introduce AutomataError exception class

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Replace the generic except Exception block with a custom AutomataError
> class that inherits from Exception. This provides more precise exception
> handling for automata parsing and validation errors while avoiding
> overly broad exception catches that could mask programming errors like
> SyntaxError or TypeError.
> 
> The AutomataError class is raised when DOT file processing fails due to
> invalid format, I/O errors, or malformed automaton definitions. The
> main entry point catches this specific exception and provides a
> user-friendly error message to stderr before exiting.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Looks very good, thanks.
Now I wonder though why is LTL not included in the change. ltl2ba.py raises a
few ValueError that should probably be treated just like these AutomataError.
You could either create a new exception class or share the same for all model
errors (DA and LTL).

What do you think?

Thanks,
Gabriele

> ---
>  tools/verification/rvgen/__main__.py        |  9 ++++++---
>  tools/verification/rvgen/rvgen/automata.py  | 17 ++++++++++++-----
>  tools/verification/rvgen/rvgen/dot2c.py     |  4 ++--
>  tools/verification/rvgen/rvgen/generator.py |  7 ++-----
>  4 files changed, 22 insertions(+), 15 deletions(-)
> 
> diff --git a/tools/verification/rvgen/__main__.py
> b/tools/verification/rvgen/__main__.py
> index fa6fc1f4de2f7..3bd438f8476ed 100644
> --- a/tools/verification/rvgen/__main__.py
> +++ b/tools/verification/rvgen/__main__.py
> @@ -8,11 +8,15 @@
>  # For further information, see:
>  #   Documentation/trace/rv/da_monitor_synthesis.rst
>  
> +from sys import stderr
> +
> +
>  if __name__ == '__main__':
>      from rvgen.dot2k import dot2k
>      from rvgen.generator import Monitor
>      from rvgen.container import Container
>      from rvgen.ltl2k import ltl2k
> +    from rvgen.automata import AutomataError
>      import argparse
>      import sys
>  
> @@ -51,9 +55,8 @@ if __name__ == '__main__':
>                  sys.exit(1)
>          else:
>              monitor = Container(vars(params))
> -    except Exception as e:
> -        print('Error: '+ str(e))
> -        print("Sorry : :-(")
> +    except AutomataError as e:
> +        print(f"There was an error processing {params.spec}: {e}",
> file=sys.stderr)
>          sys.exit(1)
>  
>      print("Writing the monitor into the directory %s" % monitor.name)
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 3f06aef8d4fdc..6ecd5ccd8f3d3 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -10,6 +10,13 @@
>  
>  import ntpath
>  
> +class AutomataError(Exception):
> +    """Exception raised for errors in automata parsing and validation.
> +
> +    Raised when DOT file processing fails due to invalid format, I/O errors,
> +    or malformed automaton definitions.
> +    """
> +
>  class Automata:
>      """Automata class: Reads a dot file and part it as an automata.
>  
> @@ -32,11 +39,11 @@ class Automata:
>          basename = ntpath.basename(self.__dot_path)
>          if not basename.endswith(".dot") and not basename.endswith(".gv"):
>              print("not a dot file")
> -            raise Exception("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError("not a dot file: %s" % self.__dot_path)
>  
>          model_name = ntpath.splitext(basename)[0]
>          if model_name.__len__() == 0:
> -            raise Exception("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError("not a dot file: %s" % self.__dot_path)
>  
>          return model_name
>  
> @@ -45,8 +52,8 @@ class Automata:
>          dot_lines = []
>          try:
>              dot_file = open(self.__dot_path)
> -        except:
> -            raise Exception("Cannot open the file: %s" % self.__dot_path)
> +        except OSError as exc:
> +            raise AutomataError(f"Cannot open the file: {self.__dot_path}")
> from exc
>  
>          dot_lines = dot_file.read().splitlines()
>          dot_file.close()
> @@ -55,7 +62,7 @@ class Automata:
>          line = dot_lines[cursor].split()
>  
>          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> -            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
> +            raise AutomataError("Not a valid .dot format: %s" %
> self.__dot_path)
>          else:
>              cursor += 1
>          return dot_lines
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index 06a26bf15a7e9..74147ae2942f9 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -13,7 +13,7 @@
>  # For further information, see:
>  #   Documentation/trace/rv/deterministic_automata.rst
>  
> -from .automata import Automata
> +from .automata import Automata, AutomataError
>  
>  class Dot2c(Automata):
>      enum_suffix = ""
> @@ -71,7 +71,7 @@ class Dot2c(Automata):
>              min_type = "unsigned int"
>  
>          if self.states.__len__() > 1000000:
> -            raise Exception("Too many states: %d" % self.states.__len__())
> +            raise AutomataError("Too many states: %d" %
> self.states.__len__())
>  
>          return min_type
>  
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index 3441385c11770..a7bee6b1ea70c 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -51,10 +51,7 @@ class RVGenerator:
>          raise FileNotFoundError("Could not find the rv directory, do you have
> the kernel source installed?")
>  
>      def _read_file(self, path):
> -        try:
> -            fd = open(path, 'r')
> -        except OSError:
> -            raise Exception("Cannot open the file: %s" % path)
> +        fd = open(path, 'r')
>  
>          content = fd.read()
>  
> @@ -65,7 +62,7 @@ class RVGenerator:
>          try:
>              path = os.path.join(self.abs_template_dir, file)
>              return self._read_file(path)
> -        except Exception:
> +        except OSError:
>              # Specific template file not found. Try the generic template file
> in the template/
>              # directory, which is one level up
>              path = os.path.join(self.abs_template_dir, "..", file)

Re: [PATCH v2 07/20] rv/rvgen: fix typos in automata and generator docstring and comments

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Fix two typos in the Automata class documentation that have been
> present since the initial implementation. Fix the class
> docstring: "part it" instead of "parses it". Additionally, a
> comment describing transition labels contained the misspelling
> "lables" instead of "labels".
> 
> Fix a typo in the comment describing the insertion of the initial
> state into the states list: "bein og" should be "beginning of".
> 
> Fix typo in the module docstring: "Abtract" should be "Abstract".
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>


While you're at it there are a few singular/plural inconsistencies, see below.

Other than that it looks good, thanks!

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>


> ---
>  tools/verification/rvgen/rvgen/automata.py  | 6 +++---
>  tools/verification/rvgen/rvgen/generator.py | 2 +-
>  2 files changed, 4 insertions(+), 4 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 1feb5f0c0bc3e..0d7cbd0c634a9 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -18,7 +18,7 @@ class AutomataError(Exception):
>      """
>  
>  class Automata:
> -    """Automata class: Reads a dot file and part it as an automata.
> +    """Automata class: Reads a dot file and parses it as an automata.
>  

Automata is plural, the singular is automaton (you can keep the class name
unchanged): 

+    """Automata class: Reads a dot file and parses it as an automaton.

>      Attributes:
>          dot_file: A dot file with an state_automaton definition.
> @@ -113,7 +113,7 @@ class Automata:
>          states = sorted(set(states))
>          states.remove(initial_state)
>  
> -        # Insert the initial state at the bein og the states
> +        # Insert the initial state at the beginning of the states
>          states.insert(0, initial_state)
>  
>          if not has_final_states:
> @@ -134,7 +134,7 @@ class Automata:
>                  line = self.__dot_lines[cursor].split()
>                  event = line[-2].replace('"','')
>  
> -                # when a transition has more than one lables, they are like
> this
> +                # when a transition has more than one labels, they are like
> this

This should be "more than one label" as singular.

>                  # "local_irq_enable\nhw_local_irq_enable_n"
>                  # so split them.
>  
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index ee75e111feef1..a3fbb1ac74916 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -3,7 +3,7 @@
>  #
>  # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira
> <bristot@kernel.org>
>  #
> -# Abtract class for generating kernel runtime verification monitors from
> specification file
> +# Abstract class for generating kernel runtime verification monitors from
> specification file
>  
>  import platform
>  import os

Re: [PATCH v2 19/20] rv/rvgen: fix _fill_states() return type annotation

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> The _fill_states() method returns a list of strings, but the type
> annotation incorrectly specified str. Update the annotation to
> list[str] to match the actual return value.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---

Looks good, thanks. I would keep all annotation changes together (i.e. squash
with the next patch), but if you prefer this way, I'm fine too.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

>  tools/verification/rvgen/rvgen/ltl2k.py | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index 2c564cc937235..de765b8486bd1 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -71,7 +71,7 @@ class ltl2k(generator.Monitor):
>          if not self.name:
>              self.name = Path(file_path).stem
>  
> -    def _fill_states(self) -> str:
> +    def _fill_states(self) -> list[str]:
>          buf = [
>              "enum ltl_buchi_state {",
>          ]

Re: [PATCH v2 20/20] rv/rvgen: add missing return type annotations

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Add missing `-> str` return type annotations to code generation
> methods in RVGenerator. These methods return strings, and the missing
> hints caused errors with static analysis tools.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> ---
>  tools/verification/rvgen/rvgen/generator.py | 16 ++++++++--------
>  1 file changed, 8 insertions(+), 8 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index ef6c9150f50c6..4b984869a7b3d 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -73,13 +73,13 @@ class RVGenerator:
>              return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
>          return ""
>  
> -    def fill_tracepoint_handlers_skel(self):
> +    def fill_tracepoint_handlers_skel(self) -> str:
>          return "NotImplemented"

Those are the ones that will raise an exception in a later iteration of this,
right? I wonder if we really need to touch them now.
Anyway I'm fine with this if it pleases your tools, thanks.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

>  
> -    def fill_tracepoint_attach_probe(self):
> +    def fill_tracepoint_attach_probe(self) -> str:
>          return "NotImplemented"
>  
> -    def fill_tracepoint_detach_helper(self):
> +    def fill_tracepoint_detach_helper(self) -> str:
>          return "NotImplemented"
>  
>      def fill_main_c(self):
> @@ -100,19 +100,19 @@ class RVGenerator:
>  
>          return main_c
>  
> -    def fill_model_h(self):
> +    def fill_model_h(self) -> str:
>          return "NotImplemented"
>  
> -    def fill_monitor_class_type(self):
> +    def fill_monitor_class_type(self) -> str:
>          return "NotImplemented"
>  
> -    def fill_monitor_class(self):
> +    def fill_monitor_class(self) -> str:
>          return "NotImplemented"
>  
> -    def fill_tracepoint_args_skel(self, tp_type):
> +    def fill_tracepoint_args_skel(self, tp_type) -> str:
>          return "NotImplemented"
>  
> -    def fill_monitor_deps(self):
> +    def fill_monitor_deps(self) -> str:
>          buff = []
>          buff.append("	# XXX: add dependencies if there")
>          if self.parent:

Re: [PATCH v2 03/20] rv/rvgen: replace % string formatting with f-strings

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Replace all instances of percent-style string formatting with
> f-strings across the rvgen codebase. This modernizes the string
> formatting to use Python 3.6+ features, providing clearer and more
> maintainable code while improving runtime performance.
> 
> The conversion handles all formatting cases including simple variable
> substitution, multi-variable formatting, and complex format specifiers.
> Dynamic width formatting is converted from "%*s" to "{var:>{width}}"
> using proper alignment syntax. Template strings for generated C code
> properly escape braces using double-brace syntax to produce literal
> braces in the output.
> 
> F-strings provide approximately 2x performance improvement over percent
> formatting and are the recommended approach in modern Python.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> Reviewed-by: Nam Cao <namcao@linutronix.de>
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---

There's a new one after the rebase, you may want to add this hunk:

diff --git a/tools/verification/rvgen/rvgen/dot2k.py
b/tools/verification/rvgen/rvgen/dot2k.py
index 4bf0db52e626..0d2cdfdf25eb 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -66,7 +66,7 @@ class dot2k(Monitor, Dot2c):
         buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
         buff.append(" */")
         buff.append("")
-        buff.append("#define MONITOR_NAME %s" % (self.name))
+        buff.append(f"#define MONITOR_NAME {self.name}")
         buff.append("")
 
         return buff

---

Thanks,
Gabriele

>  tools/verification/rvgen/__main__.py        |  6 +--
>  tools/verification/rvgen/rvgen/automata.py  |  6 +--
>  tools/verification/rvgen/rvgen/dot2c.py     | 38 ++++++-------
>  tools/verification/rvgen/rvgen/dot2k.py     | 26 ++++-----
>  tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++-----------
>  tools/verification/rvgen/rvgen/ltl2k.py     | 30 +++++------
>  6 files changed, 81 insertions(+), 84 deletions(-)
> 
> diff --git a/tools/verification/rvgen/__main__.py
> b/tools/verification/rvgen/__main__.py
> index 3bd438f8476ed..50b7d4227fb16 100644
> --- a/tools/verification/rvgen/__main__.py
> +++ b/tools/verification/rvgen/__main__.py
> @@ -45,7 +45,7 @@ if __name__ == '__main__':
>  
>      try:
>          if params.subcmd == "monitor":
> -            print("Opening and parsing the specification file %s" %
> params.spec)
> +            print(f"Opening and parsing the specification file
> {params.spec}")
>              if params.monitor_class == "da":
>                  monitor = dot2k(params.spec, params.monitor_type,
> vars(params))
>              elif params.monitor_class == "ltl":
> @@ -59,11 +59,11 @@ if __name__ == '__main__':
>          print(f"There was an error processing {params.spec}: {e}",
> file=sys.stderr)
>          sys.exit(1)
>  
> -    print("Writing the monitor into the directory %s" % monitor.name)
> +    print(f"Writing the monitor into the directory {monitor.name}")
>      monitor.print_files()
>      print("Almost done, checklist")
>      if params.subcmd == "monitor":
> -        print("  - Edit the %s/%s.c to add the instrumentation" %
> (monitor.name, monitor.name))
> +        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())
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 6ecd5ccd8f3d3..bd8c04526be3a 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -39,11 +39,11 @@ class Automata:
>          basename = ntpath.basename(self.__dot_path)
>          if not basename.endswith(".dot") and not basename.endswith(".gv"):
>              print("not a dot file")
> -            raise AutomataError("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError(f"not a dot file: {self.__dot_path}")
>  
>          model_name = ntpath.splitext(basename)[0]
>          if model_name.__len__() == 0:
> -            raise AutomataError("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError(f"not a dot file: {self.__dot_path}")
>  
>          return model_name
>  
> @@ -62,7 +62,7 @@ class Automata:
>          line = dot_lines[cursor].split()
>  
>          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> -            raise AutomataError("Not a valid .dot format: %s" %
> self.__dot_path)
> +            raise AutomataError(f"Not a valid .dot format:
> {self.__dot_path}")
>          else:
>              cursor += 1
>          return dot_lines
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index 74147ae2942f9..6a2ad4fbf7824 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -28,17 +28,17 @@ class Dot2c(Automata):
>  
>      def __get_enum_states_content(self) -> list[str]:
>          buff = []
> -        buff.append("\t%s%s," % (self.initial_state, self.enum_suffix))
> +        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
>          for state in self.states:
>              if state != self.initial_state:
> -                buff.append("\t%s%s," % (state, self.enum_suffix))
> -        buff.append("\tstate_max%s," % (self.enum_suffix))
> +                buff.append(f"\t{state}{self.enum_suffix},")
> +        buff.append(f"\tstate_max{self.enum_suffix},")
>  
>          return buff
>  
>      def format_states_enum(self) -> list[str]:
>          buff = []
> -        buff.append("enum %s {" % self.enum_states_def)
> +        buff.append(f"enum {self.enum_states_def} {{")
>          buff += self.__get_enum_states_content()
>          buff.append("};\n")
>  
> @@ -47,15 +47,15 @@ class Dot2c(Automata):
>      def __get_enum_events_content(self) -> list[str]:
>          buff = []
>          for event in self.events:
> -            buff.append("\t%s%s," % (event, self.enum_suffix))
> +            buff.append(f"\t{event}{self.enum_suffix},")
>  
> -        buff.append("\tevent_max%s," % self.enum_suffix)
> +        buff.append(f"\tevent_max{self.enum_suffix},")
>  
>          return buff
>  
>      def format_events_enum(self) -> list[str]:
>          buff = []
> -        buff.append("enum %s {" % self.enum_events_def)
> +        buff.append(f"enum {self.enum_events_def} {{")
>          buff += self.__get_enum_events_content()
>          buff.append("};\n")
>  
> @@ -71,25 +71,25 @@ class Dot2c(Automata):
>              min_type = "unsigned int"
>  
>          if self.states.__len__() > 1000000:
> -            raise AutomataError("Too many states: %d" %
> self.states.__len__())
> +            raise AutomataError(f"Too many states: {self.states.__len__()}")
>  
>          return min_type
>  
>      def format_automaton_definition(self) -> list[str]:
>          min_type = self.get_minimun_type()
>          buff = []
> -        buff.append("struct %s {" % self.struct_automaton_def)
> -        buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
> -        buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
> -        buff.append("\t%s function[state_max%s][event_max%s];" % (min_type,
> self.enum_suffix, self.enum_suffix))
> -        buff.append("\t%s initial_state;" % min_type)
> -        buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
> +        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}];")
> +        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}];")
>          buff.append("};\n")
>          return buff
>  
>      def format_aut_init_header(self) -> list[str]:
>          buff = []
> -        buff.append("static const struct %s %s = {" %
> (self.struct_automaton_def, self.var_automaton_def))
> +        buff.append(f"static const struct {self.struct_automaton_def}
> {self.var_automaton_def} = {{")
>          return buff
>  
>      def __get_string_vector_per_line_content(self, entries: list[str]) ->
> str:
> @@ -134,9 +134,9 @@ class Dot2c(Automata):
>                      next_state = self.function[x][y] + self.enum_suffix
>  
>                  if linetoolong:
> -                    line += "\t\t\t%s" % next_state
> +                    line += f"\t\t\t{next_state}"
>                  else:
> -                    line += "%*s" % (maxlen, next_state)
> +                    line += f"{next_state:>{maxlen}}"
>                  if y != nr_events-1:
>                      line += ",\n" if linetoolong else ", "
>                  else:
> @@ -180,7 +180,7 @@ class Dot2c(Automata):
>  
>      def format_aut_init_final_states(self) -> list[str]:
>         buff = []
> -       buff.append("\t.final_states = { %s }," %
> self.get_aut_init_final_states())
> +       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()}
> }},")
>  
>         return buff
>  
> @@ -196,7 +196,7 @@ class Dot2c(Automata):
>  
>      def format_invalid_state(self) -> list[str]:
>          buff = []
> -        buff.append("#define %s state_max%s\n" % (self.invalid_state_str,
> self.enum_suffix))
> +        buff.append(f"#define {self.invalid_state_str}
> state_max{self.enum_suffix}\n")
>  
>          return buff
>  
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index 6128fe2384308..6d4151acc9fe3 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -19,7 +19,7 @@ class dot2k(Monitor, Dot2c):
>          self.monitor_type = MonitorType
>          Monitor.__init__(self, extra_params)
>          Dot2c.__init__(self, file_path, extra_params.get("model_name"))
> -        self.enum_suffix = "_%s" % self.name
> +        self.enum_suffix = f"_{self.name}"
>  
>      def fill_monitor_type(self) -> str:
>          return self.monitor_type.upper()
> @@ -27,7 +27,7 @@ class dot2k(Monitor, Dot2c):
>      def fill_tracepoint_handlers_skel(self) -> str:
>          buff = []
>          for event in self.events:
> -            buff.append("static void handle_%s(void *data, /* XXX: fill
> header */)" % event)
> +            buff.append(f"static void handle_{event}(void *data, /* XXX: fill
> header */)")
>              buff.append("{")
>              handle = "handle_event"
>              if self.is_start_event(event):
> @@ -38,9 +38,9 @@ class dot2k(Monitor, Dot2c):
>                  handle = "handle_start_run_event"
>              if self.monitor_type == "per_task":
>                  buff.append("\tstruct task_struct *p = /* XXX: how do I get
> p? */;");
> -                buff.append("\tda_%s(p, %s%s);" % (handle, event,
> self.enum_suffix));
> +                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
>              else:
> -                buff.append("\tda_%s(%s%s);" % (handle, event,
> self.enum_suffix));
> +                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
>              buff.append("}")
>              buff.append("")
>          return '\n'.join(buff)
> @@ -48,20 +48,20 @@ class dot2k(Monitor, Dot2c):
>      def fill_tracepoint_attach_probe(self) -> str:
>          buff = []
>          for event in self.events:
> -            buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint
> */, handle_%s);" % (self.name, event))
> +            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX:
> tracepoint */, handle_{event});")
>          return '\n'.join(buff)
>  
>      def fill_tracepoint_detach_helper(self) -> str:
>          buff = []
>          for event in self.events:
> -            buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint
> */, handle_%s);" % (self.name, event))
> +            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX:
> tracepoint */, handle_{event});")
>          return '\n'.join(buff)
>  
>      def fill_model_h_header(self) -> list[str]:
>          buff = []
>          buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
>          buff.append("/*")
> -        buff.append(" * Automatically generated C representation of %s
> automaton" % (self.name))
> +        buff.append(f" * Automatically generated C representation of
> {self.name} automaton")
>          buff.append(" * For further information about this format, see kernel
> documentation:")
>          buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
>          buff.append(" */")
> @@ -75,10 +75,10 @@ class dot2k(Monitor, Dot2c):
>          #
>          # Adjust the definition names
>          #
> -        self.enum_states_def = "states_%s" % self.name
> -        self.enum_events_def = "events_%s" % self.name
> -        self.struct_automaton_def = "automaton_%s" % self.name
> -        self.var_automaton_def = "automaton_%s" % self.name
> +        self.enum_states_def = f"states_{self.name}"
> +        self.enum_events_def = f"events_{self.name}"
> +        self.struct_automaton_def = f"automaton_{self.name}"
> +        self.var_automaton_def = f"automaton_{self.name}"
>  
>          buff = self.fill_model_h_header()
>          buff += self.format_model()
> @@ -113,8 +113,8 @@ class dot2k(Monitor, Dot2c):
>              tp_args.insert(0, tp_args_id)
>          tp_proto_c = ", ".join([a+b for a,b in tp_args])
>          tp_args_c = ", ".join([b for a,b in tp_args])
> -        buff.append("	     TP_PROTO(%s)," % tp_proto_c)
> -        buff.append("	     TP_ARGS(%s)" % tp_args_c)
> +        buff.append(f"	     TP_PROTO({tp_proto_c}),")
> +        buff.append(f"	     TP_ARGS({tp_args_c})")
>          return '\n'.join(buff)
>  
>      def fill_main_c(self) -> str:
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index af1662e2c20a7..6d16fb68798a7 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -40,7 +40,7 @@ class RVGenerator:
>          if platform.system() != "Linux":
>              raise OSError("I can only run on Linux.")
>  
> -        kernel_path = os.path.join("/lib/modules/%s/build" %
> platform.release(), self.rv_dir)
> +        kernel_path =
> os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
>  
>          # if the current kernel is from a distro this may not be a full
> kernel tree
>          # verify that one of the files we are going to modify is available
> @@ -69,11 +69,11 @@ class RVGenerator:
>              return self._read_file(path)
>  
>      def fill_parent(self):
> -        return "&rv_%s" % self.parent if self.parent else "NULL"
> +        return f"&rv_{self.parent}" if self.parent else "NULL"
>  
>      def fill_include_parent(self):
>          if self.parent:
> -            return "#include <monitors/%s/%s.h>\n" % (self.parent,
> self.parent)
> +            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
>          return ""
>  
>      def fill_tracepoint_handlers_skel(self):
> @@ -119,7 +119,7 @@ class RVGenerator:
>          buff = []
>          buff.append("	# XXX: add dependencies if there")
>          if self.parent:
> -            buff.append("	depends on RV_MON_%s" % self.parent.upper())
> +            buff.append(f"	depends on RV_MON_{self.parent.upper()}")
>              buff.append("	default y")
>          return '\n'.join(buff)
>  
> @@ -145,31 +145,30 @@ class RVGenerator:
>          monitor_class_type = self.fill_monitor_class_type()
>          if self.auto_patch:
>              self._patch_file("rv_trace.h",
> -                            "// Add new monitors based on CONFIG_%s here" %
> monitor_class_type,
> -                            "#include <monitors/%s/%s_trace.h>" % (self.name,
> self.name))
> -            return "  - Patching %s/rv_trace.h, double check the result" %
> self.rv_dir
> +                            f"// Add new monitors based on
> CONFIG_{monitor_class_type} here",
> +                            f"#include
> <monitors/{self.name}/{self.name}_trace.h>")
> +            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the
> result"
>  
> -        return """  - Edit %s/rv_trace.h:
> -Add this line where other tracepoints are included and %s is defined:
> -#include <monitors/%s/%s_trace.h>
> -""" % (self.rv_dir, monitor_class_type, self.name, self.name)
> +        return f"""  - Edit {self.rv_dir}/rv_trace.h:
> +Add this line where other tracepoints are included and {monitor_class_type}
> is defined:
> +#include <monitors/{self.name}/{self.name}_trace.h>
> +"""
>  
>      def _kconfig_marker(self, container=None) -> str:
> -        return "# Add new %smonitors here" % (container + " "
> -                                              if container else "")
> +        return f"# Add new {container + ' ' if container else ''}monitors
> here"
>  
>      def fill_kconfig_tooltip(self):
>          if self.auto_patch:
>              # monitors with a container should stay together in the Kconfig
>              self._patch_file("Kconfig",
>                               self._kconfig_marker(self.parent),
> -                            "source \"kernel/trace/rv/monitors/%s/Kconfig\""
> % (self.name))
> -            return "  - Patching %s/Kconfig, double check the result" %
> self.rv_dir
> +                            f"source
> \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
> +            return f"  - Patching {self.rv_dir}/Kconfig, double check the
> result"
>  
> -        return """  - Edit %s/Kconfig:
> +        return f"""  - Edit {self.rv_dir}/Kconfig:
>  Add this line where other monitors are included:
> -source \"kernel/trace/rv/monitors/%s/Kconfig\"
> -""" % (self.rv_dir, self.name)
> +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
> +"""
>  
>      def fill_makefile_tooltip(self):
>          name = self.name
> @@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\"
>          if self.auto_patch:
>              self._patch_file("Makefile",
>                              "# Add new monitors here",
> -                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" %
> (name_up, name, name))
> -            return "  - Patching %s/Makefile, double check the result" %
> self.rv_dir
> +                            f"obj-$(CONFIG_RV_MON_{name_up}) +=
> monitors/{name}/{name}.o")
> +            return f"  - Patching {self.rv_dir}/Makefile, double check the
> result"
>  
> -        return """  - Edit %s/Makefile:
> +        return f"""  - Edit {self.rv_dir}/Makefile:
>  Add this line where other monitors are included:
> -obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> -""" % (self.rv_dir, name_up, name, name)
> +obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
> +"""
>  
>      def fill_monitor_tooltip(self):
>          if self.auto_patch:
> -            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir,
> self. name)
> -        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)"
> % (self.name, self.rv_dir)
> +            return f"  - Monitor created in
> {self.rv_dir}/monitors/{self.name}"
> +        return f"  - Move {self.name}/ to the kernel's monitor directory
> ({self.rv_dir}/monitors)"
>  
>      def __create_directory(self):
>          path = self.name
> @@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
>          file.close()
>  
>      def _create_file(self, file_name, content):
> -        path = "%s/%s" % (self.name, file_name)
> +        path = f"{self.name}/{file_name}"
>          if self.auto_patch:
>              path = os.path.join(self.rv_dir, "monitors", path)
>          self.__write_file(path, content)
>  
>      def __get_main_name(self):
> -        path = "%s/%s" % (self.name, "main.c")
> +        path = f"{self.name}/main.c"
>          if not os.path.exists(path):
>              return "main.c"
>          return "__main.c"
> @@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
>  
>          self.__create_directory()
>  
> -        path = "%s.c" % self.name
> +        path = f"{self.name}.c"
>          self._create_file(path, main_c)
>  
>          model_h = self.fill_model_h()
> -        path = "%s.h" % self.name
> +        path = f"{self.name}.h"
>          self._create_file(path, model_h)
>  
>          kconfig = self.fill_kconfig()
> @@ -256,5 +255,5 @@ class Monitor(RVGenerator):
>      def print_files(self):
>          super().print_files()
>          trace_h = self.fill_trace_h()
> -        path = "%s_trace.h" % self.name
> +        path = f"{self.name}_trace.h"
>          self._create_file(path, trace_h)
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index b075f98d50c47..fa9ea6d597095 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -73,7 +73,7 @@ class ltl2k(generator.Monitor):
>          ]
>  
>          for node in self.ba:
> -            buf.append("\tS%i," % node.id)
> +            buf.append(f"\tS{node.id},")
>          buf.append("\tRV_NUM_BA_STATES")
>          buf.append("};")
>          buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
> @@ -82,7 +82,7 @@ class ltl2k(generator.Monitor):
>      def _fill_atoms(self):
>          buf = ["enum ltl_atom {"]
>          for a in sorted(self.atoms):
> -            buf.append("\tLTL_%s," % a)
> +            buf.append(f"\tLTL_{a},")
>          buf.append("\tLTL_NUM_ATOM")
>          buf.append("};")
>          buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
> @@ -96,7 +96,7 @@ class ltl2k(generator.Monitor):
>          ]
>  
>          for name in self.atoms_abbr:
> -            buf.append("\t\t\"%s\"," % name)
> +            buf.append(f"\t\t\"{name}\",")
>  
>          buf.extend([
>              "\t};",
> @@ -113,19 +113,19 @@ class ltl2k(generator.Monitor):
>                  continue
>  
>              if isinstance(node.op, ltl2ba.AndOp):
> -                buf.append("\tbool %s = %s && %s;" % (node, node.op.left,
> node.op.right))
> +                buf.append(f"\tbool {node} = {node.op.left} &&
> {node.op.right};")
>                  required_values |= {str(node.op.left), str(node.op.right)}
>              elif isinstance(node.op, ltl2ba.OrOp):
> -                buf.append("\tbool %s = %s || %s;" % (node, node.op.left,
> node.op.right))
> +                buf.append(f"\tbool {node} = {node.op.left} ||
> {node.op.right};")
>                  required_values |= {str(node.op.left), str(node.op.right)}
>              elif isinstance(node.op, ltl2ba.NotOp):
> -                buf.append("\tbool %s = !%s;" % (node, node.op.child))
> +                buf.append(f"\tbool {node} = !{node.op.child};")
>                  required_values.add(str(node.op.child))
>  
>          for atom in self.atoms:
>              if atom.lower() not in required_values:
>                  continue
> -            buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" %
> (atom.lower(), atom))
> +            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon-
> >atoms);")
>  
>          buf.reverse()
>  
> @@ -153,7 +153,7 @@ class ltl2k(generator.Monitor):
>          ])
>  
>          for node in self.ba:
> -            buf.append("\tcase S%i:" % node.id)
> +            buf.append(f"\tcase S{node.id}:")
>  
>              for o in sorted(node.outgoing):
>                  line   = "\t\tif "
> @@ -163,7 +163,7 @@ class ltl2k(generator.Monitor):
>                  lines = break_long_line(line, indent)
>                  buf.extend(lines)
>  
> -                buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
> +                buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
>              buf.append("\t\tbreak;")
>          buf.extend([
>              "\t}",
> @@ -197,7 +197,7 @@ class ltl2k(generator.Monitor):
>              lines = break_long_line(line, indent)
>              buf.extend(lines)
>  
> -            buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
> +            buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
>          buf.append("}")
>          return buf
>  
> @@ -205,23 +205,21 @@ class ltl2k(generator.Monitor):
>          buff = []
>          buff.append("static void handle_example_event(void *data, /* XXX:
> fill header */)")
>          buff.append("{")
> -        buff.append("\tltl_atom_update(task, LTL_%s, true/false);" %
> self.atoms[0])
> +        buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]},
> true/false);")
>          buff.append("}")
>          buff.append("")
>          return '\n'.join(buff)
>  
>      def fill_tracepoint_attach_probe(self):
> -        return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */,
> handle_example_event);" \
> -                % self.name
> +        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> */, handle_example_event);"
>  
>      def fill_tracepoint_detach_helper(self):
> -        return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */,
> handle_sample_event);" \
> -                % self.name
> +        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> */, handle_sample_event);"
>  
>      def fill_atoms_init(self):
>          buff = []
>          for a in self.atoms:
> -            buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
> +            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
>          return '\n'.join(buff)
>  
>      def fill_model_h(self):

Re: [PATCH v2 18/20] rv/rvgen: fix unbound loop variable warning

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Pyright static analysis reports a "possibly unbound variable" warning
> for the loop variable `i` in the `abbreviate_atoms` function. The
> variable is accessed after the inner loop terminates to slice the atom
> string. While the loop logic currently ensures execution, the analyzer
> flags the reliance on the loop variable persisting outside its scope.
> 
> Refactor the prefix length calculation into a nested `find_share_length`
> helper function. This encapsulates the search logic and uses explicit
> return statements, ensuring the length value is strictly defined. This
> satisfies the type checker and improves code readability without
> altering the runtime behavior.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Looks good, that's probably the pythonic way then!

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> ---
>  tools/verification/rvgen/rvgen/ltl2k.py | 14 +++++++++-----
>  1 file changed, 9 insertions(+), 5 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index fa9ea6d597095..2c564cc937235 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -43,13 +43,17 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
>          skip = ["is", "by", "or", "and"]
>          return '_'.join([x[:2] for x in s.lower().split('_') if x not in
> skip])
>  
> -    abbrs = []
> -    for atom in atoms:
> +    def find_share_length(atom: str) -> int:
>          for i in range(len(atom), -1, -1):
>              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> -                break
> -        share = atom[:i]
> -        unique = atom[i:]
> +                return i
> +        return 0
> +
> +    abbrs = []
> +    for atom in atoms:
> +        share_len = find_share_length(atom)
> +        share = atom[:share_len]
> +        unique = atom[share_len:]
>          abbrs.append((shorten(share) + shorten(unique)))
>      return abbrs
>  

Re: [PATCH v2 17/20] rv/rvgen: enforce presence of initial state

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> The __get_state_variables() method parses DOT files to identify the
> automaton's initial state. If the input file lacks a node with the
> required initialization prefix, the initial_state variable is referenced
> before assignment, causing an UnboundLocalError or a generic error
> during the state removal step.
> 
> Initialize the variable explicitly and validate that a start node was
> found after parsing. Raise a descriptive AutomataError if the definition
> is missing to improve debugging and ensure the automaton is valid.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> ---
>  tools/verification/rvgen/rvgen/automata.py | 4 ++++
>  1 file changed, 4 insertions(+)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 270a3d0bf4ce7..cf82f04dbc661 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -105,6 +105,7 @@ class Automata:
>          # wait for node declaration
>          states = []
>          final_states = []
> +        initial_state = ""
>  
>          has_final_states = False
>          cursor = self.__get_cursor_begin_states()
> @@ -131,6 +132,9 @@ class Automata:
>                      final_states.append(state)
>                      has_final_states = True
>  
> +        if not initial_state:
> +            raise AutomataError("The automaton doesn't have an initial
> state")
> +
>          states = sorted(set(states))
>          states.remove(initial_state)
>  

Re: [PATCH v2 16/20] rv/rvgen: extract node marker string to class constant

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Add a node_marker class constant to the Automata class to replace the
> hardcoded "{node" string literal used throughout the DOT file parsing
> logic. This follows the existing pattern established by the init_marker
> and invalid_state_str class constants in the same class.
> 
> The "{node" string is used as a marker to identify node declaration
> lines in DOT files during state variable extraction and cursor
> positioning. Extracting it to a named constant improves code
> maintainability and makes the marker's purpose explicit.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> ---
>  tools/verification/rvgen/rvgen/automata.py | 9 +++++----
>  1 file changed, 5 insertions(+), 4 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 17b012b868531..270a3d0bf4ce7 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -27,6 +27,7 @@ class Automata:
>  
>      invalid_state_str = "INVALID_STATE"
>      init_marker = "__init_"
> +    node_marker = "{node"
>  
>      def __init__(self, file_path, model_name=None):
>          self.__dot_path = file_path
> @@ -72,7 +73,7 @@ class Automata:
>          for cursor, line in enumerate(self.__dot_lines):
>              split_line = line.split()
>  
> -            if len(split_line) and split_line[0] == "{node":
> +            if len(split_line) and split_line[0] == self.node_marker:
>                  return cursor
>  
>          raise AutomataError("Could not find a beginning state")
> @@ -87,9 +88,9 @@ class Automata:
>                  continue
>  
>              if state == 0:
> -                if line[0] == "{node":
> +                if line[0] == self.node_marker:
>                      state = 1
> -            elif line[0] != "{node":
> +            elif line[0] != self.node_marker:
>                  break
>          else:
>              raise AutomataError("Could not find beginning event")
> @@ -111,7 +112,7 @@ class Automata:
>          # process nodes
>          for line in islice(self.__dot_lines, cursor, None):
>              split_line = line.split()
> -            if not split_line or split_line[0] != "{node":
> +            if not split_line or split_line[0] != self.node_marker:
>                  break
>  
>              raw_state = split_line[-1]

Re: [PATCH v2 01/20] rv/rvgen: introduce AutomataError exception class

[Gabriele Monaco]

On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> Replace the generic except Exception block with a custom AutomataError
> class that inherits from Exception. This provides more precise exception
> handling for automata parsing and validation errors while avoiding
> overly broad exception catches that could mask programming errors like
> SyntaxError or TypeError.
> 
> The AutomataError class is raised when DOT file processing fails due to
> invalid format, I/O errors, or malformed automaton definitions. The
> main entry point catches this specific exception and provides a
> user-friendly error message to stderr before exiting.
> 
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
[...]
> ---
> @@ -45,8 +52,8 @@ class Automata:
>          dot_lines = []
>          try:
>              dot_file = open(self.__dot_path)
> -        except:
> -            raise Exception("Cannot open the file: %s" % self.__dot_path)
> +        except OSError as exc:
> +            raise AutomataError(f"Cannot open the file: {self.__dot_path}")
> from exc
> 

You probably don't want to mask all OSError in main.py and allow only this one.
I think it's alright to keep a simpler message for wrong model file (also LTL!),
while throwing a splat in other cases (e.g. missing templates).

But wouldn't it be better to show the error message of the OSError? 99% of the
time it's going to be ENOENT, but could also be some EPERM or who knows what.
I'm fine keeping AutomataError here but would at least propagate the error
message.

Or keep it simple and catch all OSError as well, this one included.

Thanks,
Gabriele

>  
>          dot_lines = dot_file.read().splitlines()
>          dot_file.close()
> @@ -55,7 +62,7 @@ class Automata:
>          line = dot_lines[cursor].split()
>  
>          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> -            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
> +            raise AutomataError("Not a valid .dot format: %s" %
> self.__dot_path)
>          else:
>              cursor += 1
>          return dot_lines
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index 06a26bf15a7e9..74147ae2942f9 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -13,7 +13,7 @@
>  # For further information, see:
>  #   Documentation/trace/rv/deterministic_automata.rst
>  
> -from .automata import Automata
> +from .automata import Automata, AutomataError
>  
>  class Dot2c(Automata):
>      enum_suffix = ""
> @@ -71,7 +71,7 @@ class Dot2c(Automata):
>              min_type = "unsigned int"
>  
>          if self.states.__len__() > 1000000:
> -            raise Exception("Too many states: %d" % self.states.__len__())
> +            raise AutomataError("Too many states: %d" %
> self.states.__len__())
>  
>          return min_type
>  
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index 3441385c11770..a7bee6b1ea70c 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -51,10 +51,7 @@ class RVGenerator:
>          raise FileNotFoundError("Could not find the rv directory, do you have
> the kernel source installed?")
>  
>      def _read_file(self, path):
> -        try:
> -            fd = open(path, 'r')
> -        except OSError:
> -            raise Exception("Cannot open the file: %s" % path)
> +        fd = open(path, 'r')
>  
>          content = fd.read()
>  
> @@ -65,7 +62,7 @@ class RVGenerator:
>          try:
>              path = os.path.join(self.abs_template_dir, file)
>              return self._read_file(path)
> -        except Exception:
> +        except OSError:
>              # Specific template file not found. Try the generic template file
> in the template/
>              # directory, which is one level up
>              path = os.path.join(self.abs_template_dir, "..", file)

Re: [PATCH v2 01/20] rv/rvgen: introduce AutomataError exception class

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 01:08:41PM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > Replace the generic except Exception block with a custom AutomataError
> > class that inherits from Exception. This provides more precise exception
> > handling for automata parsing and validation errors while avoiding
> > overly broad exception catches that could mask programming errors like
> > SyntaxError or TypeError.
> > 
> > The AutomataError class is raised when DOT file processing fails due to
> > invalid format, I/O errors, or malformed automaton definitions. The
> > main entry point catches this specific exception and provides a
> > user-friendly error message to stderr before exiting.
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> [...]
> > ---
> > @@ -45,8 +52,8 @@ class Automata:
> >          dot_lines = []
> >          try:
> >              dot_file = open(self.__dot_path)
> > -        except:
> > -            raise Exception("Cannot open the file: %s" % self.__dot_path)
> > +        except OSError as exc:
> > +            raise AutomataError(f"Cannot open the file: {self.__dot_path}")
> > from exc
> > 
> 
> You probably don't want to mask all OSError in main.py and allow only this one.
> I think it's alright to keep a simpler message for wrong model file (also LTL!),
> while throwing a splat in other cases (e.g. missing templates).
> 
> But wouldn't it be better to show the error message of the OSError? 99% of the
> time it's going to be ENOENT, but could also be some EPERM or who knows what.
> I'm fine keeping AutomataError here but would at least propagate the error
> message.
> 
> Or keep it simple and catch all OSError as well, this one included.

Now that we catch OSError in the main, it makes sense to remove the
try/except clause around open().

> 
> Thanks,
> Gabriele
> 
> >  
> >          dot_lines = dot_file.read().splitlines()
> >          dot_file.close()
> > @@ -55,7 +62,7 @@ class Automata:
> >          line = dot_lines[cursor].split()
> >  
> >          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> > -            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
> > +            raise AutomataError("Not a valid .dot format: %s" %
> > self.__dot_path)
> >          else:
> >              cursor += 1
> >          return dot_lines
> > diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> > b/tools/verification/rvgen/rvgen/dot2c.py
> > index 06a26bf15a7e9..74147ae2942f9 100644
> > --- a/tools/verification/rvgen/rvgen/dot2c.py
> > +++ b/tools/verification/rvgen/rvgen/dot2c.py
> > @@ -13,7 +13,7 @@
> >  # For further information, see:
> >  #   Documentation/trace/rv/deterministic_automata.rst
> >  
> > -from .automata import Automata
> > +from .automata import Automata, AutomataError
> >  
> >  class Dot2c(Automata):
> >      enum_suffix = ""
> > @@ -71,7 +71,7 @@ class Dot2c(Automata):
> >              min_type = "unsigned int"
> >  
> >          if self.states.__len__() > 1000000:
> > -            raise Exception("Too many states: %d" % self.states.__len__())
> > +            raise AutomataError("Too many states: %d" %
> > self.states.__len__())
> >  
> >          return min_type
> >  
> > diff --git a/tools/verification/rvgen/rvgen/generator.py
> > b/tools/verification/rvgen/rvgen/generator.py
> > index 3441385c11770..a7bee6b1ea70c 100644
> > --- a/tools/verification/rvgen/rvgen/generator.py
> > +++ b/tools/verification/rvgen/rvgen/generator.py
> > @@ -51,10 +51,7 @@ class RVGenerator:
> >          raise FileNotFoundError("Could not find the rv directory, do you have
> > the kernel source installed?")
> >  
> >      def _read_file(self, path):
> > -        try:
> > -            fd = open(path, 'r')
> > -        except OSError:
> > -            raise Exception("Cannot open the file: %s" % path)
> > +        fd = open(path, 'r')
> >  
> >          content = fd.read()
> >  
> > @@ -65,7 +62,7 @@ class RVGenerator:
> >          try:
> >              path = os.path.join(self.abs_template_dir, file)
> >              return self._read_file(path)
> > -        except Exception:
> > +        except OSError:
> >              # Specific template file not found. Try the generic template file
> > in the template/
> >              # directory, which is one level up
> >              path = os.path.join(self.abs_template_dir, "..", file)
> 

Re: [PATCH v2 01/20] rv/rvgen: introduce AutomataError exception class

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 07:50:57AM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > Replace the generic except Exception block with a custom AutomataError
> > class that inherits from Exception. This provides more precise exception
> > handling for automata parsing and validation errors while avoiding
> > overly broad exception catches that could mask programming errors like
> > SyntaxError or TypeError.
> > 
> > The AutomataError class is raised when DOT file processing fails due to
> > invalid format, I/O errors, or malformed automaton definitions. The
> > main entry point catches this specific exception and provides a
> > user-friendly error message to stderr before exiting.
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> 
> Looks very good, thanks.
> Now I wonder though why is LTL not included in the change. ltl2ba.py raises a
> few ValueError that should probably be treated just like these AutomataError.
> You could either create a new exception class or share the same for all model
> errors (DA and LTL).
> 
> What do you think?

Good point. I am still learning the code base, I missed it. I will add
AutomataError to the of *ba.py files.

> 
> Thanks,
> Gabriele
> 
> > ---
> >  tools/verification/rvgen/__main__.py        |  9 ++++++---
> >  tools/verification/rvgen/rvgen/automata.py  | 17 ++++++++++++-----
> >  tools/verification/rvgen/rvgen/dot2c.py     |  4 ++--
> >  tools/verification/rvgen/rvgen/generator.py |  7 ++-----
> >  4 files changed, 22 insertions(+), 15 deletions(-)
> > 
> > diff --git a/tools/verification/rvgen/__main__.py
> > b/tools/verification/rvgen/__main__.py
> > index fa6fc1f4de2f7..3bd438f8476ed 100644
> > --- a/tools/verification/rvgen/__main__.py
> > +++ b/tools/verification/rvgen/__main__.py
> > @@ -8,11 +8,15 @@
> >  # For further information, see:
> >  #   Documentation/trace/rv/da_monitor_synthesis.rst
> >  
> > +from sys import stderr
> > +
> > +
> >  if __name__ == '__main__':
> >      from rvgen.dot2k import dot2k
> >      from rvgen.generator import Monitor
> >      from rvgen.container import Container
> >      from rvgen.ltl2k import ltl2k
> > +    from rvgen.automata import AutomataError
> >      import argparse
> >      import sys
> >  
> > @@ -51,9 +55,8 @@ if __name__ == '__main__':
> >                  sys.exit(1)
> >          else:
> >              monitor = Container(vars(params))
> > -    except Exception as e:
> > -        print('Error: '+ str(e))
> > -        print("Sorry : :-(")
> > +    except AutomataError as e:
> > +        print(f"There was an error processing {params.spec}: {e}",
> > file=sys.stderr)
> >          sys.exit(1)
> >  
> >      print("Writing the monitor into the directory %s" % monitor.name)
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 3f06aef8d4fdc..6ecd5ccd8f3d3 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -10,6 +10,13 @@
> >  
> >  import ntpath
> >  
> > +class AutomataError(Exception):
> > +    """Exception raised for errors in automata parsing and validation.
> > +
> > +    Raised when DOT file processing fails due to invalid format, I/O errors,
> > +    or malformed automaton definitions.
> > +    """
> > +
> >  class Automata:
> >      """Automata class: Reads a dot file and part it as an automata.
> >  
> > @@ -32,11 +39,11 @@ class Automata:
> >          basename = ntpath.basename(self.__dot_path)
> >          if not basename.endswith(".dot") and not basename.endswith(".gv"):
> >              print("not a dot file")
> > -            raise Exception("not a dot file: %s" % self.__dot_path)
> > +            raise AutomataError("not a dot file: %s" % self.__dot_path)
> >  
> >          model_name = ntpath.splitext(basename)[0]
> >          if model_name.__len__() == 0:
> > -            raise Exception("not a dot file: %s" % self.__dot_path)
> > +            raise AutomataError("not a dot file: %s" % self.__dot_path)
> >  
> >          return model_name
> >  
> > @@ -45,8 +52,8 @@ class Automata:
> >          dot_lines = []
> >          try:
> >              dot_file = open(self.__dot_path)
> > -        except:
> > -            raise Exception("Cannot open the file: %s" % self.__dot_path)
> > +        except OSError as exc:
> > +            raise AutomataError(f"Cannot open the file: {self.__dot_path}")
> > from exc
> >  
> >          dot_lines = dot_file.read().splitlines()
> >          dot_file.close()
> > @@ -55,7 +62,7 @@ class Automata:
> >          line = dot_lines[cursor].split()
> >  
> >          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> > -            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
> > +            raise AutomataError("Not a valid .dot format: %s" %
> > self.__dot_path)
> >          else:
> >              cursor += 1
> >          return dot_lines
> > diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> > b/tools/verification/rvgen/rvgen/dot2c.py
> > index 06a26bf15a7e9..74147ae2942f9 100644
> > --- a/tools/verification/rvgen/rvgen/dot2c.py
> > +++ b/tools/verification/rvgen/rvgen/dot2c.py
> > @@ -13,7 +13,7 @@
> >  # For further information, see:
> >  #   Documentation/trace/rv/deterministic_automata.rst
> >  
> > -from .automata import Automata
> > +from .automata import Automata, AutomataError
> >  
> >  class Dot2c(Automata):
> >      enum_suffix = ""
> > @@ -71,7 +71,7 @@ class Dot2c(Automata):
> >              min_type = "unsigned int"
> >  
> >          if self.states.__len__() > 1000000:
> > -            raise Exception("Too many states: %d" % self.states.__len__())
> > +            raise AutomataError("Too many states: %d" %
> > self.states.__len__())
> >  
> >          return min_type
> >  
> > diff --git a/tools/verification/rvgen/rvgen/generator.py
> > b/tools/verification/rvgen/rvgen/generator.py
> > index 3441385c11770..a7bee6b1ea70c 100644
> > --- a/tools/verification/rvgen/rvgen/generator.py
> > +++ b/tools/verification/rvgen/rvgen/generator.py
> > @@ -51,10 +51,7 @@ class RVGenerator:
> >          raise FileNotFoundError("Could not find the rv directory, do you have
> > the kernel source installed?")
> >  
> >      def _read_file(self, path):
> > -        try:
> > -            fd = open(path, 'r')
> > -        except OSError:
> > -            raise Exception("Cannot open the file: %s" % path)
> > +        fd = open(path, 'r')
> >  
> >          content = fd.read()
> >  
> > @@ -65,7 +62,7 @@ class RVGenerator:
> >          try:
> >              path = os.path.join(self.abs_template_dir, file)
> >              return self._read_file(path)
> > -        except Exception:
> > +        except OSError:
> >              # Specific template file not found. Try the generic template file
> > in the template/
> >              # directory, which is one level up
> >              path = os.path.join(self.abs_template_dir, "..", file)

Re: [PATCH v2 03/20] rv/rvgen: replace % string formatting with f-strings

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 12:37:13PM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > Replace all instances of percent-style string formatting with
> > f-strings across the rvgen codebase. This modernizes the string
> > formatting to use Python 3.6+ features, providing clearer and more
> > maintainable code while improving runtime performance.
> > 
> > The conversion handles all formatting cases including simple variable
> > substitution, multi-variable formatting, and complex format specifiers.
> > Dynamic width formatting is converted from "%*s" to "{var:>{width}}"
> > using proper alignment syntax. Template strings for generated C code
> > properly escape braces using double-brace syntax to produce literal
> > braces in the output.
> > 
> > F-strings provide approximately 2x performance improvement over percent
> > formatting and are the recommended approach in modern Python.
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > Reviewed-by: Nam Cao <namcao@linutronix.de>
> > Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> > ---
> 
> There's a new one after the rebase, you may want to add this hunk:
> 
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index 4bf0db52e626..0d2cdfdf25eb 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -66,7 +66,7 @@ class dot2k(Monitor, Dot2c):
>          buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
>          buff.append(" */")
>          buff.append("")
> -        buff.append("#define MONITOR_NAME %s" % (self.name))
> +        buff.append(f"#define MONITOR_NAME {self.name}")
>          buff.append("")
>  
>          return buff

Ah, thanks! I will update the patch.

> 
> ---
> 
> Thanks,
> Gabriele
> 
> >  tools/verification/rvgen/__main__.py        |  6 +--
> >  tools/verification/rvgen/rvgen/automata.py  |  6 +--
> >  tools/verification/rvgen/rvgen/dot2c.py     | 38 ++++++-------
> >  tools/verification/rvgen/rvgen/dot2k.py     | 26 ++++-----
> >  tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++-----------
> >  tools/verification/rvgen/rvgen/ltl2k.py     | 30 +++++------
> >  6 files changed, 81 insertions(+), 84 deletions(-)
> > 
> > diff --git a/tools/verification/rvgen/__main__.py
> > b/tools/verification/rvgen/__main__.py
> > index 3bd438f8476ed..50b7d4227fb16 100644
> > --- a/tools/verification/rvgen/__main__.py
> > +++ b/tools/verification/rvgen/__main__.py
> > @@ -45,7 +45,7 @@ if __name__ == '__main__':
> >  
> >      try:
> >          if params.subcmd == "monitor":
> > -            print("Opening and parsing the specification file %s" %
> > params.spec)
> > +            print(f"Opening and parsing the specification file
> > {params.spec}")
> >              if params.monitor_class == "da":
> >                  monitor = dot2k(params.spec, params.monitor_type,
> > vars(params))
> >              elif params.monitor_class == "ltl":
> > @@ -59,11 +59,11 @@ if __name__ == '__main__':
> >          print(f"There was an error processing {params.spec}: {e}",
> > file=sys.stderr)
> >          sys.exit(1)
> >  
> > -    print("Writing the monitor into the directory %s" % monitor.name)
> > +    print(f"Writing the monitor into the directory {monitor.name}")
> >      monitor.print_files()
> >      print("Almost done, checklist")
> >      if params.subcmd == "monitor":
> > -        print("  - Edit the %s/%s.c to add the instrumentation" %
> > (monitor.name, monitor.name))
> > +        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())
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 6ecd5ccd8f3d3..bd8c04526be3a 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -39,11 +39,11 @@ class Automata:
> >          basename = ntpath.basename(self.__dot_path)
> >          if not basename.endswith(".dot") and not basename.endswith(".gv"):
> >              print("not a dot file")
> > -            raise AutomataError("not a dot file: %s" % self.__dot_path)
> > +            raise AutomataError(f"not a dot file: {self.__dot_path}")
> >  
> >          model_name = ntpath.splitext(basename)[0]
> >          if model_name.__len__() == 0:
> > -            raise AutomataError("not a dot file: %s" % self.__dot_path)
> > +            raise AutomataError(f"not a dot file: {self.__dot_path}")
> >  
> >          return model_name
> >  
> > @@ -62,7 +62,7 @@ class Automata:
> >          line = dot_lines[cursor].split()
> >  
> >          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> > -            raise AutomataError("Not a valid .dot format: %s" %
> > self.__dot_path)
> > +            raise AutomataError(f"Not a valid .dot format:
> > {self.__dot_path}")
> >          else:
> >              cursor += 1
> >          return dot_lines
> > diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> > b/tools/verification/rvgen/rvgen/dot2c.py
> > index 74147ae2942f9..6a2ad4fbf7824 100644
> > --- a/tools/verification/rvgen/rvgen/dot2c.py
> > +++ b/tools/verification/rvgen/rvgen/dot2c.py
> > @@ -28,17 +28,17 @@ class Dot2c(Automata):
> >  
> >      def __get_enum_states_content(self) -> list[str]:
> >          buff = []
> > -        buff.append("\t%s%s," % (self.initial_state, self.enum_suffix))
> > +        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
> >          for state in self.states:
> >              if state != self.initial_state:
> > -                buff.append("\t%s%s," % (state, self.enum_suffix))
> > -        buff.append("\tstate_max%s," % (self.enum_suffix))
> > +                buff.append(f"\t{state}{self.enum_suffix},")
> > +        buff.append(f"\tstate_max{self.enum_suffix},")
> >  
> >          return buff
> >  
> >      def format_states_enum(self) -> list[str]:
> >          buff = []
> > -        buff.append("enum %s {" % self.enum_states_def)
> > +        buff.append(f"enum {self.enum_states_def} {{")
> >          buff += self.__get_enum_states_content()
> >          buff.append("};\n")
> >  
> > @@ -47,15 +47,15 @@ class Dot2c(Automata):
> >      def __get_enum_events_content(self) -> list[str]:
> >          buff = []
> >          for event in self.events:
> > -            buff.append("\t%s%s," % (event, self.enum_suffix))
> > +            buff.append(f"\t{event}{self.enum_suffix},")
> >  
> > -        buff.append("\tevent_max%s," % self.enum_suffix)
> > +        buff.append(f"\tevent_max{self.enum_suffix},")
> >  
> >          return buff
> >  
> >      def format_events_enum(self) -> list[str]:
> >          buff = []
> > -        buff.append("enum %s {" % self.enum_events_def)
> > +        buff.append(f"enum {self.enum_events_def} {{")
> >          buff += self.__get_enum_events_content()
> >          buff.append("};\n")
> >  
> > @@ -71,25 +71,25 @@ class Dot2c(Automata):
> >              min_type = "unsigned int"
> >  
> >          if self.states.__len__() > 1000000:
> > -            raise AutomataError("Too many states: %d" %
> > self.states.__len__())
> > +            raise AutomataError(f"Too many states: {self.states.__len__()}")
> >  
> >          return min_type
> >  
> >      def format_automaton_definition(self) -> list[str]:
> >          min_type = self.get_minimun_type()
> >          buff = []
> > -        buff.append("struct %s {" % self.struct_automaton_def)
> > -        buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
> > -        buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
> > -        buff.append("\t%s function[state_max%s][event_max%s];" % (min_type,
> > self.enum_suffix, self.enum_suffix))
> > -        buff.append("\t%s initial_state;" % min_type)
> > -        buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
> > +        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}];")
> > +        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}];")
> >          buff.append("};\n")
> >          return buff
> >  
> >      def format_aut_init_header(self) -> list[str]:
> >          buff = []
> > -        buff.append("static const struct %s %s = {" %
> > (self.struct_automaton_def, self.var_automaton_def))
> > +        buff.append(f"static const struct {self.struct_automaton_def}
> > {self.var_automaton_def} = {{")
> >          return buff
> >  
> >      def __get_string_vector_per_line_content(self, entries: list[str]) ->
> > str:
> > @@ -134,9 +134,9 @@ class Dot2c(Automata):
> >                      next_state = self.function[x][y] + self.enum_suffix
> >  
> >                  if linetoolong:
> > -                    line += "\t\t\t%s" % next_state
> > +                    line += f"\t\t\t{next_state}"
> >                  else:
> > -                    line += "%*s" % (maxlen, next_state)
> > +                    line += f"{next_state:>{maxlen}}"
> >                  if y != nr_events-1:
> >                      line += ",\n" if linetoolong else ", "
> >                  else:
> > @@ -180,7 +180,7 @@ class Dot2c(Automata):
> >  
> >      def format_aut_init_final_states(self) -> list[str]:
> >         buff = []
> > -       buff.append("\t.final_states = { %s }," %
> > self.get_aut_init_final_states())
> > +       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()}
> > }},")
> >  
> >         return buff
> >  
> > @@ -196,7 +196,7 @@ class Dot2c(Automata):
> >  
> >      def format_invalid_state(self) -> list[str]:
> >          buff = []
> > -        buff.append("#define %s state_max%s\n" % (self.invalid_state_str,
> > self.enum_suffix))
> > +        buff.append(f"#define {self.invalid_state_str}
> > state_max{self.enum_suffix}\n")
> >  
> >          return buff
> >  
> > diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> > b/tools/verification/rvgen/rvgen/dot2k.py
> > index 6128fe2384308..6d4151acc9fe3 100644
> > --- a/tools/verification/rvgen/rvgen/dot2k.py
> > +++ b/tools/verification/rvgen/rvgen/dot2k.py
> > @@ -19,7 +19,7 @@ class dot2k(Monitor, Dot2c):
> >          self.monitor_type = MonitorType
> >          Monitor.__init__(self, extra_params)
> >          Dot2c.__init__(self, file_path, extra_params.get("model_name"))
> > -        self.enum_suffix = "_%s" % self.name
> > +        self.enum_suffix = f"_{self.name}"
> >  
> >      def fill_monitor_type(self) -> str:
> >          return self.monitor_type.upper()
> > @@ -27,7 +27,7 @@ class dot2k(Monitor, Dot2c):
> >      def fill_tracepoint_handlers_skel(self) -> str:
> >          buff = []
> >          for event in self.events:
> > -            buff.append("static void handle_%s(void *data, /* XXX: fill
> > header */)" % event)
> > +            buff.append(f"static void handle_{event}(void *data, /* XXX: fill
> > header */)")
> >              buff.append("{")
> >              handle = "handle_event"
> >              if self.is_start_event(event):
> > @@ -38,9 +38,9 @@ class dot2k(Monitor, Dot2c):
> >                  handle = "handle_start_run_event"
> >              if self.monitor_type == "per_task":
> >                  buff.append("\tstruct task_struct *p = /* XXX: how do I get
> > p? */;");
> > -                buff.append("\tda_%s(p, %s%s);" % (handle, event,
> > self.enum_suffix));
> > +                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
> >              else:
> > -                buff.append("\tda_%s(%s%s);" % (handle, event,
> > self.enum_suffix));
> > +                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
> >              buff.append("}")
> >              buff.append("")
> >          return '\n'.join(buff)
> > @@ -48,20 +48,20 @@ class dot2k(Monitor, Dot2c):
> >      def fill_tracepoint_attach_probe(self) -> str:
> >          buff = []
> >          for event in self.events:
> > -            buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint
> > */, handle_%s);" % (self.name, event))
> > +            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX:
> > tracepoint */, handle_{event});")
> >          return '\n'.join(buff)
> >  
> >      def fill_tracepoint_detach_helper(self) -> str:
> >          buff = []
> >          for event in self.events:
> > -            buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint
> > */, handle_%s);" % (self.name, event))
> > +            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX:
> > tracepoint */, handle_{event});")
> >          return '\n'.join(buff)
> >  
> >      def fill_model_h_header(self) -> list[str]:
> >          buff = []
> >          buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
> >          buff.append("/*")
> > -        buff.append(" * Automatically generated C representation of %s
> > automaton" % (self.name))
> > +        buff.append(f" * Automatically generated C representation of
> > {self.name} automaton")
> >          buff.append(" * For further information about this format, see kernel
> > documentation:")
> >          buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
> >          buff.append(" */")
> > @@ -75,10 +75,10 @@ class dot2k(Monitor, Dot2c):
> >          #
> >          # Adjust the definition names
> >          #
> > -        self.enum_states_def = "states_%s" % self.name
> > -        self.enum_events_def = "events_%s" % self.name
> > -        self.struct_automaton_def = "automaton_%s" % self.name
> > -        self.var_automaton_def = "automaton_%s" % self.name
> > +        self.enum_states_def = f"states_{self.name}"
> > +        self.enum_events_def = f"events_{self.name}"
> > +        self.struct_automaton_def = f"automaton_{self.name}"
> > +        self.var_automaton_def = f"automaton_{self.name}"
> >  
> >          buff = self.fill_model_h_header()
> >          buff += self.format_model()
> > @@ -113,8 +113,8 @@ class dot2k(Monitor, Dot2c):
> >              tp_args.insert(0, tp_args_id)
> >          tp_proto_c = ", ".join([a+b for a,b in tp_args])
> >          tp_args_c = ", ".join([b for a,b in tp_args])
> > -        buff.append("	     TP_PROTO(%s)," % tp_proto_c)
> > -        buff.append("	     TP_ARGS(%s)" % tp_args_c)
> > +        buff.append(f"	     TP_PROTO({tp_proto_c}),")
> > +        buff.append(f"	     TP_ARGS({tp_args_c})")
> >          return '\n'.join(buff)
> >  
> >      def fill_main_c(self) -> str:
> > diff --git a/tools/verification/rvgen/rvgen/generator.py
> > b/tools/verification/rvgen/rvgen/generator.py
> > index af1662e2c20a7..6d16fb68798a7 100644
> > --- a/tools/verification/rvgen/rvgen/generator.py
> > +++ b/tools/verification/rvgen/rvgen/generator.py
> > @@ -40,7 +40,7 @@ class RVGenerator:
> >          if platform.system() != "Linux":
> >              raise OSError("I can only run on Linux.")
> >  
> > -        kernel_path = os.path.join("/lib/modules/%s/build" %
> > platform.release(), self.rv_dir)
> > +        kernel_path =
> > os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
> >  
> >          # if the current kernel is from a distro this may not be a full
> > kernel tree
> >          # verify that one of the files we are going to modify is available
> > @@ -69,11 +69,11 @@ class RVGenerator:
> >              return self._read_file(path)
> >  
> >      def fill_parent(self):
> > -        return "&rv_%s" % self.parent if self.parent else "NULL"
> > +        return f"&rv_{self.parent}" if self.parent else "NULL"
> >  
> >      def fill_include_parent(self):
> >          if self.parent:
> > -            return "#include <monitors/%s/%s.h>\n" % (self.parent,
> > self.parent)
> > +            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
> >          return ""
> >  
> >      def fill_tracepoint_handlers_skel(self):
> > @@ -119,7 +119,7 @@ class RVGenerator:
> >          buff = []
> >          buff.append("	# XXX: add dependencies if there")
> >          if self.parent:
> > -            buff.append("	depends on RV_MON_%s" % self.parent.upper())
> > +            buff.append(f"	depends on RV_MON_{self.parent.upper()}")
> >              buff.append("	default y")
> >          return '\n'.join(buff)
> >  
> > @@ -145,31 +145,30 @@ class RVGenerator:
> >          monitor_class_type = self.fill_monitor_class_type()
> >          if self.auto_patch:
> >              self._patch_file("rv_trace.h",
> > -                            "// Add new monitors based on CONFIG_%s here" %
> > monitor_class_type,
> > -                            "#include <monitors/%s/%s_trace.h>" % (self.name,
> > self.name))
> > -            return "  - Patching %s/rv_trace.h, double check the result" %
> > self.rv_dir
> > +                            f"// Add new monitors based on
> > CONFIG_{monitor_class_type} here",
> > +                            f"#include
> > <monitors/{self.name}/{self.name}_trace.h>")
> > +            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the
> > result"
> >  
> > -        return """  - Edit %s/rv_trace.h:
> > -Add this line where other tracepoints are included and %s is defined:
> > -#include <monitors/%s/%s_trace.h>
> > -""" % (self.rv_dir, monitor_class_type, self.name, self.name)
> > +        return f"""  - Edit {self.rv_dir}/rv_trace.h:
> > +Add this line where other tracepoints are included and {monitor_class_type}
> > is defined:
> > +#include <monitors/{self.name}/{self.name}_trace.h>
> > +"""
> >  
> >      def _kconfig_marker(self, container=None) -> str:
> > -        return "# Add new %smonitors here" % (container + " "
> > -                                              if container else "")
> > +        return f"# Add new {container + ' ' if container else ''}monitors
> > here"
> >  
> >      def fill_kconfig_tooltip(self):
> >          if self.auto_patch:
> >              # monitors with a container should stay together in the Kconfig
> >              self._patch_file("Kconfig",
> >                               self._kconfig_marker(self.parent),
> > -                            "source \"kernel/trace/rv/monitors/%s/Kconfig\""
> > % (self.name))
> > -            return "  - Patching %s/Kconfig, double check the result" %
> > self.rv_dir
> > +                            f"source
> > \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
> > +            return f"  - Patching {self.rv_dir}/Kconfig, double check the
> > result"
> >  
> > -        return """  - Edit %s/Kconfig:
> > +        return f"""  - Edit {self.rv_dir}/Kconfig:
> >  Add this line where other monitors are included:
> > -source \"kernel/trace/rv/monitors/%s/Kconfig\"
> > -""" % (self.rv_dir, self.name)
> > +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
> > +"""
> >  
> >      def fill_makefile_tooltip(self):
> >          name = self.name
> > @@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\"
> >          if self.auto_patch:
> >              self._patch_file("Makefile",
> >                              "# Add new monitors here",
> > -                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" %
> > (name_up, name, name))
> > -            return "  - Patching %s/Makefile, double check the result" %
> > self.rv_dir
> > +                            f"obj-$(CONFIG_RV_MON_{name_up}) +=
> > monitors/{name}/{name}.o")
> > +            return f"  - Patching {self.rv_dir}/Makefile, double check the
> > result"
> >  
> > -        return """  - Edit %s/Makefile:
> > +        return f"""  - Edit {self.rv_dir}/Makefile:
> >  Add this line where other monitors are included:
> > -obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> > -""" % (self.rv_dir, name_up, name, name)
> > +obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
> > +"""
> >  
> >      def fill_monitor_tooltip(self):
> >          if self.auto_patch:
> > -            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir,
> > self. name)
> > -        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)"
> > % (self.name, self.rv_dir)
> > +            return f"  - Monitor created in
> > {self.rv_dir}/monitors/{self.name}"
> > +        return f"  - Move {self.name}/ to the kernel's monitor directory
> > ({self.rv_dir}/monitors)"
> >  
> >      def __create_directory(self):
> >          path = self.name
> > @@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> >          file.close()
> >  
> >      def _create_file(self, file_name, content):
> > -        path = "%s/%s" % (self.name, file_name)
> > +        path = f"{self.name}/{file_name}"
> >          if self.auto_patch:
> >              path = os.path.join(self.rv_dir, "monitors", path)
> >          self.__write_file(path, content)
> >  
> >      def __get_main_name(self):
> > -        path = "%s/%s" % (self.name, "main.c")
> > +        path = f"{self.name}/main.c"
> >          if not os.path.exists(path):
> >              return "main.c"
> >          return "__main.c"
> > @@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
> >  
> >          self.__create_directory()
> >  
> > -        path = "%s.c" % self.name
> > +        path = f"{self.name}.c"
> >          self._create_file(path, main_c)
> >  
> >          model_h = self.fill_model_h()
> > -        path = "%s.h" % self.name
> > +        path = f"{self.name}.h"
> >          self._create_file(path, model_h)
> >  
> >          kconfig = self.fill_kconfig()
> > @@ -256,5 +255,5 @@ class Monitor(RVGenerator):
> >      def print_files(self):
> >          super().print_files()
> >          trace_h = self.fill_trace_h()
> > -        path = "%s_trace.h" % self.name
> > +        path = f"{self.name}_trace.h"
> >          self._create_file(path, trace_h)
> > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > b/tools/verification/rvgen/rvgen/ltl2k.py
> > index b075f98d50c47..fa9ea6d597095 100644
> > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > @@ -73,7 +73,7 @@ class ltl2k(generator.Monitor):
> >          ]
> >  
> >          for node in self.ba:
> > -            buf.append("\tS%i," % node.id)
> > +            buf.append(f"\tS{node.id},")
> >          buf.append("\tRV_NUM_BA_STATES")
> >          buf.append("};")
> >          buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
> > @@ -82,7 +82,7 @@ class ltl2k(generator.Monitor):
> >      def _fill_atoms(self):
> >          buf = ["enum ltl_atom {"]
> >          for a in sorted(self.atoms):
> > -            buf.append("\tLTL_%s," % a)
> > +            buf.append(f"\tLTL_{a},")
> >          buf.append("\tLTL_NUM_ATOM")
> >          buf.append("};")
> >          buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
> > @@ -96,7 +96,7 @@ class ltl2k(generator.Monitor):
> >          ]
> >  
> >          for name in self.atoms_abbr:
> > -            buf.append("\t\t\"%s\"," % name)
> > +            buf.append(f"\t\t\"{name}\",")
> >  
> >          buf.extend([
> >              "\t};",
> > @@ -113,19 +113,19 @@ class ltl2k(generator.Monitor):
> >                  continue
> >  
> >              if isinstance(node.op, ltl2ba.AndOp):
> > -                buf.append("\tbool %s = %s && %s;" % (node, node.op.left,
> > node.op.right))
> > +                buf.append(f"\tbool {node} = {node.op.left} &&
> > {node.op.right};")
> >                  required_values |= {str(node.op.left), str(node.op.right)}
> >              elif isinstance(node.op, ltl2ba.OrOp):
> > -                buf.append("\tbool %s = %s || %s;" % (node, node.op.left,
> > node.op.right))
> > +                buf.append(f"\tbool {node} = {node.op.left} ||
> > {node.op.right};")
> >                  required_values |= {str(node.op.left), str(node.op.right)}
> >              elif isinstance(node.op, ltl2ba.NotOp):
> > -                buf.append("\tbool %s = !%s;" % (node, node.op.child))
> > +                buf.append(f"\tbool {node} = !{node.op.child};")
> >                  required_values.add(str(node.op.child))
> >  
> >          for atom in self.atoms:
> >              if atom.lower() not in required_values:
> >                  continue
> > -            buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" %
> > (atom.lower(), atom))
> > +            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon-
> > >atoms);")
> >  
> >          buf.reverse()
> >  
> > @@ -153,7 +153,7 @@ class ltl2k(generator.Monitor):
> >          ])
> >  
> >          for node in self.ba:
> > -            buf.append("\tcase S%i:" % node.id)
> > +            buf.append(f"\tcase S{node.id}:")
> >  
> >              for o in sorted(node.outgoing):
> >                  line   = "\t\tif "
> > @@ -163,7 +163,7 @@ class ltl2k(generator.Monitor):
> >                  lines = break_long_line(line, indent)
> >                  buf.extend(lines)
> >  
> > -                buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
> > +                buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
> >              buf.append("\t\tbreak;")
> >          buf.extend([
> >              "\t}",
> > @@ -197,7 +197,7 @@ class ltl2k(generator.Monitor):
> >              lines = break_long_line(line, indent)
> >              buf.extend(lines)
> >  
> > -            buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
> > +            buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
> >          buf.append("}")
> >          return buf
> >  
> > @@ -205,23 +205,21 @@ class ltl2k(generator.Monitor):
> >          buff = []
> >          buff.append("static void handle_example_event(void *data, /* XXX:
> > fill header */)")
> >          buff.append("{")
> > -        buff.append("\tltl_atom_update(task, LTL_%s, true/false);" %
> > self.atoms[0])
> > +        buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]},
> > true/false);")
> >          buff.append("}")
> >          buff.append("")
> >          return '\n'.join(buff)
> >  
> >      def fill_tracepoint_attach_probe(self):
> > -        return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */,
> > handle_example_event);" \
> > -                % self.name
> > +        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> > */, handle_example_event);"
> >  
> >      def fill_tracepoint_detach_helper(self):
> > -        return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */,
> > handle_sample_event);" \
> > -                % self.name
> > +        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint
> > */, handle_sample_event);"
> >  
> >      def fill_atoms_init(self):
> >          buff = []
> >          for a in self.atoms:
> > -            buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
> > +            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
> >          return '\n'.join(buff)
> >  
> >      def fill_model_h(self):

Re: [PATCH v2 19/20] rv/rvgen: fix _fill_states() return type annotation

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 08:24:11AM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > The _fill_states() method returns a list of strings, but the type
> > annotation incorrectly specified str. Update the annotation to
> > list[str] to match the actual return value.
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > ---
> 
> Looks good, thanks. I would keep all annotation changes together (i.e. squash
> with the next patch), but if you prefer this way, I'm fine too.
> 

I don't have strong feelings either way. Feel free to squash them.

> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> 
> >  tools/verification/rvgen/rvgen/ltl2k.py | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> > 
> > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > b/tools/verification/rvgen/rvgen/ltl2k.py
> > index 2c564cc937235..de765b8486bd1 100644
> > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > @@ -71,7 +71,7 @@ class ltl2k(generator.Monitor):
> >          if not self.name:
> >              self.name = Path(file_path).stem
> >  
> > -    def _fill_states(self) -> str:
> > +    def _fill_states(self) -> list[str]:
> >          buf = [
> >              "enum ltl_buchi_state {",
> >          ]
> 

Re: [PATCH v2 07/20] rv/rvgen: fix typos in automata and generator docstring and comments

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 08:03:16AM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > Fix two typos in the Automata class documentation that have been
> > present since the initial implementation. Fix the class
> > docstring: "part it" instead of "parses it". Additionally, a
> > comment describing transition labels contained the misspelling
> > "lables" instead of "labels".
> > 
> > Fix a typo in the comment describing the insertion of the initial
> > state into the states list: "bein og" should be "beginning of".
> > 
> > Fix typo in the module docstring: "Abtract" should be "Abstract".
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> 
> 
> While you're at it there are a few singular/plural inconsistencies, see below.

Okie dokie. I will update the patch

> 
> Other than that it looks good, thanks!
> 
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> 
> 
> > ---
> >  tools/verification/rvgen/rvgen/automata.py  | 6 +++---
> >  tools/verification/rvgen/rvgen/generator.py | 2 +-
> >  2 files changed, 4 insertions(+), 4 deletions(-)
> > 
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 1feb5f0c0bc3e..0d7cbd0c634a9 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -18,7 +18,7 @@ class AutomataError(Exception):
> >      """
> >  
> >  class Automata:
> > -    """Automata class: Reads a dot file and part it as an automata.
> > +    """Automata class: Reads a dot file and parses it as an automata.
> >  
> 
> Automata is plural, the singular is automaton (you can keep the class name
> unchanged): 
> 
> +    """Automata class: Reads a dot file and parses it as an automaton.
> 
> >      Attributes:
> >          dot_file: A dot file with an state_automaton definition.
> > @@ -113,7 +113,7 @@ class Automata:
> >          states = sorted(set(states))
> >          states.remove(initial_state)
> >  
> > -        # Insert the initial state at the bein og the states
> > +        # Insert the initial state at the beginning of the states
> >          states.insert(0, initial_state)
> >  
> >          if not has_final_states:
> > @@ -134,7 +134,7 @@ class Automata:
> >                  line = self.__dot_lines[cursor].split()
> >                  event = line[-2].replace('"','')
> >  
> > -                # when a transition has more than one lables, they are like
> > this
> > +                # when a transition has more than one labels, they are like
> > this
> 
> This should be "more than one label" as singular.
> 
> >                  # "local_irq_enable\nhw_local_irq_enable_n"
> >                  # so split them.
> >  
> > diff --git a/tools/verification/rvgen/rvgen/generator.py
> > b/tools/verification/rvgen/rvgen/generator.py
> > index ee75e111feef1..a3fbb1ac74916 100644
> > --- a/tools/verification/rvgen/rvgen/generator.py
> > +++ b/tools/verification/rvgen/rvgen/generator.py
> > @@ -3,7 +3,7 @@
> >  #
> >  # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira
> > <bristot@kernel.org>
> >  #
> > -# Abtract class for generating kernel runtime verification monitors from
> > specification file
> > +# Abstract class for generating kernel runtime verification monitors from
> > specification file
> >  
> >  import platform
> >  import os
> 

Re: [PATCH v2 20/20] rv/rvgen: add missing return type annotations

[Wander Lairson Costa]

On Thu, Feb 05, 2026 at 08:24:40AM +0100, Gabriele Monaco wrote:
> On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> > Add missing `-> str` return type annotations to code generation
> > methods in RVGenerator. These methods return strings, and the missing
> > hints caused errors with static analysis tools.
> > 
> > Signed-off-by: Wander Lairson Costa <wander@redhat.com>
> > ---
> >  tools/verification/rvgen/rvgen/generator.py | 16 ++++++++--------
> >  1 file changed, 8 insertions(+), 8 deletions(-)
> > 
> > diff --git a/tools/verification/rvgen/rvgen/generator.py
> > b/tools/verification/rvgen/rvgen/generator.py
> > index ef6c9150f50c6..4b984869a7b3d 100644
> > --- a/tools/verification/rvgen/rvgen/generator.py
> > +++ b/tools/verification/rvgen/rvgen/generator.py
> > @@ -73,13 +73,13 @@ class RVGenerator:
> >              return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
> >          return ""
> >  
> > -    def fill_tracepoint_handlers_skel(self):
> > +    def fill_tracepoint_handlers_skel(self) -> str:
> >          return "NotImplemented"
> 
> Those are the ones that will raise an exception in a later iteration of this,
> right? I wonder if we really need to touch them now.
> Anyway I'm fine with this if it pleases your tools, thanks.

I was uncertain if I should send now or postpone it, to be fair.

> 
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> 
> >  
> > -    def fill_tracepoint_attach_probe(self):
> > +    def fill_tracepoint_attach_probe(self) -> str:
> >          return "NotImplemented"
> >  
> > -    def fill_tracepoint_detach_helper(self):
> > +    def fill_tracepoint_detach_helper(self) -> str:
> >          return "NotImplemented"
> >  
> >      def fill_main_c(self):
> > @@ -100,19 +100,19 @@ class RVGenerator:
> >  
> >          return main_c
> >  
> > -    def fill_model_h(self):
> > +    def fill_model_h(self) -> str:
> >          return "NotImplemented"
> >  
> > -    def fill_monitor_class_type(self):
> > +    def fill_monitor_class_type(self) -> str:
> >          return "NotImplemented"
> >  
> > -    def fill_monitor_class(self):
> > +    def fill_monitor_class(self) -> str:
> >          return "NotImplemented"
> >  
> > -    def fill_tracepoint_args_skel(self, tp_type):
> > +    def fill_tracepoint_args_skel(self, tp_type) -> str:
> >          return "NotImplemented"
> >  
> > -    def fill_monitor_deps(self):
> > +    def fill_monitor_deps(self) -> str:
> >          buff = []
> >          buff.append("	# XXX: add dependencies if there")
> >          if self.parent:
>