+++ /dev/null
-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)/
+++ /dev/null
-#!/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)]
+++ /dev/null
-#!/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()
+++ /dev/null
-#!/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))
+++ /dev/null
-#!/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
-
- parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
- 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")
-
- subparsers = parser.add_subparsers(dest="subcmd", required=True)
-
- monitor_parser = subparsers.add_parser("monitor")
- monitor_parser.add_argument('-n', "--model_name", dest="model_name")
- monitor_parser.add_argument("-p", "--parent", dest="parent",
- required=False, help="Create a monitor nested to parent")
- monitor_parser.add_argument('-d', "--dot", dest="dot_file")
- monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
- help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
-
- container_parser = subparsers.add_parser("container")
- container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
-
- params = parser.parse_args()
-
- try:
- if params.subcmd == "monitor":
- print("Opening and parsing the dot file %s" % params.dot_file)
- monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
- else:
- monitor = dot2k(None, None, 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 params.subcmd == "monitor":
- 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())
+++ /dev/null
-#!/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("subcmd") == "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")
- self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
- 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 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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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)
+++ /dev/null
-# 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%%
+++ /dev/null
-config RV_MON_%%MODEL_NAME_UP%%
- depends on RV
- bool "%%MODEL_NAME%% monitor"
- help
- %%DESCRIPTION%%
+++ /dev/null
-// 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%%");
+++ /dev/null
-// 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%%");
+++ /dev/null
-/* SPDX-License-Identifier: GPL-2.0 */
-
-extern struct rv_monitor rv_%%MODEL_NAME%%;
+++ /dev/null
-/* 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%% */
--- /dev/null
+INSTALL=install
+
+prefix ?= /usr
+bindir ?= $(prefix)/bin
+mandir ?= $(prefix)/share/man
+miscdir ?= $(prefix)/share/rvgen
+srcdir ?= $(prefix)/src
+
+PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+clean:
+
+.PHONY: install
+install:
+ $(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py
+ $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py
+ $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
+ $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+ $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
+
+ mkdir -p ${miscdir}/
+ cp -rp dot2k_templates $(DESTDIR)$(miscdir)/
--- /dev/null
+#!/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 rvgen.dot2k import dot2k
+ import argparse
+ import sys
+
+ parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
+ 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")
+
+ subparsers = parser.add_subparsers(dest="subcmd", required=True)
+
+ monitor_parser = subparsers.add_parser("monitor")
+ monitor_parser.add_argument('-n', "--model_name", dest="model_name")
+ monitor_parser.add_argument("-p", "--parent", dest="parent",
+ required=False, help="Create a monitor nested to parent")
+ monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+ help="Monitor class, either \"da\" or \"ltl\"")
+ monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
+ monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
+ help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
+
+ container_parser = subparsers.add_parser("container")
+ container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+
+ params = parser.parse_args()
+
+ try:
+ if params.subcmd == "monitor":
+ print("Opening and parsing the specification file %s" % params.spec)
+ if params.monitor_class == "da":
+ monitor = dot2k(params.spec, params.monitor_type, vars(params))
+ elif params.monitor_class == "ltl":
+ raise NotImplementedError
+ else:
+ print("Unknown monitor class:", params.monitor_class)
+ sys.exit(1)
+ else:
+ monitor = dot2k(None, None, 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 params.subcmd == "monitor":
+ 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())
--- /dev/null
+#!/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 rvgen 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()
--- /dev/null
+# 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%%
--- /dev/null
+config RV_MON_%%MODEL_NAME_UP%%
+ depends on RV
+ bool "%%MODEL_NAME%% monitor"
+ help
+ %%DESCRIPTION%%
--- /dev/null
+// 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%%");
--- /dev/null
+// 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%%");
--- /dev/null
+/* SPDX-License-Identifier: GPL-2.0 */
+
+extern struct rv_monitor rv_%%MODEL_NAME%%;
--- /dev/null
+/* 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%% */
--- /dev/null
+#!/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)]
--- /dev/null
+#!/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 .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))
--- /dev/null
+#!/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 .dot2c import Dot2c
+import platform
+import os
+
+class dot2k(Dot2c):
+ monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
+ monitor_templates_dir = "rvgen/dot2k_templates/"
+ rv_dir = "kernel/trace/rv"
+ monitor_type = "per_cpu"
+
+ def __init__(self, file_path, MonitorType, extra_params={}):
+ self.container = extra_params.get("subcmd") == "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")
+ self.kconfig = self.__read_file(self.monitor_templates_dir + "Kconfig_container")
+ 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/rvgen/dot2k_templates/" % (platform.release())
+
+ if os.path.exists(kernel_path):
+ self.monitor_templates_dir = kernel_path
+ return
+
+ if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
+ self.monitor_templates_dir = "/usr/share/rvgen/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 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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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 '\n'.join(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)
projects / linux-block.git / commitdiff