rv.h

  1/* SPDX-License-Identifier: GPL-2.0 */
  2/*
  3 * Runtime Verification.
  4 *
  5 * For futher information, see: kernel/trace/rv/rv.c.
  6 */
  7#ifndef _LINUX_RV_H
  8#define _LINUX_RV_H
  9
 10#define MAX_DA_NAME_LEN			32
 11#define MAX_DA_RETRY_RACING_EVENTS	3
 12
 13#ifdef CONFIG_RV
 14#include <linux/array_size.h>
 15#include <linux/bitops.h>
 16#include <linux/list.h>
 17#include <linux/types.h>
 18
 19/*
 20 * Deterministic automaton per-object variables.
 21 */
 22struct da_monitor {
 23	bool		monitoring;
 24	unsigned int	curr_state;
 25};
 26
 27#ifdef CONFIG_RV_LTL_MONITOR
 28
 29/*
 30 * In the future, if the number of atomic propositions or the size of Buchi
 31 * automaton is larger, we can switch to dynamic allocation. For now, the code
 32 * is simpler this way.
 33 */
 34#define RV_MAX_LTL_ATOM 32
 35#define RV_MAX_BA_STATES 32
 36
 37/**
 38 * struct ltl_monitor - A linear temporal logic runtime verification monitor
 39 * @states:	States in the Buchi automaton. As Buchi automaton is a
 40 *		non-deterministic state machine, the monitor can be in multiple
 41 *		states simultaneously. This is a bitmask of all possible states.
 42 *		If this is zero, that means either:
 43 *		    - The monitor has not started yet (e.g. because not all
 44 *		      atomic propositions are known).
 45 *		    - There is no possible state to be in. In other words, a
 46 *		      violation of the LTL property is detected.
 47 * @atoms:	The values of atomic propositions.
 48 * @unknown_atoms: Atomic propositions which are still unknown.
 49 */
 50struct ltl_monitor {
 51	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
 52	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
 53	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
 54};
 55
 56static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
 57{
 58	for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
 59		if (mon->states[i])
 60			return true;
 61	}
 62	return false;
 63}
 64
 65static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
 66{
 67	for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
 68		if (mon->unknown_atoms[i])
 69			return false;
 70	}
 71	return true;
 72}
 73
 74#else
 75
 76struct ltl_monitor {};
 77
 78#endif /* CONFIG_RV_LTL_MONITOR */
 79
 80#define RV_PER_TASK_MONITOR_INIT	(CONFIG_RV_PER_TASK_MONITORS)
 81
 82union rv_task_monitor {
 83	struct da_monitor	da_mon;
 84	struct ltl_monitor	ltl_mon;
 85};
 86
 87#ifdef CONFIG_RV_REACTORS
 88struct rv_reactor {
 89	const char		*name;
 90	const char		*description;
 91	__printf(1, 0) void	(*react)(const char *msg, va_list args);
 92	struct list_head	list;
 93};
 94#endif
 95
 96struct rv_monitor {
 97	const char		*name;
 98	const char		*description;
 99	bool			enabled;
100	int			(*enable)(void);
101	void			(*disable)(void);
102	void			(*reset)(void);
103#ifdef CONFIG_RV_REACTORS
104	struct rv_reactor	*reactor;
105	__printf(1, 0) void	(*react)(const char *msg, va_list args);
106#endif
107	struct list_head	list;
108	struct rv_monitor	*parent;
109	struct dentry		*root_d;
110};
111
112bool rv_monitoring_on(void);
113int rv_unregister_monitor(struct rv_monitor *monitor);
114int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
115int rv_get_task_monitor_slot(void);
116void rv_put_task_monitor_slot(int slot);
117
118#ifdef CONFIG_RV_REACTORS
119int rv_unregister_reactor(struct rv_reactor *reactor);
120int rv_register_reactor(struct rv_reactor *reactor);
121__printf(2, 3)
122void rv_react(struct rv_monitor *monitor, const char *msg, ...);
123#else
124__printf(2, 3)
125static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...)
126{
127}
128#endif /* CONFIG_RV_REACTORS */
129
130#endif /* CONFIG_RV */
131#endif /* _LINUX_RV_H */