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 */
22 struct 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 */
50 struct 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
rv_ltl_valid_state(struct ltl_monitor * mon)56 static 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
rv_ltl_all_atoms_known(struct ltl_monitor * mon)65 static 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
76 struct ltl_monitor {};
77
78 #endif /* CONFIG_RV_LTL_MONITOR */
79
80 #define RV_PER_TASK_MONITOR_INIT (CONFIG_RV_PER_TASK_MONITORS)
81
82 union rv_task_monitor {
83 struct da_monitor da_mon;
84 struct ltl_monitor ltl_mon;
85 };
86
87 #ifdef CONFIG_RV_REACTORS
88 struct rv_reactor {
89 const char *name;
90 const char *description;
91 __printf(1, 2) void (*react)(const char *msg, ...);
92 struct list_head list;
93 };
94 #endif
95
96 struct 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, 2) void (*react)(const char *msg, ...);
106 #endif
107 struct list_head list;
108 struct rv_monitor *parent;
109 struct dentry *root_d;
110 };
111
112 bool rv_monitoring_on(void);
113 int rv_unregister_monitor(struct rv_monitor *monitor);
114 int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *parent);
115 int rv_get_task_monitor_slot(void);
116 void rv_put_task_monitor_slot(int slot);
117
118 #ifdef CONFIG_RV_REACTORS
119 bool rv_reacting_on(void);
120 int rv_unregister_reactor(struct rv_reactor *reactor);
121 int rv_register_reactor(struct rv_reactor *reactor);
122 #else
rv_reacting_on(void)123 static inline bool rv_reacting_on(void)
124 {
125 return false;
126 }
127 #endif /* CONFIG_RV_REACTORS */
128
129 #endif /* CONFIG_RV */
130 #endif /* _LINUX_RV_H */
131