diff options
| author | Zeng Chi <zengchi@kylinos.cn> | 2026-09-21 18:24:42 +0800 |
|---|---|---|
| committer | Sean Christopherson <seanjc@google.com> | 2026-09-22 08:36:16 -0700 |
| commit | 119e9db233ad0f4cbd4cfb9f9385a7bca378b37d (patch) | |
| tree | 660d50d4139cb750fbde1ae3432452c20726c99d /tools/verification | |
| download | linux-stable-119e9db233ad0f4cbd4cfb9f9385a7bca378b37d.tar.gz linux-stable-119e9db233ad0f4cbd4cfb9f9385a7bca378b37d.zip | |
KVM: Don't pre-reserve xarray entries when storing empty/NULL attributesgrafted
Skip the xarray reservation loop when clearing all memory attributes, as
storing NULL only erases the entry and never needs to allocate, so no
reservation (and no cleanup of a failed one) is required in that case.
Suggested-by: Sean Christopherson <seanjc@google.com>
Cc: David Ballesteros <davimaba.v@proton.me>
Signed-off-by: Zeng Chi <zengchi@kylinos.cn>
Link: https://patch.msgid.link/20260921102442.1232375-1-zeng_chi911@163.com
[sean: split to separate patch]
Signed-off-by: Sean Christopherson <seanjc@google.com>
Diffstat (limited to 'tools/verification')
125 files changed, 8578 insertions, 0 deletions
diff --git a/tools/verification/models/deadline/nomiss.dot b/tools/verification/models/deadline/nomiss.dot new file mode 100644 index 000000000..fd1ea6bf2 --- /dev/null +++ b/tools/verification/models/deadline/nomiss.dot @@ -0,0 +1,41 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "idle"}; + {node [shape = plaintext, style=invis, label=""] "__init_ready"}; + {node [shape = doublecircle] "ready"}; + {node [shape = circle] "ready"}; + {node [shape = circle] "running"}; + {node [shape = circle] "sleeping"}; + {node [shape = circle] "throttled"}; + "__init_ready" -> "ready"; + "idle" [label = "idle"]; + "idle" -> "idle" [ label = "dl_server_idle" ]; + "idle" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "idle" -> "running" [ label = "sched_switch_in" ]; + "idle" -> "sleeping" [ label = "dl_server_stop" ]; + "idle" -> "throttled" [ label = "dl_throttle" ]; + "ready" [label = "ready\nclk < DEADLINE_NS()", color = green3]; + "ready" -> "idle" [ label = "dl_server_idle" ]; + "ready" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "ready" -> "running" [ label = "sched_switch_in" ]; + "ready" -> "sleeping" [ label = "dl_server_stop" ]; + "ready" -> "throttled" [ label = "dl_throttle;is_defer == 1" ]; + "running" [label = "running\nclk < DEADLINE_NS()"]; + "running" -> "idle" [ label = "dl_server_idle" ]; + "running" -> "running" [ label = "dl_replenish;reset(clk)\nsched_switch_in\nsched_wakeup" ]; + "running" -> "sleeping" [ label = "sched_switch_suspend\ndl_server_stop" ]; + "running" -> "throttled" [ label = "dl_throttle" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "sleeping" -> "running" [ label = "sched_switch_in" ]; + "sleeping" -> "sleeping" [ label = "dl_server_stop\ndl_server_idle" ]; + "sleeping" -> "throttled" [ label = "dl_throttle;is_constr_dl == 1 || is_defer == 1" ]; + "throttled" [label = "throttled"]; + "throttled" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "throttled" -> "throttled" [ label = "sched_switch_suspend\nsched_wakeup\ndl_server_idle\ndl_throttle" ]; + { rank = min ; + "__init_ready"; + "ready"; + } +} diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000..d7ce62102 --- /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 000000000..4d78fdd20 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,20 @@ +RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON + and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE) + +RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + or EPOLL_WAIT + +RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and not NANOSLEEP_CLOCK_REALTIME + +RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl new file mode 100644 index 000000000..a5d63ca08 --- /dev/null +++ b/tools/verification/models/rtapp/wakeup.ltl @@ -0,0 +1,5 @@ +RULE = always (((RT and USER_THREAD) imply + (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST)) + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI diff --git a/tools/verification/models/sched/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000..77bb64669 --- /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 000000000..511051fce --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,13 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_any"}; + {node [shape = doublecircle] "any"}; + "__init_any" -> "any"; + "any" [label = "any", color = green3]; + "any" -> "any" [ label = "sched_need_resched;irq_off == 1\nsched_waking;irq_off == 1 && preempt_off == 1" ]; + { rank = min ; + "__init_any"; + "any"; + } +} diff --git a/tools/verification/models/sched/sco.dot b/tools/verification/models/sched/sco.dot new file mode 100644 index 000000000..20b0e3b44 --- /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 000000000..340413896 --- /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 000000000..fe1300e93 --- /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 000000000..8b71c32d4 --- /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 000000000..4994c3e87 --- /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 000000000..8f5f38be0 --- /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/stall.dot b/tools/verification/models/stall.dot new file mode 100644 index 000000000..50077d1df --- /dev/null +++ b/tools/verification/models/stall.dot @@ -0,0 +1,22 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "enqueued"}; + {node [shape = plaintext, style=invis, label=""] "__init_dequeued"}; + {node [shape = doublecircle] "dequeued"}; + {node [shape = circle] "running"}; + "__init_dequeued" -> "dequeued"; + "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; + "running" [label = "running"]; + "dequeued" [label = "dequeued", color = green3]; + "running" -> "running" [ label = "sched_switch_in\nsched_wakeup" ]; + "enqueued" -> "enqueued" [ label = "sched_wakeup" ]; + "enqueued" -> "running" [ label = "sched_switch_in" ]; + "running" -> "dequeued" [ label = "sched_switch_wait" ]; + "dequeued" -> "enqueued" [ label = "sched_wakeup;reset(clk)" ]; + "running" -> "enqueued" [ label = "sched_switch_preempt;reset(clk)" ]; + { rank = min ; + "__init_dequeued"; + "dequeued"; + } +} diff --git a/tools/verification/models/wip.dot b/tools/verification/models/wip.dot new file mode 100644 index 000000000..2a53a9700 --- /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 000000000..1b206e831 --- /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 000000000..34a486585 --- /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 000000000..a44c22349 --- /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 000000000..8ae5fc0d1 --- /dev/null +++ b/tools/verification/rv/Makefile @@ -0,0 +1,84 @@ +# 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 + +check: $(RV) + RV=$(RV) prove -o --directives -f tests/ + +.PHONY: FORCE clean check diff --git a/tools/verification/rv/Makefile.config b/tools/verification/rv/Makefile.config new file mode 100644 index 000000000..066302230 --- /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 000000000..2497fb96c --- /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 000000000..e96be0dff --- /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 000000000..f3bfd3b98 --- /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 000000000..6f668eb26 --- /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 000000000..8d89e8c30 --- /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 000000000..f24ae8282 --- /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 000000000..d781983c1 --- /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 000000000..e6dea4040 --- /dev/null +++ b/tools/verification/rv/src/in_kernel.c @@ -0,0 +1,853 @@ +// 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, *cursor, *line; + int len = strlen(monitor_name); + int found = 0; + + available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); + if (!available_monitors) + return -1; + + config_is_container = 0; + cursor = available_monitors; + while ((line = strsep(&cursor, "\n"))) { + char *colon = strchr(line, ':'); + + if (strcmp(line, monitor_name) && (!colon || strcmp(colon + 1, monitor_name))) + continue; + + strncpy(out_name, line, 2 * MAX_DA_NAME_LEN); + out_name[2 * MAX_DA_NAME_LEN - 1] = '\0'; + + if (colon) { + out_name[colon - line] = '/'; + } else { + /* If there are children, they are on the next line. */ + line = strsep(&cursor, "\n"); + if (line && !strncmp(line, monitor_name, len) && line[len] == ':') + config_is_container = 1; + } + + found = 1; + break; + } + + free(available_monitors); + return found; +} + +/* + * 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) { + int len = strlen(container); + + if (strncmp(name, container, len) || name[len] != ':') + 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, sizeof(ikm->name) - 1); + ikm->name[sizeof(ikm->name) - 1] = '\0'; + ikm->enabled = enabled; + strncpy(ikm->desc, desc, sizeof(ikm->desc) - 1); + ikm->desc[sizeof(ikm->desc) - 1] = '\0'; + 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) + goto out_free_instance; + } + + 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 000000000..09e0d8598 --- /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 = EXIT_SUCCESS; + char *container = NULL; + + if (argc == 2) { + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { + print_help = 1; + retval = EXIT_SUCCESS; + } else if (argv[1][0] == '-') { + /* assume invalid option */ + print_help = 1; + retval = EXIT_FAILURE; + } else + container = argv[1]; + } else if (argc > 2) { + /* more than 2 is always usage */ + print_help = 1; + retval = EXIT_FAILURE; + } + 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(EXIT_SUCCESS); +} + +/* + * 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(EXIT_FAILURE); + } 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(EXIT_SUCCESS); + } + + 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 > 0 ? EXIT_SUCCESS : EXIT_FAILURE); +} + +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(EXIT_FAILURE, "%s needs root permission", argv[0]); + + if (argc <= 1) + usage(EXIT_FAILURE, "%s requires a command", argv[0]); + + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) + usage(EXIT_SUCCESS, "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(EXIT_FAILURE, "%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 000000000..1b9f9bfa1 --- /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 000000000..5677b439d --- /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/rv/tests/rv_list.t b/tools/verification/rv/tests/rv_list.t new file mode 100644 index 000000000..201af33a5 --- /dev/null +++ b/tools/verification/rv/tests/rv_list.t @@ -0,0 +1,48 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +RVDIR=/sys/kernel/tracing/rv/ + +# Help and basic tests +check "verify help page" \ + "$RV --help" 0 "usage: rv command" + +check "verify list subcommand help" \ + "$RV list --help" 0 "list all available monitors" + +all_nested=$(grep : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +all_non_nested=$(grep -v : $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +sched_monitors=$(grep sched: $RVDIR/available_monitors | cut -d: -f2 | paste -s | sed 's/\t/\\|/g') +description_state="[[:space:]]\+[[:print:]]\+\[\(OFF\|ON\)\]" +line_nested=" - \($all_nested\)${description_state}" +line_non_nested="\($all_non_nested\)${description_state}" + +# List monitors and containers +check "list all monitors" \ + "$RV list" 0 "" "" "^\($line_nested\|$line_non_nested\)$" + +check_if_exists "list container" \ + "$RV list sched" "$RVDIR/monitors/sched" \ + "" "-- No monitor found in container sched --" \ + "^\($sched_monitors\)${description_state}$" + +check_if_exists "list non-container" \ + "$RV list wwnr" "$RVDIR/monitors/wwnr" \ + "-- No monitor found in container wwnr --" \ + "^\( - \)\?[[:alnum:]]\+${description_state}$" + +check "list incomplete container name" \ + "$RV list s" 0 "-- No monitor found in container s --" + +# Error handling tests +check "no command" \ + "$RV" 1 "rv requires a command" + +check "invalid command" \ + "$RV invalid" 1 "rv does not know the invalid command" + +test_end diff --git a/tools/verification/rv/tests/rv_mon.t b/tools/verification/rv/tests/rv_mon.t new file mode 100644 index 000000000..cbc346c74 --- /dev/null +++ b/tools/verification/rv/tests/rv_mon.t @@ -0,0 +1,95 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +RVDIR=/sys/kernel/tracing/rv/ + +# Help and basic tests +check "verify mon subcommand help" \ + "$RV mon --help" 0 "run a monitor" + +# Error handling tests +check "mon without monitor name" \ + "$RV mon" 1 "usage: rv mon" + +check "invalid monitor name" \ + "$RV mon invalid" 1 "monitor invalid does not exist" + +if [ -d $RVDIR/monitors/wwnr ]; then + +check "invalid reactor name" \ + "$RV mon wwnr -r invalid" 1 "failed to set invalid reactor, is it available?" + +check "monitor name is substring of another monitor" \ + "$RV mon nr" 1 "monitor nr does not exist" + +check "already enabled monitor returns error" \ + "echo 1 > $RVDIR/monitors/wwnr/enable; $RV mon wwnr" 1 \ + "monitor wwnr (in-kernel) is already enabled" +echo 0 > $RVDIR/monitors/wwnr/enable + +fi + +# rv mon runs until terminated +set_expected_timeout 2s + +# Run monitors with different configurations +check_if_exists "run the monitor without parameters" \ + "$RV mon wwnr" "$RVDIR/monitors/wwnr" "" "." + +check_if_exists "run the monitor as verbose" \ + "$RV mon wwnr -v" "$RVDIR/monitors/wwnr" \ + "my pid is \$pid" "\(event\|error\)" + +check_if_exists "run the monitor with a reactor" \ + "$RV mon wwnr -r printk & sleep .5 && cat $RVDIR/monitors/wwnr/reactors && wait" \ + "$RVDIR/monitors/wwnr/reactors" "\[printk\]" + +check_if_exists "reactor is restored after exit" \ + "cat $RVDIR/monitors/wwnr/reactors" \ + "$RVDIR/monitors/wwnr/reactors" "\[nop\]" + +check_if_exists "run a nested monitor with a reactor" \ + "$RV mon snroc -r printk & sleep .5 && cat $RVDIR/monitors/sched/snroc/reactors && wait" \ + "$RVDIR/monitors/sched/snroc/reactors" "\[printk\]" + +check_if_exists "run an explicitly nested monitor with a reactor" \ + "$RV mon sched:sssw -r printk & sleep .5 && cat $RVDIR/monitors/sched/sssw/reactors && wait" \ + "$RVDIR/monitors/sched/sssw/reactors" "\[printk\]" + +check_if_exists "run container monitor" \ + "$RV mon sched & sleep .5 && cat $RVDIR/monitors/sched/{sssw,sco}/enable && wait" \ + "$RVDIR/monitors/sched" "1" "0" "^1$" + +# Regexes for the trace +header="^[[:space:]]\+\(\([][A-Z_x<>-]\+\||\)[[:space:]]*\)\+$" +type="\(event\|error\)[[:space:]]\+" +genpid="[0-9]\+[[:space:]]\+" +selfpid="\$pid[[:space:]]\+" +cpu="\[[0-9]\{3\}\][[:space:]]\+" +state="[a-z_]\+ " +trace_task="${genpid}${cpu}${type}${genpid}${state}" +trace_task_self="${genpid}${cpu}${type}${selfpid}${state}" +trace_cpu="${genpid}${cpu}${type}${state}" +trace_cpu_self="${selfpid}${cpu}${type}${state}" + +check_if_exists "run per-task monitor with tracing" \ + "$RV mon sssw -t" "$RVDIR/monitors/sched/sssw" \ + "$header" "$trace_task_self" "\($header\|$trace_task\)" + +check_if_exists "run per-task monitor tracing also self" \ + "$RV mon sched:sssw -t -s" "$RVDIR/monitors/sched/sssw" \ + "$trace_task_self" "" "\($header\|$trace_task\)" + +check_if_exists "run per-cpu monitor with tracing" \ + "$RV mon sched:sco -t" "$RVDIR/monitors/sched/sco" \ + "$header" "$trace_cpu_self" "\($header\|$trace_cpu\)" + +check_if_exists "run per-cpu monitor tracing also self" \ + "$RV mon sco -t -s" "$RVDIR/monitors/sched/sco" \ + "$trace_cpu_self" "" "\($header\|$trace_cpu\)" + +test_end diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore new file mode 100644 index 000000000..1e288a076 --- /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 000000000..48d0376a5 --- /dev/null +++ b/tools/verification/rvgen/Makefile @@ -0,0 +1,32 @@ +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: check +check: + prove -o --directives -f tests/ + +.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/kunit.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/kunit.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 000000000..246b43fa2 --- /dev/null +++ b/tools/verification/rvgen/__main__.py @@ -0,0 +1,86 @@ +#!/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/monitor_synthesis.rst + +if __name__ == '__main__': + from rvgen.dot2k import da2k, ha2k + from rvgen.generator import Monitor + from rvgen.container import Container + from rvgen.ltl2k import ltl2k + from rvgen.kunit import KUnit, KUnitError + from rvgen.automata import AutomataError + from rvgen.ltl2ba import LTLError + import argparse + import sys + + parser = argparse.ArgumentParser(description='Generate kernel rv monitor') + + parent_parser = argparse.ArgumentParser(add_help=False) + parent_parser.add_argument("-D", "--description", dest="description", required=False) + parent_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", parents=[parent_parser]) + 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", required=True, + help="Monitor class, either \"da\", \"ha\" or \"ltl\"") + monitor_parser.add_argument('-s', "--spec", dest="spec", required=True, + help="Monitor specification file") + monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True, + help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") + + container_parser = subparsers.add_parser("container", parents=[parent_parser]) + container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + + kunit_parser = subparsers.add_parser("kunit", parents=[parent_parser]) + kunit_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + kunit_parser.add_argument('-l', "--local", dest="local", action="store_true", required=False, + help="Force looking for the monitor in the current directory only") + + params = parser.parse_args() + + try: + if params.subcmd == "monitor": + print(f"Opening and parsing the specification file {params.spec}") + if params.monitor_class == "da": + monitor = da2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ha": + monitor = ha2k(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) + elif params.subcmd == "container": + monitor = Container(vars(params)) + elif params.subcmd == "kunit": + monitor = KUnit(vars(params)) + monitor.print_files() + sys.exit(0) + except (AutomataError, LTLError) as e: + print(f"There was an error processing {params.spec}:\n{e}", file=sys.stderr) + sys.exit(1) + except KUnitError as e: + print(f"There was an error generating KUnit files:\n{e}", file=sys.stderr) + sys.exit(1) + + print(f"Writing the monitor into the directory {monitor.name}") + monitor.print_files() + print("Almost done, checklist") + if params.subcmd == "monitor": + print(f" - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation") + 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 000000000..1012becc7 --- /dev/null +++ b/tools/verification/rvgen/dot2c @@ -0,0 +1,25 @@ +#!/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 + + 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 000000000..fd37ce304 --- /dev/null +++ b/tools/verification/rvgen/rvgen/automata.py @@ -0,0 +1,549 @@ +#!/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 class: parse an automaton in dot file digraph format into a python object +# +# For further information, see: +# Documentation/trace/rv/deterministic_automata.rst + +import ntpath + +import lark + +class ParseTree: + # based on https://graphviz.org/doc/info/lang.html + # with the irrelevant stuffs (port and compass) removed + grammar = r''' + start: "strict"? ("graph" | "digraph") ID? "{" stmt_list "}" + + stmt_list: (stmt ";"? stmt_list)? + + stmt: node_stmt + | edge_stmt + | attr_stmt + | ID "=" ID + | subgraph + + attr_stmt: attr_type attr_list + + attr_type: "graph" -> graph + | "node" -> node + | "edge" -> edge + + attr_list: "[" a_list? "]" attr_list? + + a_list: ID "=" ID (";" | ",")? a_list? + + edge_stmt: (node_id | subgraph) edgerhs attr_list? + + edgerhs: edgeop (node_id | subgraph) edgerhs? + + edgeop: "->" | "--" + + node_stmt: node_id attr_list? + + node_id: ID + + subgraph: ("subgraph" ID?)? "{" stmt_list "}" + + ID: CNAME + | /-?(\.[0-9]+|[0-9]+(\.[0-9]*))/ + | ESCAPED_STRING + + %import common.CNAME + %import common.ESCAPED_STRING + %import common.WS + %ignore WS + ''' + + @staticmethod + def parse_edge(tree: lark.Tree) -> tuple[str, str]: + # only support a simple node-to-node edge + nodes = [] + for node in tree.iter_subtrees_topdown(): + if node.data == "node_id": + nodes.append(node.children[0].strip('"')) + + if len(nodes) != 2: + raise AutomataError("Only state-to-state transition is supported") + + return tuple(nodes) + + class ParseNodes(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.nodes = set() + super().__init__(*args, **kwargs) + + def node_stmt(self, tree): + node_id = tree.children[0] + node = node_id.children[0].strip('"') + self.nodes.add(node) + + class ParseEdges(lark.visitors.Visitor): + def __init__(self, *args, **kwargs): + self.edges = set() + super().__init__(*args, **kwargs) + + def edge_stmt(self, tree): + edge = ParseTree.parse_edge(tree) + self.edges.add(edge) + + class ParseAttributes(lark.visitors.Interpreter): + def __init__(self, *args, **kwargs): + ''' + Stacks of default attributes. [0] is the default + attributes for the outermost scope, while [-1] is the + default attributes for the current scope. + ''' + self.default_node_attrs = [{}] + self.default_edge_attrs = [{}] + + self.node_attrs = {} + self.edge_attrs = {} + + super().__init__(*args, **kwargs) + + @staticmethod + def __get_attrs(stmt: lark.Tree) -> dict[str, str]: + attrs = {} + + for node in stmt.iter_subtrees(): + if node.data == "a_list": + attrs[node.children[0]] = node.children[1].strip('"') + + return attrs + + + def subgraph(self, tree): + # We are entering a new scope, inherit the default + # attributes of the outer scope + self.default_node_attrs.append(self.default_node_attrs[-1].copy()) + self.default_edge_attrs.append(self.default_edge_attrs[-1].copy()) + + children = self.visit_children(tree) + + # Exiting the scope + del self.default_node_attrs[-1] + del self.default_edge_attrs[-1] + + return children + + def node_stmt(self, tree): + node_id = tree.children[0] + node = node_id.children[0].strip('"') + + attrs = self.default_node_attrs[-1].copy() + attrs |= self.__get_attrs(tree) + + if attrs: + if node in self.node_attrs: + self.node_attrs[node] = attrs | self.node_attrs[node] + else: + self.node_attrs[node] = attrs + + return self.visit_children(tree) + + def edge_stmt(self, tree): + edge = ParseTree.parse_edge(tree) + + attrs = self.default_edge_attrs[-1].copy() + attrs |= self.__get_attrs(tree) + + if attrs: + if edge in self.edge_attrs: + self.edge_attrs[edge] = attrs | self.edge_attrs[edge] + else: + self.edge_attrs[edge] = attrs + + return self.visit_children(tree) + + def attr_stmt(self, tree): + attr_type = tree.children[0].data + attrs = self.__get_attrs(tree) + + if attr_type == "node": + self.default_node_attrs[-1] |= attrs + elif attr_type == "edge": + self.default_edge_attrs[-1] |= attrs + else: + # graph attributes are irrelevant + pass + + self.visit_children(tree) + + def __init__(self, dot_file): + parser = lark.Lark(self.grammar, parser='lalr') + node_parser = self.ParseNodes() + edge_parser = self.ParseEdges() + attributes_parser = self.ParseAttributes() + + try: + with open(dot_file, "r") as f: + tree = parser.parse(f.read()) + attributes_parser.visit(tree) + node_parser.visit(tree) + edge_parser.visit(tree) + except OSError as exc: + raise AutomataError(exc.strerror) from exc + except lark.exceptions.UnexpectedInput as exc: + raise AutomataError(str(exc)) + + self.nodes = node_parser.nodes + self.edges = edge_parser.edges + self.node_attrs = attributes_parser.node_attrs + self.edge_attrs = attributes_parser.edge_attrs + +class ConstraintCondition: + def __init__(self, env: str, op: str, val: str, unit=None): + self.env = env + self.op = op + self.val = val + self.unit = unit + if unit is None: + # try to infer unit from constants or parameters + val_for_unit = val.lower().replace("()", "") + if val_for_unit.endswith("_ns"): + self.unit = "ns" + if val_for_unit.endswith("_jiffies"): + self.unit = "j" + +class ConstraintRule: + grammar = r''' + rule: condition (OP condition)* + + OP: "&&" | "||" + + condition: ENV CMP_OP VAL UNIT? + + ENV: CNAME + + CMP_OP: "==" | "!=" | "<=" | "<" | ">=" | ">" + + VAL: /[0-9]+/ + | /[A-Z_]+\(\)/ + | /[A-Z_]+/ + | /[a-z_]+\(\)/ + | /[a-z_]+/ + + UNIT: "ns" | "us" | "ms" | "s" | "j" + ''' + + def __init__(self, c: ConstraintCondition): + ''' + A list of pairs of + - the condition (e.g. is_constr_dl == 1) + - the logical operator ("||" or "&&") combining this + condition with the next one if it exists, otherwise None + + TODO: Perhaps use an abstract syntax tree instead, because + this representation cannot capture precedence + ''' + self.rules = [[c, None]] + + def chain(self, op: str, c: ConstraintCondition): + self.rules[-1][1] = op + self.rules.append([c, None]) + +class ConstraintReset: + def __init__(self, env): + self.env = env + +class StateLabelParser: + grammar = r''' + label: CNAME ("\\n" condition)? + + %import common.CNAME + %import common.WS + %ignore WS + ''' + ConstraintRule.grammar + + parser = lark.Lark(grammar, parser='lalr', start="label") + + def __init__(self, label: str): + try: + tree = self.parser.parse(label) + except lark.exceptions.UnexpectedInput as exc: + raise(AutomataError(f"Unrecognised state \"{label}\"\n{exc}")) + + self.state = tree.children[0] + self.constraint = None + + if len(tree.children) == 2: + self.constraint = ConstraintCondition(*tree.children[1].children) + if self.constraint.op not in ("<", "<="): + raise AutomataError("State constraints must be clock expirations like" + f" clk<N ({label})") + +class EventLabelParser: + grammar = r''' + events: event ("\\n" event)* + + event: name (";" guard)? + + guard: reset + | rule + | rule ";" reset + | reset ";" rule + + name: CNAME + + reset: "reset" "(" ENV ")" + + %import common.CNAME + %import common.WS + %ignore WS + ''' + ConstraintRule.grammar + + parser = lark.Lark(grammar, parser='lalr', start="events") + + class GetEvents(lark.visitors.Transformer): + def guard(self, args): + reset = None + rule = None + for arg in args: + if arg.data == "reset": + reset = ConstraintReset(arg.children[0]) + elif arg.data == "rule": + conditions = arg.children + rule = ConstraintRule(conditions[0]) + for i in range(1, len(conditions), 2): + rule.chain(conditions[i], conditions[i + 1]) + return reset, rule + + def OP(self, args): + return args + + def condition(self, args): + return ConstraintCondition(*args) + + def event(self, args): + assert(len(args) <= 2) + name = args[0] + rule, reset = None, None + if len(args) == 2: + reset, rule = args[1] + return name, reset, rule + + def events(self, args): + return args + + def name(self, args): + return args[0] + + def __init__(self, label: str): + try: + tree = self.parser.parse(label) + self.events = self.GetEvents().transform(tree) + except lark.exceptions.UnexpectedInput as exc: + raise(AutomataError(f"Unrecognised event \"{label}\"\n{exc}")) + +class Transition: + def __init__(self, src: str, dst: str, event: str, + reset: ConstraintReset, rule: ConstraintRule): + self.src = src + self.dst = dst + self.event = event + self.rule = rule + self.reset = reset + +class State: + def __init__(self, name: str, inv: ConstraintCondition): + self.name = name + self.inv = inv + +class AutomataError(Exception): + """Exception raised for errors in automata parsing and validation. + + Raised when DOT file processing fails due to invalid format, I/O errors, + or malformed automaton definitions. + """ + +class Automata: + """Automata class: Reads a dot file and parses it as an automaton. + + It supports both deterministic and hybrid automata. + + Attributes: + dot_file: A dot file with an state_automaton definition. + """ + + invalid_state_str = "INVALID_STATE" + init_marker = "__init_" + + def __init__(self, file_path, model_name=None): + self.__dot_path = file_path + self.name = model_name or self.__get_model_name() + self.__parse_tree = ParseTree(file_path) + self.transitions = self.__parse_transitions() + self.states, self.initial_state, self.final_states = self.__parse_states() + self.env_types = {} + self.env_stored = set() + self.constraint_vars = set() + self.self_loop_reset_events = set() + self.events, self.envs = self.__get_event_variables() + self.function = self.__create_matrix() + self.events_start, self.events_start_run = self.__store_init_events() + self.env_stored = sorted(self.env_stored) + self.constraint_vars = sorted(self.constraint_vars) + self.self_loop_reset_events = sorted(self.self_loop_reset_events) + + def __get_model_name(self) -> str: + basename = ntpath.basename(self.__dot_path) + if not basename.endswith(".dot") and not basename.endswith(".gv"): + print("not a dot file") + raise AutomataError(f"not a dot file: {self.__dot_path}") + + model_name = ntpath.splitext(basename)[0] + if not model_name: + raise AutomataError(f"not a dot file: {self.__dot_path}") + + return model_name + + def __parse_transitions(self): + transitions = [] + + for edge in self.__parse_tree.edges: + attr = self.__parse_tree.edge_attrs.get(edge) + if not attr: + continue + + label = attr.get("label") + + src, dst = edge + + parser = EventLabelParser(label) + for event, reset, rule in parser.events: + transitions.append(Transition(src, dst, event, reset, rule)) + + transitions.sort(key=lambda t : (t.src, t.event)) + return transitions + + def __parse_states(self): + initial_state = "" + states = [] + final_states = [] + + for node in self.__parse_tree.nodes: + attr = self.__parse_tree.node_attrs[node] + label = attr.get("label") + + if node.startswith(Automata.init_marker): + initial_state = node[len(Automata.init_marker):] + + if not label: + continue + + parser = StateLabelParser(label) + state = State(parser.state, parser.constraint) + + states.append(state) + + shape = attr.get("shape") + if shape in ("doublecircle", "ellipse"): + final_states.append(state) + + + initial_state = next((s for s in states if s.name == initial_state), None) + if not initial_state: + raise AutomataError("The automaton doesn't have an initial state") + + if not final_states: + final_states.append(initial_state) + + states.remove(initial_state) + states.sort(key=lambda s : s.name) + states.insert(0, initial_state) + return states, initial_state, final_states + + def __get_event_variables(self) -> tuple[list[str], list[str]]: + events: list[str] = [] + envs: list[str] = [] + + for transition in self.transitions: + events.append(transition.event) + + if transition.reset: + envs.append(transition.reset.env) + self.env_stored.add(transition.reset.env) + if transition.rule: + for c, _ in transition.rule.rules: + envs.append(c.env) + self.__extract_env_var(c) + + for state in self.states: + if state.inv: + envs.append(state.inv.env) + self.__extract_env_var(state.inv) + + return sorted(set(events)), sorted(set(envs)) + + def __extract_env_var(self, constraint: ConstraintCondition): + if constraint.unit: + self.env_types[constraint.env] = constraint.unit + if constraint.val[0].isalpha(): + self.constraint_vars.add(constraint.val) + + def __create_matrix(self) -> list[list[str]]: + # transform the array into a dictionary + events = self.events + states = [s.name for s in 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 _ in range(nr_event)] for _ in range(nr_state)] + + for transition in self.transitions: + src, dst = transition.src, transition.dst + event = transition.event + if src == dst and transition.reset: + # those events reset also on self loops + self.self_loop_reset_events.add(event) + matrix[states_dict[src]][events_dict[event]] = dst + + return matrix + + def __store_init_events(self) -> tuple[list[bool], list[bool]]: + events_start = [False] * len(self.events) + events_start_run = [False] * len(self.events) + for i in range(len(self.events)): + curr_event_will_init = 0 + curr_event_from_init = False + curr_event_used = 0 + for j in range(len(self.states)): + if self.function[j][i] != self.invalid_state_str: + curr_event_used += 1 + if self.function[j][i] == self.initial_state.name: + 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: str) -> bool: + return self.events_start[self.events.index(event)] + + def is_start_run_event(self, event: str) -> bool: + # prefer handle_start_event if there + if any(self.events_start): + return False + return self.events_start_run[self.events.index(event)] + + def is_hybrid_automata(self) -> bool: + return bool(self.envs) diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py new file mode 100644 index 000000000..51f188530 --- /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 000000000..22938ce1b --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -0,0 +1,268 @@ +#!/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 automaton 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, AutomataError + +class Dot2c(Automata): + enum_suffix = "" + enum_states_def = "states" + enum_events_def = "events" + enum_envs_def = "envs" + 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 __get_enum_states_content(self) -> list[str]: + buff = [] + buff.append(f"\t{self.initial_state.name}{self.enum_suffix},") + for state in self.states: + if state != self.initial_state: + buff.append(f"\t{state.name}{self.enum_suffix},") + buff.append(f"\tstate_max{self.enum_suffix},") + + return buff + + def format_states_enum(self) -> list[str]: + buff = [] + buff.append(f"enum {self.enum_states_def} {{") + buff += self.__get_enum_states_content() + buff.append("};\n") + + return buff + + def __get_enum_events_content(self) -> list[str]: + buff = [] + for event in self.events: + buff.append(f"\t{event}{self.enum_suffix},") + + buff.append(f"\tevent_max{self.enum_suffix},") + + return buff + + def format_events_enum(self) -> list[str]: + buff = [] + buff.append(f"enum {self.enum_events_def} {{") + buff += self.__get_enum_events_content() + buff.append("};\n") + + return buff + + def __get_non_stored_envs(self) -> list[str]: + return [e for e in self.envs if e not in self.env_stored] + + def __get_enum_envs_content(self) -> list[str]: + buff = [] + # We first place env variables that have a u64 storage. + # Those are limited by MAX_HA_ENV_LEN, other variables + # are read only and don't require a storage. + unstored = self.__get_non_stored_envs() + for env in list(self.env_stored) + unstored: + buff.append(f"\t{env}{self.enum_suffix},") + + buff.append(f"\tenv_max{self.enum_suffix},") + max_stored = unstored[0] if len(unstored) else "env_max" + buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},") + + return buff + + def format_envs_enum(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + buff.append(f"enum {self.enum_envs_def} {{") + buff += self.__get_enum_envs_content() + buff.append("};\n") + buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN," + ' "Not enough slots");') + if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()): + buff.append("#define HA_CLK_NS") + buff.append("") + return buff + + def get_minimun_type(self) -> str: + min_type = "unsigned char" + + if len(self.states) > 255: + min_type = "unsigned short" + + if len(self.states) > 65535: + min_type = "unsigned int" + + if len(self.states) > 1000000: + raise AutomataError(f"Too many states: {len(self.states)}") + + return min_type + + def format_automaton_definition(self) -> list[str]: + min_type = self.get_minimun_type() + buff = [] + buff.append(f"struct {self.struct_automaton_def} {{") + buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];") + buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];") + if self.is_hybrid_automata(): + buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];") + buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];") + buff.append(f"\t{min_type} initial_state;") + buff.append(f"\tbool final_states[state_max{self.enum_suffix}];") + buff.append("};\n") + return buff + + def format_aut_init_header(self) -> list[str]: + buff = [] + buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{") + return buff + + def __get_string_vector_per_line_content(self, entries: list[str]) -> str: + buff = [] + for entry in entries: + buff.append(f"\t\t\"{entry}\",") + return "\n".join(buff) + + def format_aut_init_events_string(self) -> list[str]: + buff = [] + buff.append("\t.event_names = {") + buff.append(self.__get_string_vector_per_line_content(self.events)) + buff.append("\t},") + return buff + + def format_aut_init_states_string(self) -> list[str]: + buff = [] + buff.append("\t.state_names = {") + buff.append(self.__get_string_vector_per_line_content([s.name for s in self.states])) + buff.append("\t},") + + return buff + + def format_aut_init_envs_string(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + buff.append("\t.env_names = {") + # maintain consistent order with the enum + ordered_envs = list(self.env_stored) + self.__get_non_stored_envs() + buff.append(self.__get_string_vector_per_line_content(ordered_envs)) + buff.append("\t},") + + return buff + + def __get_max_strlen_of_states(self) -> int: + max_state_name = max((len(s.name) for s in self.states)) + return max(max_state_name, len(self.invalid_state_str)) + + def get_aut_init_function(self) -> str: + nr_states = len(self.states) + nr_events = len(self.events) + 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 += f"\t\t\t{next_state}" + else: + line += f"{next_state:>{maxlen}}" + if y != nr_events - 1: + line += ",\n" if linetoolong else ", " + else: + line += ",\n\t\t}," if linetoolong else " }," + buff.append(line) + + return '\n'.join(buff) + + def format_aut_init_function(self) -> list[str]: + buff = [] + buff.append("\t.function = {") + buff.append(self.get_aut_init_function()) + buff.append("\t},") + + return buff + + def get_aut_init_initial_state(self) -> str: + return self.initial_state.name + + def format_aut_init_initial_state(self) -> list[str]: + 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) -> str: + line = "" + first = True + for state in self.states: + if not first: + line = line + ', ' + else: + first = False + + if state in self.final_states: + line = line + '1' + else: + line = line + '0' + return line + + def format_aut_init_final_states(self) -> list[str]: + buff = [] + buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},") + + return buff + + def __get_automaton_initialization_footer_string(self) -> str: + footer = "};\n" + return footer + + def format_aut_init_footer(self) -> list[str]: + buff = [] + buff.append(self.__get_automaton_initialization_footer_string()) + + return buff + + def format_invalid_state(self) -> list[str]: + buff = [] + buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n") + + return buff + + def format_model(self) -> list[str]: + buff = [] + buff += self.format_states_enum() + buff += self.format_invalid_state() + buff += self.format_events_enum() + buff += self.format_envs_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_envs_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('\n'.join(buff)) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py new file mode 100644 index 000000000..fd3254ea5 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -0,0 +1,512 @@ +#!/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/monitor_synthesis.rst + +from .dot2c import Dot2c +from .generator import Monitor +from .automata import ConstraintCondition, AutomataError + +class dot2k(Monitor, Dot2c): + template_dir = "dot2k" + + # only needed for the per-obj cleanup hook + cleanup_marker = "obj_cleanup" + + 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 = f"_{self.name}" + self.enum_suffix = f"_{self.name}" + self.monitor_class = extra_params["monitor_class"] + + def fill_monitor_type(self) -> str: + buff = [ self.monitor_type.upper() ] + buff += self._fill_timer_type() + if self.monitor_type == "per_obj": + buff.append("typedef /* XXX: define the target type */ *monitor_target;") + return "\n".join(buff) + + def fill_tracepoint_handlers_skel(self) -> str: + buff = [] + buff += self._fill_hybrid_definitions() + for event in self.events: + buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)") + 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(f"\tda_{handle}(p, {event}{self.enum_suffix});") + elif self.monitor_type == "per_obj": + buff.append("\tint id = /* XXX: how do I get the id? */;") + buff.append("\tmonitor_target t = /* XXX: how do I get t? */;") + buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});") + else: + buff.append(f"\tda_{handle}({event}{self.enum_suffix});") + buff.append("}") + buff.append("") + if self.monitor_type == "per_obj": + buff.append("/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */") + buff.append(f"static void handle_{self.cleanup_marker}(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tint id = /* XXX: how do I get the id? */;") + buff.append("\tda_destroy_storage(id);") + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self) -> str: + buff = [] + for event in self.events: + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") + return '\n'.join(buff) + + def fill_tracepoint_detach_helper(self) -> str: + buff = [] + for event in self.events: + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});") + if self.monitor_type == "per_obj": + buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: cleanup tracepoint */, handle_{self.cleanup_marker});") + return '\n'.join(buff) + + def fill_model_h_header(self) -> list[str]: + buff = [] + buff.append("/* SPDX-License-Identifier: GPL-2.0 */") + buff.append("/*") + buff.append(f" * Automatically generated C representation of {self.name} automaton") + buff.append(" * For further information about this format, see kernel documentation:") + buff.append(" * Documentation/trace/rv/deterministic_automata.rst") + buff.append(" */") + buff.append("") + buff.append(f"#define MONITOR_NAME {self.name}") + buff.append("") + + return buff + + def fill_model_h(self) -> str: + # + # Adjust the definition names + # + self.enum_states_def = f"states_{self.name}" + self.enum_events_def = f"events_{self.name}" + self.enum_envs_def = f"envs_{self.name}" + self.struct_automaton_def = f"automaton_{self.name}" + self.var_automaton_def = f"automaton_{self.name}" + + buff = self.fill_model_h_header() + buff += self.format_model() + + return '\n'.join(buff) + + def _is_id_monitor(self) -> bool: + return self.monitor_type in ("per_task", "per_obj") + + def fill_monitor_class_type(self) -> str: + if self._is_id_monitor(): + return "DA_MON_EVENTS_ID" + return "DA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self) -> str: + if self._is_id_monitor(): + return "da_monitor_id" + return "da_monitor" + + def fill_tracepoint_args_skel(self, tp_type: str) -> str: + buff = [] + tp_args_event = [ + ("char *", "state"), + ("char *", "event"), + ("char *", "next_state"), + ("bool ", "final_state"), + ] + tp_args_error = [ + ("char *", "state"), + ("char *", "event"), + ] + tp_args_error_env = tp_args_error + [("char *", "env")] + tp_args_dict = { + "event": tp_args_event, + "error": tp_args_error, + "error_env": tp_args_error_env + } + tp_args_id = ("int ", "id") + tp_args = tp_args_dict[tp_type] + if self._is_id_monitor(): + 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(f" TP_PROTO({tp_proto_c}),") + buff.append(f" TP_ARGS({tp_args_c})") + return '\n'.join(buff) + + def _fill_hybrid_definitions(self) -> list: + """Stub, not valid for deterministic automata""" + return [] + + def _fill_timer_type(self) -> list: + """Stub, not valid for deterministic automata""" + return [] + + def fill_main_c(self) -> str: + 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) + main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class) + + return main_c + +class da2k(dot2k): + """Deterministic automata only""" + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + if self.is_hybrid_automata(): + raise AutomataError("Detected hybrid automaton, use the 'ha' class") + +class ha2k(dot2k): + """Hybrid automata only""" + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + if not self.is_hybrid_automata(): + raise AutomataError("Detected deterministic automaton, use the 'da' class") + self.trace_h = self._read_template_file("trace_hybrid.h") + self.has_invariant = False + self.has_guard = False + for state in self.states: + if state.inv: + self.has_invariant = True + for transition in self.transitions: + if transition.rule or transition.reset: + self.has_guard = True + + def fill_monitor_class_type(self) -> str: + if self._is_id_monitor(): + return "HA_MON_EVENTS_ID" + return "HA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self) -> str: + """ + Used for tracepoint classes, since they are shared we keep da + instead of ha (also for the ha specific tracepoints). + The tracepoint class is not visible to the tools. + """ + return super().fill_monitor_class() + + def __adjust_value(self, value: str | int, unit: str | None) -> str: + """Adjust the value in ns""" + try: + value = int(value) + except ValueError: + # it's a constant, a parameter or a function + if value.endswith("()"): + return value.replace("()", "(ha_mon)") + return value + match unit: + case "us": + value *= 10**3 + case "ms": + value *= 10**6 + case "s": + value *= 10**9 + return str(value) + "ull" + + def __parse_guard_rule(self, rule) -> list[str]: + buff = [] + for c, sep in rule.rules: + env = c.env + self.enum_suffix + op = c.op + val = self.__adjust_value(c.val, c.unit) + + cond = f"ha_get_env(ha_mon, {env}, time_ns) {op} {val}" + if sep: + cond += f" {sep}" + buff.append(cond) + return buff + + def __start_to_invariant_check(self, inv: ConstraintCondition) -> str: + # by default assume the timer has ns expiration + clock_type = "ns" + if inv.unit == "j": + clock_type = "jiffy" + + value = self.__adjust_value(inv.val, inv.unit) + + return f"return ha_check_invariant_{clock_type}(ha_mon, {inv.env}_{self.name}, time_ns, {value})" + + def __parse_invariant(self, inv): + # by default assume the timer has ns expiration + clock_type = "ns" + if inv.unit == "j": + clock_type = "jiffy" + + env = inv.env + self.enum_suffix + try: + val = int(inv.val) + except ValueError: + # it's a constant, a parameter or a function + val = inv.val.replace("()", "(ha_mon)") + + match inv.unit: + case "us": + val *= 10**3 + case "ms": + val *= 10**6 + case "s": + val *= 10**9 + + return (f"ha_start_timer_{clock_type}(ha_mon, {env}," + f" {val}, time_ns)") + + def __format_guard_rules(self, rules: list[str]) -> list[str]: + """ + Merge guard constraints as a single C return statement. + If the rules include a stored env, also check its validity. + Break lines in a best effort way that tries to keep readability. + """ + if not rules: + return [] + + invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||" + for env in self.env_stored if any(env in rule for rule in rules)] + if invalid_checks and len(rules) > 1: + rules[0] = "(" + rules[0] + rules[-1] = rules[-1] + ")" + rules = invalid_checks + rules + + separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " " + return ["res = " + separator.join(rules) + ";"] + + def __fill_verify_invariants_func(self) -> list[str]: + if not self.has_invariant: + return [] + + buff = [ +f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, +\t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) +{{"""] + + _else = "" + for state in self.states: + if not state.inv: + continue + + check_str = self.__start_to_invariant_check(state.inv) + buff.append(f"\t{_else}if (curr_state == {state.name}{self.enum_suffix})") + buff.append(f"\t\t{check_str};") + _else = "else " + + buff.append("\treturn true;\n}\n") + return buff + + def __fill_verify_guards_func(self) -> list[str]: + buff = [] + + if not self.has_guard: + return [] + + buff.append( +f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{ +\tbool res = true; +""") + + _else = "" + for transition in self.transitions: + if not transition.rule and not transition.reset: + continue + + buff.append(f"\t{_else}if (curr_state == " + f"{transition.src}{self.enum_suffix} && " + f"event == {transition.event}{self.enum_suffix})") + rule = transition.rule + reset = transition.reset + if rule and reset: + buff[-1] += " {" + if rule: + buff.append("\t\t" + self.__format_guard_rules(self.__parse_guard_rule(rule))[0]) + if reset: + buff.append(f"\t\tha_reset_env(ha_mon, {reset.env}{self.enum_suffix}, time_ns);") + if rule and reset: + _else = "} else " + else: + _else = "else " + if _else[0] == "}": + buff.append("\t}") + buff.append("\treturn res;\n}\n") + return buff + + def __fill_setup_invariants_func(self) -> list[str]: + if not self.has_invariant: + return [] + + buff = [ +f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{"""] + + conditions = ["next_state == curr_state"] + conditions += [f"event != {e}{self.enum_suffix}" + for e in self.self_loop_reset_events] + condition_str = " && ".join(conditions) + buff.append(f"\tif ({condition_str})\n\t\treturn;") + + _else = "" + for state in self.states: + inv = state.inv + if not inv: + continue + inv = self.__parse_invariant(inv) + buff.append(f"\t{_else}if (next_state == {state.name}{self.enum_suffix})") + buff.append(f"\t\t{inv};") + _else = "else " + + for state in self.states: + inv = state.inv + if not inv: + continue + buff.append(f"\telse if (curr_state == {state.name}{self.enum_suffix})") + buff.append("\t\tha_cancel_timer(ha_mon);") + + buff.append("}\n") + return buff + + def __fill_constr_func(self) -> list[str]: + buff = [] + if not self.has_invariant and not self.has_guard: + return [] + + buff.append( +"""/* + * These functions are used to validate state transitions. + * + * They are generated by parsing the model, there is usually no need to change them. + * If the monitor requires a timer, there are functions responsible to arm it when + * the next state has a constraint, cancel it in any other case and to check + * that it didn't expire before the callback run. Transitions to the same state + * without a reset never affect timers. + */""") + + buff += self.__fill_verify_invariants_func() + buff += self.__fill_verify_guards_func() + buff += self.__fill_setup_invariants_func() + + buff.append( +f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, +\t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, +\t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) +{{""") + + if self.has_invariant: + buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, " + "event, next_state, time_ns))\n\t\treturn false;\n") + + if self.has_guard: + buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, " + "next_state, time_ns))\n\t\treturn false;\n") + + if self.has_invariant: + buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n") + + buff.append("\treturn true;\n}\n") + return buff + + def __fill_env_getter(self, env: str) -> str: + if env in self.env_types: + match self.env_types[env]: + case "ns" | "us" | "ms" | "s": + return "ha_get_clk_ns(ha_mon, env, time_ns);" + case "j": + return "ha_get_clk_jiffy(ha_mon, env);" + return f"/* XXX: how do I read {env}? */" + + def __fill_env_resetter(self, env: str) -> str: + if env in self.env_types: + match self.env_types[env]: + case "ns" | "us" | "ms" | "s": + return "ha_reset_clk_ns(ha_mon, env, time_ns);" + case "j": + return "ha_reset_clk_jiffy(ha_mon, env);" + return f"/* XXX: how do I reset {env}? */" + + def __fill_hybrid_get_reset_functions(self) -> list[str]: + buff = [] + if self.is_hybrid_automata(): + for var in self.constraint_vars: + if var.endswith("()"): + func_name = var.replace("()", "") + if func_name.isupper(): + buff.append(f"#define {func_name}(ha_mon) " + f"/* XXX: what is {func_name}(ha_mon)? */\n") + else: + buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{") + buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;") + buff.append("}\n") + elif var.isupper(): + buff.append(f"#define {var} /* XXX: what is {var}? */\n") + else: + buff.append(f"static u64 {var} = /* XXX: default value */;") + buff.append(f"module_param({var}, ullong, 0644);\n") + buff.append("""/* + * These functions define how to read and reset the environment variable. + * + * Common environment variables like ns-based and jiffy-based clocks have + * pre-define getters and resetters you can use. The parser can infer the type + * of the environment variable if you supply a measure unit in the constraint. + * If you define your own functions, make sure to add appropriate memory + * barriers if required. + * Some environment variables don't require a storage as they read a system + * state (e.g. preemption count). Those variables are never reset, so we don't + * define a reset function on monitors only relying on this type of variables. + */""") + buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, " + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") + _else = "" + for env in self.envs: + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") + buff.append(f"\t\treturn {self.__fill_env_getter(env)}") + _else = "else " + buff.append("\treturn ENV_INVALID_VALUE;\n}\n") + if len(self.env_stored): + buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, " + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") + _else = "" + for env in self.env_stored: + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") + buff.append(f"\t\t{self.__fill_env_resetter(env)}") + _else = "else " + buff.append("}\n") + return buff + + def _fill_hybrid_definitions(self) -> list[str]: + return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func() + + def _fill_timer_type(self) -> list: + if self.has_invariant: + return [ + "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */", + "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" + ] + return [] diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py new file mode 100644 index 000000000..45e2bab26 --- /dev/null +++ b/tools/verification/rvgen/rvgen/generator.py @@ -0,0 +1,250 @@ +#!/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> +# +# Abstract class for generating kernel runtime verification monitors from specification file + +import platform +from pathlib import Path + + +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 = \ + Path(__file__).resolve().parent / "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): + # find the kernel tree root relative to this file's location + resolved_path = Path(__file__).resolve() + if len(resolved_path.parents) > 4: + kernel_root = resolved_path.parents[4] + kernel_path = kernel_root / self.rv_dir + + if kernel_path.exists(): + self.rv_dir = str(kernel_path) + return + + # best effort if rvgen is installed and we are at the root of a kernel tree + if Path(self.rv_dir).exists(): + return + + if platform.system() != "Linux": + raise OSError("I can only run on Linux.") + + kernel_path = Path(f"/lib/modules/{platform.release()}/build") / 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 (kernel_path / "rv_trace.h").exists(): + self.rv_dir = str(kernel_path) + return + + raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") + + def _read_file(self, path): + with open(path, 'r') as fd: + content = fd.read() + return content + + def _read_template_file(self, file): + try: + path = self.abs_template_dir / file + return self._read_file(path) + except OSError: + # Specific template file not found. Try the generic template file in the template/ + # directory, which is one level up + path = self.abs_template_dir.parent / file + return self._read_file(path) + + def fill_parent(self): + return f"&rv_{self.parent}" if self.parent else "NULL" + + def fill_include_parent(self): + if self.parent: + return f"#include <monitors/{self.parent}/{self.parent}.h>\n" + 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(f" depends on RV_MON_{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 = Path(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", + f"// Add new monitors based on CONFIG_{monitor_class_type} here", + f"#include <monitors/{self.name}/{self.name}_trace.h>") + return f" - Patching {self.rv_dir}/rv_trace.h, double check the result" + + return f""" - Edit {self.rv_dir}/rv_trace.h: +Add this line where other tracepoints are included and {monitor_class_type} is defined: +#include <monitors/{self.name}/{self.name}_trace.h> +""" + + def _kconfig_marker(self, container=None) -> str: + return f"# Add new {container + ' ' if container else ''}monitors here" + + 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), + f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"") + return f" - Patching {self.rv_dir}/Kconfig, double check the result" + + return f""" - Edit {self.rv_dir}/Kconfig: +Add this line where other monitors are included: +source \"kernel/trace/rv/monitors/{self.name}/Kconfig\" +""" + + def fill_makefile_tooltip(self): + name = self.name + name_up = name.upper() + if self.auto_patch: + self._patch_file("Makefile", + "# Add new monitors here", + f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o") + return f" - Patching {self.rv_dir}/Makefile, double check the result" + + return f""" - Edit {self.rv_dir}/Makefile: +Add this line where other monitors are included: +obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o +""" + + def fill_monitor_tooltip(self): + if self.auto_patch: + return f" - Monitor created in {self.rv_dir}/monitors/{self.name}" + return f" - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)" + + def __create_directory(self): + path = Path(self.name) + if self.auto_patch: + path = Path(self.rv_dir) / "monitors" / path + path.mkdir(exist_ok=True) + + def __write_file(self, file_name, content): + with open(file_name, 'w') as file: + file.write(content) + + def _create_file(self, file_name, content): + path = Path(self.name) / file_name + if self.auto_patch: + path = Path(self.rv_dir) / "monitors" / self.name / file_name + self.__write_file(path, content) + + def print_files(self): + main_c = self.fill_main_c() + + self.__create_directory() + + path = f"{self.name}.c" + self._create_file(path, main_c) + + model_h = self.fill_model_h() + path = f"{self.name}.h" + 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, "per_obj": 4} + + 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") + tracepoint_args_skel_error_env = self.fill_tracepoint_args_skel("error_env") + 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) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%", tracepoint_args_skel_error_env) + return trace_h + + def print_files(self): + super().print_files() + trace_h = self.fill_trace_h() + path = f"{self.name}_trace.h" + self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/kunit.py b/tools/verification/rvgen/rvgen/kunit.py new file mode 100644 index 000000000..85973f918 --- /dev/null +++ b/tools/verification/rvgen/rvgen/kunit.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2026-2029 Red Hat, Inc. Gabriele Monaco <gmonaco@redhat.com> +# +# Generator for runtime verification kunit files + +import re +from pathlib import Path +from . import generator + + +class KUnitError(Exception): + """Exception raised for errors in KUnit generation and file handling.""" + + +class KUnit(generator.RVGenerator): + template_dir = "" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.local = extra_params.get("local", False) + self.kunit_c = self._read_template_file("kunit.c") + if not self.local: + self._fill_rv_kernel_dir() + try: + self.monitor_path = self.__find_monitor_c_file() + with open(self.monitor_path, 'r') as f: + self.content = f.read() + except OSError as e: + raise KUnitError(e) from e + self.monitor_class = self.__detect_monitor_class() + + def _read_template_file(self, file): + if file in ("main.c", "Kconfig"): + return "" + return super()._read_template_file(file) + + def __find_monitor_c_file(self) -> str: + """Look for the monitor file in the kernel tree or in the current folder.""" + if not self.local: + path = Path(self.rv_dir) / "monitors" / self.name / f"{self.name}.c" + if path.exists(): + return str(path) + + path = Path(self.name) / f"{self.name}.c" + if path.exists(): + return str(path) + + raise FileNotFoundError(f"Could not find monitor C file for '{self.name}'") + + def __extract_function_args(self, handler_name: str) -> str: + pattern = re.compile( + r'^\s*(.*?)\b' + re.escape(handler_name) + r'\(([^)]*)\)', + re.MULTILINE | re.DOTALL + ) + match = pattern.search(self.content) + if not match: + return "/* XXX: fill handlers argument. */" + + return match.group(2).strip() + + def __parse_attach_handlers(self) -> list[str]: + """Find handlers by parsing when they are attached to tracepoints.""" + probe_pattern = re.compile( + r'rv_attach_trace_probe\(.*, ([a-zA-Z0-9_]+)\)' + ) + handlers = [] + for match in probe_pattern.finditer(self.content): + handler = match.group(1) + if handler not in handlers: + handlers.append(handler) + return handlers + + def __detect_monitor_class(self) -> str: + for c in ("da", "ha", "ltl"): + if f"{c}_monitor.h" in self.content: + return c + return "da" + + def __fill_kunit_c(self, struct_name: str) -> str: + kunit_c = self.kunit_c + kunit_c = kunit_c.replace("%%MODEL_NAME%%", self.name) + kunit_c = kunit_c.replace("%%MODEL_NAME_UP%%", self.name.upper()) + kunit_c = kunit_c.replace("%%MONITOR_CLASS%%", self.monitor_class) + kunit_c = kunit_c.replace("%%STRUCT_NAME%%", struct_name) + return kunit_c + + def __fill_kunit_h(self, struct_name, prototypes) -> str: + return f"""/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __{self.name.upper()}_KUNIT_H +#define __{self.name.upper()}_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct {struct_name} {{ +\tstruct rv_kunit_mon mon; +\t{"\n\t".join(prototypes)} +}} {struct_name}; +#endif + +#endif /* __{self.name.upper()}_KUNIT_H */ +""" + + def __fill_monitor_handlers(self, struct_name, assignments): + struct_definition = f"""#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "{self.name}_kunit.h" + +const struct {struct_name} {struct_name} = {{ +\t.mon = RV_MON_OPS_INIT(), +\t{"\n\t".join(assignments)} +}}; +EXPORT_SYMBOL_IF_KUNIT({struct_name}); +#endif""" + + if self.auto_patch: + try: + with open(self.monitor_path, 'w') as f: + f.write(f"{self.content}\n{struct_definition}\n") + except OSError as e: + raise KUnitError(f"Error patching monitor file {self.monitor_path}: {e}") from e + else: + print(f"Append the following to {self.name}.c:\n") + print(struct_definition) + print("Now complete the test and add it to rv_monitors_test.c") + + def print_files(self): + + handlers = self.__parse_attach_handlers() + + if not handlers: + raise KUnitError(f"No handlers found in {self.monitor_path}") + + prototypes = [] + assignments = [] + for handler in handlers: + arguments = self.__extract_function_args(handler) + + prototypes.append(f"void (*{handler})({arguments});") + assignments.append(f".{handler} = {handler},") + + struct_name = f"rv_{self.name}_ops" + + self.__fill_monitor_handlers(struct_name, assignments) + + dir_path = Path(self.monitor_path).parent + + header_file_path = dir_path / f"{self.name}_kunit.h" + kunit_c_file_path = dir_path / f"{self.name}_kunit.c" + + use_backup = True + if header_file_path.exists() or kunit_c_file_path.exists(): + try: + response = input("KUnit file(s) already exist. Backup? [Y/n] ") + if response.strip().lower() in ("n", "no"): + use_backup = False + except EOFError: + print("Non-interactive session detected, backing up existing files.") + else: + use_backup = False + + if use_backup: + for path in (header_file_path, kunit_c_file_path): + if path.exists(): + try: + path.rename(path.with_suffix(path.suffix + ".old")) + except OSError as e: + raise KUnitError(f"Error backing up file {path}: {e}") from e + + header_content = self.__fill_kunit_h(struct_name, prototypes) + try: + with open(header_file_path, 'w') as f: + f.write(header_content) + print(f"Successfully created KUnit header file: {header_file_path}") + except OSError as e: + raise KUnitError(f"Error writing to file {header_file_path}: {e}") from e + + kunit_c_content = self.__fill_kunit_c(struct_name) + try: + with open(kunit_c_file_path, 'w') as f: + f.write(kunit_c_content) + print(f"Successfully created KUnit C file: {kunit_c_file_path}") + except OSError as e: + raise KUnitError(f"Error writing to file {kunit_c_file_path}: {e}") from e diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000..7cebda61b --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,524 @@ +#!/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 + +import lark + +# 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 + +GRAMMAR = r''' +start: assign+ + +assign: VARIABLE "=" _ltl + +_ltl: _opd | binop | unop + +_opd : VARIABLE + | LITERAL + | "(" _ltl ")" + +unop: UNOP _ltl +UNOP: "always" + | "eventually" + | "next" + | "not" + +binop: _opd BINOP _ltl +BINOP: "until" + | "and" + | "or" + | "imply" + +VARIABLE: /[A-Z_][A-Z0-9_]*/ +LITERAL: "true" | "false" + +COMMENT: "#" /.*/ "\n" +%ignore COMMENT + +%import common.WS +%ignore WS +''' + +class LTLError(Exception): + "Exception raised for malformed linear temporal logic" + +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 = 0 + + 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, Variable)): + return str(self.op) + 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 __str__(self): + return self.name.lower() + + 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.op, 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) + +class Transform(lark.visitors.Transformer): + def unop(self, node): + if node[0] == "always": + return ASTNode(AlwaysOp(node[1])) + if node[0] == "eventually": + return ASTNode(EventuallyOp(node[1])) + if node[0] == "next": + return ASTNode(NextOp(node[1])) + if node[0] == "not": + return ASTNode(NotOp(node[1])) + raise ValueError("Unknown operator %s" % node[0]) + + def binop(self, node): + if node[1] == "until": + return ASTNode(UntilOp(node[0], node[2])) + if node[1] == "and": + return ASTNode(AndOp(node[0], node[2])) + if node[1] == "or": + return ASTNode(OrOp(node[0], node[2])) + if node[1] == "imply": + return ASTNode(ImplyOp(node[0], node[2])) + raise ValueError("Unknown operator %s" % node[1]) + + def VARIABLE(self, args): + return ASTNode(Variable(args)) + + def LITERAL(self, args): + return ASTNode(Literal(args == "true")) + + def start(self, node): + return node + + def assign(self, node): + return node[0].op.name, node[1] + +parser = lark.Lark(GRAMMAR) + +def parse_ltl(s: str) -> ASTNode: + try: + spec = parser.parse(s) + except lark.exceptions.UnexpectedInput as e: + raise LTLError(str(e)) + spec = Transform().transform(spec) + + 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 LTLError("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 000000000..f3781a3e0 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,277 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba +from .automata import AutomataError + +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]) + + def find_share_length(atom: str) -> int: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + return i + return 0 + + abbrs = [] + for atom in atoms: + share_len = find_share_length(atom) + share = atom[:share_len] + unique = atom[share_len:] + 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) + try: + with open(file_path) as f: + self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read()) + except OSError as exc: + raise AutomataError(exc.strerror) from exc + 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) -> list[str]: + buf = [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append(f"\tS{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(f"\tLTL_{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(f"\t\t\"{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(f"\tbool {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(f"\tbool {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(f"\tbool {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(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);") + + 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(f"\tcase S{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(f"\t\t\t__set_bit(S{o.id}, next);") + 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(f"\t\t__set_bit(S{node.id}, mon->states);") + 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(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);") + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);" + + def fill_tracepoint_detach_helper(self): + return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);" + + def fill_atoms_init(self): + buff = [] + for a in self.atoms: + buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);") + 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 000000000..291b29ea2 --- /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 000000000..a60611194 --- /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 000000000..e6a20d748 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -0,0 +1,35 @@ +// 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%% = { + .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("rvgen: 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 000000000..0f6883ab4 --- /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 000000000..bd3e0aab9 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -0,0 +1,83 @@ +// 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. + */ +#define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%% +#include "%%MODEL_NAME%%.h" +#include <rv/%%MONITOR_CLASS%%_monitor.h> + +/* + * 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 = %%MONITOR_CLASS%%_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ + rv_this.enabled = 0; + +%%TRACEPOINT_DETACH%% + + %%MONITOR_CLASS%%_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_this, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: 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 000000000..87d3a1308 --- /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/dot2k/trace_hybrid.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h new file mode 100644 index 000000000..c8290e9ba --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h @@ -0,0 +1,16 @@ +/* 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%%); + +DEFINE_EVENT(error_env_%%MONITOR_CLASS%%, error_env_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ diff --git a/tools/verification/rvgen/rvgen/templates/kunit.c b/tools/verification/rvgen/rvgen/templates/kunit.c new file mode 100644 index 000000000..62092b5cc --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "%%MODEL_NAME%%_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_%%MODEL_NAME_UP%%) + +static void rv_test_%%MODEL_NAME%%(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &%%STRUCT_NAME%%.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * %%STRUCT_NAME%%.handle_event(args); + */ +} + +#else +#define rv_test_%%MODEL_NAME%% rv_test_stub +#endif 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 000000000..c33f21535 --- /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_this = { + .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_this, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +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 000000000..49394c4b0 --- /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%% */ diff --git a/tools/verification/rvgen/tests/golden/da_global/Kconfig b/tools/verification/rvgen/tests/golden/da_global/Kconfig new file mode 100644 index 000000000..799fbf11c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_GLOBAL + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "da_global monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.c b/tools/verification/rvgen/tests/golden/da_global/da_global.c new file mode 100644 index 000000000..71b26ae2d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global.c @@ -0,0 +1,95 @@ +// 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 "da_global" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_GLOBAL +#include "da_global.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_da_global); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_da_global); +} + +static int enable_da_global(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_da_global(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_global", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_global", + .description = "auto-generated", + .enable = enable_da_global, + .disable = disable_da_global, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_global(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_da_global(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_global); +module_exit(unregister_da_global); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_global: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global.h b/tools/verification/rvgen/tests/golden/da_global/da_global.h new file mode 100644 index 000000000..40b1f1c0c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_global automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_global + +enum states_da_global { + state_a_da_global, + state_b_da_global, + state_max_da_global, +}; + +#define INVALID_STATE state_max_da_global + +enum events_da_global { + event_1_da_global, + event_2_da_global, + event_max_da_global, +}; + +struct automaton_da_global { + char *state_names[state_max_da_global]; + char *event_names[event_max_da_global]; + unsigned char function[state_max_da_global][event_max_da_global]; + unsigned char initial_state; + bool final_states[state_max_da_global]; +}; + +static const struct automaton_da_global automaton_da_global = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_da_global, state_a_da_global }, + { INVALID_STATE, state_a_da_global }, + }, + .initial_state = state_a_da_global, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h new file mode 100644 index 000000000..4d2730b71 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_global/da_global_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_GLOBAL +DEFINE_EVENT(event_da_monitor, event_da_global, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_da_global, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_DA_GLOBAL */ diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig new file mode 100644 index 000000000..249ba3aee --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/Kconfig @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_PEROBJ_PARENT + depends on RV + # XXX: add dependencies if there + depends on RV_MON_PARENT_MON + default y + select DA_MON_EVENTS_ID + bool "da_perobj_parent monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c new file mode 100644 index 000000000..5c5d300b4 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.c @@ -0,0 +1,119 @@ +// 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 "da_perobj_parent" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +#include <monitors/parent_mon/parent_mon.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_OBJ +typedef /* XXX: define the target type */ *monitor_target; +#include "da_perobj_parent.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event is only valid in the initial state */ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_start_run_event(id, t, event_1_da_perobj_parent); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_event(id, t, event_2_da_perobj_parent); +} + +static void handle_event_3(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + monitor_target t = /* XXX: how do I get t? */; + da_handle_event(id, t, event_3_da_perobj_parent); +} + +/* XXX: obj is being destroyed, remove if not required (e.g. obj is static) */ +static void handle_obj_cleanup(void *data, /* XXX: fill header */) +{ + int id = /* XXX: how do I get the id? */; + da_destroy_storage(id); +} + +static int enable_da_perobj_parent(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2); + rv_attach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3); + rv_attach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup); + + return 0; +} + +static void disable_da_perobj_parent(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_2); + rv_detach_trace_probe("da_perobj_parent", /* XXX: tracepoint */, handle_event_3); + rv_detach_trace_probe("da_perobj_parent", /* XXX: cleanup tracepoint */, handle_obj_cleanup); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_perobj_parent", + .description = "auto-generated", + .enable = enable_da_perobj_parent, + .disable = disable_da_perobj_parent, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_perobj_parent(void) +{ + return rv_register_monitor(&rv_this, &rv_parent_mon); +} + +static void __exit unregister_da_perobj_parent(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_perobj_parent); +module_exit(unregister_da_perobj_parent); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_perobj_parent: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h new file mode 100644 index 000000000..3c8dc3b22 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent.h @@ -0,0 +1,64 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_perobj_parent automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_perobj_parent + +enum states_da_perobj_parent { + state_a_da_perobj_parent, + state_b_da_perobj_parent, + state_c_da_perobj_parent, + state_max_da_perobj_parent, +}; + +#define INVALID_STATE state_max_da_perobj_parent + +enum events_da_perobj_parent { + event_1_da_perobj_parent, + event_2_da_perobj_parent, + event_3_da_perobj_parent, + event_max_da_perobj_parent, +}; + +struct automaton_da_perobj_parent { + char *state_names[state_max_da_perobj_parent]; + char *event_names[event_max_da_perobj_parent]; + unsigned char function[state_max_da_perobj_parent][event_max_da_perobj_parent]; + unsigned char initial_state; + bool final_states[state_max_da_perobj_parent]; +}; + +static const struct automaton_da_perobj_parent automaton_da_perobj_parent = { + .state_names = { + "state_a", + "state_b", + "state_c", + }, + .event_names = { + "event_1", + "event_2", + "event_3", + }, + .function = { + { + state_b_da_perobj_parent, + state_c_da_perobj_parent, + INVALID_STATE, + }, + { + INVALID_STATE, + state_a_da_perobj_parent, + state_c_da_perobj_parent, + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + }, + .initial_state = state_a_da_perobj_parent, + .final_states = { 1, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h new file mode 100644 index 000000000..59bfca8f7 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_perobj_parent/da_perobj_parent_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_PEROBJ_PARENT +DEFINE_EVENT(event_da_monitor_id, event_da_perobj_parent, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_da_perobj_parent, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_DA_PEROBJ_PARENT */ diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig new file mode 100644 index 000000000..c6f350179 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_DA_PERTASK_DESC + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_ID + bool "da_pertask_desc monitor" + help + Custom description for testing diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c new file mode 100644 index 000000000..c1ae5078c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.c @@ -0,0 +1,105 @@ +// 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 "da_pertask_desc" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +#include "da_pertask_desc.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event is only valid in the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_run_event(p, event_1_da_pertask_desc); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event_2_da_pertask_desc); +} + +static void handle_event_3(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event_3_da_pertask_desc); +} + +static int enable_da_pertask_desc(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2); + rv_attach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3); + + return 0; +} + +static void disable_da_pertask_desc(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_2); + rv_detach_trace_probe("da_pertask_desc", /* XXX: tracepoint */, handle_event_3); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "da_pertask_desc", + .description = "Custom description for testing", + .enable = enable_da_pertask_desc, + .disable = disable_da_pertask_desc, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_da_pertask_desc(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_da_pertask_desc(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_da_pertask_desc); +module_exit(unregister_da_pertask_desc); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("da_pertask_desc: Custom description for testing"); diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h new file mode 100644 index 000000000..837b23875 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc.h @@ -0,0 +1,64 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of da_pertask_desc automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME da_pertask_desc + +enum states_da_pertask_desc { + state_a_da_pertask_desc, + state_b_da_pertask_desc, + state_c_da_pertask_desc, + state_max_da_pertask_desc, +}; + +#define INVALID_STATE state_max_da_pertask_desc + +enum events_da_pertask_desc { + event_1_da_pertask_desc, + event_2_da_pertask_desc, + event_3_da_pertask_desc, + event_max_da_pertask_desc, +}; + +struct automaton_da_pertask_desc { + char *state_names[state_max_da_pertask_desc]; + char *event_names[event_max_da_pertask_desc]; + unsigned char function[state_max_da_pertask_desc][event_max_da_pertask_desc]; + unsigned char initial_state; + bool final_states[state_max_da_pertask_desc]; +}; + +static const struct automaton_da_pertask_desc automaton_da_pertask_desc = { + .state_names = { + "state_a", + "state_b", + "state_c", + }, + .event_names = { + "event_1", + "event_2", + "event_3", + }, + .function = { + { + state_b_da_pertask_desc, + state_c_da_pertask_desc, + INVALID_STATE, + }, + { + INVALID_STATE, + state_a_da_pertask_desc, + state_c_da_pertask_desc, + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + }, + .initial_state = state_a_da_pertask_desc, + .final_states = { 1, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h new file mode 100644 index 000000000..4e6086c4d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/da_pertask_desc/da_pertask_desc_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_DA_PERTASK_DESC +DEFINE_EVENT(event_da_monitor_id, event_da_pertask_desc, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_da_pertask_desc, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); +#endif /* CONFIG_RV_MON_DA_PERTASK_DESC */ diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig new file mode 100644 index 000000000..0cc185ccf --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_HA_PERCPU + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_IMPLICIT + bool "ha_percpu monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c new file mode 100644 index 000000000..3a72e8671 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.c @@ -0,0 +1,227 @@ +// 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 "ha_percpu" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "ha_percpu.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * These functions define how to read and reset the environment variable. + * + * Common environment variables like ns-based and jiffy-based clocks have + * pre-define getters and resetters you can use. The parser can infer the type + * of the environment variable if you supply a measure unit in the constraint. + * If you define your own functions, make sure to add appropriate memory + * barriers if required. + * Some environment variables don't require a storage as they read a system + * state (e.g. preemption count). Those variables are never reset, so we don't + * define a reset function on monitors only relying on this type of variables. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns) +{ + if (env == clk_ha_percpu) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_ha_percpu) + return /* XXX: how do I read env1? */ + else if (env == env2_ha_percpu) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_ha_percpu env, u64 time_ns) +{ + if (env == clk_ha_percpu) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * These functions are used to validate state transitions. + * + * They are generated by parsing the model, there is usually no need to change them. + * If the monitor requires a timer, there are functions responsible to arm it when + * the next state has a constraint, cancel it in any other case and to check + * that it didn't expire before the callback run. Transitions to the same state + * without a reset never affect timers. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_ha_percpu) + return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_ha_percpu) + return ha_check_invariant_ns(ha_mon, clk_ha_percpu, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_ha_percpu && event == event0_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S0_ha_percpu && event == event1_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S1_ha_percpu && event == event0_ha_percpu) + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + else if (curr_state == S1_ha_percpu && event == event2_ha_percpu) { + res = ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + } else if (curr_state == S2_ha_percpu && event == event1_ha_percpu) + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + ha_get_env(ha_mon, clk_ha_percpu, time_ns) < foo_ns; + else if (curr_state == S3_ha_percpu && event == event0_ha_percpu) + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_ha_percpu, time_ns) == 0ull); + else if (curr_state == S3_ha_percpu && event == event1_ha_percpu) { + res = ha_monitor_env_invalid(ha_mon, clk_ha_percpu) || + (ha_get_env(ha_mon, clk_ha_percpu, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_ha_percpu, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_ha_percpu, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_ha_percpu) + return; + if (next_state == S0_ha_percpu) + ha_start_timer_ns(ha_mon, clk_ha_percpu, bar_ns(ha_mon), time_ns); + else if (next_state == S2_ha_percpu) + ha_start_timer_ns(ha_mon, clk_ha_percpu, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_ha_percpu) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_ha_percpu) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event0_ha_percpu); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + da_handle_event(event1_ha_percpu); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + da_handle_event(event2_ha_percpu); +} + +static int enable_ha_percpu(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_ha_percpu(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("ha_percpu", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "ha_percpu", + .description = "auto-generated", + .enable = enable_ha_percpu, + .disable = disable_ha_percpu, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_ha_percpu(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_ha_percpu(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_ha_percpu); +module_exit(unregister_ha_percpu); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("ha_percpu: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h new file mode 100644 index 000000000..2538db4f6 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu.h @@ -0,0 +1,72 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of ha_percpu automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME ha_percpu + +enum states_ha_percpu { + S0_ha_percpu, + S1_ha_percpu, + S2_ha_percpu, + S3_ha_percpu, + state_max_ha_percpu, +}; + +#define INVALID_STATE state_max_ha_percpu + +enum events_ha_percpu { + event0_ha_percpu, + event1_ha_percpu, + event2_ha_percpu, + event_max_ha_percpu, +}; + +enum envs_ha_percpu { + clk_ha_percpu, + env1_ha_percpu, + env2_ha_percpu, + env_max_ha_percpu, + env_max_stored_ha_percpu = env1_ha_percpu, +}; + +_Static_assert(env_max_stored_ha_percpu <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_ha_percpu { + char *state_names[state_max_ha_percpu]; + char *event_names[event_max_ha_percpu]; + char *env_names[env_max_ha_percpu]; + unsigned char function[state_max_ha_percpu][event_max_ha_percpu]; + unsigned char initial_state; + bool final_states[state_max_ha_percpu]; +}; + +static const struct automaton_ha_percpu automaton_ha_percpu = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { S0_ha_percpu, S1_ha_percpu, INVALID_STATE }, + { S0_ha_percpu, INVALID_STATE, S2_ha_percpu }, + { INVALID_STATE, S2_ha_percpu, S3_ha_percpu }, + { S0_ha_percpu, S1_ha_percpu, INVALID_STATE }, + }, + .initial_state = S0_ha_percpu, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h new file mode 100644 index 000000000..074ddff6a --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ha_percpu/ha_percpu_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_HA_PERCPU +DEFINE_EVENT(event_da_monitor, event_ha_percpu, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_ha_percpu, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); + +DEFINE_EVENT(error_env_da_monitor, error_env_ha_percpu, + TP_PROTO(char *state, char *event, char *env), + TP_ARGS(state, event, env)); +#endif /* CONFIG_RV_MON_HA_PERCPU */ diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig new file mode 100644 index 000000000..b37f46670 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_LTL_PERTASK + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "ltl_pertask monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c new file mode 100644 index 000000000..2c60b5c5b --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.c @@ -0,0 +1,107 @@ +// 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 "ltl_pertask" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "ltl_pertask.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_ltl_pertask(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_ltl_pertask(void) +{ + rv_detach_trace_probe("ltl_pertask", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "ltl_pertask", + .description = "auto-generated", + .enable = enable_ltl_pertask, + .disable = disable_ltl_pertask, +}; + +static int __init register_ltl_pertask(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_ltl_pertask(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_ltl_pertask); +module_exit(unregister_ltl_pertask); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("ltl_pertask: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h new file mode 100644 index 000000000..7e5de351b --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask.h @@ -0,0 +1,108 @@ +/* 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 ltl_pertask + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h new file mode 100644 index 000000000..ebd53621a --- /dev/null +++ b/tools/verification/rvgen/tests/golden/ltl_pertask/ltl_pertask_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_LTL_PERTASK +DEFINE_EVENT(event_ltl_monitor_id, event_ltl_pertask, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_ltl_pertask, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_LTL_PERTASK */ diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig new file mode 100644 index 000000000..175a416f8 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_BAK_KUNIT + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "test_bak_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c new file mode 100644 index 000000000..16579c1c6 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_bak_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_bak_kunit.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_bak_kunit(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_bak_kunit(void) +{ + rv_detach_trace_probe("test_bak_kunit", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_bak_kunit", + .description = "auto-generated", + .enable = enable_test_bak_kunit, + .disable = disable_test_bak_kunit, +}; + +static int __init register_test_bak_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_bak_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_bak_kunit); +module_exit(unregister_test_bak_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_bak_kunit: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h new file mode 100644 index 000000000..2bfe4e37c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit.h @@ -0,0 +1,108 @@ +/* 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 test_bak_kunit + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c new file mode 100644 index 000000000..e2b935403 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_bak_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_BAK_KUNIT) + +static void rv_test_test_bak_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_bak_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_bak_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_bak_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old new file mode 100644 index 000000000..f747925bf --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.c.old @@ -0,0 +1 @@ +DUMMY diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h new file mode 100644 index 000000000..585c4803b --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_kunit.h @@ -0,0 +1,22 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_BAK_KUNIT_KUNIT_H +#define __TEST_BAK_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_bak_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_example_event)(void *data, /* XXX: fill header */); +} rv_test_bak_kunit_ops; +#endif + +#endif /* __TEST_BAK_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h new file mode 100644 index 000000000..b98420883 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_bak_kunit/test_bak_kunit_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_BAK_KUNIT +DEFINE_EVENT(event_ltl_monitor_id, event_test_bak_kunit, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_bak_kunit, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_BAK_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_container/Kconfig b/tools/verification/rvgen/tests/golden/test_container/Kconfig new file mode 100644 index 000000000..2becb65dd --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/Kconfig @@ -0,0 +1,5 @@ +config RV_MON_TEST_CONTAINER + depends on RV + bool "test_container monitor" + help + Test container for grouping monitors diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.c b/tools/verification/rvgen/tests/golden/test_container/test_container.c new file mode 100644 index 000000000..e7e34592c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/test_container.c @@ -0,0 +1,35 @@ +// 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 "test_container" + +#include "test_container.h" + +struct rv_monitor rv_test_container = { + .name = "test_container", + .description = "Test container for grouping monitors", + .enable = NULL, + .disable = NULL, + .reset = NULL, + .enabled = 0, +}; + +static int __init register_test_container(void) +{ + return rv_register_monitor(&rv_test_container, NULL); +} + +static void __exit unregister_test_container(void) +{ + rv_unregister_monitor(&rv_test_container); +} + +module_init(register_test_container); +module_exit(unregister_test_container); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_container: Test container for grouping monitors"); diff --git a/tools/verification/rvgen/tests/golden/test_container/test_container.h b/tools/verification/rvgen/tests/golden/test_container/test_container.h new file mode 100644 index 000000000..83e434432 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_container/test_container.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_test_container; diff --git a/tools/verification/rvgen/tests/golden/test_da/Kconfig b/tools/verification/rvgen/tests/golden/test_da/Kconfig new file mode 100644 index 000000000..0143a148e --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_DA + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "test_da monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.c b/tools/verification/rvgen/tests/golden/test_da/test_da.c new file mode 100644 index 000000000..59b8dfabb --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da.c @@ -0,0 +1,95 @@ +// 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 "test_da" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +#include "test_da.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_test_da); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_test_da); +} + +static int enable_test_da(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_test_da(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("test_da", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_da", + .description = "auto-generated", + .enable = enable_test_da, + .disable = disable_test_da, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_da(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_da(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_da); +module_exit(unregister_test_da); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_da: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da.h b/tools/verification/rvgen/tests/golden/test_da/test_da.h new file mode 100644 index 000000000..d55795efb --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_da automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_da + +enum states_test_da { + state_a_test_da, + state_b_test_da, + state_max_test_da, +}; + +#define INVALID_STATE state_max_test_da + +enum events_test_da { + event_1_test_da, + event_2_test_da, + event_max_test_da, +}; + +struct automaton_test_da { + char *state_names[state_max_test_da]; + char *event_names[event_max_test_da]; + unsigned char function[state_max_test_da][event_max_test_da]; + unsigned char initial_state; + bool final_states[state_max_test_da]; +}; + +static const struct automaton_test_da automaton_test_da = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_test_da, state_a_test_da }, + { INVALID_STATE, state_a_test_da }, + }, + .initial_state = state_a_test_da, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h new file mode 100644 index 000000000..8bd67115d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da/test_da_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_DA +DEFINE_EVENT(event_da_monitor, event_test_da, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_test_da, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_TEST_DA */ diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig new file mode 100644 index 000000000..6d664ba56 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_DA_KUNIT + depends on RV + # XXX: add dependencies if there + select DA_MON_EVENTS_IMPLICIT + bool "test_da_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c new file mode 100644 index 000000000..effd26548 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_da_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_CPU +#include "test_da_kunit.h" +#include <rv/da_monitor.h> + +/* + * 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. + * + */ +static void handle_event_1(void *data, /* XXX: fill header */) +{ + da_handle_event(event_1_test_da_kunit); +} + +static void handle_event_2(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + da_handle_start_event(event_2_test_da_kunit); +} + +static int enable_test_da_kunit(void) +{ + int retval; + + retval = da_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1); + rv_attach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2); + + return 0; +} + +static void disable_test_da_kunit(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_1); + rv_detach_trace_probe("test_da_kunit", /* XXX: tracepoint */, handle_event_2); + + da_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_da_kunit", + .description = "auto-generated", + .enable = enable_test_da_kunit, + .disable = disable_test_da_kunit, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_da_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_da_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_da_kunit); +module_exit(unregister_test_da_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_da_kunit: auto-generated"); + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "test_da_kunit_kunit.h" + +const struct rv_test_da_kunit_ops rv_test_da_kunit_ops = { + .mon = RV_MON_OPS_INIT(), + .handle_event_1 = handle_event_1, + .handle_event_2 = handle_event_2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_da_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h new file mode 100644 index 000000000..290a9454c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit.h @@ -0,0 +1,47 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_da_kunit automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_da_kunit + +enum states_test_da_kunit { + state_a_test_da_kunit, + state_b_test_da_kunit, + state_max_test_da_kunit, +}; + +#define INVALID_STATE state_max_test_da_kunit + +enum events_test_da_kunit { + event_1_test_da_kunit, + event_2_test_da_kunit, + event_max_test_da_kunit, +}; + +struct automaton_test_da_kunit { + char *state_names[state_max_test_da_kunit]; + char *event_names[event_max_test_da_kunit]; + unsigned char function[state_max_test_da_kunit][event_max_test_da_kunit]; + unsigned char initial_state; + bool final_states[state_max_test_da_kunit]; +}; + +static const struct automaton_test_da_kunit automaton_test_da_kunit = { + .state_names = { + "state_a", + "state_b", + }, + .event_names = { + "event_1", + "event_2", + }, + .function = { + { state_b_test_da_kunit, state_a_test_da_kunit }, + { INVALID_STATE, state_a_test_da_kunit }, + }, + .initial_state = state_a_test_da_kunit, + .final_states = { 1, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c new file mode 100644 index 000000000..17826a5c4 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_da_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_DA_KUNIT) + +static void rv_test_test_da_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_da_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_da_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_da_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h new file mode 100644 index 000000000..0094215ff --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_kunit.h @@ -0,0 +1,23 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_DA_KUNIT_KUNIT_H +#define __TEST_DA_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_da_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_event_1)(void *data, /* XXX: fill header */); + void (*handle_event_2)(void *data, /* XXX: fill header */); +} rv_test_da_kunit_ops; +#endif + +#endif /* __TEST_DA_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h new file mode 100644 index 000000000..16804a79e --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_da_kunit/test_da_kunit_trace.h @@ -0,0 +1,15 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_DA_KUNIT +DEFINE_EVENT(event_da_monitor, event_test_da_kunit, + TP_PROTO(char *state, char *event, char *next_state, bool final_state), + TP_ARGS(state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor, error_test_da_kunit, + TP_PROTO(char *state, char *event), + TP_ARGS(state, event)); +#endif /* CONFIG_RV_MON_TEST_DA_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_ha/Kconfig b/tools/verification/rvgen/tests/golden/test_ha/Kconfig new file mode 100644 index 000000000..f4048290c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_HA + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_ID + bool "test_ha monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.c b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c new file mode 100644 index 000000000..9047ff725 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.c @@ -0,0 +1,230 @@ +// 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 "test_ha" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "test_ha.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * These functions define how to read and reset the environment variable. + * + * Common environment variables like ns-based and jiffy-based clocks have + * pre-define getters and resetters you can use. The parser can infer the type + * of the environment variable if you supply a measure unit in the constraint. + * If you define your own functions, make sure to add appropriate memory + * barriers if required. + * Some environment variables don't require a storage as they read a system + * state (e.g. preemption count). Those variables are never reset, so we don't + * define a reset function on monitors only relying on this type of variables. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns) +{ + if (env == clk_test_ha) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_test_ha) + return /* XXX: how do I read env1? */ + else if (env == env2_test_ha) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha env, u64 time_ns) +{ + if (env == clk_test_ha) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * These functions are used to validate state transitions. + * + * They are generated by parsing the model, there is usually no need to change them. + * If the monitor requires a timer, there are functions responsible to arm it when + * the next state has a constraint, cancel it in any other case and to check + * that it didn't expire before the callback run. Transitions to the same state + * without a reset never affect timers. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_test_ha) + return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_test_ha) + return ha_check_invariant_ns(ha_mon, clk_test_ha, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_test_ha && event == event0_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S0_test_ha && event == event1_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S1_test_ha && event == event0_test_ha) + ha_reset_env(ha_mon, clk_test_ha, time_ns); + else if (curr_state == S1_test_ha && event == event2_test_ha) { + res = ha_get_env(ha_mon, env1_test_ha, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_test_ha, time_ns); + } else if (curr_state == S2_test_ha && event == event1_test_ha) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + ha_get_env(ha_mon, clk_test_ha, time_ns) < foo_ns; + else if (curr_state == S3_test_ha && event == event0_test_ha) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + (ha_get_env(ha_mon, clk_test_ha, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_test_ha, time_ns) == 0ull); + else if (curr_state == S3_test_ha && event == event1_test_ha) { + res = ha_monitor_env_invalid(ha_mon, clk_test_ha) || + (ha_get_env(ha_mon, clk_test_ha, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_test_ha, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_test_ha, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_test_ha) + return; + if (next_state == S0_test_ha) + ha_start_timer_ns(ha_mon, clk_test_ha, bar_ns(ha_mon), time_ns); + else if (next_state == S2_test_ha) + ha_start_timer_ns(ha_mon, clk_test_ha, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_test_ha) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_test_ha) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_event(p, event0_test_ha); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event1_test_ha); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event2_test_ha); +} + +static int enable_test_ha(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_test_ha(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("test_ha", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ha", + .description = "auto-generated", + .enable = enable_test_ha, + .disable = disable_test_ha, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_ha(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ha(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ha); +module_exit(unregister_test_ha); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ha: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h new file mode 100644 index 000000000..949fa4453 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha.h @@ -0,0 +1,72 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_ha automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_ha + +enum states_test_ha { + S0_test_ha, + S1_test_ha, + S2_test_ha, + S3_test_ha, + state_max_test_ha, +}; + +#define INVALID_STATE state_max_test_ha + +enum events_test_ha { + event0_test_ha, + event1_test_ha, + event2_test_ha, + event_max_test_ha, +}; + +enum envs_test_ha { + clk_test_ha, + env1_test_ha, + env2_test_ha, + env_max_test_ha, + env_max_stored_test_ha = env1_test_ha, +}; + +_Static_assert(env_max_stored_test_ha <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_test_ha { + char *state_names[state_max_test_ha]; + char *event_names[event_max_test_ha]; + char *env_names[env_max_test_ha]; + unsigned char function[state_max_test_ha][event_max_test_ha]; + unsigned char initial_state; + bool final_states[state_max_test_ha]; +}; + +static const struct automaton_test_ha automaton_test_ha = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { S0_test_ha, S1_test_ha, INVALID_STATE }, + { S0_test_ha, INVALID_STATE, S2_test_ha }, + { INVALID_STATE, S2_test_ha, S3_test_ha }, + { S0_test_ha, S1_test_ha, INVALID_STATE }, + }, + .initial_state = S0_test_ha, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h new file mode 100644 index 000000000..381bafcb3 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha/test_ha_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_HA +DEFINE_EVENT(event_da_monitor_id, event_test_ha, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_test_ha, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_TEST_HA */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig new file mode 100644 index 000000000..6c48770ac --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_HA_KUNIT + depends on RV + # XXX: add dependencies if there + select HA_MON_EVENTS_ID + bool "test_ha_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c new file mode 100644 index 000000000..239b0539d --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.c @@ -0,0 +1,243 @@ +// 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 "test_ha_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#define RV_MON_TYPE RV_MON_PER_TASK +/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */ +#define HA_TIMER_TYPE HA_TIMER_HRTIMER +#include "test_ha_kunit.h" +#include <rv/ha_monitor.h> + +/* + * 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. + * + */ +#define BAR_NS(ha_mon) /* XXX: what is BAR_NS(ha_mon)? */ + +#define FOO_NS /* XXX: what is FOO_NS? */ + +static inline u64 bar_ns(struct ha_monitor *ha_mon) +{ + return /* XXX: what is bar_ns(ha_mon)? */; +} + +static u64 foo_ns = /* XXX: default value */; +module_param(foo_ns, ullong, 0644); + +/* + * These functions define how to read and reset the environment variable. + * + * Common environment variables like ns-based and jiffy-based clocks have + * pre-define getters and resetters you can use. The parser can infer the type + * of the environment variable if you supply a measure unit in the constraint. + * If you define your own functions, make sure to add appropriate memory + * barriers if required. + * Some environment variables don't require a storage as they read a system + * state (e.g. preemption count). Those variables are never reset, so we don't + * define a reset function on monitors only relying on this type of variables. + */ +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns) +{ + if (env == clk_test_ha_kunit) + return ha_get_clk_ns(ha_mon, env, time_ns); + else if (env == env1_test_ha_kunit) + return /* XXX: how do I read env1? */ + else if (env == env2_test_ha_kunit) + return /* XXX: how do I read env2? */ + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_test_ha_kunit env, u64 time_ns) +{ + if (env == clk_test_ha_kunit) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +/* + * These functions are used to validate state transitions. + * + * They are generated by parsing the model, there is usually no need to change them. + * If the monitor requires a timer, there are functions responsible to arm it when + * the next state has a constraint, cancel it in any other case and to check + * that it didn't expire before the callback run. Transitions to the same state + * without a reset never affect timers. + */ +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state == S0_test_ha_kunit) + return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, bar_ns(ha_mon)); + else if (curr_state == S2_test_ha_kunit) + return ha_check_invariant_ns(ha_mon, clk_test_ha_kunit, time_ns, BAR_NS(ha_mon)); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res = true; + + if (curr_state == S0_test_ha_kunit && event == event0_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S0_test_ha_kunit && event == event1_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S1_test_ha_kunit && event == event0_test_ha_kunit) + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + else if (curr_state == S1_test_ha_kunit && event == event2_test_ha_kunit) { + res = ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 0ull; + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + } else if (curr_state == S2_test_ha_kunit && event == event1_test_ha_kunit) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < foo_ns; + else if (curr_state == S3_test_ha_kunit && event == event0_test_ha_kunit) + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < FOO_NS && + ha_get_env(ha_mon, env2_test_ha_kunit, time_ns) == 0ull); + else if (curr_state == S3_test_ha_kunit && event == event1_test_ha_kunit) { + res = ha_monitor_env_invalid(ha_mon, clk_test_ha_kunit) || + (ha_get_env(ha_mon, clk_test_ha_kunit, time_ns) < 5000ull && + ha_get_env(ha_mon, env1_test_ha_kunit, time_ns) == 1ull); + ha_reset_env(ha_mon, clk_test_ha_kunit, time_ns); + } + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state == curr_state && event != event0_test_ha_kunit) + return; + if (next_state == S0_test_ha_kunit) + ha_start_timer_ns(ha_mon, clk_test_ha_kunit, bar_ns(ha_mon), time_ns); + else if (next_state == S2_test_ha_kunit) + ha_start_timer_ns(ha_mon, clk_test_ha_kunit, BAR_NS(ha_mon), time_ns); + else if (curr_state == S0_test_ha_kunit) + ha_cancel_timer(ha_mon); + else if (curr_state == S2_test_ha_kunit) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_event0(void *data, /* XXX: fill header */) +{ + /* XXX: validate that this event always leads to the initial state */ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_start_event(p, event0_test_ha_kunit); +} + +static void handle_event1(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event1_test_ha_kunit); +} + +static void handle_event2(void *data, /* XXX: fill header */) +{ + struct task_struct *p = /* XXX: how do I get p? */; + da_handle_event(p, event2_test_ha_kunit); +} + +static int enable_test_ha_kunit(void) +{ + int retval; + + retval = ha_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0); + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1); + rv_attach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2); + + return 0; +} + +static void disable_test_ha_kunit(void) +{ + rv_this.enabled = 0; + + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event0); + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event1); + rv_detach_trace_probe("test_ha_kunit", /* XXX: tracepoint */, handle_event2); + + ha_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ha_kunit", + .description = "auto-generated", + .enable = enable_test_ha_kunit, + .disable = disable_test_ha_kunit, + .reset = da_monitor_reset_all, + .enabled = 0, +}; + +static int __init register_test_ha_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ha_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ha_kunit); +module_exit(unregister_test_ha_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ha_kunit: auto-generated"); + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) +#include <kunit/visibility.h> +#include "test_ha_kunit_kunit.h" + +const struct rv_test_ha_kunit_ops rv_test_ha_kunit_ops = { + .mon = RV_MON_OPS_INIT(), + .handle_event0 = handle_event0, + .handle_event1 = handle_event1, + .handle_event2 = handle_event2, +}; +EXPORT_SYMBOL_IF_KUNIT(rv_test_ha_kunit_ops); +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h new file mode 100644 index 000000000..5c428f818 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit.h @@ -0,0 +1,88 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of test_ha_kunit automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME test_ha_kunit + +enum states_test_ha_kunit { + S0_test_ha_kunit, + S1_test_ha_kunit, + S2_test_ha_kunit, + S3_test_ha_kunit, + state_max_test_ha_kunit, +}; + +#define INVALID_STATE state_max_test_ha_kunit + +enum events_test_ha_kunit { + event0_test_ha_kunit, + event1_test_ha_kunit, + event2_test_ha_kunit, + event_max_test_ha_kunit, +}; + +enum envs_test_ha_kunit { + clk_test_ha_kunit, + env1_test_ha_kunit, + env2_test_ha_kunit, + env_max_test_ha_kunit, + env_max_stored_test_ha_kunit = env1_test_ha_kunit, +}; + +_Static_assert(env_max_stored_test_ha_kunit <= MAX_HA_ENV_LEN, "Not enough slots"); +#define HA_CLK_NS + +struct automaton_test_ha_kunit { + char *state_names[state_max_test_ha_kunit]; + char *event_names[event_max_test_ha_kunit]; + char *env_names[env_max_test_ha_kunit]; + unsigned char function[state_max_test_ha_kunit][event_max_test_ha_kunit]; + unsigned char initial_state; + bool final_states[state_max_test_ha_kunit]; +}; + +static const struct automaton_test_ha_kunit automaton_test_ha_kunit = { + .state_names = { + "S0", + "S1", + "S2", + "S3", + }, + .event_names = { + "event0", + "event1", + "event2", + }, + .env_names = { + "clk", + "env1", + "env2", + }, + .function = { + { + S0_test_ha_kunit, + S1_test_ha_kunit, + INVALID_STATE, + }, + { + S0_test_ha_kunit, + INVALID_STATE, + S2_test_ha_kunit, + }, + { + INVALID_STATE, + S2_test_ha_kunit, + S3_test_ha_kunit, + }, + { + S0_test_ha_kunit, + S1_test_ha_kunit, + INVALID_STATE, + }, + }, + .initial_state = S0_test_ha_kunit, + .final_states = { 1, 0, 0, 0 }, +}; diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c new file mode 100644 index 000000000..6214a4aa6 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_ha_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_HA_KUNIT) + +static void rv_test_test_ha_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_ha_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_ha_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_ha_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h new file mode 100644 index 000000000..0b2030cb6 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_kunit.h @@ -0,0 +1,24 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_HA_KUNIT_KUNIT_H +#define __TEST_HA_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_ha_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_event0)(void *data, /* XXX: fill header */); + void (*handle_event1)(void *data, /* XXX: fill header */); + void (*handle_event2)(void *data, /* XXX: fill header */); +} rv_test_ha_kunit_ops; +#endif + +#endif /* __TEST_HA_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h new file mode 100644 index 000000000..6c13ee006 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ha_kunit/test_ha_kunit_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_HA_KUNIT +DEFINE_EVENT(event_da_monitor_id, event_test_ha_kunit, + TP_PROTO(int id, char *state, char *event, char *next_state, bool final_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_test_ha_kunit, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_test_ha_kunit, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_TEST_HA_KUNIT */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig new file mode 100644 index 000000000..e2d0e721f --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/Kconfig @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_LTL + depends on RV + # XXX: add dependencies if there + depends on RV_MON_LTL_PARENT + default y + select LTL_MON_EVENTS_ID + bool "test_ltl monitor" + help + Simple description diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c new file mode 100644 index 000000000..dd961c5dc --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.c @@ -0,0 +1,108 @@ +// 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 "test_ltl" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +#include <monitors/ltl_parent/ltl_parent.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_ltl.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_ltl(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_ltl(void) +{ + rv_detach_trace_probe("test_ltl", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ltl", + .description = "Simple description", + .enable = enable_test_ltl, + .disable = disable_test_ltl, +}; + +static int __init register_test_ltl(void) +{ + return rv_register_monitor(&rv_this, &rv_ltl_parent); +} + +static void __exit unregister_test_ltl(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ltl); +module_exit(unregister_test_ltl); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ltl: Simple description"); diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h new file mode 100644 index 000000000..7895f2e23 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl.h @@ -0,0 +1,108 @@ +/* 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 test_ltl + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h new file mode 100644 index 000000000..3571b004c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl/test_ltl_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_LTL +DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_LTL */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig new file mode 100644 index 000000000..3e334c344 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_TEST_LTL_KUNIT + depends on RV + # XXX: add dependencies if there + select LTL_MON_EVENTS_ID + bool "test_ltl_kunit monitor" + help + auto-generated diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c new file mode 100644 index 000000000..c1d58ce43 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.c @@ -0,0 +1,107 @@ +// 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 "test_ltl_kunit" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> + + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "test_ltl_kunit.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. + */ + ltl_atom_set(mon, LTL_EVENT_A, true/false); + ltl_atom_set(mon, LTL_EVENT_B, true/false); +} + +/* + * 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. + */ +static void handle_example_event(void *data, /* XXX: fill header */) +{ + ltl_atom_update(task, LTL_EVENT_A, true/false); +} + +static int enable_test_ltl_kunit(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + + rv_attach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event); + + return 0; +} + +static void disable_test_ltl_kunit(void) +{ + rv_detach_trace_probe("test_ltl_kunit", /* XXX: tracepoint */, handle_example_event); + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_this = { + .name = "test_ltl_kunit", + .description = "auto-generated", + .enable = enable_test_ltl_kunit, + .disable = disable_test_ltl_kunit, +}; + +static int __init register_test_ltl_kunit(void) +{ + return rv_register_monitor(&rv_this, NULL); +} + +static void __exit unregister_test_ltl_kunit(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_test_ltl_kunit); +module_exit(unregister_test_ltl_kunit); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("rvgen: auto-generated"); +MODULE_DESCRIPTION("test_ltl_kunit: auto-generated"); diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h new file mode 100644 index 000000000..acc503b56 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit.h @@ -0,0 +1,108 @@ +/* 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 test_ltl_kunit + +enum ltl_atom { + LTL_EVENT_A, + LTL_EVENT_B, + LTL_NUM_ATOM +}; +static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM); + +static const char *ltl_atom_str(enum ltl_atom atom) +{ + static const char *const names[] = { + "ev_a", + "ev_b", + }; + + return names[atom]; +} + +enum ltl_buchi_state { + S0, + S1, + S2, + S3, + S4, + RV_NUM_BA_STATES +}; +static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES); + +static void ltl_start(struct task_struct *task, struct ltl_monitor *mon) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + if (val1) + __set_bit(S0, mon->states); + if (true) + __set_bit(S1, mon->states); + if (event_b) + __set_bit(S4, mon->states); +} + +static void +ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next) +{ + bool event_b = test_bit(LTL_EVENT_B, mon->atoms); + bool event_a = test_bit(LTL_EVENT_A, mon->atoms); + bool val1 = !event_a; + + switch (state) { + case S0: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S1: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S2: + if (true) + __set_bit(S1, next); + if (true && val1) + __set_bit(S2, next); + if (event_b && val1) + __set_bit(S3, next); + if (event_b) + __set_bit(S4, next); + break; + case S3: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + case S4: + if (val1) + __set_bit(S0, next); + if (true) + __set_bit(S1, next); + if (event_b) + __set_bit(S4, next); + break; + } +} diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c new file mode 100644 index 000000000..37dab5dfd --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.c @@ -0,0 +1,33 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/rv.h> +#include <rv/kunit.h> +/* + * XXX: include required headers, e.g., + * #include <linux/sched.h> + */ +#include "test_ltl_kunit_kunit.h" + +#if IS_REACHABLE(CONFIG_RV_MON_TEST_LTL_KUNIT) + +static void rv_test_test_ltl_kunit(struct kunit *test) +{ + struct rv_kunit_ctx *ctx = test->priv; + /* + * If you need to create task_structs with rv_kunit_alloc_mock_task() + * do it BEFORE preparing the test. + */ + + prepare_test(test, &rv_test_ltl_kunit_ops.mon); + + /* + * XXX: write the test here + * e.g. + * RV_KUNIT_EXPECT_REACTION_HERE(test, ctx) + * rv_test_ltl_kunit_ops.handle_event(args); + */ +} + +#else +#define rv_test_test_ltl_kunit rv_test_stub +#endif diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h new file mode 100644 index 000000000..b2ca34be3 --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_kunit.h @@ -0,0 +1,22 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +/* + * Automatically generated by rvgen kunit. + * May need manual intervention for function prototypes that couldn't be + * found (e.g. are in another file) or variables to be exported. + */ + +#ifndef __TEST_LTL_KUNIT_KUNIT_H +#define __TEST_LTL_KUNIT_KUNIT_H + +#if IS_ENABLED(CONFIG_RV_MONITORS_KUNIT_TEST) + +#include <linux/rv.h> +#include <rv/kunit.h> + +extern const struct rv_test_ltl_kunit_ops { + struct rv_kunit_mon mon; + void (*handle_example_event)(void *data, /* XXX: fill header */); +} rv_test_ltl_kunit_ops; +#endif + +#endif /* __TEST_LTL_KUNIT_KUNIT_H */ diff --git a/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h new file mode 100644 index 000000000..a054d5b2c --- /dev/null +++ b/tools/verification/rvgen/tests/golden/test_ltl_kunit/test_ltl_kunit_trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_TEST_LTL_KUNIT +DEFINE_EVENT(event_ltl_monitor_id, event_test_ltl_kunit, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_ltl_monitor_id, error_test_ltl_kunit, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_TEST_LTL_KUNIT */ diff --git a/tools/verification/rvgen/tests/rvgen_container.t b/tools/verification/rvgen/tests/rvgen_container.t new file mode 100644 index 000000000..fa4fb3db8 --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_container.t @@ -0,0 +1,20 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help tests +check "verify container subcommand help" \ + "$RVGEN container -h" 0 "model_name" "class" + +check_and_compare_folder "container with description" \ + "$RVGEN container -n test_container -D 'Test container for grouping monitors'" \ + "test_container" "Writing the monitor into the directory test_container" + +# Error handling tests +check "missing required model_name" \ + "$RVGEN container" 2 "the following arguments are required: -n/--model_name" + +test_end diff --git a/tools/verification/rvgen/tests/rvgen_kunit.t b/tools/verification/rvgen/tests/rvgen_kunit.t new file mode 100644 index 000000000..d27d9175f --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_kunit.t @@ -0,0 +1,41 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help tests +check "verify kunit subcommand help" \ + "$RVGEN kunit -h" 0 "model_name" "spec" + +check_and_compare_folder "KUnit generation with local lookup and test_da_kunit" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu -n test_da_kunit && $RVGEN kunit -a -l -n test_da_kunit" \ + "test_da_kunit" "Now complete the test and add it to rv_monitors_test.c" "RV_MON_OPS_INIT" + +check_and_compare_folder "KUnit generation with local lookup and test_ha_kunit" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task -n test_ha_kunit && $RVGEN kunit -a -l -n test_ha_kunit" \ + "test_ha_kunit" "Successfully created KUnit" "Append the following to" + +check_and_compare_folder "KUnit generation with local lookup and test_ltl_kunit" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_ltl_kunit && $RVGEN kunit -l -n test_ltl_kunit" \ + "test_ltl_kunit" "RV_MON_OPS_INIT" + +check_and_compare_folder "KUnit generation with backup file" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n test_bak_kunit && echo DUMMY > test_bak_kunit/test_bak_kunit_kunit.c && $RVGEN kunit -l -n test_bak_kunit" \ + "test_bak_kunit" "KUnit file(s) already exist.*backing up existing files" + +# Error handling tests +check "missing required model_name" \ + "$RVGEN kunit" 2 "the following arguments are required: -n/--model_name" + +check "non-existent model_name with auto_patch" \ + "$RVGEN kunit -a -n nonexistent" 1 \ + "Could not find monitor C file" "Traceback (most recent call last)" + +check "monitor without handlers" \ + "mkdir -p nohandler ; echo DUMMY > nohandler/nohandler.c ; $RVGEN kunit -l -n nohandler" 1 \ + "No handlers found" "Traceback (most recent call last)" +rm -rf nohandler + +test_end diff --git a/tools/verification/rvgen/tests/rvgen_monitor.t b/tools/verification/rvgen/tests/rvgen_monitor.t new file mode 100644 index 000000000..5f2562600 --- /dev/null +++ b/tools/verification/rvgen/tests/rvgen_monitor.t @@ -0,0 +1,87 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +source ../tests/engine.sh +test_begin + +set_timeout 30s + +# Help and basic tests +check "verify help page" \ + "$RVGEN --help" 0 "Generate kernel rv monitor" + +check "verify monitor subcommand help" \ + "$RVGEN monitor --help" 0 "Monitor class" + +# DA monitor tests - test all monitor types +check_and_compare_folder "DA per_cpu (default name)" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t per_cpu" \ + "test_da" "obj-\$(CONFIG_RV_MON_TEST_DA) += monitors/test_da/test_da.o" + +check_and_compare_folder "DA global type" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot -t global -n da_global" \ + "da_global" "DA_MON_EVENTS_IMPLICIT" + +check_and_compare_folder "DA per_task with description" \ + "$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_task -n da_pertask_desc -D 'Custom description for testing'" \ + "da_pertask_desc" "#include <monitors/da_pertask_desc/da_pertask_desc_trace.h>" + +check_and_compare_folder "DA per_obj with parent" \ + "$RVGEN monitor -c da -s tests/specs/test_da2.dot -t per_obj -n da_perobj_parent -p parent_mon" \ + "da_perobj_parent" "DA_MON_EVENTS_ID" + +# HA monitor tests +check_and_compare_folder "HA per_task (default name)" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_task" \ + "test_ha" "HA_MON_EVENTS_ID" + +check_and_compare_folder "HA per_cpu type" \ + "$RVGEN monitor -c ha -s tests/specs/test_ha.dot -t per_cpu -n ha_percpu" \ + "ha_percpu" "HA_MON_EVENTS_IMPLICIT" + +# LTL monitor test +check_and_compare_folder "LTL per_task" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -n ltl_pertask" \ + "ltl_pertask" "source \"kernel/trace/rv/monitors/ltl_pertask/Kconfig\"" + +check_and_compare_folder "LTL per_task with parent and description (default name)" \ + "$RVGEN monitor -c ltl -s tests/specs/test_ltl.ltl -t per_task -p ltl_parent -D 'Simple description'" \ + "test_ltl" "LTL_MON_EVENTS_ID" + +# Error handling tests +check "missing required spec argument" \ + "$RVGEN monitor -c da -t per_cpu" 2 \ + "the following arguments are required: -s/--spec" "Traceback (most recent call last)" + +check "missing required monitor type" \ + "$RVGEN monitor -c da -s tests/specs/test_da.dot" 2 \ + "the following arguments are required: -t/--monitor_type" "Traceback (most recent call last)" + +check "missing required monitor class" \ + "$RVGEN monitor -s tests/specs/test_da.dot -t per_cpu" 2 \ + "the following arguments are required: -c/--class" "Traceback (most recent call last)" + +check "invalid monitor class" \ + "$RVGEN monitor -c invalid -s tests/specs/test_da.dot -t per_cpu" 1 \ + "Unknown monitor class" "Traceback (most recent call last)" + +check "missing dot file" \ + "$RVGEN monitor -c da -s tests/specs/nonexistent.dot -t per_cpu" 1 \ + "No such file or directory" "Traceback (most recent call last)" + +check "missing ltl file" \ + "$RVGEN monitor -c ltl -s tests/specs/nonexistent.ltl -t per_task" 1 \ + "No such file or directory" "Traceback (most recent call last)" + +check "invalid dot file syntax" \ + "$RVGEN monitor -c da -s tests/specs/test_invalid.dot -t per_cpu" 1 \ + "The automaton doesn't have an initial state" "Traceback (most recent call last)" + +check "invalid ha file syntax" \ + "$RVGEN monitor -c ha -s tests/specs/test_invalid_ha.dot -t per_obj" 1 \ + "Unrecognised event" "Traceback (most recent call last)" + +check "invalid ltl file syntax" \ + "$RVGEN monitor -c ltl -s tests/specs/test_invalid.ltl -t per_task" 1 \ + "No terminal matches 'i'" "Traceback (most recent call last)" + +test_end diff --git a/tools/verification/rvgen/tests/specs/test_da.dot b/tools/verification/rvgen/tests/specs/test_da.dot new file mode 100644 index 000000000..e555c239b --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_da.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a"]; + "state_a" -> "state_a" [ label = "event_2" ]; + "state_a" -> "state_b" [ label = "event_1" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_da2.dot b/tools/verification/rvgen/tests/specs/test_da2.dot new file mode 100644 index 000000000..cdd4192f5 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_da2.dot @@ -0,0 +1,19 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = circle] "state_c"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a"]; + "state_a" -> "state_b" [ label = "event_1" ]; + "state_a" -> "state_c" [ label = "event_2" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + "state_b" -> "state_c" [ label = "event_3" ]; + "state_c" [label = "state_c"]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_ha.dot b/tools/verification/rvgen/tests/specs/test_ha.dot new file mode 100644 index 000000000..af18ad738 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_ha.dot @@ -0,0 +1,27 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "S1"}; + {node [shape = plaintext, style=invis, label=""] "__init_S0"}; + {node [shape = doublecircle] "S0"}; + {node [shape = circle] "S0"}; + {node [shape = circle] "S2"}; + {node [shape = circle] "S3"}; + "__init_S0" -> "S0"; + "S0" [label = "S0\nclk < bar_ns()", color = green3]; + "S1" [label = "S1"]; + "S2" [label = "S2\nclk < BAR_NS()"]; + "S3" [label = "S3"]; + "S1" -> "S0" [ label = "event0;reset(clk)" ]; + "S0" -> "S1" [ label = "event1;reset(clk)" ]; + "S0" -> "S0" [ label = "event0;reset(clk)" ]; + "S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ]; + "S2" -> "S3" [ label = "event2" ]; + "S2" -> "S2" [ label = "event1;clk < foo_ns" ]; + "S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ]; + "S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ]; + { rank = min ; + "__init_S0"; + "S0"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_invalid.dot b/tools/verification/rvgen/tests/specs/test_invalid.dot new file mode 100644 index 000000000..17c63fc57 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid.dot @@ -0,0 +1,8 @@ +digraph invalid { + {node [shape = circle] "init"}; + {node [shape = circle] "state1"}; + "init" [label = "init"]; + "init" -> "state1" [ label = "event_a" ]; + "state1" [label = "state1"]; + "state1" -> "init" [ label = "event_b" ]; +} diff --git a/tools/verification/rvgen/tests/specs/test_invalid.ltl b/tools/verification/rvgen/tests/specs/test_invalid.ltl new file mode 100644 index 000000000..cf36307e0 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid.ltl @@ -0,0 +1 @@ +RULE = A invalid B diff --git a/tools/verification/rvgen/tests/specs/test_invalid_ha.dot b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot new file mode 100644 index 000000000..06de6aa87 --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_invalid_ha.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a;clk < 1"]; + "state_a" -> "state_a" [ label = "event_2;reset(clk)" ]; + "state_a" -> "state_b" [ label = "event_1;wrong_constraint" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +} diff --git a/tools/verification/rvgen/tests/specs/test_ltl.ltl b/tools/verification/rvgen/tests/specs/test_ltl.ltl new file mode 100644 index 000000000..5ed658abd --- /dev/null +++ b/tools/verification/rvgen/tests/specs/test_ltl.ltl @@ -0,0 +1 @@ +RULE = always (EVENT_A imply eventually EVENT_B) diff --git a/tools/verification/tests/engine.sh b/tools/verification/tests/engine.sh new file mode 100644 index 000000000..cfdf2180a --- /dev/null +++ b/tools/verification/tests/engine.sh @@ -0,0 +1,175 @@ +#!/bin/bash +# SPDX-License-Identifier: GPL-2.0 +test_begin() { + # Count tests to allow the test harness to double-check if all were + # included correctly. + ctr=0 + [ -z "$RV" ] && RV="../rv/rv" + [ -z "$RVGEN" ] && RVGEN="python3 ../rvgen" + [ -z "$GOLDEN_DIR" ] && GOLDEN_DIR="tests/golden" + [ -n "$TEST_COUNT" ] && echo "1..$TEST_COUNT" +} + +failure() { + fail=1 + if [ $# -gt 0 ]; then + failbuf+="$1" + failbuf+=$'\n' + fi +} + +report() { + local desc="$1" + + if [ "$fail" -eq 0 ]; then + echo "ok $ctr - $desc" + else + # Add output and exit code as comments in case of failure + echo "not ok $ctr - $desc" + echo -n "$failbuf" + echo "$result" | col -b | while read -r line; do echo "# $line"; done + printf "#\n# exit code %s\n" "$exitcode" + fi +} + +_check() { + local command=$2 + local expected_exitcode=${3:-0} + local expected_output=$4 + local unexpected_output=$5 + local all_lines_pattern=$6 + local patterns="$expected_output $unexpected_output $all_lines_pattern" + local bgpid pid + + eval "$TIMEOUT" "$command" &> check_output.$$ & + bgpid=$! + + if grep -q "\$pid" <<< "$patterns"; then + for _ in {1..30}; do + pid=$(pgrep -f "${command%%[|;&>]*}" | tail -n1) + [ -n "$pid" ] && break + sleep 0.1 + done + fi + + wait $bgpid + exitcode=$? + result=$(tr -d '\0' < check_output.$$) + rm -f check_output.$$ + + failbuf='' + fail=0 + + # Suppress any other error if a needed pid is empty + if [ -z "$pid" ] && grep -q "\$pid" <<< "$patterns"; then + result='' + failure "# Empty pid for $command" + return 1 + fi + + expected_output="${expected_output//\$pid/$pid}" + unexpected_output="${unexpected_output//\$pid/$pid}" + all_lines_pattern="${all_lines_pattern//\$pid/$pid}" + + # Test if the results matches if requested + if [ -n "$expected_output" ] && ! grep -qe "$expected_output" <<< "$result"; then + failure "# Output match failed: \"$expected_output\"" + fi + + if [ -n "$unexpected_output" ] && grep -qe "$unexpected_output" <<< "$result"; then + failure "# Output non-match failed: \"$unexpected_output\"" + fi + + if [ -n "$all_lines_pattern" ] && grep -vqe "$all_lines_pattern" <<< "$result"; then + failure "# All-lines pattern failed: \"$all_lines_pattern\"" + fi + + if [ $exitcode -ne "$expected_exitcode" ]; then + failure "# Expected exit code $expected_exitcode" + fi +} + +check() { + # Simple check: run the command with given arguments and test exit code. + # If TEST_COUNT is set, run the test. Otherwise, just count. + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + _check "$@" + report "$1" + fi +} + +check_if_exists() { + # Conditional check that skips if a file or folder doesn't exist + local desc=$1 + local command=$2 + local file=$3 + local expected_output=$4 + local unexpected_output=$5 + local all_lines_pattern=$6 + + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + if [ ! -e "$file" ]; then + echo "ok $ctr - $desc # SKIP file not found: $file" + else + _check "$desc" "$command" 0 "$expected_output" \ + "$unexpected_output" "$all_lines_pattern" + report "$desc" + fi + fi +} + +check_and_compare_folder() { + # Run command, compare generated folder to golden, and cleanup + local desc=$1 + local command=$2 + local generated_dir=$3 + local expected_output=$4 + local unexpected_output=$5 + local golden_dir="$GOLDEN_DIR/$generated_dir" + + ctr=$((ctr + 1)) + if [ -n "$TEST_COUNT" ]; then + rm -rf "$generated_dir" + _check "$desc" "$command" 0 "$expected_output" "$unexpected_output" + + if [ "$fail" -eq 0 ] && [ ! -d "$generated_dir" ]; then + failure "# Generated directory not found: $generated_dir" + fi + + if [ "$fail" -ne 0 ]; then + : + elif ! diff -r "$generated_dir" "$golden_dir" &> /dev/null; then + failure "# Directories differ:" + failbuf+=$(diff -r "$generated_dir" "$golden_dir" 2>&1 | sed 's/^/# /') + failbuf+=$'\n' + fi + + report "$1" + + rm -rf "$generated_dir" + fi +} + +set_timeout() { + TIMEOUT="timeout -v -k 30s $1" +} + +set_expected_timeout() { + TIMEOUT="timeout --preserve-status -k 30s $1" +} + +unset_timeout() { + unset TIMEOUT +} + +test_end() { + # If running without TEST_COUNT, tests are not actually run, just + # counted. In that case, re-run the test with the correct count. + [ -z "$TEST_COUNT" ] && TEST_COUNT=$ctr exec bash "$0" || true +} + +# Avoid any environmental discrepancies +export LC_ALL=C +unset_timeout |
