diff options
Diffstat (limited to 'tools/verification')
46 files changed, 3881 insertions, 0 deletions
diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000000..d7ce62102733 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT) diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl new file mode 100644 index 000000000000..6379bbeb6212 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,22 @@ +RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) + and ((not WAKE) until RT_FRIENDLY_WAKE) + +RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + +RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI) + +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/sched/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000000..77bb64669416 --- /dev/null +++ b/tools/verification/models/sched/nrp.dot @@ -0,0 +1,29 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = doublecircle] "any_thread_running"}; + {node [shape = circle] "any_thread_running"}; + {node [shape = circle] "nested_preempt"}; + {node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"}; + {node [shape = circle] "preempt_irq"}; + {node [shape = circle] "rescheduling"}; + "__init_preempt_irq" -> "preempt_irq"; + "any_thread_running" [label = "any_thread_running", color = green3]; + "any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ]; + "any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ]; + "nested_preempt" [label = "nested_preempt"]; + "nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "nested_preempt" -> "nested_preempt" [ label = "irq_entry" ]; + "nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ]; + "preempt_irq" [label = "preempt_irq"]; + "preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ]; + "rescheduling" [label = "rescheduling"]; + "rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "rescheduling" -> "preempt_irq" [ label = "irq_entry" ]; + "rescheduling" -> "rescheduling" [ label = "sched_need_resched" ]; + { rank = min ; + "__init_preempt_irq"; + "preempt_irq"; + } +} diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot new file mode 100644 index 000000000000..840052f6952b --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,35 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_disabled"}; + {node [shape = circle] "disabled"}; + {node [shape = doublecircle] "enabled"}; + {node [shape = circle] "enabled"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "irq_disabled"}; + {node [shape = circle] "preempt_disabled"}; + "__init_disabled" -> "disabled"; + "disabled" [label = "disabled"]; + "disabled" -> "disabled" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "disabled" -> "irq_disabled" [ label = "preempt_enable" ]; + "disabled" -> "preempt_disabled" [ label = "irq_enable" ]; + "enabled" [label = "enabled", color = green3]; + "enabled" -> "enabled" [ label = "preempt_enable" ]; + "enabled" -> "irq_disabled" [ label = "irq_disable" ]; + "enabled" -> "preempt_disabled" [ label = "preempt_disable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "enabled" [ label = "irq_enable" ]; + "in_irq" -> "in_irq" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "irq_disabled" [label = "irq_disabled"]; + "irq_disabled" -> "disabled" [ label = "preempt_disable" ]; + "irq_disabled" -> "enabled" [ label = "irq_enable" ]; + "irq_disabled" -> "in_irq" [ label = "irq_entry" ]; + "irq_disabled" -> "irq_disabled" [ label = "sched_need_resched" ]; + "preempt_disabled" [label = "preempt_disabled"]; + "preempt_disabled" -> "disabled" [ label = "irq_disable" ]; + "preempt_disabled" -> "enabled" [ label = "preempt_enable" ]; + { rank = min ; + "__init_disabled"; + "disabled"; + } +} diff --git a/tools/verification/models/sched/sco.dot b/tools/verification/models/sched/sco.dot new file mode 100644 index 000000000000..20b0e3b449a6 --- /dev/null +++ b/tools/verification/models/sched/sco.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "scheduling_context"}; + {node [shape = plaintext, style=invis, label=""] "__init_thread_context"}; + {node [shape = ellipse] "thread_context"}; + {node [shape = plaintext] "thread_context"}; + "__init_thread_context" -> "thread_context"; + "scheduling_context" [label = "scheduling_context"]; + "scheduling_context" -> "thread_context" [ label = "schedule_exit" ]; + "thread_context" [label = "thread_context", color = green3]; + "thread_context" -> "scheduling_context" [ label = "schedule_entry" ]; + "thread_context" -> "thread_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_thread_context"; + "thread_context"; + } +} diff --git a/tools/verification/models/sched/scpd.dot b/tools/verification/models/sched/scpd.dot new file mode 100644 index 000000000000..340413896765 --- /dev/null +++ b/tools/verification/models/sched/scpd.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "can_sched"}; + {node [shape = plaintext, style=invis, label=""] "__init_cant_sched"}; + {node [shape = ellipse] "cant_sched"}; + {node [shape = plaintext] "cant_sched"}; + "__init_cant_sched" -> "cant_sched"; + "can_sched" [label = "can_sched"]; + "can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ]; + "can_sched" -> "cant_sched" [ label = "preempt_enable" ]; + "cant_sched" [label = "cant_sched", color = green3]; + "cant_sched" -> "can_sched" [ label = "preempt_disable" ]; + { rank = min ; + "__init_cant_sched"; + "cant_sched"; + } +} diff --git a/tools/verification/models/sched/snep.dot b/tools/verification/models/sched/snep.dot new file mode 100644 index 000000000000..fe1300e93f21 --- /dev/null +++ b/tools/verification/models/sched/snep.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"}; + {node [shape = ellipse] "non_scheduling_context"}; + {node [shape = plaintext] "non_scheduling_context"}; + {node [shape = plaintext] "scheduling_contex"}; + "__init_non_scheduling_context" -> "non_scheduling_context"; + "non_scheduling_context" [label = "non_scheduling_context", color = green3]; + "non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ]; + "non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ]; + "scheduling_contex" [label = "scheduling_contex"]; + "scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ]; + { rank = min ; + "__init_non_scheduling_context"; + "non_scheduling_context"; + } +} diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot new file mode 100644 index 000000000000..8b71c32d4dca --- /dev/null +++ b/tools/verification/models/sched/snroc.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_other_context"}; + {node [shape = ellipse] "other_context"}; + {node [shape = plaintext] "other_context"}; + {node [shape = plaintext] "own_context"}; + "__init_other_context" -> "other_context"; + "other_context" [label = "other_context", color = green3]; + "other_context" -> "own_context" [ label = "sched_switch_in" ]; + "own_context" [label = "own_context"]; + "own_context" -> "other_context" [ label = "sched_switch_out" ]; + "own_context" -> "own_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_other_context"; + "other_context"; + } +} diff --git a/tools/verification/models/sched/sssw.dot b/tools/verification/models/sched/sssw.dot new file mode 100644 index 000000000000..4994c3e876be --- /dev/null +++ b/tools/verification/models/sched/sssw.dot @@ -0,0 +1,30 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_runnable"}; + {node [shape = doublecircle] "runnable"}; + {node [shape = circle] "runnable"}; + {node [shape = circle] "signal_wakeup"}; + {node [shape = circle] "sleepable"}; + {node [shape = circle] "sleeping"}; + "__init_runnable" -> "runnable"; + "runnable" [label = "runnable", color = green3]; + "runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ]; + "runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "runnable" -> "sleeping" [ label = "sched_switch_blocking" ]; + "signal_wakeup" [label = "signal_wakeup"]; + "signal_wakeup" -> "runnable" [ label = "signal_deliver" ]; + "signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ]; + "signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "sleepable" [label = "sleepable"]; + "sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ]; + "sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ]; + "sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ]; + "sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "runnable" [ label = "sched_wakeup" ]; + { rank = min ; + "__init_runnable"; + "runnable"; + } +} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/models/sched/sts.dot new file mode 100644 index 000000000000..8f5f38be04d5 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; + {node [shape = doublecircle] "can_sched"}; + {node [shape = circle] "can_sched"}; + {node [shape = circle] "cant_sched"}; + {node [shape = circle] "disable_to_switch"}; + {node [shape = circle] "enable_to_exit"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "scheduling"}; + {node [shape = circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label = "can_sched", color = green3]; + "can_sched" -> "cant_sched" [ label = "irq_disable" ]; + "can_sched" -> "scheduling" [ label = "schedule_entry" ]; + "cant_sched" [label = "cant_sched"]; + "cant_sched" -> "can_sched" [ label = "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label = "irq_entry" ]; + "disable_to_switch" [label = "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label = "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label = "irq_entry" ]; + "disable_to_switch" -> "switching" [ label = "sched_switch" ]; + "enable_to_exit" [label = "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label = "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label = "irq_disable\nirq_entry\nirq_enable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "in_irq" [ label = "irq_entry" ]; + "in_irq" -> "scheduling" [ label = "irq_enable" ]; + "scheduling" [label = "scheduling"]; + "scheduling" -> "disable_to_switch" [ label = "irq_disable" ]; + "switching" [label = "switching"]; + "switching" -> "enable_to_exit" [ label = "irq_enable" ]; + { rank = min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/models/wip.dot b/tools/verification/models/wip.dot new file mode 100644 index 000000000000..2a53a9700a89 --- /dev/null +++ b/tools/verification/models/wip.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "non_preemptive"}; + {node [shape = plaintext, style=invis, label=""] "__init_preemptive"}; + {node [shape = doublecircle] "preemptive"}; + {node [shape = circle] "preemptive"}; + "__init_preemptive" -> "preemptive"; + "non_preemptive" [label = "non_preemptive"]; + "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ]; + "non_preemptive" -> "preemptive" [ label = "preempt_enable" ]; + "preemptive" [label = "preemptive"]; + "preemptive" -> "non_preemptive" [ label = "preempt_disable" ]; + { rank = min ; + "__init_preemptive"; + "preemptive"; + } +} diff --git a/tools/verification/models/wwnr.dot b/tools/verification/models/wwnr.dot new file mode 100644 index 000000000000..1b206e83129c --- /dev/null +++ b/tools/verification/models/wwnr.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = plaintext, style=invis, label=""] "__init_not_running"}; + {node [shape = ellipse] "not_running"}; + {node [shape = plaintext] "not_running"}; + {node [shape = plaintext] "running"}; + "__init_not_running" -> "not_running"; + "not_running" [label = "not_running", color = green3]; + "not_running" -> "not_running" [ label = "wakeup" ]; + "not_running" -> "running" [ label = "switch_in" ]; + "running" [label = "running"]; + "running" -> "not_running" [ label = "switch_out" ]; + { rank = min ; + "__init_not_running"; + "not_running"; + } +} diff --git a/tools/verification/rv/.gitignore b/tools/verification/rv/.gitignore new file mode 100644 index 000000000000..34a486585a34 --- /dev/null +++ b/tools/verification/rv/.gitignore @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: GPL-2.0-only +rv +rv-static +fixdep +feature +FEATURE-DUMP diff --git a/tools/verification/rv/Build b/tools/verification/rv/Build new file mode 100644 index 000000000000..a44c22349d4b --- /dev/null +++ b/tools/verification/rv/Build @@ -0,0 +1 @@ +rv-y += src/ diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile new file mode 100644 index 000000000000..5b898360ba48 --- /dev/null +++ b/tools/verification/rv/Makefile @@ -0,0 +1,81 @@ +# SPDX-License-Identifier: GPL-2.0-only + +ifeq ($(srctree),) + srctree := $(patsubst %/,%,$(dir $(CURDIR))) + srctree := $(patsubst %/,%,$(dir $(srctree))) + srctree := $(patsubst %/,%,$(dir $(srctree))) +endif + +include $(srctree)/tools/scripts/Makefile.include + +# O is an alias for OUTPUT +OUTPUT := $(O) + +ifeq ($(OUTPUT),) + OUTPUT := $(CURDIR)/ +else + # subdir is used by the ../Makefile in $(call descend,) + ifneq ($(subdir),) + OUTPUT := $(OUTPUT)/$(subdir) + endif +endif + +ifneq ($(patsubst %/,,$(lastword $(OUTPUT))),) + OUTPUT := $(OUTPUT)/ +endif + +RV := $(OUTPUT)rv +RV_IN := $(RV)-in.o + +VERSION := $(shell sh -c "make -sC ../../.. kernelversion | grep -v make") +DOCSRC := ../../../Documentation/tools/rv/ + +FEATURE_TESTS := libtraceevent +FEATURE_TESTS += libtracefs +FEATURE_DISPLAY := libtraceevent +FEATURE_DISPLAY += libtracefs + +all: $(RV) + +include $(srctree)/tools/build/Makefile.include +include Makefile.rv + +# check for dependencies only on required targets +NON_CONFIG_TARGETS := clean install doc doc_clean doc_install + +config := 1 +ifdef MAKECMDGOALS + ifeq ($(filter-out $(NON_CONFIG_TARGETS),$(MAKECMDGOALS)),) + config := 0 +endif +endif + +ifeq ($(config),1) + include $(srctree)/tools/build/Makefile.feature + include Makefile.config +endif + +CFLAGS += $(INCLUDES) $(LIB_INCLUDES) + +export CFLAGS OUTPUT srctree + +$(RV): $(RV_IN) + $(QUIET_LINK)$(CC) $(LDFLAGS) -o $(RV) $(RV_IN) $(EXTLIBS) + +static: $(RV_IN) + $(eval LDFLAGS += -static) + $(QUIET_LINK)$(CC) $(LDFLAGS) -o $(RV)-static $(RV_IN) $(EXTLIBS) + +rv.%: fixdep FORCE + make -f $(srctree)/tools/build/Makefile.build dir=. $@ + +$(RV_IN): fixdep FORCE + make $(build)=rv + +clean: doc_clean fixdep-clean + $(call QUIET_CLEAN, rv) + $(Q)find . -name '*.o' -delete -o -name '\.*.cmd' -delete -o -name '\.*.d' -delete + $(Q)rm -f rv rv-static fixdep FEATURE-DUMP rv-* + $(Q)rm -rf feature + +.PHONY: FORCE clean diff --git a/tools/verification/rv/Makefile.config b/tools/verification/rv/Makefile.config new file mode 100644 index 000000000000..066302230eb2 --- /dev/null +++ b/tools/verification/rv/Makefile.config @@ -0,0 +1,48 @@ +# SPDX-License-Identifier: GPL-2.0-only + +STOP_ERROR := + +LIBTRACEEVENT_MIN_VERSION = 1.5 +LIBTRACEFS_MIN_VERSION = 1.3 + +define lib_setup + $(eval LIB_INCLUDES += $(shell sh -c "$(PKG_CONFIG) --cflags lib$(1)")) + $(eval LDFLAGS += $(shell sh -c "$(PKG_CONFIG) --libs-only-L lib$(1)")) + $(eval EXTLIBS += $(shell sh -c "$(PKG_CONFIG) --libs-only-l lib$(1)")) +endef + +$(call feature_check,libtraceevent) +ifeq ($(feature-libtraceevent), 1) + $(call detected,CONFIG_LIBTRACEEVENT) + + TEST = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEEVENT_MIN_VERSION) libtraceevent > /dev/null 2>&1 && echo y || echo n") + ifeq ($(TEST),n) + $(info libtraceevent version is too low, it must be at least $(LIBTRACEEVENT_MIN_VERSION)) + STOP_ERROR := 1 + endif + + $(call lib_setup,traceevent) +else + STOP_ERROR := 1 + $(info libtraceevent is missing. Please install libtraceevent-dev/libtraceevent-devel) +endif + +$(call feature_check,libtracefs) +ifeq ($(feature-libtracefs), 1) + $(call detected,CONFIG_LIBTRACEFS) + + TEST = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEFS_MIN_VERSION) libtracefs > /dev/null 2>&1 && echo y || echo n") + ifeq ($(TEST),n) + $(info libtracefs version is too low, it must be at least $(LIBTRACEFS_MIN_VERSION)) + STOP_ERROR := 1 + endif + + $(call lib_setup,tracefs) +else + STOP_ERROR := 1 + $(info libtracefs is missing. Please install libtracefs-dev/libtracefs-devel) +endif + +ifeq ($(STOP_ERROR),1) + $(error Please, check the errors above.) +endif diff --git a/tools/verification/rv/Makefile.rv b/tools/verification/rv/Makefile.rv new file mode 100644 index 000000000000..2497fb96c83d --- /dev/null +++ b/tools/verification/rv/Makefile.rv @@ -0,0 +1,51 @@ +# SPDX-License-Identifier: GPL-2.0-only + +define allow-override + $(if $(or $(findstring environment,$(origin $(1))),\ + $(findstring command line,$(origin $(1)))),,\ + $(eval $(1) = $(2))) +endef + +# Allow setting CC and AR, or setting CROSS_COMPILE as a prefix. +$(call allow-override,CC,$(CROSS_COMPILE)gcc) +$(call allow-override,AR,$(CROSS_COMPILE)ar) +$(call allow-override,STRIP,$(CROSS_COMPILE)strip) +$(call allow-override,PKG_CONFIG,pkg-config) +$(call allow-override,LD_SO_CONF_PATH,/etc/ld.so.conf.d/) +$(call allow-override,LDCONFIG,ldconfig) +export CC AR STRIP PKG_CONFIG LD_SO_CONF_PATH LDCONFIG + +FOPTS :=-flto=auto -ffat-lto-objects -fexceptions -fstack-protector-strong \ + -fasynchronous-unwind-tables -fstack-clash-protection +WOPTS := -O -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 \ + -Wp,-D_GLIBCXX_ASSERTIONS -Wno-maybe-uninitialized + +ifeq ($(CC),clang) + FOPTS := $(filter-out -flto=auto -ffat-lto-objects, $(FOPTS)) + WOPTS := $(filter-out -Wno-maybe-uninitialized, $(WOPTS)) +endif + +INCLUDE := -Iinclude/ +CFLAGS := -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(WOPTS) $(EXTRA_CFLAGS) $(INCLUDE) +LDFLAGS := -ggdb $(LDFLAGS) $(EXTRA_LDFLAGS) + +INSTALL := install +MKDIR := mkdir +STRIP := strip +BINDIR := /usr/bin + +.PHONY: install +install: doc_install + $(Q)$(MKDIR) -p $(DESTDIR)$(BINDIR) + $(call QUIET_INSTALL,rv)$(INSTALL) $(OUTPUT)rv -m 755 $(DESTDIR)$(BINDIR) + $(Q)@$(STRIP) $(DESTDIR)$(BINDIR)/rv + +.PHONY: doc doc_clean doc_install +doc: + $(MAKE) -C $(DOCSRC) + +doc_clean: + $(MAKE) -C $(DOCSRC) clean + +doc_install: + $(MAKE) -C $(DOCSRC) install diff --git a/tools/verification/rv/README.txt b/tools/verification/rv/README.txt new file mode 100644 index 000000000000..e96be0dfff59 --- /dev/null +++ b/tools/verification/rv/README.txt @@ -0,0 +1,38 @@ +RV: Runtime Verification + +Runtime Verification (RV) is a lightweight (yet rigorous) method that +complements classical exhaustive verification techniques (such as model +checking and theorem proving) with a more practical approach for +complex systems. + +The rv tool is the interface for a collection of monitors that aim +analysing the logical and timing behavior of Linux. + +Installing RV + +RV depends on the following libraries and tools: + + - libtracefs + - libtraceevent + +It also depends on python3-docutils to compile man pages. + +For development, we suggest the following steps for compiling rtla: + + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git + $ cd libtraceevent/ + $ make + $ sudo make install + $ cd .. + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git + $ cd libtracefs/ + $ make + $ sudo make install + $ cd .. + $ cd $rv_src + $ make + $ sudo make install + +For further information, please see rv manpage and the kernel documentation: + Runtime Verification: + Documentation/trace/rv/runtime-verification.rst diff --git a/tools/verification/rv/include/in_kernel.h b/tools/verification/rv/include/in_kernel.h new file mode 100644 index 000000000000..f3bfd3b9895f --- /dev/null +++ b/tools/verification/rv/include/in_kernel.h @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: GPL-2.0 +int ikm_list_monitors(char *container); +int ikm_run_monitor(char *monitor, int argc, char **argv); diff --git a/tools/verification/rv/include/rv.h b/tools/verification/rv/include/rv.h new file mode 100644 index 000000000000..6f668eb266cb --- /dev/null +++ b/tools/verification/rv/include/rv.h @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_DESCRIPTION 1024 +#define MAX_DA_NAME_LEN 32 + +struct monitor { + char name[MAX_DA_NAME_LEN]; + char desc[MAX_DESCRIPTION]; + int enabled; + int nested; +}; + +int should_stop(void); diff --git a/tools/verification/rv/include/trace.h b/tools/verification/rv/include/trace.h new file mode 100644 index 000000000000..8d89e8c303fa --- /dev/null +++ b/tools/verification/rv/include/trace.h @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: GPL-2.0 + +#include <tracefs.h> + +struct trace_instance { + struct tracefs_instance *inst; + struct tep_handle *tep; + struct trace_seq *seq; +}; + +int trace_instance_init(struct trace_instance *trace, char *name); +int trace_instance_start(struct trace_instance *trace); +void trace_instance_destroy(struct trace_instance *trace); + +int collect_registered_events(struct tep_event *event, struct tep_record *record, + int cpu, void *context); diff --git a/tools/verification/rv/include/utils.h b/tools/verification/rv/include/utils.h new file mode 100644 index 000000000000..f24ae8282bd2 --- /dev/null +++ b/tools/verification/rv/include/utils.h @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_PATH 1024 + +void debug_msg(const char *fmt, ...); +void err_msg(const char *fmt, ...); + +extern int config_debug; diff --git a/tools/verification/rv/src/Build b/tools/verification/rv/src/Build new file mode 100644 index 000000000000..d781983c1a79 --- /dev/null +++ b/tools/verification/rv/src/Build @@ -0,0 +1,4 @@ +rv-y += trace.o +rv-y += utils.o +rv-y += in_kernel.o +rv-y += rv.o diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c new file mode 100644 index 000000000000..4bb746ea6e17 --- /dev/null +++ b/tools/verification/rv/src/in_kernel.c @@ -0,0 +1,846 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * in kernel monitor support: allows rv to control in-kernel monitors. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ +#include <getopt.h> +#include <stdlib.h> +#include <stdio.h> +#include <string.h> +#include <errno.h> +#include <unistd.h> +#include <dirent.h> + +#include <trace.h> +#include <utils.h> +#include <rv.h> + +static int config_has_id; +static int config_is_container; +static int config_my_pid; +static int config_trace; + +static char *config_initial_reactor; +static char *config_reactor; + +/* + * __ikm_read_enable - reads monitor's enable status + * + * __does not log errors. + * + * Returns the current status, or -1 if the monitor does not exist, + * __hence not logging errors. + */ +static int __ikm_read_enable(char *monitor_name) +{ + char path[MAX_PATH]; + long long enabled; + int retval; + + snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor_name); + + retval = tracefs_instance_file_read_number(NULL, path, &enabled); + if (retval < 0) + return -1; + + return enabled; +} + +/* + * __ikm_find_monitor - find the full name of a possibly nested module + * + * __does not log errors. + * + * Returns 1 if we found the monitor, -1 on error and 0 if it does not exist. + * The string out_name is populated with the full name, which can be + * equal to monitor_name or container/monitor_name if nested + */ +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; + + 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; + } + + 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; + } + +out_free: + free(available_monitors); + return retval; +} + +/* + * ikm_read_enable - reads monitor's enable status + * + * Returns the current status, or -1 on error. + */ +static int ikm_read_enable(char *monitor_name) +{ + int enabled; + + enabled = __ikm_read_enable(monitor_name); + if (enabled < 0) { + err_msg("ikm: fail read enabled: %d\n", enabled); + return -1; + } + + debug_msg("ikm: read enabled: %d\n", enabled); + + return enabled; +} + +/* + * ikm_write_enable - write to the monitor's enable file + * + * Return the number of bytes written, -1 on error. + */ +static int ikm_write_enable(char *monitor_name, char *enable_disable) +{ + char path[MAX_PATH]; + int retval; + + debug_msg("ikm: writing enabled: %s\n", enable_disable); + + snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor_name); + retval = tracefs_instance_file_write(NULL, path, enable_disable); + if (retval < strlen(enable_disable)) { + err_msg("ikm: writing enabled: %s\n", enable_disable); + return -1; + } + + return retval; +} + +/* + * ikm_enable - enable a monitor + * + * Returns -1 on failure. Success otherwise. + */ +static int ikm_enable(char *monitor_name) +{ + return ikm_write_enable(monitor_name, "1"); +} + +/* + * ikm_disable - disable a monitor + * + * Returns -1 on failure. Success otherwise. + */ +static int ikm_disable(char *monitor_name) +{ + return ikm_write_enable(monitor_name, "0"); +} + +/* + * ikm_read_desc - read monitors' description + * + * Return a dynamically allocated string with the monitor's + * description, NULL otherwise. + */ +static char *ikm_read_desc(char *monitor_name) +{ + char path[MAX_PATH]; + char *desc; + + snprintf(path, MAX_PATH, "rv/monitors/%s/desc", monitor_name); + desc = tracefs_instance_file_read(NULL, path, NULL); + if (!desc) { + err_msg("ikm: error reading monitor %s desc\n", monitor_name); + return NULL; + } + + *strstr(desc, "\n") = '\0'; + + return desc; +} + +/* + * ikm_fill_monitor_definition - fill monitor's definition + * + * Returns -1 on error, 1 if the monitor does not belong in the container, 0 otherwise. + * container can be NULL + */ +static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *container) +{ + int enabled; + char *desc, *nested_name; + + nested_name = strstr(name, ":"); + if (nested_name) { + /* it belongs in container if it starts with "container:" */ + if (container && strstr(name, container) != name) + return 1; + *nested_name = '/'; + ++nested_name; + ikm->nested = 1; + } else { + if (container) + return 1; + nested_name = name; + ikm->nested = 0; + } + + enabled = ikm_read_enable(name); + if (enabled < 0) { + err_msg("ikm: monitor %s fail to read enable file, bug?\n", name); + return -1; + } + + desc = ikm_read_desc(name); + if (!desc) { + err_msg("ikm: monitor %s does not have desc file, bug?\n", name); + return -1; + } + + strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); + ikm->enabled = enabled; + strncpy(ikm->desc, desc, MAX_DESCRIPTION); + + free(desc); + + return 0; +} + +/* + * ikm_write_reactor - switch the reactor to *reactor + * + * Return the number or characters written, -1 on error. + */ +static int ikm_write_reactor(char *monitor_name, char *reactor) +{ + char path[MAX_PATH]; + int retval; + + snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor_name); + retval = tracefs_instance_file_write(NULL, path, reactor); + debug_msg("ikm: write \"%s\" reactors: %d\n", reactor, retval); + + return retval; +} + +/* + * ikm_read_reactor - read the reactors file + * + * Returns a dynamically allocated string with monitor's + * available reactors, or NULL on error. + */ +static char *ikm_read_reactor(char *monitor_name) +{ + char path[MAX_PATH]; + char *reactors; + + snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor_name); + reactors = tracefs_instance_file_read(NULL, path, NULL); + if (!reactors) { + err_msg("ikm: fail reading monitor's %s reactors file\n", monitor_name); + return NULL; + } + + return reactors; +} + +/* + * ikm_get_current_reactor - get the current enabled reactor + * + * Reads the reactors file and find the currently enabled + * [reactor]. + * + * Returns a dynamically allocated memory with the current + * reactor. NULL otherwise. + */ +static char *ikm_get_current_reactor(char *monitor_name) +{ + char *reactors = ikm_read_reactor(monitor_name); + char *curr_reactor = NULL; + char *start; + char *end; + + if (!reactors) + return NULL; + + start = strstr(reactors, "["); + if (!start) + goto out_free; + + start++; + + end = strstr(start, "]"); + if (!end) + goto out_free; + + *end = '\0'; + + curr_reactor = calloc(strlen(start) + 1, sizeof(char)); + if (!curr_reactor) + goto out_free; + + strncpy(curr_reactor, start, strlen(start)); + debug_msg("ikm: read current reactor %s\n", curr_reactor); + +out_free: + free(reactors); + + return curr_reactor; +} + +static int ikm_has_id(char *monitor_name) +{ + char path[MAX_PATH]; + char *format; + int has_id; + + snprintf(path, MAX_PATH, "events/rv/event_%s/format", monitor_name); + format = tracefs_instance_file_read(NULL, path, NULL); + if (!format) { + err_msg("ikm: fail reading monitor's %s format event file\n", monitor_name); + return -1; + } + + /* print fmt: "%d: %s x %s -> %s %s", REC->id, ... */ + has_id = !!strstr(format, "REC->id"); + + debug_msg("ikm: monitor %s has id: %s\n", monitor_name, has_id ? "yes" : "no"); + + free(format); + + return has_id; +} + +/** + * ikm_list_monitors - list all available monitors + * + * Returns 0 on success, -1 otherwise. + */ +int ikm_list_monitors(char *container) +{ + char *available_monitors; + struct monitor ikm = {0}; + char *curr, *next; + int retval, list_monitor = 0; + + available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); + + if (!available_monitors) { + err_msg("ikm: available monitors is not available, is CONFIG_RV enabled?\n"); + return -1; + } + + curr = available_monitors; + do { + next = strstr(curr, "\n"); + *next = '\0'; + + retval = ikm_fill_monitor_definition(curr, &ikm, container); + if (retval < 0) + err_msg("ikm: error reading %d in kernel monitor, skipping\n", curr); + + if (!retval) { + int indent = ikm.nested && !container; + + list_monitor = 1; + printf("%s%-*s %s %s\n", indent ? " - " : "", + indent ? MAX_DA_NAME_LEN - 3 : MAX_DA_NAME_LEN, + ikm.name, ikm.desc, ikm.enabled ? "[ON]" : "[OFF]"); + } + curr = ++next; + + } while (strlen(curr)); + + if (!list_monitor) { + if (container) + printf("-- No monitor found in container %s --\n", container); + else + printf("-- No monitor found --\n"); + } + + free(available_monitors); + + return 0; +} + +static void ikm_print_header(struct trace_seq *s) +{ + trace_seq_printf(s, "%16s-%-8s %5s %5s ", "<TASK>", "PID", "[CPU]", "TYPE"); + if (config_has_id) + trace_seq_printf(s, "%8s ", "ID"); + + trace_seq_printf(s, "%24s x %-24s -> %-24s %s\n", + "STATE", + "EVENT", + "NEXT_STATE", + "FINAL"); + + trace_seq_printf(s, "%16s %-8s %5s %5s ", " | ", " | ", " | ", " | "); + + if (config_has_id) + trace_seq_printf(s, "%8s ", " | "); + + trace_seq_printf(s, "%24s %-24s %-24s %s\n", + " | ", + " | ", + " | ", + "|"); + +} + +/* + * ikm_event_handler - callback to handle event events + * + * Called any time a rv:"monitor"_event events is generated. + * It parses and prints event. + */ +static int +ikm_event_handler(struct trace_seq *s, struct tep_record *record, + struct tep_event *trace_event, void *context) +{ + /* if needed: struct trace_instance *inst = context; */ + char *state, *event, *next_state; + unsigned long long final_state; + unsigned long long pid; + unsigned long long id; + int val; + bool missing_id; + + if (config_has_id) + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); + + tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); + + if (config_has_id && (config_my_pid == id)) + return 0; + else if (config_my_pid == pid) + return 0; + + tep_print_event(trace_event->tep, s, record, "%16s-%-8d [%.3d] ", + TEP_PRINT_COMM, TEP_PRINT_PID, TEP_PRINT_CPU); + + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "event "); + + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } + + state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); + event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); + next_state = tep_get_field_raw(s, trace_event, "next_state", record, &val, 0); + tep_get_field_val(s, trace_event, "final_state", record, &final_state, 1); + + trace_seq_printf(s, "%24s x %-24s -> %-24s %s\n", + state, + event, + next_state, + final_state ? "Y" : "N"); + + trace_seq_do_printf(s); + trace_seq_reset(s); + + return 0; +} + +/* + * ikm_error_handler - callback to handle error events + * + * Called any time a rv:"monitor"_errors events is generated. + * It parses and prints event. + */ +static int +ikm_error_handler(struct trace_seq *s, struct tep_record *record, + struct tep_event *trace_event, void *context) +{ + unsigned long long pid, id; + int cpu = record->cpu; + char *state, *event; + int val; + bool missing_id; + + if (config_has_id) + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); + + tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); + + if (config_has_id && config_my_pid == id) + return 0; + else if (config_my_pid == pid) + return 0; + + trace_seq_printf(s, "%8lld [%03d] ", pid, cpu); + + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "error "); + + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } + + state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); + event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); + + trace_seq_printf(s, "%24s x %s\n", state, event); + + trace_seq_do_printf(s); + trace_seq_reset(s); + + return 0; +} + +static int ikm_enable_trace_events(char *monitor_name, struct trace_instance *inst) +{ + char event[MAX_DA_NAME_LEN + 7]; /* max(error_,event_) + '0' = 7 */ + int retval; + + snprintf(event, sizeof(event), "event_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_event_handler, NULL); + + snprintf(event, sizeof(event), "error_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_error_handler, NULL); + + /* set if at least 1 monitor has id in case of a container */ + config_has_id = ikm_has_id(monitor_name); + if (config_has_id < 0) + return -1; + + + return 0; +} + +static int ikm_enable_trace_container(char *monitor_name, + struct trace_instance *inst) +{ + DIR *dp; + char *abs_path, rv_path[MAX_PATH]; + struct dirent *ep; + int retval = 0; + + snprintf(rv_path, MAX_PATH, "rv/monitors/%s", monitor_name); + abs_path = tracefs_instance_get_file(NULL, rv_path); + if (!abs_path) + return -1; + dp = opendir(abs_path); + if (!dp) + goto out_free; + + while (!retval && (ep = readdir(dp))) { + if (ep->d_type != DT_DIR || ep->d_name[0] == '.') + continue; + retval = ikm_enable_trace_events(ep->d_name, inst); + } + + closedir(dp); +out_free: + free(abs_path); + return retval; +} + +/* + * ikm_setup_trace_instance - set up a tracing instance to collect data + * + * Create a trace instance, enable rv: events and enable the trace. + * + * Returns the trace_instance * with all set, NULL otherwise. + */ +static struct trace_instance *ikm_setup_trace_instance(char *monitor_name) +{ + struct trace_instance *inst; + int retval; + + if (!config_trace) + return NULL; + + /* alloc data */ + inst = calloc(1, sizeof(*inst)); + if (!inst) { + err_msg("ikm: failed to allocate trace instance"); + goto out_err; + } + + retval = trace_instance_init(inst, monitor_name); + if (retval) + goto out_free; + + if (config_is_container) + retval = ikm_enable_trace_container(monitor_name, inst); + else + retval = ikm_enable_trace_events(monitor_name, inst); + if (retval) + goto out_inst; + + /* ready to enable */ + tracefs_trace_on(inst->inst); + + return inst; + +out_inst: + trace_instance_destroy(inst); +out_free: + free(inst); +out_err: + return NULL; +} + +/** + * ikm_destroy_trace_instance - destroy a previously created instance + */ +static void ikm_destroy_trace_instance(struct trace_instance *inst) +{ + if (!inst) + return; + + trace_instance_destroy(inst); + free(inst); +} + +/* + * ikm_usage_print_reactors - print all available reactors, one per line. + */ +static void ikm_usage_print_reactors(void) +{ + char *reactors = tracefs_instance_file_read(NULL, "rv/available_reactors", NULL); + char *start, *end; + + if (!reactors) + return; + + fprintf(stderr, " available reactors:"); + + start = reactors; + end = strstr(start, "\n"); + + while (end) { + *end = '\0'; + + fprintf(stderr, " %s", start); + + start = ++end; + end = strstr(start, "\n"); + } + + fprintf(stderr, "\n"); +} +/* + * ikm_usage - print usage + */ +static void ikm_usage(int exit_val, char *monitor_name, const char *fmt, ...) +{ + + char message[1024]; + va_list ap; + int i; + + static const char *const usage[] = { + "", + " -h/--help: print this menu and the reactor list", + " -r/--reactor 'reactor': enables the 'reactor'", + " -s/--self: when tracing (-t), also trace rv command", + " -t/--trace: trace monitor's event", + " -v/--verbose: print debug messages", + "", + NULL, + }; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, " %s\n", message); + + fprintf(stderr, "\n usage: rv mon %s [-h] [-q] [-r reactor] [-s] [-v]", monitor_name); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + + ikm_usage_print_reactors(); + exit(exit_val); +} + +/* + * parse_arguments - parse arguments and set config + */ +static int parse_arguments(char *monitor_name, int argc, char **argv) +{ + int c, retval; + + config_my_pid = getpid(); + + while (1) { + static struct option long_options[] = { + {"help", no_argument, 0, 'h'}, + {"reactor", required_argument, 0, 'r'}, + {"self", no_argument, 0, 's'}, + {"trace", no_argument, 0, 't'}, + {"verbose", no_argument, 0, 'v'}, + {0, 0, 0, 0} + }; + + /* getopt_long stores the option index here. */ + int option_index = 0; + + c = getopt_long(argc, argv, "hr:stv", long_options, &option_index); + + /* detect the end of the options. */ + if (c == -1) + break; + + switch (c) { + case 'h': + ikm_usage(0, monitor_name, "help:"); + break; + case 'r': + config_reactor = optarg; + break; + case 's': + config_my_pid = -1; + break; + case 't': + config_trace = 1; + break; + case 'v': + config_debug = 1; + break; + } + } + + if (config_reactor) { + config_initial_reactor = ikm_get_current_reactor(monitor_name); + if (!config_initial_reactor) + ikm_usage(1, monitor_name, + "ikm: failed to read current reactor, are reactors enabled?"); + + retval = ikm_write_reactor(monitor_name, config_reactor); + if (retval <= 0) + ikm_usage(1, monitor_name, + "ikm: failed to set %s reactor, is it available?", + config_reactor); + } + + debug_msg("ikm: my pid is %d\n", config_my_pid); + + return 0; +} + +/** + * ikm_run_monitor - apply configs and run the monitor + * + * Returns 1 if a monitor was found an executed, 0 if no + * monitors were found, or -1 on error. + */ +int ikm_run_monitor(char *monitor_name, int argc, char **argv) +{ + struct trace_instance *inst = NULL; + char *nested_name, full_name[2*MAX_DA_NAME_LEN]; + int retval; + + nested_name = strstr(monitor_name, ":"); + if (nested_name) + ++nested_name; + else + nested_name = monitor_name; + + retval = __ikm_find_monitor_name(monitor_name, full_name); + if (!retval) + return 0; + if (retval < 0) { + err_msg("ikm: error finding monitor %s\n", nested_name); + return -1; + } + + retval = __ikm_read_enable(full_name); + if (retval) { + err_msg("ikm: monitor %s (in-kernel) is already enabled\n", nested_name); + return -1; + } + + /* we should be good to go */ + retval = parse_arguments(full_name, argc, argv); + if (retval) + ikm_usage(1, nested_name, "ikm: failed parsing arguments"); + + if (config_trace) { + inst = ikm_setup_trace_instance(nested_name); + if (!inst) + return -1; + } + + retval = ikm_enable(full_name); + if (retval < 0) + goto out_free_instance; + + if (config_trace) + ikm_print_header(inst->seq); + + while (!should_stop()) { + if (config_trace) { + retval = tracefs_iterate_raw_events(inst->tep, + inst->inst, + NULL, + 0, + collect_registered_events, + inst); + if (retval) { + err_msg("ikm: error reading trace buffer\n"); + break; + } + } + + sleep(1); + } + + ikm_disable(full_name); + ikm_destroy_trace_instance(inst); + + if (config_reactor && config_initial_reactor) + ikm_write_reactor(full_name, config_initial_reactor); + + return 1; + +out_free_instance: + ikm_destroy_trace_instance(inst); + if (config_reactor && config_initial_reactor) + ikm_write_reactor(full_name, config_initial_reactor); + return -1; +} diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c new file mode 100644 index 000000000000..b8fe24a87d97 --- /dev/null +++ b/tools/verification/rv/src/rv.c @@ -0,0 +1,201 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * rv tool, the interface for the Linux kernel RV subsystem and home of + * user-space controlled monitors. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <stdlib.h> +#include <signal.h> +#include <unistd.h> + +#include <trace.h> +#include <utils.h> +#include <in_kernel.h> + +static int stop_session; + +/* + * stop_rv - tell monitors to stop + */ +static void stop_rv(int sig) +{ + stop_session = 1; +} + +/** + * should_stop - check if the monitor should stop. + * + * Returns 1 if the monitor should stop, 0 otherwise. + */ +int should_stop(void) +{ + return stop_session; +} + +/* + * rv_list - list all available monitors + */ +static void rv_list(int argc, char **argv) +{ + static const char *const usage[] = { + "", + " usage: rv list [-h] [container]", + "", + " list all available monitors", + "", + " -h/--help: print this menu", + "", + " [container]: list only monitors in this container", + NULL, + }; + int i, print_help = 0, retval = 0; + char *container = NULL; + + if (argc == 2) { + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { + print_help = 1; + retval = 0; + } else if (argv[1][0] == '-') { + /* assume invalid option */ + print_help = 1; + retval = 1; + } else + container = argv[1]; + } else if (argc > 2) { + /* more than 2 is always usage */ + print_help = 1; + retval = 1; + } + if (print_help) { + fprintf(stderr, "rv version %s\n", VERSION); + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + exit(retval); + } + + ikm_list_monitors(container); + + exit(0); +} + +/* + * rv_mon - try to run a monitor passed as argument + */ +static void rv_mon(int argc, char **argv) +{ + char *monitor_name; + int i, run = 0; + + static const char *const usage[] = { + "", + " usage: rv mon [-h] monitor [monitor options]", + "", + " run a monitor", + "", + " -h/--help: print this menu", + "", + " monitor [monitor options]: the monitor, passing", + " the arguments to the [monitor options]", + NULL, + }; + + /* requires at least one argument */ + if (argc == 1) { + + fprintf(stderr, "rv version %s\n", VERSION); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + exit(1); + } 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); + } + + monitor_name = argv[1]; + /* + * Call all possible monitor implementations, looking + * for the [monitor]. + */ + run += ikm_run_monitor(monitor_name, argc-1, &argv[1]); + + if (!run) + err_msg("rv: monitor %s does not exist\n", monitor_name); + exit(!run); +} + +static void usage(int exit_val, const char *fmt, ...) +{ + char message[1024]; + va_list ap; + int i; + + static const char *const usage[] = { + "", + " usage: rv command [-h] [command_options]", + "", + " -h/--help: print this menu", + "", + " command: run one of the following command:", + " list: list all available monitors", + " mon: run a monitor", + "", + " [command options]: each command has its own set of options", + " run rv command -h for further information", + NULL, + }; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "rv version %s: %s\n", VERSION, message); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + + exit(exit_val); +} + +/* + * main - select which main sending the command + * + * main itself redirects the arguments to the sub-commands + * to handle the options. + * + * subcommands should exit. + */ +int main(int argc, char **argv) +{ + if (geteuid()) + usage(1, "%s needs root permission", argv[0]); + + if (argc <= 1) + usage(1, "%s requires a command", argv[0]); + + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) + usage(0, "help"); + + if (!strcmp(argv[1], "list")) + rv_list(--argc, &argv[1]); + + if (!strcmp(argv[1], "mon")) { + /* + * monitor's main should monitor should_stop() function. + * and exit. + */ + signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); + + rv_mon(argc - 1, &argv[1]); + } + + /* invalid sub-command */ + usage(1, "%s does not know the %s command, old version?", argv[0], argv[1]); +} diff --git a/tools/verification/rv/src/trace.c b/tools/verification/rv/src/trace.c new file mode 100644 index 000000000000..1b9f9bfa1893 --- /dev/null +++ b/tools/verification/rv/src/trace.c @@ -0,0 +1,133 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * trace helpers. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <sys/sendfile.h> +#include <tracefs.h> +#include <signal.h> +#include <stdlib.h> +#include <unistd.h> +#include <errno.h> + +#include <rv.h> +#include <trace.h> +#include <utils.h> + +/* + * create_instance - create a trace instance with *instance_name + */ +static struct tracefs_instance *create_instance(char *instance_name) +{ + return tracefs_instance_create(instance_name); +} + +/* + * destroy_instance - remove a trace instance and free the data + */ +static void destroy_instance(struct tracefs_instance *inst) +{ + tracefs_instance_destroy(inst); + tracefs_instance_free(inst); +} + +/** + * collect_registered_events - call the existing callback function for the event + * + * If an event has a registered callback function, call it. + * Otherwise, ignore the event. + * + * Returns 0 if the event was collected, 1 if the tool should stop collecting trace. + */ +int +collect_registered_events(struct tep_event *event, struct tep_record *record, + int cpu, void *context) +{ + struct trace_instance *trace = context; + struct trace_seq *s = trace->seq; + + if (should_stop()) + return 1; + + if (!event->handler) + return 0; + + event->handler(s, record, event, context); + + return 0; +} + +/** + * trace_instance_destroy - destroy and free a rv trace instance + */ +void trace_instance_destroy(struct trace_instance *trace) +{ + if (trace->inst) { + destroy_instance(trace->inst); + trace->inst = NULL; + } + + if (trace->seq) { + free(trace->seq); + trace->seq = NULL; + } + + if (trace->tep) { + tep_free(trace->tep); + trace->tep = NULL; + } +} + +/** + * trace_instance_init - create a trace instance + * + * It is more than the tracefs instance, as it contains other + * things required for the tracing, such as the local events and + * a seq file. + * + * Note that the trace instance is returned disabled. This allows + * the tool to apply some other configs, like setting priority + * to the kernel threads, before starting generating trace entries. + * + * Returns 0 on success, non-zero otherwise. + */ +int trace_instance_init(struct trace_instance *trace, char *name) +{ + trace->seq = calloc(1, sizeof(*trace->seq)); + if (!trace->seq) + goto out_err; + + trace_seq_init(trace->seq); + + trace->inst = create_instance(name); + if (!trace->inst) + goto out_err; + + trace->tep = tracefs_local_events(NULL); + if (!trace->tep) + goto out_err; + + /* + * Let the main enable the record after setting some other + * things such as the priority of the tracer's threads. + */ + tracefs_trace_off(trace->inst); + + return 0; + +out_err: + trace_instance_destroy(trace); + return 1; +} + +/** + * trace_instance_start - start tracing a given rv instance + * + * Returns 0 on success, -1 otherwise. + */ +int trace_instance_start(struct trace_instance *trace) +{ + return tracefs_trace_on(trace->inst); +} diff --git a/tools/verification/rv/src/utils.c b/tools/verification/rv/src/utils.c new file mode 100644 index 000000000000..5677b439dc2f --- /dev/null +++ b/tools/verification/rv/src/utils.c @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * util functions. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <stdarg.h> +#include <stdio.h> +#include <utils.h> + +int config_debug; + +#define MAX_MSG_LENGTH 1024 + +/** + * err_msg - print an error message to the stderr + */ +void err_msg(const char *fmt, ...) +{ + char message[MAX_MSG_LENGTH]; + va_list ap; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "%s", message); +} + +/** + * debug_msg - print a debug message to stderr if debug is set + */ +void debug_msg(const char *fmt, ...) +{ + char message[MAX_MSG_LENGTH]; + va_list ap; + + if (!config_debug) + return; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "%s", message); +} diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore new file mode 100644 index 000000000000..1e288a076560 --- /dev/null +++ b/tools/verification/rvgen/.gitignore @@ -0,0 +1,3 @@ +__pycache__/ +parser.out +parsetab.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile new file mode 100644 index 000000000000..cfc4056c1e87 --- /dev/null +++ b/tools/verification/rvgen/Makefile @@ -0,0 +1,27 @@ +INSTALL=install + +prefix ?= /usr +bindir ?= $(prefix)/bin +mandir ?= $(prefix)/share/man +srcdir ?= $(prefix)/src + +PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') + +.PHONY: all +all: + +.PHONY: clean +clean: + +.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/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 + $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen + cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py new file mode 100644 index 000000000000..fa6fc1f4de2f --- /dev/null +++ b/tools/verification/rvgen/__main__.py @@ -0,0 +1,67 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +if __name__ == '__main__': + from rvgen.dot2k import dot2k + from rvgen.generator import Monitor + from rvgen.container import Container + from rvgen.ltl2k import ltl2k + 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", + 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.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('-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(Monitor.monitor_types.keys())}") + + container_parser = subparsers.add_parser("container") + container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + + params = parser.parse_args() + + try: + if params.subcmd == "monitor": + 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": + monitor = ltl2k(params.spec, params.monitor_type, vars(params)) + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) + else: + monitor = Container(vars(params)) + except Exception as e: + print('Error: '+ str(e)) + print("Sorry : :-(") + sys.exit(1) + + print("Writing the monitor into the directory %s" % monitor.name) + monitor.print_files() + print("Almost done, checklist") + if params.subcmd == "monitor": + print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) + print(monitor.fill_tracepoint_tooltip()) + print(monitor.fill_makefile_tooltip()) + print(monitor.fill_kconfig_tooltip()) + print(monitor.fill_monitor_tooltip()) diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c new file mode 100644 index 000000000000..bf0c67c5b66c --- /dev/null +++ b/tools/verification/rvgen/dot2c @@ -0,0 +1,26 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2c: parse an automata in dot file digraph format into a C +# +# This program was written in the development of this paper: +# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. +# "Efficient Formal Verification for the Linux Kernel." International +# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. +# +# For further information, see: +# Documentation/trace/rv/deterministic_automata.rst + +if __name__ == '__main__': + from rvgen import dot2c + import argparse + import sys + + parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure') + parser.add_argument('dot_file', help='The dot file to be converted') + + args = parser.parse_args() + d = dot2c.Dot2c(args.dot_file) + d.print_model_classic() diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py new file mode 100644 index 000000000000..d9a3fe2b74bf --- /dev/null +++ b/tools/verification/rvgen/rvgen/automata.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Automata object: parse an automata in dot file digraph format into a python object +# +# For further information, see: +# Documentation/trace/rv/deterministic_automata.rst + +import ntpath + +class Automata: + """Automata class: Reads a dot file and part it as an automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + invalid_state_str = "INVALID_STATE" + + 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.events = self.__get_event_variables() + self.function = self.__create_matrix() + self.events_start, self.events_start_run = self.__store_init_events() + + def __get_model_name(self): + basename = ntpath.basename(self.__dot_path) + if not basename.endswith(".dot") and not basename.endswith(".gv"): + print("not a dot file") + raise Exception("not a dot file: %s" % self.__dot_path) + + model_name = ntpath.splitext(basename)[0] + if model_name.__len__() == 0: + raise Exception("not a dot file: %s" % self.__dot_path) + + return model_name + + def __open_dot(self): + cursor = 0 + dot_lines = [] + try: + dot_file = open(self.__dot_path) + except: + raise Exception("Cannot open the file: %s" % self.__dot_path) + + dot_lines = dot_file.read().splitlines() + dot_file.close() + + # checking the first line: + line = dot_lines[cursor].split() + + if (line[0] != "digraph") and (line[1] != "state_automaton"): + raise Exception("Not a valid .dot format: %s" % self.__dot_path) + else: + cursor += 1 + return dot_lines + + def __get_cursor_begin_states(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + return cursor + + def __get_cursor_begin_events(self): + cursor = 0 + while self.__dot_lines[cursor].split()[0] != "{node": + cursor += 1 + while self.__dot_lines[cursor].split()[0] == "{node": + cursor += 1 + # skip initial state transition + cursor += 1 + return cursor + + def __get_state_variables(self): + # wait for node declaration + states = [] + final_states = [] + + has_final_states = False + cursor = self.__get_cursor_begin_states() + + # process nodes + while self.__dot_lines[cursor].split()[0] == "{node": + line = self.__dot_lines[cursor].split() + raw_state = line[-1] + + # "enabled_fired"}; -> enabled_fired + state = raw_state.replace('"', '').replace('};', '').replace(',','_') + if state[0:7] == "__init_": + initial_state = state[7:] + else: + states.append(state) + if "doublecircle" in self.__dot_lines[cursor]: + final_states.append(state) + has_final_states = True + + if "ellipse" in self.__dot_lines[cursor]: + final_states.append(state) + has_final_states = True + + cursor += 1 + + states = sorted(set(states)) + states.remove(initial_state) + + # Insert the initial state at the bein og the states + states.insert(0, initial_state) + + if not has_final_states: + final_states.append(initial_state) + + return states, initial_state, final_states + + def __get_event_variables(self): + # here we are at the begin of transitions, take a note, we will return later. + cursor = self.__get_cursor_begin_events() + + events = [] + while self.__dot_lines[cursor].lstrip()[0] == '"': + # transitions have the format: + # "all_fired" -> "both_fired" [ label = "disable_irq" ]; + # ------------ event is here ------------^^^^^ + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + event = line[-2].replace('"','') + + # when a transition has more than one lables, they are like this + # "local_irq_enable\nhw_local_irq_enable_n" + # so split them. + + event = event.replace("\\n", " ") + for i in event.split(): + events.append(i) + cursor += 1 + + return sorted(set(events)) + + def __create_matrix(self): + # transform the array into a dictionary + events = self.events + states = self.states + events_dict = {} + states_dict = {} + nr_event = 0 + for event in events: + events_dict[event] = nr_event + nr_event += 1 + + nr_state = 0 + for state in states: + states_dict[state] = nr_state + nr_state += 1 + + # declare the matrix.... + matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)] + + # and we are back! Let's fill the matrix + cursor = self.__get_cursor_begin_events() + + while self.__dot_lines[cursor].lstrip()[0] == '"': + if self.__dot_lines[cursor].split()[1] == "->": + line = self.__dot_lines[cursor].split() + origin_state = line[0].replace('"','').replace(',','_') + dest_state = line[2].replace('"','').replace(',','_') + possible_events = line[-2].replace('"','').replace("\\n", " ") + for event in possible_events.split(): + matrix[states_dict[origin_state]][events_dict[event]] = dest_state + cursor += 1 + + return matrix + + def __store_init_events(self): + events_start = [False] * len(self.events) + events_start_run = [False] * len(self.events) + for i, _ in enumerate(self.events): + curr_event_will_init = 0 + curr_event_from_init = False + curr_event_used = 0 + for j, _ in enumerate(self.states): + if self.function[j][i] != self.invalid_state_str: + curr_event_used += 1 + if self.function[j][i] == self.initial_state: + curr_event_will_init += 1 + if self.function[0][i] != self.invalid_state_str: + curr_event_from_init = True + # this event always leads to init + if curr_event_will_init and curr_event_used == curr_event_will_init: + events_start[i] = True + # this event is only called from init + if curr_event_from_init and curr_event_used == 1: + events_start_run[i] = True + return events_start, events_start_run + + def is_start_event(self, event): + return self.events_start[self.events.index(event)] + + def is_start_run_event(self, event): + # prefer handle_start_event if there + if any(self.events_start): + return False + return self.events_start_run[self.events.index(event)] diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py new file mode 100644 index 000000000000..51f188530b4d --- /dev/null +++ b/tools/verification/rvgen/rvgen/container.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Generator for runtime verification monitor container + +from . import generator + + +class Container(generator.RVGenerator): + template_dir = "container" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.name = extra_params.get("model_name") + self.main_h = self._read_template_file("main.h") + + def fill_model_h(self): + main_h = self.main_h + main_h = main_h.replace("%%MODEL_NAME%%", self.name) + return main_h + + def fill_kconfig_tooltip(self): + """Override to produce a marker for this container in the Kconfig""" + container_marker = self._kconfig_marker(self.name) + "\n" + result = super().fill_kconfig_tooltip() + if self.auto_patch: + self._patch_file("Kconfig", + self._kconfig_marker(), container_marker) + return result + return result + container_marker diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py new file mode 100644 index 000000000000..b9b6f14cc536 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2c: parse an automata in dot file digraph format into a C +# +# This program was written in the development of this paper: +# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. +# "Efficient Formal Verification for the Linux Kernel." International +# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. +# +# For further information, see: +# Documentation/trace/rv/deterministic_automata.rst + +from .automata import Automata + +class Dot2c(Automata): + enum_suffix = "" + enum_states_def = "states" + enum_events_def = "events" + struct_automaton_def = "automaton" + var_automaton_def = "aut" + + def __init__(self, file_path, model_name=None): + super().__init__(file_path, model_name) + self.line_length = 100 + + def __buff_to_string(self, buff): + string = "" + + for line in buff: + string = string + line + "\n" + + # cut off the last \n + return string[:-1] + + def __get_enum_states_content(self): + buff = [] + buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix)) + for state in self.states: + if state != self.initial_state: + buff.append("\t%s%s," % (state, self.enum_suffix)) + buff.append("\tstate_max%s" % (self.enum_suffix)) + + return buff + + def get_enum_states_string(self): + buff = self.__get_enum_states_content() + return self.__buff_to_string(buff) + + def format_states_enum(self): + buff = [] + buff.append("enum %s {" % self.enum_states_def) + buff.append(self.get_enum_states_string()) + buff.append("};\n") + + return buff + + def __get_enum_events_content(self): + buff = [] + first = True + for event in self.events: + if first: + buff.append("\t%s%s = 0," % (event, self.enum_suffix)) + first = False + else: + buff.append("\t%s%s," % (event, self.enum_suffix)) + + buff.append("\tevent_max%s" % self.enum_suffix) + + return buff + + def get_enum_events_string(self): + buff = self.__get_enum_events_content() + return self.__buff_to_string(buff) + + def format_events_enum(self): + buff = [] + buff.append("enum %s {" % self.enum_events_def) + buff.append(self.get_enum_events_string()) + buff.append("};\n") + + return buff + + def get_minimun_type(self): + min_type = "unsigned char" + + if self.states.__len__() > 255: + min_type = "unsigned short" + + if self.states.__len__() > 65535: + min_type = "unsigned int" + + if self.states.__len__() > 1000000: + raise Exception("Too many states: %d" % self.states.__len__()) + + return min_type + + def format_automaton_definition(self): + min_type = self.get_minimun_type() + buff = [] + buff.append("struct %s {" % self.struct_automaton_def) + buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix)) + buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix)) + buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix)) + buff.append("\t%s initial_state;" % min_type) + buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix)) + buff.append("};\n") + return buff + + def format_aut_init_header(self): + buff = [] + buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def)) + return buff + + def __get_string_vector_per_line_content(self, buff): + first = True + string = "" + for entry in buff: + if first: + string = string + "\t\t\"" + entry + first = False; + else: + string = string + "\",\n\t\t\"" + entry + string = string + "\"" + + return string + + def get_aut_init_events_string(self): + return self.__get_string_vector_per_line_content(self.events) + + def get_aut_init_states_string(self): + return self.__get_string_vector_per_line_content(self.states) + + def format_aut_init_events_string(self): + buff = [] + buff.append("\t.event_names = {") + buff.append(self.get_aut_init_events_string()) + buff.append("\t},") + return buff + + def format_aut_init_states_string(self): + buff = [] + buff.append("\t.state_names = {") + buff.append(self.get_aut_init_states_string()) + buff.append("\t},") + + return buff + + def __get_max_strlen_of_states(self): + max_state_name = max(self.states, key = len).__len__() + return max(max_state_name, self.invalid_state_str.__len__()) + + def get_aut_init_function(self): + nr_states = self.states.__len__() + nr_events = self.events.__len__() + buff = [] + + maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) + tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" + comma_space = 2 # ", " count last comma here + linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length + for x in range(nr_states): + line = "\t\t{\n" if linetoolong else "\t\t{ " + for y in range(nr_events): + next_state = self.function[x][y] + if next_state != self.invalid_state_str: + next_state = self.function[x][y] + self.enum_suffix + + if linetoolong: + line += "\t\t\t%s" % next_state + else: + line += "%*s" % (maxlen, next_state) + if y != nr_events-1: + line += ",\n" if linetoolong else ", " + else: + line += "\n\t\t}," if linetoolong else " }," + buff.append(line) + + return self.__buff_to_string(buff) + + def format_aut_init_function(self): + buff = [] + buff.append("\t.function = {") + buff.append(self.get_aut_init_function()) + buff.append("\t},") + + return buff + + def get_aut_init_initial_state(self): + return self.initial_state + + def format_aut_init_initial_state(self): + buff = [] + initial_state = self.get_aut_init_initial_state() + buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",") + + return buff + + def get_aut_init_final_states(self): + line = "" + first = True + for state in self.states: + if first == False: + line = line + ', ' + else: + first = False + + if self.final_states.__contains__(state): + line = line + '1' + else: + line = line + '0' + return line + + def format_aut_init_final_states(self): + buff = [] + buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states()) + + return buff + + def __get_automaton_initialization_footer_string(self): + footer = "};\n" + return footer + + def format_aut_init_footer(self): + buff = [] + buff.append(self.__get_automaton_initialization_footer_string()) + + return buff + + def format_invalid_state(self): + buff = [] + buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix)) + + return buff + + def format_model(self): + buff = [] + buff += self.format_states_enum() + buff += self.format_invalid_state() + buff += self.format_events_enum() + buff += self.format_automaton_definition() + buff += self.format_aut_init_header() + buff += self.format_aut_init_states_string() + buff += self.format_aut_init_events_string() + buff += self.format_aut_init_function() + buff += self.format_aut_init_initial_state() + buff += self.format_aut_init_final_states() + buff += self.format_aut_init_footer() + + return buff + + def print_model_classic(self): + buff = self.format_model() + print(self.__buff_to_string(buff)) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py new file mode 100644 index 000000000000..ed0a3c901106 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +from .dot2c import Dot2c +from .generator import Monitor + + +class dot2k(Monitor, Dot2c): + template_dir = "dot2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + self.monitor_type = MonitorType + Monitor.__init__(self, extra_params) + Dot2c.__init__(self, file_path, extra_params.get("model_name")) + self.enum_suffix = "_%s" % self.name + + def fill_monitor_type(self): + return self.monitor_type.upper() + + def fill_tracepoint_handlers_skel(self): + buff = [] + for event in self.events: + buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) + buff.append("{") + handle = "handle_event" + if self.is_start_event(event): + buff.append("\t/* XXX: validate that this event always leads to the initial state */") + handle = "handle_start_event" + elif self.is_start_run_event(event): + buff.append("\t/* XXX: validate that this event is only valid in the initial state */") + handle = "handle_start_run_event" + if self.monitor_type == "per_task": + buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); + buff.append("\tda_%s_%s(p, %s%s);" % (handle, self.name, event, self.enum_suffix)); + else: + buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix)); + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + buff = [] + for event in self.events: + buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_tracepoint_detach_helper(self): + buff = [] + for event in self.events: + buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_model_h_header(self): + buff = [] + buff.append("/* SPDX-License-Identifier: GPL-2.0 */") + buff.append("/*") + buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) + buff.append(" * For further information about this format, see kernel documentation:") + buff.append(" * Documentation/trace/rv/deterministic_automata.rst") + buff.append(" */") + buff.append("") + + return buff + + def fill_model_h(self): + # + # Adjust the definition names + # + self.enum_states_def = "states_%s" % self.name + self.enum_events_def = "events_%s" % self.name + self.struct_automaton_def = "automaton_%s" % self.name + self.var_automaton_def = "automaton_%s" % self.name + + buff = self.fill_model_h_header() + buff += self.format_model() + + return '\n'.join(buff) + + def fill_monitor_class_type(self): + if self.monitor_type == "per_task": + return "DA_MON_EVENTS_ID" + return "DA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self): + if self.monitor_type == "per_task": + return "da_monitor_id" + return "da_monitor" + + def fill_tracepoint_args_skel(self, tp_type): + buff = [] + tp_args_event = [ + ("char *", "state"), + ("char *", "event"), + ("char *", "next_state"), + ("bool ", "final_state"), + ] + tp_args_error = [ + ("char *", "state"), + ("char *", "event"), + ] + tp_args_id = ("int ", "id") + tp_args = tp_args_event if tp_type == "event" else tp_args_error + if self.monitor_type == "per_task": + tp_args.insert(0, tp_args_id) + tp_proto_c = ", ".join([a+b for a,b in tp_args]) + tp_args_c = ", ".join([b for a,b in tp_args]) + buff.append(" TP_PROTO(%s)," % tp_proto_c) + buff.append(" TP_ARGS(%s)" % tp_args_c) + return '\n'.join(buff) + + def fill_main_c(self): + main_c = super().fill_main_c() + + min_type = self.get_minimun_type() + nr_events = len(self.events) + monitor_type = self.fill_monitor_type() + + main_c = main_c.replace("%%MIN_TYPE%%", min_type) + main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) + main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) + + return main_c diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py new file mode 100644 index 000000000000..3441385c1177 --- /dev/null +++ b/tools/verification/rvgen/rvgen/generator.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Abtract class for generating kernel runtime verification monitors from specification file + +import platform +import os + + +class RVGenerator: + rv_dir = "kernel/trace/rv" + + def __init__(self, extra_params={}): + 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) + 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() + + def __fill_rv_kernel_dir(self): + + # 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 os.path.exists(kernel_path): + self.rv_dir = kernel_path + return + + if platform.system() != "Linux": + raise OSError("I can only run on Linux.") + + kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), 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 + return + + raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") + + def _read_file(self, path): + try: + fd = open(path, 'r') + except OSError: + raise Exception("Cannot open the file: %s" % path) + + content = fd.read() + + fd.close() + return content + + def _read_template_file(self, file): + try: + path = os.path.join(self.abs_template_dir, file) + return self._read_file(path) + except Exception: + # 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) + return self._read_file(path) + + def fill_parent(self): + return "&rv_%s" % self.parent if self.parent else "NULL" + + def fill_include_parent(self): + if self.parent: + return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent) + return "" + + def fill_tracepoint_handlers_skel(self): + return "NotImplemented" + + def fill_tracepoint_attach_probe(self): + return "NotImplemented" + + def fill_tracepoint_detach_helper(self): + return "NotImplemented" + + def fill_main_c(self): + main_c = self.main_c + tracepoint_handlers = self.fill_tracepoint_handlers_skel() + tracepoint_attach = self.fill_tracepoint_attach_probe() + tracepoint_detach = self.fill_tracepoint_detach_helper() + parent = self.fill_parent() + parent_include = self.fill_include_parent() + + main_c = main_c.replace("%%MODEL_NAME%%", self.name) + main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers) + main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach) + main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach) + main_c = main_c.replace("%%DESCRIPTION%%", self.description) + main_c = main_c.replace("%%PARENT%%", parent) + main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include) + + return main_c + + def fill_model_h(self): + return "NotImplemented" + + def fill_monitor_class_type(self): + return "NotImplemented" + + def fill_monitor_class(self): + return "NotImplemented" + + def fill_tracepoint_args_skel(self, tp_type): + return "NotImplemented" + + def fill_monitor_deps(self): + buff = [] + buff.append(" # XXX: add dependencies if there") + if self.parent: + buff.append(" depends on RV_MON_%s" % self.parent.upper()) + buff.append(" default y") + return '\n'.join(buff) + + def fill_kconfig(self): + kconfig = self.kconfig + monitor_class_type = self.fill_monitor_class_type() + monitor_deps = self.fill_monitor_deps() + kconfig = kconfig.replace("%%MODEL_NAME%%", self.name) + kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper()) + kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) + kconfig = kconfig.replace("%%DESCRIPTION%%", self.description) + kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) + return kconfig + + def _patch_file(self, file, marker, line): + assert self.auto_patch + file_to_patch = os.path.join(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) + + def fill_tracepoint_tooltip(self): + monitor_class_type = self.fill_monitor_class_type() + if self.auto_patch: + self._patch_file("rv_trace.h", + "// Add new monitors based on CONFIG_%s here" % monitor_class_type, + "#include <monitors/%s/%s_trace.h>" % (self.name, self.name)) + return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir + + return """ - Edit %s/rv_trace.h: +Add this line where other tracepoints are included and %s is defined: +#include <monitors/%s/%s_trace.h> +""" % (self.rv_dir, monitor_class_type, self.name, self.name) + + def _kconfig_marker(self, container=None) -> str: + return "# Add new %smonitors here" % (container + " " + if container else "") + + def fill_kconfig_tooltip(self): + if self.auto_patch: + # monitors with a container should stay together in the Kconfig + self._patch_file("Kconfig", + self._kconfig_marker(self.parent), + "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name)) + return " - Patching %s/Kconfig, double check the result" % self.rv_dir + + return """ - Edit %s/Kconfig: +Add this line where other monitors are included: +source \"kernel/trace/rv/monitors/%s/Kconfig\" +""" % (self.rv_dir, self.name) + + def fill_makefile_tooltip(self): + name = self.name + name_up = name.upper() + if self.auto_patch: + self._patch_file("Makefile", + "# Add new monitors here", + "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name)) + return " - Patching %s/Makefile, double check the result" % self.rv_dir + + return """ - Edit %s/Makefile: +Add this line where other monitors are included: +obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o +""" % (self.rv_dir, name_up, name, name) + + def fill_monitor_tooltip(self): + if self.auto_patch: + return " - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name) + return " - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir) + + def __create_directory(self): + path = self.name + if self.auto_patch: + path = os.path.join(self.rv_dir, "monitors", path) + try: + os.mkdir(path) + except FileExistsError: + return + except: + print("Fail creating the output dir: %s" % self.name) + + def __write_file(self, file_name, content): + try: + file = open(file_name, 'w') + except: + print("Fail writing to file: %s" % file_name) + + file.write(content) + + file.close() + + def _create_file(self, file_name, content): + path = "%s/%s" % (self.name, file_name) + if self.auto_patch: + path = os.path.join(self.rv_dir, "monitors", path) + self.__write_file(path, content) + + def __get_main_name(self): + path = "%s/%s" % (self.name, "main.c") + if not os.path.exists(path): + return "main.c" + return "__main.c" + + def print_files(self): + main_c = self.fill_main_c() + + self.__create_directory() + + path = "%s.c" % self.name + self._create_file(path, main_c) + + model_h = self.fill_model_h() + path = "%s.h" % self.name + self._create_file(path, model_h) + + kconfig = self.fill_kconfig() + self._create_file("Kconfig", kconfig) + + +class Monitor(RVGenerator): + monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.trace_h = self._read_template_file("trace.h") + + def fill_trace_h(self): + trace_h = self.trace_h + monitor_class = self.fill_monitor_class() + monitor_class_type = self.fill_monitor_class_type() + tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") + tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") + trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) + trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) + trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) + trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) + return trace_h + + def print_files(self): + super().print_files() + trace_h = self.fill_trace_h() + path = "%s_trace.h" % self.name + self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000000..f14e6760ac3d --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,566 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Implementation based on +# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). +# Simple On-the-fly Automatic Verification of Linear Temporal Logic. +# https://doi.org/10.1007/978-0-387-34892-6_1 +# With extra optimizations + +from ply.lex import lex +from ply.yacc import yacc + +# Grammar: +# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl +# +# Operands (opd): +# true, false, user-defined names +# +# Unary Operators (unop): +# always +# eventually +# next +# not +# +# Binary Operators (binop): +# until +# and +# or +# 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 ValueError(f"Illegal character '{t.value[0]}'") + +lexer = lex() + +class GraphNode: + uid = 0 + + def __init__(self, incoming: set['GraphNode'], new, old, _next): + self.init = False + self.outgoing = set() + self.labels = set() + self.incoming = incoming.copy() + self.new = new.copy() + self.old = old.copy() + self.next = _next.copy() + self.id = GraphNode.uid + GraphNode.uid += 1 + + def expand(self, node_set): + if not self.new: + for nd in node_set: + if nd.old == self.old and nd.next == self.next: + nd.incoming |= self.incoming + return node_set + + new_current_node = GraphNode({self}, self.next, set(), set()) + return new_current_node.expand({self} | node_set) + n = self.new.pop() + return n.expand(self, node_set) + + def __lt__(self, other): + return self.id < other.id + +class ASTNode: + uid = 1 + + def __init__(self, op): + self.op = op + self.id = ASTNode.uid + ASTNode.uid += 1 + + def __hash__(self): + return hash(self.op) + + def __eq__(self, other): + return self is other + + def __iter__(self): + yield self + yield from self.op + + def negate(self): + self.op = self.op.negate() + return self + + def expand(self, node, node_set): + 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() + return "val" + str(self.id) + + def normalize(self): + # Get rid of: + # - ALWAYS + # - EVENTUALLY + # - IMPLY + # And move all the NOT to be inside + self.op = self.op.normalize() + return self + +class BinaryOp: + op_str = "not_supported" + + def __init__(self, left: ASTNode, right: ASTNode): + self.left = left + self.right = right + + def __hash__(self): + return hash((self.left, self.right)) + + def __iter__(self): + yield from self.left + yield from self.right + + def normalize(self): + raise NotImplementedError + + def negate(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.left.op.is_temporal(): + return True + if self.right.op.is_temporal(): + return True + return self._is_temporal() + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + raise NotImplementedError + +class AndOp(BinaryOp): + op_str = '&&' + + def normalize(self): + return self + + def negate(self): + return OrOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old.add(n) + return node.expand(node_set) + + tmp = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return tmp.expand(node_set) + +class OrOp(BinaryOp): + op_str = '||' + + def normalize(self): + return self + + def negate(self): + return AndOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old |= {n} + return node.expand(node_set) + + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class UntilOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return VOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class VOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return UntilOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class ImplyOp(BinaryOp): + def normalize(self): + # P -> Q === !P | Q + return OrOp(self.left.negate(), self.right) + + def _is_temporal(self): + return False + + def negate(self): + # !(P -> Q) === !(!P | Q) === P & !Q + return AndOp(self.left, self.right.negate()) + +class UnaryOp: + def __init__(self, child: ASTNode): + self.child = child + + def __iter__(self): + yield from self.child + + def __hash__(self): + return hash(self.child) + + def normalize(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.child.op.is_temporal(): + return True + return self._is_temporal() + + def negate(self): + raise NotImplementedError + +class EventuallyOp(UnaryOp): + def __str__(self): + return "eventually " + str(self.child) + + def normalize(self): + # <>F == true U F + return UntilOp(ASTNode(Literal(True)), self.child) + + def _is_temporal(self): + return True + + def negate(self): + # !<>F == [](!F) + return AlwaysOp(self.child.negate()).normalize() + +class AlwaysOp(UnaryOp): + def normalize(self): + # []F === !(true U !F) == false V F + new = ASTNode(Literal(False)) + return VOp(new, self.child) + + def _is_temporal(self): + return True + + def negate(self): + # ![]F == <>(!F) + return EventuallyOp(self.child.negate()).normalize() + +class NextOp(UnaryOp): + def normalize(self): + return self + + def _is_temporal(self): + return True + + def negate(self): + # not (next A) == next (not A) + self.child = self.child.negate() + return self + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + tmp = GraphNode(node.incoming, + node.new, + node.old | {n}, + node.next | {n.op.child}) + return tmp.expand(node_set) + +class NotOp(UnaryOp): + def __str__(self): + return "!" + str(self.child) + + def normalize(self): + return self.child.op.negate() + + def negate(self): + return self.child.op + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if n.op.child is f: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Variable: + def __init__(self, name: str): + self.name = name + + def __hash__(self): + return hash(self.name) + + def __iter__(self): + yield from () + + def negate(self): + new = ASTNode(self) + return NotOp(new) + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if isinstance(f, NotOp) and f.op.child is n: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Literal: + def __init__(self, value: bool): + self.value = value + + def __iter__(self): + yield from () + + def __hash__(self): + return hash(self.value) + + def __str__(self): + if self.value: + return "true" + return "false" + + def negate(self): + self.value = not self.value + return self + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.value: + return node_set + 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 ValueError(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 ValueError(f"Invalid binary operator {p[2]}") + + p[0] = ASTNode(op) + +parser = yacc() + +def parse_ltl(s: str) -> ASTNode: + spec = parser.parse(s) + + rule = None + subexpr = {} + + for assign in spec: + if assign[0] == "RULE": + rule = assign[1] + else: + subexpr[assign[0]] = assign[1] + + if rule is None: + raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format") + + for node in rule: + if not isinstance(node.op, Variable): + continue + replace = subexpr.get(node.op.name) + if replace is not None: + node.op = replace.op + + return rule + +def create_graph(s: str): + atoms = set() + + ltl = parse_ltl(s) + for c in ltl: + c.normalize() + if isinstance(c.op, Variable): + atoms.add(c.op.name) + + init = GraphNode(set(), set(), set(), set()) + head = GraphNode({init}, {ltl}, set(), set()) + graph = sorted(head.expand(set())) + + for i, node in enumerate(graph): + # The id assignment during graph generation has gaps. Reassign them + node.id = i + + for incoming in node.incoming: + if incoming is init: + node.init = True + else: + incoming.outgoing.add(node) + for o in node.old: + if not o.op.is_temporal(): + node.labels.add(str(o)) + + return sorted(atoms), graph, ltl diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py new file mode 100644 index 000000000000..b075f98d50c4 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba + +COLUMN_LIMIT = 100 + +def line_len(line: str) -> int: + tabs = line.count('\t') + return tabs * 7 + len(line) + +def break_long_line(line: str, indent='') -> list[str]: + result = [] + while line_len(line) > COLUMN_LIMIT: + i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ') + result.append(line[:i]) + line = indent + line[i + 1:] + if line: + result.append(line) + return result + +def build_condition_string(node: ltl2ba.GraphNode): + if not node.labels: + return "(true)" + + result = "(" + + first = True + for label in sorted(node.labels): + if not first: + result += " && " + result += label + first = False + + result += ")" + + return result + +def abbreviate_atoms(atoms: list[str]) -> list[str]: + def shorten(s: str) -> str: + skip = ["is", "by", "or", "and"] + return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip]) + + abbrs = [] + for atom in atoms: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + break + share = atom[:i] + unique = atom[i:] + abbrs.append((shorten(share) + shorten(unique))) + return abbrs + +class ltl2k(generator.Monitor): + template_dir = "ltl2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + if MonitorType != "per_task": + raise NotImplementedError("Only per_task monitor is supported for LTL") + super().__init__(extra_params) + with open(file_path) as f: + self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read()) + self.atoms_abbr = abbreviate_atoms(self.atoms) + self.name = extra_params.get("model_name") + if not self.name: + self.name = Path(file_path).stem + + def _fill_states(self) -> str: + buf = [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append("\tS%i," % node.id) + buf.append("\tRV_NUM_BA_STATES") + buf.append("};") + buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);") + return buf + + def _fill_atoms(self): + buf = ["enum ltl_atom {"] + for a in sorted(self.atoms): + buf.append("\tLTL_%s," % a) + buf.append("\tLTL_NUM_ATOM") + buf.append("};") + buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);") + return buf + + def _fill_atoms_to_string(self): + buf = [ + "static const char *ltl_atom_str(enum ltl_atom atom)", + "{", + "\tstatic const char *const names[] = {" + ] + + for name in self.atoms_abbr: + buf.append("\t\t\"%s\"," % name) + + buf.extend([ + "\t};", + "", + "\treturn names[atom];", + "}" + ]) + return buf + + def _fill_atom_values(self, required_values): + buf = [] + for node in self.ltl: + if str(node) not in required_values: + continue + + if isinstance(node.op, ltl2ba.AndOp): + buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.OrOp): + buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.NotOp): + buf.append("\tbool %s = !%s;" % (node, node.op.child)) + required_values.add(str(node.op.child)) + + for atom in self.atoms: + if atom.lower() not in required_values: + continue + buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom)) + + buf.reverse() + + buf2 = [] + for line in buf: + buf2.extend(break_long_line(line, "\t ")) + return buf2 + + def _fill_transitions(self): + buf = [ + "static void", + "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)", + "{" + ] + + required_values = set() + for node in self.ba: + for o in sorted(node.outgoing): + required_values |= o.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.extend([ + "", + "\tswitch (state) {" + ]) + + for node in self.ba: + buf.append("\tcase S%i:" % node.id) + + for o in sorted(node.outgoing): + line = "\t\tif " + indent = "\t\t " + + line += build_condition_string(o) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t\t__set_bit(S%i, next);" % o.id) + buf.append("\t\tbreak;") + buf.extend([ + "\t}", + "}" + ]) + + return buf + + def _fill_start(self): + buf = [ + "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)", + "{" + ] + + required_values = set() + for node in self.ba: + if node.init: + required_values |= node.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.append("") + + for node in self.ba: + if not node.init: + continue + + line = "\tif " + indent = "\t " + + line += build_condition_string(node) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) + buf.append("}") + return buf + + def fill_tracepoint_handlers_skel(self): + buff = [] + buff.append("static void handle_example_event(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0]) + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \ + % self.name + + def fill_tracepoint_detach_helper(self): + return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \ + % self.name + + def fill_atoms_init(self): + buff = [] + for a in self.atoms: + buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a) + return '\n'.join(buff) + + def fill_model_h(self): + buf = [ + "/* 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 " + self.name, + "" + ] + + buf.extend(self._fill_atoms()) + buf.append('') + + buf.extend(self._fill_atoms_to_string()) + buf.append('') + + buf.extend(self._fill_states()) + buf.append('') + + buf.extend(self._fill_start()) + buf.append('') + + buf.extend(self._fill_transitions()) + buf.append('') + + return '\n'.join(buf) + + def fill_monitor_class_type(self): + return "LTL_MON_EVENTS_ID" + + def fill_monitor_class(self): + return "ltl_monitor_id" + + def fill_main_c(self): + main_c = super().fill_main_c() + main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + + return main_c diff --git a/tools/verification/rvgen/rvgen/templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig new file mode 100644 index 000000000000..291b29ea28db --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_%%MODEL_NAME_UP%% + depends on RV +%%MONITOR_DEPS%% + select %%MONITOR_CLASS_TYPE%% + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% diff --git a/tools/verification/rvgen/rvgen/templates/container/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig new file mode 100644 index 000000000000..a606111949c2 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig @@ -0,0 +1,5 @@ +config RV_MON_%%MODEL_NAME_UP%% + depends on RV + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c new file mode 100644 index 000000000000..7d9b2f95c7e9 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -0,0 +1,37 @@ +// 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 "%%MODEL_NAME%%" + +#include "%%MODEL_NAME%%.h" + +struct rv_monitor rv_%%MODEL_NAME%%; + +struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = NULL, + .disable = NULL, + .reset = NULL, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/container/main.h b/tools/verification/rvgen/rvgen/templates/container/main.h new file mode 100644 index 000000000000..0f6883ab4bcc --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_%%MODEL_NAME%%; diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c new file mode 100644 index 000000000000..e0fd1134bd85 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -0,0 +1,90 @@ +// 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> +#include <rv/da_monitor.h> + +#define MODULE_NAME "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +%%INCLUDE_PARENT%% +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "%%MODEL_NAME%%.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +static struct rv_monitor rv_%%MODEL_NAME%%; +DECLARE_DA_MON_%%MONITOR_TYPE%%(%%MODEL_NAME%%, %%MIN_TYPE%%); + +/* + * 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. + * + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval = da_monitor_init_%%MODEL_NAME%%(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ + rv_%%MODEL_NAME%%.enabled = 0; + +%%TRACEPOINT_DETACH%% + + da_monitor_destroy_%%MODEL_NAME%%(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, + .reset = da_monitor_reset_all_%%MODEL_NAME%%, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h new file mode 100644 index 000000000000..87d3a1308926 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h @@ -0,0 +1,13 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_EVENT%%); + +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_ERROR%%); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c new file mode 100644 index 000000000000..f85d076fbf78 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -0,0 +1,102 @@ +// 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 "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +%%INCLUDE_PARENT%% + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "%%MODEL_NAME%%.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. + */ +%%ATOMS_INIT%% +} + +/* + * 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. + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ +%%TRACEPOINT_DETACH%% + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR(/* TODO */); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h new file mode 100644 index 000000000000..49394c4b0f1c --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ |