diff options
Diffstat (limited to 'tools/verification/dot2')
| -rw-r--r-- | tools/verification/dot2/Makefile | 26 | ||||
| -rw-r--r-- | tools/verification/dot2/automata.py | 206 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2c | 26 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2c.py | 254 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k | 53 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k.py | 389 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k_templates/Kconfig | 9 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k_templates/main.c | 91 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k_templates/main_container.c | 38 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k_templates/main_container.h | 3 | ||||
| -rw-r--r-- | tools/verification/dot2/dot2k_templates/trace.h | 13 |
11 files changed, 0 insertions, 1108 deletions
diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile deleted file mode 100644 index 021beb07a521..000000000000 --- a/tools/verification/dot2/Makefile +++ /dev/null @@ -1,26 +0,0 @@ -INSTALL=install - -prefix ?= /usr -bindir ?= $(prefix)/bin -mandir ?= $(prefix)/share/man -miscdir ?= $(prefix)/share/dot2 -srcdir ?= $(prefix)/src - -PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') - -.PHONY: all -all: - -.PHONY: clean -clean: - -.PHONY: install -install: - $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py - $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py - $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ - - mkdir -p ${miscdir}/ - cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/automata.py deleted file mode 100644 index d9a3fe2b74bf..000000000000 --- a/tools/verification/dot2/automata.py +++ /dev/null @@ -1,206 +0,0 @@ -#!/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> -# -# Automata object: parse an automata in dot file digraph format into a python object -# -# For further information, see: -# Documentation/trace/rv/deterministic_automata.rst - -import ntpath - -class Automata: - """Automata class: Reads a dot file and part it as an automata. - - Attributes: - dot_file: A dot file with an state_automaton definition. - """ - - invalid_state_str = "INVALID_STATE" - - def __init__(self, file_path, model_name=None): - self.__dot_path = file_path - self.name = model_name or self.__get_model_name() - self.__dot_lines = self.__open_dot() - self.states, self.initial_state, self.final_states = self.__get_state_variables() - self.events = self.__get_event_variables() - self.function = self.__create_matrix() - self.events_start, self.events_start_run = self.__store_init_events() - - def __get_model_name(self): - basename = ntpath.basename(self.__dot_path) - if not basename.endswith(".dot") and not basename.endswith(".gv"): - print("not a dot file") - raise Exception("not a dot file: %s" % self.__dot_path) - - model_name = ntpath.splitext(basename)[0] - if model_name.__len__() == 0: - raise Exception("not a dot file: %s" % self.__dot_path) - - return model_name - - def __open_dot(self): - cursor = 0 - dot_lines = [] - try: - dot_file = open(self.__dot_path) - except: - raise Exception("Cannot open the file: %s" % self.__dot_path) - - dot_lines = dot_file.read().splitlines() - dot_file.close() - - # checking the first line: - line = dot_lines[cursor].split() - - if (line[0] != "digraph") and (line[1] != "state_automaton"): - raise Exception("Not a valid .dot format: %s" % self.__dot_path) - else: - cursor += 1 - return dot_lines - - def __get_cursor_begin_states(self): - cursor = 0 - while self.__dot_lines[cursor].split()[0] != "{node": - cursor += 1 - return cursor - - def __get_cursor_begin_events(self): - cursor = 0 - while self.__dot_lines[cursor].split()[0] != "{node": - cursor += 1 - while self.__dot_lines[cursor].split()[0] == "{node": - cursor += 1 - # skip initial state transition - cursor += 1 - return cursor - - def __get_state_variables(self): - # wait for node declaration - states = [] - final_states = [] - - has_final_states = False - cursor = self.__get_cursor_begin_states() - - # process nodes - while self.__dot_lines[cursor].split()[0] == "{node": - line = self.__dot_lines[cursor].split() - raw_state = line[-1] - - # "enabled_fired"}; -> enabled_fired - state = raw_state.replace('"', '').replace('};', '').replace(',','_') - if state[0:7] == "__init_": - initial_state = state[7:] - else: - states.append(state) - if "doublecircle" in self.__dot_lines[cursor]: - final_states.append(state) - has_final_states = True - - if "ellipse" in self.__dot_lines[cursor]: - final_states.append(state) - has_final_states = True - - cursor += 1 - - states = sorted(set(states)) - states.remove(initial_state) - - # Insert the initial state at the bein og the states - states.insert(0, initial_state) - - if not has_final_states: - final_states.append(initial_state) - - return states, initial_state, final_states - - def __get_event_variables(self): - # here we are at the begin of transitions, take a note, we will return later. - cursor = self.__get_cursor_begin_events() - - events = [] - while self.__dot_lines[cursor].lstrip()[0] == '"': - # transitions have the format: - # "all_fired" -> "both_fired" [ label = "disable_irq" ]; - # ------------ event is here ------------^^^^^ - if self.__dot_lines[cursor].split()[1] == "->": - line = self.__dot_lines[cursor].split() - event = line[-2].replace('"','') - - # when a transition has more than one lables, they are like this - # "local_irq_enable\nhw_local_irq_enable_n" - # so split them. - - event = event.replace("\\n", " ") - for i in event.split(): - events.append(i) - cursor += 1 - - return sorted(set(events)) - - def __create_matrix(self): - # transform the array into a dictionary - events = self.events - states = self.states - events_dict = {} - states_dict = {} - nr_event = 0 - for event in events: - events_dict[event] = nr_event - nr_event += 1 - - nr_state = 0 - for state in states: - states_dict[state] = nr_state - nr_state += 1 - - # declare the matrix.... - matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)] - - # and we are back! Let's fill the matrix - cursor = self.__get_cursor_begin_events() - - while self.__dot_lines[cursor].lstrip()[0] == '"': - if self.__dot_lines[cursor].split()[1] == "->": - line = self.__dot_lines[cursor].split() - origin_state = line[0].replace('"','').replace(',','_') - dest_state = line[2].replace('"','').replace(',','_') - possible_events = line[-2].replace('"','').replace("\\n", " ") - for event in possible_events.split(): - matrix[states_dict[origin_state]][events_dict[event]] = dest_state - cursor += 1 - - return matrix - - def __store_init_events(self): - events_start = [False] * len(self.events) - events_start_run = [False] * len(self.events) - for i, _ in enumerate(self.events): - curr_event_will_init = 0 - curr_event_from_init = False - curr_event_used = 0 - for j, _ in enumerate(self.states): - if self.function[j][i] != self.invalid_state_str: - curr_event_used += 1 - if self.function[j][i] == self.initial_state: - curr_event_will_init += 1 - if self.function[0][i] != self.invalid_state_str: - curr_event_from_init = True - # this event always leads to init - if curr_event_will_init and curr_event_used == curr_event_will_init: - events_start[i] = True - # this event is only called from init - if curr_event_from_init and curr_event_used == 1: - events_start_run[i] = True - return events_start, events_start_run - - def is_start_event(self, event): - return self.events_start[self.events.index(event)] - - def is_start_run_event(self, event): - # prefer handle_start_event if there - if any(self.events_start): - return False - return self.events_start_run[self.events.index(event)] diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c deleted file mode 100644 index 3fe89ab88b65..000000000000 --- a/tools/verification/dot2/dot2c +++ /dev/null @@ -1,26 +0,0 @@ -#!/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> -# -# dot2c: parse an automata in dot file digraph format into a C -# -# This program was written in the development of this paper: -# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. -# "Efficient Formal Verification for the Linux Kernel." International -# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. -# -# For further information, see: -# Documentation/trace/rv/deterministic_automata.rst - -if __name__ == '__main__': - from dot2 import dot2c - import argparse - import sys - - parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure') - parser.add_argument('dot_file', help='The dot file to be converted') - - args = parser.parse_args() - d = dot2c.Dot2c(args.dot_file) - d.print_model_classic() diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2c.py deleted file mode 100644 index fa2816ac7b61..000000000000 --- a/tools/verification/dot2/dot2c.py +++ /dev/null @@ -1,254 +0,0 @@ -#!/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> -# -# dot2c: parse an automata in dot file digraph format into a C -# -# This program was written in the development of this paper: -# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. -# "Efficient Formal Verification for the Linux Kernel." International -# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. -# -# For further information, see: -# Documentation/trace/rv/deterministic_automata.rst - -from dot2.automata import Automata - -class Dot2c(Automata): - enum_suffix = "" - enum_states_def = "states" - enum_events_def = "events" - struct_automaton_def = "automaton" - var_automaton_def = "aut" - - def __init__(self, file_path, model_name=None): - super().__init__(file_path, model_name) - self.line_length = 100 - - def __buff_to_string(self, buff): - string = "" - - for line in buff: - string = string + line + "\n" - - # cut off the last \n - return string[:-1] - - def __get_enum_states_content(self): - buff = [] - buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix)) - for state in self.states: - if state != self.initial_state: - buff.append("\t%s%s," % (state, self.enum_suffix)) - buff.append("\tstate_max%s" % (self.enum_suffix)) - - return buff - - def get_enum_states_string(self): - buff = self.__get_enum_states_content() - return self.__buff_to_string(buff) - - def format_states_enum(self): - buff = [] - buff.append("enum %s {" % self.enum_states_def) - buff.append(self.get_enum_states_string()) - buff.append("};\n") - - return buff - - def __get_enum_events_content(self): - buff = [] - first = True - for event in self.events: - if first: - buff.append("\t%s%s = 0," % (event, self.enum_suffix)) - first = False - else: - buff.append("\t%s%s," % (event, self.enum_suffix)) - - buff.append("\tevent_max%s" % self.enum_suffix) - - return buff - - def get_enum_events_string(self): - buff = self.__get_enum_events_content() - return self.__buff_to_string(buff) - - def format_events_enum(self): - buff = [] - buff.append("enum %s {" % self.enum_events_def) - buff.append(self.get_enum_events_string()) - buff.append("};\n") - - return buff - - def get_minimun_type(self): - min_type = "unsigned char" - - if self.states.__len__() > 255: - min_type = "unsigned short" - - if self.states.__len__() > 65535: - min_type = "unsigned int" - - if self.states.__len__() > 1000000: - raise Exception("Too many states: %d" % self.states.__len__()) - - return min_type - - def format_automaton_definition(self): - min_type = self.get_minimun_type() - buff = [] - buff.append("struct %s {" % self.struct_automaton_def) - buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix)) - buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix)) - buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix)) - buff.append("\t%s initial_state;" % min_type) - buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix)) - buff.append("};\n") - return buff - - def format_aut_init_header(self): - buff = [] - buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def)) - return buff - - def __get_string_vector_per_line_content(self, buff): - first = True - string = "" - for entry in buff: - if first: - string = string + "\t\t\"" + entry - first = False; - else: - string = string + "\",\n\t\t\"" + entry - string = string + "\"" - - return string - - def get_aut_init_events_string(self): - return self.__get_string_vector_per_line_content(self.events) - - def get_aut_init_states_string(self): - return self.__get_string_vector_per_line_content(self.states) - - def format_aut_init_events_string(self): - buff = [] - buff.append("\t.event_names = {") - buff.append(self.get_aut_init_events_string()) - buff.append("\t},") - return buff - - def format_aut_init_states_string(self): - buff = [] - buff.append("\t.state_names = {") - buff.append(self.get_aut_init_states_string()) - buff.append("\t},") - - return buff - - def __get_max_strlen_of_states(self): - max_state_name = max(self.states, key = len).__len__() - return max(max_state_name, self.invalid_state_str.__len__()) - - def __get_state_string_length(self): - maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__() - return "%" + str(maxlen) + "s" - - def get_aut_init_function(self): - nr_states = self.states.__len__() - nr_events = self.events.__len__() - buff = [] - - strformat = self.__get_state_string_length() - - for x in range(nr_states): - line = "\t\t{ " - for y in range(nr_events): - next_state = self.function[x][y] - if next_state != self.invalid_state_str: - next_state = self.function[x][y] + self.enum_suffix - - if y != nr_events-1: - line = line + strformat % next_state + ", " - else: - line = line + strformat % next_state + " }," - buff.append(line) - - return self.__buff_to_string(buff) - - def format_aut_init_function(self): - buff = [] - buff.append("\t.function = {") - buff.append(self.get_aut_init_function()) - buff.append("\t},") - - return buff - - def get_aut_init_initial_state(self): - return self.initial_state - - def format_aut_init_initial_state(self): - buff = [] - initial_state = self.get_aut_init_initial_state() - buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",") - - return buff - - def get_aut_init_final_states(self): - line = "" - first = True - for state in self.states: - if first == False: - line = line + ', ' - else: - first = False - - if self.final_states.__contains__(state): - line = line + '1' - else: - line = line + '0' - return line - - def format_aut_init_final_states(self): - buff = [] - buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states()) - - return buff - - def __get_automaton_initialization_footer_string(self): - footer = "};\n" - return footer - - def format_aut_init_footer(self): - buff = [] - buff.append(self.__get_automaton_initialization_footer_string()) - - return buff - - def format_invalid_state(self): - buff = [] - buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix)) - - return buff - - def format_model(self): - buff = [] - buff += self.format_states_enum() - buff += self.format_invalid_state() - buff += self.format_events_enum() - buff += self.format_automaton_definition() - buff += self.format_aut_init_header() - buff += self.format_aut_init_states_string() - buff += self.format_aut_init_events_string() - buff += self.format_aut_init_function() - buff += self.format_aut_init_initial_state() - buff += self.format_aut_init_final_states() - buff += self.format_aut_init_footer() - - return buff - - def print_model_classic(self): - buff = self.format_model() - print(self.__buff_to_string(buff)) diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k deleted file mode 100644 index 767064f415e7..000000000000 --- a/tools/verification/dot2/dot2k +++ /dev/null @@ -1,53 +0,0 @@ -#!/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 - -if __name__ == '__main__': - from dot2.dot2k import dot2k - import argparse - import sys - - def is_container(): - """Should work even before parsing the arguments""" - return "-c" in sys.argv or "--container" in sys.argv - - parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') - parser.add_argument('-d', "--dot", dest="dot_file", required=not is_container()) - parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=not is_container(), - help=f"Available options: {', '.join(dot2k.monitor_types.keys())}") - parser.add_argument('-n', "--model_name", dest="model_name", required=is_container()) - parser.add_argument("-D", "--description", dest="description", required=False) - parser.add_argument("-a", "--auto_patch", dest="auto_patch", - action="store_true", required=False, - help="Patch the kernel in place") - parser.add_argument("-p", "--parent", dest="parent", - required=False, help="Create a monitor nested to parent") - parser.add_argument("-c", "--container", dest="container", - action="store_true", required=False, - help="Create an empty monitor to be used as a container") - params = parser.parse_args() - - if not is_container(): - print("Opening and parsing the dot file %s" % params.dot_file) - try: - monitor=dot2k(params.dot_file, params.monitor_type, vars(params)) - except Exception as e: - print('Error: '+ str(e)) - print("Sorry : :-(") - sys.exit(1) - - print("Writing the monitor into the directory %s" % monitor.name) - monitor.print_files() - print("Almost done, checklist") - if not is_container(): - print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) - print(monitor.fill_tracepoint_tooltip()) - print(monitor.fill_makefile_tooltip()) - print(monitor.fill_kconfig_tooltip()) - print(monitor.fill_monitor_tooltip()) diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py deleted file mode 100644 index 745d35a4a379..000000000000 --- a/tools/verification/dot2/dot2k.py +++ /dev/null @@ -1,389 +0,0 @@ -#!/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 dot2.dot2c import Dot2c -import platform -import os - -class dot2k(Dot2c): - monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir = "dot2/dot2k_templates/" - rv_dir = "kernel/trace/rv" - monitor_type = "per_cpu" - - def __init__(self, file_path, MonitorType, extra_params={}): - self.container = extra_params.get("container") - self.parent = extra_params.get("parent") - self.__fill_rv_templates_dir() - - if self.container: - if file_path: - raise ValueError("A container does not require a dot file") - if MonitorType: - raise ValueError("A container does not require a monitor type") - if self.parent: - raise ValueError("A container cannot have a parent") - self.name = extra_params.get("model_name") - self.events = [] - self.states = [] - self.main_c = self.__read_file(self.monitor_templates_dir + "main_container.c") - self.main_h = self.__read_file(self.monitor_templates_dir + "main_container.h") - else: - super().__init__(file_path, extra_params.get("model_name")) - - self.monitor_type = self.monitor_types.get(MonitorType) - if self.monitor_type is None: - raise ValueError("Unknown monitor type: %s" % MonitorType) - self.monitor_type = MonitorType - self.main_c = self.__read_file(self.monitor_templates_dir + "main.c") - self.trace_h = self.__read_file(self.monitor_templates_dir + "trace.h") - self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig") - self.enum_suffix = "_%s" % self.name - self.description = extra_params.get("description", self.name) or "auto-generated" - self.auto_patch = extra_params.get("auto_patch") - if self.auto_patch: - self.__fill_rv_kernel_dir() - - def __fill_rv_templates_dir(self): - - if os.path.exists(self.monitor_templates_dir): - return - - if platform.system() != "Linux": - raise OSError("I can only run on Linux.") - - kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release()) - - if os.path.exists(kernel_path): - self.monitor_templates_dir = kernel_path - return - - if os.path.exists("/usr/share/dot2/dot2k_templates/"): - self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/" - return - - raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?") - - def __fill_rv_kernel_dir(self): - - # first try if we are running in the kernel tree root - if os.path.exists(self.rv_dir): - return - - # offset if we are running inside the kernel tree from verification/dot2 - kernel_path = os.path.join("../..", self.rv_dir) - - if os.path.exists(kernel_path): - self.rv_dir = kernel_path - return - - if platform.system() != "Linux": - raise OSError("I can only run on Linux.") - - kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir) - - # if the current kernel is from a distro this may not be a full kernel tree - # verify that one of the files we are going to modify is available - if os.path.exists(os.path.join(kernel_path, "rv_trace.h")): - self.rv_dir = kernel_path - return - - raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") - - def __read_file(self, path): - try: - fd = open(path, 'r') - except OSError: - raise Exception("Cannot open the file: %s" % path) - - content = fd.read() - - fd.close() - return content - - def __buff_to_string(self, buff): - string = "" - - for line in buff: - string = string + line + "\n" - - # cut off the last \n - return string[:-1] - - def fill_monitor_type(self): - return self.monitor_type.upper() - - def fill_parent(self): - return "&rv_%s" % self.parent if self.parent else "NULL" - - def fill_include_parent(self): - if self.parent: - return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent) - return "" - - def fill_tracepoint_handlers_skel(self): - buff = [] - for event in self.events: - buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) - 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("\tda_%s_%s(p, %s%s);" % (handle, self.name, event, self.enum_suffix)); - else: - buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix)); - buff.append("}") - buff.append("") - return self.__buff_to_string(buff) - - def fill_tracepoint_attach_probe(self): - buff = [] - for event in self.events: - buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) - - def fill_tracepoint_detach_helper(self): - buff = [] - for event in self.events: - buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) - - def fill_main_c(self): - main_c = self.main_c - monitor_type = self.fill_monitor_type() - min_type = self.get_minimun_type() - nr_events = len(self.events) - tracepoint_handlers = self.fill_tracepoint_handlers_skel() - tracepoint_attach = self.fill_tracepoint_attach_probe() - tracepoint_detach = self.fill_tracepoint_detach_helper() - parent = self.fill_parent() - parent_include = self.fill_include_parent() - - main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) - main_c = main_c.replace("%%MIN_TYPE%%", min_type) - main_c = main_c.replace("%%MODEL_NAME%%", self.name) - main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) - main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers) - main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach) - main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach) - main_c = main_c.replace("%%DESCRIPTION%%", self.description) - main_c = main_c.replace("%%PARENT%%", parent) - main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include) - - return main_c - - def fill_model_h_header(self): - buff = [] - buff.append("/* SPDX-License-Identifier: GPL-2.0 */") - buff.append("/*") - buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) - buff.append(" * For further information about this format, see kernel documentation:") - buff.append(" * Documentation/trace/rv/deterministic_automata.rst") - buff.append(" */") - buff.append("") - - return buff - - def fill_model_h(self): - # - # Adjust the definition names - # - self.enum_states_def = "states_%s" % self.name - self.enum_events_def = "events_%s" % self.name - self.struct_automaton_def = "automaton_%s" % self.name - self.var_automaton_def = "automaton_%s" % self.name - - buff = self.fill_model_h_header() - buff += self.format_model() - - return self.__buff_to_string(buff) - - def fill_monitor_class_type(self): - if self.monitor_type == "per_task": - return "DA_MON_EVENTS_ID" - return "DA_MON_EVENTS_IMPLICIT" - - def fill_monitor_class(self): - if self.monitor_type == "per_task": - return "da_monitor_id" - return "da_monitor" - - def fill_tracepoint_args_skel(self, tp_type): - buff = [] - tp_args_event = [ - ("char *", "state"), - ("char *", "event"), - ("char *", "next_state"), - ("bool ", "final_state"), - ] - tp_args_error = [ - ("char *", "state"), - ("char *", "event"), - ] - tp_args_id = ("int ", "id") - tp_args = tp_args_event if tp_type == "event" else tp_args_error - if self.monitor_type == "per_task": - tp_args.insert(0, tp_args_id) - tp_proto_c = ", ".join([a+b for a,b in tp_args]) - tp_args_c = ", ".join([b for a,b in tp_args]) - buff.append(" TP_PROTO(%s)," % tp_proto_c) - buff.append(" TP_ARGS(%s)" % tp_args_c) - return self.__buff_to_string(buff) - - def fill_monitor_deps(self): - buff = [] - buff.append(" # XXX: add dependencies if there") - if self.parent: - buff.append(" depends on RV_MON_%s" % self.parent.upper()) - buff.append(" default y") - return self.__buff_to_string(buff) - - def fill_trace_h(self): - trace_h = self.trace_h - monitor_class = self.fill_monitor_class() - monitor_class_type = self.fill_monitor_class_type() - tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") - tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") - trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) - trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) - trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) - trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) - trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) - trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) - return trace_h - - def fill_kconfig(self): - kconfig = self.kconfig - monitor_class_type = self.fill_monitor_class_type() - monitor_deps = self.fill_monitor_deps() - kconfig = kconfig.replace("%%MODEL_NAME%%", self.name) - kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper()) - kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) - kconfig = kconfig.replace("%%DESCRIPTION%%", self.description) - kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) - return kconfig - - def fill_main_container_h(self): - main_h = self.main_h - main_h = main_h.replace("%%MODEL_NAME%%", self.name) - return main_h - - def __patch_file(self, file, marker, line): - file_to_patch = os.path.join(self.rv_dir, file) - content = self.__read_file(file_to_patch) - content = content.replace(marker, line + "\n" + marker) - self.__write_file(file_to_patch, content) - - def fill_tracepoint_tooltip(self): - monitor_class_type = self.fill_monitor_class_type() - if self.auto_patch: - self.__patch_file("rv_trace.h", - "// Add new monitors based on CONFIG_%s here" % monitor_class_type, - "#include <monitors/%s/%s_trace.h>" % (self.name, self.name)) - return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir - - return """ - Edit %s/rv_trace.h: -Add this line where other tracepoints are included and %s is defined: -#include <monitors/%s/%s_trace.h> -""" % (self.rv_dir, monitor_class_type, self.name, self.name) - - def fill_kconfig_tooltip(self): - if self.auto_patch: - self.__patch_file("Kconfig", - "# Add new monitors here", - "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name)) - return " - Patching %s/Kconfig, double check the result" % self.rv_dir - - return """ - Edit %s/Kconfig: -Add this line where other monitors are included: -source \"kernel/trace/rv/monitors/%s/Kconfig\" -""" % (self.rv_dir, self.name) - - def fill_makefile_tooltip(self): - name = self.name - name_up = name.upper() - if self.auto_patch: - self.__patch_file("Makefile", - "# Add new monitors here", - "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name)) - return " - Patching %s/Makefile, double check the result" % self.rv_dir - - return """ - Edit %s/Makefile: -Add this line where other monitors are included: -obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o -""" % (self.rv_dir, name_up, name, name) - - def fill_monitor_tooltip(self): - if self.auto_patch: - return " - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name) - return " - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir) - - def __create_directory(self): - path = self.name - if self.auto_patch: - path = os.path.join(self.rv_dir, "monitors", path) - try: - os.mkdir(path) - except FileExistsError: - return - except: - print("Fail creating the output dir: %s" % self.name) - - def __write_file(self, file_name, content): - try: - file = open(file_name, 'w') - except: - print("Fail writing to file: %s" % file_name) - - file.write(content) - - file.close() - - def __create_file(self, file_name, content): - path = "%s/%s" % (self.name, file_name) - if self.auto_patch: - path = os.path.join(self.rv_dir, "monitors", path) - self.__write_file(path, content) - - def __get_main_name(self): - path = "%s/%s" % (self.name, "main.c") - if not os.path.exists(path): - return "main.c" - return "__main.c" - - def print_files(self): - main_c = self.fill_main_c() - - self.__create_directory() - - path = "%s.c" % self.name - self.__create_file(path, main_c) - - if self.container: - main_h = self.fill_main_container_h() - path = "%s.h" % self.name - self.__create_file(path, main_h) - else: - model_h = self.fill_model_h() - path = "%s.h" % self.name - self.__create_file(path, model_h) - - trace_h = self.fill_trace_h() - path = "%s_trace.h" % self.name - self.__create_file(path, trace_h) - - kconfig = self.fill_kconfig() - self.__create_file("Kconfig", kconfig) diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/dot2/dot2k_templates/Kconfig deleted file mode 100644 index 291b29ea28db..000000000000 --- a/tools/verification/dot2/dot2k_templates/Kconfig +++ /dev/null @@ -1,9 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-only -# -config RV_MON_%%MODEL_NAME_UP%% - depends on RV -%%MONITOR_DEPS%% - select %%MONITOR_CLASS_TYPE%% - bool "%%MODEL_NAME%% monitor" - help - %%DESCRIPTION%% diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/dot2/dot2k_templates/main.c deleted file mode 100644 index 83044a20c89a..000000000000 --- a/tools/verification/dot2/dot2k_templates/main.c +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "%%MODEL_NAME%%" - -/* - * XXX: include required tracepoint headers, e.g., - * #include <trace/events/sched.h> - */ -#include <rv_trace.h> -%%INCLUDE_PARENT%% -/* - * This is the self-generated part of the monitor. Generally, there is no need - * to touch this section. - */ -#include "%%MODEL_NAME%%.h" - -/* - * Declare the deterministic automata monitor. - * - * The rv monitor reference is needed for the monitor declaration. - */ -static struct rv_monitor rv_%%MODEL_NAME%%; -DECLARE_DA_MON_%%MONITOR_TYPE%%(%%MODEL_NAME%%, %%MIN_TYPE%%); - -/* - * This is the instrumentation part of the monitor. - * - * This is the section where manual work is required. Here the kernel events - * are translated into model's event. - * - */ -%%TRACEPOINT_HANDLERS_SKEL%% -static int enable_%%MODEL_NAME%%(void) -{ - int retval; - - retval = da_monitor_init_%%MODEL_NAME%%(); - if (retval) - return retval; - -%%TRACEPOINT_ATTACH%% - - return 0; -} - -static void disable_%%MODEL_NAME%%(void) -{ - rv_%%MODEL_NAME%%.enabled = 0; - -%%TRACEPOINT_DETACH%% - - da_monitor_destroy_%%MODEL_NAME%%(); -} - -/* - * This is the monitor register section. - */ -static struct rv_monitor rv_%%MODEL_NAME%% = { - .name = "%%MODEL_NAME%%", - .description = "%%DESCRIPTION%%", - .enable = enable_%%MODEL_NAME%%, - .disable = disable_%%MODEL_NAME%%, - .reset = da_monitor_reset_all_%%MODEL_NAME%%, - .enabled = 0, -}; - -static int __init register_%%MODEL_NAME%%(void) -{ - rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); - return 0; -} - -static void __exit unregister_%%MODEL_NAME%%(void) -{ - rv_unregister_monitor(&rv_%%MODEL_NAME%%); -} - -module_init(register_%%MODEL_NAME%%); -module_exit(unregister_%%MODEL_NAME%%); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/dot2/dot2k_templates/main_container.c deleted file mode 100644 index 89fc17cf8958..000000000000 --- a/tools/verification/dot2/dot2k_templates/main_container.c +++ /dev/null @@ -1,38 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> - -#define MODULE_NAME "%%MODEL_NAME%%" - -#include "%%MODEL_NAME%%.h" - -struct rv_monitor rv_%%MODEL_NAME%%; - -struct rv_monitor rv_%%MODEL_NAME%% = { - .name = "%%MODEL_NAME%%", - .description = "%%DESCRIPTION%%", - .enable = NULL, - .disable = NULL, - .reset = NULL, - .enabled = 0, -}; - -static int __init register_%%MODEL_NAME%%(void) -{ - rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); - return 0; -} - -static void __exit unregister_%%MODEL_NAME%%(void) -{ - rv_unregister_monitor(&rv_%%MODEL_NAME%%); -} - -module_init(register_%%MODEL_NAME%%); -module_exit(unregister_%%MODEL_NAME%%); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/dot2/dot2k_templates/main_container.h deleted file mode 100644 index 0f6883ab4bcc..000000000000 --- a/tools/verification/dot2/dot2k_templates/main_container.h +++ /dev/null @@ -1,3 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ - -extern struct rv_monitor rv_%%MODEL_NAME%%; diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/dot2/dot2k_templates/trace.h deleted file mode 100644 index 87d3a1308926..000000000000 --- a/tools/verification/dot2/dot2k_templates/trace.h +++ /dev/null @@ -1,13 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ - -/* - * Snippet to be included in rv_trace.h - */ - -#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% -DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, -%%TRACEPOINT_ARGS_SKEL_EVENT%%); - -DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, -%%TRACEPOINT_ARGS_SKEL_ERROR%%); -#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ |