From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 92E8B305E10 for ; Mon, 23 Feb 2026 16:25:34 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863936; cv=none; b=UkL/kNQXbNZHY0bTteO4QcqL36SFPQPSct0tQT98f9moJkOfwnw5lQcRYyUkIdD58rjq3lpL2cyllh+XTRrSlID3vezvfsEjDRyWSNKjJ04+AlDxJSYVau9y7sYNT+evy1E2p6Jg5K7x4TGPwv5cRFo5/O9OX5cmMRnfqN+y7H0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863936; c=relaxed/simple; bh=Ju+HDZuzf2pq5QYcTVsR1EkKfnFFhNanEAoVUoMXt+o=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=jC+Xlmu5SXJQuUExCHpgNWrc0hgpfhUQg8c2m2SPb3ny+Ax4k8rkU49Q9zhvWT6cE+W8b/CsEJGkjW+idyeKLmSiC/PYbWAb61NZ1bV0ubK2sTmTg/5kCvzzbw0TDEsNLra6RgjPV02v5Q4/lVy48TDUQ0PsH6GZ9tXZYsPHNvg= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=a62CO/2I; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="a62CO/2I" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771863933; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=857XS0LLSd69kHZwdL6IntKG+3a4rRKFrejXsWKnDLM=; b=a62CO/2I4e0Tx3s7SDbSjOdOeuYuNwP3NNYsg9gD/2qZ8+0i4lDttn3ElANf7HTqZMNfPf vmzAd6qqsbOvID8ZOstxOKM+oh+g+OyJjzQ1m8Xd0Jzy7KZKb50OjXMFJJjMdZJQdCNfLN M6eFHw9UMlwXWs+VhDI+bReE+RIPX88= Received: from mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-280-SueilCcqPU2vZxWZNQgnBg-1; Mon, 23 Feb 2026 11:25:31 -0500 X-MC-Unique: SueilCcqPU2vZxWZNQgnBg-1 X-Mimecast-MFC-AGG-ID: SueilCcqPU2vZxWZNQgnBg_1771863930 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 626E218002C4; Mon, 23 Feb 2026 16:25:30 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 3E6641800370; Mon, 23 Feb 2026 16:25:27 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 01/19] rv/rvgen: introduce AutomataError exception class Date: Mon, 23 Feb 2026 13:17:44 -0300 Message-ID: <20260223162407.147003-2-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Replace the generic except Exception block with a custom AutomataError class that inherits from Exception. This provides more precise exception handling for automata parsing and validation errors while avoiding overly broad exception catches that could mask programming errors like SyntaxError or TypeError. The AutomataError class is raised when DOT file processing fails due to invalid format, I/O errors, or malformed automaton definitions. The main entry point catches this specific exception and provides a user-friendly error message to stderr before exiting. Also, replace generic exceptions raising in HA and LTL with AutomataError. Co-authored-by: Gabriele Monaco Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/__main__.py | 6 ++--- tools/verification/rvgen/rvgen/automata.py | 17 ++++++++++---- tools/verification/rvgen/rvgen/dot2c.py | 4 ++-- tools/verification/rvgen/rvgen/dot2k.py | 26 ++++++++++----------- tools/verification/rvgen/rvgen/generator.py | 7 ++---- tools/verification/rvgen/rvgen/ltl2ba.py | 9 +++---- tools/verification/rvgen/rvgen/ltl2k.py | 8 +++++-- 7 files changed, 43 insertions(+), 34 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 9a5a9f08eae21..5a3f090ac3316 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -13,6 +13,7 @@ if __name__ =3D=3D '__main__': from rvgen.generator import Monitor from rvgen.container import Container from rvgen.ltl2k import ltl2k + from rvgen.automata import AutomataError import argparse import sys =20 @@ -55,9 +56,8 @@ if __name__ =3D=3D '__main__': sys.exit(1) else: monitor =3D Container(vars(params)) - except Exception as e: - print('Error: '+ str(e)) - print("Sorry : :-(") + except AutomataError as e: + print(f"There was an error processing {params.spec}: {e}", file=3D= sys.stderr) sys.exit(1) =20 print("Writing the monitor into the directory %s" % monitor.name) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 5c1c5597d839f..9cc452305a2aa 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -25,6 +25,13 @@ class _EventConstraintKey(_ConstraintKey, tuple): def __new__(cls, state_id: int, event_id: int): return super().__new__(cls, (state_id, event_id)) =20 +class AutomataError(Exception): + """Exception raised for errors in automata parsing and validation. + + Raised when DOT file processing fails due to invalid format, I/O error= s, + or malformed automaton definitions. + """ + class Automata: """Automata class: Reads a dot file and part it as an automata. =20 @@ -72,11 +79,11 @@ class Automata: basename =3D ntpath.basename(self.__dot_path) if not basename.endswith(".dot") and not basename.endswith(".gv"): print("not a dot file") - raise Exception("not a dot file: %s" % self.__dot_path) + raise AutomataError("not a dot file: %s" % self.__dot_path) =20 model_name =3D ntpath.splitext(basename)[0] if model_name.__len__() =3D=3D 0: - raise Exception("not a dot file: %s" % self.__dot_path) + raise AutomataError("not a dot file: %s" % self.__dot_path) =20 return model_name =20 @@ -85,8 +92,8 @@ class Automata: dot_lines =3D [] try: dot_file =3D open(self.__dot_path) - except: - raise Exception("Cannot open the file: %s" % self.__dot_path) + except OSError as exc: + raise AutomataError(exc.strerror) from exc =20 dot_lines =3D dot_file.read().splitlines() dot_file.close() @@ -95,7 +102,7 @@ class Automata: line =3D dot_lines[cursor].split() =20 if (line[0] !=3D "digraph") and (line[1] !=3D "state_automaton"): - raise Exception("Not a valid .dot format: %s" % self.__dot_pat= h) + raise AutomataError("Not a valid .dot format: %s" % self.__dot= _path) else: cursor +=3D 1 return dot_lines diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index f779d9528af3f..6878cc79e6f70 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -13,7 +13,7 @@ # For further information, see: # Documentation/trace/rv/deterministic_automata.rst =20 -from .automata import Automata +from .automata import Automata, AutomataError =20 class Dot2c(Automata): enum_suffix =3D "" @@ -103,7 +103,7 @@ class Dot2c(Automata): min_type =3D "unsigned int" =20 if self.states.__len__() > 1000000: - raise Exception("Too many states: %d" % self.states.__len__()) + raise AutomataError("Too many states: %d" % self.states.__len_= _()) =20 return min_type =20 diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index e7ba68a54c1f8..55222e38323f5 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -11,7 +11,7 @@ from collections import deque from .dot2c import Dot2c from .generator import Monitor -from .automata import _EventConstraintKey, _StateConstraintKey +from .automata import _EventConstraintKey, _StateConstraintKey, AutomataEr= ror =20 =20 class dot2k(Monitor, Dot2c): @@ -166,14 +166,14 @@ class da2k(dot2k): def __init__(self, *args, **kwargs): super().__init__(*args, **kwargs) if self.is_hybrid_automata(): - raise ValueError("Detected hybrid automata, use the 'ha' class= ") + raise AutomataError("Detected hybrid automata, use the 'ha' cl= ass") =20 class ha2k(dot2k): """Hybrid automata only""" def __init__(self, *args, **kwargs): super().__init__(*args, **kwargs) if not self.is_hybrid_automata(): - raise ValueError("Detected deterministic automata, use the 'da= ' class") + raise AutomataError("Detected deterministic automata, use the = 'da' class") self.trace_h =3D self._read_template_file("trace_hybrid.h") self.__parse_constraints() =20 @@ -266,22 +266,22 @@ class ha2k(dot2k): # state constraints are only used for expirations (e.g. clk None: self.guards: dict[_EventConstraintKey, str] =3D {} diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 5eac12e110dce..571093a92bdc8 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -51,10 +51,7 @@ class RVGenerator: raise FileNotFoundError("Could not find the rv directory, do you h= ave the kernel source installed?") =20 def _read_file(self, path): - try: - fd =3D open(path, 'r') - except OSError: - raise Exception("Cannot open the file: %s" % path) + fd =3D open(path, 'r') =20 content =3D fd.read() =20 @@ -65,7 +62,7 @@ class RVGenerator: try: path =3D os.path.join(self.abs_template_dir, file) return self._read_file(path) - except Exception: + except OSError: # Specific template file not found. Try the generic template f= ile in the template/ # directory, which is one level up path =3D os.path.join(self.abs_template_dir, "..", file) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/= rvgen/rvgen/ltl2ba.py index f14e6760ac3db..f9855dfa3bc1c 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -9,6 +9,7 @@ =20 from ply.lex import lex from ply.yacc import yacc +from .automata import AutomataError =20 # Grammar: # ltl ::=3D opd | ( ltl ) | ltl binop ltl | unop ltl @@ -62,7 +63,7 @@ t_ignore_COMMENT =3D r'\#.*' t_ignore =3D ' \t\n' =20 def t_error(t): - raise ValueError(f"Illegal character '{t.value[0]}'") + raise AutomataError(f"Illegal character '{t.value[0]}'") =20 lexer =3D lex() =20 @@ -487,7 +488,7 @@ def p_unop(p): elif p[1] =3D=3D "not": op =3D NotOp(p[2]) else: - raise ValueError(f"Invalid unary operator {p[1]}") + raise AutomataError(f"Invalid unary operator {p[1]}") =20 p[0] =3D ASTNode(op) =20 @@ -507,7 +508,7 @@ def p_binop(p): elif p[2] =3D=3D "imply": op =3D ImplyOp(p[1], p[3]) else: - raise ValueError(f"Invalid binary operator {p[2]}") + raise AutomataError(f"Invalid binary operator {p[2]}") =20 p[0] =3D ASTNode(op) =20 @@ -526,7 +527,7 @@ def parse_ltl(s: str) -> ASTNode: subexpr[assign[0]] =3D assign[1] =20 if rule is None: - raise ValueError("Please define your specification in the \"RULE = =3D \" format") + raise AutomataError("Please define your specification in the \"RUL= E =3D \" format") =20 for node in rule: if not isinstance(node.op, Variable): diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index b075f98d50c47..08ad245462e7d 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -4,6 +4,7 @@ from pathlib import Path from . import generator from . import ltl2ba +from .automata import AutomataError =20 COLUMN_LIMIT =3D 100 =20 @@ -60,8 +61,11 @@ class ltl2k(generator.Monitor): if MonitorType !=3D "per_task": raise NotImplementedError("Only per_task monitor is supported = for LTL") super().__init__(extra_params) - with open(file_path) as f: - self.atoms, self.ba, self.ltl =3D ltl2ba.create_graph(f.read()) + try: + with open(file_path) as f: + self.atoms, self.ba, self.ltl =3D ltl2ba.create_graph(f.re= ad()) + except OSError as exc: + raise AutomataError(exc.strerror) from exc self.atoms_abbr =3D abbreviate_atoms(self.atoms) self.name =3D extra_params.get("model_name") if not self.name: --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 D994630F946 for ; Mon, 23 Feb 2026 16:25:54 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863957; cv=none; b=qRsqj4S5mK3dWNqrYirXxLYjU0mTs+Haj1tp2uINEgEjGB/s48sDkapj9szI5AnUCPkvajZKgqtaiMv9f71oZUdXX9AuN6SYAWYTSNuJ9y9eDTgGix9m7HNJo7GMVR1sB7yMlGgjOiCqtGPQT5fVVjMAN8hIBPLrLz0A+/Pyx7M= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863957; c=relaxed/simple; bh=ktZs/oReU8TuKEe4kJTZBKFlXLAtDnmWnm7XzJL2g8Q=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=t9i/hvcpvSFp7ItXhbbEXcWAqZtn2QFQKo8mAiNDqlhH4PV5gk4+XYjlBkuRA+b7dl6xEfgQVMaAXXFnC3G2Ym9LAb6y/lBJgACthiWu9mUvUjqEFZUSJ8Reeg3zAEbIJq5eapNyUtMZpagz3b3CWZ4xqxVl1Cj41YHeIhnbNe4= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=ISg3KYWt; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="ISg3KYWt" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771863953; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=ZhMtnK5rUYRMnC5b1qkWK5XScEQOjsKc5cOJAnZqE9U=; b=ISg3KYWthIeynOGaK1n64Qm8HNK64XlsScB6mOIc+R9DAS8rn/H/b+v8Mpi+L3x2dpNxA6 dKeMiKDA2mj6U6SUcaRoctny1cWy33lwFTQQSs7s00bPcjg53ysoZa5ylIwNp2oniZlU2/ amf2s7buBYNt6NiwGzm9ysLK4EX7HUQ= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-201-UP2JIAwvP2O6dMN-9VRiiA-1; Mon, 23 Feb 2026 11:25:51 -0500 X-MC-Unique: UP2JIAwvP2O6dMN-9VRiiA-1 X-Mimecast-MFC-AGG-ID: UP2JIAwvP2O6dMN-9VRiiA_1771863950 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 730881956052; Mon, 23 Feb 2026 16:25:50 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 4E5BC180066A; Mon, 23 Feb 2026 16:25:48 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 02/19] rv/rvgen: remove bare except clauses in generator Date: Mon, 23 Feb 2026 13:17:45 -0300 Message-ID: <20260223162407.147003-3-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Remove bare except clauses from the generator module that were catching all exceptions including KeyboardInterrupt and SystemExit. This follows the same exception handling improvements made in the previous AutomataError commit and addresses PEP 8 violations. The bare except clause in __create_directory was silently catching and ignoring all errors after printing a message, which could mask serious issues. For __write_file, the bare except created a critical bug where the file variable could remain undefined if open() failed, causing a NameError when attempting to write to or close the file. These methods now let OSError propagate naturally, allowing callers to handle file system errors appropriately. This provides clearer error reporting and allows Python's exception handling to show complete stack traces with proper error types and locations. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/generator.py | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 571093a92bdc8..a2391a4c21ed6 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -198,17 +198,10 @@ obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o os.mkdir(path) except FileExistsError: return - except: - print("Fail creating the output dir: %s" % self.name) =20 def __write_file(self, file_name, content): - try: - file =3D open(file_name, 'w') - except: - print("Fail writing to file: %s" % file_name) - + file =3D open(file_name, 'w') file.write(content) - file.close() =20 def _create_file(self, file_name, content): --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 E153A1FBCA7 for ; Mon, 23 Feb 2026 16:26:15 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863978; cv=none; b=jL3IjPIhzmCn8SEZcJs/3Gk57pm5mV5EJcPbMTSD9iCj89yVApuaPQzbEydRyF8BGHXhHWriY8aNa1Fz2sQikVnCzJJJIHvQTlVGzqThGrZ3oQmVgp3UpCVPkm+NsgStG5/mlx+Z0+aa9iXmIS0GyTUfMssr1IP+E/Bc3zyPRco= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771863978; c=relaxed/simple; bh=AeamI9E2tWqooFuBj/eFM/AN3ChY90D2IXEHO3s/788=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=MtM8kOKssSECcR4jI2CH2POq+aHdqS7eQWMoL7yadYPOXVZ7RNRFMk+g+rlhx51KUtq94cKCzw2tXjka+Hw+B3AN+3nhiWYjM173xwJ6NoaTPaP7VxTRqIuD3owSYaL3LE5tuIqyx0afUJ0bqwO5V6rrg070NxZ4Fve7zWzenCA= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=ZmWq0pol; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="ZmWq0pol" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771863974; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=EV32T6SowwYbAi8UylMNYhXx7ZcN4OrwsdxuP4kDb/I=; b=ZmWq0pol2hv0tGzy2nxdanvo0j/0s0joe1G7dM3VECaO7gxMusegGJFYYv1jR1QkBJ1/V/ 9sNddUyo8byjf3mNajmEFdY1BeoiR8tYXvFLpYAqSw8+stLwcs/CUntd5uKx/BMwToEEmb wgzN6ZIrGEkmJw+D9I6U9paNTm0w6hs= Received: from mx-prod-mc-01.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-63-FQYrYd6OO7if3N0S7ecgHQ-1; Mon, 23 Feb 2026 11:26:12 -0500 X-MC-Unique: FQYrYd6OO7if3N0S7ecgHQ-1 X-Mimecast-MFC-AGG-ID: FQYrYd6OO7if3N0S7ecgHQ_1771863971 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-01.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id DE6571956056; Mon, 23 Feb 2026 16:26:10 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 88F3E1800677; Mon, 23 Feb 2026 16:26:08 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 03/19] rv/rvgen: replace % string formatting with f-strings Date: Mon, 23 Feb 2026 13:17:46 -0300 Message-ID: <20260223162407.147003-4-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Replace all instances of percent-style string formatting with f-strings across the rvgen codebase. This modernizes the string formatting to use Python 3.6+ features, providing clearer and more maintainable code while improving runtime performance. The conversion handles all formatting cases including simple variable substitution, multi-variable formatting, and complex format specifiers. Dynamic width formatting is converted from "%*s" to "{var:>{width}}" using proper alignment syntax. Template strings for generated C code properly escape braces using double-brace syntax to produce literal braces in the output. F-strings provide approximately 2x performance improvement over percent formatting and are the recommended approach in modern Python. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/__main__.py | 6 +-- tools/verification/rvgen/rvgen/automata.py | 6 +-- tools/verification/rvgen/rvgen/dot2c.py | 38 ++++++------- tools/verification/rvgen/rvgen/dot2k.py | 29 +++++----- tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++----------- tools/verification/rvgen/rvgen/ltl2k.py | 30 +++++------ 6 files changed, 83 insertions(+), 85 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 5a3f090ac3316..2e5b868535470 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -44,7 +44,7 @@ if __name__ =3D=3D '__main__': =20 try: if params.subcmd =3D=3D "monitor": - print("Opening and parsing the specification file %s" % params= .spec) + print(f"Opening and parsing the specification file {params.spe= c}") if params.monitor_class =3D=3D "da": monitor =3D da2k(params.spec, params.monitor_type, vars(pa= rams)) elif params.monitor_class =3D=3D "ha": @@ -60,11 +60,11 @@ if __name__ =3D=3D '__main__': print(f"There was an error processing {params.spec}: {e}", file=3D= sys.stderr) sys.exit(1) =20 - print("Writing the monitor into the directory %s" % monitor.name) + print(f"Writing the monitor into the directory {monitor.name}") monitor.print_files() print("Almost done, checklist") if params.subcmd =3D=3D "monitor": - print(" - Edit the %s/%s.c to add the instrumentation" % (monitor= .name, monitor.name)) + print(f" - Edit the {monitor.name}/{monitor.name}.c to add the in= strumentation") print(monitor.fill_tracepoint_tooltip()) print(monitor.fill_makefile_tooltip()) print(monitor.fill_kconfig_tooltip()) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 9cc452305a2aa..4fed58cfa3c6e 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -79,11 +79,11 @@ class Automata: basename =3D ntpath.basename(self.__dot_path) if not basename.endswith(".dot") and not basename.endswith(".gv"): print("not a dot file") - raise AutomataError("not a dot file: %s" % self.__dot_path) + raise AutomataError(f"not a dot file: {self.__dot_path}") =20 model_name =3D ntpath.splitext(basename)[0] if model_name.__len__() =3D=3D 0: - raise AutomataError("not a dot file: %s" % self.__dot_path) + raise AutomataError(f"not a dot file: {self.__dot_path}") =20 return model_name =20 @@ -102,7 +102,7 @@ class Automata: line =3D dot_lines[cursor].split() =20 if (line[0] !=3D "digraph") and (line[1] !=3D "state_automaton"): - raise AutomataError("Not a valid .dot format: %s" % self.__dot= _path) + raise AutomataError(f"Not a valid .dot format: {self.__dot_pat= h}") else: cursor +=3D 1 return dot_lines diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index 6878cc79e6f70..e6a440e1588cd 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -29,17 +29,17 @@ class Dot2c(Automata): =20 def __get_enum_states_content(self) -> list[str]: buff =3D [] - buff.append("\t%s%s," % (self.initial_state, self.enum_suffix)) + buff.append(f"\t{self.initial_state}{self.enum_suffix},") for state in self.states: if state !=3D self.initial_state: - buff.append("\t%s%s," % (state, self.enum_suffix)) - buff.append("\tstate_max%s," % (self.enum_suffix)) + buff.append(f"\t{state}{self.enum_suffix},") + buff.append(f"\tstate_max{self.enum_suffix},") =20 return buff =20 def format_states_enum(self) -> list[str]: buff =3D [] - buff.append("enum %s {" % self.enum_states_def) + buff.append(f"enum {self.enum_states_def} {{") buff +=3D self.__get_enum_states_content() buff.append("};\n") =20 @@ -48,15 +48,15 @@ class Dot2c(Automata): def __get_enum_events_content(self) -> list[str]: buff =3D [] for event in self.events: - buff.append("\t%s%s," % (event, self.enum_suffix)) + buff.append(f"\t{event}{self.enum_suffix},") =20 - buff.append("\tevent_max%s," % self.enum_suffix) + buff.append(f"\tevent_max{self.enum_suffix},") =20 return buff =20 def format_events_enum(self) -> list[str]: buff =3D [] - buff.append("enum %s {" % self.enum_events_def) + buff.append(f"enum {self.enum_events_def} {{") buff +=3D self.__get_enum_events_content() buff.append("};\n") =20 @@ -103,27 +103,27 @@ class Dot2c(Automata): min_type =3D "unsigned int" =20 if self.states.__len__() > 1000000: - raise AutomataError("Too many states: %d" % self.states.__len_= _()) + raise AutomataError(f"Too many states: {self.states.__len__()}= ") =20 return min_type =20 def format_automaton_definition(self) -> list[str]: min_type =3D self.get_minimun_type() buff =3D [] - buff.append("struct %s {" % self.struct_automaton_def) - buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffi= x)) - buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffi= x)) + buff.append(f"struct {self.struct_automaton_def} {{") + buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];") + buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];") if self.is_hybrid_automata(): buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];") - buff.append("\t%s function[state_max%s][event_max%s];" % (min_type= , self.enum_suffix, self.enum_suffix)) - buff.append("\t%s initial_state;" % min_type) - buff.append("\tbool final_states[state_max%s];" % (self.enum_suffi= x)) + buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][e= vent_max{self.enum_suffix}];") + buff.append(f"\t{min_type} initial_state;") + buff.append(f"\tbool final_states[state_max{self.enum_suffix}];") buff.append("};\n") return buff =20 def format_aut_init_header(self) -> list[str]: buff =3D [] - buff.append("static const struct %s %s =3D {" % (self.struct_autom= aton_def, self.var_automaton_def)) + buff.append(f"static const struct {self.struct_automaton_def} {sel= f.var_automaton_def} =3D {{") return buff =20 def __get_string_vector_per_line_content(self, entries: list[str]) -> = str: @@ -179,9 +179,9 @@ class Dot2c(Automata): next_state =3D self.function[x][y] + self.enum_suffix =20 if linetoolong: - line +=3D "\t\t\t%s" % next_state + line +=3D f"\t\t\t{next_state}" else: - line +=3D "%*s" % (maxlen, next_state) + line +=3D f"{next_state:>{maxlen}}" if y !=3D nr_events-1: line +=3D ",\n" if linetoolong else ", " else: @@ -225,7 +225,7 @@ class Dot2c(Automata): =20 def format_aut_init_final_states(self) -> list[str]: buff =3D [] - buff.append("\t.final_states =3D { %s }," % self.get_aut_init_final= _states()) + buff.append(f"\t.final_states =3D {{ {self.get_aut_init_final_state= s()} }},") =20 return buff =20 @@ -241,7 +241,7 @@ class Dot2c(Automata): =20 def format_invalid_state(self) -> list[str]: buff =3D [] - buff.append("#define %s state_max%s\n" % (self.invalid_state_str, = self.enum_suffix)) + buff.append(f"#define {self.invalid_state_str} state_max{self.enum= _suffix}\n") =20 return buff =20 diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index 55222e38323f5..e26f2b47390ab 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -21,7 +21,8 @@ class dot2k(Monitor, Dot2c): self.monitor_type =3D MonitorType Monitor.__init__(self, extra_params) Dot2c.__init__(self, file_path, extra_params.get("model_name")) - self.enum_suffix =3D "_%s" % self.name + self.enum_suffix =3D f"_{self.name}" + self.enum_suffix =3D f"_{self.name}" self.monitor_class =3D extra_params["monitor_class"] =20 def fill_monitor_type(self) -> str: @@ -35,7 +36,7 @@ class dot2k(Monitor, Dot2c): buff =3D [] buff +=3D self._fill_hybrid_definitions() for event in self.events: - buff.append("static void handle_%s(void *data, /* XXX: fill he= ader */)" % event) + buff.append(f"static void handle_{event}(void *data, /* XXX: f= ill header */)") buff.append("{") handle =3D "handle_event" if self.is_start_event(event): @@ -46,13 +47,13 @@ class dot2k(Monitor, Dot2c): handle =3D "handle_start_run_event" if self.monitor_type =3D=3D "per_task": buff.append("\tstruct task_struct *p =3D /* XXX: how do I = get p? */;"); - buff.append("\tda_%s(p, %s%s);" % (handle, event, self.enu= m_suffix)); + buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});= "); elif self.monitor_type =3D=3D "per_obj": buff.append("\tint id =3D /* XXX: how do I get the id? */;= ") buff.append("\tmonitor_target t =3D /* XXX: how do I get t= ? */;") buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffi= x});") else: - buff.append("\tda_%s(%s%s);" % (handle, event, self.enum_s= uffix)); + buff.append(f"\tda_{handle}({event}{self.enum_suffix});"); buff.append("}") buff.append("") return '\n'.join(buff) @@ -60,25 +61,25 @@ class dot2k(Monitor, Dot2c): def fill_tracepoint_attach_probe(self) -> str: buff =3D [] for event in self.events: - buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoin= t */, handle_%s);" % (self.name, event)) + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX:= tracepoint */, handle_{event});") return '\n'.join(buff) =20 def fill_tracepoint_detach_helper(self) -> str: buff =3D [] for event in self.events: - buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoin= t */, handle_%s);" % (self.name, event)) + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX:= tracepoint */, handle_{event});") return '\n'.join(buff) =20 def fill_model_h_header(self) -> list[str]: buff =3D [] buff.append("/* SPDX-License-Identifier: GPL-2.0 */") buff.append("/*") - buff.append(" * Automatically generated C representation of %s aut= omaton" % (self.name)) + buff.append(f" * Automatically generated C representation of {self= .name} automaton") buff.append(" * For further information about this format, see ker= nel documentation:") buff.append(" * Documentation/trace/rv/deterministic_automata.rs= t") buff.append(" */") buff.append("") - buff.append("#define MONITOR_NAME %s" % (self.name)) + buff.append(f"#define MONITOR_NAME {self.name}") buff.append("") =20 return buff @@ -87,11 +88,11 @@ class dot2k(Monitor, Dot2c): # # Adjust the definition names # - self.enum_states_def =3D "states_%s" % self.name - self.enum_events_def =3D "events_%s" % self.name + self.enum_states_def =3D f"states_{self.name}" + self.enum_events_def =3D f"events_{self.name}" self.enum_envs_def =3D f"envs_{self.name}" - self.struct_automaton_def =3D "automaton_%s" % self.name - self.var_automaton_def =3D "automaton_%s" % self.name + self.struct_automaton_def =3D f"automaton_{self.name}" + self.var_automaton_def =3D f"automaton_{self.name}" =20 buff =3D self.fill_model_h_header() buff +=3D self.format_model() @@ -135,8 +136,8 @@ class dot2k(Monitor, Dot2c): tp_args.insert(0, tp_args_id) tp_proto_c =3D ", ".join([a+b for a,b in tp_args]) tp_args_c =3D ", ".join([b for a,b in tp_args]) - buff.append(" TP_PROTO(%s)," % tp_proto_c) - buff.append(" TP_ARGS(%s)" % tp_args_c) + buff.append(f" TP_PROTO({tp_proto_c}),") + buff.append(f" TP_ARGS({tp_args_c})") return '\n'.join(buff) =20 def _fill_hybrid_definitions(self) -> list: diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index a2391a4c21ed6..61174b139123b 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -40,7 +40,7 @@ class RVGenerator: if platform.system() !=3D "Linux": raise OSError("I can only run on Linux.") =20 - kernel_path =3D os.path.join("/lib/modules/%s/build" % platform.re= lease(), self.rv_dir) + kernel_path =3D os.path.join(f"/lib/modules/{platform.release()}/b= uild", self.rv_dir) =20 # if the current kernel is from a distro this may not be a full ke= rnel tree # verify that one of the files we are going to modify is available @@ -69,11 +69,11 @@ class RVGenerator: return self._read_file(path) =20 def fill_parent(self): - return "&rv_%s" % self.parent if self.parent else "NULL" + return f"&rv_{self.parent}" if self.parent else "NULL" =20 def fill_include_parent(self): if self.parent: - return "#include \n" % (self.parent, self.pa= rent) + return f"#include \n" return "" =20 def fill_tracepoint_handlers_skel(self): @@ -119,7 +119,7 @@ class RVGenerator: buff =3D [] buff.append(" # XXX: add dependencies if there") if self.parent: - buff.append(" depends on RV_MON_%s" % self.parent.upper()) + buff.append(f" depends on RV_MON_{self.parent.upper()}") buff.append(" default y") return '\n'.join(buff) =20 @@ -145,31 +145,30 @@ class RVGenerator: monitor_class_type =3D self.fill_monitor_class_type() if self.auto_patch: self._patch_file("rv_trace.h", - "// Add new monitors based on CONFIG_%s here" = % monitor_class_type, - "#include " % (self.na= me, self.name)) - return " - Patching %s/rv_trace.h, double check the result" %= self.rv_dir + f"// Add new monitors based on CONFIG_{monitor= _class_type} here", + f"#include ") + return f" - Patching {self.rv_dir}/rv_trace.h, double check t= he result" =20 - return """ - Edit %s/rv_trace.h: -Add this line where other tracepoints are included and %s is defined: -#include -""" % (self.rv_dir, monitor_class_type, self.name, self.name) + return f""" - Edit {self.rv_dir}/rv_trace.h: +Add this line where other tracepoints are included and {monitor_class_type= } is defined: +#include +""" =20 def _kconfig_marker(self, container=3DNone) -> str: - return "# Add new %smonitors here" % (container + " " - if container else "") + return f"# Add new {container + ' ' if container else ''}monitors = here" =20 def fill_kconfig_tooltip(self): if self.auto_patch: # monitors with a container should stay together in the Kconfig self._patch_file("Kconfig", self._kconfig_marker(self.parent), - "source \"kernel/trace/rv/monitors/%s/Kconfig\= "" % (self.name)) - return " - Patching %s/Kconfig, double check the result" % se= lf.rv_dir + f"source \"kernel/trace/rv/monitors/{self.name= }/Kconfig\"") + return f" - Patching {self.rv_dir}/Kconfig, double check the = result" =20 - return """ - Edit %s/Kconfig: + return f""" - Edit {self.rv_dir}/Kconfig: Add this line where other monitors are included: -source \"kernel/trace/rv/monitors/%s/Kconfig\" -""" % (self.rv_dir, self.name) +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\" +""" =20 def fill_makefile_tooltip(self): name =3D self.name @@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\" if self.auto_patch: self._patch_file("Makefile", "# Add new monitors here", - "obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o= " % (name_up, name, name)) - return " - Patching %s/Makefile, double check the result" % s= elf.rv_dir + f"obj-$(CONFIG_RV_MON_{name_up}) +=3D monitors= /{name}/{name}.o") + return f" - Patching {self.rv_dir}/Makefile, double check the= result" =20 - return """ - Edit %s/Makefile: + return f""" - Edit {self.rv_dir}/Makefile: Add this line where other monitors are included: -obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o -""" % (self.rv_dir, name_up, name, name) +obj-$(CONFIG_RV_MON_{name_up}) +=3D monitors/{name}/{name}.o +""" =20 def fill_monitor_tooltip(self): if self.auto_patch: - return " - Monitor created in %s/monitors/%s" % (self.rv_dir,= self. name) - return " - Move %s/ to the kernel's monitor directory (%s/monitor= s)" % (self.name, self.rv_dir) + return f" - Monitor created in {self.rv_dir}/monitors/{self.n= ame}" + return f" - Move {self.name}/ to the kernel's monitor directory (= {self.rv_dir}/monitors)" =20 def __create_directory(self): path =3D self.name @@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o file.close() =20 def _create_file(self, file_name, content): - path =3D "%s/%s" % (self.name, file_name) + path =3D f"{self.name}/{file_name}" if self.auto_patch: path =3D os.path.join(self.rv_dir, "monitors", path) self.__write_file(path, content) =20 def __get_main_name(self): - path =3D "%s/%s" % (self.name, "main.c") + path =3D f"{self.name}/main.c" if not os.path.exists(path): return "main.c" return "__main.c" @@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o =20 self.__create_directory() =20 - path =3D "%s.c" % self.name + path =3D f"{self.name}.c" self._create_file(path, main_c) =20 model_h =3D self.fill_model_h() - path =3D "%s.h" % self.name + path =3D f"{self.name}.h" self._create_file(path, model_h) =20 kconfig =3D self.fill_kconfig() @@ -258,5 +257,5 @@ class Monitor(RVGenerator): def print_files(self): super().print_files() trace_h =3D self.fill_trace_h() - path =3D "%s_trace.h" % self.name + path =3D f"{self.name}_trace.h" self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index 08ad245462e7d..b6300c38154dc 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -77,7 +77,7 @@ class ltl2k(generator.Monitor): ] =20 for node in self.ba: - buf.append("\tS%i," % node.id) + buf.append(f"\tS{node.id},") buf.append("\tRV_NUM_BA_STATES") buf.append("};") buf.append("static_assert(RV_NUM_BA_STATES <=3D RV_MAX_BA_STATES);= ") @@ -86,7 +86,7 @@ class ltl2k(generator.Monitor): def _fill_atoms(self): buf =3D ["enum ltl_atom {"] for a in sorted(self.atoms): - buf.append("\tLTL_%s," % a) + buf.append(f"\tLTL_{a},") buf.append("\tLTL_NUM_ATOM") buf.append("};") buf.append("static_assert(LTL_NUM_ATOM <=3D RV_MAX_LTL_ATOM);") @@ -100,7 +100,7 @@ class ltl2k(generator.Monitor): ] =20 for name in self.atoms_abbr: - buf.append("\t\t\"%s\"," % name) + buf.append(f"\t\t\"{name}\",") =20 buf.extend([ "\t};", @@ -117,19 +117,19 @@ class ltl2k(generator.Monitor): continue =20 if isinstance(node.op, ltl2ba.AndOp): - buf.append("\tbool %s =3D %s && %s;" % (node, node.op.left= , node.op.right)) + buf.append(f"\tbool {node} =3D {node.op.left} && {node.op.= right};") required_values |=3D {str(node.op.left), str(node.op.right= )} elif isinstance(node.op, ltl2ba.OrOp): - buf.append("\tbool %s =3D %s || %s;" % (node, node.op.left= , node.op.right)) + buf.append(f"\tbool {node} =3D {node.op.left} || {node.op.= right};") required_values |=3D {str(node.op.left), str(node.op.right= )} elif isinstance(node.op, ltl2ba.NotOp): - buf.append("\tbool %s =3D !%s;" % (node, node.op.child)) + buf.append(f"\tbool {node} =3D !{node.op.child};") required_values.add(str(node.op.child)) =20 for atom in self.atoms: if atom.lower() not in required_values: continue - buf.append("\tbool %s =3D test_bit(LTL_%s, mon->atoms);" % (at= om.lower(), atom)) + buf.append(f"\tbool {atom.lower()} =3D test_bit(LTL_{atom}, mo= n->atoms);") =20 buf.reverse() =20 @@ -157,7 +157,7 @@ class ltl2k(generator.Monitor): ]) =20 for node in self.ba: - buf.append("\tcase S%i:" % node.id) + buf.append(f"\tcase S{node.id}:") =20 for o in sorted(node.outgoing): line =3D "\t\tif " @@ -167,7 +167,7 @@ class ltl2k(generator.Monitor): lines =3D break_long_line(line, indent) buf.extend(lines) =20 - buf.append("\t\t\t__set_bit(S%i, next);" % o.id) + buf.append(f"\t\t\t__set_bit(S{o.id}, next);") buf.append("\t\tbreak;") buf.extend([ "\t}", @@ -201,7 +201,7 @@ class ltl2k(generator.Monitor): lines =3D break_long_line(line, indent) buf.extend(lines) =20 - buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) + buf.append(f"\t\t__set_bit(S{node.id}, mon->states);") buf.append("}") return buf =20 @@ -209,23 +209,21 @@ class ltl2k(generator.Monitor): buff =3D [] buff.append("static void handle_example_event(void *data, /* XXX: = fill header */)") buff.append("{") - buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.= atoms[0]) + buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/fa= lse);") buff.append("}") buff.append("") return '\n'.join(buff) =20 def fill_tracepoint_attach_probe(self): - return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, han= dle_example_event);" \ - % self.name + return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoi= nt */, handle_example_event);" =20 def fill_tracepoint_detach_helper(self): - return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, han= dle_sample_event);" \ - % self.name + return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoi= nt */, handle_sample_event);" =20 def fill_atoms_init(self): buff =3D [] for a in self.atoms: - buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a) + buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);") return '\n'.join(buff) =20 def fill_model_h(self): --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 35EFA30F92D for ; Mon, 23 Feb 2026 16:26:38 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864000; cv=none; b=EFGW8BhYk8MHF0vXE06ieZLZV8SRpSIuQqTtBk83YfNj7ZISLSTJ7FFQ1L9lCjNUhxSsMTRBzSddnIptktsxg0iAjruI6vE8TtRrtoSPYbX1IiXZSkWyIN9SxRbJIZ7KPVPtHqRWKwfRuDHRlwtffpJoAfZ3pk/2mes0Y1TaQos= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864000; c=relaxed/simple; bh=DFgFqsuoyMh37BT1ZXCagkOYOZ/F0IAgde64JQKp6TI=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=aMqeecaHCNf8morfxWRbf+rVvkD3OZhEWJ4OegDZ71vpGPydWEQGuyeejZAUbbcMmecSBooNNtj+S+8OQvkk0KckIUwMiJNaE7U7bSMtpm4sCMm+A/8bGyWG8cOpb0Nd+wZeXjoOkwMwXSFxhHXn0+Cpvafgq3yuNNh2W1NyfJw= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=bpe2Bhj7; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="bpe2Bhj7" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771863998; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=o88xK5pKfHpNkibMTGO9a/VFXbqGwcnPn0WqRMK1hGY=; b=bpe2Bhj7+KPLPqfcyKlSkqnwQILnkt2kh1ng67TrW0ETw1yntgenQIp0IvIyQDxbMHnjBc UsA6VdAD5t/CGrHaqVJz1cj/v7EqftTVQKgnG32udqVQfiS/d9xlPYTfqxs2Gxo7vaIn4x L9v/TO9WqZzZ+yeaZUZDoHbDzvDTDzY= Received: from mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-479-ksNtpQg1PqmHonqpRyxbfQ-1; Mon, 23 Feb 2026 11:26:32 -0500 X-MC-Unique: ksNtpQg1PqmHonqpRyxbfQ-1 X-Mimecast-MFC-AGG-ID: ksNtpQg1PqmHonqpRyxbfQ_1771863991 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 0FC8C1800615; Mon, 23 Feb 2026 16:26:31 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id E04321800370; Mon, 23 Feb 2026 16:26:28 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 04/19] rv/rvgen: replace __len__() calls with len() Date: Mon, 23 Feb 2026 13:17:47 -0300 Message-ID: <20260223162407.147003-5-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Replace all direct calls to the __len__() dunder method with the idiomatic len() built-in function across the rvgen codebase. This change eliminates a Python anti-pattern where dunder methods are called directly instead of using their corresponding built-in functions. The changes affect nine instances across two files. In automata.py, the empty string check is further improved by using truthiness testing instead of explicit length comparison. In dot2c.py, all length checks in the get_minimun_type, __get_max_strlen_of_states, and get_aut_init_function methods now use the standard len() function. Additionally, spacing around keyword arguments has been corrected to follow PEP 8 guidelines. Direct calls to dunder methods like __len__() are discouraged in Python because they bypass the language's abstraction layer and reduce code readability. Using len() provides the same functionality while adhering to Python community standards and making the code more familiar to Python developers. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao --- tools/verification/rvgen/rvgen/automata.py | 2 +- tools/verification/rvgen/rvgen/dot2c.py | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 4fed58cfa3c6e..4f5681265ee24 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -82,7 +82,7 @@ class Automata: raise AutomataError(f"not a dot file: {self.__dot_path}") =20 model_name =3D ntpath.splitext(basename)[0] - if model_name.__len__() =3D=3D 0: + if not model_name: raise AutomataError(f"not a dot file: {self.__dot_path}") =20 return model_name diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index e6a440e1588cd..fa44795adef46 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -96,14 +96,14 @@ class Dot2c(Automata): def get_minimun_type(self) -> str: min_type =3D "unsigned char" =20 - if self.states.__len__() > 255: + if len(self.states) > 255: min_type =3D "unsigned short" =20 - if self.states.__len__() > 65535: + if len(self.states) > 65535: min_type =3D "unsigned int" =20 - if self.states.__len__() > 1000000: - raise AutomataError(f"Too many states: {self.states.__len__()}= ") + if len(self.states) > 1000000: + raise AutomataError(f"Too many states: {len(self.states)}") =20 return min_type =20 @@ -159,12 +159,12 @@ class Dot2c(Automata): return buff =20 def __get_max_strlen_of_states(self) -> int: - max_state_name =3D max(self.states, key =3D len).__len__() - return max(max_state_name, self.invalid_state_str.__len__()) + max_state_name =3D len(max(self.states, key=3Dlen)) + return max(max_state_name, len(self.invalid_state_str)) =20 def get_aut_init_function(self) -> str: - nr_states =3D self.states.__len__() - nr_events =3D self.events.__len__() + nr_states =3D len(self.states) + nr_events =3D len(self.events) buff =3D [] =20 maxlen =3D self.__get_max_strlen_of_states() + len(self.enum_suffi= x) --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 16F233101B1 for ; Mon, 23 Feb 2026 16:26:56 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864018; cv=none; b=E2DKr8r/ZfusORAPjSQXhJeZEvM+ciLo0G1nXPDR4nX4bxw7KxInAGd4wfJuWC4HnNcrLyfyuFuYUSjTmyuSeZEMa3AG74E8Moj+AidfM6ULdsmhw9lMiBZejZ06Vf/nuReuCdsK70KPd/8jMoCo3ER5clVroPXXmaNp9P01vaI= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864018; c=relaxed/simple; bh=QL2ejv2+3YvAWL5CSkNwYRn11wU4PTBvlTsWRS+pJ9w=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=gHKPepbTYFE7TAhvAEDUOAFvu6jIHRR0sUiTOvBJUw8oPBDfUHogGcUfE67zICBTndxZtlSHMGJZoLpccDEocxfl6/9IFJEHfrarTDNLUkfA1USWcu86PUgr8CywlbKAqC4+LVWXyycPMPjo3TwC6IIOfxZseG2L1HfOxzDdDMw= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=jDn1ajD/; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="jDn1ajD/" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864016; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=toYc/KytBJDS3v29J7Ao5zr1crGTZ/8ZX2w/8ex74No=; b=jDn1ajD//CMzXGCgy6XSg+oaXUZI465/hqE8C/xhJlOwtKs8YtQJo0WW4DlTToT08NroTa AhiovKrtmXRTQILz5Wj6qq5QEMxgDKic7Do4G9jcocZu7Qmclrjmj1xTenotlO6m4iqum6 bmx6e1E/rOUjpm0OV2Rsqmr8cUmxkwk= Received: from mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-133-ciXsZJhrOki_xPsqwN-fCA-1; Mon, 23 Feb 2026 11:26:52 -0500 X-MC-Unique: ciXsZJhrOki_xPsqwN-fCA-1 X-Mimecast-MFC-AGG-ID: ciXsZJhrOki_xPsqwN-fCA_1771864011 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id D59C218003F5; Mon, 23 Feb 2026 16:26:50 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id B9BC01800669; Mon, 23 Feb 2026 16:26:48 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 05/19] rv/rvgen: remove unnecessary semicolons Date: Mon, 23 Feb 2026 13:17:48 -0300 Message-ID: <20260223162407.147003-6-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Remove unnecessary semicolons from Python code in the rvgen tool. Python does not require semicolons to terminate statements, and their presence goes against PEP 8 style guidelines. These semicolons were likely added out of habit from C-style languages. This cleanup improves consistency with Python coding standards and aligns with the recent improvements to remove other Python anti-patterns from the codebase. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/dot2k.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index e26f2b47390ab..47af9f104a829 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -46,14 +46,14 @@ class dot2k(Monitor, Dot2c): buff.append("\t/* XXX: validate that this event is only va= lid in the initial state */") handle =3D "handle_start_run_event" if self.monitor_type =3D=3D "per_task": - buff.append("\tstruct task_struct *p =3D /* XXX: how do I = get p? */;"); - buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});= "); + buff.append("\tstruct task_struct *p =3D /* XXX: how do I = get p? */;") + buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});= ") elif self.monitor_type =3D=3D "per_obj": buff.append("\tint id =3D /* XXX: how do I get the id? */;= ") buff.append("\tmonitor_target t =3D /* XXX: how do I get t= ? */;") buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffi= x});") else: - buff.append(f"\tda_{handle}({event}{self.enum_suffix});"); + buff.append(f"\tda_{handle}({event}{self.enum_suffix});") buff.append("}") buff.append("") return '\n'.join(buff) --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 307E230FC2E for ; Mon, 23 Feb 2026 16:27:17 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864038; cv=none; b=pteSPEvYrNn/VF22ROgW/ki1u+UlE0le+G8mbdgGUhu86/tb+HcBndy0HpFccCjYf1egQIoc4GCEfHi9Y1RXxHcY1Y/kAI49uvUY4VsUVBh5w6aEaqb/bWZKC4LSrv6HCxOzXMXyjDyBIqQzDSuHNR9YrbYSmiUVzXW1EEcx/zc= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864038; c=relaxed/simple; bh=J3sPcfz4gojiOiJFFuYU+FJssFjLUIPfHpd24s+ff1M=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=Iz1tPO/5CPKMITNp6Jo7xtKwovr2E5nPUYK+ucrprP7GhJX0BxQfrgLq0le8cC7u6cR9pg4+LjiVjC3X1OLbzyxavm+d/FnW+x+FzCzoQbzVG4AWungSYcpr23/qoD0JYObjt2wt4fn/JuL7fFnca/ArJV3a+/BtLrYjy0uV3zo= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=gBzR5USS; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="gBzR5USS" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864036; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=s+Yn0zt6+sQ5OLXpiasx6aOYEpSEow6FT6ozp6AHGpg=; b=gBzR5USSGXFOlFKMY9T0zak8OTW5TpABGOlx4P6O44Lqyehr+BmvAXa3CXqGHCHHz7Ybuw pBDk9xbGSJaJUjrI5Gp9zlY2nIdfsT4ixjyGt6Dj6SsfxorSl/sw83qTZ/eiiOPNQN5eyP 7mUyp6J+CSvK8oLwynmcaAUMP+SRfaw= Received: from mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-494-s-AJGslQOEOtd2vOdbjEPQ-1; Mon, 23 Feb 2026 11:27:12 -0500 X-MC-Unique: s-AJGslQOEOtd2vOdbjEPQ-1 X-Mimecast-MFC-AGG-ID: s-AJGslQOEOtd2vOdbjEPQ_1771864031 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id D2D8219560A2; Mon, 23 Feb 2026 16:27:10 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id B9DCF180066A; Mon, 23 Feb 2026 16:27:08 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 06/19] rv/rvgen: use context managers for file operations Date: Mon, 23 Feb 2026 13:17:49 -0300 Message-ID: <20260223162407.147003-7-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Replace manual file open and close operations with context managers throughout the rvgen codebase. The previous implementation used explicit open() and close() calls, which could lead to resource leaks if exceptions occurred between opening and closing the file handles. This change affects three file operations: reading DOT specification files in the automata parser, reading template files in the generator base class, and writing generated monitor files. All now use the with statement to ensure proper resource cleanup even in error conditions. Context managers provide automatic cleanup through the with statement, which guarantees that file handles are closed when the with block exits regardless of whether an exception occurred. This follows PEP 343 recommendations and is the standard Python idiom for resource management. The change also reduces code verbosity while improving safety and maintainability. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 6 ++---- tools/verification/rvgen/rvgen/generator.py | 12 ++++-------- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 4f5681265ee24..10146b6061ed2 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -91,13 +91,11 @@ class Automata: cursor =3D 0 dot_lines =3D [] try: - dot_file =3D open(self.__dot_path) + with open(self.__dot_path) as dot_file: + dot_lines =3D dot_file.read().splitlines() except OSError as exc: raise AutomataError(exc.strerror) from exc =20 - dot_lines =3D dot_file.read().splitlines() - dot_file.close() - # checking the first line: line =3D dot_lines[cursor].split() =20 diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 61174b139123b..d932e96dd66d3 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -51,11 +51,8 @@ class RVGenerator: raise FileNotFoundError("Could not find the rv directory, do you h= ave the kernel source installed?") =20 def _read_file(self, path): - fd =3D open(path, 'r') - - content =3D fd.read() - - fd.close() + with open(path, 'r') as fd: + content =3D fd.read() return content =20 def _read_template_file(self, file): @@ -199,9 +196,8 @@ obj-$(CONFIG_RV_MON_{name_up}) +=3D monitors/{name}/{na= me}.o return =20 def __write_file(self, file_name, content): - file =3D open(file_name, 'w') - file.write(content) - file.close() + with open(file_name, 'w') as file: + file.write(content) =20 def _create_file(self, file_name, content): path =3D f"{self.name}/{file_name}" --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 1C8E431196C for ; Mon, 23 Feb 2026 16:27:33 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864055; cv=none; b=g/YpVLwc3KCsFyAbRZRh3Z+YzExl2mK6E3h0XGN7fEFv/alKkqccwDOAYIi4/EctqLG4ZDEOoupV6vGMD24iATtWayyVpOeXUJ88sr3xG+A41f0SdT4f0uOVsZQnp9M5IIj7GQKlTc6QrCdmclcuulatTevficU1sdGEEAWKgSE= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864055; c=relaxed/simple; bh=ntVk9vb5+bDGwMQjVfmIDX4VnU7IlD06N2nv4VO11SI=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=TZFEgcv30ij37zuIY7dht71S/kQFyuN4TMLmF8XFHIP5FnskXKKqaBov3oV0Qr6MuSNGjHpOT9DEeAtCq4WUQW/5EdwoX2cQBgxMpGAlB6S6zN422rGneUisrl2JCe5SvAU3tcEb8KtcYLzlDS36VFu7PwbU7NpFR0d4JsoWktk= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=SWRAZiCg; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="SWRAZiCg" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864053; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=sEf5cNZX+eiFDwZbI3I2oBbq99wA4y6PNvMILeXGY0M=; b=SWRAZiCgtE0VCzHxuvIGVUCCVN6CDj89Kjn8w/vsOxTH3kqo0psezejuE0rhZjs4D1DEKm 81XOPesgxDTlk9owxL3scJrRCTm+7QlOCYGn5ZPBAL5Cg4hY36kd3u5dAMEqjl+x6j59+L hl1hgNqxIV582hUrWR3G8bCQ5uBrd1s= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-381-0UdJbZN1MOChyKC2RyFpUg-1; Mon, 23 Feb 2026 11:27:31 -0500 X-MC-Unique: 0UdJbZN1MOChyKC2RyFpUg-1 X-Mimecast-MFC-AGG-ID: 0UdJbZN1MOChyKC2RyFpUg_1771864050 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id B84331955F38; Mon, 23 Feb 2026 16:27:30 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 9EFDB1800669; Mon, 23 Feb 2026 16:27:28 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 07/19] rv/rvgen: fix typos in automata and generator docstring and comments Date: Mon, 23 Feb 2026 13:17:50 -0300 Message-ID: <20260223162407.147003-8-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Fix two typos in the Automata class documentation that have been present since the initial implementation. Fix the class docstring: "part it" instead of "parses it". Additionally, a comment describing transition labels contained the misspelling "lables" instead of "labels". Fix a typo in the comment describing the insertion of the initial state into the states list: "bein og" should be "beginning of". Fix typo in the module docstring: "Abtract" should be "Abstract". Fix several occurrences of "automata" where it should be the singular form "automaton". Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 8 ++++---- tools/verification/rvgen/rvgen/dot2c.py | 2 +- tools/verification/rvgen/rvgen/dot2k.py | 4 ++-- tools/verification/rvgen/rvgen/generator.py | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 10146b6061ed2..b25378e92b16d 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -3,7 +3,7 @@ # # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira # -# Automata object: parse an automata in dot file digraph format into a pyt= hon object +# Automata class: parse an automaton in dot file digraph format into a pyt= hon object # # For further information, see: # Documentation/trace/rv/deterministic_automata.rst @@ -33,7 +33,7 @@ class AutomataError(Exception): """ =20 class Automata: - """Automata class: Reads a dot file and part it as an automata. + """Automata class: Reads a dot file and parses it as an automaton. =20 It supports both deterministic and hybrid automata. =20 @@ -153,7 +153,7 @@ class Automata: states =3D sorted(set(states)) states.remove(initial_state) =20 - # Insert the initial state at the bein og the states + # Insert the initial state at the beginning of the states states.insert(0, initial_state) =20 if not has_final_states: @@ -175,7 +175,7 @@ class Automata: line =3D self.__dot_lines[cursor].split() event =3D "".join(line[line.index("label") + 2:-1]).replac= e('"', '') =20 - # when a transition has more than one lables, they are lik= e this + # when a transition has more than one labels, they are lik= e this # "local_irq_enable\nhw_local_irq_enable_n" # so split them. =20 diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index fa44795adef46..9255cc2153a31 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -3,7 +3,7 @@ # # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira # -# dot2c: parse an automata in dot file digraph format into a C +# dot2c: parse an automaton in dot file digraph format into a C # # This program was written in the development of this paper: # de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index 47af9f104a829..aedc2a7799b32 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -167,14 +167,14 @@ class da2k(dot2k): def __init__(self, *args, **kwargs): super().__init__(*args, **kwargs) if self.is_hybrid_automata(): - raise AutomataError("Detected hybrid automata, use the 'ha' cl= ass") + raise AutomataError("Detected hybrid automaton, use the 'ha' c= lass") =20 class ha2k(dot2k): """Hybrid automata only""" def __init__(self, *args, **kwargs): super().__init__(*args, **kwargs) if not self.is_hybrid_automata(): - raise AutomataError("Detected deterministic automata, use the = 'da' class") + raise AutomataError("Detected deterministic automaton, use the= 'da' class") self.trace_h =3D self._read_template_file("trace_hybrid.h") self.__parse_constraints() =20 diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index d932e96dd66d3..988ccdc27fa37 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -3,7 +3,7 @@ # # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira # -# Abtract class for generating kernel runtime verification monitors from s= pecification file +# Abstract class for generating kernel runtime verification monitors from = specification file =20 import platform import os --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 CA3C2310779 for ; Mon, 23 Feb 2026 16:27:53 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864075; cv=none; b=DmTPoIg+eaT8CzBQD3+pkqaCBMt575a0RSd51qo80fh/84gOUPc7e9dnlVZbYy+fQrmUNuZdQJsHXznRBT8x9ehDiEIeoRZ7LSVrVgxnukPUlHlV7wX9okE35mu+uS6pQfY6jHIOZ3Wu8iQDTDJc8hmizJntIYBCUzUGE3siQi8= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864075; c=relaxed/simple; bh=tkQIqMDRYo46V5iDA5bMpwWOaTpjQP2z8Khn96PUVPc=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=jsl8ViEfJRoVAd+h3Xc745FCJEZGuus8xVEhGqelbfkx1+zSiaj5XAl5mW+f8IlRLgiW1reaKJCgrmQjep56aXZFCmrCU6+UVIkT8IAtOLkWJmP1PMuwB6vIWTd+BuJzWf1mOU3mAlr0ta7WvTP2aybeVHOKibMenIYgPCvMXic= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=ZtzZ+fjy; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="ZtzZ+fjy" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864072; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=SrUFZV6oLK679oGJODiDwGHpUK22sR45oyIvkICSS4c=; b=ZtzZ+fjyKOsxxOyZ4uxuk+LAkFM5+fyw+220KBkFEr/gqi5xH+VicDRagFnsVaa4S60tck RcfFiIoTQfEN1CBW8pTusrf4ttA8TDo6GAz2AoCC4tgY2Lvp6vE7r+BThcc4V11A44tsfC Y0aMq++pwGhEDbDbbpqhTC0GecPrVPU= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-711-TPzP1EzVN16W_juiwlUrgA-1; Mon, 23 Feb 2026 11:27:51 -0500 X-MC-Unique: TPzP1EzVN16W_juiwlUrgA-1 X-Mimecast-MFC-AGG-ID: TPzP1EzVN16W_juiwlUrgA_1771864070 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 7B53719560B7; Mon, 23 Feb 2026 16:27:50 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 61B631800370; Mon, 23 Feb 2026 16:27:48 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 08/19] rv/rvgen: fix PEP 8 whitespace violations Date: Mon, 23 Feb 2026 13:17:51 -0300 Message-ID: <20260223162407.147003-9-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Fix whitespace violations throughout the rvgen codebase to comply with PEP 8 style guidelines. The changes address missing whitespace after commas, around operators, and in collection literals that were flagged by pycodestyle. The fixes include adding whitespace after commas in string replace chains and function arguments, adding whitespace around arithmetic operators, removing extra whitespace in list comprehensions, and fixing dictionary literal spacing. These changes improve code readability and consistency with Python coding standards. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao --- tools/verification/rvgen/rvgen/automata.py | 8 ++++---- tools/verification/rvgen/rvgen/dot2c.py | 2 +- tools/verification/rvgen/rvgen/dot2k.py | 4 ++-- tools/verification/rvgen/rvgen/generator.py | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index b25378e92b16d..e54486c69a191 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -135,7 +135,7 @@ class Automata: raw_state =3D line[-1] =20 # "enabled_fired"}; -> enabled_fired - state =3D raw_state.replace('"', '').replace('};', '').replace= (',','_') + state =3D raw_state.replace('"', '').replace('};', '').replace= (',', '_') if state[0:7] =3D=3D "__init_": initial_state =3D state[7:] else: @@ -264,7 +264,7 @@ class Automata: nr_state +=3D 1 =20 # declare the matrix.... - matrix =3D [[ self.invalid_state_str for x in range(nr_event)] for= y in range(nr_state)] + matrix =3D [[self.invalid_state_str for x in range(nr_event)] for = y in range(nr_state)] constraints: dict[_ConstraintKey, list[str]] =3D {} =20 # and we are back! Let's fill the matrix @@ -273,8 +273,8 @@ class Automata: while self.__dot_lines[cursor].lstrip()[0] =3D=3D '"': if self.__dot_lines[cursor].split()[1] =3D=3D "->": line =3D self.__dot_lines[cursor].split() - origin_state =3D line[0].replace('"','').replace(',','_') - dest_state =3D line[2].replace('"','').replace(',','_') + origin_state =3D line[0].replace('"', '').replace(',', '_') + dest_state =3D line[2].replace('"', '').replace(',', '_') possible_events =3D "".join(line[line.index("label") + 2:-= 1]).replace('"', '') for event in possible_events.split("\\n"): event, *constr =3D event.split(";") diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index 9255cc2153a31..fc85ba1f649e7 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -182,7 +182,7 @@ class Dot2c(Automata): line +=3D f"\t\t\t{next_state}" else: line +=3D f"{next_state:>{maxlen}}" - if y !=3D nr_events-1: + if y !=3D nr_events - 1: line +=3D ",\n" if linetoolong else ", " else: line +=3D ",\n\t\t}," if linetoolong else " }," diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index aedc2a7799b32..e6f476b903b0a 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -134,8 +134,8 @@ class dot2k(Monitor, Dot2c): tp_args =3D tp_args_dict[tp_type] if self._is_id_monitor(): tp_args.insert(0, tp_args_id) - tp_proto_c =3D ", ".join([a+b for a,b in tp_args]) - tp_args_c =3D ", ".join([b for a,b in tp_args]) + tp_proto_c =3D ", ".join([a + b for a, b in tp_args]) + tp_args_c =3D ", ".join([b for a, b in tp_args]) buff.append(f" TP_PROTO({tp_proto_c}),") buff.append(f" TP_ARGS({tp_args_c})") return '\n'.join(buff) diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 988ccdc27fa37..40d82afb018f5 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -228,7 +228,7 @@ obj-$(CONFIG_RV_MON_{name_up}) +=3D monitors/{name}/{na= me}.o =20 =20 class Monitor(RVGenerator): - monitor_types =3D { "global" : 1, "per_cpu" : 2, "per_task" : 3, "per_= obj" : 4 } + monitor_types =3D {"global": 1, "per_cpu": 2, "per_task": 3, "per_obj"= : 4} =20 def __init__(self, extra_params=3D{}): super().__init__(extra_params) --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 236813101B9 for ; Mon, 23 Feb 2026 16:28:16 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864100; cv=none; b=CInmiRJfCuahOb7Jb36oeei0x8OfRTotacf8GI2waeROwKhyQbSgq+63rvFADk3nqnq16r4leTKzkKeA7z5qzbxWmCAF14lXwOtywSLpMG20tzfZ7kRpheDcfbn1UmWBuEMxyteN+2mhCSJI3Y3YiHT1hWCfbDN9eGR1//Dphiw= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864100; c=relaxed/simple; bh=CQ8+qfz2sCZDuJ/AwN5KOiHhqxqCx7uNoqRGLi3yT0E=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=SUH1Ymhtu57nQ069tbaeSTwLb59a5y0S617o5cBCsis9gkZ68XddiameZ9cMJq40veyFsaHSJVLOoR8v+HCWSFUqr2i7bVy8kyDFTqwC9UWODzgoD5iDanBPMXPUHeBqqG57pc1XblgGvmXRSTYntSuHDkwMzu/upwluIiMPf2A= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=fvtmYW1N; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="fvtmYW1N" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864096; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=9MpwDsN2zeO6ezJv8SGR7mHck7dW4y6GEUXw6asn0Ng=; b=fvtmYW1NQ9LH7PjJn1z0IqhUiwhjWO86/8MrWSips9dMzR44SGcq34DkdLdgMFv/GJ5Hzy leNfYOmTL2Waw21t2c8pLBMwpWMLiJqtlrlE/aQw1ljrqOEU3W3m2gZPyLUXirC2cgJ4Kq qZx7Bd/RckJsfQ8oJgkh8RQqCvJyhBo= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-313-T-KqSGAfNE6aN4wdMYNzDA-1; Mon, 23 Feb 2026 11:28:11 -0500 X-MC-Unique: T-KqSGAfNE6aN4wdMYNzDA-1 X-Mimecast-MFC-AGG-ID: T-KqSGAfNE6aN4wdMYNzDA_1771864090 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 75402195605A; Mon, 23 Feb 2026 16:28:10 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 3186D1800370; Mon, 23 Feb 2026 16:28:07 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 09/19] rv/rvgen: fix DOT file validation logic error Date: Mon, 23 Feb 2026 13:17:52 -0300 Message-ID: <20260223162407.147003-10-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Fix incorrect boolean logic in automata DOT file format validation that allowed malformed files to pass undetected. The previous implementation used a logical AND operator where OR was required, causing the validation to only reject files when both the first token was not "digraph" AND the second token was not "state_automaton". This meant a file starting with "digraph" but having an incorrect second token would incorrectly pass validation. The corrected logic properly rejects DOT files where either the first token is not "digraph" or the second token is not "state_automaton", ensuring that only properly formatted automaton definition files are accepted for processing. Without this fix, invalid DOT files could cause downstream parsing failures or generate incorrect C code for runtime verification monitors. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index e54486c69a191..e4c0335cd0fba 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -99,7 +99,7 @@ class Automata: # checking the first line: line =3D dot_lines[cursor].split() =20 - if (line[0] !=3D "digraph") and (line[1] !=3D "state_automaton"): + if (line[0] !=3D "digraph") or (line[1] !=3D "state_automaton"): raise AutomataError(f"Not a valid .dot format: {self.__dot_pat= h}") else: cursor +=3D 1 --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 2D23D30F52C for ; Mon, 23 Feb 2026 16:28:37 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864118; cv=none; b=ldCvnPKjNplePqaKtD5uPF9VYBomONsaw1Ym2rRJzqWlUdheqGjarjeFmUjfEvtaLq+kUFivR45aZnGvUe2vWYXFuWpgKi5yBearIQuXpp+Jjdm+kpIZBJvyBWNHRoNh6ZZC9oh8+lWjdlRhOhd1WntXiyUvJ9OVY1eZlAJMz7g= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864118; c=relaxed/simple; bh=+Rz5Al002Pg+QmwS3Sgv5FtNfWEPgkOkRu97wAzbifQ=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=p1UcNC3SkISH/Fz4OT/+QGNDIhQOk1X/8tvGaaB9zWG0Yb+SMqk+SMCTV77R77eME7vaDRk42geamkkqPooBItRewqGqQsAA/zfC4VpJqsEZ5af0Zw0pjT0PXxM08FltC4py6A68/X9hhtArxsWlN60DPKk8FiaI2CXlhjF68ns= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=gIGc3CCI; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="gIGc3CCI" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864116; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=+PHQlGbsOT9oGTPjaz6e2nYz9/uHpMjqGVB/iTMTzY8=; b=gIGc3CCIE9dNq0a5Dreksb4fbBm+iOTzIp7KrbIXuuQytaPMZpB3Acr9MnSMWU9sf1FSs/ pFcycNFRNiiy/7lsptPZ0tFBHIjPnXMObwaOrfjtRhHqTcwlBWY5pwhZzFaUjeM0xjB0Dv jY9ncdrNCSELRAYK3RA+BsRwkrTfZV8= Received: from mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-152-3wuLTW5IOUGL3GxnuySftA-1; Mon, 23 Feb 2026 11:28:31 -0500 X-MC-Unique: 3wuLTW5IOUGL3GxnuySftA-1 X-Mimecast-MFC-AGG-ID: 3wuLTW5IOUGL3GxnuySftA_1771864110 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 4A4A918005AD; Mon, 23 Feb 2026 16:28:30 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 2FF0F1800669; Mon, 23 Feb 2026 16:28:27 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 10/19] rv/rvgen: use class constant for init marker Date: Mon, 23 Feb 2026 13:17:53 -0300 Message-ID: <20260223162407.147003-11-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Replace hardcoded string literal and magic number with a class constant for the initial state marker in DOT file parsing. The previous implementation used the magic string "__init_" directly in the code along with a hardcoded length of 7 for substring extraction, which made the code less maintainable and harder to understand. This change introduces a class constant init_marker to serve as a single source of truth for the initial state prefix. The code now uses startswith() for clearer intent and calculates the substring position dynamically using len(), eliminating the magic number. If the marker value needs to change in the future, only the constant definition requires updating rather than multiple locations in the code. The refactoring improves code readability and maintainability while preserving the exact same runtime behavior. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao --- tools/verification/rvgen/rvgen/automata.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index e4c0335cd0fba..cdec78a4bbbae 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -42,6 +42,7 @@ class Automata: """ =20 invalid_state_str =3D "INVALID_STATE" + init_marker =3D "__init_" # 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""" @@ -136,8 +137,8 @@ class Automata: =20 # "enabled_fired"}; -> enabled_fired state =3D raw_state.replace('"', '').replace('};', '').replace= (',', '_') - if state[0:7] =3D=3D "__init_": - initial_state =3D state[7:] + if state.startswith(self.init_marker): + initial_state =3D state[len(self.init_marker):] else: states.append(state) if "doublecircle" in self.__dot_lines[cursor]: --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 C8F8030F924 for ; Mon, 23 Feb 2026 16:28:57 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864139; cv=none; b=cMUL+NVf20mXgPx03MzF9kPsZLxHDrGHEp19MYBukaWSF0lfhjzynKZvJce1WX2pmBCcfByiLMeukSCPhruwlYpKBJg1wOVM5AYl922vOXs0hzSrPGJ7diuflgRlJGvnmCn+wNkUWH8xy5PXOeO/wqfYfh79Lfyf1t8sGurXn4s= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864139; c=relaxed/simple; bh=vEkF9WavzD5KqlmPKhm2df4adhITkvjyI+DumhCrwss=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=s1O9ZyejJtrzexj9IbzQTXeQFUQvk4wk6s8xqrvdxL8uG38UXfEZb8V88iG4ivwUZ/2wqbvpvuy3hOQGO0OI2C8kmlzRz8CVWYgZBBzXXoMdIJM1QA2bTXabmcWFhmIE2BLPGeCJkhCnd3jg9vRwyqgdzKQ5gM6HvDUU1Zb5JlU= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=c9K9nsNr; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="c9K9nsNr" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864137; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=4+pkJNQaowjoHPGEYfVu6sri2iWmaCVQLnXkzvb9518=; b=c9K9nsNrsQPk9DubynVWMn+GsIpw7KxnR6oJkHYMvcQ1hDrl4Cl6KS895bt1jwK573joxx zFIrmo5iU9/xWRXsuyW3OHWwOzF15ETuzMgMfywabSP2RBMwciD41jw8X+E7BFs5QfjnF7 AB+5GZi0rdW63mTmEhU5FTIZDsgfUbc= Received: from mx-prod-mc-01.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-88-0uvrOOW0OEyzp89ypLiAlg-1; Mon, 23 Feb 2026 11:28:51 -0500 X-MC-Unique: 0uvrOOW0OEyzp89ypLiAlg-1 X-Mimecast-MFC-AGG-ID: 0uvrOOW0OEyzp89ypLiAlg_1771864130 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-01.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 31A221956067; Mon, 23 Feb 2026 16:28:50 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 062CE1800674; Mon, 23 Feb 2026 16:28:47 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 11/19] rv/rvgen: refactor automata.py to use iterator-based parsing Date: Mon, 23 Feb 2026 13:17:54 -0300 Message-ID: <20260223162407.147003-12-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Refactor the DOT file parsing logic in automata.py to use Python's iterator-based patterns instead of manual cursor indexing. The previous implementation relied on while loops with explicit cursor management, which made the code prone to off-by-one errors and would crash on malformed input files containing empty lines. The new implementation uses enumerate and itertools.islice to iterate over lines, eliminating manual cursor tracking. Functions that search for specific markers now use for loops with early returns and explicit AutomataError exceptions for missing markers, rather than assuming the markers exist. Additional bounds checking ensures that split line arrays have sufficient elements before accessing specific indices, preventing IndexError exceptions on malformed DOT files. The matrix creation and event variable extraction methods now use functional patterns with map combined with itertools.islice, making the intent clearer while maintaining the same behavior. Minor improvements include using extend instead of append in a loop, adding empty file validation, and replacing enumerate with range where the enumerated value was unused. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 116 +++++++++++++-------- 1 file changed, 71 insertions(+), 45 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index cdec78a4bbbae..6613a9d6159a9 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -11,6 +11,7 @@ import ntpath import re from typing import Iterator +from itertools import islice =20 class _ConstraintKey: """Base class for constraint keys.""" @@ -89,37 +90,54 @@ class Automata: return model_name =20 def __open_dot(self) -> list[str]: - cursor =3D 0 dot_lines =3D [] try: with open(self.__dot_path) as dot_file: - dot_lines =3D dot_file.read().splitlines() + dot_lines =3D dot_file.readlines() except OSError as exc: raise AutomataError(exc.strerror) from exc =20 + if not dot_lines: + raise AutomataError(f"{self.__dot_path} is empty") + # checking the first line: - line =3D dot_lines[cursor].split() + line =3D dot_lines[0].split() =20 - if (line[0] !=3D "digraph") or (line[1] !=3D "state_automaton"): + 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}") - else: - cursor +=3D 1 + return dot_lines =20 def __get_cursor_begin_states(self) -> int: - cursor =3D 0 - while self.__dot_lines[cursor].split()[0] !=3D "{node": - cursor +=3D 1 - return cursor + for cursor, line in enumerate(self.__dot_lines): + split_line =3D line.split() + + if len(split_line) and split_line[0] =3D=3D "{node": + return cursor + + raise AutomataError("Could not find a beginning state") =20 def __get_cursor_begin_events(self) -> int: - cursor =3D 0 - while self.__dot_lines[cursor].split()[0] !=3D "{node": - cursor +=3D 1 - while self.__dot_lines[cursor].split()[0] =3D=3D "{node": - cursor +=3D 1 - # skip initial state transition - cursor +=3D 1 + 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 "{node": + state =3D 1 + elif line[0] !=3D "{node": + 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 =20 def __get_state_variables(self) -> tuple[list[str], str, list[str]]: @@ -131,9 +149,12 @@ class Automata: cursor =3D self.__get_cursor_begin_states() =20 # process nodes - while self.__dot_lines[cursor].split()[0] =3D=3D "{node": - line =3D self.__dot_lines[cursor].split() - raw_state =3D line[-1] + for line in islice(self.__dot_lines, cursor, None): + split_line =3D line.split() + if not split_line or split_line[0] !=3D "{node": + break + + raw_state =3D split_line[-1] =20 # "enabled_fired"}; -> enabled_fired state =3D raw_state.replace('"', '').replace('};', '').replace= (',', '_') @@ -141,16 +162,14 @@ class Automata: initial_state =3D state[len(self.init_marker):] else: states.append(state) - if "doublecircle" in self.__dot_lines[cursor]: + if "doublecircle" in line: final_states.append(state) has_final_states =3D True =20 - if "ellipse" in self.__dot_lines[cursor]: + if "ellipse" in line: final_states.append(state) has_final_states =3D True =20 - cursor +=3D 1 - states =3D sorted(set(states)) states.remove(initial_state) =20 @@ -163,18 +182,21 @@ class Automata: return states, initial_state, final_states =20 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 - events =3D [] - envs =3D [] - while self.__dot_lines[cursor].lstrip()[0] =3D=3D '"': + for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)= ): + if not line.startswith('"'): + break + # transitions have the format: # "all_fired" -> "both_fired" [ label =3D "disable_irq" ]; # ------------ event is here ------------^^^^^ - if self.__dot_lines[cursor].split()[1] =3D=3D "->": - line =3D self.__dot_lines[cursor].split() - event =3D "".join(line[line.index("label") + 2:-1]).replac= e('"', '') + 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('"', '') =20 # when a transition has more than one labels, they are lik= e this # "local_irq_enable\nhw_local_irq_enable_n" @@ -187,7 +209,7 @@ class Automata: ev, *constr =3D i.split(";") if constr: if len(constr) > 2: - raise ValueError("Only 1 constraint and 1 rese= t are supported") + raise AutomataError("Only 1 constraint and 1 r= eset are supported") envs +=3D self.__extract_env_var(constr) events.append(ev) else: @@ -195,13 +217,12 @@ class Automata: # "enable_fired" [label =3D "enable_fired\ncondition"]; # ----- label is here -----^^^^^ # label and node name must be the same, condition is optio= nal - state =3D self.__dot_lines[cursor].split("label")[1].split= ('"')[1] + state =3D line.split("label")[1].split('"')[1] _, *constr =3D state.split("\\n") if constr: if len(constr) > 1: - raise ValueError("Only 1 constraint is supported i= n the state") + raise AutomataError("Only 1 constraint is supporte= d in the state") envs +=3D self.__extract_env_var([constr[0].replace(" = ", "")]) - cursor +=3D 1 =20 return sorted(set(events)), sorted(set(envs)) =20 @@ -265,18 +286,24 @@ class Automata: nr_state +=3D 1 =20 # declare the matrix.... - matrix =3D [[self.invalid_state_str for x in range(nr_event)] for = y in range(nr_state)] + 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() =20 - while self.__dot_lines[cursor].lstrip()[0] =3D=3D '"': - if self.__dot_lines[cursor].split()[1] =3D=3D "->": - line =3D self.__dot_lines[cursor].split() - origin_state =3D line[0].replace('"', '').replace(',', '_') - dest_state =3D line[2].replace('"', '').replace(',', '_') - possible_events =3D "".join(line[line.index("label") + 2:-= 1]).replace('"', '') + 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: @@ -287,22 +314,21 @@ class Automata: self.self_loop_reset_events.add(event) matrix[states_dict[origin_state]][events_dict[event]] = =3D dest_state else: - state =3D self.__dot_lines[cursor].split("label")[1].split= ('"')[1] + state =3D line.split("label")[1].split('"')[1] state, *constr =3D state.replace(" ", "").split("\\n") if constr: constraints[_StateConstraintKey(states_dict[state])] = =3D constr - cursor +=3D 1 =20 return matrix, constraints =20 def __store_init_events(self) -> tuple[list[bool], list[bool]]: events_start =3D [False] * len(self.events) events_start_run =3D [False] * len(self.events) - for i, _ in enumerate(self.events): + for i in range(len(self.events)): curr_event_will_init =3D 0 curr_event_from_init =3D False curr_event_used =3D 0 - for j, _ in enumerate(self.states): + 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: --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 435BC30F924 for ; Mon, 23 Feb 2026 16:29:16 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864157; cv=none; b=HKacWg7v4QP0eugCtR36HG7XR4O6kpz8Jj8pjJkVp+BAWftvRj/xOHuL95kZKvVi60v+tU2XsorcDxPZu/UIljIXllbfyaVbJGqiZJ5QLSnS3h//eBoypJblUF0M7m18iNjjvWcduIpfF+fOTBQ+7vMuOyuSFcoNR+LUsETe0O4= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864157; c=relaxed/simple; bh=tkxyV2/SJmMyCf1/A4WWOPt/5oameV796XbiX6OYyx4=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=IAc+Mo+GL5J7n//dSbgN//5clrliLSUAFtpBKWXQhLnq5HFrw9EuvWLOUGB5A8szHQ8iJ2vjErJlI6al6L5Hyd41U+S9E5oPFDaC+DIGJoPxcybReZUyeu0rYrqct1//34ZUn8wLmK04nu+ZRcWjcEAzjrK2paXVibOkWdLzYJY= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=KwOAiw5x; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="KwOAiw5x" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864155; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=7Gg0Xg7GuMZrOytFimMyWzeLYWG1wEiuU7NhsKmvk4Q=; b=KwOAiw5xXrnawfdmDbbnQKTqP2ZZAC9T3VUUE3JU6SKoS/cg736VWQNuqkr0Zu9mlvhKne K6Y7l7ciukKLgzzpJ9VdLIJc9iD3w+sUGC037PINVqC0ltWlhjq8TBrY3LKE0HnOtJFeS6 kdnmOsrm8vlSnsQQAv5iXp4PF9FaKGE= Received: from mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-39-9dqp60XrM-Cp2BMxxspYdg-1; Mon, 23 Feb 2026 11:29:12 -0500 X-MC-Unique: 9dqp60XrM-Cp2BMxxspYdg-1 X-Mimecast-MFC-AGG-ID: 9dqp60XrM-Cp2BMxxspYdg_1771864150 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 43CF318005B0; Mon, 23 Feb 2026 16:29:10 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 03BB4180066A; Mon, 23 Feb 2026 16:29:07 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 12/19] rv/rvgen: remove unused sys import from dot2c Date: Mon, 23 Feb 2026 13:17:55 -0300 Message-ID: <20260223162407.147003-13-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" The sys module was imported in the dot2c frontend script but never used. This import was likely left over from earlier development or copied from a template that required sys for exit handling. Remove the unused import to clean up the code and satisfy linters that flag unused imports as errors. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/dot2c | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c index bf0c67c5b66c8..1012becc7fab6 100644 --- a/tools/verification/rvgen/dot2c +++ b/tools/verification/rvgen/dot2c @@ -16,7 +16,6 @@ if __name__ =3D=3D '__main__': from rvgen import dot2c import argparse - import sys =20 parser =3D argparse.ArgumentParser(description=3D'dot2c: converts a .d= ot file into a C structure') parser.add_argument('dot_file', help=3D'The dot file to be converted') --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 50B1B30F818 for ; Mon, 23 Feb 2026 16:29:36 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864177; cv=none; b=sIGqikgXrNda0TZ2Et/G9sLYaKf68tdAV4nQolwaZevpGCHeQ8Bg8X6pZ5KJBwE3FS7hVxaDqJFQoCNrSTS8u6VkXWmb+35Rpt589D/1dgu3eyByYWZMkFSgU8CuygToMcnhlb8K230Bc7eUJ53acOPeHp1JimHpX9Kjq8+oi+U= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864177; c=relaxed/simple; bh=p+D3Eg0BKQWyZJQJRybbBR91hPF08V1/L2VyA/w8Ej8=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=YjrSkEZWb2hIVoQy5hRphGJi4FOypz7J6UA77xHG4wp6jUNK5EMXq4usrpQpwtnJKW8m6+gGPf3rZkQQpmVYSUzaQL+6KJ+QcWDKxLMwAnfECRDpfRZ+8u/q6pAU04wxyrJi+us05DMsNAPOOGvuQoCCI9HCBcq4hc6Mr3ZXrSU= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=Uk6Spajt; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="Uk6Spajt" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864175; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=cZGFMHus8YoaDUQgv49h9/RSwMSUiJxNbxlWLqqVtB4=; b=Uk6SpajthzaYX3wj2v5w/iF79nZdt9sMM72EEW6LMpDVpiRwT2NkJsfmEodSAWVA4DQXuD 5Sb/Roy8vZasVqikQ0asH9cHxnoJkM/xYGcD9hc122o8cvk68/+VuJBJHUH2y9a9VYUIRS ccYYh789WdNRQtr3ryE/ynJeWieqeWg= Received: from mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-168-VHHKup8UPy6jBl8ce8ObKA-1; Mon, 23 Feb 2026 11:29:31 -0500 X-MC-Unique: VHHKup8UPy6jBl8ce8ObKA-1 X-Mimecast-MFC-AGG-ID: VHHKup8UPy6jBl8ce8ObKA_1771864170 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 31AE818002C4; Mon, 23 Feb 2026 16:29:30 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 0ED36180066A; Mon, 23 Feb 2026 16:29:27 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 13/19] rv/rvgen: remove unused __get_main_name method Date: Mon, 23 Feb 2026 13:17:56 -0300 Message-ID: <20260223162407.147003-14-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" The __get_main_name() method in the generator module is never called from anywhere in the codebase. Remove this dead code to improve maintainability. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/generator.py | 6 ------ 1 file changed, 6 deletions(-) diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 40d82afb018f5..56f3bd8db8503 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -205,12 +205,6 @@ obj-$(CONFIG_RV_MON_{name_up}) +=3D monitors/{name}/{n= ame}.o path =3D os.path.join(self.rv_dir, "monitors", path) self.__write_file(path, content) =20 - def __get_main_name(self): - path =3D f"{self.name}/main.c" - if not os.path.exists(path): - return "main.c" - return "__main.c" - def print_files(self): main_c =3D self.fill_main_c() =20 --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 378243101B1 for ; Mon, 23 Feb 2026 16:29:55 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864196; cv=none; b=c8jXijR6jEJCwii0Gjy2Kku/gVPhZ/Iat+xQ0qb7uEqIjAF0b4WACSoJxa/pukTh+5+Lg3GNEWqaidAd+6EHEmT1R/yf31GrJNCQTYQoRwRvf/01zeUMnn2B+4DL3v+6MHUsH/KM7PGMZ6OW6ugtHJqwlb9hgvuRDjE+NCjt7kQ= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864196; c=relaxed/simple; bh=LMj5rhRFqnrHfDcT6VaaFlcCmAbdPhNnzOV+/AzY8ws=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=rFbELH/w44Det6PD2B3ebTJT/IQ6voppU6Ij2f3OHn9l085T17HP9XnIonpzP83yEbTQjFEBOovAj29X2TvG9czqTjPg+x2DYs8FUZOAkI1xNWhlvbKAvzbk551TcEf0Mg12n9ivbXgYtdyMzhU75NvV/GQ4BpHPMCM1NPIE/L8= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=d3xXU9pl; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="d3xXU9pl" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864194; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=0szSBMKq3bi1BM65D50ndvrCiTCipHHqtfMmivl635Y=; b=d3xXU9plG0EiTlhlemhIOQSw3p2eO+GJBFFxva+9snmfl/7W0ydPkWM+Yw4yt4t5Qn8izG De2nk+U+3bEOJX5FtKVcyYGx+dNsqzLxHi8J7E06dLYLJRREbRpIXqbIc7tO/40kDDJUdi X+l9vPDWRNgv2nDa40yKLpgpyG8JwzU= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-633-2NMBgsh9OoK_W1Ikoc5GJA-1; Mon, 23 Feb 2026 11:29:51 -0500 X-MC-Unique: 2NMBgsh9OoK_W1Ikoc5GJA-1 X-Mimecast-MFC-AGG-ID: 2NMBgsh9OoK_W1Ikoc5GJA_1771864190 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id F153E195605A; Mon, 23 Feb 2026 16:29:49 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id D6CAB1800673; Mon, 23 Feb 2026 16:29:47 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 14/19] rv/rvgen: make monitor arguments required in rvgen Date: Mon, 23 Feb 2026 13:17:57 -0300 Message-ID: <20260223162407.147003-15-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Add required=3DTrue to the monitor subcommand arguments for class, spec, and monitor_type in rvgen. These arguments are essential for monitor generation and attempting to run without them would cause AttributeError exceptions later in the code when the script tries to access them. Making these arguments explicitly required provides clearer error messages to users at parse time rather than cryptic exceptions during execution. This improves the user experience by catching missing arguments early with helpful usage information. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao --- tools/verification/rvgen/__main__.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 2e5b868535470..5c923dc10d0f0 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -31,10 +31,11 @@ if __name__ =3D=3D '__main__': monitor_parser.add_argument('-n', "--model_name", dest=3D"model_name") monitor_parser.add_argument("-p", "--parent", dest=3D"parent", required=3DFalse, help=3D"Create a monitor= nested to parent") - monitor_parser.add_argument('-c', "--class", dest=3D"monitor_class", + monitor_parser.add_argument('-c', "--class", dest=3D"monitor_class", r= equired=3DTrue, help=3D"Monitor class, either \"da\", \"ha= \" or \"ltl\"") - monitor_parser.add_argument('-s', "--spec", dest=3D"spec", help=3D"Mon= itor specification file") - monitor_parser.add_argument('-t', "--monitor_type", dest=3D"monitor_ty= pe", + monitor_parser.add_argument('-s', "--spec", dest=3D"spec", required=3D= True, + help=3D"Monitor specification file") + monitor_parser.add_argument('-t', "--monitor_type", dest=3D"monitor_ty= pe", required=3DTrue, help=3Df"Available options: {', '.join(Mon= itor.monitor_types.keys())}") =20 container_parser =3D subparsers.add_parser("container", parents=3D[par= ent_parser]) --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 81EEA30BB83 for ; Mon, 23 Feb 2026 16:30:17 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864218; cv=none; b=qxodz6iNu+zpqV9VbrGnz8br6kJjtoShxuFdRVUpUa0OdbyIWE4O5YOWeJCy0QT7RALPpVSVgzJazVKkFhsiEQ0hJI466uh+Y0J+QibYWHyvwRHMZDbGi74pSJP8LijzaNMwk1H0dOXfuGqmBhO/Qh2XGMzCwwKocqJA4uBkgI0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864218; c=relaxed/simple; bh=3+1mH0oEHDjZM17U3urFB35D5e/V331jenjy+2qK/Cc=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=ONnf5sjR0j1ZOkBLLvBsaLXGA3i4vicAUa8Yk/dAwGb63yt5wV1uxpHT4ThSRzeSbyqc1+WAJWf6RtMbZvTU2Lq7UvuD0JoNEFbraS02Bjay5gS+pvw3EiA9qyhiQwWIpCqTqMlfQgPTbEZu4IVi0JZRMIoYKcIZwBq09LnoNt0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=ABmulni9; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="ABmulni9" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864216; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PUGGPkspJ3zMYbMOZig+zlLmAaK6PE0VrPjeBJRZrt8=; b=ABmulni96Q9Ac0lqs+0kgbPYg/J7Y9vsGkd37MARuPo5Zd8uV5MjraFpsoDhbOFuj0SLqL 4HIlgwKQVey2uOVveelzAPN6zcfgKlV2g0f7i0I2dHlXlhMNWXo/a3Ib+PzlzS0X41QSGP 79fb89fajNTW5Yk3aByutbkfyTwK0hM= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-256-AfcpOgBhMtaRRtK-iLCWvA-1; Mon, 23 Feb 2026 11:30:11 -0500 X-MC-Unique: AfcpOgBhMtaRRtK-iLCWvA-1 X-Mimecast-MFC-AGG-ID: AfcpOgBhMtaRRtK-iLCWvA_1771864210 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id EE5F01955F2D; Mon, 23 Feb 2026 16:30:09 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id D606C1800669; Mon, 23 Feb 2026 16:30:07 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 15/19] rv/rvgen: fix isinstance check in Variable.expand() Date: Mon, 23 Feb 2026 13:17:58 -0300 Message-ID: <20260223162407.147003-16-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" The Variable.expand() method in ltl2ba.py performs contradiction detection by checking if a negated variable already exists in the graph node's old set. However, the isinstance check was incorrectly testing the ASTNode wrapper instead of the wrapped operator, causing the check to always return False. The old set contains ASTNode instances which wrap LTL operators via their .op attribute. The fix changes isinstance(f, NotOp) to isinstance(f.op, NotOp) to correctly examine the wrapped operator type. This follows the established pattern used elsewhere in the file, such as the iteration at lines 572-574 which accesses o.op.is_temporal() on items from node.old. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao --- tools/verification/rvgen/rvgen/ltl2ba.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/= rvgen/rvgen/ltl2ba.py index f9855dfa3bc1c..7f538598a8681 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -395,7 +395,7 @@ class Variable: @staticmethod def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: for f in node.old: - if isinstance(f, NotOp) and f.op.child is n: + if isinstance(f.op, NotOp) and f.op.child is n: return node_set node.old |=3D {n} return node.expand(node_set) --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 4710F3128D4 for ; Mon, 23 Feb 2026 16:30:33 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864234; cv=none; b=KpeEe9oE3WxjDfNFkThaiKHyqyI1G8uBrcHVXBsfCAaUVLttq5FccYRM9zKiGV2gL0Q1/p2ClHgGVp8oYSEq89QmUq9DTUFjDEO6C5fZrnWFY1TXhQ0mClKxU0B+tW7PvxPeUIAUTRW9aZGWcX6P9scBXs3LQfT8uXIS8T96z2U= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864234; c=relaxed/simple; bh=JKCYNEeN/DjkXwRGymqHAF0dsNfsOprRq4sv49NAUYM=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=FPCwNjAhoKQZGGPjJm3cwKQof43UkLyaMKbrwVE8NxeIHOEDlWSAvOH0lufr2hLi7zfRcdHkxwP3FDt5IH4pGZrLStqxZfA487KgoyOYFyj2dnufeVj+vqdEoo66yE8o/XyeugspqXMWPYW8MJuev4CaolmP+5935x9GXJ3IvMU= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=fO6DShav; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="fO6DShav" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864232; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=C80re9BR9cuOqri0fwco4+uqG9iMQO/SIrKYil8gync=; b=fO6DShavd0QZiV55jirN8RswEat8d+RlrDS9DOBeJmWD8TppDxTwnuFuJLqlqdjPdQkWnm 37CKYP616dG6lHtQAzCSYmKMOf0V5vRsSUQMItCHvyoqnJbOLAQncSOr1VRSLFBv+O92GP qA3gOQjT5fahaDH/zjiE6PvDSS246To= Received: from mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-269-bnehINCWOPKbnii0F-GiWQ-1; Mon, 23 Feb 2026 11:30:30 -0500 X-MC-Unique: bnehINCWOPKbnii0F-GiWQ-1 X-Mimecast-MFC-AGG-ID: bnehINCWOPKbnii0F-GiWQ_1771864229 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 95F3019560B2; Mon, 23 Feb 2026 16:30:29 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 7DC811800669; Mon, 23 Feb 2026 16:30:27 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 16/19] rv/rvgen: extract node marker string to class constant Date: Mon, 23 Feb 2026 13:17:59 -0300 Message-ID: <20260223162407.147003-17-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Add a node_marker class constant to the Automata class to replace the hardcoded "{node" string literal used throughout the DOT file parsing logic. This follows the existing pattern established by the init_marker and invalid_state_str class constants in the same class. The "{node" string is used as a marker to identify node declaration lines in DOT files during state variable extraction and cursor positioning. Extracting it to a named constant improves code maintainability and makes the marker's purpose explicit. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index 6613a9d6159a9..fd2a4a0c3f6eb 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -44,6 +44,7 @@ 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""" @@ -112,7 +113,7 @@ class Automata: for cursor, line in enumerate(self.__dot_lines): split_line =3D line.split() =20 - if len(split_line) and split_line[0] =3D=3D "{node": + if len(split_line) and split_line[0] =3D=3D self.node_marker: return cursor =20 raise AutomataError("Could not find a beginning state") @@ -127,9 +128,9 @@ class Automata: continue =20 if state =3D=3D 0: - if line[0] =3D=3D "{node": + if line[0] =3D=3D self.node_marker: state =3D 1 - elif line[0] !=3D "{node": + elif line[0] !=3D self.node_marker: break else: raise AutomataError("Could not find beginning event") @@ -151,7 +152,7 @@ class Automata: # 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 "{node": + if not split_line or split_line[0] !=3D self.node_marker: break =20 raw_state =3D split_line[-1] --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 DB4B63128D4 for ; Mon, 23 Feb 2026 16:30:55 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864257; cv=none; b=ZPdm8gOkoacUnntKaE1UvSmz3f/fMuB1ZzfjlWKH3wXWjDuPAJ0JEgTxwdllwSuKBeCmAsr97diEnE51YOE9tXXCG6lkpPuHhK/l4kw0UKShJ8j/yT/yeHhrrY+KPr6306fazbZiawIcZBUpgQRiG2+E+FBSM1P1R2SqRA8bChA= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864257; c=relaxed/simple; bh=4M22TMqr4Kp7d6uOCNhz/fRmCEbkYk7/hUz8OUuWkys=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=ZrFpikt77T0ywNoduqWHq1WFpDXC3ZGWz/BjczoZQ2v7JDy2+qFPBTbLc+ey1UGXsDCHIZvB1oamHb/yclbK/WLYJ/y9melHAHDnM718RmHnDprw1VF03nR6mpbyViLLybbHXEf0gQBEbCzb1xl1a9pj0AfSqeU24YkemgaT62k= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=E2R6gC55; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="E2R6gC55" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864254; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=AHpeVA2TW9g1nzpiKCBeIjVkqx/nyz9EMg/ZqH0sr8w=; b=E2R6gC55THXxF6SBHlFTsBsW2mSmMoIQU5IUnLv2BlmrVVsKEIEaXuEpn+zNGxZKkRlllC 5D/xoGG22Y2wMkCv8d3s37BiQxWtplHyePErcUQmLN83I/SVlzNoPXLO9FJRofqrdwn9Il /3H4Fbifn9PkPnGJ2Dj8nlpnQOmZX1Q= Received: from mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-628-jioOAsEAM0GA8o3Fu3jJXg-1; Mon, 23 Feb 2026 11:30:51 -0500 X-MC-Unique: jioOAsEAM0GA8o3Fu3jJXg-1 X-Mimecast-MFC-AGG-ID: jioOAsEAM0GA8o3Fu3jJXg_1771864249 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-05.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 542B9195608F; Mon, 23 Feb 2026 16:30:49 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 3BC791800370; Mon, 23 Feb 2026 16:30:46 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 17/19] rv/rvgen: enforce presence of initial state Date: Mon, 23 Feb 2026 13:18:00 -0300 Message-ID: <20260223162407.147003-18-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" The __get_state_variables() method parses DOT files to identify the automaton's initial state. If the input file lacks a node with the required initialization prefix, the initial_state variable is referenced before assignment, causing an UnboundLocalError or a generic error during the state removal step. Initialize the variable explicitly and validate that a start node was found after parsing. Raise a descriptive AutomataError if the definition is missing to improve debugging and ensure the automaton is valid. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/automata.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verificatio= n/rvgen/rvgen/automata.py index fd2a4a0c3f6eb..ac765c9b2dece 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -145,6 +145,7 @@ class Automata: # wait for node declaration states =3D [] final_states =3D [] + initial_state =3D "" =20 has_final_states =3D False cursor =3D self.__get_cursor_begin_states() @@ -171,6 +172,9 @@ class Automata: final_states.append(state) has_final_states =3D True =20 + if not initial_state: + raise AutomataError("The automaton doesn't have an initial sta= te") + states =3D sorted(set(states)) states.remove(initial_state) =20 --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (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 00B69313543 for ; Mon, 23 Feb 2026 16:31:14 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864276; cv=none; b=NVLMgeYUQ6zucett7F6HbsfZkk7IPNBOSkdcBg1/uw1E0P3C2fiV2arq/ytzY9JAi1FnZGbkFNDoWG7Ky5FaT7wKnt3ZXtEv3e7RpBR3sISWsyhU5wjzdNtMoL/jHZd+RLu6SRZd/JsGiUF2dyc4a107YTyT5iKQJZi30LM/iYM= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864276; c=relaxed/simple; bh=0fVlBJQm+igAU5t1TvfWsxMcVM5Q0TPaMEDt9Vk5wnM=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=KelgZp79O+kjSNWoW+xEzisl4kIARuNUjFXabzv1ebpCUFaFztkhedmfG+0Hfgblj3NkzLUl15txO2T1IoZ1z/1cC4+e4GvTrCxyQr7XMHnQz3rPDr2EpItq4vbc8vkAmFikl3HW/rbCP+XyhFRs0jzQw0A7pyHZYG7DjjDjLSQ= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=eqBZvFP9; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="eqBZvFP9" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864274; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=dCAIlwTWFIiBKB7lUUOxEwC4wlCG1Kk+xafXT1zGEqU=; b=eqBZvFP9HO3RjNJ6+I3VFqUn0rqPnLbl7RHZm8OryCAnCkKMECxfOFk2cKiG3R/coY+58q Tf695At+YvsKAF73jwbIvDiDg91aFGuvmwXPfGT+pgkbV9k7vq/FKyphJDYCcXEl3UWiDz 82nE4Cokafw6kXivnZ9wnyj9i1BivYg= Received: from mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-639-WdGEk8MEPXOTd9SEuYNzXw-1; Mon, 23 Feb 2026 11:31:10 -0500 X-MC-Unique: WdGEk8MEPXOTd9SEuYNzXw-1 X-Mimecast-MFC-AGG-ID: WdGEk8MEPXOTd9SEuYNzXw_1771864269 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 67D7A1800464; Mon, 23 Feb 2026 16:31:09 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 4D74A1800370; Mon, 23 Feb 2026 16:31:07 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 18/19] rv/rvgen: fix unbound loop variable warning Date: Mon, 23 Feb 2026 13:18:01 -0300 Message-ID: <20260223162407.147003-19-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" Pyright static analysis reports a "possibly unbound variable" warning for the loop variable `i` in the `abbreviate_atoms` function. The variable is accessed after the inner loop terminates to slice the atom string. While the loop logic currently ensures execution, the analyzer flags the reliance on the loop variable persisting outside its scope. Refactor the prefix length calculation into a nested `find_share_length` helper function. This encapsulates the search logic and uses explicit return statements, ensuring the length value is strictly defined. This satisfies the type checker and improves code readability without altering the runtime behavior. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/ltl2k.py | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index b6300c38154dc..b8ac584fe2504 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -44,13 +44,17 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]: skip =3D ["is", "by", "or", "and"] return '_'.join([x[:2] for x in s.lower().split('_') if x not in s= kip]) =20 - abbrs =3D [] - for atom in atoms: + def find_share_length(atom: str) -> int: for i in range(len(atom), -1, -1): if sum(a.startswith(atom[:i]) for a in atoms) > 1: - break - share =3D atom[:i] - unique =3D atom[i:] + return i + return 0 + + abbrs =3D [] + for atom in atoms: + share_len =3D find_share_length(atom) + share =3D atom[:share_len] + unique =3D atom[share_len:] abbrs.append((shorten(share) + shorten(unique))) return abbrs =20 --=20 2.53.0 From nobody Thu Apr 2 00:12:48 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (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 20960311C1D for ; Mon, 23 Feb 2026 16:31:35 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864296; cv=none; b=fmkR38R00AT3rBPdXeLMAmT3ahEEVQmhRO6SwTrQXI8qpatkfVy1sYvxHJCapvaJ/Pa3Hkvgnpq1H0PzjDCLn1FwqOnm0sl6TXMFaAAnweHATAT+ShRPBol4ruUEw3n8g5QWkVwqkZT+H7sY5CL1A5Tp2ClMBKEb7BJARKdNErE= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864296; c=relaxed/simple; bh=KU9/4VAZzijQArIsaKiYpI841fkcKtb9bMBsovL0JqQ=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=Uj9AsXSAVIlN3DChioywtVGfP9nhkVqZSJIv/qWz/IGMf1rvXQuUaLEP5Z21FFtNhzXK99CZBeywbZpJgancNTx5sSYj/5NOQBNS+rQ1fTIcLL7Q26LtV+lS0DifCtST3D9Os5BUW7n3/chFryFbX1BO+Bp4C+3bxfumOfqwqYI= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=G1g44mxB; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="G1g44mxB" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864294; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=dI23U9Hdos8EpUNnWdFryDt4BhqGz6vCVqX1QyTKn7I=; b=G1g44mxBKZZ5YXaWxcYFqjzf8biWaa+dUAyuvAAik6mgXCUtuTx4QgtDN1QqE4aihY2Jh1 3QzUhzYT3IwFiAVcG5eQfPeNlwPOjsxz8PYCoD3/vdP33lWkuZBoHewCuvYltCONysoucK /gaFZO71GrBR/pso59DsyH6NnRgnik8= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-526-12TAfljIONCEnDH90iwtBw-1; Mon, 23 Feb 2026 11:31:30 -0500 X-MC-Unique: 12TAfljIONCEnDH90iwtBw-1 X-Mimecast-MFC-AGG-ID: 12TAfljIONCEnDH90iwtBw_1771864289 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id B5E321956068; Mon, 23 Feb 2026 16:31:29 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 7DB7E1800669; Mon, 23 Feb 2026 16:31:27 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 19/19] rv/rvgen: fix _fill_states() return type annotation Date: Mon, 23 Feb 2026 13:18:02 -0300 Message-ID: <20260223162407.147003-20-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> 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 X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" The _fill_states() method returns a list of strings, but the type annotation incorrectly specified str. Update the annotation to list[str] to match the actual return value. Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/ltl2k.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index b8ac584fe2504..81fd1f5ea5ea2 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -75,7 +75,7 @@ class ltl2k(generator.Monitor): if not self.name: self.name =3D Path(file_path).stem =20 - def _fill_states(self) -> str: + def _fill_states(self) -> list[str]: buf =3D [ "enum ltl_buchi_state {", ] --=20 2.53.0