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 <[email protected]> --- 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
