Re: [PATCH v2 13/13] verification/rvgen: Remove dead code
From: Gabriele Monaco
Date: Wed Jun 03 2026 - 12:25:39 EST
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@xxxxxxxxxxxxx>
> ---
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@xxxxxxxxxx>
> 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"