summaryrefslogtreecommitdiffstats
path: root/tools/verification
diff options
context:
space:
mode:
authorDaniel Baumann <daniel.baumann@progress-linux.org>2024-04-07 18:49:45 +0000
committerDaniel Baumann <daniel.baumann@progress-linux.org>2024-04-07 18:49:45 +0000
commit2c3c1048746a4622d8c89a29670120dc8fab93c4 (patch)
tree848558de17fb3008cdf4d861b01ac7781903ce39 /tools/verification
parentInitial commit. (diff)
downloadlinux-2c3c1048746a4622d8c89a29670120dc8fab93c4.tar.xz
linux-2c3c1048746a4622d8c89a29670120dc8fab93c4.zip
Adding upstream version 6.1.76.upstream/6.1.76
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'tools/verification')
-rw-r--r--tools/verification/dot2/Makefile26
-rw-r--r--tools/verification/dot2/automata.py174
-rw-r--r--tools/verification/dot2/dot2c26
-rw-r--r--tools/verification/dot2/dot2c.py254
-rw-r--r--tools/verification/dot2/dot2k47
-rw-r--r--tools/verification/dot2/dot2k.py177
-rw-r--r--tools/verification/dot2/dot2k_templates/main_global.c91
-rw-r--r--tools/verification/dot2/dot2k_templates/main_per_cpu.c91
-rw-r--r--tools/verification/dot2/dot2k_templates/main_per_task.c91
-rw-r--r--tools/verification/models/wip.dot16
-rw-r--r--tools/verification/models/wwnr.dot16
11 files changed, 1009 insertions, 0 deletions
diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile
new file mode 100644
index 000000000..021beb07a
--- /dev/null
+++ b/tools/verification/dot2/Makefile
@@ -0,0 +1,26 @@
+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
new file mode 100644
index 000000000..baffeb960
--- /dev/null
+++ b/tools/verification/dot2/automata.py
@@ -0,0 +1,174 @@
+#!/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):
+ self.__dot_path = file_path
+ self.name = 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()
+
+ def __get_model_name(self):
+ basename = ntpath.basename(self.__dot_path)
+ if basename.endswith(".dot") == False:
+ print("not a dot file")
+ raise Exception("not a dot file: %s" % self.__dot_path)
+
+ model_name = basename[0:-4]
+ 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 self.__dot_lines[cursor].__contains__("doublecircle") == True:
+ final_states.append(state)
+ has_final_states = True
+
+ if self.__dot_lines[cursor].__contains__("ellipse") == True:
+ 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 has_final_states == False:
+ 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][1] == '"':
+ # 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][1] == '"':
+ 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
diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c
new file mode 100644
index 000000000..3fe89ab88
--- /dev/null
+++ b/tools/verification/dot2/dot2c
@@ -0,0 +1,26 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
+#
+# dot2c: parse an automata in dot file digraph format into a C
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# For further information, see:
+# Documentation/trace/rv/deterministic_automata.rst
+
+if __name__ == '__main__':
+ from dot2 import dot2c
+ import argparse
+ import sys
+
+ parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+ parser.add_argument('dot_file', help='The dot file to be converted')
+
+ args = parser.parse_args()
+ d = dot2c.Dot2c(args.dot_file)
+ d.print_model_classic()
diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2c.py
new file mode 100644
index 000000000..be8a364a4
--- /dev/null
+++ b/tools/verification/dot2/dot2c.py
@@ -0,0 +1,254 @@
+#!/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):
+ super().__init__(file_path)
+ 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 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
new file mode 100644
index 000000000..9dcd38abe
--- /dev/null
+++ b/tools/verification/dot2/dot2k
@@ -0,0 +1,47 @@
+#!/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
+ import sys
+ import argparse
+
+ 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)
+ params = parser.parse_args()
+
+ print("Opening and parsing the dot file %s" % params.dot_file)
+ try:
+ monitor=dot2k(params.dot_file, params.monitor_type)
+ except Exception as e:
+ print('Error: '+ str(e))
+ print("Sorry : :-(")
+ sys.exit(1)
+
+ # easier than using argparse action.
+ if params.model_name != None:
+ print(params.model_name)
+
+ 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(" - Edit include/trace/events/rv.h to add the tracepoint entry")
+ print(" - Move it to the kernel's monitor directory")
+ print(" - Edit kernel/trace/rv/Makefile")
+ print(" - Edit kernel/trace/rv/Kconfig")
diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py
new file mode 100644
index 000000000..016550fcc
--- /dev/null
+++ b/tools/verification/dot2/dot2k.py
@@ -0,0 +1,177 @@
+#!/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 = "dot2k/rv_templates/"
+ monitor_type = "per_cpu"
+
+ def __init__(self, file_path, MonitorType):
+ super().__init__(file_path)
+
+ self.monitor_type = self.monitor_types.get(MonitorType)
+ if self.monitor_type == None:
+ raise Exception("Unknown monitor type: %s" % MonitorType)
+
+ self.monitor_type = MonitorType
+ self.__fill_rv_templates_dir()
+ self.main_c = self.__open_file(self.monitor_templates_dir + "main_" + MonitorType + ".c")
+ self.enum_suffix = "_%s" % self.name
+
+ def __fill_rv_templates_dir(self):
+
+ if os.path.exists(self.monitor_templates_dir) == True:
+ return
+
+ if platform.system() != "Linux":
+ raise Exception("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) == True:
+ self.monitor_templates_dir = kernel_path
+ return
+
+ if os.path.exists("/usr/share/dot2/dot2k_templates/") == True:
+ self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/"
+ return
+
+ raise Exception("Could not find the template directory, do you have the kernel source installed?")
+
+
+ def __open_file(self, path):
+ try:
+ fd = open(path)
+ except OSError:
+ raise Exception("Cannot open the file: %s" % path)
+
+ content = fd.read()
+
+ 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_tracepoint_handlers_skel(self):
+ buff = []
+ for event in self.events:
+ buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event)
+ buff.append("{")
+ if self.monitor_type == "per_task":
+ buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;");
+ buff.append("\tda_handle_event_%s(p, %s%s);" % (self.name, event, self.enum_suffix));
+ else:
+ buff.append("\tda_handle_event_%s(%s%s);" % (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
+ min_type = self.get_minimun_type()
+ nr_events = self.events.__len__()
+ 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("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)
+
+ 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 __create_directory(self):
+ try:
+ os.mkdir(self.name)
+ except FileExistsError:
+ return
+ except:
+ print("Fail creating the output dir: %s" % self.name)
+
+ def __create_file(self, file_name, content):
+ path = "%s/%s" % (self.name, file_name)
+ try:
+ file = open(path, 'w')
+ except FileExistsError:
+ return
+ except:
+ print("Fail creating file: %s" % path)
+
+ file.write(content)
+
+ file.close()
+
+ def __get_main_name(self):
+ path = "%s/%s" % (self.name, "main.c")
+ if os.path.exists(path) == False:
+ 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)
diff --git a/tools/verification/dot2/dot2k_templates/main_global.c b/tools/verification/dot2/dot2k_templates/main_global.c
new file mode 100644
index 000000000..a5658bfb9
--- /dev/null
+++ b/tools/verification/dot2/dot2k_templates/main_global.c
@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <trace/events/sched.h>
+ */
+#include <trace/events/rv.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "MODEL_NAME.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+static struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_GLOBAL(MODEL_NAME, MIN_TYPE);
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+TRACEPOINT_HANDLERS_SKEL
+static int enable_MODEL_NAME(void)
+{
+ int retval;
+
+ retval = da_monitor_init_MODEL_NAME();
+ if (retval)
+ return retval;
+
+TRACEPOINT_ATTACH
+
+ return 0;
+}
+
+static void disable_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+
+TRACEPOINT_DETACH
+
+ da_monitor_destroy_MODEL_NAME();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .enable = enable_MODEL_NAME,
+ .disable = disable_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+static int __init register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+static void __exit unregister_MODEL_NAME(void)
+{
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/verification/dot2/dot2k_templates/main_per_cpu.c b/tools/verification/dot2/dot2k_templates/main_per_cpu.c
new file mode 100644
index 000000000..03539a976
--- /dev/null
+++ b/tools/verification/dot2/dot2k_templates/main_per_cpu.c
@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <linux/trace/events/sched.h>
+ */
+#include <trace/events/rv.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "MODEL_NAME.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+static struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_PER_CPU(MODEL_NAME, MIN_TYPE);
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+TRACEPOINT_HANDLERS_SKEL
+static int enable_MODEL_NAME(void)
+{
+ int retval;
+
+ retval = da_monitor_init_MODEL_NAME();
+ if (retval)
+ return retval;
+
+TRACEPOINT_ATTACH
+
+ return 0;
+}
+
+static void disable_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+
+TRACEPOINT_DETACH
+
+ da_monitor_destroy_MODEL_NAME();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .enable = enable_MODEL_NAME,
+ .disable = disable_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+static int __init register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+static void __exit unregister_MODEL_NAME(void)
+{
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/verification/dot2/dot2k_templates/main_per_task.c b/tools/verification/dot2/dot2k_templates/main_per_task.c
new file mode 100644
index 000000000..ffd92af87
--- /dev/null
+++ b/tools/verification/dot2/dot2k_templates/main_per_task.c
@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "MODEL_NAME"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <linux/trace/events/sched.h>
+ */
+#include <trace/events/rv.h>
+
+/*
+ * This is the self-generated part of the monitor. Generally, there is no need
+ * to touch this section.
+ */
+#include "MODEL_NAME.h"
+
+/*
+ * Declare the deterministic automata monitor.
+ *
+ * The rv monitor reference is needed for the monitor declaration.
+ */
+static struct rv_monitor rv_MODEL_NAME;
+DECLARE_DA_MON_PER_TASK(MODEL_NAME, MIN_TYPE);
+
+/*
+ * This is the instrumentation part of the monitor.
+ *
+ * This is the section where manual work is required. Here the kernel events
+ * are translated into model's event.
+ *
+ */
+TRACEPOINT_HANDLERS_SKEL
+static int enable_MODEL_NAME(void)
+{
+ int retval;
+
+ retval = da_monitor_init_MODEL_NAME();
+ if (retval)
+ return retval;
+
+TRACEPOINT_ATTACH
+
+ return 0;
+}
+
+static void disable_MODEL_NAME(void)
+{
+ rv_MODEL_NAME.enabled = 0;
+
+TRACEPOINT_DETACH
+
+ da_monitor_destroy_MODEL_NAME();
+}
+
+/*
+ * This is the monitor register section.
+ */
+static struct rv_monitor rv_MODEL_NAME = {
+ .name = "MODEL_NAME",
+ .description = "auto-generated MODEL_NAME",
+ .enable = enable_MODEL_NAME,
+ .disable = disable_MODEL_NAME,
+ .reset = da_monitor_reset_all_MODEL_NAME,
+ .enabled = 0,
+};
+
+static int __init register_MODEL_NAME(void)
+{
+ rv_register_monitor(&rv_MODEL_NAME);
+ return 0;
+}
+
+static void __exit unregister_MODEL_NAME(void)
+{
+ rv_unregister_monitor(&rv_MODEL_NAME);
+}
+
+module_init(register_MODEL_NAME);
+module_exit(unregister_MODEL_NAME);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("MODEL_NAME");
diff --git a/tools/verification/models/wip.dot b/tools/verification/models/wip.dot
new file mode 100644
index 000000000..2a53a9700
--- /dev/null
+++ b/tools/verification/models/wip.dot
@@ -0,0 +1,16 @@
+digraph state_automaton {
+ {node [shape = circle] "non_preemptive"};
+ {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
+ {node [shape = doublecircle] "preemptive"};
+ {node [shape = circle] "preemptive"};
+ "__init_preemptive" -> "preemptive";
+ "non_preemptive" [label = "non_preemptive"];
+ "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
+ "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
+ "preemptive" [label = "preemptive"];
+ "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
+ { rank = min ;
+ "__init_preemptive";
+ "preemptive";
+ }
+}
diff --git a/tools/verification/models/wwnr.dot b/tools/verification/models/wwnr.dot
new file mode 100644
index 000000000..1b206e831
--- /dev/null
+++ b/tools/verification/models/wwnr.dot
@@ -0,0 +1,16 @@
+digraph state_automaton {
+ {node [shape = plaintext, style=invis, label=""] "__init_not_running"};
+ {node [shape = ellipse] "not_running"};
+ {node [shape = plaintext] "not_running"};
+ {node [shape = plaintext] "running"};
+ "__init_not_running" -> "not_running";
+ "not_running" [label = "not_running", color = green3];
+ "not_running" -> "not_running" [ label = "wakeup" ];
+ "not_running" -> "running" [ label = "switch_in" ];
+ "running" [label = "running"];
+ "running" -> "not_running" [ label = "switch_out" ];
+ { rank = min ;
+ "__init_not_running";
+ "not_running";
+ }
+}