xref: /linux/tools/verification/rvgen/rvgen/dot2k.py (revision 67f8bc848ee31831336bd478e57d2f993551902e)
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/monitor_synthesis.rst
10
11from .dot2c import Dot2c
12from .generator import Monitor
13from .automata import ConstraintCondition, AutomataError
14
15class dot2k(Monitor, Dot2c):
16    template_dir = "dot2k"
17
18    # only needed for the per-obj cleanup hook
19    cleanup_marker = "obj_cleanup"
20
21    def __init__(self, file_path, MonitorType, extra_params={}):
22        self.monitor_type = MonitorType
23        Monitor.__init__(self, extra_params)
24        Dot2c.__init__(self, file_path, extra_params.get("model_name"))
25        self.enum_suffix = f"_{self.name}"
26        self.enum_suffix = f"_{self.name}"
27        self.monitor_class = extra_params["monitor_class"]
28
29    def fill_monitor_type(self) -> str:
30        buff = [ self.monitor_type.upper() ]
31        buff += self._fill_timer_type()
32        if self.monitor_type == "per_obj":
33            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
34        return "\n".join(buff)
35
36    def fill_tracepoint_handlers_skel(self) -> str:
37        buff = []
38        buff += self._fill_hybrid_definitions()
39        for event in self.events:
40            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
41            buff.append("{")
42            handle = "handle_event"
43            if self.is_start_event(event):
44                buff.append("\t/* XXX: validate that this event always leads to the initial state */")
45                handle = "handle_start_event"
46            elif self.is_start_run_event(event):
47                buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
48                handle = "handle_start_run_event"
49            if self.monitor_type == "per_task":
50                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
51                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
52            elif self.monitor_type == "per_obj":
53                buff.append("\tint id = /* XXX: how do I get the id? */;")
54                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
55                buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
56            else:
57                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
58            buff.append("}")
59            buff.append("")
60        if self.monitor_type == "per_obj":
61            buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */")
62            buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)")
63            buff.append("{")
64            buff.append("\tint id = /* XXX: how do I get the id? */;")
65            buff.append("\tda_destroy_storage(id);")
66            buff.append("}")
67            buff.append("")
68        return '\n'.join(buff)
69
70    def fill_tracepoint_attach_probe(self) -> str:
71        buff = []
72        for event in self.events:
73            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
74        if self.monitor_type == "per_obj":
75            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
76        return '\n'.join(buff)
77
78    def fill_tracepoint_detach_helper(self) -> str:
79        buff = []
80        for event in self.events:
81            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
82        if self.monitor_type == "per_obj":
83            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});")
84        return '\n'.join(buff)
85
86    def fill_model_h_header(self) -> list[str]:
87        buff = []
88        buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
89        buff.append("/*")
90        buff.append(f" * Automatically generated C representation of {self.name} automaton")
91        buff.append(" * For further information about this format, see kernel documentation:")
92        buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
93        buff.append(" */")
94        buff.append("")
95        buff.append(f"#define MONITOR_NAME {self.name}")
96        buff.append("")
97
98        return buff
99
100    def fill_model_h(self) -> str:
101        #
102        # Adjust the definition names
103        #
104        self.enum_states_def = f"states_{self.name}"
105        self.enum_events_def = f"events_{self.name}"
106        self.enum_envs_def = f"envs_{self.name}"
107        self.struct_automaton_def = f"automaton_{self.name}"
108        self.var_automaton_def = f"automaton_{self.name}"
109
110        buff = self.fill_model_h_header()
111        buff += self.format_model()
112
113        return '\n'.join(buff)
114
115    def _is_id_monitor(self) -> bool:
116        return self.monitor_type in ("per_task", "per_obj")
117
118    def fill_monitor_class_type(self) -> str:
119        if self._is_id_monitor():
120            return "DA_MON_EVENTS_ID"
121        return "DA_MON_EVENTS_IMPLICIT"
122
123    def fill_monitor_class(self) -> str:
124        if self._is_id_monitor():
125            return "da_monitor_id"
126        return "da_monitor"
127
128    def fill_tracepoint_args_skel(self, tp_type: str) -> str:
129        buff = []
130        tp_args_event = [
131                ("char *", "state"),
132                ("char *", "event"),
133                ("char *", "next_state"),
134                ("bool ",  "final_state"),
135                ]
136        tp_args_error = [
137                ("char *", "state"),
138                ("char *", "event"),
139                ]
140        tp_args_error_env = tp_args_error + [("char *", "env")]
141        tp_args_dict = {
142                "event": tp_args_event,
143                "error": tp_args_error,
144                "error_env": tp_args_error_env
145                }
146        tp_args_id = ("int ", "id")
147        tp_args = tp_args_dict[tp_type]
148        if self._is_id_monitor():
149            tp_args.insert(0, tp_args_id)
150        tp_proto_c = ", ".join([a + b for a, b in tp_args])
151        tp_args_c = ", ".join([b for a, b in tp_args])
152        buff.append(f"	     TP_PROTO({tp_proto_c}),")
153        buff.append(f"	     TP_ARGS({tp_args_c})")
154        return '\n'.join(buff)
155
156    def _fill_hybrid_definitions(self) -> list:
157        """Stub, not valid for deterministic automata"""
158        return []
159
160    def _fill_timer_type(self) -> list:
161        """Stub, not valid for deterministic automata"""
162        return []
163
164    def fill_main_c(self) -> str:
165        main_c = super().fill_main_c()
166
167        min_type = self.get_minimun_type()
168        nr_events = len(self.events)
169        monitor_type = self.fill_monitor_type()
170
171        main_c = main_c.replace("%%MIN_TYPE%%", min_type)
172        main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events))
173        main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type)
174        main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class)
175
176        return main_c
177
178class da2k(dot2k):
179    """Deterministic automata only"""
180    def __init__(self, *args, **kwargs):
181        super().__init__(*args, **kwargs)
182        if self.is_hybrid_automata():
183            raise AutomataError("Detected hybrid automaton, use the 'ha' class")
184
185class ha2k(dot2k):
186    """Hybrid automata only"""
187    def __init__(self, *args, **kwargs):
188        super().__init__(*args, **kwargs)
189        if not self.is_hybrid_automata():
190            raise AutomataError("Detected deterministic automaton, use the 'da' class")
191        self.trace_h = self._read_template_file("trace_hybrid.h")
192        self.has_invariant = False
193        self.has_guard = False
194        for state in self.states:
195            if state.inv:
196                self.has_invariant = True
197        for transition in self.transitions:
198            if transition.rule or transition.reset:
199                self.has_guard = True
200
201    def fill_monitor_class_type(self) -> str:
202        if self._is_id_monitor():
203            return "HA_MON_EVENTS_ID"
204        return "HA_MON_EVENTS_IMPLICIT"
205
206    def fill_monitor_class(self) -> str:
207        """
208        Used for tracepoint classes, since they are shared we keep da
209        instead of ha (also for the ha specific tracepoints).
210        The tracepoint class is not visible to the tools.
211        """
212        return super().fill_monitor_class()
213
214    def __adjust_value(self, value: str | int, unit: str | None) -> str:
215        """Adjust the value in ns"""
216        try:
217            value = int(value)
218        except ValueError:
219            # it's a constant, a parameter or a function
220            if value.endswith("()"):
221                return value.replace("()", "(ha_mon)")
222            return value
223        match unit:
224            case "us":
225                value *= 10**3
226            case "ms":
227                value *= 10**6
228            case "s":
229                value *= 10**9
230        return str(value) + "ull"
231
232    def __parse_guard_rule(self, rule) -> list[str]:
233        buff = []
234        for c, sep in rule.rules:
235            env = c.env + self.enum_suffix
236            op = c.op
237            val = self.__adjust_value(c.val, c.unit)
238
239            cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}"
240            if sep:
241                cond += f" {sep}"
242            buff.append(cond)
243        return buff
244
245    def __start_to_invariant_check(self, inv: ConstraintCondition) -> str:
246        # by default assume the timer has ns expiration
247        clock_type = "ns"
248        if inv.unit == "j":
249            clock_type = "jiffy"
250
251        value = self.__adjust_value(inv.val, inv.unit)
252
253        return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})"
254
255    def __parse_invariant(self, inv):
256        # by default assume the timer has ns expiration
257        clock_type = "ns"
258        if inv.unit == "j":
259            clock_type = "jiffy"
260
261        env = inv.env + self.enum_suffix
262        try:
263            val = int(inv.val)
264        except ValueError:
265            # it's a constant, a parameter or a function
266            val = inv.val.replace("()", "(ha_mon)")
267
268        match inv.unit:
269            case "us":
270                val *= 10**3
271            case "ms":
272                val *= 10**6
273            case "s":
274                val *= 10**9
275
276        return (f"ha_start_timer_{clock_type}(ha_mon, {env},"
277                f" {val}, time_ns)")
278
279    def __format_guard_rules(self, rules: list[str]) -> list[str]:
280        """
281        Merge guard constraints as a single C return statement.
282        If the rules include a stored env, also check its validity.
283        Break lines in a best effort way that tries to keep readability.
284        """
285        if not rules:
286            return []
287
288        invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||"
289                          for env in self.env_stored if any(env in rule for rule in rules)]
290        if invalid_checks and len(rules) > 1:
291            rules[0] = "(" + rules[0]
292            rules[-1] = rules[-1] + ")"
293        rules = invalid_checks + rules
294
295        separator = "\n\t\t      " if sum(len(r) for r in rules) > 80 else " "
296        return ["res = " + separator.join(rules) + ";"]
297
298    def __fill_verify_invariants_func(self) -> list[str]:
299        if not self.has_invariant:
300            return []
301
302        buff = [
303f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon,
304\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
305\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns)
306{{"""]
307
308        _else = ""
309        for state in self.states:
310            if not state.inv:
311                continue
312
313            check_str = self.__start_to_invariant_check(state.inv)
314            buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})")
315            buff.append(f"\t\t{check_str};")
316            _else = "else "
317
318        buff.append("\treturn true;\n}\n")
319        return buff
320
321    def __fill_verify_guards_func(self) -> list[str]:
322        buff = []
323
324        if not self.has_guard:
325            return []
326
327        buff.append(
328f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon,
329\t\t\t\t    enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
330\t\t\t\t    enum {self.enum_states_def} next_state, u64 time_ns)
331{{
332\tbool res = true;
333""")
334
335        _else = ""
336        for transition in self.transitions:
337            if not transition.rule and not transition.reset:
338                continue
339
340            buff.append(f"\t{_else}if (curr_state == "
341                        f"{transition.src}{self.enum_suffix} && "
342                        f"event == {transition.event}{self.enum_suffix})")
343            rule = transition.rule
344            reset = transition.reset
345            if rule and reset:
346                buff[-1] += " {"
347            if rule:
348                buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0])
349            if reset:
350                buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);")
351            if rule and reset:
352                _else = "} else "
353            else:
354                _else = "else "
355        if _else[0] == "}":
356            buff.append("\t}")
357        buff.append("\treturn res;\n}\n")
358        return buff
359
360    def __fill_setup_invariants_func(self) -> list[str]:
361        if not self.has_invariant:
362            return []
363
364        buff = [
365f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon,
366\t\t\t\t       enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
367\t\t\t\t       enum {self.enum_states_def} next_state, u64 time_ns)
368{{"""]
369
370        conditions = ["next_state == curr_state"]
371        conditions += [f"event != {e}{self.enum_suffix}"
372                       for e in self.self_loop_reset_events]
373        condition_str = " && ".join(conditions)
374        buff.append(f"\tif ({condition_str})\n\t\treturn;")
375
376        _else = ""
377        for state in self.states:
378            inv = state.inv
379            if not inv:
380                continue
381            inv = self.__parse_invariant(inv)
382            buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})")
383            buff.append(f"\t\t{inv};")
384            _else = "else "
385
386        for state in self.states:
387            inv = state.inv
388            if not inv:
389                continue
390            buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})")
391            buff.append("\t\tha_cancel_timer(ha_mon);")
392
393        buff.append("}\n")
394        return buff
395
396    def __fill_constr_func(self) -> list[str]:
397        buff = []
398        if not self.has_invariant and not self.has_guard:
399            return []
400
401        buff.append(
402"""/*
403 * These functions are used to validate state transitions.
404 *
405 * They are generated by parsing the model, there is usually no need to change them.
406 * If the monitor requires a timer, there are functions responsible to arm it when
407 * the next state has a constraint, cancel it in any other case and to check
408 * that it didn't expire before the callback run. Transitions to the same state
409 * without a reset never affect timers.
410 */""")
411
412        buff += self.__fill_verify_invariants_func()
413        buff += self.__fill_verify_guards_func()
414        buff += self.__fill_setup_invariants_func()
415
416        buff.append(
417f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon,
418\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event,
419\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns)
420{{""")
421
422        if self.has_invariant:
423            buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, "
424                        "event, next_state, time_ns))\n\t\treturn false;\n")
425
426        if self.has_guard:
427            buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, "
428                        "next_state, time_ns))\n\t\treturn false;\n")
429
430        if self.has_invariant:
431            buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n")
432
433        buff.append("\treturn true;\n}\n")
434        return buff
435
436    def __fill_env_getter(self, env: str) -> str:
437        if env in self.env_types:
438            match self.env_types[env]:
439                case "ns" | "us" | "ms" | "s":
440                    return "ha_get_clk_ns(ha_mon, env, time_ns);"
441                case "j":
442                    return "ha_get_clk_jiffy(ha_mon, env);"
443        return f"/* XXX: how do I read {env}? */"
444
445    def __fill_env_resetter(self, env: str) -> str:
446        if env in self.env_types:
447            match self.env_types[env]:
448                case "ns" | "us" | "ms" | "s":
449                    return "ha_reset_clk_ns(ha_mon, env, time_ns);"
450                case "j":
451                    return "ha_reset_clk_jiffy(ha_mon, env);"
452        return f"/* XXX: how do I reset {env}? */"
453
454    def __fill_hybrid_get_reset_functions(self) -> list[str]:
455        buff = []
456        if self.is_hybrid_automata():
457            for var in self.constraint_vars:
458                if var.endswith("()"):
459                    func_name = var.replace("()", "")
460                    if func_name.isupper():
461                        buff.append(f"#define {func_name}(ha_mon) "
462                                    f"/* XXX: what is {func_name}(ha_mon)? */\n")
463                    else:
464                        buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{")
465                        buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;")
466                        buff.append("}\n")
467                elif var.isupper():
468                    buff.append(f"#define {var} /* XXX: what is {var}? */\n")
469                else:
470                    buff.append(f"static u64 {var} = /* XXX: default value */;")
471                    buff.append(f"module_param({var}, ullong, 0644);\n")
472            buff.append("""/*
473 * These functions define how to read and reset the environment variable.
474 *
475 * Common environment variables like ns-based and jiffy-based clocks have
476 * pre-define getters and resetters you can use. The parser can infer the type
477 * of the environment variable if you supply a measure unit in the constraint.
478 * If you define your own functions, make sure to add appropriate memory
479 * barriers if required.
480 * Some environment variables don't require a storage as they read a system
481 * state (e.g. preemption count). Those variables are never reset, so we don't
482 * define a reset function on monitors only relying on this type of variables.
483 */""")
484            buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, "
485                        f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
486            _else = ""
487            for env in self.envs:
488                buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
489                buff.append(f"\t\treturn {self.__fill_env_getter(env)}")
490                _else = "else "
491            buff.append("\treturn ENV_INVALID_VALUE;\n}\n")
492            if len(self.env_stored):
493                buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, "
494                            f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{")
495                _else = ""
496                for env in self.env_stored:
497                    buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})")
498                    buff.append(f"\t\t{self.__fill_env_resetter(env)}")
499                    _else = "else "
500                buff.append("}\n")
501        return buff
502
503    def _fill_hybrid_definitions(self) -> list[str]:
504        return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func()
505
506    def _fill_timer_type(self) -> list:
507        if self.has_invariant:
508            return [
509                    "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */",
510                    "#define HA_TIMER_TYPE HA_TIMER_HRTIMER"
511                    ]
512        return []
513