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