github-mirror/linux
1
0
Fork 0
mirror of https://github.com/torvalds/linux.git synced 2026-09-22 12:44:03 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity Graph

verification/rvgen: Remove dead code

Browse Source 
The conversion to use Lark left some dead code behind. Remove them.

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/98115605a49c819adae9329823d4010bf181c3b7.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
This commit is contained in:
Nam Cao 2026-06-19 07:52:16 +02:00 committed by Gabriele Monaco
parent 7edaba052d
commit fc0663ec31
2 changed files with 1 additions and 185 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

157
tools/verification/rvgen/rvgen/automata.py
View File

@ -9,9 +9,6 @@
# Documentation/trace/rv/deterministic_automata.rst
import ntpath
import re
from typing import Iterator
from itertools import islice
import lark
@ -356,19 +353,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 +371,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 +401,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 +457,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 +479,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 +547,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)

29
tools/verification/rvgen/rvgen/dot2k.py
View File

@ -8,12 +8,9 @@
# For further information, see:
# Documentation/trace/rv/da_monitor_synthesis.rst
from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
from .automata import ConstraintCondition
from .automata import ConstraintCondition, AutomataError
class dot2k(Monitor, Dot2c):
template_dir = "dot2k"
@ -217,9 +214,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 +227,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.removesuffix(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 +237,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"