diff options
Diffstat (limited to 'tools/verification')
43 files changed, 3167 insertions, 970 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.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 559ba191a1f6..000000000000 --- a/tools/verification/dot2/dot2k +++ /dev/null @@ -1,44 +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 ntpath - import os - import platform - import sys - - parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') - parser.add_argument('-d', "--dot", dest="dot_file", required=True) - parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True) - parser.add_argument('-n', "--model_name", dest="model_name", required=False) - 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") - params = parser.parse_args() - - 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") - 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 7547eb290b7d..000000000000 --- a/tools/verification/dot2/dot2k.py +++ /dev/null @@ -1,341 +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={}): - 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.__fill_rv_templates_dir() - 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_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() - - 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) - - return main_c - - def fill_model_h_header(self): - buff = [] - 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_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() - 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) - return kconfig - - 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() - model_h = self.fill_model_h() - - self.__create_directory() - - path = "%s.c" % self.name - self.__create_file(path, main_c) - - 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/models/deadline/nomiss.dot b/tools/verification/models/deadline/nomiss.dot new file mode 100644 index 000000000000..fd1ea6bf2509 --- /dev/null +++ b/tools/verification/models/deadline/nomiss.dot @@ -0,0 +1,41 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "idle"}; + {node [shape = plaintext, style=invis, label=""] "__init_ready"}; + {node [shape = doublecircle] "ready"}; + {node [shape = circle] "ready"}; + {node [shape = circle] "running"}; + {node [shape = circle] "sleeping"}; + {node [shape = circle] "throttled"}; + "__init_ready" -> "ready"; + "idle" [label = "idle"]; + "idle" -> "idle" [ label = "dl_server_idle" ]; + "idle" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "idle" -> "running" [ label = "sched_switch_in" ]; + "idle" -> "sleeping" [ label = "dl_server_stop" ]; + "idle" -> "throttled" [ label = "dl_throttle" ]; + "ready" [label = "ready\nclk < DEADLINE_NS()", color = green3]; + "ready" -> "idle" [ label = "dl_server_idle" ]; + "ready" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "ready" -> "running" [ label = "sched_switch_in" ]; + "ready" -> "sleeping" [ label = "dl_server_stop" ]; + "ready" -> "throttled" [ label = "dl_throttle;is_defer == 1" ]; + "running" [label = "running\nclk < DEADLINE_NS()"]; + "running" -> "idle" [ label = "dl_server_idle" ]; + "running" -> "running" [ label = "dl_replenish;reset(clk)\nsched_switch_in\nsched_wakeup" ]; + "running" -> "sleeping" [ label = "sched_switch_suspend\ndl_server_stop" ]; + "running" -> "throttled" [ label = "dl_throttle" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "sleeping" -> "running" [ label = "sched_switch_in" ]; + "sleeping" -> "sleeping" [ label = "dl_server_stop\ndl_server_idle" ]; + "sleeping" -> "throttled" [ label = "dl_throttle;is_constr_dl == 1 || is_defer == 1" ]; + "throttled" [label = "throttled"]; + "throttled" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "throttled" -> "throttled" [ label = "sched_switch_suspend\nsched_wakeup\ndl_server_idle\ndl_throttle" ]; + { rank = min ; + "__init_ready"; + "ready"; + } +} diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000000..d7ce62102733 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT) diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl new file mode 100644 index 000000000000..6f26c4810f78 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,23 @@ +RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) + and ((not WAKE) until RT_FRIENDLY_WAKE) + +RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + or EPOLL_WAIT + +RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI) + +RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + or KTHREAD_SHOULD_STOP + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI + or TASK_IS_RCU + or TASK_IS_MIGRATION diff --git a/tools/verification/models/sched/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000000..77bb64669416 --- /dev/null +++ b/tools/verification/models/sched/nrp.dot @@ -0,0 +1,29 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = doublecircle] "any_thread_running"}; + {node [shape = circle] "any_thread_running"}; + {node [shape = circle] "nested_preempt"}; + {node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"}; + {node [shape = circle] "preempt_irq"}; + {node [shape = circle] "rescheduling"}; + "__init_preempt_irq" -> "preempt_irq"; + "any_thread_running" [label = "any_thread_running", color = green3]; + "any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ]; + "any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ]; + "nested_preempt" [label = "nested_preempt"]; + "nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "nested_preempt" -> "nested_preempt" [ label = "irq_entry" ]; + "nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ]; + "preempt_irq" [label = "preempt_irq"]; + "preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ]; + "rescheduling" [label = "rescheduling"]; + "rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "rescheduling" -> "preempt_irq" [ label = "irq_entry" ]; + "rescheduling" -> "rescheduling" [ label = "sched_need_resched" ]; + { rank = min ; + "__init_preempt_irq"; + "preempt_irq"; + } +} diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot new file mode 100644 index 000000000000..511051fce430 --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,13 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_any"}; + {node [shape = doublecircle] "any"}; + "__init_any" -> "any"; + "any" [label = "any", color = green3]; + "any" -> "any" [ label = "sched_need_resched;irq_off == 1\nsched_waking;irq_off == 1 && preempt_off == 1" ]; + { rank = min ; + "__init_any"; + "any"; + } +} diff --git a/tools/verification/models/sched/sco.dot b/tools/verification/models/sched/sco.dot new file mode 100644 index 000000000000..20b0e3b449a6 --- /dev/null +++ b/tools/verification/models/sched/sco.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "scheduling_context"}; + {node [shape = plaintext, style=invis, label=""] "__init_thread_context"}; + {node [shape = ellipse] "thread_context"}; + {node [shape = plaintext] "thread_context"}; + "__init_thread_context" -> "thread_context"; + "scheduling_context" [label = "scheduling_context"]; + "scheduling_context" -> "thread_context" [ label = "schedule_exit" ]; + "thread_context" [label = "thread_context", color = green3]; + "thread_context" -> "scheduling_context" [ label = "schedule_entry" ]; + "thread_context" -> "thread_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_thread_context"; + "thread_context"; + } +} diff --git a/tools/verification/models/sched/scpd.dot b/tools/verification/models/sched/scpd.dot new file mode 100644 index 000000000000..340413896765 --- /dev/null +++ b/tools/verification/models/sched/scpd.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "can_sched"}; + {node [shape = plaintext, style=invis, label=""] "__init_cant_sched"}; + {node [shape = ellipse] "cant_sched"}; + {node [shape = plaintext] "cant_sched"}; + "__init_cant_sched" -> "cant_sched"; + "can_sched" [label = "can_sched"]; + "can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ]; + "can_sched" -> "cant_sched" [ label = "preempt_enable" ]; + "cant_sched" [label = "cant_sched", color = green3]; + "cant_sched" -> "can_sched" [ label = "preempt_disable" ]; + { rank = min ; + "__init_cant_sched"; + "cant_sched"; + } +} diff --git a/tools/verification/models/sched/snep.dot b/tools/verification/models/sched/snep.dot new file mode 100644 index 000000000000..fe1300e93f21 --- /dev/null +++ b/tools/verification/models/sched/snep.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"}; + {node [shape = ellipse] "non_scheduling_context"}; + {node [shape = plaintext] "non_scheduling_context"}; + {node [shape = plaintext] "scheduling_contex"}; + "__init_non_scheduling_context" -> "non_scheduling_context"; + "non_scheduling_context" [label = "non_scheduling_context", color = green3]; + "non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ]; + "non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ]; + "scheduling_contex" [label = "scheduling_contex"]; + "scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ]; + { rank = min ; + "__init_non_scheduling_context"; + "non_scheduling_context"; + } +} diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot new file mode 100644 index 000000000000..8b71c32d4dca --- /dev/null +++ b/tools/verification/models/sched/snroc.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_other_context"}; + {node [shape = ellipse] "other_context"}; + {node [shape = plaintext] "other_context"}; + {node [shape = plaintext] "own_context"}; + "__init_other_context" -> "other_context"; + "other_context" [label = "other_context", color = green3]; + "other_context" -> "own_context" [ label = "sched_switch_in" ]; + "own_context" [label = "own_context"]; + "own_context" -> "other_context" [ label = "sched_switch_out" ]; + "own_context" -> "own_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_other_context"; + "other_context"; + } +} diff --git a/tools/verification/models/sched/sssw.dot b/tools/verification/models/sched/sssw.dot new file mode 100644 index 000000000000..4994c3e876be --- /dev/null +++ b/tools/verification/models/sched/sssw.dot @@ -0,0 +1,30 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_runnable"}; + {node [shape = doublecircle] "runnable"}; + {node [shape = circle] "runnable"}; + {node [shape = circle] "signal_wakeup"}; + {node [shape = circle] "sleepable"}; + {node [shape = circle] "sleeping"}; + "__init_runnable" -> "runnable"; + "runnable" [label = "runnable", color = green3]; + "runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ]; + "runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "runnable" -> "sleeping" [ label = "sched_switch_blocking" ]; + "signal_wakeup" [label = "signal_wakeup"]; + "signal_wakeup" -> "runnable" [ label = "signal_deliver" ]; + "signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ]; + "signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "sleepable" [label = "sleepable"]; + "sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ]; + "sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ]; + "sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ]; + "sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "runnable" [ label = "sched_wakeup" ]; + { rank = min ; + "__init_runnable"; + "runnable"; + } +} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/models/sched/sts.dot new file mode 100644 index 000000000000..8f5f38be04d5 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; + {node [shape = doublecircle] "can_sched"}; + {node [shape = circle] "can_sched"}; + {node [shape = circle] "cant_sched"}; + {node [shape = circle] "disable_to_switch"}; + {node [shape = circle] "enable_to_exit"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "scheduling"}; + {node [shape = circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label = "can_sched", color = green3]; + "can_sched" -> "cant_sched" [ label = "irq_disable" ]; + "can_sched" -> "scheduling" [ label = "schedule_entry" ]; + "cant_sched" [label = "cant_sched"]; + "cant_sched" -> "can_sched" [ label = "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label = "irq_entry" ]; + "disable_to_switch" [label = "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label = "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label = "irq_entry" ]; + "disable_to_switch" -> "switching" [ label = "sched_switch" ]; + "enable_to_exit" [label = "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label = "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label = "irq_disable\nirq_entry\nirq_enable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "in_irq" [ label = "irq_entry" ]; + "in_irq" -> "scheduling" [ label = "irq_enable" ]; + "scheduling" [label = "scheduling"]; + "scheduling" -> "disable_to_switch" [ label = "irq_disable" ]; + "switching" [label = "switching"]; + "switching" -> "enable_to_exit" [ label = "irq_enable" ]; + { rank = min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/models/stall.dot b/tools/verification/models/stall.dot new file mode 100644 index 000000000000..50077d1dff74 --- /dev/null +++ b/tools/verification/models/stall.dot @@ -0,0 +1,22 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "enqueued"}; + {node [shape = plaintext, style=invis, label=""] "__init_dequeued"}; + {node [shape = doublecircle] "dequeued"}; + {node [shape = circle] "running"}; + "__init_dequeued" -> "dequeued"; + "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; + "running" [label = "running"]; + "dequeued" [label = "dequeued", color = green3]; + "running" -> "running" [ label = "sched_switch_in\nsched_wakeup" ]; + "enqueued" -> "enqueued" [ label = "sched_wakeup" ]; + "enqueued" -> "running" [ label = "sched_switch_in" ]; + "running" -> "dequeued" [ label = "sched_switch_wait" ]; + "dequeued" -> "enqueued" [ label = "sched_wakeup;reset(clk)" ]; + "running" -> "enqueued" [ label = "sched_switch_preempt;reset(clk)" ]; + { rank = min ; + "__init_dequeued"; + "dequeued"; + } +} diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile index 411d62b3d8eb..5b898360ba48 100644 --- a/tools/verification/rv/Makefile +++ b/tools/verification/rv/Makefile @@ -35,12 +35,6 @@ FEATURE_TESTS += libtracefs FEATURE_DISPLAY := libtraceevent FEATURE_DISPLAY += libtracefs -ifeq ($(V),1) - Q = -else - Q = @ -endif - all: $(RV) include $(srctree)/tools/build/Makefile.include diff --git a/tools/verification/rv/Makefile.rv b/tools/verification/rv/Makefile.rv index 161baa29eb86..2497fb96c83d 100644 --- a/tools/verification/rv/Makefile.rv +++ b/tools/verification/rv/Makefile.rv @@ -27,7 +27,7 @@ endif INCLUDE := -Iinclude/ CFLAGS := -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(WOPTS) $(EXTRA_CFLAGS) $(INCLUDE) -LDFLAGS := -ggdb $(EXTRA_LDFLAGS) +LDFLAGS := -ggdb $(LDFLAGS) $(EXTRA_LDFLAGS) INSTALL := install MKDIR := mkdir diff --git a/tools/verification/rv/include/in_kernel.h b/tools/verification/rv/include/in_kernel.h index 3090638c8d71..f3bfd3b9895f 100644 --- a/tools/verification/rv/include/in_kernel.h +++ b/tools/verification/rv/include/in_kernel.h @@ -1,3 +1,3 @@ // SPDX-License-Identifier: GPL-2.0 -int ikm_list_monitors(void); +int ikm_list_monitors(char *container); int ikm_run_monitor(char *monitor, int argc, char **argv); diff --git a/tools/verification/rv/include/rv.h b/tools/verification/rv/include/rv.h index 770fd6da3610..6f668eb266cb 100644 --- a/tools/verification/rv/include/rv.h +++ b/tools/verification/rv/include/rv.h @@ -1,12 +1,13 @@ // SPDX-License-Identifier: GPL-2.0 #define MAX_DESCRIPTION 1024 -#define MAX_DA_NAME_LEN 24 +#define MAX_DA_NAME_LEN 32 struct monitor { char name[MAX_DA_NAME_LEN]; char desc[MAX_DESCRIPTION]; int enabled; + int nested; }; int should_stop(void); diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index f2bbc75a76f4..4bb746ea6e17 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -6,15 +6,18 @@ */ #include <getopt.h> #include <stdlib.h> +#include <stdio.h> #include <string.h> #include <errno.h> #include <unistd.h> +#include <dirent.h> #include <trace.h> #include <utils.h> #include <rv.h> static int config_has_id; +static int config_is_container; static int config_my_pid; static int config_trace; @@ -45,6 +48,51 @@ static int __ikm_read_enable(char *monitor_name) } /* + * __ikm_find_monitor - find the full name of a possibly nested module + * + * __does not log errors. + * + * Returns 1 if we found the monitor, -1 on error and 0 if it does not exist. + * The string out_name is populated with the full name, which can be + * equal to monitor_name or container/monitor_name if nested + */ +static int __ikm_find_monitor_name(char *monitor_name, char *out_name) +{ + char *available_monitors, container[MAX_DA_NAME_LEN+1], *cursor, *end; + int retval = 1; + + available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); + if (!available_monitors) + return -1; + + cursor = strstr(available_monitors, monitor_name); + if (!cursor) { + retval = 0; + goto out_free; + } + + for (; cursor > available_monitors; cursor--) + if (*(cursor-1) == '\n') + break; + end = strstr(cursor, "\n"); + memcpy(out_name, cursor, end-cursor); + out_name[end-cursor] = '\0'; + + cursor = strstr(out_name, ":"); + if (cursor) + *cursor = '/'; + else { + sprintf(container, "%s:", monitor_name); + if (strstr(available_monitors, container)) + config_is_container = 1; + } + +out_free: + free(available_monitors); + return retval; +} + +/* * ikm_read_enable - reads monitor's enable status * * Returns the current status, or -1 on error. @@ -132,12 +180,28 @@ static char *ikm_read_desc(char *monitor_name) /* * ikm_fill_monitor_definition - fill monitor's definition * - * Returns -1 on error, 0 otherwise. + * Returns -1 on error, 1 if the monitor does not belong in the container, 0 otherwise. + * container can be NULL */ -static int ikm_fill_monitor_definition(char *name, struct monitor *ikm) +static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *container) { int enabled; - char *desc; + char *desc, *nested_name; + + nested_name = strstr(name, ":"); + if (nested_name) { + /* it belongs in container if it starts with "container:" */ + if (container && strstr(name, container) != name) + return 1; + *nested_name = '/'; + ++nested_name; + ikm->nested = 1; + } else { + if (container) + return 1; + nested_name = name; + ikm->nested = 0; + } enabled = ikm_read_enable(name); if (enabled < 0) { @@ -151,7 +215,7 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm) return -1; } - strncpy(ikm->name, name, MAX_DA_NAME_LEN); + strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); ikm->enabled = enabled; strncpy(ikm->desc, desc, MAX_DESCRIPTION); @@ -270,12 +334,12 @@ static int ikm_has_id(char *monitor_name) * * Returns 0 on success, -1 otherwise. */ -int ikm_list_monitors(void) +int ikm_list_monitors(char *container) { char *available_monitors; - struct monitor ikm; + struct monitor ikm = {0}; char *curr, *next; - int retval; + int retval, list_monitor = 0; available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); @@ -289,15 +353,29 @@ int ikm_list_monitors(void) next = strstr(curr, "\n"); *next = '\0'; - retval = ikm_fill_monitor_definition(curr, &ikm); - if (retval) + retval = ikm_fill_monitor_definition(curr, &ikm, container); + if (retval < 0) err_msg("ikm: error reading %d in kernel monitor, skipping\n", curr); - printf("%-24s %s %s\n", ikm.name, ikm.desc, ikm.enabled ? "[ON]" : "[OFF]"); + if (!retval) { + int indent = ikm.nested && !container; + + list_monitor = 1; + printf("%s%-*s %s %s\n", indent ? " - " : "", + indent ? MAX_DA_NAME_LEN - 3 : MAX_DA_NAME_LEN, + ikm.name, ikm.desc, ikm.enabled ? "[ON]" : "[OFF]"); + } curr = ++next; } while (strlen(curr)); + if (!list_monitor) { + if (container) + printf("-- No monitor found in container %s --\n", container); + else + printf("-- No monitor found --\n"); + } + free(available_monitors); return 0; @@ -343,25 +421,34 @@ ikm_event_handler(struct trace_seq *s, struct tep_record *record, unsigned long long final_state; unsigned long long pid; unsigned long long id; - int cpu = record->cpu; int val; + bool missing_id; if (config_has_id) - tep_get_field_val(s, trace_event, "id", record, &id, 1); + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); if (config_has_id && (config_my_pid == id)) return 0; - else if (config_my_pid && (config_my_pid == pid)) + else if (config_my_pid == pid) return 0; - tep_print_event(trace_event->tep, s, record, "%16s-%-8d ", TEP_PRINT_COMM, TEP_PRINT_PID); + tep_print_event(trace_event->tep, s, record, "%16s-%-8d [%.3d] ", + TEP_PRINT_COMM, TEP_PRINT_PID, TEP_PRINT_CPU); - trace_seq_printf(s, "[%.3d] event ", cpu); + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "event "); - if (config_has_id) - trace_seq_printf(s, "%8llu ", id); + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); @@ -394,9 +481,10 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, int cpu = record->cpu; char *state, *event; int val; + bool missing_id; if (config_has_id) - tep_get_field_val(s, trace_event, "id", record, &id, 1); + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); @@ -405,10 +493,20 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, else if (config_my_pid == pid) return 0; - trace_seq_printf(s, "%8lld [%03d] error ", pid, cpu); + trace_seq_printf(s, "%8lld [%03d] ", pid, cpu); - if (config_has_id) - trace_seq_printf(s, "%8llu ", id); + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "error "); + + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); @@ -421,6 +519,64 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, return 0; } +static int ikm_enable_trace_events(char *monitor_name, struct trace_instance *inst) +{ + char event[MAX_DA_NAME_LEN + 7]; /* max(error_,event_) + '0' = 7 */ + int retval; + + snprintf(event, sizeof(event), "event_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_event_handler, NULL); + + snprintf(event, sizeof(event), "error_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_error_handler, NULL); + + /* set if at least 1 monitor has id in case of a container */ + config_has_id = ikm_has_id(monitor_name); + if (config_has_id < 0) + return -1; + + + return 0; +} + +static int ikm_enable_trace_container(char *monitor_name, + struct trace_instance *inst) +{ + DIR *dp; + char *abs_path, rv_path[MAX_PATH]; + struct dirent *ep; + int retval = 0; + + snprintf(rv_path, MAX_PATH, "rv/monitors/%s", monitor_name); + abs_path = tracefs_instance_get_file(NULL, rv_path); + if (!abs_path) + return -1; + dp = opendir(abs_path); + if (!dp) + goto out_free; + + while (!retval && (ep = readdir(dp))) { + if (ep->d_type != DT_DIR || ep->d_name[0] == '.') + continue; + retval = ikm_enable_trace_events(ep->d_name, inst); + } + + closedir(dp); +out_free: + free(abs_path); + return retval; +} + /* * ikm_setup_trace_instance - set up a tracing instance to collect data * @@ -430,19 +586,12 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, */ static struct trace_instance *ikm_setup_trace_instance(char *monitor_name) { - char event[MAX_DA_NAME_LEN + 7]; /* max(error_,event_) + '0' = 7 */ struct trace_instance *inst; int retval; if (!config_trace) return NULL; - config_has_id = ikm_has_id(monitor_name); - if (config_has_id < 0) { - err_msg("ikm: failed to read monitor %s event format\n", monitor_name); - goto out_err; - } - /* alloc data */ inst = calloc(1, sizeof(*inst)); if (!inst) { @@ -454,23 +603,13 @@ static struct trace_instance *ikm_setup_trace_instance(char *monitor_name) if (retval) goto out_free; - /* enable events */ - snprintf(event, sizeof(event), "event_%s", monitor_name); - retval = tracefs_event_enable(inst->inst, "rv", event); + if (config_is_container) + retval = ikm_enable_trace_container(monitor_name, inst); + else + retval = ikm_enable_trace_events(monitor_name, inst); if (retval) goto out_inst; - tep_register_event_handler(inst->tep, -1, "rv", event, - ikm_event_handler, NULL); - - snprintf(event, sizeof(event), "error_%s", monitor_name); - retval = tracefs_event_enable(inst->inst, "rv", event); - if (retval) - goto out_inst; - - tep_register_event_handler(inst->tep, -1, "rv", event, - ikm_error_handler, NULL); - /* ready to enable */ tracefs_trace_on(inst->inst); @@ -595,7 +734,7 @@ static int parse_arguments(char *monitor_name, int argc, char **argv) config_reactor = optarg; break; case 's': - config_my_pid = 0; + config_my_pid = -1; break; case 't': config_trace = 1; @@ -633,32 +772,41 @@ static int parse_arguments(char *monitor_name, int argc, char **argv) int ikm_run_monitor(char *monitor_name, int argc, char **argv) { struct trace_instance *inst = NULL; + char *nested_name, full_name[2*MAX_DA_NAME_LEN]; int retval; - /* - * Check if monitor exists by seeing it is enabled. - */ - retval = __ikm_read_enable(monitor_name); - if (retval < 0) + nested_name = strstr(monitor_name, ":"); + if (nested_name) + ++nested_name; + else + nested_name = monitor_name; + + retval = __ikm_find_monitor_name(monitor_name, full_name); + if (!retval) return 0; + if (retval < 0) { + err_msg("ikm: error finding monitor %s\n", nested_name); + return -1; + } + retval = __ikm_read_enable(full_name); if (retval) { - err_msg("ikm: monitor %s (in-kernel) is already enabled\n", monitor_name); + err_msg("ikm: monitor %s (in-kernel) is already enabled\n", nested_name); return -1; } /* we should be good to go */ - retval = parse_arguments(monitor_name, argc, argv); + retval = parse_arguments(full_name, argc, argv); if (retval) - ikm_usage(1, monitor_name, "ikm: failed parsing arguments"); + ikm_usage(1, nested_name, "ikm: failed parsing arguments"); if (config_trace) { - inst = ikm_setup_trace_instance(monitor_name); + inst = ikm_setup_trace_instance(nested_name); if (!inst) return -1; } - retval = ikm_enable(monitor_name); + retval = ikm_enable(full_name); if (retval < 0) goto out_free_instance; @@ -682,17 +830,17 @@ int ikm_run_monitor(char *monitor_name, int argc, char **argv) sleep(1); } - ikm_disable(monitor_name); + ikm_disable(full_name); ikm_destroy_trace_instance(inst); if (config_reactor && config_initial_reactor) - ikm_write_reactor(monitor_name, config_initial_reactor); + ikm_write_reactor(full_name, config_initial_reactor); return 1; out_free_instance: ikm_destroy_trace_instance(inst); if (config_reactor && config_initial_reactor) - ikm_write_reactor(monitor_name, config_initial_reactor); + ikm_write_reactor(full_name, config_initial_reactor); return -1; } diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index 1ddb85532816..b8fe24a87d97 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -41,30 +41,42 @@ static void rv_list(int argc, char **argv) { static const char *const usage[] = { "", - " usage: rv list [-h]", + " usage: rv list [-h] [container]", "", " list all available monitors", "", " -h/--help: print this menu", + "", + " [container]: list only monitors in this container", NULL, }; - int i; - - if (argc > 1) { + int i, print_help = 0, retval = 0; + char *container = NULL; + + if (argc == 2) { + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { + print_help = 1; + retval = 0; + } else if (argv[1][0] == '-') { + /* assume invalid option */ + print_help = 1; + retval = 1; + } else + container = argv[1]; + } else if (argc > 2) { + /* more than 2 is always usage */ + print_help = 1; + retval = 1; + } + if (print_help) { fprintf(stderr, "rv version %s\n", VERSION); - - /* more than 1 is always usage */ for (i = 0; usage[i]; i++) fprintf(stderr, "%s\n", usage[i]); - - /* but only -h is valid */ - if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) - exit(0); - else - exit(1); + exit(retval); } - ikm_list_monitors(); + ikm_list_monitors(container); + exit(0); } @@ -179,6 +191,7 @@ int main(int argc, char **argv) * and exit. */ signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); rv_mon(argc - 1, &argv[1]); } diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore new file mode 100644 index 000000000000..1e288a076560 --- /dev/null +++ b/tools/verification/rvgen/.gitignore @@ -0,0 +1,3 @@ +__pycache__/ +parser.out +parsetab.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile new file mode 100644 index 000000000000..cfc4056c1e87 --- /dev/null +++ b/tools/verification/rvgen/Makefile @@ -0,0 +1,27 @@ +INSTALL=install + +prefix ?= /usr +bindir ?= $(prefix)/bin +mandir ?= $(prefix)/share/man +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) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py + $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py + $(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py + $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen + cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py new file mode 100644 index 000000000000..3be7f85fe37b --- /dev/null +++ b/tools/verification/rvgen/__main__.py @@ -0,0 +1,70 @@ +#!/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 da2k, ha2k + from rvgen.generator import Monitor + from rvgen.container import Container + from rvgen.ltl2k import ltl2k + from rvgen.automata import AutomataError + 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", required=True, + help="Monitor class, either \"da\", \"ha\" or \"ltl\"") + monitor_parser.add_argument('-s', "--spec", dest="spec", required=True, + help="Monitor specification file") + monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True, + help=f"Available options: {', '.join(Monitor.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(f"Opening and parsing the specification file {params.spec}") + if params.monitor_class == "da": + monitor = da2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ha": + monitor = ha2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ltl": + monitor = ltl2k(params.spec, params.monitor_type, vars(params)) + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) + else: + monitor = Container(vars(params)) + except AutomataError as e: + print(f"There was an error processing {params.spec}: {e}", file=sys.stderr) + sys.exit(1) + + print(f"Writing the monitor into the directory {monitor.name}") + monitor.print_files() + print("Almost done, checklist") + if params.subcmd == "monitor": + print(f" - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation") + 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/dot2c b/tools/verification/rvgen/dot2c index 3fe89ab88b65..1012becc7fab 100644 --- a/tools/verification/dot2/dot2c +++ b/tools/verification/rvgen/dot2c @@ -14,9 +14,8 @@ # Documentation/trace/rv/deterministic_automata.rst if __name__ == '__main__': - from dot2 import dot2c + 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') diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py new file mode 100644 index 000000000000..b9f8149f7118 --- /dev/null +++ b/tools/verification/rvgen/rvgen/automata.py @@ -0,0 +1,368 @@ +#!/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 class: parse an automaton in dot file digraph format into a python object +# +# For further information, see: +# Documentation/trace/rv/deterministic_automata.rst + +import ntpath +import re +from typing import Iterator +from itertools import islice + +class _ConstraintKey: + """Base class for constraint keys.""" + +class _StateConstraintKey(_ConstraintKey, int): + """Key for a state constraint. Under the hood just state_id.""" + def __new__(cls, state_id: int): + return super().__new__(cls, state_id) + +class _EventConstraintKey(_ConstraintKey, tuple): + """Key for an event constraint. Under the hood just tuple(state_id,event_id).""" + def __new__(cls, state_id: int, event_id: int): + return super().__new__(cls, (state_id, event_id)) + +class AutomataError(Exception): + """Exception raised for errors in automata parsing and validation. + + Raised when DOT file processing fails due to invalid format, I/O errors, + or malformed automaton definitions. + """ + +class Automata: + """Automata class: Reads a dot file and parses it as an automaton. + + It supports both deterministic and hybrid automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + invalid_state_str = "INVALID_STATE" + init_marker = "__init_" + node_marker = "{node" + # val can be numerical, uppercase (constant or macro), lowercase (parameter or function) + # only numerical values should have units + constraint_rule = re.compile(r""" + ^ + (?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env var + (?P<op>[!<=>]{1,2}) # operator + (?P<val> + [0-9]+ | # numerical value + [A-Z_]+\(\) | # macro + [A-Z_]+ | # constant + [a-z_]+\(\) | # function + [a-z_]+ # parameter + ) + (?P<unit>[a-z]{1,2})? # optional unit for numerical values + """, re.VERBOSE) + constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)") + + 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.env_types = {} + self.env_stored = set() + self.constraint_vars = set() + self.self_loop_reset_events = set() + self.events, self.envs = self.__get_event_variables() + self.function, self.constraints = self.__create_matrix() + self.events_start, self.events_start_run = self.__store_init_events() + self.env_stored = sorted(self.env_stored) + self.constraint_vars = sorted(self.constraint_vars) + self.self_loop_reset_events = sorted(self.self_loop_reset_events) + + def __get_model_name(self) -> str: + basename = ntpath.basename(self.__dot_path) + if not basename.endswith(".dot") and not basename.endswith(".gv"): + print("not a dot file") + raise AutomataError(f"not a dot file: {self.__dot_path}") + + model_name = ntpath.splitext(basename)[0] + if not model_name: + raise AutomataError(f"not a dot file: {self.__dot_path}") + + return model_name + + def __open_dot(self) -> list[str]: + dot_lines = [] + try: + with open(self.__dot_path) as dot_file: + dot_lines = dot_file.readlines() + except OSError as exc: + raise AutomataError(exc.strerror) from exc + + if not dot_lines: + raise AutomataError(f"{self.__dot_path} is empty") + + # checking the first line: + line = dot_lines[0].split() + + if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton": + raise AutomataError(f"Not a valid .dot format: {self.__dot_path}") + + return dot_lines + + def __get_cursor_begin_states(self) -> int: + for cursor, line in enumerate(self.__dot_lines): + split_line = line.split() + + if len(split_line) and split_line[0] == self.node_marker: + return cursor + + raise AutomataError("Could not find a beginning state") + + def __get_cursor_begin_events(self) -> int: + state = 0 + cursor = 0 # make pyright happy + + for cursor, line in enumerate(self.__dot_lines): + line = line.split() + if not line: + continue + + if state == 0: + if line[0] == self.node_marker: + state = 1 + elif line[0] != self.node_marker: + break + else: + raise AutomataError("Could not find beginning event") + + cursor += 1 # skip initial state transition + if cursor == len(self.__dot_lines): + raise AutomataError("Dot file ended after event beginning") + + return cursor + + def __get_state_variables(self) -> tuple[list[str], str, list[str]]: + # wait for node declaration + states = [] + final_states = [] + initial_state = "" + + has_final_states = False + cursor = self.__get_cursor_begin_states() + + # process nodes + for line in islice(self.__dot_lines, cursor, None): + split_line = line.split() + if not split_line or split_line[0] != self.node_marker: + break + + raw_state = split_line[-1] + + # "enabled_fired"}; -> enabled_fired + state = raw_state.replace('"', '').replace('};', '').replace(',', '_') + if state.startswith(self.init_marker): + initial_state = state[len(self.init_marker):] + else: + states.append(state) + if "doublecircle" in line: + final_states.append(state) + has_final_states = True + + if "ellipse" in line: + final_states.append(state) + has_final_states = True + + if not initial_state: + raise AutomataError("The automaton doesn't have an initial state") + + states = sorted(set(states)) + states.remove(initial_state) + + # Insert the initial state at the beginning of 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) -> tuple[list[str], list[str]]: + events: list[str] = [] + envs: list[str] = [] + # here we are at the begin of transitions, take a note, we will return later. + cursor = self.__get_cursor_begin_events() + + for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)): + if not line.startswith('"'): + break + + # transitions have the format: + # "all_fired" -> "both_fired" [ label = "disable_irq" ]; + # ------------ event is here ------------^^^^^ + split_line = line.split() + if len(split_line) > 1 and split_line[1] == "->": + event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '') + + # when a transition has more than one label, they are like this + # "local_irq_enable\nhw_local_irq_enable_n" + # so split them. + + for i in event.split("\\n"): + # if the event contains a constraint (hybrid automata), + # it will be separated by a ";": + # "sched_switch;x<1000;reset(x)" + ev, *constr = i.split(";") + if constr: + if len(constr) > 2: + raise AutomataError("Only 1 constraint and 1 reset are supported") + envs += self.__extract_env_var(constr) + events.append(ev) + else: + # state labels have the format: + # "enable_fired" [label = "enable_fired\ncondition"]; + # ----- label is here -----^^^^^ + # label and node name must be the same, condition is optional + state = line.split("label")[1].split('"')[1] + _, *constr = state.split("\\n") + if constr: + if len(constr) > 1: + raise AutomataError("Only 1 constraint is supported in the state") + envs += self.__extract_env_var([constr[0].replace(" ", "")]) + + return sorted(set(events)), sorted(set(envs)) + + def _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str, + str | None]]: + """ + Get a list of strings of the type constr1 && constr2 and returns a list of + constraints and separators: [[constr1,"&&"],[constr2,None]] + """ + exprs = [] + seps = [] + for c in constr: + while "&&" in c or "||" in c: + a = c.find("&&") + o = c.find("||") + pos = a if o < 0 or 0 < a < o else o + exprs.append(c[:pos].replace(" ", "")) + seps.append(c[pos:pos + 2].replace(" ", "")) + c = c[pos + 2:].replace(" ", "") + exprs.append(c) + seps.append(None) + return zip(exprs, seps) + + def __extract_env_var(self, constraint: list[str]) -> list[str]: + env = [] + for c, _ in self._split_constraint_expr(constraint): + rule = self.constraint_rule.search(c) + reset = self.constraint_reset.search(c) + if rule: + env.append(rule["env"]) + if rule.groupdict().get("unit"): + self.env_types[rule["env"]] = rule["unit"] + if rule["val"][0].isalpha(): + self.constraint_vars.add(rule["val"]) + # try to infer unit from constants or parameters + val_for_unit = rule["val"].lower().replace("()", "") + if val_for_unit.endswith("_ns"): + self.env_types[rule["env"]] = "ns" + if val_for_unit.endswith("_jiffies"): + self.env_types[rule["env"]] = "j" + if reset: + env.append(reset["env"]) + # environment variables that are reset need a storage + self.env_stored.add(reset["env"]) + return env + + def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]: + # 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 _ in range(nr_event)] for _ in range(nr_state)] + constraints: dict[_ConstraintKey, list[str]] = {} + + # and we are back! Let's fill the matrix + cursor = self.__get_cursor_begin_events() + + for line in map(str.lstrip, + islice(self.__dot_lines, cursor, None)): + + if not line or line[0] != '"': + break + + split_line = line.split() + + if len(split_line) > 2 and split_line[1] == "->": + origin_state = split_line[0].replace('"', '').replace(',', '_') + dest_state = split_line[2].replace('"', '').replace(',', '_') + possible_events = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '') + for event in possible_events.split("\\n"): + event, *constr = event.split(";") + if constr: + key = _EventConstraintKey(states_dict[origin_state], events_dict[event]) + constraints[key] = constr + # those events reset also on self loops + if origin_state == dest_state and "reset" in "".join(constr): + self.self_loop_reset_events.add(event) + matrix[states_dict[origin_state]][events_dict[event]] = dest_state + else: + state = line.split("label")[1].split('"')[1] + state, *constr = state.replace(" ", "").split("\\n") + if constr: + constraints[_StateConstraintKey(states_dict[state])] = constr + + return matrix, constraints + + def __store_init_events(self) -> tuple[list[bool], list[bool]]: + events_start = [False] * len(self.events) + events_start_run = [False] * len(self.events) + for i in range(len(self.events)): + curr_event_will_init = 0 + curr_event_from_init = False + curr_event_used = 0 + for j in range(len(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: str) -> bool: + return self.events_start[self.events.index(event)] + + def is_start_run_event(self, event: str) -> bool: + # prefer handle_start_event if there + if any(self.events_start): + return False + return self.events_start_run[self.events.index(event)] + + def is_hybrid_automata(self) -> bool: + return bool(self.envs) + + def is_event_constraint(self, key: _ConstraintKey) -> bool: + """ + Given the key in self.constraints return true if it is an event + constraint, false if it is a state constraint + """ + return isinstance(key, _EventConstraintKey) diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py new file mode 100644 index 000000000000..51f188530b4d --- /dev/null +++ b/tools/verification/rvgen/rvgen/container.py @@ -0,0 +1,32 @@ +#!/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> +# +# Generator for runtime verification monitor container + +from . import generator + + +class Container(generator.RVGenerator): + template_dir = "container" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.name = extra_params.get("model_name") + self.main_h = self._read_template_file("main.h") + + def fill_model_h(self): + main_h = self.main_h + main_h = main_h.replace("%%MODEL_NAME%%", self.name) + return main_h + + def fill_kconfig_tooltip(self): + """Override to produce a marker for this container in the Kconfig""" + container_marker = self._kconfig_marker(self.name) + "\n" + result = super().fill_kconfig_tooltip() + if self.auto_patch: + self._patch_file("Kconfig", + self._kconfig_marker(), container_marker) + return result + return result + container_marker diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py new file mode 100644 index 000000000000..fc85ba1f649e --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -0,0 +1,268 @@ +#!/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 automaton 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, AutomataError + +class Dot2c(Automata): + enum_suffix = "" + enum_states_def = "states" + enum_events_def = "events" + enum_envs_def = "envs" + 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 __get_enum_states_content(self) -> list[str]: + buff = [] + buff.append(f"\t{self.initial_state}{self.enum_suffix},") + for state in self.states: + if state != self.initial_state: + buff.append(f"\t{state}{self.enum_suffix},") + buff.append(f"\tstate_max{self.enum_suffix},") + + return buff + + def format_states_enum(self) -> list[str]: + buff = [] + buff.append(f"enum {self.enum_states_def} {{") + buff += self.__get_enum_states_content() + buff.append("};\n") + + return buff + + def __get_enum_events_content(self) -> list[str]: + buff = [] + for event in self.events: + buff.append(f"\t{event}{self.enum_suffix},") + + buff.append(f"\tevent_max{self.enum_suffix},") + + return buff + + def format_events_enum(self) -> list[str]: + buff = [] + buff.append(f"enum {self.enum_events_def} {{") + buff += self.__get_enum_events_content() + buff.append("};\n") + + return buff + + def __get_non_stored_envs(self) -> list[str]: + return [e for e in self.envs if e not in self.env_stored] + + def __get_enum_envs_content(self) -> list[str]: + buff = [] + # We first place env variables that have a u64 storage. + # Those are limited by MAX_HA_ENV_LEN, other variables + # are read only and don't require a storage. + unstored = self.__get_non_stored_envs() + for env in list(self.env_stored) + unstored: + buff.append(f"\t{env}{self.enum_suffix},") + + buff.append(f"\tenv_max{self.enum_suffix},") + max_stored = unstored[0] if len(unstored) else "env_max" + buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},") + + return buff + + def format_envs_enum(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + buff.append(f"enum {self.enum_envs_def} {{") + buff += self.__get_enum_envs_content() + buff.append("};\n") + buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN," + ' "Not enough slots");') + if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()): + buff.append("#define HA_CLK_NS") + buff.append("") + return buff + + def get_minimun_type(self) -> str: + min_type = "unsigned char" + + if len(self.states) > 255: + min_type = "unsigned short" + + if len(self.states) > 65535: + min_type = "unsigned int" + + if len(self.states) > 1000000: + raise AutomataError(f"Too many states: {len(self.states)}") + + return min_type + + def format_automaton_definition(self) -> list[str]: + min_type = self.get_minimun_type() + buff = [] + buff.append(f"struct {self.struct_automaton_def} {{") + buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];") + buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];") + if self.is_hybrid_automata(): + buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];") + buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];") + buff.append(f"\t{min_type} initial_state;") + buff.append(f"\tbool final_states[state_max{self.enum_suffix}];") + buff.append("};\n") + return buff + + def format_aut_init_header(self) -> list[str]: + buff = [] + buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{") + return buff + + def __get_string_vector_per_line_content(self, entries: list[str]) -> str: + buff = [] + for entry in entries: + buff.append(f"\t\t\"{entry}\",") + return "\n".join(buff) + + def format_aut_init_events_string(self) -> list[str]: + buff = [] + buff.append("\t.event_names = {") + buff.append(self.__get_string_vector_per_line_content(self.events)) + buff.append("\t},") + return buff + + def format_aut_init_states_string(self) -> list[str]: + buff = [] + buff.append("\t.state_names = {") + buff.append(self.__get_string_vector_per_line_content(self.states)) + buff.append("\t},") + + return buff + + def format_aut_init_envs_string(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + buff.append("\t.env_names = {") + # maintain consistent order with the enum + ordered_envs = list(self.env_stored) + self.__get_non_stored_envs() + buff.append(self.__get_string_vector_per_line_content(ordered_envs)) + buff.append("\t},") + + return buff + + def __get_max_strlen_of_states(self) -> int: + max_state_name = len(max(self.states, key=len)) + return max(max_state_name, len(self.invalid_state_str)) + + def get_aut_init_function(self) -> str: + nr_states = len(self.states) + nr_events = len(self.events) + buff = [] + + maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) + tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" + comma_space = 2 # ", " count last comma here + linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length + for x in range(nr_states): + line = "\t\t{\n" if linetoolong else "\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 linetoolong: + line += f"\t\t\t{next_state}" + else: + line += f"{next_state:>{maxlen}}" + if y != nr_events - 1: + line += ",\n" if linetoolong else ", " + else: + line += ",\n\t\t}," if linetoolong else " }," + buff.append(line) + + return '\n'.join(buff) + + def format_aut_init_function(self) -> list[str]: + buff = [] + buff.append("\t.function = {") + buff.append(self.get_aut_init_function()) + buff.append("\t},") + + return buff + + def get_aut_init_initial_state(self) -> str: + return self.initial_state + + def format_aut_init_initial_state(self) -> list[str]: + 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) -> str: + line = "" + first = True + for state in self.states: + if not first: + line = line + ', ' + else: + first = False + + if state in self.final_states: + line = line + '1' + else: + line = line + '0' + return line + + def format_aut_init_final_states(self) -> list[str]: + buff = [] + buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},") + + return buff + + def __get_automaton_initialization_footer_string(self) -> str: + footer = "};\n" + return footer + + def format_aut_init_footer(self) -> list[str]: + buff = [] + buff.append(self.__get_automaton_initialization_footer_string()) + + return buff + + def format_invalid_state(self) -> list[str]: + buff = [] + buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n") + + return buff + + def format_model(self) -> list[str]: + buff = [] + buff += self.format_states_enum() + buff += self.format_invalid_state() + buff += self.format_events_enum() + buff += self.format_envs_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_envs_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('\n'.join(buff)) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py new file mode 100644 index 000000000000..e6f476b903b0 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -0,0 +1,611 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +from collections import deque +from .dot2c import Dot2c +from .generator import Monitor +from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError + + +class dot2k(Monitor, Dot2c): + template_dir = "dot2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + self.monitor_type = MonitorType + Monitor.__init__(self, extra_params) + Dot2c.__init__(self, file_path, extra_params.get("model_name")) + self.enum_suffix = f"_{self.name}" + self.enum_suffix = f"_{self.name}" + self.monitor_class = extra_params["monitor_class"] + + def fill_monitor_type(self) -> str: + buff = [ self.monitor_type.upper() ] + buff += self._fill_timer_type() + if self.monitor_type == "per_obj": + buff.append("typedef /* XXX: define the target type */ *monitor_target;") + return "\n".join(buff) + + def fill_tracepoint_handlers_skel(self) -> str: + buff = [] + buff += self._fill_hybrid_definitions() + for event in self.events: + buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)") + buff.append("{") + handle = "handle_event" + if self.is_start_event(event): + buff.append("\t/* XXX: validate that this event always leads to the initial state */") + handle = "handle_start_event" + elif self.is_start_run_event(event): + buff.append("\t/* XXX: validate that this event is only valid in the initial state */") + handle = "handle_start_run_event" + if self.monitor_type == "per_task": + buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;") + buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});") + elif self.monitor_type == "per_obj": + buff.append("\tint id = /* XXX: how do I get the id? */;") + buff.append("\tmonitor_target t = /* XXX: how do I get t? */;") + buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});") + else: + buff.append(f"\tda_{handle}({event}{self.enum_suffix});") + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self) -> str: + buff = [] + for event in self.events: + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + return '\n'.join(buff) + + def fill_tracepoint_detach_helper(self) -> str: + buff = [] + for event in self.events: + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + return '\n'.join(buff) + + def fill_model_h_header(self) -> list[str]: + buff = [] + buff.append("/* SPDX-License-Identifier: GPL-2.0 */") + buff.append("/*") + buff.append(f" * Automatically generated C representation of {self.name} automaton") + buff.append(" * For further information about this format, see kernel documentation:") + buff.append(" * Documentation/trace/rv/deterministic_automata.rst") + buff.append(" */") + buff.append("") + buff.append(f"#define MONITOR_NAME {self.name}") + buff.append("") + + return buff + + def fill_model_h(self) -> str: + # + # Adjust the definition names + # + self.enum_states_def = f"states_{self.name}" + self.enum_events_def = f"events_{self.name}" + self.enum_envs_def = f"envs_{self.name}" + self.struct_automaton_def = f"automaton_{self.name}" + self.var_automaton_def = f"automaton_{self.name}" + + buff = self.fill_model_h_header() + buff += self.format_model() + + return '\n'.join(buff) + + def _is_id_monitor(self) -> bool: + return self.monitor_type in ("per_task", "per_obj") + + def fill_monitor_class_type(self) -> str: + if self._is_id_monitor(): + return "DA_MON_EVENTS_ID" + return "DA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self) -> str: + if self._is_id_monitor(): + return "da_monitor_id" + return "da_monitor" + + def fill_tracepoint_args_skel(self, tp_type: str) -> str: + buff = [] + tp_args_event = [ + ("char *", "state"), + ("char *", "event"), + ("char *", "next_state"), + ("bool ", "final_state"), + ] + tp_args_error = [ + ("char *", "state"), + ("char *", "event"), + ] + tp_args_error_env = tp_args_error + [("char *", "env")] + tp_args_dict = { + "event": tp_args_event, + "error": tp_args_error, + "error_env": tp_args_error_env + } + tp_args_id = ("int ", "id") + tp_args = tp_args_dict[tp_type] + if self._is_id_monitor(): + 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(f" TP_PROTO({tp_proto_c}),") + buff.append(f" TP_ARGS({tp_args_c})") + return '\n'.join(buff) + + def _fill_hybrid_definitions(self) -> list: + """Stub, not valid for deterministic automata""" + return [] + + def _fill_timer_type(self) -> list: + """Stub, not valid for deterministic automata""" + return [] + + def fill_main_c(self) -> str: + main_c = super().fill_main_c() + + min_type = self.get_minimun_type() + nr_events = len(self.events) + monitor_type = self.fill_monitor_type() + + main_c = main_c.replace("%%MIN_TYPE%%", min_type) + main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) + main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) + main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class) + + return main_c + +class da2k(dot2k): + """Deterministic automata only""" + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + if self.is_hybrid_automata(): + raise AutomataError("Detected hybrid automaton, use the 'ha' class") + +class ha2k(dot2k): + """Hybrid automata only""" + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + if not self.is_hybrid_automata(): + raise AutomataError("Detected deterministic automaton, use the 'da' class") + self.trace_h = self._read_template_file("trace_hybrid.h") + self.__parse_constraints() + + def fill_monitor_class_type(self) -> str: + if self._is_id_monitor(): + return "HA_MON_EVENTS_ID" + return "HA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self) -> str: + """ + Used for tracepoint classes, since they are shared we keep da + instead of ha (also for the ha specific tracepoints). + The tracepoint class is not visible to the tools. + """ + return super().fill_monitor_class() + + def __adjust_value(self, value: str | int, unit: str | None) -> str: + """Adjust the value in ns""" + try: + value = int(value) + except ValueError: + # it's a constant, a parameter or a function + if value.endswith("()"): + return value.replace("()", "(ha_mon)") + return value + match unit: + case "us": + value *= 10**3 + case "ms": + value *= 10**6 + case "s": + value *= 10**9 + return str(value) + "ull" + + def __parse_single_constraint(self, rule: dict, value: str) -> str: + return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}" + + def __get_constraint_env(self, constr: str) -> str: + """Extract the second argument from an ha_ function""" + env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",") + assert env.rstrip(f"_{self.name}") in self.envs + return env + + def __start_to_invariant_check(self, constr: str) -> str: + # by default assume the timer has ns expiration + env = self.__get_constraint_env(constr) + clock_type = "ns" + if self.env_types.get(env.rstrip(f"_{self.name}")) == "j": + clock_type = "jiffy" + + return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" + + def __start_to_conv(self, constr: str) -> str: + """ + Undo the storage conversion done by ha_start_timer_ + """ + return "ha_inv_to_guard" + constr[constr.find("("):] + + def __parse_timer_constraint(self, rule: dict, value: str) -> str: + # by default assume the timer has ns expiration + clock_type = "ns" + if self.env_types.get(rule["env"]) == "j": + clock_type = "jiffy" + + return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix}," + f" {value}, time_ns)") + + def __format_guard_rules(self, rules: list[str]) -> list[str]: + """ + Merge guard constraints as a single C return statement. + If the rules include a stored env, also check its validity. + Break lines in a best effort way that tries to keep readability. + """ + if not rules: + return [] + + invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||" + for env in self.env_stored if any(env in rule for rule in rules)] + if invalid_checks and len(rules) > 1: + rules[0] = "(" + rules[0] + rules[-1] = rules[-1] + ")" + rules = invalid_checks + rules + + separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " " + return ["res = " + separator.join(rules)] + + def __validate_constraint(self, key: tuple[int, int] | int, constr: str, + rule, reset) -> None: + # event constrains are tuples and allow both rules and reset + # state constraints are only used for expirations (e.g. clk<N) + if self.is_event_constraint(key): + if not rule and not reset: + raise AutomataError("Unrecognised event constraint " + f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})") + if rule and (rule["env"] in self.env_types and + rule["env"] not in self.env_stored): + raise AutomataError("Clocks in hybrid automata always require a storage" + f" ({rule["env"]})") + else: + if not rule: + raise AutomataError("Unrecognised state constraint " + f"({self.states[key]}: {constr})") + if rule["env"] not in self.env_stored: + raise AutomataError("State constraints always require a storage " + f"({rule["env"]})") + if rule["op"] not in ["<", "<="]: + raise AutomataError("State constraints must be clock expirations like" + f" clk<N ({rule.string})") + + def __parse_constraints(self) -> None: + self.guards: dict[_EventConstraintKey, str] = {} + self.invariants: dict[_StateConstraintKey, str] = {} + for key, constraint in self.constraints.items(): + rules = [] + resets = [] + for c, sep in self._split_constraint_expr(constraint): + rule = self.constraint_rule.search(c) + reset = self.constraint_reset.search(c) + self.__validate_constraint(key, c, rule, reset) + if rule: + value = rule["val"] + value_len = len(rule["val"]) + unit = None + if rule.groupdict().get("unit"): + value_len += len(rule["unit"]) + unit = rule["unit"] + c = c[:-(value_len)] + value = self.__adjust_value(value, unit) + if self.is_event_constraint(key): + c = self.__parse_single_constraint(rule, value) + if sep: + c += f" {sep}" + else: + c = self.__parse_timer_constraint(rule, value) + rules.append(c) + if reset: + c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)" + resets.append(c) + if self.is_event_constraint(key): + res = self.__format_guard_rules(rules) + resets + self.guards[key] = ";".join(res) + else: + self.invariants[key] = rules[0] + + def __fill_verify_invariants_func(self) -> list[str]: + buff = [] + if not self.invariants: + return [] + + buff.append( +f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, +\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) +{{""") + + _else = "" + for state, constr in sorted(self.invariants.items()): + check_str = self.__start_to_invariant_check(constr) + buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})") + buff.append(f"\t\t{check_str};") + _else = "else " + + buff.append("\treturn true;\n}\n") + return buff + + def __fill_convert_inv_guard_func(self) -> list[str]: + buff = [] + if not self.invariants: + return [] + + conflict_guards, conflict_invs = self.__find_inv_conflicts() + if not conflict_guards and not conflict_invs: + return [] + + buff.append( +f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon, +\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) +{{""") + buff.append("\tif (curr_state == next_state)\n\t\treturn;") + + _else = "" + for state, constr in sorted(self.invariants.items()): + # a state with invariant can reach us without reset + # multiple conflicts must have the same invariant, otherwise we cannot + # know how to reset the value + conf_i = [start for start, end in conflict_invs if end == state] + # we can reach a guard without reset + conf_g = [e for s, e in conflict_guards if s == state] + if not conf_i and not conf_g: + continue + buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})") + + buff.append(f"\t\t{self.__start_to_conv(constr)};") + _else = "else " + + buff.append("}\n") + return buff + + def __fill_verify_guards_func(self) -> list[str]: + buff = [] + if not self.guards: + return [] + + buff.append( +f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{ +\tbool res = true; +""") + + _else = "" + for edge, constr in sorted(self.guards.items()): + buff.append(f"\t{_else}if (curr_state == " + f"{self.states[edge[0]]}{self.enum_suffix} && " + f"event == {self.events[edge[1]]}{self.enum_suffix})") + if constr.count(";") > 0: + buff[-1] += " {" + buff += [f"\t\t{c};" for c in constr.split(";")] + if constr.count(";") > 0: + _else = "} else " + else: + _else = "else " + if _else[0] == "}": + buff.append("\t}") + buff.append("\treturn res;\n}\n") + return buff + + def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]], + set[tuple[int, _StateConstraintKey]]]: + """ + Run a breadth first search from all states with an invariant. + Find any conflicting constraints reachable from there, this can be + another state with an invariant or an edge with a non-reset guard. + Stop when we find a reset. + + Return the set of conflicting guards and invariants as tuples of + conflicting state and constraint key. + """ + conflict_guards: set[tuple[int, _EventConstraintKey]] = set() + conflict_invs: set[tuple[int, _StateConstraintKey]] = set() + for start_idx in self.invariants: + queue = deque([(start_idx, 0)]) # (state_idx, distance) + env = self.__get_constraint_env(self.invariants[start_idx]) + + while queue: + curr_idx, distance = queue.popleft() + + # Check state condition + if curr_idx != start_idx and curr_idx in self.invariants: + conflict_invs.add((start_idx, _StateConstraintKey(curr_idx))) + continue + + # Check if we should stop + if distance > len(self.states): + break + if curr_idx != start_idx and distance > 1: + continue + + for event_idx, next_state_name in enumerate(self.function[curr_idx]): + if next_state_name == self.invalid_state_str: + continue + curr_guard = self.guards.get((curr_idx, event_idx), "") + if "reset" in curr_guard and env in curr_guard: + continue + + if env in curr_guard: + conflict_guards.add((start_idx, + _EventConstraintKey(curr_idx, event_idx))) + continue + + next_idx = self.states.index(next_state_name) + queue.append((next_idx, distance + 1)) + + return conflict_guards, conflict_invs + + def __fill_setup_invariants_func(self) -> list[str]: + buff = [] + if not self.invariants: + return [] + + buff.append( +f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{""") + + conditions = ["next_state == curr_state"] + conditions += [f"event != {e}{self.enum_suffix}" + for e in self.self_loop_reset_events] + condition_str = " && ".join(conditions) + buff.append(f"\tif ({condition_str})\n\t\treturn;") + + _else = "" + for state, constr in sorted(self.invariants.items()): + buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})") + buff.append(f"\t\t{constr};") + _else = "else " + + for state in self.invariants: + buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})") + buff.append("\t\tha_cancel_timer(ha_mon);") + + buff.append("}\n") + return buff + + def __fill_constr_func(self) -> list[str]: + buff = [] + if not self.constraints: + return [] + + buff.append( +"""/* + * These functions are used to validate state transitions. + * + * They are generated by parsing the model, there is usually no need to change them. + * If the monitor requires a timer, there are functions responsible to arm it when + * the next state has a constraint, cancel it in any other case and to check + * that it didn't expire before the callback run. Transitions to the same state + * without a reset never affect timers. + * Due to the different representations between invariants and guards, there is + * a function to convert it in case invariants or guards are reachable from + * another invariant without reset. Those are not present if not required in + * the model. This is all automatic but is worth checking because it may show + * errors in the model (e.g. missing resets). + */""") + + buff += self.__fill_verify_invariants_func() + inv_conflicts = self.__fill_convert_inv_guard_func() + buff += inv_conflicts + buff += self.__fill_verify_guards_func() + buff += self.__fill_setup_invariants_func() + + buff.append( +f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{""") + + if self.invariants: + buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, " + "event, next_state, time_ns))\n\t\treturn false;\n") + if inv_conflicts: + buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, " + "next_state, time_ns);\n") + + if self.guards: + buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, " + "next_state, time_ns))\n\t\treturn false;\n") + + if self.invariants: + buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n") + + buff.append("\treturn true;\n}\n") + return buff + + def __fill_env_getter(self, env: str) -> str: + if env in self.env_types: + match self.env_types[env]: + case "ns" | "us" | "ms" | "s": + return "ha_get_clk_ns(ha_mon, env, time_ns);" + case "j": + return "ha_get_clk_jiffy(ha_mon, env);" + return f"/* XXX: how do I read {env}? */" + + def __fill_env_resetter(self, env: str) -> str: + if env in self.env_types: + match self.env_types[env]: + case "ns" | "us" | "ms" | "s": + return "ha_reset_clk_ns(ha_mon, env, time_ns);" + case "j": + return "ha_reset_clk_jiffy(ha_mon, env);" + return f"/* XXX: how do I reset {env}? */" + + def __fill_hybrid_get_reset_functions(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + for var in self.constraint_vars: + if var.endswith("()"): + func_name = var.replace("()", "") + if func_name.isupper(): + buff.append(f"#define {func_name}(ha_mon) " + f"/* XXX: what is {func_name}(ha_mon)? */\n") + else: + buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{") + buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;") + buff.append("}\n") + elif var.isupper(): + buff.append(f"#define {var} /* XXX: what is {var}? */\n") + else: + buff.append(f"static u64 {var} = /* XXX: default value */;") + buff.append(f"module_param({var}, ullong, 0644);\n") + buff.append("""/* + * These functions define how to read and reset the environment variable. + * + * Common environment variables like ns-based and jiffy-based clocks have + * pre-define getters and resetters you can use. The parser can infer the type + * of the environment variable if you supply a measure unit in the constraint. + * If you define your own functions, make sure to add appropriate memory + * barriers if required. + * Some environment variables don't require a storage as they read a system + * state (e.g. preemption count). Those variables are never reset, so we don't + * define a reset function on monitors only relying on this type of variables. + */""") + buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, " + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") + _else = "" + for env in self.envs: + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") + buff.append(f"\t\treturn {self.__fill_env_getter(env)}") + _else = "else " + buff.append("\treturn ENV_INVALID_VALUE;\n}\n") + if len(self.env_stored): + buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, " + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") + _else = "" + for env in self.env_stored: + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") + buff.append(f"\t\t{self.__fill_env_resetter(env)}") + _else = "else " + buff.append("}\n") + return buff + + def _fill_hybrid_definitions(self) -> list[str]: + return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func() + + def _fill_timer_type(self) -> list: + if self.invariants: + return [ + "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */", + "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" + ] + return [] diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py new file mode 100644 index 000000000000..56f3bd8db850 --- /dev/null +++ b/tools/verification/rvgen/rvgen/generator.py @@ -0,0 +1,251 @@ +#!/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> +# +# Abstract class for generating kernel runtime verification monitors from specification file + +import platform +import os + + +class RVGenerator: + rv_dir = "kernel/trace/rv" + + def __init__(self, extra_params={}): + self.name = extra_params.get("model_name") + self.parent = extra_params.get("parent") + self.abs_template_dir = \ + os.path.join(os.path.dirname(__file__), "templates", self.template_dir) + self.main_c = self._read_template_file("main.c") + self.kconfig = self._read_template_file("Kconfig") + 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_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(f"/lib/modules/{platform.release()}/build", 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): + with open(path, 'r') as fd: + content = fd.read() + return content + + def _read_template_file(self, file): + try: + path = os.path.join(self.abs_template_dir, file) + return self._read_file(path) + except OSError: + # Specific template file not found. Try the generic template file in the template/ + # directory, which is one level up + path = os.path.join(self.abs_template_dir, "..", file) + return self._read_file(path) + + def fill_parent(self): + return f"&rv_{self.parent}" if self.parent else "NULL" + + def fill_include_parent(self): + if self.parent: + return f"#include <monitors/{self.parent}/{self.parent}.h>\n" + return "" + + def fill_tracepoint_handlers_skel(self): + return "NotImplemented" + + def fill_tracepoint_attach_probe(self): + return "NotImplemented" + + def fill_tracepoint_detach_helper(self): + return "NotImplemented" + + def fill_main_c(self): + main_c = self.main_c + 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("%%MODEL_NAME%%", self.name) + 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(self): + return "NotImplemented" + + def fill_monitor_class_type(self): + return "NotImplemented" + + def fill_monitor_class(self): + return "NotImplemented" + + def fill_tracepoint_args_skel(self, tp_type): + return "NotImplemented" + + def fill_monitor_deps(self): + buff = [] + buff.append(" # XXX: add dependencies if there") + if self.parent: + buff.append(f" depends on RV_MON_{self.parent.upper()}") + buff.append(" default y") + return '\n'.join(buff) + + 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 _patch_file(self, file, marker, line): + assert self.auto_patch + 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", + f"// Add new monitors based on CONFIG_{monitor_class_type} here", + f"#include <monitors/{self.name}/{self.name}_trace.h>") + return f" - Patching {self.rv_dir}/rv_trace.h, double check the result" + + return f""" - Edit {self.rv_dir}/rv_trace.h: +Add this line where other tracepoints are included and {monitor_class_type} is defined: +#include <monitors/{self.name}/{self.name}_trace.h> +""" + + def _kconfig_marker(self, container=None) -> str: + return f"# Add new {container + ' ' if container else ''}monitors here" + + def fill_kconfig_tooltip(self): + if self.auto_patch: + # monitors with a container should stay together in the Kconfig + self._patch_file("Kconfig", + self._kconfig_marker(self.parent), + f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"") + return f" - Patching {self.rv_dir}/Kconfig, double check the result" + + return f""" - Edit {self.rv_dir}/Kconfig: +Add this line where other monitors are included: +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\" +""" + + def fill_makefile_tooltip(self): + name = self.name + name_up = name.upper() + if self.auto_patch: + self._patch_file("Makefile", + "# Add new monitors here", + f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o") + return f" - Patching {self.rv_dir}/Makefile, double check the result" + + return f""" - Edit {self.rv_dir}/Makefile: +Add this line where other monitors are included: +obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o +""" + + def fill_monitor_tooltip(self): + if self.auto_patch: + return f" - Monitor created in {self.rv_dir}/monitors/{self.name}" + return f" - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)" + + 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 + + def __write_file(self, file_name, content): + with open(file_name, 'w') as file: + file.write(content) + + def _create_file(self, file_name, content): + path = f"{self.name}/{file_name}" + if self.auto_patch: + path = os.path.join(self.rv_dir, "monitors", path) + self.__write_file(path, content) + + def print_files(self): + main_c = self.fill_main_c() + + self.__create_directory() + + path = f"{self.name}.c" + self._create_file(path, main_c) + + model_h = self.fill_model_h() + path = f"{self.name}.h" + self._create_file(path, model_h) + + kconfig = self.fill_kconfig() + self._create_file("Kconfig", kconfig) + + +class Monitor(RVGenerator): + monitor_types = {"global": 1, "per_cpu": 2, "per_task": 3, "per_obj": 4} + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.trace_h = self._read_template_file("trace.h") + + 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") + tracepoint_args_skel_error_env = self.fill_tracepoint_args_skel("error_env") + 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) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%", tracepoint_args_skel_error_env) + return trace_h + + def print_files(self): + super().print_files() + trace_h = self.fill_trace_h() + path = f"{self.name}_trace.h" + self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000000..7f538598a868 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,567 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Implementation based on +# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). +# Simple On-the-fly Automatic Verification of Linear Temporal Logic. +# https://doi.org/10.1007/978-0-387-34892-6_1 +# With extra optimizations + +from ply.lex import lex +from ply.yacc import yacc +from .automata import AutomataError + +# Grammar: +# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl +# +# Operands (opd): +# true, false, user-defined names +# +# Unary Operators (unop): +# always +# eventually +# next +# not +# +# Binary Operators (binop): +# until +# and +# or +# imply +# equivalent + +tokens = ( + 'AND', + 'OR', + 'IMPLY', + 'UNTIL', + 'ALWAYS', + 'EVENTUALLY', + 'NEXT', + 'VARIABLE', + 'LITERAL', + 'NOT', + 'LPAREN', + 'RPAREN', + 'ASSIGN', +) + +t_AND = r'and' +t_OR = r'or' +t_IMPLY = r'imply' +t_UNTIL = r'until' +t_ALWAYS = r'always' +t_NEXT = r'next' +t_EVENTUALLY = r'eventually' +t_VARIABLE = r'[A-Z_0-9]+' +t_LITERAL = r'true|false' +t_NOT = r'not' +t_LPAREN = r'\(' +t_RPAREN = r'\)' +t_ASSIGN = r'=' +t_ignore_COMMENT = r'\#.*' +t_ignore = ' \t\n' + +def t_error(t): + raise AutomataError(f"Illegal character '{t.value[0]}'") + +lexer = lex() + +class GraphNode: + uid = 0 + + def __init__(self, incoming: set['GraphNode'], new, old, _next): + self.init = False + self.outgoing = set() + self.labels = set() + self.incoming = incoming.copy() + self.new = new.copy() + self.old = old.copy() + self.next = _next.copy() + self.id = GraphNode.uid + GraphNode.uid += 1 + + def expand(self, node_set): + if not self.new: + for nd in node_set: + if nd.old == self.old and nd.next == self.next: + nd.incoming |= self.incoming + return node_set + + new_current_node = GraphNode({self}, self.next, set(), set()) + return new_current_node.expand({self} | node_set) + n = self.new.pop() + return n.expand(self, node_set) + + def __lt__(self, other): + return self.id < other.id + +class ASTNode: + uid = 1 + + def __init__(self, op): + self.op = op + self.id = ASTNode.uid + ASTNode.uid += 1 + + def __hash__(self): + return hash(self.op) + + def __eq__(self, other): + return self is other + + def __iter__(self): + yield self + yield from self.op + + def negate(self): + self.op = self.op.negate() + return self + + def expand(self, node, node_set): + return self.op.expand(self, node, node_set) + + def __str__(self): + if isinstance(self.op, Literal): + return str(self.op.value) + if isinstance(self.op, Variable): + return self.op.name.lower() + return "val" + str(self.id) + + def normalize(self): + # Get rid of: + # - ALWAYS + # - EVENTUALLY + # - IMPLY + # And move all the NOT to be inside + self.op = self.op.normalize() + return self + +class BinaryOp: + op_str = "not_supported" + + def __init__(self, left: ASTNode, right: ASTNode): + self.left = left + self.right = right + + def __hash__(self): + return hash((self.left, self.right)) + + def __iter__(self): + yield from self.left + yield from self.right + + def normalize(self): + raise NotImplementedError + + def negate(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.left.op.is_temporal(): + return True + if self.right.op.is_temporal(): + return True + return self._is_temporal() + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + raise NotImplementedError + +class AndOp(BinaryOp): + op_str = '&&' + + def normalize(self): + return self + + def negate(self): + return OrOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old.add(n) + return node.expand(node_set) + + tmp = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return tmp.expand(node_set) + +class OrOp(BinaryOp): + op_str = '||' + + def normalize(self): + return self + + def negate(self): + return AndOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old |= {n} + return node.expand(node_set) + + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class UntilOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return VOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class VOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return UntilOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class ImplyOp(BinaryOp): + def normalize(self): + # P -> Q === !P | Q + return OrOp(self.left.negate(), self.right) + + def _is_temporal(self): + return False + + def negate(self): + # !(P -> Q) === !(!P | Q) === P & !Q + return AndOp(self.left, self.right.negate()) + +class UnaryOp: + def __init__(self, child: ASTNode): + self.child = child + + def __iter__(self): + yield from self.child + + def __hash__(self): + return hash(self.child) + + def normalize(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.child.op.is_temporal(): + return True + return self._is_temporal() + + def negate(self): + raise NotImplementedError + +class EventuallyOp(UnaryOp): + def __str__(self): + return "eventually " + str(self.child) + + def normalize(self): + # <>F == true U F + return UntilOp(ASTNode(Literal(True)), self.child) + + def _is_temporal(self): + return True + + def negate(self): + # !<>F == [](!F) + return AlwaysOp(self.child.negate()).normalize() + +class AlwaysOp(UnaryOp): + def normalize(self): + # []F === !(true U !F) == false V F + new = ASTNode(Literal(False)) + return VOp(new, self.child) + + def _is_temporal(self): + return True + + def negate(self): + # ![]F == <>(!F) + return EventuallyOp(self.child.negate()).normalize() + +class NextOp(UnaryOp): + def normalize(self): + return self + + def _is_temporal(self): + return True + + def negate(self): + # not (next A) == next (not A) + self.child = self.child.negate() + return self + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + tmp = GraphNode(node.incoming, + node.new, + node.old | {n}, + node.next | {n.op.child}) + return tmp.expand(node_set) + +class NotOp(UnaryOp): + def __str__(self): + return "!" + str(self.child) + + def normalize(self): + return self.child.op.negate() + + def negate(self): + return self.child.op + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if n.op.child is f: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Variable: + def __init__(self, name: str): + self.name = name + + def __hash__(self): + return hash(self.name) + + def __iter__(self): + yield from () + + def negate(self): + new = ASTNode(self) + return NotOp(new) + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if isinstance(f.op, NotOp) and f.op.child is n: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Literal: + def __init__(self, value: bool): + self.value = value + + def __iter__(self): + yield from () + + def __hash__(self): + return hash(self.value) + + def __str__(self): + if self.value: + return "true" + return "false" + + def negate(self): + self.value = not self.value + return self + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.value: + return node_set + node.old |= {n} + return node.expand(node_set) + +def p_spec(p): + ''' + spec : assign + | assign spec + ''' + if len(p) == 3: + p[2].append(p[1]) + p[0] = p[2] + else: + p[0] = [p[1]] + +def p_assign(p): + ''' + assign : VARIABLE ASSIGN ltl + ''' + p[0] = (p[1], p[3]) + +def p_ltl(p): + ''' + ltl : opd + | binop + | unop + ''' + p[0] = p[1] + +def p_opd(p): + ''' + opd : VARIABLE + | LITERAL + | LPAREN ltl RPAREN + ''' + if p[1] == "true": + p[0] = ASTNode(Literal(True)) + elif p[1] == "false": + p[0] = ASTNode(Literal(False)) + elif p[1] == '(': + p[0] = p[2] + else: + p[0] = ASTNode(Variable(p[1])) + +def p_unop(p): + ''' + unop : ALWAYS ltl + | EVENTUALLY ltl + | NEXT ltl + | NOT ltl + ''' + if p[1] == "always": + op = AlwaysOp(p[2]) + elif p[1] == "eventually": + op = EventuallyOp(p[2]) + elif p[1] == "next": + op = NextOp(p[2]) + elif p[1] == "not": + op = NotOp(p[2]) + else: + raise AutomataError(f"Invalid unary operator {p[1]}") + + p[0] = ASTNode(op) + +def p_binop(p): + ''' + binop : opd UNTIL ltl + | opd AND ltl + | opd OR ltl + | opd IMPLY ltl + ''' + if p[2] == "and": + op = AndOp(p[1], p[3]) + elif p[2] == "until": + op = UntilOp(p[1], p[3]) + elif p[2] == "or": + op = OrOp(p[1], p[3]) + elif p[2] == "imply": + op = ImplyOp(p[1], p[3]) + else: + raise AutomataError(f"Invalid binary operator {p[2]}") + + p[0] = ASTNode(op) + +parser = yacc() + +def parse_ltl(s: str) -> ASTNode: + spec = parser.parse(s) + + rule = None + subexpr = {} + + for assign in spec: + if assign[0] == "RULE": + rule = assign[1] + else: + subexpr[assign[0]] = assign[1] + + if rule is None: + raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format") + + for node in rule: + if not isinstance(node.op, Variable): + continue + replace = subexpr.get(node.op.name) + if replace is not None: + node.op = replace.op + + return rule + +def create_graph(s: str): + atoms = set() + + ltl = parse_ltl(s) + for c in ltl: + c.normalize() + if isinstance(c.op, Variable): + atoms.add(c.op.name) + + init = GraphNode(set(), set(), set(), set()) + head = GraphNode({init}, {ltl}, set(), set()) + graph = sorted(head.expand(set())) + + for i, node in enumerate(graph): + # The id assignment during graph generation has gaps. Reassign them + node.id = i + + for incoming in node.incoming: + if incoming is init: + node.init = True + else: + incoming.outgoing.add(node) + for o in node.old: + if not o.op.is_temporal(): + node.labels.add(str(o)) + + return sorted(atoms), graph, ltl diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py new file mode 100644 index 000000000000..81fd1f5ea5ea --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,277 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba +from .automata import AutomataError + +COLUMN_LIMIT = 100 + +def line_len(line: str) -> int: + tabs = line.count('\t') + return tabs * 7 + len(line) + +def break_long_line(line: str, indent='') -> list[str]: + result = [] + while line_len(line) > COLUMN_LIMIT: + i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ') + result.append(line[:i]) + line = indent + line[i + 1:] + if line: + result.append(line) + return result + +def build_condition_string(node: ltl2ba.GraphNode): + if not node.labels: + return "(true)" + + result = "(" + + first = True + for label in sorted(node.labels): + if not first: + result += " && " + result += label + first = False + + result += ")" + + return result + +def abbreviate_atoms(atoms: list[str]) -> list[str]: + def shorten(s: str) -> str: + skip = ["is", "by", "or", "and"] + return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip]) + + def find_share_length(atom: str) -> int: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + return i + return 0 + + abbrs = [] + for atom in atoms: + share_len = find_share_length(atom) + share = atom[:share_len] + unique = atom[share_len:] + abbrs.append((shorten(share) + shorten(unique))) + return abbrs + +class ltl2k(generator.Monitor): + template_dir = "ltl2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + if MonitorType != "per_task": + raise NotImplementedError("Only per_task monitor is supported for LTL") + super().__init__(extra_params) + try: + with open(file_path) as f: + self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read()) + except OSError as exc: + raise AutomataError(exc.strerror) from exc + self.atoms_abbr = abbreviate_atoms(self.atoms) + self.name = extra_params.get("model_name") + if not self.name: + self.name = Path(file_path).stem + + def _fill_states(self) -> list[str]: + buf = [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append(f"\tS{node.id},") + buf.append("\tRV_NUM_BA_STATES") + buf.append("};") + buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);") + return buf + + def _fill_atoms(self): + buf = ["enum ltl_atom {"] + for a in sorted(self.atoms): + buf.append(f"\tLTL_{a},") + buf.append("\tLTL_NUM_ATOM") + buf.append("};") + buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);") + return buf + + def _fill_atoms_to_string(self): + buf = [ + "static const char *ltl_atom_str(enum ltl_atom atom)", + "{", + "\tstatic const char *const names[] = {" + ] + + for name in self.atoms_abbr: + buf.append(f"\t\t\"{name}\",") + + buf.extend([ + "\t};", + "", + "\treturn names[atom];", + "}" + ]) + return buf + + def _fill_atom_values(self, required_values): + buf = [] + for node in self.ltl: + if str(node) not in required_values: + continue + + if isinstance(node.op, ltl2ba.AndOp): + buf.append(f"\tbool {node} = {node.op.left} && {node.op.right};") + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.OrOp): + buf.append(f"\tbool {node} = {node.op.left} || {node.op.right};") + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.NotOp): + buf.append(f"\tbool {node} = !{node.op.child};") + required_values.add(str(node.op.child)) + + for atom in self.atoms: + if atom.lower() not in required_values: + continue + buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);") + + buf.reverse() + + buf2 = [] + for line in buf: + buf2.extend(break_long_line(line, "\t ")) + return buf2 + + def _fill_transitions(self): + buf = [ + "static void", + "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)", + "{" + ] + + required_values = set() + for node in self.ba: + for o in sorted(node.outgoing): + required_values |= o.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.extend([ + "", + "\tswitch (state) {" + ]) + + for node in self.ba: + buf.append(f"\tcase S{node.id}:") + + for o in sorted(node.outgoing): + line = "\t\tif " + indent = "\t\t " + + line += build_condition_string(o) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append(f"\t\t\t__set_bit(S{o.id}, next);") + buf.append("\t\tbreak;") + buf.extend([ + "\t}", + "}" + ]) + + return buf + + def _fill_start(self): + buf = [ + "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)", + "{" + ] + + required_values = set() + for node in self.ba: + if node.init: + required_values |= node.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.append("") + + for node in self.ba: + if not node.init: + continue + + line = "\tif " + indent = "\t " + + line += build_condition_string(node) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append(f"\t\t__set_bit(S{node.id}, mon->states);") + buf.append("}") + return buf + + def fill_tracepoint_handlers_skel(self): + buff = [] + buff.append("static void handle_example_event(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);") + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);" + + def fill_tracepoint_detach_helper(self): + return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_sample_event);" + + def fill_atoms_init(self): + buff = [] + for a in self.atoms: + buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);") + return '\n'.join(buff) + + def fill_model_h(self): + buf = [ + "/* SPDX-License-Identifier: GPL-2.0 */", + "", + "/*", + " * C implementation of Buchi automaton, automatically generated by", + " * tools/verification/rvgen from the linear temporal logic specification.", + " * For further information, see kernel documentation:", + " * Documentation/trace/rv/linear_temporal_logic.rst", + " */", + "", + "#include <linux/rv.h>", + "", + "#define MONITOR_NAME " + self.name, + "" + ] + + buf.extend(self._fill_atoms()) + buf.append('') + + buf.extend(self._fill_atoms_to_string()) + buf.append('') + + buf.extend(self._fill_states()) + buf.append('') + + buf.extend(self._fill_start()) + buf.append('') + + buf.extend(self._fill_transitions()) + buf.append('') + + return '\n'.join(buf) + + def fill_monitor_class_type(self): + return "LTL_MON_EVENTS_ID" + + def fill_monitor_class(self): + return "ltl_monitor_id" + + def fill_main_c(self): + main_c = super().fill_main_c() + main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + + return main_c diff --git a/tools/verification/rvgen/rvgen/templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig new file mode 100644 index 000000000000..291b29ea28db --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/Kconfig @@ -0,0 +1,9 @@ +# 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/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig index 90cdc1e9379e..a606111949c2 100644 --- a/tools/verification/dot2/dot2k_templates/Kconfig +++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig @@ -1,6 +1,5 @@ config RV_MON_%%MODEL_NAME_UP%% depends on RV - select %%MONITOR_CLASS_TYPE%% bool "%%MODEL_NAME%% monitor" help %%DESCRIPTION%% diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c new file mode 100644 index 000000000000..5fc89b46f279 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -0,0 +1,35 @@ +// 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%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = NULL, + .disable = NULL, + .reset = NULL, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); +} + +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/rvgen/rvgen/templates/container/main.h b/tools/verification/rvgen/rvgen/templates/container/main.h new file mode 100644 index 000000000000..0f6883ab4bcc --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_%%MODEL_NAME%%; diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c index 9605ca994416..bf0999f6657a 100644 --- a/tools/verification/dot2/dot2k_templates/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -6,7 +6,6 @@ #include <linux/init.h> #include <linux/rv.h> #include <rv/instrumentation.h> -#include <rv/da_monitor.h> #define MODULE_NAME "%%MODEL_NAME%%" @@ -15,20 +14,14 @@ * #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. */ +#define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%% #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%%); +#include <rv/%%MONITOR_CLASS%%_monitor.h> /* * This is the instrumentation part of the monitor. @@ -42,7 +35,7 @@ static int enable_%%MODEL_NAME%%(void) { int retval; - retval = da_monitor_init_%%MODEL_NAME%%(); + retval = da_monitor_init(); if (retval) return retval; @@ -53,34 +46,33 @@ static int enable_%%MODEL_NAME%%(void) static void disable_%%MODEL_NAME%%(void) { - rv_%%MODEL_NAME%%.enabled = 0; + rv_this.enabled = 0; %%TRACEPOINT_DETACH%% - da_monitor_destroy_%%MODEL_NAME%%(); + da_monitor_destroy(); } /* * This is the monitor register section. */ -static struct rv_monitor rv_%%MODEL_NAME%% = { +static struct rv_monitor rv_this = { .name = "%%MODEL_NAME%%", .description = "%%DESCRIPTION%%", .enable = enable_%%MODEL_NAME%%, .disable = disable_%%MODEL_NAME%%, - .reset = da_monitor_reset_all_%%MODEL_NAME%%, + .reset = da_monitor_reset_all, .enabled = 0, }; static int __init register_%%MODEL_NAME%%(void) { - rv_register_monitor(&rv_%%MODEL_NAME%%); - return 0; + return rv_register_monitor(&rv_this, %%PARENT%%); } static void __exit unregister_%%MODEL_NAME%%(void) { - rv_unregister_monitor(&rv_%%MODEL_NAME%%); + rv_unregister_monitor(&rv_this); } module_init(register_%%MODEL_NAME%%); diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h index 87d3a1308926..87d3a1308926 100644 --- a/tools/verification/dot2/dot2k_templates/trace.h +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h new file mode 100644 index 000000000000..c8290e9ba2f4 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h @@ -0,0 +1,16 @@ +/* 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%%); + +DEFINE_EVENT(error_env_%%MONITOR_CLASS%%, error_env_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c new file mode 100644 index 000000000000..f85d076fbf78 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -0,0 +1,102 @@ +// 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> + +#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" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + /* + * This is called everytime the Buchi automaton is triggered. + * + * This function could be used to fetch the atomic propositions which + * are expensive to trace. It is possible only if the atomic proposition + * does not need to be updated at precise time. + * + * It is recommended to use tracepoints and ltl_atom_update() instead. + */ +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + /* + * This should initialize as many atomic propositions as possible. + * + * @task_creation indicates whether the task is being created. This is + * false if the task is already running before the monitor is enabled. + */ +%%ATOMS_INIT%% +} + +/* + * 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 = ltl_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ +%%TRACEPOINT_DETACH%% + + ltl_monitor_destroy(); +} + +/* + * 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%%, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +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(/* TODO */); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h new file mode 100644 index 000000000000..49394c4b0f1c --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -0,0 +1,14 @@ +/* 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%%, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ |