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