Thank you for your contribution! Sashiko AI review found 7 potential issue(s) to consider: - [High] Spurious invalidity checks generated due to naive substring matching. - [High] State-specific self-loop resets are applied globally, causing improper invariant timer restarts. - [High] Incorrect tracepoint class returned by `fill_monitor_class`, leading to compilation failures. - [Medium] Premature truncation of BFS algorithm in `__find_inv_conflicts`. - [Medium] Regex `constraint_rule` fails to parse valid single-character variables and identifiers containing digits. - [Medium] Multiple state invariants separated by logical operators are silently truncated. - [Medium] Substring matching for clock resets in `__find_inv_conflicts` yields false positives. --
--- Patch [4]: [PATCH v8 04/12] verification/rvgen: Add support for Hybrid Automata --- commit 12c92be15261e4701023aceb7f2bd71c606ecce3 Author: Gabriele Monaco <[email protected]> verification/rvgen: Add support for Hybrid Automata Add the possibility to parse dot files as hybrid automata and generate the necessary code from rvgen. > diff --git a/tools/verification/rvgen/rvgen/automata.py > b/tools/verification/rvgen/rvgen/automata.py > --- a/tools/verification/rvgen/rvgen/automata.py > +++ b/tools/verification/rvgen/rvgen/automata.py [ ... ] > + # val can be numerical, uppercase (constant or macro), lowercase > (parameter or function) > + # only numerical values should have units > + constraint_rule = re.compile(r""" > + ^ > + (?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env var > + (?P<op>[!<=>]{1,2}) # operator > + (?P<val> > + [0-9]+ | # numerical value > + [A-Z_]+\(\) | # macro > + [A-Z_]+ | # constant > + [a-z_]+\(\) | # function > + [a-z_]+ # parameter > + ) > + (?P<unit>[a-z]{1,2})? # optional unit for numerical values > + """, re.VERBOSE) [Severity: Medium] Could this regular expression reject valid single-character variables? The pattern requires environment variables to be at least two characters long, which rejects single-letter variables like 'x' or 't'. Additionally, does the value matching group (?P<val> ...) correctly handle digits in constant, macro, function, or parameter names? The current character sets [a-z_]+ and [A-Z_]+ appear to exclude numbers. [ ... ] > @@ -157,6 +260,7 @@ class Automata: > > # declare the matrix.... > matrix = [[ self.invalid_state_str for x in range(nr_event)] for y > in range(nr_state)] > + constraints: dict[_ConstraintKey, list[str]] = {} > > # and we are back! Let's fill the matrix > cursor = self.__get_cursor_begin_events() > @@ -166,12 +270,24 @@ class Automata: > line = self.__dot_lines[cursor].split() > origin_state = line[0].replace('"','').replace(',','_') > dest_state = line[2].replace('"','').replace(',','_') > - possible_events = > "".join(line[line.index("label")+2:-1]).replace('"', '') > + possible_events = "".join(line[line.index("label") + > 2:-1]).replace('"', '') > for event in possible_events.split("\\n"): > + event, *constr = event.split(";") > + if constr: > + key = _EventConstraintKey(states_dict[origin_state], > events_dict[event]) > + constraints[key] = constr > + # those events reset also on self loops > + if origin_state == dest_state and "reset" in > "".join(constr): > + self.self_loop_reset_events.add(event) [Severity: High] Does recording these events globally create issues when the same event triggers different behavior in other states? When an event triggers a variable reset on a self-loop, it is recorded by name in the global self_loop_reset_events set without associating it with the specific state where the reset occurs. > diff --git a/tools/verification/rvgen/rvgen/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > --- a/tools/verification/rvgen/rvgen/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py [ ... ] > +class ha2k(dot2k): > + """Hybrid automata only""" > + def __init__(self, *args, **kwargs): > + super().__init__(*args, **kwargs) > + if not self.is_hybrid_automata(): > + raise ValueError("Detected deterministic automata, use the 'da' > class") > + self.trace_h = self._read_template_file("trace_hybrid.h") > + self.__parse_constraints() > + > + def fill_monitor_class_type(self) -> str: > + if self.monitor_type == "per_task": > + return "HA_MON_EVENTS_ID" > + return "HA_MON_EVENTS_IMPLICIT" > + > + def fill_monitor_class(self) -> str: > + """ > + Used for tracepoint classes, since they are shared we keep da > + instead of ha (also for the ha specific tracepoints). > + The tracepoint class is not visible to the tools. > + """ > + return super().fill_monitor_class() [Severity: High] Does this method return the correct tracepoint class? The docstring mentions keeping 'da' instead of 'ha' because tracepoint classes are shared. However, calling super().fill_monitor_class() returns self.monitor_class, which is set to 'ha' for this subclass. This generates DEFINE_EVENT(error_ha, ...) in the C code, but the error_ha tracepoint class is not declared in the kernel headers, which expect error_da. Could this lead to compilation failures? [ ... ] > + def __format_guard_rules(self, rules: list[str]) -> list[str]: > + """ > + Merge guard constraints as a single C return statement. > + If the rules include a stored env, also check its validity. > + Break lines in a best effort way that tries to keep readability. > + """ > + if not rules: > + return [] > + > + invalid_checks = [f"ha_monitor_env_invalid(ha_mon, > {env}{self.enum_suffix}) ||" > + for env in self.env_stored if any(env in rule for > rule in rules)] [Severity: High] Can this substring check incorrectly match unrelated variables in the generated C code? The expression "env in rule" checks if the variable name is a substring of the generated C code. If env is a short string like "i", it will match inside unrelated words like "time_ns". This could inject spurious ha_monitor_env_invalid() checks for the wrong environment variables. If those variables are uninitialized, the condition short-circuits to true, incorrectly allowing state transitions. [ ... ] > + 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): [ ... ] > + if self.is_event_constraint(key): > + res = self.__format_guard_rules(rules) + resets > + self.guards[key] = ";".join(res) > + else: > + self.invariants[key] = rules[0] [Severity: Medium] Are subsequent rules silently ignored here? When parsing state invariants with multiple rules separated by logical operators, this assignment only stores the first parsed rule and discards the rest. Does this mean the generated monitor might fail to enforce all specified invariants? [ ... ] > + def __find_inv_conflicts(self) -> tuple[set[tuple[int, > _EventConstraintKey]], > + set[tuple[int, > _StateConstraintKey]]]: > + """ > + Run a breadth first search from all states with an invariant. > + Find any conflicting constraints reachable from there, this can be > + another state with an invariant or an edge with a non-reset guard. > + Stop when we find a reset. > + > + Return the set of conflicting guards and invariants as tuples of > + conflicting state and constraint key. > + """ > + conflict_guards: set[tuple[int, _EventConstraintKey]] = set() > + conflict_invs: set[tuple[int, _StateConstraintKey]] = set() > + for start_idx in self.invariants: > + queue = deque([(start_idx, 0)]) # (state_idx, distance) > + env = self.__get_constraint_env(self.invariants[start_idx]) > + > + while queue: > + curr_idx, distance = queue.popleft() > + > + # Check state condition > + if curr_idx != start_idx and curr_idx in self.invariants: > + conflict_invs.add((start_idx, > _StateConstraintKey(curr_idx))) > + continue > + > + # Check if we should stop > + if distance > len(self.states): > + break > + if curr_idx != start_idx and distance > 1: > + continue [Severity: Medium] Does this condition prematurely stop the breadth-first search? The BFS algorithm appears designed to explore paths up to len(self.states) deep, but this check restricts the search to depth 1. Any paths longer than 1 edge are not explored, which might cause the generator to silently miss required invariant-to-guard conversions. > + > + for event_idx, next_state_name in > enumerate(self.function[curr_idx]): > + if next_state_name == self.invalid_state_str: > + continue > + curr_guard = self.guards.get((curr_idx, event_idx), "") > + if "reset" in curr_guard and env in curr_guard: > + continue [Severity: Medium] Could this naive substring search yield false positives? If env is a short string like "t", and curr_guard contains a reset for a completely different variable like "time_ns" or "limit", the substring check evaluates to true. This might wrongly signal that the target variable was reset, causing the conflict detection loop to skip generating necessary timer conversions. [ ... ] > + def __fill_setup_invariants_func(self) -> list[str]: > + buff = [] > + if not self.invariants: > + return [] > + > + buff.append( > +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}" > + for e in self.self_loop_reset_events] [Severity: High] Could this cause unintended timer restarts? Because the self_loop_reset_events set records events globally, if any self-loop occurs with this event name, the generated monitor bypasses the early return and restarts the invariant timer for the current state. This means a self-loop reset intended for state A might erroneously restart the timer in state B, masking potential timing violations. -- Sashiko AI review ยท https://sashiko.dev/#/patchset/[email protected]?part=4
