| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-ID: <e766f1fa039da6bc560ce5290ec0d5ce5ba24fc5.camel@redhat.com>
Date: Wed, 16 Apr 2025 15:21:17 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>, Steven Rostedt <rostedt@...dmis.org>,
linux-trace-kernel@...r.kernel.org, linux-kernel@...r.kernel.org
Cc: john.ogness@...utronix.de
Subject: Re: [PATCH v3 09/22] verification/dot2k: Prepare the frontend for
LTL inclusion
On Wed, 2025-04-16 at 08:51 +0200, Nam Cao wrote:
> 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 dot2/dot2k monitor -c da -s wip.dot -t per_cpu
Some more things changed here:
python3 rvgen monitor -c da -s wip.dot -t per_cpu
For the rest, all changes in the scripts (11-12/22) look good to me.
Reviewed-by: Gabriele Monaco <gmonaco@...hat.com>
Thanks,
Gabriele
>
> Signed-off-by: Nam Cao <namcao@...utronix.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?")
Powered by blists - more mailing lists