Messages in this thread Patch in this message |  | | From | Nam Cao <> | | Subject | [PATCH 13/13] verification/rvgen: Remove dead code | | Date | Tue, 5 May 2026 08:59:34 +0200 |
| |
The conversion to use Lark left some dead code behind. Remove them.
Signed-off-by: Nam Cao <namcao@linutronix.de> --- 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 e0d3f83cbd3c..cc42b8127fc0 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -343,19 +343,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. @@ -374,28 +361,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() @@ -422,57 +391,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 = [] @@ -529,51 +447,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] = [] @@ -596,26 +469,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) -> list[str]: if constraint.unit: self.env_types[constraint.env] = constraint.unit @@ -684,10 +537,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 12d944bcd6f3..12589fbb180c 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 - +from .automata import ConstraintRule, 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) -> str: buff = [] for c, sep in rule.rules: @@ -234,12 +229,6 @@ class ha2k(dot2k): buff[-1] += ';' 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: ConstraintRule) -> str: # by default assume the timer has ns expiration clock_type = "ns" @@ -248,21 +237,6 @@ class ha2k(dot2k): return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {inv.val})" - 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" -- 2.47.3
|  |