bybrooklyn/linux
1
0
Fork 0
mirror of https://github.com/torvalds/linux.git synced 2026-04-18 06:44:00 -04:00
Code Issues Packages Projects Releases Wiki Activity

rv/rvgen: introduce AutomataError exception class

Browse Source 
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 <gmonaco@redhat.com>
Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/20260223162407.147003-2-wander@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
This commit is contained in:
Wander Lairson Costa
2026-02-23 13:17:44 -03:00
committed by Gabriele Monaco
parent b133207deb
commit a115ee5a32
7 changed files with 43 additions and 34 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
tools/verification/rvgen/__main__.py
View File

@@ -13,6 +13,7 @@ if __name__ == '__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
@@ -53,9 +54,8 @@ if __name__ == '__main__':
sys.exit(1)
else:
monitor = 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=sys.stderr)
sys.exit(1)
print("Writing the monitor into the directory %s" % monitor.name)

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

@@ -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))
class AutomataError(Exception):
"""Exception raised for errors in automata parsing and validation.
Raised when DOT file processing fails due to invalid format, I/O errors,
or malformed automaton definitions.
"""
class Automata:
"""Automata class: Reads a dot file and part it as an automata.
@@ -72,11 +79,11 @@ class Automata:
basename = 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)
model_name = ntpath.splitext(basename)[0]
if model_name.__len__() == 0:
raise Exception("not a dot file: %s" % self.__dot_path)
raise AutomataError("not a dot file: %s" % self.__dot_path)
return model_name
@@ -85,8 +92,8 @@ class Automata:
dot_lines = []
try:
dot_file = 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
dot_lines = dot_file.read().splitlines()
dot_file.close()
@@ -95,7 +102,7 @@ class Automata:
line = dot_lines[cursor].split()
if (line[0] != "digraph") and (line[1] != "state_automaton"):
raise Exception("Not a valid .dot format: %s" % self.__dot_path)
raise AutomataError("Not a valid .dot format: %s" % self.__dot_path)
else:
cursor += 1
return dot_lines

4
tools/verification/rvgen/rvgen/dot2c.py
View File

@@ -13,7 +13,7 @@
# For further information, see:
# Documentation/trace/rv/deterministic_automata.rst
from .automata import Automata
from .automata import Automata, AutomataError
class Dot2c(Automata):
enum_suffix = ""
@@ -103,7 +103,7 @@ class Dot2c(Automata):
min_type = "unsigned int"
if self.states.__len__() > 1000000:
raise Exception("Too many states: %d" % self.states.__len__())
raise AutomataError("Too many states: %d" % self.states.__len__())
return min_type

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

@@ -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, AutomataError
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' class")
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 = self._read_template_file("trace_hybrid.h")
self.__parse_constraints()
@@ -266,22 +266,22 @@ class ha2k(dot2k):
# state constraints are only used for expirations (e.g. clk<N)
if self.is_event_constraint(key):
if not rule and not reset:
raise ValueError("Unrecognised event constraint "
f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
raise AutomataError("Unrecognised event constraint "
f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
if rule and (rule["env"] in self.env_types and
rule["env"] not in self.env_stored):
raise ValueError("Clocks in hybrid automata always require a storage"
f" ({rule["env"]})")
raise AutomataError("Clocks in hybrid automata always require a storage"
f" ({rule["env"]})")
else:
if not rule:
raise ValueError("Unrecognised state constraint "
f"({self.states[key]}: {constr})")
raise AutomataError("Unrecognised state constraint "
f"({self.states[key]}: {constr})")
if rule["env"] not in self.env_stored:
raise ValueError("State constraints always require a storage "
f"({rule["env"]})")
raise AutomataError("State constraints always require a storage "
f"({rule["env"]})")
if rule["op"] not in ["<", "<="]:
raise ValueError("State constraints must be clock expirations like"
f" clk<N ({rule.string})")
raise AutomataError("State constraints must be clock expirations like"
f" clk<N ({rule.string})")
def __parse_constraints(self) -> None:
self.guards: dict[_EventConstraintKey, str] = {}

7
tools/verification/rvgen/rvgen/generator.py
View File

@@ -51,10 +51,7 @@ class RVGenerator:
raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
def _read_file(self, path):
try:
fd = open(path, 'r')
except OSError:
raise Exception("Cannot open the file: %s" % path)
fd = open(path, 'r')
content = fd.read()
@@ -65,7 +62,7 @@ class RVGenerator:
try:
path = 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 file in the template/
# directory, which is one level up
path = os.path.join(self.abs_template_dir, "..", file)

9
tools/verification/rvgen/rvgen/ltl2ba.py
View File

@@ -9,6 +9,7 @@
from ply.lex import lex
from ply.yacc import yacc
from .automata import AutomataError
# Grammar:
# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -62,7 +63,7 @@ t_ignore_COMMENT = r'\#.*'
t_ignore = ' \t\n'
def t_error(t):
raise ValueError(f"Illegal character '{t.value[0]}'")
raise AutomataError(f"Illegal character '{t.value[0]}'")
lexer = lex()
@@ -487,7 +488,7 @@ def p_unop(p):
elif p[1] == "not":
op = NotOp(p[2])
else:
raise ValueError(f"Invalid unary operator {p[1]}")
raise AutomataError(f"Invalid unary operator {p[1]}")
p[0] = ASTNode(op)
@@ -507,7 +508,7 @@ def p_binop(p):
elif p[2] == "imply":
op = ImplyOp(p[1], p[3])
else:
raise ValueError(f"Invalid binary operator {p[2]}")
raise AutomataError(f"Invalid binary operator {p[2]}")
p[0] = ASTNode(op)
@@ -526,7 +527,7 @@ def parse_ltl(s: str) -> ASTNode:
subexpr[assign[0]] = assign[1]
if rule is None:
raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format")
raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
for node in rule:
if not isinstance(node.op, Variable):

8
tools/verification/rvgen/rvgen/ltl2k.py
View File

@@ -4,6 +4,7 @@
from pathlib import Path
from . import generator
from . import ltl2ba
from .automata import AutomataError
COLUMN_LIMIT = 100
@@ -60,8 +61,11 @@ class ltl2k(generator.Monitor):
if MonitorType != "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 = ltl2ba.create_graph(f.read())
try:
with open(file_path) as f:
self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
except OSError as exc:
raise AutomataError(exc.strerror) from exc
self.atoms_abbr = abbreviate_atoms(self.atoms)
self.name = extra_params.get("model_name")
if not self.name: