kernel/linux.git/tools/verification/rvgen, branch v7.1

verification/rvgen: Fix ltl2k writing True as a literal

2026-06-04T14:44:25+00:00

The rvgen parser for LTL stores literal true values in the python representation (capitalised True), this doesn't build in C. The Literal class should already handle this case but ASTNode skips its strigification method and converts the value (true/false) directly. Fix by delegating ASTNode stringification to the Literal and Variable classes instead of bypassing them. Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

verification/rvgen: Fix options shared among commands

2026-06-04T14:44:25+00:00

After rvgen was refactored to use subparsers, the common options (-a and -D) were left in the main parser. This meant that they needed to be called /before/ the subcommand and using them without subcommand was allowed. This is not the original intent. rvgen -D "some description" container -n name Define the options as parent in the subparsers to allow them to be used from both subcommands together with other options. rvgen container -n name -D "some description" Fixes: 5270a0e3041c ("verification/dot2k: Replace is_container() hack with subparsers") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260514152055.229162-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

verification/rvgen: Fix suffix strip in dot2k

2026-06-04T14:44:25+00:00

__start_to_invariant_check() and __get_constraint_env() parse the environment variable's name from sources that have it padded with the monitor name. This is removed using rstrip(), which is not meant to strip a substring but rather a set of characters. Use removesuffix() to actually get rid of the trailing _. Fixes: a82adadb16894 ("verification/rvgen: Add support for Hybrid Automata") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-12-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv: Add automatic cleanup handlers for per-task HA monitors

2026-06-03T10:33:24+00:00

Hybrid automata monitors may start timers, depending on the model, these may remain active on an exiting task and cause false positives or even access freed memory. Add an enable/disable hook in the HA code, currently only populated by the per-task handler for registration and deregistration. This hooks to the sched_process_exit event and ensures the timer is stopped for every exiting task. The handler is enabled automatically but may be disabled, for instance if the monitor uses the event for another purpose (but should still manually ensure timers are stopped). Fixes: f5587d1b6ec9 ("rv: Add Hybrid Automata monitor type") Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260601153840.124372-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: fix _fill_states() return type annotation

2026-04-01T08:16:20+00:00

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:20+00:00

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:20+00:00

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:19+00:00

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:19+00:00

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:19+00:00

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