This patch series introduces fixes and improvements to the RV Generator
(rvgen) tool in tools/verification. The primary goal is to enhance the
tool's robustness, maintainability, and correctness by addressing
several latent bugs, modernizing the Python codebase, and improving its
overall structure and error handling.
The changes include fixing logic errors in DOT file validation,
resolving unbound variable errors that could lead to runtime crashes,
and improving exception handling by removing dangerous bare except
clauses. The codebase is updated to use contemporary Python idioms such
as f-strings and context managers. Additionally, type annotations are
added to resolve static analysis errors.
Changes in v3:
- Dropped patch "add missing return type annotations" as per Gabriele
Monaco's feedback that annotations on stub methods are not needed at
this stage.
- Expanded AutomataError exception class patch to also replace generic
ValueError exceptions in HA and LTL modules, as suggested by Gabriele
Monaco.
- Updated typo fix patch to also correct singular/plural inconsistencies
("automata" to "automaton"), as noted by Gabriele Monaco.
- Included additional f-string conversion in dot2k.py found by Gabriele
Monaco after rebase.
Changes in v2:
- Dropped patches related to the @not_implemented decorator and abstract
method stubs (v1 patches 9, 18, 19) to address class hierarchy
improvements in a separate series.
- Dropped trivial cleanup patches (boolean simplification, __contains__)
as they were already fixed after rebasing from
linux-trace/latency/for-next.
- Merged typo fix patches into a single patch.
- Changed the fix for the unbound loop variable warning in abbreviate_atoms
pyright report.
- Reworked initial state validation to strictly enforce the presence of
an initial state.
Wander Lairson Costa (19):
rv/rvgen: introduce AutomataError exception class
rv/rvgen: remove bare except clauses in generator
rv/rvgen: replace % string formatting with f-strings
rv/rvgen: replace __len__() calls with len()
rv/rvgen: remove unnecessary semicolons
rv/rvgen: use context managers for file operations
rv/rvgen: fix typos in automata and generator docstring and comments
rv/rvgen: fix PEP 8 whitespace violations
rv/rvgen: fix DOT file validation logic error
rv/rvgen: use class constant for init marker
rv/rvgen: refactor automata.py to use iterator-based parsing
rv/rvgen: remove unused sys import from dot2c
rv/rvgen: remove unused __get_main_name method
rv/rvgen: make monitor arguments required in rvgen
rv/rvgen: fix isinstance check in Variable.expand()
rv/rvgen: extract node marker string to class constant
rv/rvgen: enforce presence of initial state
rv/rvgen: fix unbound loop variable warning
rv/rvgen: fix _fill_states() return type annotation
tools/verification/rvgen/__main__.py | 19 +--
tools/verification/rvgen/dot2c | 1 -
tools/verification/rvgen/rvgen/automata.py | 155 ++++++++++++--------
tools/verification/rvgen/rvgen/dot2c.py | 58 ++++----
tools/verification/rvgen/rvgen/dot2k.py | 61 ++++----
tools/verification/rvgen/rvgen/generator.py | 91 +++++-------
tools/verification/rvgen/rvgen/ltl2ba.py | 11 +-
tools/verification/rvgen/rvgen/ltl2k.py | 54 ++++---
8 files changed, 237 insertions(+), 213 deletions(-)
--
2.53.0
