pagefault.h

 1/* SPDX-License-Identifier: GPL-2.0 */
 2
 3/*
 4 * C implementation of Buchi automaton, automatically generated by
 5 * tools/verification/rvgen from the linear temporal logic specification.
 6 * For further information, see kernel documentation:
 7 *   Documentation/trace/rv/linear_temporal_logic.rst
 8 */
 9
10#include <linux/rv.h>
11
12#define MONITOR_NAME pagefault
13
14enum ltl_atom {
15	LTL_PAGEFAULT,
16	LTL_RT,
17	LTL_NUM_ATOM
18};
19static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);
20
21static const char *ltl_atom_str(enum ltl_atom atom)
22{
23	static const char *const names[] = {
24		"pa",
25		"rt",
26	};
27
28	return names[atom];
29}
30
31enum ltl_buchi_state {
32	S0,
33	RV_NUM_BA_STATES
34};
35static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
36
37static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
38{
39	bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
40	bool val3 = !pagefault;
41	bool rt = test_bit(LTL_RT, mon->atoms);
42	bool val1 = !rt;
43	bool val4 = val1 || val3;
44
45	if (val4)
46		__set_bit(S0, mon->states);
47}
48
49static void
50ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
51{
52	bool pagefault = test_bit(LTL_PAGEFAULT, mon->atoms);
53	bool val3 = !pagefault;
54	bool rt = test_bit(LTL_RT, mon->atoms);
55	bool val1 = !rt;
56	bool val4 = val1 || val3;
57
58	switch (state) {
59	case S0:
60		if (val4)
61			__set_bit(S0, next);
62		break;
63	}
64}