From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 6FB133A8721; Mon, 8 Jun 2026 08:57:26 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; cv=none; b=UqXt/n/8TfA1VYM6V/iK0nFMv4C2V1nk4EJxs63nko22U6bvRzT2TAlPmFIoHH+inhIny0CnqBYFUVk/3KZKGoMPlesc3HmB3ffrIw9a5ARLviajNkdlBF37aPhy6MzbZtvUcHRsUB/J9LDRWKddQz1O52EacrcxF4JOCiIJO8g= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; c=relaxed/simple; bh=I0RFHaJ0uyVjD8Y4yb61W3Sq9/JxOY6uGz6HtaofIoU=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=i9DQifuNMkepqclhR232CophPvfVWjMkv30cJOd+IPUUw/CsshZegDzg1hpreDRYJnGalf2jJpNaYSF8NsaH6KGMN74iXLQ+MmqShW6l62qB1zNKL7nVkYqwMjfTbkBNkYzaSvR0vHX/XZkX+8QXcEQ/BdkMPlO0anckHrYWNW4= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=zNIJHk57; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=zqgp5DEz; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="zNIJHk57"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="zqgp5DEz" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=CmzKqFGh0o8uVtWZjNM4SQj84FV9pp6B5uCmDnjQf6k=; b=zNIJHk57HKo5r9/D5zbEPjWpePD4LysYoSDQ9eFmcRTOBf04JZzmGjLyDjWMYHweUk1GpI c+Y8LpBYH4ar0N50U3og7afaEtNGwLVVoPJLFgB3MefN93SLAUZDDGU9NZWGSk1mRq4NPd corj8OnR0W1AXLQd/t9FCt6jtqqFX7n2mXYMwSjsh3OgJCaxvua/Eq4We3tLJ7t8f1PdoP L0eL8Lw3q2Hs+pr3gsDejOkhnd0rBi2qzKXThYC5nPW27SJ/03UKMSbB2ecNHwfk9YU75W Be/1nfkOzlLSULBi4e+3RuB26lWs+N9ER/Xk5DDvwQI8+7Atx7J6Jo+rHcTscA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=CmzKqFGh0o8uVtWZjNM4SQj84FV9pp6B5uCmDnjQf6k=; b=zqgp5DEzmPrpEMd+OC2N/YPPNDAm8JX3fvPZCW/DCvo24JmIxgo6rpIKwf8qrUeXPAJbb1 NDDxhq/1daG0N1Dw== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 01/13] verification/rvgen: Switch LTL parser to Lark Date: Mon, 8 Jun 2026 10:56:57 +0200 Message-ID: <970f991dbddd2372b9f32c31243b67e7fe88ecfd.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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/9d7c40099e23ff78f9d86ef69a26c1e8= a83e706a [1] Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- tools/verification/rvgen/__main__.py | 5 +- tools/verification/rvgen/rvgen/ltl2ba.py | 202 +++++++++-------------- 2 files changed, 82 insertions(+), 125 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 5c923dc10d0f..0915cf86e43b 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -14,6 +14,7 @@ if __name__ =3D=3D '__main__': from rvgen.container import Container from rvgen.ltl2k import ltl2k from rvgen.automata import AutomataError + from rvgen.ltl2ba import LTLError import argparse import sys =20 @@ -57,8 +58,8 @@ if __name__ =3D=3D '__main__': sys.exit(1) else: monitor =3D Container(vars(params)) - except AutomataError as e: - print(f"There was an error processing {params.spec}: {e}", file=3D= sys.stderr) + except (AutomataError, LTLError) as e: + print(f"There was an error processing {params.spec}:\n{e}", file= =3Dsys.stderr) sys.exit(1) =20 print(f"Writing the monitor into the directory {monitor.name}") diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/= rvgen/rvgen/ltl2ba.py index 016e7cf93bbb..7cebda61bce8 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -7,9 +7,7 @@ # https://doi.org/10.1007/978-0-387-34892-6_1 # With extra optimizations =20 -from ply.lex import lex -from ply.yacc import yacc -from .automata import AutomataError +import lark =20 # Grammar: # ltl ::=3D opd | ( ltl ) | ltl binop ltl | unop ltl @@ -30,42 +28,41 @@ from .automata import AutomataError # imply # equivalent =20 -tokens =3D ( - 'AND', - 'OR', - 'IMPLY', - 'UNTIL', - 'ALWAYS', - 'EVENTUALLY', - 'NEXT', - 'VARIABLE', - 'LITERAL', - 'NOT', - 'LPAREN', - 'RPAREN', - 'ASSIGN', -) - -t_AND =3D r'and' -t_OR =3D r'or' -t_IMPLY =3D r'imply' -t_UNTIL =3D r'until' -t_ALWAYS =3D r'always' -t_NEXT =3D r'next' -t_EVENTUALLY =3D r'eventually' -t_VARIABLE =3D r'[A-Z_0-9]+' -t_LITERAL =3D r'true|false' -t_NOT =3D r'not' -t_LPAREN =3D r'\(' -t_RPAREN =3D r'\)' -t_ASSIGN =3D r'=3D' -t_ignore_COMMENT =3D r'\#.*' -t_ignore =3D ' \t\n' - -def t_error(t): - raise AutomataError(f"Illegal character '{t.value[0]}'") - -lexer =3D lex() +GRAMMAR =3D r''' +start: assign+ + +assign: VARIABLE "=3D" _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_][A-Z0-9_]*/ +LITERAL: "true" | "false" + +COMMENT: "#" /.*/ "\n" +%ignore COMMENT + +%import common.WS +%ignore WS +''' + +class LTLError(Exception): + "Exception raised for malformed linear temporal logic" =20 class GraphNode: uid =3D 0 @@ -97,7 +94,7 @@ class GraphNode: return self.id < other.id =20 class ASTNode: - uid =3D 1 + uid =3D 0 =20 def __init__(self, op): self.op =3D op @@ -433,90 +430,49 @@ class Literal: node.old |=3D {n} return node.expand(node_set) =20 -def p_spec(p): - ''' - spec : assign - | assign spec - ''' - if len(p) =3D=3D 3: - p[2].append(p[1]) - p[0] =3D p[2] - else: - p[0] =3D [p[1]] - -def p_assign(p): - ''' - assign : VARIABLE ASSIGN ltl - ''' - p[0] =3D (p[1], p[3]) - -def p_ltl(p): - ''' - ltl : opd - | binop - | unop - ''' - p[0] =3D p[1] - -def p_opd(p): - ''' - opd : VARIABLE - | LITERAL - | LPAREN ltl RPAREN - ''' - if p[1] =3D=3D "true": - p[0] =3D ASTNode(Literal(True)) - elif p[1] =3D=3D "false": - p[0] =3D ASTNode(Literal(False)) - elif p[1] =3D=3D '(': - p[0] =3D p[2] - else: - p[0] =3D ASTNode(Variable(p[1])) - -def p_unop(p): - ''' - unop : ALWAYS ltl - | EVENTUALLY ltl - | NEXT ltl - | NOT ltl - ''' - if p[1] =3D=3D "always": - op =3D AlwaysOp(p[2]) - elif p[1] =3D=3D "eventually": - op =3D EventuallyOp(p[2]) - elif p[1] =3D=3D "next": - op =3D NextOp(p[2]) - elif p[1] =3D=3D "not": - op =3D NotOp(p[2]) - else: - raise AutomataError(f"Invalid unary operator {p[1]}") - - p[0] =3D ASTNode(op) - -def p_binop(p): - ''' - binop : opd UNTIL ltl - | opd AND ltl - | opd OR ltl - | opd IMPLY ltl - ''' - if p[2] =3D=3D "and": - op =3D AndOp(p[1], p[3]) - elif p[2] =3D=3D "until": - op =3D UntilOp(p[1], p[3]) - elif p[2] =3D=3D "or": - op =3D OrOp(p[1], p[3]) - elif p[2] =3D=3D "imply": - op =3D ImplyOp(p[1], p[3]) - else: - raise AutomataError(f"Invalid binary operator {p[2]}") - - p[0] =3D ASTNode(op) - -parser =3D yacc() +class Transform(lark.visitors.Transformer): + def unop(self, node): + if node[0] =3D=3D "always": + return ASTNode(AlwaysOp(node[1])) + if node[0] =3D=3D "eventually": + return ASTNode(EventuallyOp(node[1])) + if node[0] =3D=3D "next": + return ASTNode(NextOp(node[1])) + if node[0] =3D=3D "not": + return ASTNode(NotOp(node[1])) + raise ValueError("Unknown operator %s" % node[0]) + + def binop(self, node): + if node[1] =3D=3D "until": + return ASTNode(UntilOp(node[0], node[2])) + if node[1] =3D=3D "and": + return ASTNode(AndOp(node[0], node[2])) + if node[1] =3D=3D "or": + return ASTNode(OrOp(node[0], node[2])) + if node[1] =3D=3D "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(Literal(args =3D=3D "true")) + + def start(self, node): + return node + + def assign(self, node): + return node[0].op.name, node[1] + +parser =3D lark.Lark(GRAMMAR) =20 def parse_ltl(s: str) -> ASTNode: - spec =3D parser.parse(s) + try: + spec =3D parser.parse(s) + except lark.exceptions.UnexpectedInput as e: + raise LTLError(str(e)) + spec =3D Transform().transform(spec) =20 rule =3D None subexpr =3D {} @@ -528,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode: subexpr[assign[0]] =3D assign[1] =20 if rule is None: - raise AutomataError("Please define your specification in the \"RUL= E =3D \" format") + raise LTLError("Please define your specification in the \"RULE =3D= \" format") =20 for node in rule: if not isinstance(node.op, Variable): --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 98F1C3B0AE5; Mon, 8 Jun 2026 08:57:26 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; cv=none; b=MedVJYT2gqvLQoScbEMY/H2g+Rx5wBKBVuFKuInaVQVJnOY53OlUlEoAeFVOvsfOULkFuNixZ04nV5FKzdP5BCeMe2kafsYcOWQoKM/pEo9Djv4+AUSrPwsn5P9/VuT5dCF8CGm+pUWHdB2jz7IJ1GrnGHBmcW3fB1NV7ewJRfU= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; c=relaxed/simple; bh=axik62hu9fRkZUmDyzJ4xqvLwHa8J79mHVN6BX3Pm/Q=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=GTXL1K6ahkK++qIXaVikG89OYIRv6e/anO3TcXPjGIX3PhJIRPjv1ZF8l1xH8PYrT7BVflCEb2LMBsn460Yb6TLJWhkAAc60vR9hF8ZusfwIv4pUAfPN58gFhkaAIU/MFOYlqO6kR+PokntJ5iZQXZeFDdaTzka53TYH3DU3WAM= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=qBg+kTiM; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=Qz2VBEJH; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="qBg+kTiM"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="Qz2VBEJH" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=wxi1srjPJPML219bqJzQ0+WNJaQw3+gcjWnYqs0hQWs=; b=qBg+kTiMEB964ztn0X9E8dzfMC4W2KJyZLY3vxY5uo+ykL9YMQEaCsTmzjJ6oi4H1G2zpu +0lBbakYspGDM5lSe81M1dBUnHN/GDQyKAX9xrBr417MUIlRCuZGBt1wEknqtBhm62ix8W BAXJUm195eLwozsw+TzUStaFyedOqUZ7AxU2LmH6ysImgxdCAmhtTv8epipnS0AMgi6H7Q MFuwizj5kPXN9he8a3/t0YjeCGpqp5a61/qDnI3ePoSGZTjLqDr/gQcovYmrTL2vD22P+h U0+id6OjHABuuoNFvJTem9XPyg/8seodOIP1Q0fKPQG42OuqAMi1bFOV5UyXeA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=wxi1srjPJPML219bqJzQ0+WNJaQw3+gcjWnYqs0hQWs=; b=Qz2VBEJHRc/EeEOtvb0Ym4dr18z7MR7mOkG9axM/O8cdQLYPXmB23RrqwLNOIsunzPEgnz XbrdDpRnvzyjTmAw== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 02/13] verification/rvgen: Introduce a parse tree for automata using Lark Date: Mon, 8 Jun 2026 10:56:58 +0200 Message-ID: <1688aa1c7b7064488aa080b7ac580b6b08cb74f9.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- tools/verification/rvgen/rvgen/automata.py | 186 +++++++++++++++++++++ 1 file changed, 186 insertions(+) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index b9f8149f7118..8649d982383d 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -13,6 +13,191 @@ import re from typing import Iterator from itertools import islice =20 +import lark + +class ParseTree: + # based on https://graphviz.org/doc/info/lang.html + # with the irrelevant stuffs (port and compass) removed + grammar =3D r''' + start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}" + + stmt_list: (stmt ";"? stmt_list)? + + stmt: node_stmt + | edge_stmt + | attr_stmt + | ID "=3D" 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 "=3D" 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: CNAME + | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/ + | ESCAPED_STRING + + %import common.CNAME + %import common.ESCAPED_STRING + %import common.WS + %ignore WS + ''' + + @staticmethod + def parse_edge(tree: lark.Tree) -> tuple[str, str]: + # only support a simple node-to-node edge + nodes =3D [] + for node in tree.iter_subtrees_topdown(): + if node.data =3D=3D "node_id": + nodes.append(node.children[0].strip('"')) + + if len(nodes) !=3D 2: + raise AutomataError("Only state-to-state transition is support= ed") + + return tuple(nodes) + + class ParseNodes(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.nodes =3D set() + super().__init__(*args, **kwargs) + + def node_stmt(self, tree): + node_id =3D tree.children[0] + node =3D node_id.children[0].strip('"') + self.nodes.add(node) + + class ParseEdges(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.edges =3D set() + super().__init__(*args, **kwargs) + + def edge_stmt(self, tree): + edge =3D 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 =3D [{}] + self.default_edge_attrs =3D [{}] + + self.node_attrs =3D {} + self.edge_attrs =3D {} + + super().__init__(*args, **kwargs) + + @staticmethod + def __get_attrs(stmt: lark.Tree) -> dict[str, str]: + attrs =3D {} + + for node in stmt.iter_subtrees(): + if node.data =3D=3D "a_list": + attrs[node.children[0]] =3D 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].cop= y()) + self.default_edge_attrs.append(self.default_edge_attrs[-1].cop= y()) + + children =3D 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 =3D tree.children[0] + node =3D node_id.children[0].strip('"') + + attrs =3D self.default_node_attrs[-1].copy() + attrs |=3D self.__get_attrs(tree) + + if attrs: + if node in self.node_attrs: + self.node_attrs[node] =3D attrs | self.node_attrs[node] + else: + self.node_attrs[node] =3D attrs + + return self.visit_children(tree) + + def edge_stmt(self, tree): + edge =3D ParseTree.parse_edge(tree) + + attrs =3D self.default_edge_attrs[-1].copy() + attrs |=3D self.__get_attrs(tree) + + if attrs: + if edge in self.edge_attrs: + self.edge_attrs[edge] =3D attrs | self.edge_attrs[edge] + else: + self.edge_attrs[edge] =3D attrs + + return self.visit_children(tree) + + def attr_stmt(self, tree): + attr_type =3D tree.children[0].data + attrs =3D self.__get_attrs(tree) + + if attr_type =3D=3D "node": + self.default_node_attrs[-1] |=3D attrs + elif attr_type =3D=3D "edge": + self.default_edge_attrs[-1] |=3D attrs + else: + # graph attributes are irrelevant + pass + + self.visit_children(tree) + + def __init__(self, dot_file): + parser =3D lark.Lark(self.grammar, parser=3D'lalr') + node_parser =3D self.ParseNodes() + edge_parser =3D self.ParseEdges() + attributes_parser =3D self.ParseAttributes() + + try: + with open(dot_file, "r") as f: + tree =3D parser.parse(f.read()) + attributes_parser.visit(tree) + node_parser.visit(tree) + edge_parser.visit(tree) + except OSError as exc: + raise AutomataError(exc.strerror) from exc + except lark.exceptions.UnexpectedInput as exc: + raise AutomataError(str(exc)) + + self.nodes =3D node_parser.nodes + self.edges =3D edge_parser.edges + self.node_attrs =3D attributes_parser.node_attrs + self.edge_attrs =3D attributes_parser.edge_attrs + class _ConstraintKey: """Base class for constraint keys.""" =20 @@ -66,6 +251,7 @@ class Automata: self.__dot_path =3D file_path self.name =3D model_name or self.__get_model_name() self.__dot_lines =3D self.__open_dot() + self.__parse_tree =3D ParseTree(file_path) self.states, self.initial_state, self.final_states =3D self.__get_= state_variables() self.env_types =3D {} self.env_stored =3D set() --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id E133C3B14BE; Mon, 8 Jun 2026 08:57:26 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; cv=none; b=YZ1CUEcLcl4ngH+LsPwYkMLbznhNr1RGZVCyFD9op7aK6gYntaH6si0v5+hdhJQxunKOxmAqSwjXkBYLqsn/PyUDnJJscQaXXGqu4OaeVpS3/OpM2IaiQiZI1nBR1iqclOJRq8I3xC8ve3nXX1Ah/BfCur27CAq2/3igGuGfu0c= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; c=relaxed/simple; bh=ezDTI9Ssy71qH8gl/qpo/ufrkH/UfQcR7UHF9HkpcqE=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=dBhwUt7C0p/i18wPqA3BHZ+cuju0gM4U0dnJt0YxpMu82DtVxFIX2YhnDd/oLywjPrvxhKJ5nC886IPgLErEj9v0wcpbOrD8+C3goiuB3q2gAJTPeFLF6z5gmgKOzhOY8HE1ePJsqZsXd7t9Ite591AnMvgnklB0z8GRPPLXs/0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=TYs1s+0L; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=IeYMX0No; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="TYs1s+0L"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="IeYMX0No" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=RurhsS8UBLDY7FDyN6pd33mJFyUia5q2qCGObl7k6gU=; b=TYs1s+0L3ytrYs9edxiwU6Lk8UZhkA2MNGfwmdDGvWVnynE56rD53xJtAGX8LHWB+74S20 Vvq0XEBQZW5Y21BXiX8Z2XSeXf7N2LboiRqVOppnr1q9l/dMXFEXXCVgIxLhjGeaK8zmKD J9Tuy599+aUIxI8qiXyxsmYKan//reh7A9gdeZ3ELcdeViBWWF6jtdrDRImruxsxSbxtY5 DK3BJs0ABv0fP5LHONpQmR1Qxkn6InDWb/xEmd3oiiyncbjgSqqAwukoAxxneENT81Bi8/ KSB2fI852iIPCfEx1uDeI/XE4ohAYp+Fqo2iYd/CVZG0IvPQdT3wL2o3AZR4GQ== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=RurhsS8UBLDY7FDyN6pd33mJFyUia5q2qCGObl7k6gU=; b=IeYMX0No+vK3tCGu9PWWmax0czoan4+LrjQTqe6HY4ukWn2qG5zzcMtCI1ghcV/yrMftIa ZJoCOxneO04JZIDQ== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 03/13] verification/rvgen: Implement state and transition parser based on Lark Date: Mon, 8 Jun 2026 10:56:59 +0200 Message-ID: <8964bf8b7c20fa1a5b8ef2a7081cf8ba11d70526.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- tools/verification/rvgen/rvgen/automata.py | 216 +++++++++++++++++++++ 1 file changed, 216 insertions(+) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 8649d982383d..b86275e7bf28 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -198,6 +198,164 @@ class ParseTree: self.node_attrs =3D attributes_parser.node_attrs self.edge_attrs =3D attributes_parser.edge_attrs =20 +class ConstraintCondition: + def __init__(self, env: str, op: str, val: str, unit=3DNone): + self.env =3D env + self.op =3D op + self.val =3D val + self.unit =3D unit + if unit is None: + # try to infer unit from constants or parameters + val_for_unit =3D val.lower().replace("()", "") + if val_for_unit.endswith("_ns"): + self.unit =3D "ns" + if val_for_unit.endswith("_jiffies"): + self.unit =3D "j" + +class ConstraintRule: + grammar =3D r''' + rule: condition (OP condition)* + + OP: "&&" | "||" + + condition: ENV CMP_OP VAL UNIT? + + ENV: CNAME + + CMP_OP: "=3D=3D" | "<=3D" | "<" | ">=3D" | ">" + + 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 =3D=3D 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 =3D [[c, None]] + + def chain(self, op: str, c: ConstraintCondition): + self.rules[-1][1] =3D op + self.rules.append([c, None]) + +class ConstraintReset: + def __init__(self, env): + self.env =3D env + +class StateLabelParser: + grammar =3D r''' + label: CNAME ("\\n" condition)? + + %import common.CNAME + %import common.WS + %ignore WS + ''' + ConstraintRule.grammar + + parser =3D lark.Lark(grammar, parser=3D'lalr', start=3D"label") + + def __init__(self, label: str): + try: + tree =3D self.parser.parse(label) + except lark.exceptions.UnexpectedInput as exc: + raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}")) + + self.state =3D tree.children[0] + self.constraint =3D None + + if len(tree.children) =3D=3D 2: + self.constraint =3D ConstraintCondition(*tree.children[1].chil= dren) + if self.constraint.op not in ("<", "<=3D"): + raise AutomataError("State constraints must be clock expir= ations like" + f" clk tuple[list[str], str, list[str]]: # wait for node declaration states =3D [] --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 5D0003B3887; Mon, 8 Jun 2026 08:57:27 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; cv=none; b=tEKjGU3+WvmQvb0hH0uIDm2eBfvr82tdhJKSFMFO5L5AhY24T2XsIZ4HnSKtzkSh1tszs9nDScIh31IHHPOqsirEBPU+xkz/hGMRvqJJLr1FWl+jB6F21UOIpt0zC7yzhxlaysh9Q+PYNCEjfFSzIFhhHqnlTw1DrKevWheO/Tc= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909048; c=relaxed/simple; bh=fWDOil+1nalo8bXMWCuGsQj/R1sipl6kSB3bKbJG1kw=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=fQXi/fQ1Tewua7LQF8A8CXGwcdiq/CTauevPJMDKiTmEjevXmRfJU3qsOhqWnwfCh8PbbHv/1ZuvWiKb8+iJ0nyVmVhunO7X72VTxnB9464xvYGkJrDMfilK1Lb9HA67XQKnkLISAZNmK5CIaXrSQ2Ee4+5bNjwkS5pGmDFrmbA= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=palc1tK8; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=nuUIbVlR; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="palc1tK8"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="nuUIbVlR" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=XGdJn1kK1yjAiJ1GvD7KIXuOfVDkCf2rQ+rNK2oX5iE=; b=palc1tK8/tZYe4EtyvjtnVECPfUZzBXQ+XCa1FYYrdyDkxqCxTSLqlj2PydsO0MzZBpYvF bqo7Bu5PTT8YZHtn1bOCIeD50CK3/FM3qSHw/wL/sjboPrTOnq5EYlMv2p3QT8gJOknF91 IHF79Y3gbVgXB73zdZJobDXsRrjFlDNkEvTFm0DoaQbkMRMkaOkEsBzY5Y46QjHCBVHY/G dnEE2PAuBoWhGF6kDlSOETMb4CVp9oHCWdAieSHULnq8eEEdo1UzkP0xz8avSH4SwLcuMu Wy8SvPPt0BXHDXHYjhteXQcCWKGKqa/UY98CS2NN5Ngi7XF/HlB1aRboCi5kvA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909045; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=XGdJn1kK1yjAiJ1GvD7KIXuOfVDkCf2rQ+rNK2oX5iE=; b=nuUIbVlRpC6zV7LhxSgJiNc+5vHVn2Y47M2T3ECcaqo4UN+Q3cu2d9+8Zvun5MCC6fuT/J W5z+VMcsj+v9ckCA== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark Date: Mon, 8 Jun 2026 10:57:00 +0200 Message-ID: In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Convert __fill_verify_invariants_func() to use the parsed states information from Lark, prepare to remove the old raw text parsing code. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v3: - remove unused import --- 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/r= vgen/rvgen/dot2k.py index 110cfd69e53a..0595bfcd232e 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, AutomataEr= ror +from .automata import ConstraintCondition =20 =20 class dot2k(Monitor, Dot2c): @@ -177,6 +178,14 @@ class ha2k(dot2k): raise AutomataError("Detected deterministic automaton, use the= 'da' class") self.trace_h =3D self._read_template_file("trace_hybrid.h") self.__parse_constraints() + self.has_invariant =3D False + self.has_guard =3D False + for state in self._states: + if state.inv: + self.has_invariant =3D True + for transition in self.transitions: + if transition.rule or transition.reset: + self.has_guard =3D True =20 def fill_monitor_class_type(self) -> str: if self._is_id_monitor(): @@ -218,14 +227,13 @@ class ha2k(dot2k): assert env.removesuffix(f"_{self.name}") in self.envs return env =20 - def __start_to_invariant_check(self, constr: str) -> str: + def __start_to_invariant_check(self, inv: ConstraintCondition) -> str: # by default assume the timer has ns expiration - env =3D self.__get_constraint_env(constr) clock_type =3D "ns" - if self.env_types.get(env.removesuffix(f"_{self.name}")) =3D=3D "j= ": + if inv.unit =3D=3D "j": clock_type =3D "jiffy" =20 - return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, tim= e_ns)" + return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_= {self.name}, time_ns)" =20 def __start_to_conv(self, constr: str) -> str: """ @@ -320,20 +328,22 @@ class ha2k(dot2k): self.invariants[key] =3D rules[0] =20 def __fill_verify_invariants_func(self) -> list[str]: - buff =3D [] - if not self.invariants: + if not self.has_invariant: return [] =20 - buff.append( + buff =3D [ 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_d= ef} event, \t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) -{{""") +{{"""] =20 _else =3D "" - for state, constr in sorted(self.invariants.items()): - check_str =3D self.__start_to_invariant_check(constr) - buff.append(f"\t{_else}if (curr_state =3D=3D {self.states[stat= e]}{self.enum_suffix})") + for state in self._states: + if not state.inv: + continue + + check_str =3D self.__start_to_invariant_check(state.inv) + buff.append(f"\t{_else}if (curr_state =3D=3D {state.name}{self= .enum_suffix})") buff.append(f"\t\t{check_str};") _else =3D "else " =20 --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id F327A3B42F9; Mon, 8 Jun 2026 08:57:28 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; cv=none; b=puvRdrAqZ6W8oplWLqPVwtDR6d++u2Yb/oX9vUdad63cJs8rt25DxstloC0nnwZlMrqdvHq+q+tVU+72tqvYYE18tFmy4/UR1fsPQOTXz6LGPSO5468PpMK0nyqSL36DJ31dTJHTwysEWDP1rw4DELoOSRY7p0QnaV01+V+Ts0Y= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; c=relaxed/simple; bh=nxXI/sbEg7sQYczA8k0dJsBSDlRQ7oSqvTggSL6UfOM=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=R19rE5r/09SOcyw4nBQ331q3gfXyYcgEY+rbZLGh+cvfzT1hrqueB6Fc7yCj12OckDGem1YZFEGFgzAT84Brl2y9Dk513u64YHcXblibcrrZ38RIvJyH1Soyz4hyqn6+8A0GL5C9d3OasC6XqaDvhgd4mTUlF++r62mkeY+UiOo= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=ieOiJA1f; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=7x+MF/Fs; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="ieOiJA1f"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="7x+MF/Fs" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909046; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=hTq+GETCeldyfomjfzUFOZclOm/T6717ndV3i0vpoaI=; b=ieOiJA1fbN/ebbzDSM5c2vHGQXpVHcE6rGZRKawctdov7/zmdCGD/DGzKDJOQUHJOfV08P b7Pe1LLuJAbNpEiEhTic6NcCbcLlVqJhE2UlwJ5M5fbnXGTi+a6+wg5XxrQ714u5kOW6X5 9ekSIhhLHL0xYWPC7P/AgSLMOzmRQuBdLCVnqWXn2L3Qs0ACskJN+0b1JRi+mndb/0SkM1 lSjOuuzVKL/Bo62ug+OnN0T5Mo5xvWoQQ9KFzjbTO2rlliVTczamx5Gxvn3tOn+F9DWbU6 r3ZW488pR6yuCbQmIiV3DDM0ogmD7Dxuwz18jv8GDnHo8HuShuBuyBxKnxMXeA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909046; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=hTq+GETCeldyfomjfzUFOZclOm/T6717ndV3i0vpoaI=; b=7x+MF/Fs1HL2temJ9Lp2qRvKgS5Xk3W3sWAVYYa5aAP/RvpWkzI7O21mR48pN1X63JYOyp 26xr6eTtbIJ+KIAQ== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark Date: Mon, 8 Jun 2026 10:57:01 +0200 Message-ID: In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Prepare for self.invariants and __parse_constraints() to be removed. convert __fill_setup_invariants_func() to use the new parsed states from Lark. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- tools/verification/rvgen/rvgen/dot2k.py | 44 ++++++++++++++++++++----- 1 file changed, 35 insertions(+), 9 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index 0595bfcd232e..1b29792ed630 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -250,6 +250,26 @@ class ha2k(dot2k): return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.e= num_suffix}," f" {value}, time_ns)") =20 + def __parse_invariant(self, inv): + # by default assume the timer has ns expiration + clock_type =3D "ns" + if inv.unit =3D=3D "j": + clock_type =3D "jiffy" + + env =3D inv.env + self.enum_suffix + val =3D inv.val.replace("()", "(ha_mon)") + + match inv.unit: + case "us": + val *=3D 10**3 + case "ms": + val *=3D 10**6 + case "s": + val *=3D 10**9 + + 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 +483,14 @@ f"""static inline bool ha_verify_guards(struct ha_mon= itor *ha_mon, return conflict_guards, conflict_invs =20 def __fill_setup_invariants_func(self) -> list[str]: - buff =3D [] - if not self.invariants: + if not self.has_invariant: return [] =20 - buff.append( + buff =3D [ 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_eve= nts_def} event, \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) -{{""") +{{"""] =20 conditions =3D ["next_state =3D=3D curr_state"] conditions +=3D [f"event !=3D {e}{self.enum_suffix}" @@ -480,13 +499,20 @@ f"""static inline void ha_setup_invariants(struct ha_= monitor *ha_mon, buff.append(f"\tif ({condition_str})\n\t\treturn;") =20 _else =3D "" - for state, constr in sorted(self.invariants.items()): - buff.append(f"\t{_else}if (next_state =3D=3D {self.states[stat= e]}{self.enum_suffix})") - buff.append(f"\t\t{constr};") + for state in self._states: + inv =3D state.inv + if not inv: + continue + inv =3D self.__parse_invariant(inv) + buff.append(f"\t{_else}if (next_state =3D=3D {state.name}{self= .enum_suffix})") + buff.append(f"\t\t{inv};") _else =3D "else " =20 - for state in self.invariants: - buff.append(f"\telse if (curr_state =3D=3D {self.states[state]= }{self.enum_suffix})") + for state in self._states: + inv =3D state.inv + if not inv: + continue + buff.append(f"\telse if (curr_state =3D=3D {state.name}{self.e= num_suffix})") buff.append("\t\tha_cancel_timer(ha_mon);") =20 buff.append("}\n") --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 2F9BA3B47C9; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; cv=none; b=g7nQIzRWuOetkyGwThMcgDPdR1ZnKSFgfPXt7pihod9gb5tNum/fgLTKnlipLTCRgTX4vNXz/JR2znHUHqWcEbEAoP5TM1xIECBZ8YPnBs6PHT+WqFUGGvquIG2zqsx0kp6qMvOWxRpQV0LzErjjtzvYu6Qxf46Pbom0bHkhKCE= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; c=relaxed/simple; bh=8zumhxn0uBbwstlGZfXS86mKSv2fQYnnyl7DAZnKNKE=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=HHBlZjYCsa2LIre8CV0A9qW6OWOmdVVZmCerkBnbWovhEeKTkoTRDOen4vJtImGDAm1KqBrHzcfOb/apOmVYZZct0TJLogUokyCyM0wKwbDuKEz95/lzEPUkzkFEPqmBat25y6P1N9CZh2Xw5S24U8NdMZqq2rFYHOQuOyZ3kcY= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=Di5JtR7f; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=smKVrjtB; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="Di5JtR7f"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="smKVrjtB" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909046; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=VIYbDZpsVo2P3xrAA9JNP2SSQR+D2XJCTE0OZczvZUs=; b=Di5JtR7fH/8Rvs/LzpWG4qP++OK444mQIoFPaF93IzjMhwTWJ8t+Acr1hVkzjn9dgYjl6G jrTG7gMdXlOafdCB49Ugg2BiLWVOWZDswWpmWgWlk1A86PjETbwtbjTvw4zx5uwR+POMpv IoZBn2kGNOmGaekekdJYjzEnFF+SHxb8DP8Eo8bhTBUdxP4FmBmY99iQdHJvKGJcCJGQSW lN+Tsk16g8a1VNKY5Ve79U+8R96wm1yL1khOEEV5Ekjo+MXGcpezwBLp76UAWqQkjj7S2P 4U0K2MmYv1PXwH/qMM5HCgWIuyUim9eh3jmwmkdUymfOdpDiWjITGZKvWEHeQA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909046; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=VIYbDZpsVo2P3xrAA9JNP2SSQR+D2XJCTE0OZczvZUs=; b=smKVrjtBqZvftYl8NSC7kzT+lTh5yXKimd7Qf6AlhISx3UpMHOnxzmsfh+lR4bxfhjJp0l lDgxcevSotBB15DA== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 06/13] verification/rvgen: Convert __fill_verify_guards_func() to Lark Date: Mon, 8 Jun 2026 10:57:02 +0200 Message-ID: <8182bdf6a06a762799bd6edc2a5bdaca4b3ed916.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Prepare to remove self.guards and self.__parse_constraints(), convert __fill_verify_guards_func() to use the parsed transitions from Lark. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- tools/verification/rvgen/rvgen/dot2k.py | 38 +++++++++++++++++++------ 1 file changed, 30 insertions(+), 8 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index 1b29792ed630..e91717fde30d 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -221,6 +221,19 @@ 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}" =20 + def __parse_guard_rule(self, rule) -> list[str]: + buff =3D [] + for c, sep in rule.rules: + env =3D c.env + self.enum_suffix + op =3D c.op + val =3D self.__adjust_value(c.val, c.unit) + + cond =3D f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}" + if sep: + cond +=3D f" {sep}" + buff.append(cond) + return buff + def __get_constraint_env(self, constr: str) -> str: """Extract the second argument from an ha_ function""" env =3D constr.split("(")[1].split()[1].rstrip(")").rstrip(",") @@ -287,7 +300,7 @@ class ha2k(dot2k): rules =3D invalid_checks + rules =20 separator =3D "\n\t\t " if sum(len(r) for r in rules) > 80 el= se " " - return ["res =3D " + separator.join(rules)] + return ["res =3D " + separator.join(rules) + ";"] =20 def __validate_constraint(self, key: tuple[int, int] | int, constr: st= r, rule, reset) -> None: @@ -406,7 +419,8 @@ f"""static inline void ha_convert_inv_guard(struct ha_m= onitor *ha_mon, =20 def __fill_verify_guards_func(self) -> list[str]: buff =3D [] - if not self.guards: + + if not self.has_guard: return [] =20 buff.append( @@ -418,14 +432,22 @@ f"""static inline bool ha_verify_guards(struct ha_mon= itor *ha_mon, """) =20 _else =3D "" - 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 =3D=3D " - f"{self.states[edge[0]]}{self.enum_suffix} && " - f"event =3D=3D {self.events[edge[1]]}{self.enum_su= ffix})") - if constr.count(";") > 0: + f"{transition.src}{self.enum_suffix} && " + f"event =3D=3D {transition.event}{self.enum_suffix= })") + rule =3D transition.rule + reset =3D transition.reset + if rule and reset: buff[-1] +=3D " {" - buff +=3D [f"\t\t{c};" for c in constr.split(";")] - if constr.count(";") > 0: + if rule: + buff.append("\t\t" + self.__format_guard_rules(self.__pars= e_guard_rule(rule))[0]) + if reset: + buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.en= um_suffix}, time_ns);") + if rule and reset: _else =3D "} else " else: _else =3D "else " --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 5608F3B47D2; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909053; cv=none; b=hJqQcVEfxXhWXwHkPiYkwHD4gGWJG0PQVmK6WTQK7b5VSA2BrxgW6qX6khyXU1pGGirSvPoHBzD/U0ZkVLnopjft63TkQYc2lUFSQIeelR/l6gEI3GiJQ3/xGaIldvLPv+1PXhlmK0gZtFL+DRjEb7a1WE7+igUNdSeY/3ZrvTI= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909053; c=relaxed/simple; bh=t8Yp1bXY6HZ9xmibsWPBng/F81fqrrv91sgUj0BddMY=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=rcqfWg3CMFHzVT+7h5FZLG4sLOOP4AfSLRJENhTT4BxJY47FyPI3wfSTTDjXMNFzZGfRa8gOj7b7shqp9Lwf1lCzv+xF9tmUTnChB5sw8CDKk+9gesdQhDba49xmEB7k7HCiCTBrxr2krqViJydad/OfXKWTo9o6rO94a84tgvA= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=Tt+IgOgh; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=KOz5IHLP; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="Tt+IgOgh"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="KOz5IHLP" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=8uyMduLEgsDHq0m1vaQkuvyF2pN5Tlwf1yEvS+sWVhs=; b=Tt+IgOghmBoX8p3XpUedX0gjNYukASw4QY3QOboRjODmO/3SB5hAwCw8ETg0eOyGEAIO6f bHNA8qnW0vJIX6YfX7mb+NiY2jsmnhdQKCnKQf26zYp3+KFn3pbglfHHgr0KYT+vVh8h+Z Gah2CVVQiGrCiOJtDrXrftOUn41iSJMpTxpXVI8ZAS8gfhrSxWsOYwrhX78+kN2wZ7Ge1w /CrvjiCFoc5HFO5kPrPnqSJb51XfuWRs51MOyR41UspNImMymOevVPlrFA1Gm1tckSrk81 yjWQSv6LswAqsLCYm8Uzg0sOMnEcEFV8bWILQZ2bR+Ih4I7KHioJ12+Nk24rTg== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=8uyMduLEgsDHq0m1vaQkuvyF2pN5Tlwf1yEvS+sWVhs=; b=KOz5IHLPS92bwGAH0+fPeINt1SCDdHnJx3H4VlC6GGexFnVQs4scN51+NxzIoqkvXKZdcX UAlAtHhYMQywE0DA== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 07/13] rv: Simplify hybrid automata monitors's clock variables Date: Mon, 8 Jun 2026 10:57:03 +0200 Message-ID: <08188c28f274da63a3f8549add3086a92aef45e5.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v3: - fix wrongly passing expire to ha_invariant_passed_jiffy() - typo --- include/rv/ha_monitor.h | 64 ++++++------------------ kernel/trace/rv/monitors/nomiss/nomiss.c | 18 +------ kernel/trace/rv/monitors/stall/stall.c | 2 +- 3 files changed, 19 insertions(+), 65 deletions(-) diff --git a/include/rv/ha_monitor.h b/include/rv/ha_monitor.h index 28d3c74cabfc..9144b4c06f3f 100644 --- a/include/rv/ha_monitor.h +++ b/include/rv/ha_monitor.h @@ -327,19 +327,8 @@ static inline void __ha_monitor_timer_callback(struct = ha_monitor *ha_mon) } =20 /* - * 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 expi= res - * As the representations are incompatible, care must be taken when switch= ing - * between them: the invariant representation can only be used when starti= ng a - * timer when the previous representation was guard (e.g. no other invaria= nt - * started since the last reset operation). - * Likewise, switching from invariant to guard representation without a re= set - * can be done only by subtracting the exact value used to start the invar= iant. - * - * Reading the environment variable (ha_get_clk) also reflects this differ= ence - * any reads in states that have an invariant return the (possibly negativ= e) - * 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. */ =20 /* @@ -353,31 +342,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 env= s 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 e= nvs env, + u64 time_ns, u64 expire_ns) { - return READ_ONCE(ha_mon->env_store[env]) >=3D time_ns; + return READ_ONCE(ha_mon->env_store[env]) >=3D time_ns - expire_ns; } /* * ha_invariant_passed_ns - prepare the invariant and return the time sinc= e reset */ -static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum e= nvs env, - u64 expire, u64 time_ns) +static inline u64 ha_invariant_passed_ns(struct ha_monitor *ha_mon, enum e= nvs env, u64 time_ns) { - u64 passed =3D 0; - if (env < 0 || env >=3D ENV_MAX_STORED) return 0; if (ha_monitor_env_invalid(ha_mon, env)) return 0; - passed =3D 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); } =20 /* @@ -391,32 +370,21 @@ static inline void ha_reset_clk_jiffy(struct ha_monit= or *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) +static inline bool ha_check_invariant_jiffy(struct ha_monitor *ha_mon, enu= m envs env, + u64 time_ns, u64 expire_jiffy) { - 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) -{ - return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64()); - + return time_after64(READ_ONCE(ha_mon->env_store[env]), get_jiffies_64() -= expire_jiffy); } /* * ha_invariant_passed_jiffy - prepare the invariant and return the time s= ince reset */ -static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enu= m envs env, - u64 expire, u64 time_ns) +static inline u64 ha_invariant_passed_jiffy(struct ha_monitor *ha_mon, enu= m envs env, u64 time_ns) { - u64 passed =3D 0; - if (env < 0 || env >=3D ENV_MAX_STORED) return 0; if (ha_monitor_env_invalid(ha_mon, env)) return 0; - passed =3D 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); } =20 /* @@ -463,14 +431,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 en= vs env, u64 expire, u64 time_ns) { - u64 passed =3D ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns); + u64 passed =3D ha_invariant_passed_jiffy(ha_mon, env, time_ns); =20 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 =3D ha_invariant_passed_ns(ha_mon, env, expire, time_ns); + u64 passed =3D ha_invariant_passed_ns(ha_mon, env, time_ns); =20 ha_start_timer_jiffy(ha_mon, ENV_MAX_STORED, nsecs_to_jiffies(expire - passed + TICK_NSEC - 1), time_ns); @@ -516,7 +484,7 @@ static inline void ha_start_timer_ns(struct ha_monitor = *ha_mon, enum envs env, u64 expire, u64 time_ns) { int mode =3D HRTIMER_MODE_REL_HARD; - u64 passed =3D ha_invariant_passed_ns(ha_mon, env, expire, time_ns); + u64 passed =3D ha_invariant_passed_ns(ha_mon, env, time_ns); =20 if (RV_MON_TYPE =3D=3D RV_MON_PER_CPU) mode |=3D HRTIMER_MODE_PINNED; @@ -525,7 +493,7 @@ static inline void ha_start_timer_ns(struct ha_monitor = *ha_mon, enum envs env, static inline void ha_start_timer_jiffy(struct ha_monitor *ha_mon, enum en= vs env, u64 expire, u64 time_ns) { - u64 passed =3D ha_invariant_passed_jiffy(ha_mon, env, expire, time_ns); + u64 passed =3D ha_invariant_passed_jiffy(ha_mon, env, time_ns); =20 ha_start_timer_ns(ha_mon, ENV_MAX_STORED, jiffies_to_nsecs(expire - passed), time_ns); diff --git a/kernel/trace/rv/monitors/nomiss/nomiss.c b/kernel/trace/rv/mon= itors/nomiss/nomiss.c index 8ead8783c29f..515ece5ce0ca 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_monit= or *ha_mon, enum states next_state, u64 time_ns) { if (curr_state =3D=3D 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 =3D=3D 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; } =20 -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 =3D=3D next_state) - return; - if (curr_state =3D=3D ready_nomiss) - ha_inv_to_guard(ha_mon, clk_nomiss, DEADLINE_NS(ha_mon), time_ns); - else if (curr_state =3D=3D 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; =20 - 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; =20 diff --git a/kernel/trace/rv/monitors/stall/stall.c b/kernel/trace/rv/monit= ors/stall/stall.c index 3c38fb1a0159..b265578f845c 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 =3D=3D 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_ji= ffies); return true; } =20 --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 5B35C3B47D6; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; cv=none; b=TMzP4Lv3IUGENNcruaXmxENWOf8nltWhmTsspoAmvzeP8Ai2y4lDyi+4IHvOw+aJLrpN9B7NEfpRsyvEbFeE0ScjBmOcaVe8brfm0oCHSYcZaZEzEhVXNjI194pQfH/X4QyjknQEX8GFTRlt2WjLklSnoyreGABR6nunxrbqhHI= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909051; c=relaxed/simple; bh=hzk7wwL4YpZjPt7CTDtp1gn5/7sdD/SaQLz0JUdHGvU=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=GRfgb8Nq/SfK9EM6GfZxJNeOXi+L1TiJGbxYfym3+lT44ZIt3p0V6/O0ZunyKqnU5pI2Xn0mkyw5Cq8zvriZQm6nRvwSa0yIoBFnumUru9IesdrKj8yHJGNEnIQkpLzjwLYobHEaUzAy4x2j6DbR15JkTwZPPNzeuXJ8NUXRFn4= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=i9F2FPne; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=t9QI+6Oa; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="i9F2FPne"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="t9QI+6Oa" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PTuMWZJQaJHSFCHxageLFGEL0EPkBs1RBomFaBfK0cQ=; b=i9F2FPnenJmdYZTd8dvqNOlq03s1FNwGSj9OIj2mcLOhEvc/rkeJ1MqM9g/774WpqLuuBs ki3gYeEOVvJNH4jYEBLub0qrmNsHuy8f33QtwQr/+DFNbEeTzSsrLxd/Mgt6zjBN8BDuvj 28XAwFvaNQgDXseQIl89FfMmdO7ZWWCSk54Ru1WFzM+Es6mw1JprahnecP0Gv0v7UfjA25 Vkth5Pji9IPxIUMsKqoMu2AyTQqMD7BXZJBfIKHsc7TucM1rvpGF9xYwLY8WkhshjhkAtX 50xuj09LPSTC5pZCOW4XN77s1/dTcKLqm3desJC0eCLTiz3oijKPzPthwqcEEA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PTuMWZJQaJHSFCHxageLFGEL0EPkBs1RBomFaBfK0cQ=; b=t9QI+6Oa5bJT2TE5uiHk0rRR1eJCMnMyUbZSpwElsWroAUUMON3MslW4BJPYmDZeU1Yi9W 6QigIO4LI4KLylBg== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 08/13] verification/rvgen: Simplify the generation for clock variables Date: Mon, 8 Jun 2026 10:57:04 +0200 Message-ID: In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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 --- tools/verification/rvgen/rvgen/dot2k.py | 96 +------------------------ 1 file changed, 3 insertions(+), 93 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index e91717fde30d..6d346a718a39 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -246,7 +246,9 @@ class ha2k(dot2k): if inv.unit =3D=3D "j": clock_type =3D "jiffy" =20 - return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_= {self.name}, time_ns)" + value =3D self.__adjust_value(inv.val, inv.unit) + + return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_= {self.name}, time_ns, {value})" =20 def __start_to_conv(self, constr: str) -> str: """ @@ -383,40 +385,6 @@ f"""static inline bool ha_verify_invariants(struct ha_= monitor *ha_mon, buff.append("\treturn true;\n}\n") return buff =20 - def __fill_convert_inv_guard_func(self) -> list[str]: - buff =3D [] - if not self.invariants: - return [] - - conflict_guards, conflict_invs =3D 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_d= ef} event, -\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) -{{""") - buff.append("\tif (curr_state =3D=3D next_state)\n\t\treturn;") - - _else =3D "" - 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 w= e cannot - # know how to reset the value - conf_i =3D [start for start, end in conflict_invs if end =3D= =3D state] - # we can reach a guard without reset - conf_g =3D [e for s, e in conflict_guards if s =3D=3D state] - if not conf_i and not conf_g: - continue - buff.append(f"\t{_else}if (curr_state =3D=3D {self.states[stat= e]}{self.enum_suffix})") - - buff.append(f"\t\t{self.__start_to_conv(constr)};") - _else =3D "else " - - buff.append("}\n") - return buff - def __fill_verify_guards_func(self) -> list[str]: buff =3D [] =20 @@ -456,54 +424,6 @@ f"""static inline bool ha_verify_guards(struct ha_moni= tor *ha_mon, buff.append("\treturn res;\n}\n") return buff =20 - def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstrain= tKey]], - set[tuple[int, _StateConstrain= tKey]]]: - """ - 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]] =3D set() - conflict_invs: set[tuple[int, _StateConstraintKey]] =3D set() - for start_idx in self.invariants: - queue =3D deque([(start_idx, 0)]) # (state_idx, distance) - env =3D self.__get_constraint_env(self.invariants[start_idx]) - - while queue: - curr_idx, distance =3D queue.popleft() - - # Check state condition - if curr_idx !=3D 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 !=3D start_idx and distance > 1: - continue - - for event_idx, next_state_name in enumerate(self.function[= curr_idx]): - if next_state_name =3D=3D self.invalid_state_str: - continue - curr_guard =3D 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 =3D 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 [] @@ -554,16 +474,9 @@ f"""static inline void ha_setup_invariants(struct ha_m= onitor *ha_mon, * the next state has a constraint, cancel it in any other case and to che= ck * that it didn't expire before the callback run. Transitions to the same = state * without a reset never affect timers. - * Due to the different representations between invariants and guards, the= re is - * a function to convert it in case invariants or guards are reachable from - * another invariant without reset. Those are not present if not required = in - * the model. This is all automatic but is worth checking because it may s= how - * errors in the model (e.g. missing resets). */""") =20 buff +=3D self.__fill_verify_invariants_func() - inv_conflicts =3D self.__fill_convert_inv_guard_func() - buff +=3D inv_conflicts buff +=3D self.__fill_verify_guards_func() buff +=3D self.__fill_setup_invariants_func() =20 @@ -576,9 +489,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") =20 if self.guards: buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event= , " --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id E94693B4E81; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; cv=none; b=lTfE0JxwuFjDTfZO3C1s4jXTG7khHFoHM0h9y7DlB1ldLZpVuJZy6PFWt8RAQ4mKCQVvA1CX1Qs+t1kwTTj6PAwySdu5hOKSwUAQSxsqxqS1vyViKx3zjAnbtfqsQh5VZD7mN1H63s7PJIHNuIgrDmtAHXCPO5md3le9qT8BuRo= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; c=relaxed/simple; bh=xB+mFvL/Gk3hD0symPhFYGjtdqFOIbUfP3scdyYgoWw=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=HLBdsaj1xKFRWpVNPMTKcUMLcuBzOOEuDF67z1iT9/2o7fVpcF5Sgix23gJkp8OVLt02emxiwahCbey3m5AbsyE2MSuTIKCX3Wvv7mrDVWnPRjHsDxXXrNFYTowmBl01bz4LCgvh3RqN0gVkeuopOgqQLKbL6tzs/ZJAipfqdHI= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=ZeE3bKyK; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=T97ZN7Kw; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="ZeE3bKyK"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="T97ZN7Kw" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PcYajoyp4TEVGAqefl9kQPnOV2nCEMbqQf4yFAPefF8=; b=ZeE3bKyKiG7FFvOJ5+pa0t0uXdbjfydew6WWUcmUX29sCnTwvA6v4KKJm2DQZHpBmx2HdW 24qDYnboitTn+K/57BMRnNwZ4aZcxuDABz/jPTzws3rdgCT/Z1/mr25QE3t8ZN7B5B9aHN KRvLIYSNqDVPpEJz8Gii9xuOI0IGSsCi6t3xBuOmGXHqYbSekR6rOoFPljJKbWL3BqykCC Vb6mJVW8vL8IGUHQib6CV56wt4P/GYzs2IbQVCX5qLBk3JudSQOMeXd1M9RrLWu5rTvXoV 2hR/cwncR8bmipyD0Nm3qsKiKOnVOE0g6kmwNf6LL8yescvCisKnMqQF9/B23w== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909047; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PcYajoyp4TEVGAqefl9kQPnOV2nCEMbqQf4yFAPefF8=; b=T97ZN7Kw2oLw395zWn+7/DfDMM4/xyFdQqe+sHcuvLfAS/+PuLlSmfslYv/25NPn5aDsUG Rn2uGKnteXbvf9Dw== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 09/13] verification/rvgen: Delete __parse_constraint() Date: Mon, 8 Jun 2026 10:57:05 +0200 Message-ID: <8d9b9068a5dde8256edd7debe7aab33e15a7fc51.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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 --- 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/r= vgen/rvgen/dot2k.py index 6d346a718a39..a38ef735a861 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 =3D self._read_template_file("trace_hybrid.h") - self.__parse_constraints() self.has_invariant =3D False self.has_guard =3D False for state in self._states: @@ -304,64 +303,6 @@ class ha2k(dot2k): separator =3D "\n\t\t " if sum(len(r) for r in rules) > 80 el= se " " return ["res =3D " + separator.join(rules) + ";"] =20 - def __validate_constraint(self, key: tuple[int, int] | int, constr: st= r, - rule, reset) -> None: - # event constrains are tuples and allow both rules and reset - # state constraints are only used for expirations (e.g. clk None: - self.guards: dict[_EventConstraintKey, str] =3D {} - self.invariants: dict[_StateConstraintKey, str] =3D {} - for key, constraint in self.constraints.items(): - rules =3D [] - resets =3D [] - for c, sep in self._split_constraint_expr(constraint): - rule =3D self.constraint_rule.search(c) - reset =3D self.constraint_reset.search(c) - self.__validate_constraint(key, c, rule, reset) - if rule: - value =3D rule["val"] - value_len =3D len(rule["val"]) - unit =3D None - if rule.groupdict().get("unit"): - value_len +=3D len(rule["unit"]) - unit =3D rule["unit"] - c =3D c[:-(value_len)] - value =3D self.__adjust_value(value, unit) - if self.is_event_constraint(key): - c =3D self.__parse_single_constraint(rule, value) - if sep: - c +=3D f" {sep}" - else: - c =3D self.__parse_timer_constraint(rule, value) - rules.append(c) - if reset: - c =3D f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_= suffix}, time_ns)" - resets.append(c) - if self.is_event_constraint(key): - res =3D self.__format_guard_rules(rules) + resets - self.guards[key] =3D ";".join(res) - else: - self.invariants[key] =3D rules[0] - def __fill_verify_invariants_func(self) -> list[str]: if not self.has_invariant: return [] @@ -486,15 +427,15 @@ f"""static bool ha_verify_constraint(struct ha_monito= r *ha_mon, \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) {{""") =20 - 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= ") =20 - 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") =20 - if self.invariants: + if self.has_invariant: buff.append("\tha_setup_invariants(ha_mon, curr_state, event, = next_state, time_ns);\n") =20 buff.append("\treturn true;\n}\n") @@ -571,7 +512,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor = *ha_mon, return self.__fill_hybrid_get_reset_functions() + self.__fill_cons= tr_func() =20 def _fill_timer_type(self) -> list: - if self.invariants: + if self.has_invariant: return [ "/* XXX: If the monitor has several instances, conside= r HA_TIMER_WHEEL */", "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id C800C3B47F6; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; cv=none; b=CrCRnpvd9kMtp7KdPzUavPzcDmFTyIhcdgVTMvBW+JUUcJGNsdqSHWJ8vGK3Rzx81GHbpo91IK1iz6iscEYzBAXqVmFLSwXZn3GgE32zjhZRaYDhlfmsvgM+9AiE8QJiiBvvDeUmV+ofRZM3WuqZTURWmHaSJUEDUgWbwNMoCJ4= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; c=relaxed/simple; bh=1MhA2aRP60183cN4HBLv3Aj1A/11LGKf9X/a96VYV4s=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=bNHxAtbRKOQv+iO+3APLXtwwvmln1aUa6x2uwIhZNFHVtkJPV6qKAQD/y49jrxCtcjDObxiqzHGvPRxrKhrhmRMGr4DuAfngD2qvzGbkCU7PaIen4ZhfZdqRB31cMrVeduulUiaDGq/26mqzb1w1QLaBiO6Npc29fGnW8UNhG5I= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=kzD4VZQc; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=Gx4eqVxO; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="kzD4VZQc"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="Gx4eqVxO" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=iUxzZb6WjvKyMCBcd/paWjOXRIvgAJq42QDVRrYlzeg=; b=kzD4VZQcOBlBJ7g62SxQ+ahKX7evRR/2LlOExgR1c0tqe/HgToT/4F8j1BJw3AaJipdTLs UTzftXzgf2ig1XqVIVcPt+7OssMSU59mnyKkla+nZLpsoDHUUQdnqKy+jXvRSbvCSPLoce bqt4LbcxiQAz2yVTWPHxBnjMnMe1uquCbgFK48F2pqTmyjMTL7wSa/0NGlKZOq/INvsHLM hE9XETm/dyvTAmv5h/4swqPqaWgHVhjTWo+SjDKNuq1bLtJIKiEg5JGQbhpqRMh6bNKfZz sfqBFRw2T0egRNVfklDj6lgQb4An1YvY5BaOXFbSqu8W1bkM/0mXagYOTaVW/A== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=iUxzZb6WjvKyMCBcd/paWjOXRIvgAJq42QDVRrYlzeg=; b=Gx4eqVxOdO3WQCAf7EikqZb5+61eyNPquCZvQMOToOyDyNKY8KHEjJ6au753H2X6rOAOlH WKTH6Gl9m8dAa8Cw== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 10/13] verification/rvgen: Switch __get_event_variables() to Lark Date: Mon, 8 Jun 2026 10:57:06 +0200 Message-ID: <50df4dd278779328cf2aa283c8353bac2281a337.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Switch __get_event_variables() to use the parsed results from Lark, instead of raw text processing. Signed-off-by: Nam Cao --- 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/verificatio= n/rvgen/rvgen/automata.py index b86275e7bf28..2e26bb863245 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -591,45 +591,22 @@ class Automata: def __get_event_variables(self) -> tuple[list[str], list[str]]: events: list[str] =3D [] envs: list[str] =3D [] - # here we are at the begin of transitions, take a note, we will re= turn later. - cursor =3D self.__get_cursor_begin_events() =20 - 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) =20 - # transitions have the format: - # "all_fired" -> "both_fired" [ label =3D "disable_irq" ]; - # ------------ event is here ------------^^^^^ - split_line =3D line.split() - if len(split_line) > 1 and split_line[1] =3D=3D "->": - event =3D "".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 =3D i.split(";") - if constr: - if len(constr) > 2: - raise AutomataError("Only 1 constraint and 1 r= eset are supported") - envs +=3D self.__extract_env_var(constr) - events.append(ev) - else: - # state labels have the format: - # "enable_fired" [label =3D "enable_fired\ncondition"]; - # ----- label is here -----^^^^^ - # label and node name must be the same, condition is optio= nal - state =3D line.split("label")[1].split('"')[1] - _, *constr =3D state.split("\\n") - if constr: - if len(constr) > 1: - raise AutomataError("Only 1 constraint is supporte= d in the state") - envs +=3D 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) =20 return sorted(set(events)), sorted(set(envs)) =20 @@ -653,28 +630,11 @@ class Automata: seps.append(None) return zip(exprs, seps) =20 - def __extract_env_var(self, constraint: list[str]) -> list[str]: - env =3D [] - for c, _ in self._split_constraint_expr(constraint): - rule =3D self.constraint_rule.search(c) - reset =3D self.constraint_reset.search(c) - if rule: - env.append(rule["env"]) - if rule.groupdict().get("unit"): - self.env_types[rule["env"]] =3D rule["unit"] - if rule["val"][0].isalpha(): - self.constraint_vars.add(rule["val"]) - # try to infer unit from constants or parameters - val_for_unit =3D rule["val"].lower().replace("()", "") - if val_for_unit.endswith("_ns"): - self.env_types[rule["env"]] =3D "ns" - if val_for_unit.endswith("_jiffies"): - self.env_types[rule["env"]] =3D "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): + if constraint.unit: + self.env_types[constraint.env] =3D constraint.unit + if constraint.val[0].isalpha(): + self.constraint_vars.add(constraint.val) =20 def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKe= y, list[str]]]: # transform the array into a dictionary --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id EB41C3B4E84; Mon, 8 Jun 2026 08:57:29 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; cv=none; b=X8QmX3vuYdpIG6F+0BD5c8MvRtMIHTVQTUwv0tcVlqVmc2WXW0MV+o5swIYRnGjWw+mRr7mQgrM0bcE0xwixUhAcfPOwRYnT44XG/amNWAWSXIgPf1CyL4jv8PxZF5W232J121dREA/wZ1nuo9nHSTiZlkyQ1jd5hExowHeLeM0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; c=relaxed/simple; bh=2WPjMY33orsToURjb7ZXHlVMYfa2lVeoNHh8wJLmook=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=lD/nU/lNzDKdULOEIkwIxsddl7u7pnsADC4DqlA/k7pEWZQ5yyX7J9+mpkQf6dKnR8SlUXidlBq3EKCrAyOi9YcITGXJbTKPyr4AcW0EJgbNYUw+9LHaAfxVChchTl1/N6Bk/IeWWB2JnvKx8PIQJJgX/LvSmTfDJFMhPd0V/Qw= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=ctis4pq1; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=fLFPMF54; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="ctis4pq1"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="fLFPMF54" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=Bv9On0UMEixskcuwDIk9hWUsnhiTMI2IAVc1WhiXmVY=; b=ctis4pq1bpb15NApuQ/+qCkOoG75DSBBc/96zlx17XtjvDMqgkFicx6iuSoauRNLfjvp7k gbZ883ePCbnDIzyxxDVB1Px0Q3ufEoyA/IoqMa7mS6W5E+QPIiHXOwm6xqZmuvFcOzZlfM p+5WWe6ziWTM1t6ySkuJvLoLqKq5ut+kMuNQ5cnybQbFnpcMSvpeAIrbTM1Sa9bfnU6NmW drCyJYfF482OA8gou02nO6MGgzMDXav4XrCfsnWglIwb3EWEDMRokViGI7xFAoSKHLTQc5 OSMua71SjonaSjteTG4Sz4qBlzLnEcLvZ/W/CdTRXbk2YrQcREYjHk/Xi9e1YA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=Bv9On0UMEixskcuwDIk9hWUsnhiTMI2IAVc1WhiXmVY=; b=fLFPMF54oZH+A/0nh6+u1E3eQB4GVsAjCvekcY6LogFNMa826R85AEPyZRwe71BLTnk5b1 hmLASAJ8Zh1uW5Aw== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 11/13] verification/rvgen: Switch __create_matrix() to Lark Date: Mon, 8 Jun 2026 10:57:07 +0200 Message-ID: <4e501de8e4e84a3de3370d82bf346f916aa97706.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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 --- 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/verificatio= n/rvgen/rvgen/automata.py index 2e26bb863245..4c302f5cba68 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -418,7 +418,7 @@ class Automata: self.constraint_vars =3D set() self.self_loop_reset_events =3D set() self.events, self.envs =3D self.__get_event_variables() - self.function, self.constraints =3D self.__create_matrix() + self.function =3D self.__create_matrix() self.events_start, self.events_start_run =3D self.__store_init_eve= nts() self.env_stored =3D sorted(self.env_stored) self.constraint_vars =3D sorted(self.constraint_vars) @@ -636,10 +636,10 @@ class Automata: if constraint.val[0].isalpha(): self.constraint_vars.add(constraint.val) =20 - def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKe= y, list[str]]]: + def __create_matrix(self) -> list[list[str]]: # transform the array into a dictionary events =3D self.events - states =3D self.states + states =3D [s.name for s in self._states] events_dict =3D {} states_dict =3D {} nr_event =3D 0 @@ -654,39 +654,16 @@ class Automata: =20 # declare the matrix.... matrix =3D [[self.invalid_state_str for _ in range(nr_event)] for = _ in range(nr_state)] - constraints: dict[_ConstraintKey, list[str]] =3D {} =20 - # and we are back! Let's fill the matrix - cursor =3D self.__get_cursor_begin_events() - - for line in map(str.lstrip, - islice(self.__dot_lines, cursor, None)): - - if not line or line[0] !=3D '"': - break - - split_line =3D line.split() - - if len(split_line) > 2 and split_line[1] =3D=3D "->": - origin_state =3D split_line[0].replace('"', '').replace(',= ', '_') - dest_state =3D split_line[2].replace('"', '').replace(',',= '_') - possible_events =3D "".join(split_line[split_line.index("l= abel") + 2:-1]).replace('"', '') - for event in possible_events.split("\\n"): - event, *constr =3D event.split(";") - if constr: - key =3D _EventConstraintKey(states_dict[origin_sta= te], events_dict[event]) - constraints[key] =3D constr - # those events reset also on self loops - if origin_state =3D=3D dest_state and "reset" in "= ".join(constr): - self.self_loop_reset_events.add(event) - matrix[states_dict[origin_state]][events_dict[event]] = =3D dest_state - else: - state =3D line.split("label")[1].split('"')[1] - state, *constr =3D state.replace(" ", "").split("\\n") - if constr: - constraints[_StateConstraintKey(states_dict[state])] = =3D constr - - return matrix, constraints + for transition in self.transitions: + src, dst =3D transition.src, transition.dst + event =3D transition.event + if src =3D=3D 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]] =3D dst + + return matrix =20 def __store_init_events(self) -> tuple[list[bool], list[bool]]: events_start =3D [False] * len(self.events) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index a38ef735a861..dc6d6f33729b 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -403,7 +403,7 @@ f"""static inline void ha_setup_invariants(struct ha_mo= nitor *ha_mon, =20 def __fill_constr_func(self) -> list[str]: buff =3D [] - if not self.constraints: + if not self.has_invariant and not self.has_guard: return [] =20 buff.append( --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 517703B4E8B; Mon, 8 Jun 2026 08:57:30 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; cv=none; b=LKUdxTgMvrwdys5DHHt7GfHRKmCjcclGKMZkXBX9aXBvB8aprJNzBu8c5c7/2fo05l6N5cLIa+OhncxnLk3wI5Ni+AYN8CA+p2SDGc8OioGfMYKYe3Eqi3JO1zFZgBw7cdzOiZPOvGismzHlq4y+xWbknN2vyFOKrMAXHFBDvWc= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909052; c=relaxed/simple; bh=6WE49ZkUd+vsfZbMzmZxNQpB4/9CkjUNJz9iNzUnQlY=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=OIr3t+xs+2V/7bHNBzHvSCTyJ1SoQ1/QJ4dKyxpkUMKMnpUdtyWb/VOEglmkweKpP61Utma0nGHjrkuakzGylZB949q2tANe/LEtiDVMt5XZC6DRwhay0jkBCMo4xH1hwr/k3TuLORR7rLWFWPnHTzLBn0P/e4SWUbHp9wnVN3U= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=D2khbv2S; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=AyEWV16d; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="D2khbv2S"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="AyEWV16d" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=XEWztHfKtcbLHVroyyT8qivNrqEtC8Rcli9fhqUjJo8=; b=D2khbv2SCtHQuqqvODxI0FmrjQ9kZMdesuPNMlZLI08a42MnRfRXo4he0W0OPzP9g9O+bp p77DID+R4rCC7r4L5Kj8ov3vIG8a/bXVLR2QlhlM+7I6vfctnYhNPm9YZ5iQ6PJbWRQmQK 00h6XeSKAX9ou5fDNG/Q6K46okEI0lQedLzDOhJdQNDVGV44nnT0tzvybcIAG/+rEubbsJ Z1RLZmpyrmUI4wGUixWR69Rjvl5gXg41BkUXGu0s+GkvapeCTNYasy70tuPzavdT8JbxoN 2w5fBZxZpyTe+o/+1WZOcuszGB+UjfFfu/RieCWi4CCoUGzjpCM9wsk0uHva0g== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909048; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=XEWztHfKtcbLHVroyyT8qivNrqEtC8Rcli9fhqUjJo8=; b=AyEWV16dNzrENhk1VdASSe81eqScliWmxW+TG0R7siCbzJTYgHRYsEvf+phrbmFAr5SPM4 dkNf7qqdLV8+HrAg== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 12/13] verification/rvgen: Remove the old state variables Date: Mon, 8 Jun 2026 10:57:08 +0200 Message-ID: In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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 --- 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/verificatio= n/rvgen/rvgen/automata.py index 4c302f5cba68..a3be327c2a73 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -411,8 +411,7 @@ class Automata: self.__dot_lines =3D self.__open_dot() self.__parse_tree =3D ParseTree(file_path) self.transitions =3D self.__parse_transitions() - self._states, self._initial_state, self._final_states =3D self.__p= arse_states() - self.states, self.initial_state, self.final_states =3D self.__get_= state_variables() + self.states, self.initial_state, self.final_states =3D self.__pars= e_states() self.env_types =3D {} self.env_stored =3D set() self.constraint_vars =3D set() @@ -603,7 +602,7 @@ class Automata: envs.append(c.env) self.__extract_env_var(c) =20 - for state in self._states: + for state in self.states: if state.inv: envs.append(state.inv.env) self.__extract_env_var(state.inv) @@ -639,7 +638,7 @@ class Automata: def __create_matrix(self) -> list[list[str]]: # transform the array into a dictionary events =3D self.events - states =3D [s.name for s in self._states] + states =3D [s.name for s in self.states] events_dict =3D {} states_dict =3D {} nr_event =3D 0 @@ -675,7 +674,7 @@ class Automata: for j in range(len(self.states)): if self.function[j][i] !=3D self.invalid_state_str: curr_event_used +=3D 1 - if self.function[j][i] =3D=3D self.initial_state: + if self.function[j][i] =3D=3D self.initial_state.name: curr_event_will_init +=3D 1 if self.function[0][i] !=3D self.invalid_state_str: curr_event_from_init =3D True diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/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): =20 def __get_enum_states_content(self) -> list[str]: buff =3D [] - 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 !=3D 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},") =20 return buff @@ -142,7 +142,7 @@ class Dot2c(Automata): def format_aut_init_states_string(self) -> list[str]: buff =3D [] buff.append("\t.state_names =3D {") - 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},") =20 return buff @@ -159,7 +159,7 @@ class Dot2c(Automata): return buff =20 def __get_max_strlen_of_states(self) -> int: - max_state_name =3D len(max(self.states, key=3Dlen)) + max_state_name =3D max((len(s.name) for s in self.states)) return max(max_state_name, len(self.invalid_state_str)) =20 def get_aut_init_function(self) -> str: @@ -199,7 +199,7 @@ class Dot2c(Automata): return buff =20 def get_aut_init_initial_state(self) -> str: - return self.initial_state + return self.initial_state.name =20 def format_aut_init_initial_state(self) -> list[str]: buff =3D [] diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index dc6d6f33729b..e4b6c7c09170 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 =3D self._read_template_file("trace_hybrid.h") self.has_invariant =3D False self.has_guard =3D False - for state in self._states: + for state in self.states: if state.inv: self.has_invariant =3D True for transition in self.transitions: @@ -314,7 +314,7 @@ f"""static inline bool ha_verify_invariants(struct ha_m= onitor *ha_mon, {{"""] =20 _else =3D "" - for state in self._states: + for state in self.states: if not state.inv: continue =20 @@ -382,7 +382,7 @@ f"""static inline void ha_setup_invariants(struct ha_mo= nitor *ha_mon, buff.append(f"\tif ({condition_str})\n\t\treturn;") =20 _else =3D "" - for state in self._states: + for state in self.states: inv =3D state.inv if not inv: continue @@ -391,7 +391,7 @@ f"""static inline void ha_setup_invariants(struct ha_mo= nitor *ha_mon, buff.append(f"\t\t{inv};") _else =3D "else " =20 - for state in self._states: + for state in self.states: inv =3D state.inv if not inv: continue --=20 2.47.3 From nobody Mon Jun 8 15:36:53 2026 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 762933B6360; Mon, 8 Jun 2026 08:57:32 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909054; cv=none; b=B8iwMthb77KvVVTeOvZyjP3SpOU+4YMSKXN/iiVRtuTBtHJw38q8P9k1/vO2IclXkN/QV0PcXwzHaGpC9WypwB50HFScrn1bgaYRJCcBpQdfu5YkpgUHQ8i/03La1UNcV0q1D27vxza9Q1yUI+3n75D6kUoELONXW7tpgli0zF4= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1780909054; c=relaxed/simple; bh=iHDbEV5tgOIJ+prrWKE06PpPskR06N/V/uw3z0vBMvQ=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=g+h9bGqmuS0j/xkgZINj9y9/d6lSZwPTQbCro8Fa8q/nOWhmTkgiISQ94Y8gOzl/gzi7XP0MWi9Bwqg57ChnkxAhnwJMzY82QFFP0vF+TA8c+YZtpz30v9J5d663kgQUj8ECky0QFRjmatYlBlx5pnPY1rEyJfCbyotw4HwAv7E= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=lN+Z6GEg; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=54F5qPTs; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="lN+Z6GEg"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="54F5qPTs" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1780909049; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=nvdb9GWfB/xMqK59RK6jWy5HMpwfMv+MHfy3F+lWCTc=; b=lN+Z6GEgqiW46xNDv28/8Z2Ts12zKdwsKfYccAWkVvlRUrvpC4EfozG6hgU9AlSCXKh0/N UQVSymMCH+hOPdtjLS8YFcBrYWcLYGmRSerA/VNlePJSrROqe1sc0z5wTmJnn6srYQEkG6 spAv/gr6IZ2hbQK8btWdmaU/kQRD/LbvFRuQLbBQ+e64ri+9XLf/2i2bziz/S92D3q7uB6 77FfowAbVTlbSRkBgDKZ3s0WgF9RY7UGLHq++GB72N6rVvzxvkbmKMTiCsR+lAyXB2wCS1 A9QMiWefz0ly7HeIi9Wt3+NtYkQULSMjopplgedzJ0UwXXZ7wW7vsQ/Zmm0EWw== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1780909049; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=nvdb9GWfB/xMqK59RK6jWy5HMpwfMv+MHfy3F+lWCTc=; b=54F5qPTsghEn91t/uj/O7ScIR+a7+0SK+HZLltzuJmFuUr6U+VuZo0Wt72d0l0j1TBEzur cjXZIg8WwJR7i+AA== To: Gabriele Monaco , Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Nam Cao Subject: [PATCH v3 13/13] verification/rvgen: Remove dead code Date: Mon, 8 Jun 2026 10:57:09 +0200 Message-ID: <0cecddde5da0f833871993c8089d0b3b79142229.1780908661.git.namcao@linutronix.de> In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" The conversion to use Lark left some dead code behind. Remove them. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- v3: delete unused import --- tools/verification/rvgen/rvgen/automata.py | 157 --------------------- tools/verification/rvgen/rvgen/dot2k.py | 29 +--- 2 files changed, 1 insertion(+), 185 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index a3be327c2a73..bfc997f630d7 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -9,9 +9,6 @@ # Documentation/trace/rv/deterministic_automata.rst =20 import ntpath -import re -from typing import Iterator -from itertools import islice =20 import lark =20 @@ -356,19 +353,6 @@ class State: self.name =3D name self.inv =3D inv =20 -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,eve= nt_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. =20 @@ -387,28 +371,10 @@ class Automata: =20 invalid_state_str =3D "INVALID_STATE" init_marker =3D "__init_" - node_marker =3D "{node" - # val can be numerical, uppercase (constant or macro), lowercase (para= meter or function) - # only numerical values should have units - constraint_rule =3D re.compile(r""" - ^ - (?P[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env v= ar - (?P[!<=3D>]{1,2}) # operator - (?P - [0-9]+ | # numerical value - [A-Z_]+\(\) | # macro - [A-Z_]+ | # constant - [a-z_]+\(\) | # function - [a-z_]+ # parameter - ) - (?P[a-z]{1,2})? # optional unit for numerical val= ues - """, re.VERBOSE) - constraint_reset =3D re.compile(r"^reset\((?P[a-zA-Z_][a-zA-Z0-9_= ]+)\)") =20 def __init__(self, file_path, model_name=3DNone): self.__dot_path =3D file_path self.name =3D model_name or self.__get_model_name() - self.__dot_lines =3D self.__open_dot() self.__parse_tree =3D ParseTree(file_path) self.transitions =3D self.__parse_transitions() self.states, self.initial_state, self.final_states =3D self.__pars= e_states() @@ -435,57 +401,6 @@ class Automata: =20 return model_name =20 - def __open_dot(self) -> list[str]: - dot_lines =3D [] - try: - with open(self.__dot_path) as dot_file: - dot_lines =3D 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 =3D dot_lines[0].split() - - if len(line) < 2 or line[0] !=3D "digraph" or line[1] !=3D "state_= automaton": - raise AutomataError(f"Not a valid .dot format: {self.__dot_pat= h}") - - return dot_lines - - def __get_cursor_begin_states(self) -> int: - for cursor, line in enumerate(self.__dot_lines): - split_line =3D line.split() - - if len(split_line) and split_line[0] =3D=3D self.node_marker: - return cursor - - raise AutomataError("Could not find a beginning state") - - def __get_cursor_begin_events(self) -> int: - state =3D 0 - cursor =3D 0 # make pyright happy - - for cursor, line in enumerate(self.__dot_lines): - line =3D line.split() - if not line: - continue - - if state =3D=3D 0: - if line[0] =3D=3D self.node_marker: - state =3D 1 - elif line[0] !=3D self.node_marker: - break - else: - raise AutomataError("Could not find beginning event") - - cursor +=3D 1 # skip initial state transition - if cursor =3D=3D len(self.__dot_lines): - raise AutomataError("Dot file ended after event beginning") - - return cursor - def __parse_transitions(self): transitions =3D [] =20 @@ -542,51 +457,6 @@ class Automata: states.insert(0, initial_state) return states, initial_state, final_states =20 - def __get_state_variables(self) -> tuple[list[str], str, list[str]]: - # wait for node declaration - states =3D [] - final_states =3D [] - initial_state =3D "" - - has_final_states =3D False - cursor =3D self.__get_cursor_begin_states() - - # process nodes - for line in islice(self.__dot_lines, cursor, None): - split_line =3D line.split() - if not split_line or split_line[0] !=3D self.node_marker: - break - - raw_state =3D split_line[-1] - - # "enabled_fired"}; -> enabled_fired - state =3D raw_state.replace('"', '').replace('};', '').replace= (',', '_') - if state.startswith(self.init_marker): - initial_state =3D state[len(self.init_marker):] - else: - states.append(state) - if "doublecircle" in line: - final_states.append(state) - has_final_states =3D True - - if "ellipse" in line: - final_states.append(state) - has_final_states =3D True - - if not initial_state: - raise AutomataError("The automaton doesn't have an initial sta= te") - - states =3D 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] =3D [] envs: list[str] =3D [] @@ -609,26 +479,6 @@ class Automata: =20 return sorted(set(events)), sorted(set(envs)) =20 - 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 =3D [] - seps =3D [] - for c in constr: - while "&&" in c or "||" in c: - a =3D c.find("&&") - o =3D c.find("||") - pos =3D a if o < 0 or 0 < a < o else o - exprs.append(c[:pos].replace(" ", "")) - seps.append(c[pos:pos + 2].replace(" ", "")) - c =3D 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] =3D constraint.unit @@ -697,10 +547,3 @@ class Automata: =20 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/r= vgen/rvgen/dot2k.py index e4b6c7c09170..a080b92334f9 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -8,12 +8,9 @@ # For further information, see: # Documentation/trace/rv/da_monitor_synthesis.rst =20 -from collections import deque from .dot2c import Dot2c from .generator import Monitor -from .automata import _EventConstraintKey, _StateConstraintKey, AutomataEr= ror -from .automata import ConstraintCondition - +from .automata import ConstraintCondition, AutomataError =20 class dot2k(Monitor, Dot2c): template_dir =3D "dot2k" @@ -217,9 +214,6 @@ class ha2k(dot2k): value *=3D 10**9 return str(value) + "ull" =20 - 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 =3D [] for c, sep in rule.rules: @@ -233,12 +227,6 @@ class ha2k(dot2k): buff.append(cond) return buff =20 - def __get_constraint_env(self, constr: str) -> str: - """Extract the second argument from an ha_ function""" - env =3D 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 =3D "ns" @@ -249,21 +237,6 @@ class ha2k(dot2k): =20 return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_= {self.name}, time_ns, {value})" =20 - 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 =3D "ns" - if self.env_types.get(rule["env"]) =3D=3D "j": - clock_type =3D "jiffy" - - return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.e= num_suffix}," - f" {value}, time_ns)") - def __parse_invariant(self, inv): # by default assume the timer has ns expiration clock_type =3D "ns" --=20 2.47.3