xref: /linux/tools/verification/rvgen/rvgen/dot2k.py (revision 0fc8f6200d2313278fbf4539bbab74677c685531)
1#!/usr/bin/env python3
2# SPDX-License-Identifier: GPL-2.0-only
3#
4# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
5#
6# dot2k: transform dot files into a monitor for the Linux kernel.
7#
8# For further information, see:
9#   Documentation/trace/rv/da_monitor_synthesis.rst
10
11from collections import deque
12from .dot2c import Dot2c
13from .generator import Monitor
14from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
15
16
17class dot2k(Monitor, Dot2c):
18    template_dir = "dot2k"
19
20    def __init__(self, file_path, MonitorType, extra_params={}):
21        self.monitor_type = MonitorType
22        Monitor.__init__(self, extra_params)
23        Dot2c.__init__(self, file_path, extra_params.get("model_name"))
24        self.enum_suffix = f"_{self.name}"
25        self.enum_suffix = f"_{self.name}"
26        self.monitor_class = extra_params["monitor_class"]
27
28    def fill_monitor_type(self) -> str:
29        buff = [ self.monitor_type.upper() ]
30        buff += self._fill_timer_type()
31        if self.monitor_type == "per_obj":
32            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
33        return "\n".join(buff)
34
35    def fill_tracepoint_handlers_skel(self) -> str:
36        buff = []
37        buff += self._fill_hybrid_definitions()
38        for event in self.events:
39            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
40            buff.append("{")
41            handle = "handle_event"
42            if self.is_start_event(event):
43                buff.append("\t/* XXX: validate that this event always leads to the initial state */")
44                handle = "handle_start_event"
45            elif self.is_start_run_event(event):
46                buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
47                handle = "handle_start_run_event"
48            if self.monitor_type == "per_task":
49                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
50                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
51            elif self.monitor_type == "per_obj":
52                buff.append("\tint id = /* XXX: how do I get the id? */;")
53                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
54                buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
55            else:
56                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
57            buff.append("}")
58            buff.append("")
59        return '\n'.join(buff)
60
61    def fill_tracepoint_attach_probe(self) -> str:
62        buff = []
63        for event in self.events:
64            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
65        return '\n'.join(buff)
66
67    def fill_tracepoint_detach_helper(self) -> str:
68        buff = []
69        for event in self.events:
70            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
71        return '\n'.join(buff)
72
73    def fill_model_h_header(self) -> list[str]:
74        buff = []
75        buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
76        buff.append("/*")
77        buff.append(f" * Automatically generated C representation of {self.name} automaton")
78        buff.append(" * For further information about this format, see kernel documentation:")
79        buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
80        buff.append(" */")
81        buff.append("")
82        buff.append(f"#define MONITOR_NAME {self.name}")
83        buff.append("")
84
85        return buff
86
87    def fill_model_h(self) -> str:
88        #
89        # Adjust the definition names
90        #
91        self.enum_states_def = f"states_{self.name}"
92        self.enum_events_def = f"events_{self.name}"
93        self.enum_envs_def = f"envs_{self.name}"
94        self.struct_automaton_def = f"automaton_{self.name}"
95        self.var_automaton_def = f"automaton_{self.name}"
96
97        buff = self.fill_model_h_header()
98        buff += self.format_model()
99
100        return '\n'.join(buff)
101
102    def _is_id_monitor(self) -> bool:
103        return self.monitor_type in ("per_task", "per_obj")
104
105    def fill_monitor_class_type(self) -> str:
106        if self._is_id_monitor():
107            return "DA_MON_EVENTS_ID"
108        return "DA_MON_EVENTS_IMPLICIT"
109
110    def fill_monitor_class(self) -> str:
111        if self._is_id_monitor():
112            return "da_monitor_id"
113        return "da_monitor"
114
115    def fill_tracepoint_args_skel(self, tp_type: str) -> str:
116        buff = []
117        tp_args_event = [
118                ("char *", "state"),
119                ("char *", "event"),
120                ("char *", "next_state"),
121                ("bool ",  "final_state"),
122                ]
123        tp_args_error = [
124                ("char *", "state"),
125                ("char *", "event"),
126                ]
127        tp_args_error_env = tp_args_error + [("char *", "env")]
128        tp_args_dict = {
129                "event": tp_args_event,
130                "error": tp_args_error,
131                "error_env": tp_args_error_env
132                }
133        tp_args_id = ("int ", "id")
134        tp_args = tp_args_dict[tp_type]
135        if self._is_id_monitor():
136            tp_args.insert(0, tp_args_id)
137        tp_proto_c = ", ".join([a + b for a, b in tp_args])
138        tp_args_c = ", ".join([b for a, b in tp_args])
139        buff.append(f"	     TP_PROTO({tp_proto_c}),")
140        buff.append(f"	     TP_ARGS({tp_args_c})")
141        return '\n'.join(buff)
142
143    def _fill_hybrid_definitions(self) -> list:
144        """Stub, not valid for deterministic automata"""
145        return []
146
147    def _fill_timer_type(self) -> list:
148        """Stub, not valid for deterministic automata"""
149        return []
150
151    def fill_main_c(self) -> str:
152        main_c = super().fill_main_c()
153
154        min_type = self.get_minimun_type()
155        nr_events = len(self.events)
156        monitor_type = self.fill_monitor_type()
157
158        main_c = main_c.replace("%%MIN_TYPE%%", min_type)
159        main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
160        main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
161        main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
162
163        return main_c
164
165class da2k(dot2k):
166    """Deterministic automata only"""
167    def __init__(self, *args, **kwargs):
168        super().__init__(*args, **kwargs)
169        if self.is_hybrid_automata():
170            raise AutomataError("Detected hybrid automaton, use the 'ha' class")
171
172class ha2k(dot2k):
173    """Hybrid automata only"""
174    def __init__(self, *args, **kwargs):
175        super().__init__(*args, **kwargs)
176        if not self.is_hybrid_automata():
177            raise AutomataError("Detected deterministic automaton, use the 'da' class")
178        self.trace_h = self._read_template_file("trace_hybrid.h")
179        self.__parse_constraints()
180
181    def fill_monitor_class_type(self) -> str:
182        if self._is_id_monitor():
183            return "HA_MON_EVENTS_ID"
184        return "HA_MON_EVENTS_IMPLICIT"
185
186    def fill_monitor_class(self) -> str:
187        """
188        Used for tracepoint classes, since they are shared we keep da
189        instead of ha (also for the ha specific tracepoints).
190        The tracepoint class is not visible to the tools.
191        """
192        return super().fill_monitor_class()
193
194    def __adjust_value(self, value: str | int, unit: str | None) -> str:
195        """Adjust the value in ns"""
196        try:
197            value = int(value)
198        except ValueError:
199            # it's a constant, a parameter or a function
200            if value.endswith("()"):
201                return value.replace("()", "(ha_mon)")
202            return value
203        match unit:
204            case "us":
205                value *= 10**3
206            case "ms":
207                value *= 10**6
208            case "s":
209                value *= 10**9
210        return str(value) + "ull"
211
212    def __parse_single_constraint(self, rule: dict, value: str) -> str:
213        return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}"
214
215    def __get_constraint_env(self, constr: str) -> str:
216        """Extract the second argument from an ha_ function"""
217        env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",")
218        assert env.rstrip(f"_{self.name}") in self.envs
219        return env
220
221    def __start_to_invariant_check(self, constr: str) -> str:
222        # by default assume the timer has ns expiration
223        env = self.__get_constraint_env(constr)
224        clock_type = "ns"
225        if self.env_types.get(env.rstrip(f"_{self.name}")) == "j":
226            clock_type = "jiffy"
227
228        return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)"
229
230    def __start_to_conv(self, constr: str) -> str:
231        """
232        Undo the storage conversion done by ha_start_timer_
233        """
234        return "ha_inv_to_guard" + constr[constr.find("("):]
235
236    def __parse_timer_constraint(self, rule: dict, value: str) -> str:
237        # by default assume the timer has ns expiration
238        clock_type = "ns"
239        if self.env_types.get(rule["env"]) == "j":
240            clock_type = "jiffy"
241
242        return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix},"
243                f" {value}, time_ns)")
244
245    def __format_guard_rules(self, rules: list[str]) -> list[str]:
246        """
247        Merge guard constraints as a single C return statement.
248        If the rules include a stored env, also check its validity.
249        Break lines in a best effort way that tries to keep readability.
250        """
251        if not rules:
252            return []
253
254        invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||"
255                          for env in self.env_stored if any(env in rule for rule in rules)]
256        if invalid_checks and len(rules) > 1:
257            rules[0] = "(" + rules[0]
258            rules[-1] = rules[-1] + ")"
259        rules = invalid_checks + rules
260
261        separator = "\n\t\t      " if sum(len(r) for r in rules) > 80 else " "
262        return ["res = " + separator.join(rules)]
263
264    def __validate_constraint(self, key: tuple[int, int] | int, constr: str,
265                              rule, reset) -> None:
266        # event constrains are tuples and allow both rules and reset
267        # state constraints are only used for expirations (e.g. clk<N)
268        if self.is_event_constraint(key):
269            if not rule and not reset:
270                raise AutomataError("Unrecognised event constraint "
271                                    f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
272            if rule and (rule["env"] in self.env_types and
273                         rule["env"] not in self.env_stored):
274                raise AutomataError("Clocks in hybrid automata always require a storage"
275                                    f" ({rule["env"]})")
276        else:
277            if not rule:
278                raise AutomataError("Unrecognised state constraint "
279                                    f"({self.states[key]}: {constr})")
280            if rule["env"] not in self.env_stored:
281                raise AutomataError("State constraints always require a storage "
282                                    f"({rule["env"]})")
283            if rule["op"] not in ["<", "<="]:
284                raise AutomataError("State constraints must be clock expirations like"
285                                    f" clk<N ({rule.string})")
286
287    def __parse_constraints(self) -> None:
288        self.guards: dict[_EventConstraintKey, str] = {}
289        self.invariants: dict[_StateConstraintKey, str] = {}
290        for key, constraint in self.constraints.items():
291            rules = []
292            resets = []
293            for c, sep in self._split_constraint_expr(constraint):
294                rule = self.constraint_rule.search(c)
295                reset = self.constraint_reset.search(c)
296                self.__validate_constraint(key, c, rule, reset)
297                if rule:
298                    value = rule["val"]
299                    value_len = len(rule["val"])
300                    unit = None
301                    if rule.groupdict().get("unit"):
302                        value_len += len(rule["unit"])
303                        unit = rule["unit"]
304                    c = c[:-(value_len)]
305                    value = self.__adjust_value(value, unit)
306                    if self.is_event_constraint(key):
307                        c = self.__parse_single_constraint(rule, value)
308                        if sep:
309                            c += f" {sep}"
310                    else:
311                        c = self.__parse_timer_constraint(rule, value)
312                    rules.append(c)
313                if reset:
314                    c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)"
315                    resets.append(c)
316            if self.is_event_constraint(key):
317                res = self.__format_guard_rules(rules) + resets
318                self.guards[key] = ";".join(res)
319            else:
320                self.invariants[key] = rules[0]
321
322    def __fill_verify_invariants_func(self) -> list[str]:
323        buff = []
324        if not self.invariants:
325            return []
326
327        buff.append(
328f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
329\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
330\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
331{{""")
332
333        _else = ""
334        for state, constr in sorted(self.invariants.items()):
335            check_str = self.__start_to_invariant_check(constr)
336            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
337            buff.append(f"\t\t{check_str};")
338            _else = "else "
339
340        buff.append("\treturn true;\n}\n")
341        return buff
342
343    def __fill_convert_inv_guard_func(self) -> list[str]:
344        buff = []
345        if not self.invariants:
346            return []
347
348        conflict_guards, conflict_invs = self.__find_inv_conflicts()
349        if not conflict_guards and not conflict_invs:
350            return []
351
352        buff.append(
353f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon,
354\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
355\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
356{{""")
357        buff.append("\tif (curr_state == next_state)\n\t\treturn;")
358
359        _else = ""
360        for state, constr in sorted(self.invariants.items()):
361            # a state with invariant can reach us without reset
362            # multiple conflicts must have the same invariant, otherwise we cannot
363            # know how to reset the value
364            conf_i = [start for start, end in conflict_invs if end == state]
365            # we can reach a guard without reset
366            conf_g = [e for s, e in conflict_guards if s == state]
367            if not conf_i and not conf_g:
368                continue
369            buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})")
370
371            buff.append(f"\t\t{self.__start_to_conv(constr)};")
372            _else = "else "
373
374        buff.append("}\n")
375        return buff
376
377    def __fill_verify_guards_func(self) -> list[str]:
378        buff = []
379        if not self.guards:
380            return []
381
382        buff.append(
383f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
384\t\t\t\t    enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
385\t\t\t\t    enum {self.enum_states_def} next_state, u64 time_ns)
386{{
387\tbool res = true;
388""")
389
390        _else = ""
391        for edge, constr in sorted(self.guards.items()):
392            buff.append(f"\t{_else}if (curr_state == "
393                        f"{self.states[edge[0]]}{self.enum_suffix} && "
394                        f"event == {self.events[edge[1]]}{self.enum_suffix})")
395            if constr.count(";") > 0:
396                buff[-1] += " {"
397            buff += [f"\t\t{c};" for c in constr.split(";")]
398            if constr.count(";") > 0:
399                _else = "} else "
400            else:
401                _else = "else "
402        if _else[0] == "}":
403            buff.append("\t}")
404        buff.append("\treturn res;\n}\n")
405        return buff
406
407    def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]],
408                                            set[tuple[int, _StateConstraintKey]]]:
409        """
410        Run a breadth first search from all states with an invariant.
411        Find any conflicting constraints reachable from there, this can be
412        another state with an invariant or an edge with a non-reset guard.
413        Stop when we find a reset.
414
415        Return the set of conflicting guards and invariants as tuples of
416        conflicting state and constraint key.
417        """
418        conflict_guards: set[tuple[int, _EventConstraintKey]] = set()
419        conflict_invs: set[tuple[int, _StateConstraintKey]] = set()
420        for start_idx in self.invariants:
421            queue = deque([(start_idx, 0)])  # (state_idx, distance)
422            env = self.__get_constraint_env(self.invariants[start_idx])
423
424            while queue:
425                curr_idx, distance = queue.popleft()
426
427                # Check state condition
428                if curr_idx != start_idx and curr_idx in self.invariants:
429                    conflict_invs.add((start_idx, _StateConstraintKey(curr_idx)))
430                    continue
431
432                # Check if we should stop
433                if distance > len(self.states):
434                    break
435                if curr_idx != start_idx and distance > 1:
436                    continue
437
438                for event_idx, next_state_name in enumerate(self.function[curr_idx]):
439                    if next_state_name == self.invalid_state_str:
440                        continue
441                    curr_guard = self.guards.get((curr_idx, event_idx), "")
442                    if "reset" in curr_guard and env in curr_guard:
443                        continue
444
445                    if env in curr_guard:
446                        conflict_guards.add((start_idx,
447                                             _EventConstraintKey(curr_idx, event_idx)))
448                        continue
449
450                    next_idx = self.states.index(next_state_name)
451                    queue.append((next_idx, distance + 1))
452
453        return conflict_guards, conflict_invs
454
455    def __fill_setup_invariants_func(self) -> list[str]:
456        buff = []
457        if not self.invariants:
458            return []
459
460        buff.append(
461f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
462\t\t\t\t       enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
463\t\t\t\t       enum {self.enum_states_def} next_state, u64 time_ns)
464{{""")
465
466        conditions = ["next_state == curr_state"]
467        conditions += [f"event != {e}{self.enum_suffix}"
468                       for e in self.self_loop_reset_events]
469        condition_str = " && ".join(conditions)
470        buff.append(f"\tif ({condition_str})\n\t\treturn;")
471
472        _else = ""
473        for state, constr in sorted(self.invariants.items()):
474            buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})")
475            buff.append(f"\t\t{constr};")
476            _else = "else "
477
478        for state in self.invariants:
479            buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})")
480            buff.append("\t\tha_cancel_timer(ha_mon);")
481
482        buff.append("}\n")
483        return buff
484
485    def __fill_constr_func(self) -> list[str]:
486        buff = []
487        if not self.constraints:
488            return []
489
490        buff.append(
491"""/*
492 * These functions are used to validate state transitions.
493 *
494 * They are generated by parsing the model, there is usually no need to change them.
495 * If the monitor requires a timer, there are functions responsible to arm it when
496 * the next state has a constraint, cancel it in any other case and to check
497 * that it didn't expire before the callback run. Transitions to the same state
498 * without a reset never affect timers.
499 * Due to the different representations between invariants and guards, there is
500 * a function to convert it in case invariants or guards are reachable from
501 * another invariant without reset. Those are not present if not required in
502 * the model. This is all automatic but is worth checking because it may show
503 * errors in the model (e.g. missing resets).
504 */""")
505
506        buff += self.__fill_verify_invariants_func()
507        inv_conflicts = self.__fill_convert_inv_guard_func()
508        buff += inv_conflicts
509        buff += self.__fill_verify_guards_func()
510        buff += self.__fill_setup_invariants_func()
511
512        buff.append(
513f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
514\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
515\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
516{{""")
517
518        if self.invariants:
519            buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
520                        "event, next_state, time_ns))\n\t\treturn false;\n")
521        if inv_conflicts:
522            buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, "
523                        "next_state, time_ns);\n")
524
525        if self.guards:
526            buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
527                        "next_state, time_ns))\n\t\treturn false;\n")
528
529        if self.invariants:
530            buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
531
532        buff.append("\treturn true;\n}\n")
533        return buff
534
535    def __fill_env_getter(self, env: str) -> str:
536        if env in self.env_types:
537            match self.env_types[env]:
538                case "ns" | "us" | "ms" | "s":
539                    return "ha_get_clk_ns(ha_mon, env, time_ns);"
540                case "j":
541                    return "ha_get_clk_jiffy(ha_mon, env);"
542        return f"/* XXX: how do I read {env}? */"
543
544    def __fill_env_resetter(self, env: str) -> str:
545        if env in self.env_types:
546            match self.env_types[env]:
547                case "ns" | "us" | "ms" | "s":
548                    return "ha_reset_clk_ns(ha_mon, env, time_ns);"
549                case "j":
550                    return "ha_reset_clk_jiffy(ha_mon, env);"
551        return f"/* XXX: how do I reset {env}? */"
552
553    def __fill_hybrid_get_reset_functions(self) -> list[str]:
554        buff = []
555        if self.is_hybrid_automata():
556            for var in self.constraint_vars:
557                if var.endswith("()"):
558                    func_name = var.replace("()", "")
559                    if func_name.isupper():
560                        buff.append(f"#define {func_name}(ha_mon) "
561                                    f"/* XXX: what is {func_name}(ha_mon)? */\n")
562                    else:
563                        buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{")
564                        buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;")
565                        buff.append("}\n")
566                elif var.isupper():
567                    buff.append(f"#define {var} /* XXX: what is {var}? */\n")
568                else:
569                    buff.append(f"static u64 {var} = /* XXX: default value */;")
570                    buff.append(f"module_param({var}, ullong, 0644);\n")
571            buff.append("""/*
572 * These functions define how to read and reset the environment variable.
573 *
574 * Common environment variables like ns-based and jiffy-based clocks have
575 * pre-define getters and resetters you can use. The parser can infer the type
576 * of the environment variable if you supply a measure unit in the constraint.
577 * If you define your own functions, make sure to add appropriate memory
578 * barriers if required.
579 * Some environment variables don't require a storage as they read a system
580 * state (e.g. preemption count). Those variables are never reset, so we don't
581 * define a reset function on monitors only relying on this type of variables.
582 */""")
583            buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, "
584                        f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
585            _else = ""
586            for env in self.envs:
587                buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
588                buff.append(f"\t\treturn {self.__fill_env_getter(env)}")
589                _else = "else "
590            buff.append("\treturn ENV_INVALID_VALUE;\n}\n")
591            if len(self.env_stored):
592                buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, "
593                            f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
594                _else = ""
595                for env in self.env_stored:
596                    buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
597                    buff.append(f"\t\t{self.__fill_env_resetter(env)}")
598                    _else = "else "
599                buff.append("}\n")
600        return buff
601
602    def _fill_hybrid_definitions(self) -> list[str]:
603        return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
604
605    def _fill_timer_type(self) -> list:
606        if self.invariants:
607            return [
608                    "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
609                    "#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
610                    ]
611        return []
612