Re: [PATCH v2 13/13] verification/rvgen: Remove dead code

[Gabriele Monaco <gmonaco@redhat.com>]

On Thu, 2026-05-28 at 10:28 +0200, Nam Cao wrote:
> The conversion to use Lark left some dead code behind. Remove them.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>
> ---

You might want to remove unused imports (linters should help you with
that too):
* re, typing.Iterator, and itertools.islice from automata.py
* deque and ConstraintRule from dot2k

Other than that

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

>  tools/verification/rvgen/rvgen/automata.py | 154 -------------------
> --
>  tools/verification/rvgen/rvgen/dot2k.py    |  28 +---
>  2 files changed, 1 insertion(+), 181 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index a3be327c2a73..b6ff5fceb820 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -356,19 +356,6 @@ class State:
>          self.name = name
>          self.inv = inv
>  
> -class _ConstraintKey:
> -    """Base class for constraint keys."""
> -
> -class _StateConstraintKey(_ConstraintKey, int):
> -    """Key for a state constraint. Under the hood just state_id."""
> -    def __new__(cls, state_id: int):
> -        return super().__new__(cls, state_id)
> -
> -class _EventConstraintKey(_ConstraintKey, tuple):
> -    """Key for an event constraint. Under the hood just
> tuple(state_id,event_id)."""
> -    def __new__(cls, state_id: int, event_id: int):
> -        return super().__new__(cls, (state_id, event_id))
> -
>  class AutomataError(Exception):
>      """Exception raised for errors in automata parsing and
> validation.
>  
> @@ -387,28 +374,10 @@ class Automata:
>  
>      invalid_state_str = "INVALID_STATE"
>      init_marker = "__init_"
> -    node_marker = "{node"
> -    # val can be numerical, uppercase (constant or macro), lowercase
> (parameter or function)
> -    # only numerical values should have units
> -    constraint_rule = re.compile(r"""
> -        ^
> -        (?P<env>[a-zA-Z_][a-zA-Z0-9_]+)  # C-like identifier for the
> env var
> -        (?P<op>[!<=>]{1,2})              # operator
> -        (?P<val>
> -            [0-9]+ |                     # numerical value
> -            [A-Z_]+\(\) |                # macro
> -            [A-Z_]+ |                    # constant
> -            [a-z_]+\(\) |                # function
> -            [a-z_]+                      # parameter
> -        )
> -        (?P<unit>[a-z]{1,2})?            # optional unit for
> numerical values
> -        """, re.VERBOSE)
> -    constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-
> Z0-9_]+)\)")
>  
>      def __init__(self, file_path, model_name=None):
>          self.__dot_path = file_path
>          self.name = model_name or self.__get_model_name()
> -        self.__dot_lines = self.__open_dot()
>          self.__parse_tree = ParseTree(file_path)
>          self.transitions = self.__parse_transitions()
>          self.states, self.initial_state, self.final_states =
> self.__parse_states()
> @@ -435,57 +404,6 @@ class Automata:
>  
>          return model_name
>  
> -    def __open_dot(self) -> list[str]:
> -        dot_lines = []
> -        try:
> -            with open(self.__dot_path) as dot_file:
> -                dot_lines = dot_file.readlines()
> -        except OSError as exc:
> -            raise AutomataError(exc.strerror) from exc
> -
> -        if not dot_lines:
> -            raise AutomataError(f"{self.__dot_path} is empty")
> -
> -        # checking the first line:
> -        line = dot_lines[0].split()
> -
> -        if len(line) < 2 or line[0] != "digraph" or line[1] !=
> "state_automaton":
> -            raise AutomataError(f"Not a valid .dot format:
> {self.__dot_path}")
> -
> -        return dot_lines
> -
> -    def __get_cursor_begin_states(self) -> int:
> -        for cursor, line in enumerate(self.__dot_lines):
> -            split_line = line.split()
> -
> -            if len(split_line) and split_line[0] ==
> self.node_marker:
> -                return cursor
> -
> -        raise AutomataError("Could not find a beginning state")
> -
> -    def __get_cursor_begin_events(self) -> int:
> -        state = 0
> -        cursor = 0 # make pyright happy
> -
> -        for cursor, line in enumerate(self.__dot_lines):
> -            line = line.split()
> -            if not line:
> -                continue
> -
> -            if state == 0:
> -                if line[0] == self.node_marker:
> -                    state = 1
> -            elif line[0] != self.node_marker:
> -                break
> -        else:
> -            raise AutomataError("Could not find beginning event")
> -
> -        cursor += 1 # skip initial state transition
> -        if cursor == len(self.__dot_lines):
> -            raise AutomataError("Dot file ended after event
> beginning")
> -
> -        return cursor
> -
>      def __parse_transitions(self):
>          transitions = []
>  
> @@ -542,51 +460,6 @@ class Automata:
>          states.insert(0, initial_state)
>          return states, initial_state, final_states
>  
> -    def __get_state_variables(self) -> tuple[list[str], str,
> list[str]]:
> -        # wait for node declaration
> -        states = []
> -        final_states = []
> -        initial_state = ""
> -
> -        has_final_states = False
> -        cursor = self.__get_cursor_begin_states()
> -
> -        # process nodes
> -        for line in islice(self.__dot_lines, cursor, None):
> -            split_line = line.split()
> -            if not split_line or split_line[0] != self.node_marker:
> -                break
> -
> -            raw_state = split_line[-1]
> -
> -            #  "enabled_fired"}; -> enabled_fired
> -            state = raw_state.replace('"', '').replace('};',
> '').replace(',', '_')
> -            if state.startswith(self.init_marker):
> -                initial_state = state[len(self.init_marker):]
> -            else:
> -                states.append(state)
> -                if "doublecircle" in line:
> -                    final_states.append(state)
> -                    has_final_states = True
> -
> -                if "ellipse" in line:
> -                    final_states.append(state)
> -                    has_final_states = True
> -
> -        if not initial_state:
> -            raise AutomataError("The automaton doesn't have an
> initial state")
> -
> -        states = sorted(set(states))
> -        states.remove(initial_state)
> -
> -        # Insert the initial state at the beginning of the states
> -        states.insert(0, initial_state)
> -
> -        if not has_final_states:
> -            final_states.append(initial_state)
> -
> -        return states, initial_state, final_states
> -
>      def __get_event_variables(self) -> tuple[list[str], list[str]]:
>          events: list[str] = []
>          envs: list[str] = []
> @@ -609,26 +482,6 @@ class Automata:
>  
>          return sorted(set(events)), sorted(set(envs))
>  
> -    def _split_constraint_expr(self, constr: list[str]) ->
> Iterator[tuple[str,
> -
>                                                                       
>     str | None]]:
> -        """
> -        Get a list of strings of the type constr1 && constr2 and
> returns a list of
> -        constraints and separators: [[constr1,"&&"],[constr2,None]]
> -        """
> -        exprs = []
> -        seps = []
> -        for c in constr:
> -            while "&&" in c or "||" in c:
> -                a = c.find("&&")
> -                o = c.find("||")
> -                pos = a if o < 0 or 0 < a < o else o
> -                exprs.append(c[:pos].replace(" ", ""))
> -                seps.append(c[pos:pos + 2].replace(" ", ""))
> -                c = c[pos + 2:].replace(" ", "")
> -            exprs.append(c)
> -            seps.append(None)
> -        return zip(exprs, seps)
> -
>      def __extract_env_var(self, constraint: ConstraintCondition):
>          if constraint.unit:
>              self.env_types[constraint.env] = constraint.unit
> @@ -697,10 +550,3 @@ class Automata:
>  
>      def is_hybrid_automata(self) -> bool:
>          return bool(self.envs)
> -
> -    def is_event_constraint(self, key: _ConstraintKey) -> bool:
> -        """
> -        Given the key in self.constraints return true if it is an
> event
> -        constraint, false if it is a state constraint
> -        """
> -        return isinstance(key, _EventConstraintKey)
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index 49cb3e724a93..d6779ac6b7dd 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -11,9 +11,7 @@
>  from collections import deque
>  from .dot2c import Dot2c
>  from .generator import Monitor
> -from .automata import _EventConstraintKey, _StateConstraintKey,
> AutomataError
> -from .automata import ConstraintRule, ConstraintCondition
> -
> +from .automata import ConstraintRule, ConstraintCondition,
> AutomataError
>  
>  class dot2k(Monitor, Dot2c):
>      template_dir = "dot2k"
> @@ -217,9 +215,6 @@ class ha2k(dot2k):
>                  value *= 10**9
>          return str(value) + "ull"
>  
> -    def __parse_single_constraint(self, rule: dict, value: str) ->
> str:
> -        return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix},
> time_ns) {rule["op"]} {value}"
> -
>      def __parse_guard_rule(self, rule) -> list[str]:
>          buff = []
>          for c, sep in rule.rules:
> @@ -233,12 +228,6 @@ class ha2k(dot2k):
>              buff.append(cond)
>          return buff
>  
> -    def __get_constraint_env(self, constr: str) -> str:
> -        """Extract the second argument from an ha_ function"""
> -        env =
> constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
> -        assert env.rstrip(f"_{self.name}") in self.envs
> -        return env
> -
>      def __start_to_invariant_check(self, inv: ConstraintCondition) -
> > str:
>          # by default assume the timer has ns expiration
>          clock_type = "ns"
> @@ -249,21 +238,6 @@ class ha2k(dot2k):
>  
>          return f"return ha_check_invariant_{clock_type}(ha_mon,
> {inv.env}_{self.name}, time_ns, {value})"
>  
> -    def __start_to_conv(self, constr: str) -> str:
> -        """
> -        Undo the storage conversion done by ha_start_timer_
> -        """
> -        return "ha_inv_to_guard" + constr[constr.find("("):]
> -
> -    def __parse_timer_constraint(self, rule: dict, value: str) ->
> str:
> -        # by default assume the timer has ns expiration
> -        clock_type = "ns"
> -        if self.env_types.get(rule["env"]) == "j":
> -            clock_type = "jiffy"
> -
> -        return (f"ha_start_timer_{clock_type}(ha_mon,
> {rule["env"]}{self.enum_suffix},"
> -                f" {value}, time_ns)")
> -
>      def __parse_invariant(self, inv):
>          # by default assume the timer has ns expiration
>          clock_type = "ns"