Message-ID: <20260119205601.105821-17-wander@redhat.com>
Date: Mon, 19 Jan 2026 17:45:52 -0300
From: Wander Lairson Costa <wander@...hat.com>
To: Steven Rostedt <rostedt@...dmis.org>,
	Gabriele Monaco <gmonaco@...hat.com>,
	Nam Cao <namcao@...utronix.de>,
	Wander Lairson Costa <wander@...hat.com>,
	linux-kernel@...r.kernel.org (open list),
	linux-trace-kernel@...r.kernel.org (open list:RUNTIME VERIFICATION (RV))
Subject: [PATCH 16/26] rv/rvgen: fix unbound initial_state variable

Initialize initial_state to None and validate its assignment after
parsing DOT file state nodes. The previous implementation left
initial_state uninitialized if the DOT file contained no state with
the init_marker prefix, which would cause an UnboundLocalError when
the code attempted to use the variable at the end of the function.

This bug was identified by pyright static type checker, which correctly
flagged that initial_state could be referenced before assignment. The
fix adds proper initialization and validation, raising a AutomataError if
no initial state marker is found in the automaton definition. This
ensures that malformed DOT files missing an initial state are caught
early with a clear error message rather than causing cryptic runtime
exceptions.

The change also includes minor code formatting improvements to comply
with PEP 8 style guidelines, including consistent use of double quotes
for string literals and proper line length formatting for improved
readability.

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

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.
     """
 
+
 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()
+        )
         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(",", "_")
             if state.startswith(self.init_marker):
-                initial_state = state[len(self.init_marker):]
+                initial_state = state[len(self.init_marker) :]
             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")
+
         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", " ")
                 for event in possible_events.split():
                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
             cursor += 1
-- 
2.52.0

Powered by blists - more mailing lists