[PATCH 05/13] verification/rvgen: Convert __fill_setup_invariants_func() to Lark

Nam Cao
2026-05-05T06:59:49Z

Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed states from
Lark.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
tools/verification/rvgen/rvgen/dot2k.py | 36 ++++++++++++++++++-------
1 file changed, 27 insertions(+), 9 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 3e7040398a20..3a39ae29e41e 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -250,6 +250,18 @@ class ha2k(dot2k):
return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
f" {value}, time_ns)")

+ def __parse_invariant(self, inv):
+ # by default assume the timer has ns expiration
+ clock_type = "ns"
+ if inv.unit == "j":
+ clock_type = "jiffy"
+
+ env = inv.env + self.enum_suffix
+ val = inv.val.replace("()", "(ha_mon)")
+
+ return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
+ f" {val}, time_ns)")
+
def __format_guard_rules(self, rules: list[str]) -> list[str]:
"""
Merge guard constraints as a single C return statement.
@@ -463,15 +475,14 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
return conflict_guards, conflict_invs

def __fill_setup_invariants_func(self) -> list[str]:
- buff = []
- if not self.invariants:
+ if not self.has_invariant:
return []

- buff.append(
+ buff = [
f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]

conditions = ["next_state == curr_state"]
conditions += [f"event != {e}{self.enum_suffix}"
@@ -480,13 +491,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
buff.append(f"\tif ({condition_str})\n\t\treturn;")

_else = ""
- for state, constr in sorted(self.invariants.items()):
- buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
- buff.append(f"\t\t{constr};")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ inv = self.__parse_invariant(inv)
+ buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
+ buff.append(f"\t\t{inv};")
_else = "else "

- for state in self.invariants:
- buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
+ for state in self._states:
+ inv = state.inv
+ if not inv:
+ continue
+ buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
buff.append("\t\tha_cancel_timer(ha_mon);")

buff.append("}\n")
--
2.47.3