verification/dot2k: Prepare the frontend for LTL inclusion

The dot2k tool has some code that can be reused for linear temporal logic
monitor. Prepare its frontend for LTL inclusion:

  1. Rename to be generic: rvgen

  2. Replace the parameter --dot with 2 parameters:
     --class: to specific the monitor class, can be 'da' or 'ltl'
     --spec: the monitor specification file, .dot file for DA, and .ltl
             file for LTL

The old command:

  python3 dot2/dot2k monitor -d wip.dot -t per_cpu

is equivalent to the new commands:

  python3 rvgen monitor -c da -s wip.dot -t per_cpu

Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com>
Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>

diff --git a/tools/verification/dot2/Makefile b/tools/verification/rvgen/Makefile
similarity index 55%
rename from tools/verification/dot2/Makefile
rename to tools/verification/rvgen/Makefile
index 021beb07a5213acc4e66adea94a0442b6620d32c..cea9c21c3bced83b4db2697ec92d817346516fba 100644 (file)
--- a/tools/verification/dot2/Makefile
+++ b/tools/verification/rvgen/Makefile
@@ -3,7 +3,7 @@ INSTALL=install
 prefix  ?= /usr
 bindir  ?= $(prefix)/bin
 mandir  ?= $(prefix)/share/man
-miscdir ?= $(prefix)/share/dot2
+miscdir ?= $(prefix)/share/rvgen
 srcdir  ?= $(prefix)/src
 
 PYLIB  ?= $(shell python3 -c 'import sysconfig;  print (sysconfig.get_path("purelib"))')
@@ -16,11 +16,11 @@ clean:
 
 .PHONY: install
 install:
-       $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
-       $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+       $(INSTALL) 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) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py
-       $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/
+       $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py
+       $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen
 
        mkdir -p ${miscdir}/
        cp -rp dot2k_templates $(DESTDIR)$(miscdir)/

diff --git a/tools/verification/dot2/dot2k b/tools/verification/rvgen/__main__.py
similarity index 72%
rename from tools/verification/dot2/dot2k
rename to tools/verification/rvgen/__main__.py
index 133fb17d9d475ec5a223e582aa45f530dcfaa876..994d320ad2d1fe65a66947292f225df4e9344ff4 100644 (file)
--- a/tools/verification/dot2/dot2k
+++ b/tools/verification/rvgen/__main__.py
@@ -9,11 +9,11 @@
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
 if __name__ == '__main__':
-    from dot2.dot2k import dot2k
+    from rvgen.dot2k import dot2k
     import argparse
     import sys
 
-    parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor')
+    parser = argparse.ArgumentParser(description='Generate kernel rv monitor')
     parser.add_argument("-D", "--description", dest="description", required=False)
     parser.add_argument("-a", "--auto_patch", dest="auto_patch",
                         action="store_true", required=False,
@@ -25,7 +25,9 @@ if __name__ == '__main__':
     monitor_parser.add_argument('-n', "--model_name", dest="model_name")
     monitor_parser.add_argument("-p", "--parent", dest="parent",
                                 required=False, help="Create a monitor nested to parent")
-    monitor_parser.add_argument('-d', "--dot", dest="dot_file")
+    monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+                                help="Monitor class, either \"da\" or \"ltl\"")
+    monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
     monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
                                 help=f"Available options: {', '.join(dot2k.monitor_types.keys())}")
 
@@ -36,8 +38,14 @@ if __name__ == '__main__':
 
     try:
         if params.subcmd == "monitor":
-            print("Opening and parsing the dot file %s" % params.dot_file)
-            monitor = dot2k(params.dot_file, params.monitor_type, vars(params))
+            print("Opening and parsing the specification file %s" % params.spec)
+            if params.monitor_class == "da":
+                monitor = dot2k(params.spec, params.monitor_type, vars(params))
+            elif params.monitor_class == "ltl":
+                raise NotImplementedError
+            else:
+                print("Unknown monitor class:", params.monitor_class)
+                sys.exit(1)
         else:
             monitor = dot2k(None, None, vars(params))
     except Exception as e:

diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c
similarity index 97%
rename from tools/verification/dot2/dot2c
rename to tools/verification/rvgen/dot2c
index 3fe89ab88b65aa0aaa3c1f3f6de518ff96eef989..bf0c67c5b66c87c5f310a30e6058221889a612ee 100644 (file)
--- a/tools/verification/dot2/dot2c
+++ b/tools/verification/rvgen/dot2c
@@ -14,7 +14,7 @@
 #   Documentation/trace/rv/deterministic_automata.rst
 
 if __name__ == '__main__':
-    from dot2 import dot2c
+    from rvgen import dot2c
     import argparse
     import sys
 

diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/rvgen/dot2k_templates/Kconfig
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig
rename to tools/verification/rvgen/dot2k_templates/Kconfig

diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/tools/verification/rvgen/dot2k_templates/Kconfig_container
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/Kconfig_container
rename to tools/verification/rvgen/dot2k_templates/Kconfig_container

diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verification/rvgen/dot2k_templates/main.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main.c
rename to tools/verification/rvgen/dot2k_templates/main.c

diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/rvgen/dot2k_templates/main_container.c
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.c
rename to tools/verification/rvgen/dot2k_templates/main_container.c

diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/rvgen/dot2k_templates/main_container.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/main_container.h
rename to tools/verification/rvgen/dot2k_templates/main_container.h

diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verification/rvgen/dot2k_templates/trace.h
similarity index 100%
rename from tools/verification/dot2/dot2k_templates/trace.h
rename to tools/verification/rvgen/dot2k_templates/trace.h

diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py
similarity index 100%
rename from tools/verification/dot2/automata.py
rename to tools/verification/rvgen/rvgen/automata.py

diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
similarity index 99%
rename from tools/verification/dot2/dot2c.py
rename to tools/verification/rvgen/rvgen/dot2c.py
index fa2816ac7b61acd1e3462e943f1c2f3e70406eaa..6009caf568d924f3498bf85829817898512bdb50 100644 (file)
--- a/tools/verification/dot2/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -13,7 +13,7 @@
 # For further information, see:
 #   Documentation/trace/rv/deterministic_automata.rst
 
-from dot2.automata import Automata
+from .automata import Automata
 
 class Dot2c(Automata):
     enum_suffix = ""

diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
similarity index 98%
rename from tools/verification/dot2/dot2k.py
rename to tools/verification/rvgen/rvgen/dot2k.py
index 9ec99e297012a5761d9c1f67fbd3ab2a72436a05..e294624131943a4070ddd8b3788b908da52dca3a 100644 (file)
--- a/tools/verification/dot2/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -8,13 +8,13 @@
 # For further information, see:
 #   Documentation/trace/rv/da_monitor_synthesis.rst
 
-from dot2.dot2c import Dot2c
+from .dot2c import Dot2c
 import platform
 import os
 
 class dot2k(Dot2c):
     monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 }
-    monitor_templates_dir = "dot2/dot2k_templates/"
+    monitor_templates_dir = "rvgen/dot2k_templates/"
     rv_dir = "kernel/trace/rv"
     monitor_type = "per_cpu"
 
@@ -60,14 +60,14 @@ class dot2k(Dot2c):
         if platform.system() != "Linux":
             raise OSError("I can only run on Linux.")
 
-        kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release())
+        kernel_path = "/lib/modules/%s/build/tools/verification/rvgen/dot2k_templates/" % (platform.release())
 
         if os.path.exists(kernel_path):
             self.monitor_templates_dir = kernel_path
             return
 
-        if os.path.exists("/usr/share/dot2/dot2k_templates/"):
-            self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/"
+        if os.path.exists("/usr/share/rvgen/dot2k_templates/"):
+            self.monitor_templates_dir = "/usr/share/rvgen/dot2k_templates/"
             return
 
         raise FileNotFoundError("Could not find the template directory, do you have the kernel source installed?")