xref: /linux/tools/verification/rvgen/__main__.py (revision da245fae4041774bc467fc62fbbfc36a57442e4c)
1#!/usr/bin/env python3
2# SPDX-License-Identifier: GPL-2.0-only
3#
4# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
5#
6# dot2k: transform dot files into a monitor for the Linux kernel.
7#
8# For further information, see:
9#   Documentation/trace/rv/monitor_synthesis.rst
10
11if __name__ == '__main__':
12    from rvgen.dot2k import da2k, ha2k
13    from rvgen.generator import Monitor
14    from rvgen.container import Container
15    from rvgen.ltl2k import ltl2k
16    from rvgen.automata import AutomataError
17    from rvgen.ltl2ba import LTLError
18    import argparse
19    import sys
20
21    parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
22
23    parent_parser = argparse.ArgumentParser(add_help=False)
24    parent_parser.add_argument("-D", "--description", dest="description", required=False)
25    parent_parser.add_argument("-a", "--auto_patch", dest="auto_patch",
26                        action="store_true", required=False,
27                        help="Patch the kernel in place")
28
29    subparsers = parser.add_subparsers(dest="subcmd", required=True)
30
31    monitor_parser = subparsers.add_parser("monitor", parents=[parent_parser])
32    monitor_parser.add_argument('-n', "--model_name", dest="model_name")
33    monitor_parser.add_argument("-p", "--parent", dest="parent",
34                                required=False, help="Create a monitor nested to parent")
35    monitor_parser.add_argument('-c', "--class", dest="monitor_class", required=True,
36                                help="Monitor class, either \"da\", \"ha\" or \"ltl\"")
37    monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
38                                help="Monitor specification file")
39    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True,
40                                help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
41
42    container_parser = subparsers.add_parser("container", parents=[parent_parser])
43    container_parser.add_argument('-n', "--model_name", dest="model_name", required=True)
44
45    params = parser.parse_args()
46
47    try:
48        if params.subcmd == "monitor":
49            print(f"Opening and parsing the specification file {params.spec}")
50            if params.monitor_class == "da":
51                monitor = da2k(params.spec, params.monitor_type, vars(params))
52            elif params.monitor_class == "ha":
53                monitor = ha2k(params.spec, params.monitor_type, vars(params))
54            elif params.monitor_class == "ltl":
55                monitor = ltl2k(params.spec, params.monitor_type, vars(params))
56            else:
57                print("Unknown monitor class:", params.monitor_class)
58                sys.exit(1)
59        else:
60            monitor = Container(vars(params))
61    except (AutomataError, LTLError) as e:
62        print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr)
63        sys.exit(1)
64
65    print(f"Writing the monitor into the directory {monitor.name}")
66    monitor.print_files()
67    print("Almost done, checklist")
68    if params.subcmd == "monitor":
69        print(f"  - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation")
70        print(monitor.fill_tracepoint_tooltip())
71    print(monitor.fill_makefile_tooltip())
72    print(monitor.fill_kconfig_tooltip())
73    print(monitor.fill_monitor_tooltip())
74