user/sven/linux.git/tools/verification/rvgen, branch master

rv/rvgen: fix _fill_states() return type annotation

2026-04-01T08:16:20Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-20-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: fix unbound loop variable warning

2026-04-01T08:16:20Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-19-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: enforce presence of initial state

2026-04-01T08:16:20Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-18-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: extract node marker string to class constant

2026-04-01T08:16:19Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-17-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: fix isinstance check in Variable.expand()

2026-04-01T08:16:19Z

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 Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260223162407.147003-16-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: make monitor arguments required in rvgen

2026-04-01T08:16:19Z

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 Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260223162407.147003-15-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: remove unused __get_main_name method

2026-04-01T08:16:19Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-14-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: remove unused sys import from dot2c

2026-04-01T08:16:19Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-13-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: refactor automata.py to use iterator-based parsing

2026-04-01T08:16:18Z

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 Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-12-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: use class constant for init marker

2026-04-01T08:16:18Z

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 Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260223162407.147003-11-wander@redhat.com Signed-off-by: Gabriele Monaco