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

[Nam Cao]

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@xxxxxxxxxxxxx>
---
 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