* [PATCH 01/13] verification/rvgen: Switch LTL parser to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 02/13] verification/rvgen: Introduce a parse tree for automata using Lark Nam Cao
` (11 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
The LTL parser is built using Ply. However, Ply is no longer
maintained [1].
Switch to use Lark instead. In addition to being actively maintained, Lark
also offers additional features (namely, automatically creating the
abstract syntax tree) which make the parser simpler.
Link: https://github.com/dabeaz/ply/commit/9d7c40099e23ff78f9d86ef69a26c1e8a83e706a [1]
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/ltl2ba.py | 189 +++++++++--------------
1 file changed, 70 insertions(+), 119 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index 7f538598a868..b2dee2dbe257 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -7,8 +7,7 @@
# https://doi.org/10.1007/978-0-387-34892-6_1
# With extra optimizations
-from ply.lex import lex
-from ply.yacc import yacc
+import lark
from .automata import AutomataError
# Grammar:
@@ -30,42 +29,38 @@ from .automata import AutomataError
# imply
# equivalent
-tokens = (
- 'AND',
- 'OR',
- 'IMPLY',
- 'UNTIL',
- 'ALWAYS',
- 'EVENTUALLY',
- 'NEXT',
- 'VARIABLE',
- 'LITERAL',
- 'NOT',
- 'LPAREN',
- 'RPAREN',
- 'ASSIGN',
-)
-
-t_AND = r'and'
-t_OR = r'or'
-t_IMPLY = r'imply'
-t_UNTIL = r'until'
-t_ALWAYS = r'always'
-t_NEXT = r'next'
-t_EVENTUALLY = r'eventually'
-t_VARIABLE = r'[A-Z_0-9]+'
-t_LITERAL = r'true|false'
-t_NOT = r'not'
-t_LPAREN = r'\('
-t_RPAREN = r'\)'
-t_ASSIGN = r'='
-t_ignore_COMMENT = r'\#.*'
-t_ignore = ' \t\n'
-
-def t_error(t):
- raise AutomataError(f"Illegal character '{t.value[0]}'")
-
-lexer = lex()
+GRAMMAR = r'''
+start: assign+
+
+assign: VARIABLE "=" _ltl
+
+_ltl: _opd | binop | unop
+
+_opd : VARIABLE
+ | LITERAL
+ | "(" _ltl ")"
+
+unop: UNOP _ltl
+UNOP: "always"
+ | "eventually"
+ | "next"
+ | "not"
+
+binop: _opd BINOP _ltl
+BINOP: "until"
+ | "and"
+ | "or"
+ | "imply"
+
+VARIABLE: /[A-Z_0-9]+/
+LITERAL: "true" | "false"
+
+COMMENT: "#" /.*/ "\n"
+%ignore COMMENT
+
+%import common.WS
+%ignore WS
+'''
class GraphNode:
uid = 0
@@ -432,90 +427,46 @@ class Literal:
node.old |= {n}
return node.expand(node_set)
-def p_spec(p):
- '''
- spec : assign
- | assign spec
- '''
- if len(p) == 3:
- p[2].append(p[1])
- p[0] = p[2]
- else:
- p[0] = [p[1]]
-
-def p_assign(p):
- '''
- assign : VARIABLE ASSIGN ltl
- '''
- p[0] = (p[1], p[3])
-
-def p_ltl(p):
- '''
- ltl : opd
- | binop
- | unop
- '''
- p[0] = p[1]
-
-def p_opd(p):
- '''
- opd : VARIABLE
- | LITERAL
- | LPAREN ltl RPAREN
- '''
- if p[1] == "true":
- p[0] = ASTNode(Literal(True))
- elif p[1] == "false":
- p[0] = ASTNode(Literal(False))
- elif p[1] == '(':
- p[0] = p[2]
- else:
- p[0] = ASTNode(Variable(p[1]))
-
-def p_unop(p):
- '''
- unop : ALWAYS ltl
- | EVENTUALLY ltl
- | NEXT ltl
- | NOT ltl
- '''
- if p[1] == "always":
- op = AlwaysOp(p[2])
- elif p[1] == "eventually":
- op = EventuallyOp(p[2])
- elif p[1] == "next":
- op = NextOp(p[2])
- elif p[1] == "not":
- op = NotOp(p[2])
- else:
- raise AutomataError(f"Invalid unary operator {p[1]}")
-
- p[0] = ASTNode(op)
-
-def p_binop(p):
- '''
- binop : opd UNTIL ltl
- | opd AND ltl
- | opd OR ltl
- | opd IMPLY ltl
- '''
- if p[2] == "and":
- op = AndOp(p[1], p[3])
- elif p[2] == "until":
- op = UntilOp(p[1], p[3])
- elif p[2] == "or":
- op = OrOp(p[1], p[3])
- elif p[2] == "imply":
- op = ImplyOp(p[1], p[3])
- else:
- raise AutomataError(f"Invalid binary operator {p[2]}")
-
- p[0] = ASTNode(op)
-
-parser = yacc()
+class Transform(lark.visitors.Transformer):
+ def unop(self, node):
+ if node[0] == "always":
+ return ASTNode(AlwaysOp(node[1]))
+ if node[0] == "eventually":
+ return ASTNode(EventuallyOp(node[1]))
+ if node[0] == "next":
+ return ASTNode(NextOp(node[1]))
+ if node[0] == "not":
+ return ASTNode(NotOp(node[1]))
+ raise ValueError("Unknown operator %s" % node[1])
+
+ def binop(self, node):
+ if node[1] == "until":
+ return ASTNode(UntilOp(node[0], node[2]))
+ if node[1] == "and":
+ return ASTNode(AndOp(node[0], node[2]))
+ if node[1] == "or":
+ return ASTNode(OrOp(node[0], node[2]))
+ if node[1] == "imply":
+ return ASTNode(ImplyOp(node[0], node[2]))
+ raise ValueError("Unknown operator %s" % node[1])
+
+ def VARIABLE(self, args):
+ return ASTNode(Variable(args))
+
+ def LITERAL(self, args):
+ return ASTNode(Variable(args))
+
+ def start(self, node):
+ return node
+
+ def assign(self, node):
+ return node[0].op.name, node[1]
+
+parser = lark.Lark(GRAMMAR)
def parse_ltl(s: str) -> ASTNode:
spec = parser.parse(s)
+ spec = Transform().transform(spec)
rule = None
subexpr = {}
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 02/13] verification/rvgen: Introduce a parse tree for automata using Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
2026-05-05 6:59 ` [PATCH 01/13] verification/rvgen: Switch LTL parser " Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark Nam Cao
` (10 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT language
defined by graphviz), the scripts would fail.
To make the scripts robust, the parser should be implemented based on the
dot language specification, not based on how the existing dot files look.
As a first step, use Lark to implement a Parser based on the graphviz dot
language specification. The resulting parse tree is not used yet, but the
existing scripts will be converted one by one to use this new parse tree in
the follow-up commits.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 182 +++++++++++++++++++++
1 file changed, 182 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b9f8149f7118..4e3d719a0952 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -13,6 +13,187 @@ import re
from typing import Iterator
from itertools import islice
+import lark
+
+class ParseTree:
+ # based on https://graphviz.org/doc/info/lang.html
+ # with the irrelevant stuffs (port and compass) removed
+ grammar = r'''
+ start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}"
+
+ stmt_list: (stmt ";"? stmt_list)?
+
+ stmt: node_stmt
+ | edge_stmt
+ | attr_stmt
+ | ID "=" ID
+ | subgraph
+
+ attr_stmt: attr_type attr_list
+
+ attr_type: "graph" -> graph
+ | "node" -> node
+ | "edge" -> edge
+
+ attr_list: "[" a_list? "]" attr_list?
+
+ a_list: ID "=" ID (";" | ",")? a_list?
+
+ edge_stmt: (node_id | subgraph) edgerhs attr_list?
+
+ edgerhs: edgeop (node_id | subgraph) edgerhs?
+
+ edgeop: "->" | "--"
+
+ node_stmt: node_id attr_list?
+
+ node_id: ID
+
+ subgraph: ("subgraph" ID?)? "{" stmt_list "}"
+
+ ID: /[_a-zA-Z][_a-zA-Z0-9]+/
+ | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/
+ | /".*?"/
+
+ %import common.WS
+ %ignore WS
+ '''
+
+ @staticmethod
+ def parse_edge(tree: lark.Tree) -> tuple[str, str]:
+ # only support a simple node-to-node edge
+ nodes = []
+ for node in tree.iter_subtrees_topdown():
+ if node.data == "node_id":
+ nodes.append(node.children[0].strip('"'))
+
+ if len(nodes) != 2:
+ raise AutomataError("Only state-to-state transition is supported")
+
+ return tuple(nodes)
+
+ class ParseNodes(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.nodes = set()
+ super().__init__(*args, **kwargs)
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+ self.nodes.add(node)
+
+ class ParseEdges(lark.visitors.Visitor):
+ def __init__(self, *args, **kwargs):
+ self.edges = set()
+ super().__init__(*args, **kwargs)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+ self.edges.add(edge)
+
+ class ParseAttributes(lark.visitors.Interpreter):
+ def __init__(self, *args, **kwargs):
+ '''
+ Stacks of default attributes. [0] is the default
+ attributes for the outermost scope, while [-1] is the
+ default attributes for the current scope.
+ '''
+ self.default_node_attrs = [{}]
+ self.default_edge_attrs = [{}]
+
+ self.node_attrs = {}
+ self.edge_attrs = {}
+
+ super().__init__(*args, **kwargs)
+
+ @staticmethod
+ def __get_attrs(stmt: lark.Tree) -> dict[str, str]:
+ attrs = {}
+
+ for node in stmt.iter_subtrees():
+ if node.data == "a_list":
+ attrs[node.children[0]] = node.children[1].strip('"')
+
+ return attrs
+
+
+ def subgraph(self, tree):
+ # We are entering a new scope, inherit the default
+ # attributes of the outer scope
+ self.default_node_attrs.append(self.default_node_attrs[-1].copy())
+ self.default_edge_attrs.append(self.default_edge_attrs[-1].copy())
+
+ children = self.visit_children(tree)
+
+ # Exiting the scope
+ del self.default_node_attrs[-1]
+ del self.default_edge_attrs[-1]
+
+ return children
+
+ def node_stmt(self, tree):
+ node_id = tree.children[0]
+ node = node_id.children[0].strip('"')
+
+ attrs = self.default_node_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if node in self.node_attrs:
+ self.node_attrs[node] = attrs | self.node_attrs[node]
+ else:
+ self.node_attrs[node] = attrs
+
+ return self.visit_children(tree)
+
+ def edge_stmt(self, tree):
+ edge = ParseTree.parse_edge(tree)
+
+ attrs = self.default_edge_attrs[-1].copy()
+ attrs |= self.__get_attrs(tree)
+
+ if attrs:
+ if edge in self.edge_attrs:
+ self.edge_attrs[edge] = attrs | self.edge_attrs[edge]
+ else:
+ self.edge_attrs[edge] = attrs
+
+ return self.visit_children(tree)
+
+ def attr_stmt(self, tree):
+ attr_type = tree.children[0].data
+ attrs = self.__get_attrs(tree)
+
+ if attr_type == "node":
+ self.default_node_attrs[-1] |= attrs
+ elif attr_type == "edge":
+ self.default_edge_attrs[-1] |= attrs
+ else:
+ # graph attributes are irrelevant
+ pass
+
+ self.visit_children(tree)
+
+ def __init__(self, dot_file):
+ parser = lark.Lark(self.grammar, parser='lalr')
+ node_parser = self.ParseNodes()
+ edge_parser = self.ParseEdges()
+ attributes_parser = self.ParseAttributes()
+
+ try:
+ with open(dot_file, "r") as dot_file:
+ tree = parser.parse(dot_file.read())
+ attributes_parser.visit(tree)
+ node_parser.visit(tree)
+ edge_parser.visit(tree)
+ except OSError as exc:
+ raise AutomataError(exc.strerror) from exc
+
+ self.nodes = node_parser.nodes
+ self.edges = edge_parser.edges
+ self.node_attrs = attributes_parser.node_attrs
+ self.edge_attrs = attributes_parser.edge_attrs
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -66,6 +247,7 @@ class Automata:
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.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
2026-05-05 6:59 ` [PATCH 01/13] verification/rvgen: Switch LTL parser " Nam Cao
2026-05-05 6:59 ` [PATCH 02/13] verification/rvgen: Introduce a parse tree for automata using Lark Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark Nam Cao
` (9 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT
language), the scripts would fail.
Prepare to move away from the raw text processing, implement parsers based
on Lark which parse states, transitions and constraints.
The parse results are not used yet. The existing scripts will be converted
one by one to them, and the raw text processing will eventually be removed.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 207 +++++++++++++++++++++
1 file changed, 207 insertions(+)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4e3d719a0952..32c16736a41b 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -194,6 +194,155 @@ class ParseTree:
self.node_attrs = attributes_parser.node_attrs
self.edge_attrs = attributes_parser.edge_attrs
+class ConstraintCondition:
+ def __init__(self, env: str, op: str, val: str, unit=None):
+ self.env = env
+ self.op = op
+ self.val = val
+ self.unit = unit
+ if unit is None:
+ # try to infer unit from constants or parameters
+ val_for_unit = val.lower().replace("()", "")
+ if val_for_unit.endswith("_ns"):
+ self.unit = "ns"
+ if val_for_unit.endswith("_jiffies"):
+ self.unit = "j"
+
+class ConstraintRule:
+ grammar = r'''
+ rule: condition (OP condition)*
+
+ OP: "&&" | "||"
+
+ condition: ENV CMP_OP VAL UNIT?
+
+ ENV: CNAME
+
+ CMP_OP: "==" | "<=" | "<" | ">=" | ">"
+
+ VAL: /[0-9]+/
+ | /[A-Z_]+\(\)/
+ | /[A-Z_]+/
+ | /[a-z_]+\(\)/
+ | /[a-z_]+/
+
+ UNIT: "ns" | "us" | "ms" | "s"
+ '''
+
+ def __init__(self, c: ConstraintCondition):
+ '''
+ A list of pairs of
+ - the condition (e.g. is_constr_dl == 1)
+ - the logical operator ("||" or "&&") combining this
+ condition with the next one if it exists, otherwise None
+
+ TODO: Perhaps use an abstract syntax tree instead, because
+ this representation cannot capture precedence
+ '''
+ self.rules = [[c, None]]
+
+ def chain(self, op: str, c: ConstraintCondition):
+ self.rules[-1][1] = op
+ self.rules.append((c, None))
+
+class ConstraintReset:
+ def __init__(self, env):
+ self.env = env
+
+class StateLabelParser:
+ grammar = r'''
+ label: CNAME ("\\n" condition)?
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ def __init__(self, label: str):
+ parser = lark.Lark(self.grammar, parser='lalr', start="label")
+ tree = parser.parse(label)
+
+ self.state = tree.children[0]
+ self.constraint = None
+
+ if len(tree.children) == 2:
+ self.constraint = ConstraintCondition(*tree.children[1].children)
+ if self.constraint.op not in ("<", "<="):
+ raise AutomataError("State constraints must be clock expirations like"
+ f" clk<N ({label})")
+
+class EventLabelParser:
+ grammar = r'''
+ events: event ("\\n" event)*
+
+ event: name (";" guard)*
+
+ guard: reset
+ | rule
+ | rule reset
+ | reset rule
+
+ name: CNAME
+
+ reset: "reset" "(" ENV ")"
+
+ %import common.CNAME
+ %import common.WS
+ %ignore WS
+ ''' + ConstraintRule.grammar
+
+ class GetEvents(lark.visitors.Transformer):
+ def guard(self, args):
+ reset = None
+ rule = None
+ for arg in args:
+ if arg.data == "reset":
+ reset = ConstraintReset(arg.children[0])
+ elif arg.data == "rule":
+ conditions = arg.children
+ rule = ConstraintRule(conditions[0])
+ for i in range(1, len(conditions), 2):
+ rule.chain(conditions[i], conditions[i + 1])
+ return reset, rule
+
+ def OP(self, args):
+ return args
+
+ def condition(self, args):
+ return ConstraintCondition(*args)
+
+ def event(self, args):
+ name = args[0]
+ rule, reset = None, None
+ if len(args) == 2:
+ reset, rule = args[1]
+ return name, reset, rule
+
+ def events(self, args):
+ return args
+
+ def name(self, args):
+ return args[0]
+
+ def __init__(self, label: str):
+ parser = lark.Lark(self.grammar, parser='lalr', start="events")
+ tree = parser.parse(label)
+ self.events = self.GetEvents().transform(tree)
+
+class Transition:
+ def __init__(self, src: str, dst: str, event: str,
+ reset: ConstraintReset, rule: ConstraintRule):
+ self.src = src
+ self.dst = dst
+ self.event = event
+ self.rule = rule
+ self.reset = reset
+
+class State:
+ def __init__(self, name: str, inv: ConstraintRule):
+ self.name = name
+ self.inv = inv
+
class _ConstraintKey:
"""Base class for constraint keys."""
@@ -248,6 +397,8 @@ class Automata:
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()
self.states, self.initial_state, self.final_states = self.__get_state_variables()
self.env_types = {}
self.env_stored = set()
@@ -323,6 +474,62 @@ class Automata:
return cursor
+ def __parse_transitions(self):
+ transitions = []
+
+ for edge in self.__parse_tree.edges:
+ attr = self.__parse_tree.edge_attrs.get(edge)
+ if not attr:
+ continue
+
+ label = attr.get("label")
+
+ src, dst = edge
+
+ parser = EventLabelParser(label)
+ for event, reset, rule in parser.events:
+ transitions.append(Transition(src, dst, event, reset, rule))
+
+ transitions.sort(key=lambda t : (t.src, t.event))
+ return transitions
+
+ def __parse_states(self):
+ initial_state = ""
+ states = []
+ final_states = []
+
+ for node in self.__parse_tree.nodes:
+ attr = self.__parse_tree.node_attrs[node]
+ label = attr["label"]
+
+ if node.startswith(Automata.init_marker):
+ initial_state = node[len(Automata.init_marker):]
+
+ if not label:
+ continue
+
+ parser = StateLabelParser(attr["label"])
+ state = State(parser.state, parser.constraint)
+
+ states.append(state)
+
+ shape = attr.get("shape")
+ if shape in ("doublecircle", "ellipse"):
+ final_states.append(state)
+
+
+ initial_state = next((s for s in states if s.name == initial_state), None)
+ if not initial_state:
+ raise AutomataError("The automaton doesn't have an initial state")
+
+ if not final_states:
+ final_states.append(initial_state)
+
+ states.remove(initial_state)
+ states.sort(key=lambda s : s.name)
+ 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 = []
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (2 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 03/13] verification/rvgen: Implement state and transition parser based on Lark Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() " Nam Cao
` (8 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing code.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 32 ++++++++++++++++---------
1 file changed, 21 insertions(+), 11 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e6f476b903b0..3e7040398a20 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -12,6 +12,7 @@ from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
+from .automata import ConstraintRule
class dot2k(Monitor, Dot2c):
@@ -177,6 +178,14 @@ class ha2k(dot2k):
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
+ self.has_invariant = False
+ self.has_guard = False
+ for state in self._states:
+ if state.inv:
+ self.has_invariant = True
+ for transition in self.transitions:
+ if transition.rule or transition.reset:
+ self.has_guard = True
def fill_monitor_class_type(self) -> str:
if self._is_id_monitor():
@@ -218,14 +227,13 @@ class ha2k(dot2k):
assert env.rstrip(f"_{self.name}") in self.envs
return env
- def __start_to_invariant_check(self, constr: str) -> str:
+ def __start_to_invariant_check(self, inv: ConstraintRule) -> str:
# by default assume the timer has ns expiration
- env = self.__get_constraint_env(constr)
clock_type = "ns"
- if self.env_types.get(env.rstrip(f"_{self.name}")) == "j":
+ if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+ return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
def __start_to_conv(self, constr: str) -> str:
"""
@@ -320,20 +328,22 @@ class ha2k(dot2k):
self.invariants[key] = rules[0]
def __fill_verify_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
_else = ""
- for state, constr in sorted(self.invariants.items()):
- check_str = self.__start_to_invariant_check(constr)
- buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ if not state.inv:
+ continue
+
+ check_str = self.__start_to_invariant_check(state.inv)
+ buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
buff.append(f"\t\t{check_str};")
_else = "else "
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (3 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 06/13] verification/rvgen: Convert __fill_verify_guards_func() " Nam Cao
` (7 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed states from
Lark.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 36 ++++++++++++++++++-------
1 file changed, 27 insertions(+), 9 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3e7040398a20..3a39ae29e41e 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,18 @@ class ha2k(dot2k):
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"
+ if inv.unit == "j":
+ clock_type = "jiffy"
+
+ env = inv.env + self.enum_suffix
+ val = inv.val.replace("()", "(ha_mon)")
+
+ return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+ f" {val}, time_ns)")
+
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
Merge guard constraints as a single C return statement.
@@ -463,15 +475,14 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
return conflict_guards, conflict_invs
def __fill_setup_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []
- buff.append(
+ buff = [
f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
conditions = ["next_state == curr_state"]
conditions += [f"event != {e}{self.enum_suffix}"
@@ -480,13 +491,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state, constr in sorted(self.invariants.items()):
- buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
- buff.append(f"\t\t{constr};")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ inv = self.__parse_invariant(inv)
+ buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+ buff.append(f"\t\t{inv};")
_else = "else "
- for state in self.invariants:
- buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")
buff.append("}\n")
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (4 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() " Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables Nam Cao
` (6 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Prepare to remove self.guards and self.__parse_constraints(), convert
__fill_verify_guards_func() to use the parsed transitions from Lark.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 39 ++++++++++++++++++++-----
1 file changed, 31 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3a39ae29e41e..cf7e5ddc649c 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -221,6 +221,20 @@ class ha2k(dot2k):
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:
+ env = c.env + self.enum_suffix
+ op = c.op
+ val = self.__adjust_value(c.val, c.unit)
+
+ cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
+ if sep:
+ cond += f" {sep}"
+ buff.append(cond)
+ 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(",")
@@ -398,8 +412,9 @@ f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
def __fill_verify_guards_func(self) -> list[str]:
buff = []
- if not self.guards:
- return []
+
+ if not self.has_guard:
+ return
buff.append(
f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
@@ -410,14 +425,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
""")
_else = ""
- for edge, constr in sorted(self.guards.items()):
+ for transition in self.transitions:
+ if not transition.rule and not transition.reset:
+ continue
+
buff.append(f"\t{_else}if (curr_state == "
- f"{self.states[edge[0]]}{self.enum_suffix} && "
- f"event == {self.events[edge[1]]}{self.enum_suffix})")
- if constr.count(";") > 0:
+ f"{transition.src}{self.enum_suffix} && "
+ f"event == {transition.event}{self.enum_suffix})")
+ rule = transition.rule
+ reset = transition.reset
+ if rule and reset:
buff[-1] += " {"
- buff += [f"\t\t{c};" for c in constr.split(";")]
- if constr.count(";") > 0:
+ if rule:
+ buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
+ if reset:
+ buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
+ if rule and reset:
_else = "} else "
else:
_else = "else "
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (5 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 06/13] verification/rvgen: Convert __fill_verify_guards_func() " Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 08/13] verification/rvgen: Simplify the generation for " Nam Cao
` (5 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Hybrid automata monitors's clock variables have two different
representations:
- The invariant representation, which is the timestamp when the invariant
expires
- The guard representation, which is the timestamp when the clock is last
reset
This dual representation makes the logic quite difficult to follow (well,
at least for me). It also complicates the monitors and the generation tool,
as it requires conversion back and forth between the representation.
Simplify by using the clock variables for a single purpose: storing the
time stamp since the clock is last reset.
This also allows simplifying rvgen, which will be done in a follow-up
commit.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
include/rv/ha_monitor.h | 60 ++++++------------------
kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------
kernel/trace/rv/monitors/stall/stall.c | 2 +-
3 files changed, 17 insertions(+), 63 deletions(-)
diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h
index d59507e8cb30..1ce3fd324d2c 100644
--- a/include/rv/ha_monitor.h
+++ b/include/rv/ha_monitor.h
@@ -253,19 +253,8 @@ static inline void __ha_monitor_timer_callback(struct ha_monitor *ha_mon)
}
/*
- * The clock variables have 2 different representations in the env_store:
- * - The guard representation is the timestamp of the last reset
- * - The invariant representation is the timestamp when the invariant expires
- * As the representations are incompatible, care must be taken when switching
- * between them: the invariant representation can only be used when starting a
- * timer when the previous representation was guard (e.g. no other invariant
- * started since the last reset operation).
- * Likewise, switching from invariant to guard representation without a reset
- * can be done only by subtracting the exact value used to start the invariant.
- *
- * Reading the environment variable (ha_get_clk) also reflects this difference
- * any reads in states that have an invariant return the (possibly negative)
- * time since expiration, other reads return the time since last reset.
+ * The clock variables store the time epoch - the timestamp when the clock was last reset.
+ * They are read by subtracting the time epoch from the current time.
*/
/*
@@ -279,31 +268,21 @@ static inline void ha_reset_clk_ns(struct ha_monitor *ha_mon, enum envs env, u64
{
WRITE_ONCE(ha_mon->env_store[env], time_ns);
}
-static inline void ha_set_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 value, u64 time_ns)
-{
- WRITE_ONCE(ha_mon->env_store[env], time_ns + value);
-}
-static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
+static inline bool ha_check_invariant_ns(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_ns)
{
- return READ_ONCE(ha_mon->env_store[env]) >= time_ns;
+ return time_ns - READ_ONCE(ha_mon->env_store[env]) <= expire_ns;
}
/*
* ha_invariant_passed_ns - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_ns(ha_mon, env, expire - passed, time_ns);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -317,32 +296,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monitor *ha_mon, enum envs env)
{
WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64());
}
-static inline void ha_set_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 value)
-{
- WRITE_ONCE(ha_mon->env_store[env], get_jiffies_64() + value);
-}
-static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon,
- enum envs env, u64 time_ns)
+static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enum envs env,
+ u64 time_ns, u64 expire_jiffy)
{
- return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64());
-
+ return time_after64(READ_ONCE(ha_mon->env_store[env]) + expire_jiffy, get_jiffies_64());
}
/*
* ha_invariant_passed_jiffy - prepare the invariant and return the time since reset
*/
-static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env,
- u64 expire, u64 time_ns)
+static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enum envs env, u64 time_ns)
{
- u64 passed = 0;
-
if (env < 0 || env >= ENV_MAX_STORED)
return 0;
if (ha_monitor_env_invalid(ha_mon, env))
return 0;
- passed = ha_get_env(ha_mon, env, time_ns);
- ha_set_invariant_jiffy(ha_mon, env, expire - passed);
- return passed;
+ return ha_get_env(ha_mon, env, time_ns);
}
/*
@@ -389,14 +357,14 @@ static inline void ha_setup_timer(struct ha_monitor *ha_mon)
static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_jiffy(ha_mon, env, time_ns);
mod_timer(&ha_mon->timer, get_jiffies_64() + expire - passed);
}
static inline void ha_start_timer_ns(struct ha_monitor *ha_mon, enum envs env,
u64 expire, u64 time_ns)
{
- u64 passed = ha_invariant_passed_ns(ha_mon, env, expire, time_ns);
+ u64 passed = ha_invariant_passed_ns(ha_mon, env, time_ns);
ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED,
nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns);
diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/monitors/nomiss/nomiss.c
index 31f90f3638d8..6b3f93866d56 100644
--- a/kernel/trace/rv/monitors/nomiss/nomiss.c
+++ b/kernel/trace/rv/monitors/nomiss/nomiss.c
@@ -57,24 +57,12 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == ready_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
else if (curr_state == running_nomiss)
- return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns);
+ return ha_check_invariant_ns(ha_mon, clk_nomiss, time_ns, DEADLINE_NS(ha_mon));
return true;
}
-static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
- enum states curr_state, enum events event,
- enum states next_state, u64 time_ns)
-{
- if (curr_state == next_state)
- return;
- if (curr_state == ready_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
- else if (curr_state == running_nomiss)
- ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns);
-}
-
static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
enum states curr_state, enum events event,
enum states next_state, u64 time_ns)
@@ -122,8 +110,6 @@ static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns))
return false;
- ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns);
-
if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns))
return false;
diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monitors/stall/stall.c
index 9ccfda6b0e73..1aa65d7e690d 100644
--- a/kernel/trace/rv/monitors/stall/stall.c
+++ b/kernel/trace/rv/monitors/stall/stall.c
@@ -38,7 +38,7 @@ static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
enum states next_state, u64 time_ns)
{
if (curr_state == enqueued_stall)
- return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns);
+ return ha_check_invariant_jiffy(ha_mon, clk_stall, time_ns, threshold_jiffies);
return true;
}
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 08/13] verification/rvgen: Simplify the generation for clock variables
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (6 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 07/13] rv: Simply hybrid automata monitors's clock variables Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 09/13] verification/rvgen: Delete __parse_constraint() Nam Cao
` (4 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate code to
convert between the two representations.
Delete __fill_convert_inv_guard_func() and its associates. Update
__start_to_invariant_check() to how invariants now work.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 89 +------------------------
1 file changed, 1 insertion(+), 88 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index cf7e5ddc649c..c662c888f991 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -247,7 +247,7 @@ class ha2k(dot2k):
if inv.unit == "j":
clock_type = "jiffy"
- return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
+ 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:
"""
@@ -376,40 +376,6 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
buff.append("\treturn true;\n}\n")
return buff
- def __fill_convert_inv_guard_func(self) -> list[str]:
- buff = []
- if not self.invariants:
- return []
-
- conflict_guards, conflict_invs = self.__find_inv_conflicts()
- if not conflict_guards and not conflict_invs:
- return []
-
- buff.append(
-f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
-\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
-\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
- buff.append("\tif (curr_state == next_state)\n\t\treturn;")
-
- _else = ""
- for state, constr in sorted(self.invariants.items()):
- # a state with invariant can reach us without reset
- # multiple conflicts must have the same invariant, otherwise we cannot
- # know how to reset the value
- conf_i = [start for start, end in conflict_invs if end == state]
- # we can reach a guard without reset
- conf_g = [e for s, e in conflict_guards if s == state]
- if not conf_i and not conf_g:
- continue
- buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
-
- buff.append(f"\t\t{self.__start_to_conv(constr)};")
- _else = "else "
-
- buff.append("}\n")
- return buff
-
def __fill_verify_guards_func(self) -> list[str]:
buff = []
@@ -449,54 +415,6 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
buff.append("\treturn res;\n}\n")
return buff
- def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
- set[tuple[int, _StateConstraintKey]]]:
- """
- Run a breadth first search from all states with an invariant.
- Find any conflicting constraints reachable from there, this can be
- another state with an invariant or an edge with a non-reset guard.
- Stop when we find a reset.
-
- Return the set of conflicting guards and invariants as tuples of
- conflicting state and constraint key.
- """
- conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
- conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
- for start_idx in self.invariants:
- queue = deque([(start_idx, 0)]) # (state_idx, distance)
- env = self.__get_constraint_env(self.invariants[start_idx])
-
- while queue:
- curr_idx, distance = queue.popleft()
-
- # Check state condition
- if curr_idx != start_idx and curr_idx in self.invariants:
- conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
- continue
-
- # Check if we should stop
- if distance > len(self.states):
- break
- if curr_idx != start_idx and distance > 1:
- continue
-
- for event_idx, next_state_name in enumerate(self.function[curr_idx]):
- if next_state_name == self.invalid_state_str:
- continue
- curr_guard = self.guards.get((curr_idx, event_idx), "")
- if "reset" in curr_guard and env in curr_guard:
- continue
-
- if env in curr_guard:
- conflict_guards.add((start_idx,
- _EventConstraintKey(curr_idx, event_idx)))
- continue
-
- next_idx = self.states.index(next_state_name)
- queue.append((next_idx, distance + 1))
-
- return conflict_guards, conflict_invs
-
def __fill_setup_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -555,8 +473,6 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
*/""")
buff += self.__fill_verify_invariants_func()
- inv_conflicts = self.__fill_convert_inv_guard_func()
- buff += inv_conflicts
buff += self.__fill_verify_guards_func()
buff += self.__fill_setup_invariants_func()
@@ -569,9 +485,6 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
if self.invariants:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if inv_conflicts:
- buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
- "next_state, time_ns);\n")
if self.guards:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 09/13] verification/rvgen: Delete __parse_constraint()
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (7 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 08/13] verification/rvgen: Simplify the generation for " Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 10/13] verification/rvgen: Switch __get_event_variables() to Lark Nam Cao
` (3 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 67 ++-----------------------
1 file changed, 4 insertions(+), 63 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index c662c888f991..5ea5d16df29b 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -177,7 +177,6 @@ class ha2k(dot2k):
if not self.is_hybrid_automata():
raise AutomataError("Detected deterministic automaton, use the 'da' class")
self.trace_h = self._read_template_file("trace_hybrid.h")
- self.__parse_constraints()
self.has_invariant = False
self.has_guard = False
for state in self._states:
@@ -295,64 +294,6 @@ class ha2k(dot2k):
separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " "
return ["res = " + separator.join(rules)]
- def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
- rule, reset) -> None:
- # event constrains are tuples and allow both rules and reset
- # state constraints are only used for expirations (e.g. clk<N)
- if self.is_event_constraint(key):
- if not rule and not reset:
- raise AutomataError("Unrecognised event constraint "
- f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
- if rule and (rule["env"] in self.env_types and
- rule["env"] not in self.env_stored):
- raise AutomataError("Clocks in hybrid automata always require a storage"
- f" ({rule["env"]})")
- else:
- if not rule:
- raise AutomataError("Unrecognised state constraint "
- f"({self.states[key]}: {constr})")
- if rule["env"] not in self.env_stored:
- raise AutomataError("State constraints always require a storage "
- f"({rule["env"]})")
- if rule["op"] not in ["<", "<="]:
- raise AutomataError("State constraints must be clock expirations like"
- f" clk<N ({rule.string})")
-
- def __parse_constraints(self) -> None:
- self.guards: dict[_EventConstraintKey, str] = {}
- self.invariants: dict[_StateConstraintKey, str] = {}
- for key, constraint in self.constraints.items():
- rules = []
- resets = []
- for c, sep in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- self.__validate_constraint(key, c, rule, reset)
- if rule:
- value = rule["val"]
- value_len = len(rule["val"])
- unit = None
- if rule.groupdict().get("unit"):
- value_len += len(rule["unit"])
- unit = rule["unit"]
- c = c[:-(value_len)]
- value = self.__adjust_value(value, unit)
- if self.is_event_constraint(key):
- c = self.__parse_single_constraint(rule, value)
- if sep:
- c += f" {sep}"
- else:
- c = self.__parse_timer_constraint(rule, value)
- rules.append(c)
- if reset:
- c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
- resets.append(c)
- if self.is_event_constraint(key):
- res = self.__format_guard_rules(rules) + resets
- self.guards[key] = ";".join(res)
- else:
- self.invariants[key] = rules[0]
-
def __fill_verify_invariants_func(self) -> list[str]:
if not self.has_invariant:
return []
@@ -482,15 +423,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
{{""")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
"event, next_state, time_ns))\n\t\treturn false;\n")
- if self.guards:
+ if self.has_guard:
buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
"next_state, time_ns))\n\t\treturn false;\n")
- if self.invariants:
+ if self.has_invariant:
buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
buff.append("\treturn true;\n}\n")
@@ -567,7 +508,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
def _fill_timer_type(self) -> list:
- if self.invariants:
+ if self.has_invariant:
return [
"/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
"#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 10/13] verification/rvgen: Switch __get_event_variables() to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (8 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 09/13] verification/rvgen: Delete __parse_constraint() Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 11/13] verification/rvgen: Switch __create_matrix() " Nam Cao
` (2 subsequent siblings)
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 78 ++++++----------------
1 file changed, 19 insertions(+), 59 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 32c16736a41b..a29dcde1348c 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -578,45 +578,22 @@ class Automata:
def __get_event_variables(self) -> tuple[list[str], list[str]]:
events: list[str] = []
envs: list[str] = []
- # here we are at the begin of transitions, take a note, we will return later.
- cursor = self.__get_cursor_begin_events()
- for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
- if not line.startswith('"'):
- break
+ for transition in self.transitions:
+ events.append(transition.event)
- # transitions have the format:
- # "all_fired" -> "both_fired" [ label = "disable_irq" ];
- # ------------ event is here ------------^^^^^
- split_line = line.split()
- if len(split_line) > 1 and split_line[1] == "->":
- event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
-
- # when a transition has more than one label, they are like this
- # "local_irq_enable\nhw_local_irq_enable_n"
- # so split them.
-
- for i in event.split("\\n"):
- # if the event contains a constraint (hybrid automata),
- # it will be separated by a ";":
- # "sched_switch;x<1000;reset(x)"
- ev, *constr = i.split(";")
- if constr:
- if len(constr) > 2:
- raise AutomataError("Only 1 constraint and 1 reset are supported")
- envs += self.__extract_env_var(constr)
- events.append(ev)
- else:
- # state labels have the format:
- # "enable_fired" [label = "enable_fired\ncondition"];
- # ----- label is here -----^^^^^
- # label and node name must be the same, condition is optional
- state = line.split("label")[1].split('"')[1]
- _, *constr = state.split("\\n")
- if constr:
- if len(constr) > 1:
- raise AutomataError("Only 1 constraint is supported in the state")
- envs += self.__extract_env_var([constr[0].replace(" ", "")])
+ if transition.reset:
+ envs.append(transition.reset.env)
+ self.env_stored.add(transition.reset.env)
+ if transition.rule:
+ for c, _ in transition.rule.rules:
+ envs.append(c.env)
+ self.__extract_env_var(c)
+
+ for state in self._states:
+ if state.inv:
+ envs.append(state.inv.env)
+ self.__extract_env_var(state.inv)
return sorted(set(events)), sorted(set(envs))
@@ -640,28 +617,11 @@ class Automata:
seps.append(None)
return zip(exprs, seps)
- def __extract_env_var(self, constraint: list[str]) -> list[str]:
- env = []
- for c, _ in self._split_constraint_expr(constraint):
- rule = self.constraint_rule.search(c)
- reset = self.constraint_reset.search(c)
- if rule:
- env.append(rule["env"])
- if rule.groupdict().get("unit"):
- self.env_types[rule["env"]] = rule["unit"]
- if rule["val"][0].isalpha():
- self.constraint_vars.add(rule["val"])
- # try to infer unit from constants or parameters
- val_for_unit = rule["val"].lower().replace("()", "")
- if val_for_unit.endswith("_ns"):
- self.env_types[rule["env"]] = "ns"
- if val_for_unit.endswith("_jiffies"):
- self.env_types[rule["env"]] = "j"
- if reset:
- env.append(reset["env"])
- # environment variables that are reset need a storage
- self.env_stored.add(reset["env"])
- return env
+ def __extract_env_var(self, constraint: ConstraintCondition) -> list[str]:
+ if constraint.unit:
+ self.env_types[constraint.env] = constraint.unit
+ if constraint.val[0].isalpha():
+ self.constraint_vars.add(constraint.val)
def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
# transform the array into a dictionary
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 11/13] verification/rvgen: Switch __create_matrix() to Lark
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (9 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 10/13] verification/rvgen: Switch __get_event_variables() to Lark Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 12/13] verification/rvgen: Remove the old state variables Nam Cao
2026-05-05 6:59 ` [PATCH 13/13] verification/rvgen: Remove dead code Nam Cao
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matrix(), that is not used
anymore.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 47 ++++++----------------
tools/verification/rvgen/rvgen/dot2k.py | 2 +-
2 files changed, 13 insertions(+), 36 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index a29dcde1348c..d40d037f4cfd 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -405,7 +405,7 @@ class Automata:
self.constraint_vars = set()
self.self_loop_reset_events = set()
self.events, self.envs = self.__get_event_variables()
- self.function, self.constraints = self.__create_matrix()
+ self.function = self.__create_matrix()
self.events_start, self.events_start_run = self.__store_init_events()
self.env_stored = sorted(self.env_stored)
self.constraint_vars = sorted(self.constraint_vars)
@@ -623,10 +623,10 @@ class Automata:
if constraint.val[0].isalpha():
self.constraint_vars.add(constraint.val)
- def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]:
+ def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = self.states
+ states = [s.name for s in self._states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -641,39 +641,16 @@ class Automata:
# declare the matrix....
matrix = [[self.invalid_state_str for _ in range(nr_event)] for _ in range(nr_state)]
- constraints: dict[_ConstraintKey, list[str]] = {}
- # and we are back! Let's fill the matrix
- cursor = self.__get_cursor_begin_events()
-
- for line in map(str.lstrip,
- islice(self.__dot_lines, cursor, None)):
-
- if not line or line[0] != '"':
- break
-
- split_line = line.split()
-
- if len(split_line) > 2 and split_line[1] == "->":
- origin_state = split_line[0].replace('"', '').replace(',', '_')
- dest_state = split_line[2].replace('"', '').replace(',', '_')
- possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
- for event in possible_events.split("\\n"):
- event, *constr = event.split(";")
- if constr:
- key = _EventConstraintKey(states_dict[origin_state], events_dict[event])
- constraints[key] = constr
- # those events reset also on self loops
- if origin_state == dest_state and "reset" in "".join(constr):
- self.self_loop_reset_events.add(event)
- matrix[states_dict[origin_state]][events_dict[event]] = dest_state
- else:
- state = line.split("label")[1].split('"')[1]
- state, *constr = state.replace(" ", "").split("\\n")
- if constr:
- constraints[_StateConstraintKey(states_dict[state])] = constr
-
- return matrix, constraints
+ for transition in self.transitions:
+ src, dst = transition.src, transition.dst
+ event = transition.event
+ if src == dst and transition.reset:
+ # those events reset also on self loops
+ self.self_loop_reset_events.add(event)
+ matrix[states_dict[src]][events_dict[event]] = dst
+
+ return matrix
def __store_init_events(self) -> tuple[list[bool], list[bool]]:
events_start = [False] * len(self.events)
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 5ea5d16df29b..708e1f223728 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -394,7 +394,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
def __fill_constr_func(self) -> list[str]:
buff = []
- if not self.constraints:
+ if not self.has_invariant and not self.has_guard:
return []
buff.append(
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 12/13] verification/rvgen: Remove the old state variables
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (10 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 11/13] verification/rvgen: Switch __create_matrix() " Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
2026-05-05 6:59 ` [PATCH 13/13] verification/rvgen: Remove dead code Nam Cao
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
The state variables (states, initial_state, final_states) only capture the
states' names and have less information than their Lark-based counterparts.
Switch to use the new state variables and delete these old ones.
Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/automata.py | 9 ++++-----
tools/verification/rvgen/rvgen/dot2c.py | 10 +++++-----
tools/verification/rvgen/rvgen/dot2k.py | 8 ++++----
3 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index d40d037f4cfd..e0d3f83cbd3c 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -398,8 +398,7 @@ class Automata:
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()
- self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.states, self.initial_state, self.final_states = self.__parse_states()
self.env_types = {}
self.env_stored = set()
self.constraint_vars = set()
@@ -590,7 +589,7 @@ class Automata:
envs.append(c.env)
self.__extract_env_var(c)
- for state in self._states:
+ for state in self.states:
if state.inv:
envs.append(state.inv.env)
self.__extract_env_var(state.inv)
@@ -626,7 +625,7 @@ class Automata:
def __create_matrix(self) -> list[list[str]]:
# transform the array into a dictionary
events = self.events
- states = [s.name for s in self._states]
+ states = [s.name for s in self.states]
events_dict = {}
states_dict = {}
nr_event = 0
@@ -662,7 +661,7 @@ class Automata:
for j in range(len(self.states)):
if self.function[j][i] != self.invalid_state_str:
curr_event_used += 1
- if self.function[j][i] == self.initial_state:
+ if self.function[j][i] == self.initial_state.name:
curr_event_will_init += 1
if self.function[0][i] != self.invalid_state_str:
curr_event_from_init = True
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index fc85ba1f649e..22938ce1bf6c 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -29,10 +29,10 @@ class Dot2c(Automata):
def __get_enum_states_content(self) -> list[str]:
buff = []
- buff.append(f"\t{self.initial_state}{self.enum_suffix},")
+ buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
for state in self.states:
if state != self.initial_state:
- buff.append(f"\t{state}{self.enum_suffix},")
+ buff.append(f"\t{state.name}{self.enum_suffix},")
buff.append(f"\tstate_max{self.enum_suffix},")
return buff
@@ -142,7 +142,7 @@ class Dot2c(Automata):
def format_aut_init_states_string(self) -> list[str]:
buff = []
buff.append("\t.state_names = {")
- buff.append(self.__get_string_vector_per_line_content(self.states))
+ buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states]))
buff.append("\t},")
return buff
@@ -159,7 +159,7 @@ class Dot2c(Automata):
return buff
def __get_max_strlen_of_states(self) -> int:
- max_state_name = len(max(self.states, key=len))
+ max_state_name = max((len(s.name) for s in self.states))
return max(max_state_name, len(self.invalid_state_str))
def get_aut_init_function(self) -> str:
@@ -199,7 +199,7 @@ class Dot2c(Automata):
return buff
def get_aut_init_initial_state(self) -> str:
- return self.initial_state
+ return self.initial_state.name
def format_aut_init_initial_state(self) -> list[str]:
buff = []
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 708e1f223728..12d944bcd6f3 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -179,7 +179,7 @@ class ha2k(dot2k):
self.trace_h = self._read_template_file("trace_hybrid.h")
self.has_invariant = False
self.has_guard = False
- for state in self._states:
+ for state in self.states:
if state.inv:
self.has_invariant = True
for transition in self.transitions:
@@ -305,7 +305,7 @@ f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
{{"""]
_else = ""
- for state in self._states:
+ for state in self.states:
if not state.inv:
continue
@@ -373,7 +373,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")
_else = ""
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
@@ -382,7 +382,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\t\t{inv};")
_else = "else "
- for state in self._states:
+ for state in self.states:
inv = state.inv
if not inv:
continue
--
2.47.3
^ permalink raw reply related [flat|nested] 14+ messages in thread* [PATCH 13/13] verification/rvgen: Remove dead code
2026-05-05 6:59 [PATCH 00/13] rv: Convert rvgen to Lark Nam Cao
` (11 preceding siblings ...)
2026-05-05 6:59 ` [PATCH 12/13] verification/rvgen: Remove the old state variables Nam Cao
@ 2026-05-05 6:59 ` Nam Cao
12 siblings, 0 replies; 14+ messages in thread
From: Nam Cao @ 2026-05-05 6:59 UTC (permalink / raw)
To: Gabriele Monaco, Steven Rostedt, Wander Lairson Costa,
linux-trace-kernel, linux-kernel
Cc: Nam Cao
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
^ permalink raw reply related [flat|nested] 14+ messages in thread