linux-stable.git/tools/verification, branch linux-7.1.y

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

tools/rv: Fix cleanup after failed trace setup

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

Currently if ikm_setup_trace_instance() fails, the tool returns without
any cleanup, if rv was called with both -t and -r, this means the
reactor is not going to be cleared.

Jump to the cleanup label to restore the reactor if necessary.

Fixes: 6d60f89691fc9 ("tools/rv: Add in-kernel monitor interface")
Reviewed-by: Nam Cao 
Link: https://lore.kernel.org/r/20260514152055.229162-5-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco

tools/rv: Fix substring match when listing container monitors

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

When listing monitors within a specific container (rv list ),
the tool incorrectly matched monitors if the requested container name
was only a prefix of the actual container (e.g., 'rv list sche' would
incorrectly list monitors from 'sched:').

Fix this by ensuring the container name is an exact match and is
immediately followed by the ':' separator.

Fixes: eba321a16fc6 ("tools/rv: Add support for nested monitors")
Reviewed-by: Nam Cao 
Link: https://lore.kernel.org/r/20260514152055.229162-3-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco

tools/rv: Fix substring match bug in monitor name search

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

__ikm_find_monitor_name() relies on strstr() to find a monitor by name,
which fails if the target monitor is a substring of a previously listed
monitor.

Fix it by tokenizing the available_monitors file and matching full
tokens instead.

Fixes: eba321a16fc6 ("tools/rv: Add support for nested monitors")
Reviewed-by: Nam Cao 
Link: https://lore.kernel.org/r/20260514152055.229162-2-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco

tools/rv: Ensure monitor name and desc are NUL-terminated

2026-06-04T14:43:43+00:00

ikm_fill_monitor_definition() copies monitor name and description with
strncpy(), but does not guarantee NUL termination when source strings are
equal to or longer than the destination buffers.

Clamp copies to sizeof(dst) - 1 and explicitly append '\0' for both fields
to keep them safe for later string operations.

Suggested-by: unknownbbqrx 
Fixes: 6d60f89691fc9 ("tools/rv: Add in-kernel monitor interface")
Link: https://lore.kernel.org/r/20260604120946.90302-2-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: Allow epoll in rtapp-sleep monitor

2026-04-01T13:18:30+00:00

Since commit 0c43094f8cc9 ("eventpoll: Replace rwlock with spinlock"),
epoll_wait is real-time-safe syscall for sleeping.

Add epoll_wait to the list of rt-safe sleeping APIs.

Signed-off-by: Nam Cao 
Reviewed-by: Gabriele Monaco 
Link: https://lore.kernel.org/r/20260401130828.3115428-1-namcao@linutronix.de
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