All previous users of self.invariants and self.guards have been converted to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <[email protected]> --- tools/verification/rvgen/rvgen/dot2k.py | 67 ++----------------------- 1 file changed, 4 insertions(+), 63 deletions(-) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index c662c888f991..5ea5d16df29b 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -177,7 +177,6 @@ class ha2k(dot2k): if not self.is_hybrid_automata(): 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: @@ -295,64 +294,6 @@ class ha2k(dot2k): separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " " return ["res = " + separator.join(rules)] - def __validate_constraint(self, key: tuple[int, int] | int, constr: str, - rule, reset) -> None: - # event constrains are tuples and allow both rules and reset - # state constraints are only used for expirations (e.g. clk<N) - if self.is_event_constraint(key): - if not rule and not reset: - raise AutomataError("Unrecognised event constraint " - f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})") - if rule and (rule["env"] in self.env_types and - rule["env"] not in self.env_stored): - raise AutomataError("Clocks in hybrid automata always require a storage" - f" ({rule["env"]})") - else: - if not rule: - raise AutomataError("Unrecognised state constraint " - f"({self.states[key]}: {constr})") - if rule["env"] not in self.env_stored: - raise AutomataError("State constraints always require a storage " - f"({rule["env"]})") - if rule["op"] not in ["<", "<="]: - raise AutomataError("State constraints must be clock expirations like" - f" clk<N ({rule.string})") - - def __parse_constraints(self) -> None: - self.guards: dict[_EventConstraintKey, str] = {} - self.invariants: dict[_StateConstraintKey, str] = {} - for key, constraint in self.constraints.items(): - rules = [] - resets = [] - for c, sep in self._split_constraint_expr(constraint): - rule = self.constraint_rule.search(c) - reset = self.constraint_reset.search(c) - self.__validate_constraint(key, c, rule, reset) - if rule: - value = rule["val"] - value_len = len(rule["val"]) - unit = None - if rule.groupdict().get("unit"): - value_len += len(rule["unit"]) - unit = rule["unit"] - c = c[:-(value_len)] - value = self.__adjust_value(value, unit) - if self.is_event_constraint(key): - c = self.__parse_single_constraint(rule, value) - if sep: - c += f" {sep}" - else: - c = self.__parse_timer_constraint(rule, value) - rules.append(c) - if reset: - c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)" - resets.append(c) - if self.is_event_constraint(key): - res = self.__format_guard_rules(rules) + resets - self.guards[key] = ";".join(res) - else: - self.invariants[key] = rules[0] - def __fill_verify_invariants_func(self) -> list[str]: if not self.has_invariant: return [] @@ -482,15 +423,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) {{""") - if self.invariants: + if self.has_invariant: buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, " "event, next_state, time_ns))\n\t\treturn false;\n") - if self.guards: + if self.has_guard: buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, " "next_state, time_ns))\n\t\treturn false;\n") - if self.invariants: + if self.has_invariant: buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n") buff.append("\treturn true;\n}\n") @@ -567,7 +508,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func() def _fill_timer_type(self) -> list: - if self.invariants: + if self.has_invariant: return [ "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */", "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" -- 2.47.3
