diff options
Diffstat (limited to 'tools/verification')
91 files changed, 4662 insertions, 660 deletions
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl index 6f26c4810f78..4d78fdd204c0 100644 --- a/tools/verification/models/rtapp/sleep.ltl +++ b/tools/verification/models/rtapp/sleep.ltl @@ -1,7 +1,7 @@ -RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) +RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) -RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) - and ((not WAKE) until RT_FRIENDLY_WAKE) +RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON + and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE) RT_VALID_SLEEP_REASON = FUTEX_WAIT or RT_FRIENDLY_NANOSLEEP @@ -9,15 +9,12 @@ RT_VALID_SLEEP_REASON = FUTEX_WAIT RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP and NANOSLEEP_TIMER_ABSTIME - and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI) + and not NANOSLEEP_CLOCK_REALTIME 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/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl new file mode 100644 index 000000000000..a5d63ca0811a --- /dev/null +++ b/tools/verification/models/rtapp/wakeup.ltl @@ -0,0 +1,5 @@ +RULE = always (((RT and USER_THREAD) imply + (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST)) + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile index 5b898360ba48..8ae5fc0d1d17 100644 --- a/tools/verification/rv/Makefile +++ b/tools/verification/rv/Makefile @@ -78,4 +78,7 @@ clean: doc_clean fixdep-clean $(Q)rm -f rv rv-static fixdep FEATURE-DUMP rv-* $(Q)rm -rf feature -.PHONY: FORCE clean +check: $(RV) + RV=$(RV) prove -o --directives -f tests/ + +.PHONY: FORCE clean check diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index 4bb746ea6e17..e6dea4040f8f 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -58,38 +58,40 @@ static int __ikm_read_enable(char *monitor_name) */ 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; + char *available_monitors, *cursor, *line; + int len = strlen(monitor_name); + int found = 0; 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; - } + config_is_container = 0; + cursor = available_monitors; + while ((line = strsep(&cursor, "\n"))) { + char *colon = strchr(line, ':'); - 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; + if (strcmp(line, monitor_name) && (!colon || strcmp(colon + 1, monitor_name))) + continue; + + strncpy(out_name, line, 2 * MAX_DA_NAME_LEN); + out_name[2 * MAX_DA_NAME_LEN - 1] = '\0'; + + if (colon) { + out_name[colon - line] = '/'; + } else { + /* If there are children, they are on the next line. */ + line = strsep(&cursor, "\n"); + if (line && !strncmp(line, monitor_name, len) && line[len] == ':') + config_is_container = 1; + } + + found = 1; + break; } -out_free: free(available_monitors); - return retval; + return found; } /* @@ -191,8 +193,12 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co nested_name = strstr(name, ":"); if (nested_name) { /* it belongs in container if it starts with "container:" */ - if (container && strstr(name, container) != name) - return 1; + if (container) { + int len = strlen(container); + + if (strncmp(name, container, len) || name[len] != ':') + return 1; + } *nested_name = '/'; ++nested_name; ikm->nested = 1; @@ -215,10 +221,11 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *co return -1; } - strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); + strncpy(ikm->name, nested_name, sizeof(ikm->name) - 1); + ikm->name[sizeof(ikm->name) - 1] = '\0'; ikm->enabled = enabled; - strncpy(ikm->desc, desc, MAX_DESCRIPTION); - + strncpy(ikm->desc, desc, sizeof(ikm->desc) - 1); + ikm->desc[sizeof(ikm->desc) - 1] = '\0'; free(desc); return 0; @@ -803,7 +810,7 @@ int ikm_run_monitor(char *monitor_name, int argc, char **argv) if (config_trace) { inst = ikm_setup_trace_instance(nested_name); if (!inst) - return -1; + goto out_free_instance; } retval = ikm_enable(full_name); diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index b8fe24a87d97..09e0d8598619 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -50,23 +50,23 @@ static void rv_list(int argc, char **argv) " [container]: list only monitors in this container", NULL, }; - int i, print_help = 0, retval = 0; + int i, print_help = 0, retval = EXIT_SUCCESS; char *container = NULL; if (argc == 2) { if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { print_help = 1; - retval = 0; + retval = EXIT_SUCCESS; } else if (argv[1][0] == '-') { /* assume invalid option */ print_help = 1; - retval = 1; + retval = EXIT_FAILURE; } else container = argv[1]; } else if (argc > 2) { /* more than 2 is always usage */ print_help = 1; - retval = 1; + retval = EXIT_FAILURE; } if (print_help) { fprintf(stderr, "rv version %s\n", VERSION); @@ -77,7 +77,7 @@ static void rv_list(int argc, char **argv) ikm_list_monitors(container); - exit(0); + exit(EXIT_SUCCESS); } /* @@ -108,14 +108,14 @@ static void rv_mon(int argc, char **argv) for (i = 0; usage[i]; i++) fprintf(stderr, "%s\n", usage[i]); - exit(1); + exit(EXIT_FAILURE); } else if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { fprintf(stderr, "rv version %s\n", VERSION); for (i = 0; usage[i]; i++) fprintf(stderr, "%s\n", usage[i]); - exit(0); + exit(EXIT_SUCCESS); } monitor_name = argv[1]; @@ -127,7 +127,7 @@ static void rv_mon(int argc, char **argv) if (!run) err_msg("rv: monitor %s does not exist\n", monitor_name); - exit(!run); + exit(run > 0 ? EXIT_SUCCESS : EXIT_FAILURE); } static void usage(int exit_val, const char *fmt, ...) @@ -174,13 +174,13 @@ static void usage(int exit_val, const char *fmt, ...) int main(int argc, char **argv) { if (geteuid()) - usage(1, "%s needs root permission", argv[0]); + usage(EXIT_FAILURE, "%s needs root permission", argv[0]); if (argc <= 1) - usage(1, "%s requires a command", argv[0]); + usage(EXIT_FAILURE, "%s requires a command", argv[0]); if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) - usage(0, "help"); + usage(EXIT_SUCCESS, "help"); if (!strcmp(argv[1], "list")) rv_list(--argc, &argv[1]); @@ -197,5 +197,5 @@ int main(int argc, char **argv) } /* invalid sub-command */ - usage(1, "%s does not know the %s command, old version?", argv[0], argv[1]); + usage(EXIT_FAILURE, "%s does not know the %s command, old version?", argv[0], argv[1]); } diff --git a/tools/verification/rv/tests/rv_list.t b/tools/verification/rv/tests/rv_list.t new file mode 100644 index 000000000000..201af33a52cc --- /dev/null +++ b/tools/verification/rv/tests/rv_list.t @@ -0,0 +1,48 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +RVDIR=/sys/kernel/tracing/rv/ + +# Help and basic tests +check "verify help page" \ + "$RV --help" 0 "usage: rv command" + +check "verify list subcommand help" \ + "$RV list --help" 0 "list all available monitors" + +all_nested=$(grep : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +all_non_nested=$(grep -v : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +sched_monitors=$(grep sched: $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +description_state="[[:space:]]\+[[:print:]]\+\[\(OFF\|ON\)\]" +line_nested=" - \($all_nested\)${description_state}" +line_non_nested="\($all_non_nested\)${description_state}" + +# List monitors and containers +check "list all monitors" \ + "$RV list" 0 "" "" "^\($line_nested\|$line_non_nested\)$" + +check_if_exists "list container" \ + "$RV list sched" "$RVDIR/monitors/sched" \ + "" "-- No monitor found in container sched --" \ + "^\($sched_monitors\)${description_state}$" + +check_if_exists "list non-container" \ + "$RV list wwnr" "$RVDIR/monitors/wwnr" \ + "-- No monitor found in container wwnr --" \ + "^\( - \)\?[[:alnum:]]\+${description_state}$" + +check "list incomplete container name" \ + "$RV list s" 0 "-- No monitor found in container s --" + +# Error handling tests +check "no command" \ + "$RV" 1 "rv requires a command" + +check "invalid command" \ + "$RV invalid" 1 "rv does not know the invalid command" + +test_end diff --git a/tools/verification/rv/tests/rv_mon.t b/tools/verification/rv/tests/rv_mon.t new file mode 100644 index 000000000000..cbc346c74c71 --- /dev/null +++ b/tools/verification/rv/tests/rv_mon.t @@ -0,0 +1,95 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +RVDIR=/sys/kernel/tracing/rv/ + +# Help and basic tests +check "verify mon subcommand help" \ + "$RV mon --help" 0 "run a monitor" + +# Error handling tests +check "mon without monitor name" \ + "$RV mon" 1 "usage: rv mon" + +check "invalid monitor name" \ + "$RV mon invalid" 1 "monitor invalid does not exist" + +if [ -d $RVDIR/monitors/wwnr ]; then + +check "invalid reactor name" \ + "$RV mon wwnr -r invalid" 1 "failed to set invalid reactor, is it available?" + +check "monitor name is substring of another monitor" \ + "$RV mon nr" 1 "monitor nr does not exist" + +check "already enabled monitor returns error" \ + "echo 1 > $RVDIR/monitors/wwnr/enable; $RV mon wwnr" 1 \ + "monitor wwnr (in-kernel) is already enabled" +echo 0 > $RVDIR/monitors/wwnr/enable + +fi + +# rv mon runs until terminated +set_expected_timeout 2s + +# Run monitors with different configurations +check_if_exists "run the monitor without parameters" \ + "$RV mon wwnr" "$RVDIR/monitors/wwnr" "" "." + +check_if_exists "run the monitor as verbose" \ + "$RV mon wwnr -v" "$RVDIR/monitors/wwnr" \ + "my pid is \$pid" "\(event\|error\)" + +check_if_exists "run the monitor with a reactor" \ + "$RV mon wwnr -r printk & sleep .5 && cat $RVDIR/monitors/wwnr/reactors && wait" \ + "$RVDIR/monitors/wwnr/reactors" "\[printk\]" + +check_if_exists "reactor is restored after exit" \ + "cat $RVDIR/monitors/wwnr/reactors" \ + "$RVDIR/monitors/wwnr/reactors" "\[nop\]" + +check_if_exists "run a nested monitor with a reactor" \ + "$RV mon snroc -r printk & sleep .5 && cat $RVDIR/monitors/sched/snroc/reactors && wait" \ + "$RVDIR/monitors/sched/snroc/reactors" "\[printk\]" + +check_if_exists "run an explicitly nested monitor with a reactor" \ + "$RV mon sched:sssw -r printk & sleep .5 && cat $RVDIR/monitors/sched/sssw/reactors && wait" \ + "$RVDIR/monitors/sched/sssw/reactors" "\[printk\]" + +check_if_exists "run container monitor" \ + "$RV mon sched & sleep .5 && cat $RVDIR/monitors/sched/{sssw,sco}/enable && wait" \ + "$RVDIR/monitors/sched" "1" "0" "^1$" + +# Regexes for the trace +header="^[[:space:]]\+\(\([][A-Z_x<>-]\+\||\)[[:space:]]*\)\+$" +type="\(event\|error\)[[:space:]]\+" +genpid="[0-9]\+[[:space:]]\+" +selfpid="\$pid[[:space:]]\+" +cpu="\[[0-9]\{3\}\][[:space:]]\+" +state="[a-z_]\+ " +trace_task="${genpid}${cpu}${type}${genpid}${state}" +trace_task_self="${genpid}${cpu}${type}${selfpid}${state}" +trace_cpu="${genpid}${cpu}${type}${state}" +trace_cpu_self="${selfpid}${cpu}${type}${state}" + +check_if_exists "run per-task monitor with tracing" \ + "$RV mon sssw -t" "$RVDIR/monitors/sched/sssw" \ + "$header" "$trace_task_self" "\($header\|$trace_task\)" + +check_if_exists "run per-task monitor tracing also self" \ + "$RV mon sched:sssw -t -s" "$RVDIR/monitors/sched/sssw" \ + "$trace_task_self" "" "\($header\|$trace_task\)" + +check_if_exists "run per-cpu monitor with tracing" \ + "$RV mon sched:sco -t" "$RVDIR/monitors/sched/sco" \ + "$header" "$trace_cpu_self" "\($header\|$trace_cpu\)" + +check_if_exists "run per-cpu monitor tracing also self" \ + "$RV mon sco -t -s" "$RVDIR/monitors/sched/sco" \ + "$trace_cpu_self" "" "\($header\|$trace_cpu\)" + +test_end diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile index cfc4056c1e87..48d0376a5cc4 100644 --- a/tools/verification/rvgen/Makefile +++ b/tools/verification/rvgen/Makefile @@ -13,12 +13,17 @@ all: .PHONY: clean clean: +.PHONY: check +check: + prove -o --directives -f tests/ + .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/kunit.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/kunit.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 diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py index 3be7f85fe37b..246b43fa29f1 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -6,26 +6,30 @@ # dot2k: transform dot files into a monitor for the Linux kernel. # # For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst +# Documentation/trace/rv/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.kunit import KUnit, KUnitError from rvgen.automata import AutomataError + from rvgen.ltl2ba import LTLError 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", + + parent_parser = argparse.ArgumentParser(add_help=False) + parent_parser.add_argument("-D", "--description", dest="description", required=False) + parent_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 = subparsers.add_parser("monitor", parents=[parent_parser]) 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") @@ -36,9 +40,14 @@ if __name__ == '__main__': 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 = subparsers.add_parser("container", parents=[parent_parser]) container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + kunit_parser = subparsers.add_parser("kunit", parents=[parent_parser]) + kunit_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + kunit_parser.add_argument('-l', "--local", dest="local", action="store_true", required=False, + help="Force looking for the monitor in the current directory only") + params = parser.parse_args() try: @@ -53,10 +62,17 @@ if __name__ == '__main__': else: print("Unknown monitor class:", params.monitor_class) sys.exit(1) - else: + elif params.subcmd == "container": monitor = Container(vars(params)) - except AutomataError as e: - print(f"There was an error processing {params.spec}: {e}", file=sys.stderr) + elif params.subcmd == "kunit": + monitor = KUnit(vars(params)) + monitor.print_files() + sys.exit(0) + except (AutomataError, LTLError) as e: + print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr) + sys.exit(1) + except KUnitError as e: + print(f"There was an error generating KUnit files:\n{e}", file=sys.stderr) sys.exit(1) print(f"Writing the monitor into the directory {monitor.name}") diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py index b9f8149f7118..fd37ce304276 100644 --- a/tools/verification/rvgen/rvgen/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -9,22 +9,349 @@ # 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.""" +import lark -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 ParseTree: + # based on https://graphviz.org/doc/info/lang.html + # with the irrelevant stuffs (port and compass) removed + grammar = r''' + start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}" -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)) + stmt_list: (stmt ";"? stmt_list)? + + stmt: node_stmt + | edge_stmt + | attr_stmt + | ID "=" ID + | subgraph + + attr_stmt: attr_type attr_list + + attr_type: "graph" -> graph + | "node" -> node + | "edge" -> edge + + attr_list: "[" a_list? "]" attr_list? + + a_list: ID "=" ID (";" | ",")? a_list? + + edge_stmt: (node_id | subgraph) edgerhs attr_list? + + edgerhs: edgeop (node_id | subgraph) edgerhs? + + edgeop: "->" | "--" + + node_stmt: node_id attr_list? + + node_id: ID + + subgraph: ("subgraph" ID?)? "{" stmt_list "}" + + ID: CNAME + | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/ + | ESCAPED_STRING + + %import common.CNAME + %import common.ESCAPED_STRING + %import common.WS + %ignore WS + ''' + + @staticmethod + def parse_edge(tree: lark.Tree) -> tuple[str, str]: + # only support a simple node-to-node edge + nodes = [] + for node in tree.iter_subtrees_topdown(): + if node.data == "node_id": + nodes.append(node.children[0].strip('"')) + + if len(nodes) != 2: + raise AutomataError("Only state-to-state transition is supported") + + return tuple(nodes) + + class ParseNodes(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.nodes = set() + super().__init__(*args, **kwargs) + + def node_stmt(self, tree): + node_id = tree.children[0] + node = node_id.children[0].strip('"') + self.nodes.add(node) + + class ParseEdges(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.edges = set() + super().__init__(*args, **kwargs) + + def edge_stmt(self, tree): + edge = ParseTree.parse_edge(tree) + self.edges.add(edge) + + class ParseAttributes(lark.visitors.Interpreter): + def __init__(self, *args, **kwargs): + ''' + Stacks of default attributes. [0] is the default + attributes for the outermost scope, while [-1] is the + default attributes for the current scope. + ''' + self.default_node_attrs = [{}] + self.default_edge_attrs = [{}] + + self.node_attrs = {} + self.edge_attrs = {} + + super().__init__(*args, **kwargs) + + @staticmethod + def __get_attrs(stmt: lark.Tree) -> dict[str, str]: + attrs = {} + + for node in stmt.iter_subtrees(): + if node.data == "a_list": + attrs[node.children[0]] = node.children[1].strip('"') + + return attrs + + + def subgraph(self, tree): + # We are entering a new scope, inherit the default + # attributes of the outer scope + self.default_node_attrs.append(self.default_node_attrs[-1].copy()) + self.default_edge_attrs.append(self.default_edge_attrs[-1].copy()) + + children = self.visit_children(tree) + + # Exiting the scope + del self.default_node_attrs[-1] + del self.default_edge_attrs[-1] + + return children + + def node_stmt(self, tree): + node_id = tree.children[0] + node = node_id.children[0].strip('"') + + attrs = self.default_node_attrs[-1].copy() + attrs |= self.__get_attrs(tree) + + if attrs: + if node in self.node_attrs: + self.node_attrs[node] = attrs | self.node_attrs[node] + else: + self.node_attrs[node] = attrs + + return self.visit_children(tree) + + def edge_stmt(self, tree): + edge = ParseTree.parse_edge(tree) + + attrs = self.default_edge_attrs[-1].copy() + attrs |= self.__get_attrs(tree) + + if attrs: + if edge in self.edge_attrs: + self.edge_attrs[edge] = attrs | self.edge_attrs[edge] + else: + self.edge_attrs[edge] = attrs + + return self.visit_children(tree) + + def attr_stmt(self, tree): + attr_type = tree.children[0].data + attrs = self.__get_attrs(tree) + + if attr_type == "node": + self.default_node_attrs[-1] |= attrs + elif attr_type == "edge": + self.default_edge_attrs[-1] |= attrs + else: + # graph attributes are irrelevant + pass + + self.visit_children(tree) + + def __init__(self, dot_file): + parser = lark.Lark(self.grammar, parser='lalr') + node_parser = self.ParseNodes() + edge_parser = self.ParseEdges() + attributes_parser = self.ParseAttributes() + + try: + with open(dot_file, "r") as f: + tree = parser.parse(f.read()) + attributes_parser.visit(tree) + node_parser.visit(tree) + edge_parser.visit(tree) + except OSError as exc: + raise AutomataError(exc.strerror) from exc + except lark.exceptions.UnexpectedInput as exc: + raise AutomataError(str(exc)) + + self.nodes = node_parser.nodes + self.edges = edge_parser.edges + self.node_attrs = attributes_parser.node_attrs + self.edge_attrs = attributes_parser.edge_attrs + +class ConstraintCondition: + def __init__(self, env: str, op: str, val: str, unit=None): + self.env = env + self.op = op + self.val = val + self.unit = unit + if unit is None: + # try to infer unit from constants or parameters + val_for_unit = val.lower().replace("()", "") + if val_for_unit.endswith("_ns"): + self.unit = "ns" + if val_for_unit.endswith("_jiffies"): + self.unit = "j" + +class ConstraintRule: + grammar = r''' + rule: condition (OP condition)* + + OP: "&&" | "||" + + condition: ENV CMP_OP VAL UNIT? + + ENV: CNAME + + CMP_OP: "==" | "!=" | "<=" | "<" | ">=" | ">" + + VAL: /[0-9]+/ + | /[A-Z_]+\(\)/ + | /[A-Z_]+/ + | /[a-z_]+\(\)/ + | /[a-z_]+/ + + UNIT: "ns" | "us" | "ms" | "s" | "j" + ''' + + def __init__(self, c: ConstraintCondition): + ''' + A list of pairs of + - the condition (e.g. is_constr_dl == 1) + - the logical operator ("||" or "&&") combining this + condition with the next one if it exists, otherwise None + + TODO: Perhaps use an abstract syntax tree instead, because + this representation cannot capture precedence + ''' + self.rules = [[c, None]] + + def chain(self, op: str, c: ConstraintCondition): + self.rules[-1][1] = op + self.rules.append([c, None]) + +class ConstraintReset: + def __init__(self, env): + self.env = env + +class StateLabelParser: + grammar = r''' + label: CNAME ("\\n" condition)? + + %import common.CNAME + %import common.WS + %ignore WS + ''' + ConstraintRule.grammar + + parser = lark.Lark(grammar, parser='lalr', start="label") + + def __init__(self, label: str): + try: + tree = self.parser.parse(label) + except lark.exceptions.UnexpectedInput as exc: + raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}")) + + self.state = tree.children[0] + self.constraint = None + + if len(tree.children) == 2: + self.constraint = ConstraintCondition(*tree.children[1].children) + if self.constraint.op not in ("<", "<="): + raise AutomataError("State constraints must be clock expirations like" + f" clk<N ({label})") + +class EventLabelParser: + grammar = r''' + events: event ("\\n" event)* + + event: name (";" guard)? + + guard: reset + | rule + | rule ";" reset + | reset ";" rule + + name: CNAME + + reset: "reset" "(" ENV ")" + + %import common.CNAME + %import common.WS + %ignore WS + ''' + ConstraintRule.grammar + + parser = lark.Lark(grammar, parser='lalr', start="events") + + class GetEvents(lark.visitors.Transformer): + def guard(self, args): + reset = None + rule = None + for arg in args: + if arg.data == "reset": + reset = ConstraintReset(arg.children[0]) + elif arg.data == "rule": + conditions = arg.children + rule = ConstraintRule(conditions[0]) + for i in range(1, len(conditions), 2): + rule.chain(conditions[i], conditions[i + 1]) + return reset, rule + + def OP(self, args): + return args + + def condition(self, args): + return ConstraintCondition(*args) + + def event(self, args): + assert(len(args) <= 2) + name = args[0] + rule, reset = None, None + if len(args) == 2: + reset, rule = args[1] + return name, reset, rule + + def events(self, args): + return args + + def name(self, args): + return args[0] + + def __init__(self, label: str): + try: + tree = self.parser.parse(label) + self.events = self.GetEvents().transform(tree) + except lark.exceptions.UnexpectedInput as exc: + raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}")) + +class Transition: + def __init__(self, src: str, dst: str, event: str, + reset: ConstraintReset, rule: ConstraintRule): + self.src = src + self.dst = dst + self.event = event + self.rule = rule + self.reset = reset + +class State: + def __init__(self, name: str, inv: ConstraintCondition): + self.name = name + self.inv = inv class AutomataError(Exception): """Exception raised for errors in automata parsing and validation. @@ -44,35 +371,19 @@ class Automata: 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.__parse_tree = ParseTree(file_path) + self.transitions = self.__parse_transitions() + self.states, self.initial_state, self.final_states = self.__parse_states() 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.function = 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) @@ -90,194 +401,94 @@ class Automata: 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 + def __parse_transitions(self): + transitions = [] - if not dot_lines: - raise AutomataError(f"{self.__dot_path} is empty") + for edge in self.__parse_tree.edges: + attr = self.__parse_tree.edge_attrs.get(edge) + if not attr: + continue - # checking the first line: - line = dot_lines[0].split() + label = attr.get("label") - if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton": - raise AutomataError(f"Not a valid .dot format: {self.__dot_path}") + src, dst = edge - return dot_lines + parser = EventLabelParser(label) + for event, reset, rule in parser.events: + transitions.append(Transition(src, dst, event, reset, rule)) - def __get_cursor_begin_states(self) -> int: - for cursor, line in enumerate(self.__dot_lines): - split_line = line.split() + transitions.sort(key=lambda t : (t.src, t.event)) + return transitions - if len(split_line) and split_line[0] == self.node_marker: - return cursor + def __parse_states(self): + initial_state = "" + states = [] + final_states = [] - raise AutomataError("Could not find a beginning state") + for node in self.__parse_tree.nodes: + attr = self.__parse_tree.node_attrs[node] + label = attr.get("label") - def __get_cursor_begin_events(self) -> int: - state = 0 - cursor = 0 # make pyright happy + if node.startswith(Automata.init_marker): + initial_state = node[len(Automata.init_marker):] - for cursor, line in enumerate(self.__dot_lines): - line = line.split() - if not line: + if not label: 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 + parser = StateLabelParser(label) + state = State(parser.state, parser.constraint) - raw_state = split_line[-1] + states.append(state) - # "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 + shape = attr.get("shape") + if shape in ("doublecircle", "ellipse"): + final_states.append(state) - if "ellipse" in line: - final_states.append(state) - has_final_states = True + initial_state = next((s for s in states if s.name == initial_state), None) 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: + if not final_states: final_states.append(initial_state) + states.remove(initial_state) + states.sort(key=lambda s : s.name) + states.insert(0, 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(" ", "")]) + + for transition in self.transitions: + events.append(transition.event) + + if transition.reset: + envs.append(transition.reset.env) + self.env_stored.add(transition.reset.env) + if transition.rule: + for c, _ in transition.rule.rules: + envs.append(c.env) + self.__extract_env_var(c) + + for state in self.states: + if state.inv: + envs.append(state.inv.env) + self.__extract_env_var(state.inv) 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]]]: + def __extract_env_var(self, constraint: ConstraintCondition): + if constraint.unit: + self.env_types[constraint.env] = constraint.unit + if constraint.val[0].isalpha(): + self.constraint_vars.add(constraint.val) + + def __create_matrix(self) -> list[list[str]]: # transform the array into a dictionary events = self.events - states = self.states + states = [s.name for s in self.states] events_dict = {} states_dict = {} nr_event = 0 @@ -292,39 +503,16 @@ class Automata: # 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 + for transition in self.transitions: + src, dst = transition.src, transition.dst + event = transition.event + if src == dst and transition.reset: + # those events reset also on self loops + self.self_loop_reset_events.add(event) + matrix[states_dict[src]][events_dict[event]] = dst + + return matrix def __store_init_events(self) -> tuple[list[bool], list[bool]]: events_start = [False] * len(self.events) @@ -336,7 +524,7 @@ class Automata: 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: + if self.function[j][i] == self.initial_state.name: curr_event_will_init += 1 if self.function[0][i] != self.invalid_state_str: curr_event_from_init = True @@ -359,10 +547,3 @@ class Automata: 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/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py index fc85ba1f649e..22938ce1bf6c 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -29,10 +29,10 @@ class Dot2c(Automata): def __get_enum_states_content(self) -> list[str]: buff = [] - buff.append(f"\t{self.initial_state}{self.enum_suffix},") + buff.append(f"\t{self.initial_state.name}{self.enum_suffix},") for state in self.states: if state != self.initial_state: - buff.append(f"\t{state}{self.enum_suffix},") + buff.append(f"\t{state.name}{self.enum_suffix},") buff.append(f"\tstate_max{self.enum_suffix},") return buff @@ -142,7 +142,7 @@ class Dot2c(Automata): 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(self.__get_string_vector_per_line_content([s.name for s in self.states])) buff.append("\t},") return buff @@ -159,7 +159,7 @@ class Dot2c(Automata): return buff def __get_max_strlen_of_states(self) -> int: - max_state_name = len(max(self.states, key=len)) + max_state_name = max((len(s.name) for s in self.states)) return max(max_state_name, len(self.invalid_state_str)) def get_aut_init_function(self) -> str: @@ -199,7 +199,7 @@ class Dot2c(Automata): return buff def get_aut_init_initial_state(self) -> str: - return self.initial_state + return self.initial_state.name def format_aut_init_initial_state(self) -> list[str]: buff = [] diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py index e6f476b903b0..fd3254ea5b4d 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -6,17 +6,18 @@ # dot2k: transform dot files into a monitor for the Linux kernel. # # For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst +# Documentation/trace/rv/monitor_synthesis.rst -from collections import deque from .dot2c import Dot2c from .generator import Monitor -from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError - +from .automata import ConstraintCondition, AutomataError class dot2k(Monitor, Dot2c): template_dir = "dot2k" + # only needed for the per-obj cleanup hook + cleanup_marker = "obj_cleanup" + def __init__(self, file_path, MonitorType, extra_params={}): self.monitor_type = MonitorType Monitor.__init__(self, extra_params) @@ -56,18 +57,30 @@ class dot2k(Monitor, Dot2c): buff.append(f"\tda_{handle}({event}{self.enum_suffix});") buff.append("}") buff.append("") + if self.monitor_type == "per_obj": + buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */") + buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tint id = /* XXX: how do I get the id? */;") + buff.append("\tda_destroy_storage(id);") + 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});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") 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});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") return '\n'.join(buff) def fill_model_h_header(self) -> list[str]: @@ -176,7 +189,14 @@ class ha2k(dot2k): 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() + self.has_invariant = False + self.has_guard = False + for state in self.states: + if state.inv: + self.has_invariant = True + for transition in self.transitions: + if transition.rule or transition.reset: + self.has_guard = True def fill_monitor_class_type(self) -> str: if self._is_id_monitor(): @@ -209,38 +229,52 @@ class ha2k(dot2k): 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 __parse_guard_rule(self, rule) -> list[str]: + buff = [] + for c, sep in rule.rules: + env = c.env + self.enum_suffix + op = c.op + val = self.__adjust_value(c.val, c.unit) + + cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}" + if sep: + cond += f" {sep}" + buff.append(cond) + return buff - def __start_to_invariant_check(self, constr: str) -> str: + def __start_to_invariant_check(self, inv: ConstraintCondition) -> 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": + if inv.unit == "j": clock_type = "jiffy" - return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" + value = self.__adjust_value(inv.val, inv.unit) - 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("("):] + return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})" - def __parse_timer_constraint(self, rule: dict, value: str) -> str: + def __parse_invariant(self, inv): # by default assume the timer has ns expiration clock_type = "ns" - if self.env_types.get(rule["env"]) == "j": + if inv.unit == "j": clock_type = "jiffy" - return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix}," - f" {value}, time_ns)") + env = inv.env + self.enum_suffix + try: + val = int(inv.val) + except ValueError: + # it's a constant, a parameter or a function + val = inv.val.replace("()", "(ha_mon)") + + match inv.unit: + case "us": + val *= 10**3 + case "ms": + val *= 10**6 + case "s": + val *= 10**9 + + return (f"ha_start_timer_{clock_type}(ha_mon, {env}," + f" {val}, time_ns)") def __format_guard_rules(self, rules: list[str]) -> list[str]: """ @@ -259,124 +293,35 @@ class ha2k(dot2k): 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] + return ["res = " + separator.join(rules) + ";"] def __fill_verify_invariants_func(self) -> list[str]: - buff = [] - if not self.invariants: + if not self.has_invariant: return [] - buff.append( + buff = [ 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: + for state in self.states: + if not state.inv: 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)};") + check_str = self.__start_to_invariant_check(state.inv) + buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})") + buff.append(f"\t\t{check_str};") _else = "else " - buff.append("}\n") + buff.append("\treturn true;\n}\n") return buff def __fill_verify_guards_func(self) -> list[str]: buff = [] - if not self.guards: + + if not self.has_guard: return [] buff.append( @@ -388,14 +333,22 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon, """) _else = "" - for edge, constr in sorted(self.guards.items()): + for transition in self.transitions: + if not transition.rule and not transition.reset: + continue + 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: + f"{transition.src}{self.enum_suffix} && " + f"event == {transition.event}{self.enum_suffix})") + rule = transition.rule + reset = transition.reset + if rule and reset: buff[-1] += " {" - buff += [f"\t\t{c};" for c in constr.split(";")] - if constr.count(";") > 0: + if rule: + buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0]) + if reset: + buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);") + if rule and reset: _else = "} else " else: _else = "else " @@ -404,64 +357,15 @@ f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon, 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: + if not self.has_invariant: return [] - buff.append( + buff = [ 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}" @@ -470,13 +374,20 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, 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};") + for state in self.states: + inv = state.inv + if not inv: + continue + inv = self.__parse_invariant(inv) + buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})") + buff.append(f"\t\t{inv};") _else = "else " - for state in self.invariants: - buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})") + for state in self.states: + inv = state.inv + if not inv: + continue + buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})") buff.append("\t\tha_cancel_timer(ha_mon);") buff.append("}\n") @@ -484,7 +395,7 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, def __fill_constr_func(self) -> list[str]: buff = [] - if not self.constraints: + if not self.has_invariant and not self.has_guard: return [] buff.append( @@ -496,16 +407,9 @@ f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, * 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() @@ -515,18 +419,15 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) {{""") - if self.invariants: + if self.has_invariant: 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: + if self.has_guard: buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, " "next_state, time_ns))\n\t\treturn false;\n") - if self.invariants: + if self.has_invariant: buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n") buff.append("\treturn true;\n}\n") @@ -603,7 +504,7 @@ f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func() def _fill_timer_type(self) -> list: - if self.invariants: + if self.has_invariant: return [ "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */", "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py index 56f3bd8db850..45e2bab26cb5 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -6,7 +6,7 @@ # Abstract class for generating kernel runtime verification monitors from specification file import platform -import os +from pathlib import Path class RVGenerator: @@ -16,36 +16,38 @@ class RVGenerator: 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) + Path(__file__).resolve().parent / "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() + self._fill_rv_kernel_dir() - def __fill_rv_kernel_dir(self): + def _fill_rv_kernel_dir(self): + # find the kernel tree root relative to this file's location + resolved_path = Path(__file__).resolve() + if len(resolved_path.parents) > 4: + kernel_root = resolved_path.parents[4] + kernel_path = kernel_root / self.rv_dir - # 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 kernel_path.exists(): + self.rv_dir = str(kernel_path) + return - if os.path.exists(kernel_path): - self.rv_dir = kernel_path + # best effort if rvgen is installed and we are at the root of a kernel tree + if Path(self.rv_dir).exists(): 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) + kernel_path = Path(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 + if (kernel_path / "rv_trace.h").exists(): + self.rv_dir = str(kernel_path) return raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") @@ -57,12 +59,12 @@ class RVGenerator: def _read_template_file(self, file): try: - path = os.path.join(self.abs_template_dir, file) + path = 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) + path = self.abs_template_dir.parent / file return self._read_file(path) def fill_parent(self): @@ -133,7 +135,7 @@ class RVGenerator: def _patch_file(self, file, marker, line): assert self.auto_patch - file_to_patch = os.path.join(self.rv_dir, file) + file_to_patch = Path(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) @@ -187,22 +189,19 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o return f" - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)" def __create_directory(self): - path = self.name + path = Path(self.name) if self.auto_patch: - path = os.path.join(self.rv_dir, "monitors", path) - try: - os.mkdir(path) - except FileExistsError: - return + path = Path(self.rv_dir) / "monitors" / path + path.mkdir(exist_ok=True) 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}" + path = Path(self.name) / file_name if self.auto_patch: - path = os.path.join(self.rv_dir, "monitors", path) + path = Path(self.rv_dir) / "monitors" / self.name / file_name self.__write_file(path, content) def print_files(self): diff --git a/tools/verification/rvgen/rvgen/kunit.py b/tools/verification/rvgen/rvgen/kunit.py new file mode 100644 index 000000000000..85973f918c9b --- /dev/null +++ b/tools/verification/rvgen/rvgen/kunit.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com> +# +# Generator for runtime verification kunit files + +import re +from pathlib import Path +from . import generator + + +class KUnitError(Exception): + """Exception raised for errors in KUnit generation and file handling.""" + + +class KUnit(generator.RVGenerator): + template_dir = "" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.local = extra_params.get("local", False) + self.kunit_c = self._read_template_file("kunit.c") + if not self.local: + self._fill_rv_kernel_dir() + try: + self.monitor_path = self.__find_monitor_c_file() + with open(self.monitor_path, 'r') as f: + self.content = f.read() + except OSError as e: + raise KUnitError(e) from e + self.monitor_class = self.__detect_monitor_class() + + def _read_template_file(self, file): + if file in ("main.c", "Kconfig"): + return "" + return super()._read_template_file(file) + + def __find_monitor_c_file(self) -> str: + """Look for the monitor file in the kernel tree or in the current folder.""" + if not self.local: + path = Path(self.rv_dir) / "monitors" / self.name / f"{self.name}.c" + if path.exists(): + return str(path) + + path = Path(self.name) / f"{self.name}.c" + if path.exists(): + return str(path) + + raise FileNotFoundError(f"Could not find monitor C file for '{self.name}'") + + def __extract_function_args(self, handler_name: str) -> str: + pattern = re.compile( + r'^\s*(.*?)\b' + re.escape(handler_name) + r'\(([^)]*)\)', + re.MULTILINE | re.DOTALL + ) + match = pattern.search(self.content) + if not match: + return "/* XXX: fill handlers argument. */" + + return match.group(2).strip() + + def __parse_attach_handlers(self) -> list[str]: + """Find handlers by parsing when they are attached to tracepoints.""" + probe_pattern = re.compile( + r'rv_attach_trace_probe\(.*, ([a-zA-Z0-9_]+)\)' + ) + handlers = [] + for match in probe_pattern.finditer(self.content): + handler = match.group(1) + if handler not in handlers: + handlers.append(handler) + return handlers + + def __detect_monitor_class(self) -> str: + for c in ("da", "ha", "ltl"): + if f"{c}_monitor.h" in self.content: + return c + return "da" + + def __fill_kunit_c(self, struct_name: str) -> str: + kunit_c = self.kunit_c + kunit_c = kunit_c.replace("%%MODEL_NAME%%", self.name) + kunit_c = kunit_c.replace("%%MODEL_NAME_UP%%", self.name.upper()) + kunit_c = kunit_c.replace("%%MONITOR_CLASS%%", self.monitor_class) + kunit_c = kunit_c.replace("%%STRUCT_NAME%%", struct_name) + return kunit_c + + def __fill_kunit_h(self, struct_name, prototypes) -> str: + return f"""/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __{self.name.upper()}_KUNIT_H +#define __{self.name.upper()}_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct {struct_name} {{ +\tstruct rv_kunit_mon mon; +\t{"\n\t".join(prototypes)} +}} {struct_name}; +#endif + +#endif /* __{self.name.upper()}_KUNIT_H */ +""" + + def __fill_monitor_handlers(self, struct_name, assignments): + struct_definition = f"""#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "{self.name}_kunit.h" + +const struct {struct_name} {struct_name} = {{ +\t.mon = RV_MON_OPS_INIT(), +\t{"\n\t".join(assignments)} +}}; +EXPORT_SYMBOL_IF_KUNIT({struct_name}); +#endif""" + + if self.auto_patch: + try: + with open(self.monitor_path, 'w') as f: + f.write(f"{self.content}\n{struct_definition}\n") + except OSError as e: + raise KUnitError(f"Error patching monitor file {self.monitor_path}: {e}") from e + else: + print(f"Append the following to {self.name}.c:\n") + print(struct_definition) + print("Now complete the test and add it to rv_monitors_test.c") + + def print_files(self): + + handlers = self.__parse_attach_handlers() + + if not handlers: + raise KUnitError(f"No handlers found in {self.monitor_path}") + + prototypes = [] + assignments = [] + for handler in handlers: + arguments = self.__extract_function_args(handler) + + prototypes.append(f"void (*{handler})({arguments});") + assignments.append(f".{handler} = {handler},") + + struct_name = f"rv_{self.name}_ops" + + self.__fill_monitor_handlers(struct_name, assignments) + + dir_path = Path(self.monitor_path).parent + + header_file_path = dir_path / f"{self.name}_kunit.h" + kunit_c_file_path = dir_path / f"{self.name}_kunit.c" + + use_backup = True + if header_file_path.exists() or kunit_c_file_path.exists(): + try: + response = input("KUnit file(s) already exist. Backup? [Y/n] ") + if response.strip().lower() in ("n", "no"): + use_backup = False + except EOFError: + print("Non-interactive session detected, backing up existing files.") + else: + use_backup = False + + if use_backup: + for path in (header_file_path, kunit_c_file_path): + if path.exists(): + try: + path.rename(path.with_suffix(path.suffix + ".old")) + except OSError as e: + raise KUnitError(f"Error backing up file {path}: {e}") from e + + header_content = self.__fill_kunit_h(struct_name, prototypes) + try: + with open(header_file_path, 'w') as f: + f.write(header_content) + print(f"Successfully created KUnit header file: {header_file_path}") + except OSError as e: + raise KUnitError(f"Error writing to file {header_file_path}: {e}") from e + + kunit_c_content = self.__fill_kunit_c(struct_name) + try: + with open(kunit_c_file_path, 'w') as f: + f.write(kunit_c_content) + print(f"Successfully created KUnit C file: {kunit_c_file_path}") + except OSError as e: + raise KUnitError(f"Error writing to file {kunit_c_file_path}: {e}") from e diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index 7f538598a868..7cebda61bce8 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -7,9 +7,7 @@ # 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 +import lark # Grammar: # ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl @@ -30,42 +28,41 @@ from .automata import AutomataError # 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() +GRAMMAR = r''' +start: assign+ + +assign: VARIABLE "=" _ltl + +_ltl: _opd | binop | unop + +_opd : VARIABLE + | LITERAL + | "(" _ltl ")" + +unop: UNOP _ltl +UNOP: "always" + | "eventually" + | "next" + | "not" + +binop: _opd BINOP _ltl +BINOP: "until" + | "and" + | "or" + | "imply" + +VARIABLE: /[A-Z_][A-Z0-9_]*/ +LITERAL: "true" | "false" + +COMMENT: "#" /.*/ "\n" +%ignore COMMENT + +%import common.WS +%ignore WS +''' + +class LTLError(Exception): + "Exception raised for malformed linear temporal logic" class GraphNode: uid = 0 @@ -97,7 +94,7 @@ class GraphNode: return self.id < other.id class ASTNode: - uid = 1 + uid = 0 def __init__(self, op): self.op = op @@ -122,10 +119,8 @@ class ASTNode: 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() + if isinstance(self.op, (Literal, Variable)): + return str(self.op) return "val" + str(self.id) def normalize(self): @@ -382,6 +377,9 @@ class Variable: def __iter__(self): yield from () + def __str__(self): + return self.name.lower() + def negate(self): new = ASTNode(self) return NotOp(new) @@ -432,90 +430,49 @@ class Literal: 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() +class Transform(lark.visitors.Transformer): + def unop(self, node): + if node[0] == "always": + return ASTNode(AlwaysOp(node[1])) + if node[0] == "eventually": + return ASTNode(EventuallyOp(node[1])) + if node[0] == "next": + return ASTNode(NextOp(node[1])) + if node[0] == "not": + return ASTNode(NotOp(node[1])) + raise ValueError("Unknown operator %s" % node[0]) + + def binop(self, node): + if node[1] == "until": + return ASTNode(UntilOp(node[0], node[2])) + if node[1] == "and": + return ASTNode(AndOp(node[0], node[2])) + if node[1] == "or": + return ASTNode(OrOp(node[0], node[2])) + if node[1] == "imply": + return ASTNode(ImplyOp(node[0], node[2])) + raise ValueError("Unknown operator %s" % node[1]) + + def VARIABLE(self, args): + return ASTNode(Variable(args)) + + def LITERAL(self, args): + return ASTNode(Literal(args == "true")) + + def start(self, node): + return node + + def assign(self, node): + return node[0].op.name, node[1] + +parser = lark.Lark(GRAMMAR) def parse_ltl(s: str) -> ASTNode: - spec = parser.parse(s) + try: + spec = parser.parse(s) + except lark.exceptions.UnexpectedInput as e: + raise LTLError(str(e)) + spec = Transform().transform(spec) rule = None subexpr = {} @@ -527,7 +484,7 @@ def parse_ltl(s: str) -> ASTNode: subexpr[assign[0]] = assign[1] if rule is None: - raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format") + raise LTLError("Please define your specification in the \"RULE = <LTL spec>\" format") for node in rule: if not isinstance(node.op, Variable): diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py index 81fd1f5ea5ea..f3781a3e0856 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -222,7 +222,7 @@ class ltl2k(generator.Monitor): 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);" + return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);" def fill_atoms_init(self): buff = [] diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c index 5fc89b46f279..e6a20d74886c 100644 --- a/tools/verification/rvgen/rvgen/templates/container/main.c +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -31,5 +31,5 @@ module_init(register_%%MODEL_NAME%%); module_exit(unregister_%%MODEL_NAME%%); MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_AUTHOR("rvgen: auto-generated"); MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c index bf0999f6657a..bd3e0aab9cc5 100644 --- a/tools/verification/rvgen/rvgen/templates/dot2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -35,7 +35,7 @@ static int enable_%%MODEL_NAME%%(void) { int retval; - retval = da_monitor_init(); + retval = %%MONITOR_CLASS%%_monitor_init(); if (retval) return retval; @@ -50,7 +50,7 @@ static void disable_%%MODEL_NAME%%(void) %%TRACEPOINT_DETACH%% - da_monitor_destroy(); + %%MONITOR_CLASS%%_monitor_destroy(); } /* @@ -79,5 +79,5 @@ module_init(register_%%MODEL_NAME%%); module_exit(unregister_%%MODEL_NAME%%); MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_AUTHOR("rvgen: auto-generated"); MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c new file mode 100644 index 000000000000..62092b5cc6d4 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "%%MODEL_NAME%%_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%) + +static void rv_test_%%MODEL_NAME%%(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &%%STRUCT_NAME%%.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * %%STRUCT_NAME%%.handle_event(args); + */ +} + +#else +#define rv_test_%%MODEL_NAME%% rv_test_stub +#endif diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c index f85d076fbf78..c33f21535a7a 100644 --- a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -77,7 +77,7 @@ static void disable_%%MODEL_NAME%%(void) /* * 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%%, @@ -86,17 +86,17 @@ static struct rv_monitor rv_%%MODEL_NAME%% = { static int __init register_%%MODEL_NAME%%(void) { - return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); + 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%%); module_exit(unregister_%%MODEL_NAME%%); MODULE_LICENSE("GPL"); -MODULE_AUTHOR(/* TODO */); +MODULE_AUTHOR("rvgen: auto-generated"); MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/tests/golden/da_global/Kconfig b/tools/verification/rvgen/tests/golden/da_global/Kconfig new file mode 100644 index 000000000000..799fbf11c3ac --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_GLOBAL + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "da_global monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.c b/tools/verification/rvgen/tests/golden/da_global/da_global.c new file mode 100644 index 000000000000..71b26ae2d51c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global.c @@ -0,0 +1,95 @@ +// 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 "da_global" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_GLOBAL +#include "da_global.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_da_global); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_da_global); +} + +static int enable_da_global(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_da_global(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_global", + .description = "auto-generated", + .enable = enable_da_global, + .disable = disable_da_global, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_global(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_da_global(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_global); +module_exit(unregister_da_global); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_global: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.h b/tools/verification/rvgen/tests/golden/da_global/da_global.h new file mode 100644 index 000000000000..40b1f1c0c681 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_global automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_global + +enum states_da_global { + state_a_da_global, + state_b_da_global, + state_max_da_global, +}; + +#define INVALID_STATE state_max_da_global + +enum events_da_global { + event_1_da_global, + event_2_da_global, + event_max_da_global, +}; + +struct automaton_da_global { + char *state_names[state_max_da_global]; + char *event_names[event_max_da_global]; + unsigned char function[state_max_da_global][event_max_da_global]; + unsigned char initial_state; + bool final_states[state_max_da_global]; +}; + +static const struct automaton_da_global automaton_da_global = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_da_global, state_a_da_global }, + { INVALID_STATE, state_a_da_global }, + }, + .initial_state = state_a_da_global, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h new file mode 100644 index 000000000000..4d2730b71dd0 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_GLOBAL +DEFINE_EVENT(event_da_monitor, event_da_global, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_da_global, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_DA_GLOBAL */ diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig new file mode 100644 index 000000000000..249ba3aee8d7 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_PEROBJ_PARENT + depends on RV + # XXX: add dependencies if there + depends on RV_MON_PARENT_MON + default y + select DA_MON_EVENTS_ID + bool "da_perobj_parent monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c new file mode 100644 index 000000000000..5c5d300b4183 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c @@ -0,0 +1,119 @@ +// 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 "da_perobj_parent" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +#include <monitors/parent_mon/parent_mon.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_OBJ +typedef /* XXX: define the target type */ *monitor_target; +#include "da_perobj_parent.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event is only valid in the initial state */ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_start_run_event(id, t, event_1_da_perobj_parent); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_event(id, t, event_2_da_perobj_parent); +} + +static void handle_event_3(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_event(id, t, event_3_da_perobj_parent); +} + +/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */ +static void handle_obj_cleanup(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + da_destroy_storage(id); +} + +static int enable_da_perobj_parent(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2); + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3); + rv_attach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup); + + return 0; +} + +static void disable_da_perobj_parent(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2); + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3); + rv_detach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_perobj_parent", + .description = "auto-generated", + .enable = enable_da_perobj_parent, + .disable = disable_da_perobj_parent, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_perobj_parent(void) +{ + return rv_register_monitor(&rv_this, &rv_parent_mon); +} + +static void __exit unregister_da_perobj_parent(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_perobj_parent); +module_exit(unregister_da_perobj_parent); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_perobj_parent: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h new file mode 100644 index 000000000000..3c8dc3b22443 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h @@ -0,0 +1,64 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_perobj_parent automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_perobj_parent + +enum states_da_perobj_parent { + state_a_da_perobj_parent, + state_b_da_perobj_parent, + state_c_da_perobj_parent, + state_max_da_perobj_parent, +}; + +#define INVALID_STATE state_max_da_perobj_parent + +enum events_da_perobj_parent { + event_1_da_perobj_parent, + event_2_da_perobj_parent, + event_3_da_perobj_parent, + event_max_da_perobj_parent, +}; + +struct automaton_da_perobj_parent { + char *state_names[state_max_da_perobj_parent]; + char *event_names[event_max_da_perobj_parent]; + unsigned char function[state_max_da_perobj_parent][event_max_da_perobj_parent]; + unsigned char initial_state; + bool final_states[state_max_da_perobj_parent]; +}; + +static const struct automaton_da_perobj_parent automaton_da_perobj_parent = { + .state_names = { + "state_a", + "state_b", + "state_c", + }, + .event_names = { + "event_1", + "event_2", + "event_3", + }, + .function = { + { + state_b_da_perobj_parent, + state_c_da_perobj_parent, + INVALID_STATE, + }, + { + INVALID_STATE, + state_a_da_perobj_parent, + state_c_da_perobj_parent, + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + }, + .initial_state = state_a_da_perobj_parent, + .final_states = { 1, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h new file mode 100644 index 000000000000..59bfca8f73d2 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_PEROBJ_PARENT +DEFINE_EVENT(event_da_monitor_id, event_da_perobj_parent, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_da_perobj_parent, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_DA_PEROBJ_PARENT */ diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig new file mode 100644 index 000000000000..c6f350179098 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_PERTASK_DESC + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_ID + bool "da_pertask_desc monitor" + help + Custom description for testing diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c new file mode 100644 index 000000000000..c1ae5078c4f9 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c @@ -0,0 +1,105 @@ +// 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 "da_pertask_desc" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +#include "da_pertask_desc.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event is only valid in the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_run_event(p, event_1_da_pertask_desc); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event_2_da_pertask_desc); +} + +static void handle_event_3(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event_3_da_pertask_desc); +} + +static int enable_da_pertask_desc(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2); + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3); + + return 0; +} + +static void disable_da_pertask_desc(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2); + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_pertask_desc", + .description = "Custom description for testing", + .enable = enable_da_pertask_desc, + .disable = disable_da_pertask_desc, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_pertask_desc(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_da_pertask_desc(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_pertask_desc); +module_exit(unregister_da_pertask_desc); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_pertask_desc: Custom description for testing"); diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h new file mode 100644 index 000000000000..837b238754b0 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h @@ -0,0 +1,64 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_pertask_desc automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_pertask_desc + +enum states_da_pertask_desc { + state_a_da_pertask_desc, + state_b_da_pertask_desc, + state_c_da_pertask_desc, + state_max_da_pertask_desc, +}; + +#define INVALID_STATE state_max_da_pertask_desc + +enum events_da_pertask_desc { + event_1_da_pertask_desc, + event_2_da_pertask_desc, + event_3_da_pertask_desc, + event_max_da_pertask_desc, +}; + +struct automaton_da_pertask_desc { + char *state_names[state_max_da_pertask_desc]; + char *event_names[event_max_da_pertask_desc]; + unsigned char function[state_max_da_pertask_desc][event_max_da_pertask_desc]; + unsigned char initial_state; + bool final_states[state_max_da_pertask_desc]; +}; + +static const struct automaton_da_pertask_desc automaton_da_pertask_desc = { + .state_names = { + "state_a", + "state_b", + "state_c", + }, + .event_names = { + "event_1", + "event_2", + "event_3", + }, + .function = { + { + state_b_da_pertask_desc, + state_c_da_pertask_desc, + INVALID_STATE, + }, + { + INVALID_STATE, + state_a_da_pertask_desc, + state_c_da_pertask_desc, + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + }, + .initial_state = state_a_da_pertask_desc, + .final_states = { 1, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h new file mode 100644 index 000000000000..4e6086c4d86e --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_PERTASK_DESC +DEFINE_EVENT(event_da_monitor_id, event_da_pertask_desc, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_da_pertask_desc, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_DA_PERTASK_DESC */ diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig new file mode 100644 index 000000000000..0cc185ccfddf --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_HA_PERCPU + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_IMPLICIT + bool "ha_percpu monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c new file mode 100644 index 000000000000..3a72e867122c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c @@ -0,0 +1,227 @@ +// 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 "ha_percpu" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "ha_percpu.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * 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. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns) +{ + if (env == clk_ha_percpu) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_ha_percpu) + return /* XXX: how do I read env1? */ + else if (env == env2_ha_percpu) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns) +{ + if (env == clk_ha_percpu) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * 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. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_ha_percpu) + return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_ha_percpu) + return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_ha_percpu && event == event0_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S0_ha_percpu && event == event1_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S1_ha_percpu && event == event0_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) { + res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + } else if (curr_state == S2_ha_percpu && event == event1_ha_percpu) + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns; + else if (curr_state == S3_ha_percpu && event == event0_ha_percpu) + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull); + else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) { + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_ha_percpu) + return; + if (next_state == S0_ha_percpu) + ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns); + else if (next_state == S2_ha_percpu) + ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_ha_percpu) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_ha_percpu) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event0_ha_percpu); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + da_handle_event(event1_ha_percpu); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + da_handle_event(event2_ha_percpu); +} + +static int enable_ha_percpu(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_ha_percpu(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "ha_percpu", + .description = "auto-generated", + .enable = enable_ha_percpu, + .disable = disable_ha_percpu, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_ha_percpu(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_ha_percpu(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_ha_percpu); +module_exit(unregister_ha_percpu); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("ha_percpu: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h new file mode 100644 index 000000000000..2538db4f6a26 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h @@ -0,0 +1,72 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of ha_percpu automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME ha_percpu + +enum states_ha_percpu { + S0_ha_percpu, + S1_ha_percpu, + S2_ha_percpu, + S3_ha_percpu, + state_max_ha_percpu, +}; + +#define INVALID_STATE state_max_ha_percpu + +enum events_ha_percpu { + event0_ha_percpu, + event1_ha_percpu, + event2_ha_percpu, + event_max_ha_percpu, +}; + +enum envs_ha_percpu { + clk_ha_percpu, + env1_ha_percpu, + env2_ha_percpu, + env_max_ha_percpu, + env_max_stored_ha_percpu = env1_ha_percpu, +}; + +_Static_assert(env_max_stored_ha_percpu <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_ha_percpu { + char *state_names[state_max_ha_percpu]; + char *event_names[event_max_ha_percpu]; + char *env_names[env_max_ha_percpu]; + unsigned char function[state_max_ha_percpu][event_max_ha_percpu]; + unsigned char initial_state; + bool final_states[state_max_ha_percpu]; +}; + +static const struct automaton_ha_percpu automaton_ha_percpu = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { S0_ha_percpu, S1_ha_percpu, INVALID_STATE }, + { S0_ha_percpu, INVALID_STATE, S2_ha_percpu }, + { INVALID_STATE, S2_ha_percpu, S3_ha_percpu }, + { S0_ha_percpu, S1_ha_percpu, INVALID_STATE }, + }, + .initial_state = S0_ha_percpu, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h new file mode 100644 index 000000000000..074ddff6a60d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_HA_PERCPU +DEFINE_EVENT(event_da_monitor, event_ha_percpu, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_ha_percpu, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); + +DEFINE_EVENT(error_env_da_monitor, error_env_ha_percpu, + TP_PROTO(char *state, char *event, char *env), + TP_ARGS(state, event, env)); +#endif /* CONFIG_RV_MON_HA_PERCPU */ diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig new file mode 100644 index 000000000000..b37f46670bfd --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_LTL_PERTASK + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "ltl_pertask monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c new file mode 100644 index 000000000000..2c60b5c5b4e0 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c @@ -0,0 +1,107 @@ +// 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 "ltl_pertask" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "ltl_pertask.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_ltl_pertask(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_ltl_pertask(void) +{ + rv_detach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "ltl_pertask", + .description = "auto-generated", + .enable = enable_ltl_pertask, + .disable = disable_ltl_pertask, +}; + +static int __init register_ltl_pertask(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_ltl_pertask(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_ltl_pertask); +module_exit(unregister_ltl_pertask); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("ltl_pertask: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h new file mode 100644 index 000000000000..7e5de351b8fa --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h @@ -0,0 +1,108 @@ +/* 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 ltl_pertask + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h new file mode 100644 index 000000000000..ebd53621a5b1 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_LTL_PERTASK +DEFINE_EVENT(event_ltl_monitor_id, event_ltl_pertask, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_ltl_pertask, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_LTL_PERTASK */ diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig new file mode 100644 index 000000000000..175a416f8b18 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_BAK_KUNIT + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "test_bak_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c new file mode 100644 index 000000000000..16579c1c6910 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_bak_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_bak_kunit.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_bak_kunit(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_bak_kunit(void) +{ + rv_detach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_bak_kunit", + .description = "auto-generated", + .enable = enable_test_bak_kunit, + .disable = disable_test_bak_kunit, +}; + +static int __init register_test_bak_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_bak_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_bak_kunit); +module_exit(unregister_test_bak_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_bak_kunit: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h new file mode 100644 index 000000000000..2bfe4e37cea7 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h @@ -0,0 +1,108 @@ +/* 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 test_bak_kunit + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c new file mode 100644 index 000000000000..e2b9354034cc --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_bak_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_BAK_KUNIT) + +static void rv_test_test_bak_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_bak_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_bak_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_bak_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old new file mode 100644 index 000000000000..f747925bf542 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old @@ -0,0 +1 @@ +DUMMY diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h new file mode 100644 index 000000000000..585c4803be23 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h @@ -0,0 +1,22 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_BAK_KUNIT_KUNIT_H +#define __TEST_BAK_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_bak_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_example_event)(void *data, /* XXX: fill header */); +} rv_test_bak_kunit_ops; +#endif + +#endif /* __TEST_BAK_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h new file mode 100644 index 000000000000..b984208838c4 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_BAK_KUNIT +DEFINE_EVENT(event_ltl_monitor_id, event_test_bak_kunit, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_bak_kunit, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_BAK_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_container/Kconfig b/tools/verification/rvgen/tests/golden/test_container/Kconfig new file mode 100644 index 000000000000..2becb65dddad --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/Kconfig @@ -0,0 +1,5 @@ +config RV_MON_TEST_CONTAINER + depends on RV + bool "test_container monitor" + help + Test container for grouping monitors diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.c b/tools/verification/rvgen/tests/golden/test_container/test_container.c new file mode 100644 index 000000000000..e7e34592c6c5 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/test_container.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 "test_container" + +#include "test_container.h" + +struct rv_monitor rv_test_container = { + .name = "test_container", + .description = "Test container for grouping monitors", + .enable = NULL, + .disable = NULL, + .reset = NULL, + .enabled = 0, +}; + +static int __init register_test_container(void) +{ + return rv_register_monitor(&rv_test_container, NULL); +} + +static void __exit unregister_test_container(void) +{ + rv_unregister_monitor(&rv_test_container); +} + +module_init(register_test_container); +module_exit(unregister_test_container); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_container: Test container for grouping monitors"); diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.h b/tools/verification/rvgen/tests/golden/test_container/test_container.h new file mode 100644 index 000000000000..83e434432650 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/test_container.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_test_container; diff --git a/tools/verification/rvgen/tests/golden/test_da/Kconfig b/tools/verification/rvgen/tests/golden/test_da/Kconfig new file mode 100644 index 000000000000..0143a148ef34 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_DA + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "test_da monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.c b/tools/verification/rvgen/tests/golden/test_da/test_da.c new file mode 100644 index 000000000000..59b8dfabbbf1 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da.c @@ -0,0 +1,95 @@ +// 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 "test_da" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +#include "test_da.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_test_da); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_test_da); +} + +static int enable_test_da(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_test_da(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_da", + .description = "auto-generated", + .enable = enable_test_da, + .disable = disable_test_da, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_da(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_da(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_da); +module_exit(unregister_test_da); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_da: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.h b/tools/verification/rvgen/tests/golden/test_da/test_da.h new file mode 100644 index 000000000000..d55795efbb61 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_da automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_da + +enum states_test_da { + state_a_test_da, + state_b_test_da, + state_max_test_da, +}; + +#define INVALID_STATE state_max_test_da + +enum events_test_da { + event_1_test_da, + event_2_test_da, + event_max_test_da, +}; + +struct automaton_test_da { + char *state_names[state_max_test_da]; + char *event_names[event_max_test_da]; + unsigned char function[state_max_test_da][event_max_test_da]; + unsigned char initial_state; + bool final_states[state_max_test_da]; +}; + +static const struct automaton_test_da automaton_test_da = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_test_da, state_a_test_da }, + { INVALID_STATE, state_a_test_da }, + }, + .initial_state = state_a_test_da, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h new file mode 100644 index 000000000000..8bd67115d244 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_DA +DEFINE_EVENT(event_da_monitor, event_test_da, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_test_da, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_TEST_DA */ diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig new file mode 100644 index 000000000000..6d664ba5624d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_DA_KUNIT + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "test_da_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c new file mode 100644 index 000000000000..effd26548b07 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_da_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +#include "test_da_kunit.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_test_da_kunit); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_test_da_kunit); +} + +static int enable_test_da_kunit(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_test_da_kunit(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_da_kunit", + .description = "auto-generated", + .enable = enable_test_da_kunit, + .disable = disable_test_da_kunit, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_da_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_da_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_da_kunit); +module_exit(unregister_test_da_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_da_kunit: auto-generated"); + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "test_da_kunit_kunit.h" + +const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = { + .mon = RV_MON_OPS_INIT(), + .handle_event_1 = handle_event_1, + .handle_event_2 = handle_event_2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h new file mode 100644 index 000000000000..290a9454caa4 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_da_kunit automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_da_kunit + +enum states_test_da_kunit { + state_a_test_da_kunit, + state_b_test_da_kunit, + state_max_test_da_kunit, +}; + +#define INVALID_STATE state_max_test_da_kunit + +enum events_test_da_kunit { + event_1_test_da_kunit, + event_2_test_da_kunit, + event_max_test_da_kunit, +}; + +struct automaton_test_da_kunit { + char *state_names[state_max_test_da_kunit]; + char *event_names[event_max_test_da_kunit]; + unsigned char function[state_max_test_da_kunit][event_max_test_da_kunit]; + unsigned char initial_state; + bool final_states[state_max_test_da_kunit]; +}; + +static const struct automaton_test_da_kunit automaton_test_da_kunit = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_test_da_kunit, state_a_test_da_kunit }, + { INVALID_STATE, state_a_test_da_kunit }, + }, + .initial_state = state_a_test_da_kunit, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c new file mode 100644 index 000000000000..17826a5c47c8 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_da_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_DA_KUNIT) + +static void rv_test_test_da_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_da_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_da_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_da_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h new file mode 100644 index 000000000000..0094215ff4fb --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h @@ -0,0 +1,23 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_DA_KUNIT_KUNIT_H +#define __TEST_DA_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_da_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_event_1)(void *data, /* XXX: fill header */); + void (*handle_event_2)(void *data, /* XXX: fill header */); +} rv_test_da_kunit_ops; +#endif + +#endif /* __TEST_DA_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h new file mode 100644 index 000000000000..16804a79e834 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_DA_KUNIT +DEFINE_EVENT(event_da_monitor, event_test_da_kunit, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_test_da_kunit, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_TEST_DA_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_ha/Kconfig b/tools/verification/rvgen/tests/golden/test_ha/Kconfig new file mode 100644 index 000000000000..f4048290c774 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_HA + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_ID + bool "test_ha monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.c b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c new file mode 100644 index 000000000000..9047ff725546 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c @@ -0,0 +1,230 @@ +// 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 "test_ha" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "test_ha.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * 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. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns) +{ + if (env == clk_test_ha) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_test_ha) + return /* XXX: how do I read env1? */ + else if (env == env2_test_ha) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns) +{ + if (env == clk_test_ha) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * 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. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_test_ha) + return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_test_ha) + return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_test_ha && event == event0_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S0_test_ha && event == event1_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S1_test_ha && event == event0_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S1_test_ha && event == event2_test_ha) { + res = ha_get_env(ha_mon, env1_test_ha, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_test_ha, time_ns); + } else if (curr_state == S2_test_ha && event == event1_test_ha) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + ha_get_env(ha_mon, clk_test_ha, time_ns) < foo_ns; + else if (curr_state == S3_test_ha && event == event0_test_ha) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + (ha_get_env(ha_mon, clk_test_ha, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_test_ha, time_ns) == 0ull); + else if (curr_state == S3_test_ha && event == event1_test_ha) { + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + (ha_get_env(ha_mon, clk_test_ha, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_test_ha, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_test_ha, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_test_ha) + return; + if (next_state == S0_test_ha) + ha_start_timer_ns(ha_mon, clk_test_ha, bar_ns(ha_mon), time_ns); + else if (next_state == S2_test_ha) + ha_start_timer_ns(ha_mon, clk_test_ha, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_test_ha) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_test_ha) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_event(p, event0_test_ha); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event1_test_ha); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event2_test_ha); +} + +static int enable_test_ha(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_test_ha(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ha", + .description = "auto-generated", + .enable = enable_test_ha, + .disable = disable_test_ha, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_ha(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ha(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ha); +module_exit(unregister_test_ha); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ha: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h new file mode 100644 index 000000000000..949fa4453403 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h @@ -0,0 +1,72 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_ha automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_ha + +enum states_test_ha { + S0_test_ha, + S1_test_ha, + S2_test_ha, + S3_test_ha, + state_max_test_ha, +}; + +#define INVALID_STATE state_max_test_ha + +enum events_test_ha { + event0_test_ha, + event1_test_ha, + event2_test_ha, + event_max_test_ha, +}; + +enum envs_test_ha { + clk_test_ha, + env1_test_ha, + env2_test_ha, + env_max_test_ha, + env_max_stored_test_ha = env1_test_ha, +}; + +_Static_assert(env_max_stored_test_ha <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_test_ha { + char *state_names[state_max_test_ha]; + char *event_names[event_max_test_ha]; + char *env_names[env_max_test_ha]; + unsigned char function[state_max_test_ha][event_max_test_ha]; + unsigned char initial_state; + bool final_states[state_max_test_ha]; +}; + +static const struct automaton_test_ha automaton_test_ha = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { S0_test_ha, S1_test_ha, INVALID_STATE }, + { S0_test_ha, INVALID_STATE, S2_test_ha }, + { INVALID_STATE, S2_test_ha, S3_test_ha }, + { S0_test_ha, S1_test_ha, INVALID_STATE }, + }, + .initial_state = S0_test_ha, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h new file mode 100644 index 000000000000..381bafcb3322 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_HA +DEFINE_EVENT(event_da_monitor_id, event_test_ha, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_test_ha, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_TEST_HA */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig new file mode 100644 index 000000000000..6c48770ace1a --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_HA_KUNIT + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_ID + bool "test_ha_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c new file mode 100644 index 000000000000..239b0539df18 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c @@ -0,0 +1,243 @@ +// 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 "test_ha_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "test_ha_kunit.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * 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. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns) +{ + if (env == clk_test_ha_kunit) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_test_ha_kunit) + return /* XXX: how do I read env1? */ + else if (env == env2_test_ha_kunit) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns) +{ + if (env == clk_test_ha_kunit) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * 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. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_test_ha_kunit) + return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_test_ha_kunit) + return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_test_ha_kunit && event == event0_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S0_test_ha_kunit && event == event1_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S1_test_ha_kunit && event == event0_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S1_test_ha_kunit && event == event2_test_ha_kunit) { + res = ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + } else if (curr_state == S2_test_ha_kunit && event == event1_test_ha_kunit) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < foo_ns; + else if (curr_state == S3_test_ha_kunit && event == event0_test_ha_kunit) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_test_ha_kunit, time_ns) == 0ull); + else if (curr_state == S3_test_ha_kunit && event == event1_test_ha_kunit) { + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_test_ha_kunit) + return; + if (next_state == S0_test_ha_kunit) + ha_start_timer_ns(ha_mon, clk_test_ha_kunit, bar_ns(ha_mon), time_ns); + else if (next_state == S2_test_ha_kunit) + ha_start_timer_ns(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_test_ha_kunit) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_test_ha_kunit) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_event(p, event0_test_ha_kunit); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event1_test_ha_kunit); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event2_test_ha_kunit); +} + +static int enable_test_ha_kunit(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_test_ha_kunit(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ha_kunit", + .description = "auto-generated", + .enable = enable_test_ha_kunit, + .disable = disable_test_ha_kunit, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_ha_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ha_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ha_kunit); +module_exit(unregister_test_ha_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ha_kunit: auto-generated"); + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "test_ha_kunit_kunit.h" + +const struct rv_test_ha_kunit_ops rv_test_ha_kunit_ops = { + .mon = RV_MON_OPS_INIT(), + .handle_event0 = handle_event0, + .handle_event1 = handle_event1, + .handle_event2 = handle_event2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h new file mode 100644 index 000000000000..5c428f818bdf --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h @@ -0,0 +1,88 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_ha_kunit automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_ha_kunit + +enum states_test_ha_kunit { + S0_test_ha_kunit, + S1_test_ha_kunit, + S2_test_ha_kunit, + S3_test_ha_kunit, + state_max_test_ha_kunit, +}; + +#define INVALID_STATE state_max_test_ha_kunit + +enum events_test_ha_kunit { + event0_test_ha_kunit, + event1_test_ha_kunit, + event2_test_ha_kunit, + event_max_test_ha_kunit, +}; + +enum envs_test_ha_kunit { + clk_test_ha_kunit, + env1_test_ha_kunit, + env2_test_ha_kunit, + env_max_test_ha_kunit, + env_max_stored_test_ha_kunit = env1_test_ha_kunit, +}; + +_Static_assert(env_max_stored_test_ha_kunit <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_test_ha_kunit { + char *state_names[state_max_test_ha_kunit]; + char *event_names[event_max_test_ha_kunit]; + char *env_names[env_max_test_ha_kunit]; + unsigned char function[state_max_test_ha_kunit][event_max_test_ha_kunit]; + unsigned char initial_state; + bool final_states[state_max_test_ha_kunit]; +}; + +static const struct automaton_test_ha_kunit automaton_test_ha_kunit = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { + S0_test_ha_kunit, + S1_test_ha_kunit, + INVALID_STATE, + }, + { + S0_test_ha_kunit, + INVALID_STATE, + S2_test_ha_kunit, + }, + { + INVALID_STATE, + S2_test_ha_kunit, + S3_test_ha_kunit, + }, + { + S0_test_ha_kunit, + S1_test_ha_kunit, + INVALID_STATE, + }, + }, + .initial_state = S0_test_ha_kunit, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c new file mode 100644 index 000000000000..6214a4aa6d25 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_ha_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_HA_KUNIT) + +static void rv_test_test_ha_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_ha_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_ha_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_ha_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h new file mode 100644 index 000000000000..0b2030cb644a --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h @@ -0,0 +1,24 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_HA_KUNIT_KUNIT_H +#define __TEST_HA_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_ha_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_event0)(void *data, /* XXX: fill header */); + void (*handle_event1)(void *data, /* XXX: fill header */); + void (*handle_event2)(void *data, /* XXX: fill header */); +} rv_test_ha_kunit_ops; +#endif + +#endif /* __TEST_HA_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h new file mode 100644 index 000000000000..6c13ee0068d3 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_HA_KUNIT +DEFINE_EVENT(event_da_monitor_id, event_test_ha_kunit, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_test_ha_kunit, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha_kunit, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_TEST_HA_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig new file mode 100644 index 000000000000..e2d0e721f180 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_LTL + depends on RV + # XXX: add dependencies if there + depends on RV_MON_LTL_PARENT + default y + select LTL_MON_EVENTS_ID + bool "test_ltl monitor" + help + Simple description diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c new file mode 100644 index 000000000000..dd961c5dc8ad --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c @@ -0,0 +1,108 @@ +// 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 "test_ltl" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +#include <monitors/ltl_parent/ltl_parent.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_ltl.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_ltl(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_ltl(void) +{ + rv_detach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ltl", + .description = "Simple description", + .enable = enable_test_ltl, + .disable = disable_test_ltl, +}; + +static int __init register_test_ltl(void) +{ + return rv_register_monitor(&rv_this, &rv_ltl_parent); +} + +static void __exit unregister_test_ltl(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ltl); +module_exit(unregister_test_ltl); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ltl: Simple description"); diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h new file mode 100644 index 000000000000..7895f2e233e8 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h @@ -0,0 +1,108 @@ +/* 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 test_ltl + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h new file mode 100644 index 000000000000..3571b004c114 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_LTL +DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_LTL */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig new file mode 100644 index 000000000000..3e334c344261 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_LTL_KUNIT + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "test_ltl_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c new file mode 100644 index 000000000000..c1d58ce435a8 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_ltl_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_ltl_kunit.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_ltl_kunit(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_ltl_kunit(void) +{ + rv_detach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ltl_kunit", + .description = "auto-generated", + .enable = enable_test_ltl_kunit, + .disable = disable_test_ltl_kunit, +}; + +static int __init register_test_ltl_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ltl_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ltl_kunit); +module_exit(unregister_test_ltl_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ltl_kunit: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h new file mode 100644 index 000000000000..acc503b56e87 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h @@ -0,0 +1,108 @@ +/* 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 test_ltl_kunit + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c new file mode 100644 index 000000000000..37dab5dfdebc --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_ltl_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_LTL_KUNIT) + +static void rv_test_test_ltl_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_ltl_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_ltl_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_ltl_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h new file mode 100644 index 000000000000..b2ca34be327f --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h @@ -0,0 +1,22 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_LTL_KUNIT_KUNIT_H +#define __TEST_LTL_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_ltl_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_example_event)(void *data, /* XXX: fill header */); +} rv_test_ltl_kunit_ops; +#endif + +#endif /* __TEST_LTL_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h new file mode 100644 index 000000000000..a054d5b2c0ea --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_LTL_KUNIT +DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl_kunit, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl_kunit, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_LTL_KUNIT */ diff --git a/tools/verification/rvgen/tests/rvgen_container.t b/tools/verification/rvgen/tests/rvgen_container.t new file mode 100644 index 000000000000..fa4fb3db8288 --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_container.t @@ -0,0 +1,20 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help tests +check "verify container subcommand help" \ + "$RVGEN container -h" 0 "model_name" "class" + +check_and_compare_folder "container with description" \ + "$RVGEN container -n test_container -D 'Test container for grouping monitors'" \ + "test_container" "Writing the monitor into the directory test_container" + +# Error handling tests +check "missing required model_name" \ + "$RVGEN container" 2 "the following arguments are required: -n/--model_name" + +test_end diff --git a/tools/verification/rvgen/tests/rvgen_kunit.t b/tools/verification/rvgen/tests/rvgen_kunit.t new file mode 100644 index 000000000000..d27d9175f562 --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_kunit.t @@ -0,0 +1,41 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help tests +check "verify kunit subcommand help" \ + "$RVGEN kunit -h" 0 "model_name" "spec" + +check_and_compare_folder "KUnit generation with local lookup and test_da_kunit" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu -n test_da_kunit && $RVGEN kunit -a -l -n test_da_kunit" \ + "test_da_kunit" "Now complete the test and add it to rv_monitors_test.c" "RV_MON_OPS_INIT" + +check_and_compare_folder "KUnit generation with local lookup and test_ha_kunit" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task -n test_ha_kunit && $RVGEN kunit -a -l -n test_ha_kunit" \ + "test_ha_kunit" "Successfully created KUnit" "Append the following to" + +check_and_compare_folder "KUnit generation with local lookup and test_ltl_kunit" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_ltl_kunit && $RVGEN kunit -l -n test_ltl_kunit" \ + "test_ltl_kunit" "RV_MON_OPS_INIT" + +check_and_compare_folder "KUnit generation with backup file" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_bak_kunit && echo DUMMY > test_bak_kunit/test_bak_kunit_kunit.c && $RVGEN kunit -l -n test_bak_kunit" \ + "test_bak_kunit" "KUnit file(s) already exist.*backing up existing files" + +# Error handling tests +check "missing required model_name" \ + "$RVGEN kunit" 2 "the following arguments are required: -n/--model_name" + +check "non-existent model_name with auto_patch" \ + "$RVGEN kunit -a -n nonexistent" 1 \ + "Could not find monitor C file" "Traceback (most recent call last)" + +check "monitor without handlers" \ + "mkdir -p nohandler ; echo DUMMY > nohandler/nohandler.c ; $RVGEN kunit -l -n nohandler" 1 \ + "No handlers found" "Traceback (most recent call last)" +rm -rf nohandler + +test_end diff --git a/tools/verification/rvgen/tests/rvgen_monitor.t b/tools/verification/rvgen/tests/rvgen_monitor.t new file mode 100644 index 000000000000..5f2562600bad --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_monitor.t @@ -0,0 +1,87 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help and basic tests +check "verify help page" \ + "$RVGEN --help" 0 "Generate kernel rv monitor" + +check "verify monitor subcommand help" \ + "$RVGEN monitor --help" 0 "Monitor class" + +# DA monitor tests - test all monitor types +check_and_compare_folder "DA per_cpu (default name)" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu" \ + "test_da" "obj-\$(CONFIG_RV_MON_TEST_DA) += monitors/test_da/test_da.o" + +check_and_compare_folder "DA global type" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t global -n da_global" \ + "da_global" "DA_MON_EVENTS_IMPLICIT" + +check_and_compare_folder "DA per_task with description" \ + "$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_task -n da_pertask_desc -D 'Custom description for testing'" \ + "da_pertask_desc" "#include <monitors/da_pertask_desc/da_pertask_desc_trace.h>" + +check_and_compare_folder "DA per_obj with parent" \ + "$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_obj -n da_perobj_parent -p parent_mon" \ + "da_perobj_parent" "DA_MON_EVENTS_ID" + +# HA monitor tests +check_and_compare_folder "HA per_task (default name)" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task" \ + "test_ha" "HA_MON_EVENTS_ID" + +check_and_compare_folder "HA per_cpu type" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_cpu -n ha_percpu" \ + "ha_percpu" "HA_MON_EVENTS_IMPLICIT" + +# LTL monitor test +check_and_compare_folder "LTL per_task" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n ltl_pertask" \ + "ltl_pertask" "source \"kernel/trace/rv/monitors/ltl_pertask/Kconfig\"" + +check_and_compare_folder "LTL per_task with parent and description (default name)" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -p ltl_parent -D 'Simple description'" \ + "test_ltl" "LTL_MON_EVENTS_ID" + +# Error handling tests +check "missing required spec argument" \ + "$RVGEN monitor -c da -t per_cpu" 2 \ + "the following arguments are required: -s/--spec" "Traceback (most recent call last)" + +check "missing required monitor type" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot" 2 \ + "the following arguments are required: -t/--monitor_type" "Traceback (most recent call last)" + +check "missing required monitor class" \ + "$RVGEN monitor -s tests/specs/test_da.dot -t per_cpu" 2 \ + "the following arguments are required: -c/--class" "Traceback (most recent call last)" + +check "invalid monitor class" \ + "$RVGEN monitor -c invalid -s tests/specs/test_da.dot -t per_cpu" 1 \ + "Unknown monitor class" "Traceback (most recent call last)" + +check "missing dot file" \ + "$RVGEN monitor -c da -s tests/specs/nonexistent.dot -t per_cpu" 1 \ + "No such file or directory" "Traceback (most recent call last)" + +check "missing ltl file" \ + "$RVGEN monitor -c ltl -s tests/specs/nonexistent.ltl -t per_task" 1 \ + "No such file or directory" "Traceback (most recent call last)" + +check "invalid dot file syntax" \ + "$RVGEN monitor -c da -s tests/specs/test_invalid.dot -t per_cpu" 1 \ + "The automaton doesn't have an initial state" "Traceback (most recent call last)" + +check "invalid ha file syntax" \ + "$RVGEN monitor -c ha -s tests/specs/test_invalid_ha.dot -t per_obj" 1 \ + "Unrecognised event" "Traceback (most recent call last)" + +check "invalid ltl file syntax" \ + "$RVGEN monitor -c ltl -s tests/specs/test_invalid.ltl -t per_task" 1 \ + "No terminal matches 'i'" "Traceback (most recent call last)" + +test_end diff --git a/tools/verification/rvgen/tests/specs/test_da.dot b/tools/verification/rvgen/tests/specs/test_da.dot new file mode 100644 index 000000000000..e555c239b221 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_da.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a"]; + "state_a" -> "state_a" [ label = "event_2" ]; + "state_a" -> "state_b" [ label = "event_1" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_da2.dot b/tools/verification/rvgen/tests/specs/test_da2.dot new file mode 100644 index 000000000000..cdd4192f58ae --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_da2.dot @@ -0,0 +1,19 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = circle] "state_c"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a"]; + "state_a" -> "state_b" [ label = "event_1" ]; + "state_a" -> "state_c" [ label = "event_2" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + "state_b" -> "state_c" [ label = "event_3" ]; + "state_c" [label = "state_c"]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_ha.dot b/tools/verification/rvgen/tests/specs/test_ha.dot new file mode 100644 index 000000000000..af18ad7389ec --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_ha.dot @@ -0,0 +1,27 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "S1"}; + {node [shape = plaintext, style=invis, label=""] "__init_S0"}; + {node [shape = doublecircle] "S0"}; + {node [shape = circle] "S0"}; + {node [shape = circle] "S2"}; + {node [shape = circle] "S3"}; + "__init_S0" -> "S0"; + "S0" [label = "S0\nclk < bar_ns()", color = green3]; + "S1" [label = "S1"]; + "S2" [label = "S2\nclk < BAR_NS()"]; + "S3" [label = "S3"]; + "S1" -> "S0" [ label = "event0;reset(clk)" ]; + "S0" -> "S1" [ label = "event1;reset(clk)" ]; + "S0" -> "S0" [ label = "event0;reset(clk)" ]; + "S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ]; + "S2" -> "S3" [ label = "event2" ]; + "S2" -> "S2" [ label = "event1;clk < foo_ns" ]; + "S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ]; + "S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ]; + { rank = min ; + "__init_S0"; + "S0"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_invalid.dot b/tools/verification/rvgen/tests/specs/test_invalid.dot new file mode 100644 index 000000000000..17c63fc57f17 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid.dot @@ -0,0 +1,8 @@ +digraph invalid { + {node [shape = circle] "init"}; + {node [shape = circle] "state1"}; + "init" [label = "init"]; + "init" -> "state1" [ label = "event_a" ]; + "state1" [label = "state1"]; + "state1" -> "init" [ label = "event_b" ]; +} diff --git a/tools/verification/rvgen/tests/specs/test_invalid.ltl b/tools/verification/rvgen/tests/specs/test_invalid.ltl new file mode 100644 index 000000000000..cf36307e003c --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid.ltl @@ -0,0 +1 @@ +RULE = A invalid B diff --git a/tools/verification/rvgen/tests/specs/test_invalid_ha.dot b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot new file mode 100644 index 000000000000..06de6aa8709f --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a;clk < 1"]; + "state_a" -> "state_a" [ label = "event_2;reset(clk)" ]; + "state_a" -> "state_b" [ label = "event_1;wrong_constraint" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_ltl.ltl b/tools/verification/rvgen/tests/specs/test_ltl.ltl new file mode 100644 index 000000000000..5ed658abd69c --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_ltl.ltl @@ -0,0 +1 @@ +RULE = always (EVENT_A imply eventually EVENT_B) diff --git a/tools/verification/tests/engine.sh b/tools/verification/tests/engine.sh new file mode 100644 index 000000000000..cfdf2180aad8 --- /dev/null +++ b/tools/verification/tests/engine.sh @@ -0,0 +1,175 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +test_begin() { + # Count tests to allow the test harness to double-check if all were + # included correctly. + ctr=0 + [ -z "$RV" ] && RV="../rv/rv" + [ -z "$RVGEN" ] && RVGEN="python3 ../rvgen" + [ -z "$GOLDEN_DIR" ] && GOLDEN_DIR="tests/golden" + [ -n "$TEST_COUNT" ] && echo "1..$TEST_COUNT" +} + +failure() { + fail=1 + if [ $# -gt 0 ]; then + failbuf+="$1" + failbuf+=$'\n' + fi +} + +report() { + local desc="$1" + + if [ "$fail" -eq 0 ]; then + echo "ok $ctr - $desc" + else + # Add output and exit code as comments in case of failure + echo "not ok $ctr - $desc" + echo -n "$failbuf" + echo "$result" | col -b | while read -r line; do echo "# $line"; done + printf "#\n# exit code %s\n" "$exitcode" + fi +} + +_check() { + local command=$2 + local expected_exitcode=${3:-0} + local expected_output=$4 + local unexpected_output=$5 + local all_lines_pattern=$6 + local patterns="$expected_output $unexpected_output $all_lines_pattern" + local bgpid pid + + eval "$TIMEOUT" "$command" &> check_output.$$ & + bgpid=$! + + if grep -q "\$pid" <<< "$patterns"; then + for _ in {1..30}; do + pid=$(pgrep -f "${command%%[|;&>]*}" | tail -n1) + [ -n "$pid" ] && break + sleep 0.1 + done + fi + + wait $bgpid + exitcode=$? + result=$(tr -d '\0' < check_output.$$) + rm -f check_output.$$ + + failbuf='' + fail=0 + + # Suppress any other error if a needed pid is empty + if [ -z "$pid" ] && grep -q "\$pid" <<< "$patterns"; then + result='' + failure "# Empty pid for $command" + return 1 + fi + + expected_output="${expected_output//\$pid/$pid}" + unexpected_output="${unexpected_output//\$pid/$pid}" + all_lines_pattern="${all_lines_pattern//\$pid/$pid}" + + # Test if the results matches if requested + if [ -n "$expected_output" ] && ! grep -qe "$expected_output" <<< "$result"; then + failure "# Output match failed: \"$expected_output\"" + fi + + if [ -n "$unexpected_output" ] && grep -qe "$unexpected_output" <<< "$result"; then + failure "# Output non-match failed: \"$unexpected_output\"" + fi + + if [ -n "$all_lines_pattern" ] && grep -vqe "$all_lines_pattern" <<< "$result"; then + failure "# All-lines pattern failed: \"$all_lines_pattern\"" + fi + + if [ $exitcode -ne "$expected_exitcode" ]; then + failure "# Expected exit code $expected_exitcode" + fi +} + +check() { + # Simple check: run the command with given arguments and test exit code. + # If TEST_COUNT is set, run the test. Otherwise, just count. + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + _check "$@" + report "$1" + fi +} + +check_if_exists() { + # Conditional check that skips if a file or folder doesn't exist + local desc=$1 + local command=$2 + local file=$3 + local expected_output=$4 + local unexpected_output=$5 + local all_lines_pattern=$6 + + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + if [ ! -e "$file" ]; then + echo "ok $ctr - $desc # SKIP file not found: $file" + else + _check "$desc" "$command" 0 "$expected_output" \ + "$unexpected_output" "$all_lines_pattern" + report "$desc" + fi + fi +} + +check_and_compare_folder() { + # Run command, compare generated folder to golden, and cleanup + local desc=$1 + local command=$2 + local generated_dir=$3 + local expected_output=$4 + local unexpected_output=$5 + local golden_dir="$GOLDEN_DIR/$generated_dir" + + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + rm -rf "$generated_dir" + _check "$desc" "$command" 0 "$expected_output" "$unexpected_output" + + if [ "$fail" -eq 0 ] && [ ! -d "$generated_dir" ]; then + failure "# Generated directory not found: $generated_dir" + fi + + if [ "$fail" -ne 0 ]; then + : + elif ! diff -r "$generated_dir" "$golden_dir" &> /dev/null; then + failure "# Directories differ:" + failbuf+=$(diff -r "$generated_dir" "$golden_dir" 2>&1 | sed 's/^/# /') + failbuf+=$'\n' + fi + + report "$1" + + rm -rf "$generated_dir" + fi +} + +set_timeout() { + TIMEOUT="timeout -v -k 30s $1" +} + +set_expected_timeout() { + TIMEOUT="timeout --preserve-status -k 30s $1" +} + +unset_timeout() { + unset TIMEOUT +} + +test_end() { + # If running without TEST_COUNT, tests are not actually run, just + # counted. In that case, re-run the test with the correct count. + [ -z "$TEST_COUNT" ] && TEST_COUNT=$ctr exec bash "$0" || true +} + +# Avoid any environmental discrepancies +export LC_ALL=C +unset_timeout |