linux-kernel - Re: [PATCH 16/26] rv/rvgen: fix unbound initial

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives
Hash Suite: Windows password security audit tool. GUI, reports in PDF.
[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <7d37e29989e08e62a419f2ae8000ed7ec1913713.camel@redhat.com>
Date: Tue, 20 Jan 2026 09:21:01 +0100
From: Gabriele Monaco <gmonaco@...hat.com>
To: Wander Lairson Costa <wander@...hat.com>
Cc: Steven Rostedt <rostedt@...dmis.org>, Nam Cao <namcao@...utronix.de>, 
 open list <linux-kernel@...r.kernel.org>, "open list:RUNTIME VERIFICATION
 (RV)"	 <linux-trace-kernel@...r.kernel.org>
Subject: Re: [PATCH 16/26] rv/rvgen: fix unbound initial_state variable

On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:


[...]
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 8548265955570..083d0f5cfb773 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -10,6 +10,7 @@
>  
>  import ntpath
>  
> +
>  class AutomataError(OSError):
>      """Exception raised for errors in automata parsing and validation.
>  
> @@ -17,6 +18,7 @@ class AutomataError(OSError):
>      or malformed automaton definitions.
>      """
>  
> +

I believe these newlines were added automatically by some tools, not sure if we
really want them but they don't belong in this patch (since 1/26 added this
class).

>  class Automata:
>      """Automata class: Reads a dot file and parses it as an automata.
>  
> @@ -31,7 +33,9 @@ class Automata:
>          self.__dot_path = file_path
>          self.name = model_name or self.__get_model_name()
>          self.__dot_lines = self.__open_dot()
> -        self.states, self.initial_state, self.final_states =
> self.__get_state_variables()
> +        self.states, self.initial_state, self.final_states = (
> +            self.__get_state_variables()
> +        )

There is no strict 80 character limit for python code and I personally find this
less readable. Is this again what the tool suggested?

>          self.events = self.__get_event_variables()
>          self.function = self.__create_matrix()
>          self.events_start, self.events_start_run = self.__store_init_events()
> @@ -86,6 +90,7 @@ class Automata:
>          # wait for node declaration
>          states = []
>          final_states = []
> +        initial_state = None
>  
>          has_final_states = False
>          cursor = self.__get_cursor_begin_states()
> @@ -96,9 +101,9 @@ class Automata:
>              raw_state = line[-1]
>  
>              #  "enabled_fired"}; -> enabled_fired
> -            state = raw_state.replace('"', '').replace('};', '').replace(',',
> '_')
> +            state = raw_state.replace('"', "").replace("};", "").replace(",",
> "_")

Ok this change is good.

>              if state.startswith(self.init_marker):
> -                initial_state = state[len(self.init_marker):]
> +                initial_state = state[len(self.init_marker) :]

You fixed spacing in 12/26. We could either keep move this change there or just
merge that patch with others touching the same files.

>              else:
>                  states.append(state)
>                  if "doublecircle" in self.__dot_lines[cursor]:
> @@ -111,6 +116,9 @@ class Automata:
>  
>              cursor += 1
>  
> +        if initial_state is None:
> +            raise AutomataError("The automaton doesn't have a initial state")
> +

Yeah that's needed.

>          states = sorted(set(states))
>  
>          # Insert the initial state at the beginning of the states
> @@ -132,7 +140,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 +170,9 @@ 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 +180,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", "
> ")

All in all looks good, thanks.

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

>                  for event in possible_events.split():
>                      matrix[states_dict[origin_state]][events_dict[event]] =
> dest_state
>              cursor += 1