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
Reviewed-by: Gabriele Monaco <gmon...@redhat.com>
Signed-off-by: Nam Cao <nam...@linutronix.de>
---
tools/verification/{dot2 => rvgen}/Makefile | 10 +++++-----
.../{dot2/dot2k => rvgen/__main__.py} | 18 +++++++++++++-----
tools/verification/{dot2 => rvgen}/dot2c | 2 +-
.../{dot2 => rvgen}/dot2k_templates/Kconfig | 0
.../dot2k_templates/Kconfig_container | 0
.../{dot2 => rvgen}/dot2k_templates/main.c | 0
.../dot2k_templates/main_container.c | 0
.../dot2k_templates/main_container.h | 0
.../{dot2 => rvgen}/dot2k_templates/trace.h | 0
.../{dot2 => rvgen/rvgen}/automata.py | 0
.../{dot2 => rvgen/rvgen}/dot2c.py | 2 +-
.../{dot2 => rvgen/rvgen}/dot2k.py | 10 +++++-----
12 files changed, 25 insertions(+), 17 deletions(-)
rename tools/verification/{dot2 => rvgen}/Makefile (55%)
rename tools/verification/{dot2/dot2k => rvgen/__main__.py} (72%)
rename tools/verification/{dot2 => rvgen}/dot2c (97%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/Kconfig_container
(100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main.c (100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.c
(100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/main_container.h
(100%)
rename tools/verification/{dot2 => rvgen}/dot2k_templates/trace.h (100%)
rename tools/verification/{dot2 => rvgen/rvgen}/automata.py (100%)
rename tools/verification/{dot2 => rvgen/rvgen}/dot2c.py (99%)
rename tools/verification/{dot2 => rvgen/rvgen}/dot2k.py (98%)
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 021beb07a521..cea9c21c3bce 100644
--- 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 133fb17d9d47..994d320ad2d1 100644
--- 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 3fe89ab88b65..bf0c67c5b66c 100644
--- 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 fa2816ac7b61..6009caf568d9 100644
--- 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 9ec99e297012..e29462413194 100644
--- 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?")
--
2.39.5
