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