tools/verification/rvgen/rvgen/dot2k.py

Source file repositories/reference/linux-study-clean/tools/verification/rvgen/rvgen/dot2k.py

File Facts

System
Linux kernel
Corpus path
tools/verification/rvgen/rvgen/dot2k.py
Extension
.py
Size
25515 bytes
Lines
612
Domain
Support Tooling And Documentation
Bucket
tools
Inferred role
Support Tooling And Documentation: tools
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

#!/usr/bin/env python3
# SPDX-License-Identifier: GPL-2.0-only
#
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
#
# dot2k: transform dot files into a monitor for the Linux kernel.
#
# For further information, see:
#   Documentation/trace/rv/da_monitor_synthesis.rst

from collections import deque
from .dot2c import Dot2c
from .generator import Monitor
from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError


class dot2k(Monitor, Dot2c):
    template_dir = "dot2k"

    def __init__(self, file_path, MonitorType, extra_params={}):
        self.monitor_type = MonitorType
        Monitor.__init__(self, extra_params)
        Dot2c.__init__(self, file_path, extra_params.get("model_name"))
        self.enum_suffix = f"_{self.name}"
        self.enum_suffix = f"_{self.name}"
        self.monitor_class = extra_params["monitor_class"]

    def fill_monitor_type(self) -> str:
        buff = [ self.monitor_type.upper() ]
        buff += self._fill_timer_type()
        if self.monitor_type == "per_obj":
            buff.append("typedef /* XXX: define the target type */ *monitor_target;")
        return "\n".join(buff)

    def fill_tracepoint_handlers_skel(self) -> str:
        buff = []
        buff += self._fill_hybrid_definitions()
        for event in self.events:
            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
            buff.append("{")
            handle = "handle_event"
            if self.is_start_event(event):
                buff.append("\t/* XXX: validate that this event always leads to the initial state */")
                handle = "handle_start_event"
            elif self.is_start_run_event(event):
                buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
                handle = "handle_start_run_event"
            if self.monitor_type == "per_task":
                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
            elif self.monitor_type == "per_obj":
                buff.append("\tint id = /* XXX: how do I get the id? */;")
                buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
                buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
            else:
                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
            buff.append("}")
            buff.append("")
        return '\n'.join(buff)

    def fill_tracepoint_attach_probe(self) -> str:
        buff = []
        for event in self.events:
            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
        return '\n'.join(buff)

    def fill_tracepoint_detach_helper(self) -> str:
        buff = []
        for event in self.events:
            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")

Annotation

Implementation Notes