[PATCH 04/13] verification/rvgen: Convert __fill_verify_invariants_func() to Lark

[Nam Cao]

Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing code.

Signed-off-by: Nam Cao <namcao@xxxxxxxxxxxxx>
---
 tools/verification/rvgen/rvgen/dot2k.py | 32 ++++++++++++++++---------
 1 file changed, 21 insertions(+), 11 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e6f476b903b0..3e7040398a20 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -12,6 +12,7 @@ from collections import deque
 from .dot2c import Dot2c
 from .generator import Monitor
 from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
+from .automata import ConstraintRule
 
 
 class dot2k(Monitor, Dot2c):
@@ -177,6 +178,14 @@ class ha2k(dot2k):
             raise AutomataError("Detected deterministic automaton, use the 'da' class")
         self.trace_h = self._read_template_file("trace_hybrid.h")
         self.__parse_constraints()
+        self.has_invariant = False
+        self.has_guard = False
+        for state in self._states:
+            if state.inv:
+                self.has_invariant = True
+        for transition in self.transitions:
+            if transition.rule or transition.reset:
+                self.has_guard = True
 
     def fill_monitor_class_type(self) -> str:
         if self._is_id_monitor():
@@ -218,14 +227,13 @@ class ha2k(dot2k):
         assert env.rstrip(f"_{self.name}") in self.envs
         return env
 
-    def __start_to_invariant_check(self, constr: str) -> str:
+    def __start_to_invariant_check(self, inv: ConstraintRule) -> str:
         # by default assume the timer has ns expiration
-        env = self.__get_constraint_env(constr)
         clock_type = "ns"
-        if self.env_types.get(env.rstrip(f"_{self.name}")) == "j":
+        if inv.unit == "j":
             clock_type = "jiffy"
 
-        return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
+        return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns)"
 
     def __start_to_conv(self, constr: str) -> str:
         """
@@ -320,20 +328,22 @@ class ha2k(dot2k):
                 self.invariants[key] = rules[0]
 
     def __fill_verify_invariants_func(self) -> list[str]:
-        buff = []
-        if not self.invariants:
+        if not self.has_invariant:
             return []
 
-        buff.append(
+        buff = [
 f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
 \t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
 \t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
-{{""")
+{{"""]
 
         _else = ""
-        for state, constr in sorted(self.invariants.items()):
-            check_str = self.__start_to_invariant_check(constr)
-            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
+        for state in self._states:
+            if not state.inv:
+                continue
+
+            check_str = self.__start_to_invariant_check(state.inv)
+            buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
             buff.append(f"\t\t{check_str};")
             _else = "else "
 
-- 
2.47.3