diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py index b8e07e463293..55041d128b09 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -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) diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py index 5c1c5597d839..9cc452305a2a 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)) +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 diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py index f779d9528af3..6878cc79e6f7 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 -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 diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index e7ba68a54c1f..55222e38323f 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, 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 None: self.guards: dict[_EventConstraintKey, str] = {} diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py index 5eac12e110dc..571093a92bdc 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 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) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index f14e6760ac3d..f9855dfa3bc1 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -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 = \" format") + raise AutomataError("Please define your specification in the \"RULE = \" format") for node in rule: if not isinstance(node.op, Variable): diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py index b075f98d50c4..08ad245462e7 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 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: