include/linux/rv.h

/* SPDX-License-Identifier: GPL-2.0 */
/*
 * Runtime Verification.
 *
 * For futher information, see: kernel/trace/rv/rv.c.
 */
#ifndef _LINUX_RV_H
#define _LINUX_RV_H

#define MAX_DA_NAME_LEN			32
#define MAX_DA_RETRY_RACING_EVENTS	3

#define RV_MON_GLOBAL   0
#define RV_MON_PER_CPU  1
#define RV_MON_PER_TASK 2
#define RV_MON_PER_OBJ  3

#ifdef CONFIG_RV
#include <linux/array_size.h>
#include <linux/bitops.h>
#include <linux/list.h>
#include <linux/types.h>

/*
 * Deterministic automaton per-object variables.
 */
struct da_monitor {
	bool		monitoring;
	unsigned int	curr_state;
};

#ifdef CONFIG_RV_LTL_MONITOR

/*
 * In the future, if the number of atomic propositions or the size of Buchi
 * automaton is larger, we can switch to dynamic allocation. For now, the code
 * is simpler this way.
 */
#define RV_MAX_LTL_ATOM 32
#define RV_MAX_BA_STATES 32

/**
 * struct ltl_monitor - A linear temporal logic runtime verification monitor
 * @states:	States in the Buchi automaton. As Buchi automaton is a
 *		non-deterministic state machine, the monitor can be in multiple
 *		states simultaneously. This is a bitmask of all possible states.
 *		If this is zero, that means either:
 *		    - The monitor has not started yet (e.g. because not all
 *		      atomic propositions are known).
 *		    - There is no possible state to be in. In other words, a
 *		      violation of the LTL property is detected.
 * @atoms:	The values of atomic propositions.
 * @unknown_atoms: Atomic propositions which are still unknown.
 */
struct ltl_monitor {
	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
};

static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
{
	for (int i = 0; i < ARRAY_SIZE(mon->states); ++i) {
		if (mon->states[i])
			return true;
	}
	return false;
}

static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
{
	for (int i = 0; i < ARRAY_SIZE(mon->unknown_atoms); ++i) {
		if (mon->unknown_atoms[i])
			return false;
	}
	return true;
}

#else

struct ltl_monitor {};

#endif /* CONFIG_RV_LTL_MONITOR */

#ifdef CONFIG_RV_HA_MONITOR
/*
 * In the future, hybrid automata may rely on multiple
 * environment variables, e.g. different clocks started at
 * different times or running at different speed.
 * For now we support only 1 variable.
 */
#define MAX_HA_ENV_LEN 1

/*
 * Monitors can pick the preferred timer implementation:
 * No timer: if monitors don't have state invariants.
 * Timer wheel: lightweight invariants check but far less precise.
 * Hrtimer: accurate invariants check with higher overhead.
 */
#define HA_TIMER_NONE 0
#define HA_TIMER_WHEEL 1
#define HA_TIMER_HRTIMER 2

/*
 * Hybrid automaton per-object variables.
 */
struct ha_monitor {
	struct da_monitor da_mon;
	u64 env_store[MAX_HA_ENV_LEN];
	union {
		struct hrtimer hrtimer;
		struct timer_list timer;
	};
};

#else

struct ha_monitor { };

#endif /* CONFIG_RV_HA_MONITOR */

#define RV_PER_TASK_MONITOR_INIT	(CONFIG_RV_PER_TASK_MONITORS)

union rv_task_monitor {
	struct da_monitor	da_mon;
	struct ltl_monitor	ltl_mon;
	struct ha_monitor	ha_mon;
};

#ifdef CONFIG_RV_REACTORS
struct rv_reactor {
	const char		*name;
	const char		*description;
	__printf(1, 0) void	(*react)(const char *msg, va_list args);
	struct list_head	list;
};
#endif

struct rv_monitor {
	const char		*name;
	const char		*description;
	bool			enabled;
	int			(*enable)(void);
	void			(*disable)(void);
	void			(*reset)(void);
#ifdef CONFIG_RV_REACTORS
	struct rv_reactor	*reactor;
	__printf(1, 0) void	(*react)(const char *msg, va_list args);
#endif
	struct list_head	list;
	struct rv_monitor	*parent;
	struct dentry		*root_d;
};

bool rv_monitoring_on(void);
int rv_unregister_monitor(struct rv_monitor *monitor);
int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
int rv_get_task_monitor_slot(void);
void rv_put_task_monitor_slot(int slot);

#ifdef CONFIG_RV_REACTORS
int rv_unregister_reactor(struct rv_reactor *reactor);
int rv_register_reactor(struct rv_reactor *reactor);
__printf(2, 3)
void rv_react(struct rv_monitor *monitor, const char *msg, ...);
#else
__printf(2, 3)
static inline void rv_react(struct rv_monitor *monitor, const char *msg, ...)
{
}
#endif /* CONFIG_RV_REACTORS */

#endif /* CONFIG_RV */
#endif /* _LINUX_RV_H */