verification/rvgen: Add support for Hybrid Automata

+5 -3

tools/verification/rvgen/__main__.py

··· 9 9 # Documentation/trace/rv/da_monitor_synthesis.rst 10 10 11 11 if __name__ == '__main__': 12 - from rvgen.dot2k import dot2k 12 + from rvgen.dot2k import da2k, ha2k 13 13 from rvgen.generator import Monitor 14 14 from rvgen.container import Container 15 15 from rvgen.ltl2k import ltl2k ··· 29 29 monitor_parser.add_argument("-p", "--parent", dest="parent", 30 30 required=False, help="Create a monitor nested to parent") 31 31 monitor_parser.add_argument('-c', "--class", dest="monitor_class", 32 - help="Monitor class, either \"da\" or \"ltl\"") 32 + help="Monitor class, either \"da\", \"ha\" or \"ltl\"") 33 33 monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file") 34 34 monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", 35 35 help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") ··· 43 43 if params.subcmd == "monitor": 44 44 print("Opening and parsing the specification file %s" % params.spec) 45 45 if params.monitor_class == "da": 46 - monitor = dot2k(params.spec, params.monitor_type, vars(params)) 46 + monitor = da2k(params.spec, params.monitor_type, vars(params)) 47 + elif params.monitor_class == "ha": 48 + monitor = ha2k(params.spec, params.monitor_type, vars(params)) 47 49 elif params.monitor_class == "ltl": 48 50 monitor = ltl2k(params.spec, params.monitor_type, vars(params)) 49 51 else:

+135 -9

tools/verification/rvgen/rvgen/automata.py

··· 9 9 # Documentation/trace/rv/deterministic_automata.rst 10 10 11 11 import ntpath 12 + import re 13 + from typing import Iterator 14 + 15 + class _ConstraintKey: 16 + """Base class for constraint keys.""" 17 + 18 + class _StateConstraintKey(_ConstraintKey, int): 19 + """Key for a state constraint. Under the hood just state_id.""" 20 + def __new__(cls, state_id: int): 21 + return super().__new__(cls, state_id) 22 + 23 + class _EventConstraintKey(_ConstraintKey, tuple): 24 + """Key for an event constraint. Under the hood just tuple(state_id,event_id).""" 25 + def __new__(cls, state_id: int, event_id: int): 26 + return super().__new__(cls, (state_id, event_id)) 12 27 13 28 class Automata: 14 29 """Automata class: Reads a dot file and part it as an automata. 30 + 31 + It supports both deterministic and hybrid automata. 15 32 16 33 Attributes: 17 34 dot_file: A dot file with an state_automaton definition. 18 35 """ 19 36 20 37 invalid_state_str = "INVALID_STATE" 38 + # val can be numerical, uppercase (constant or macro), lowercase (parameter or function) 39 + # only numerical values should have units 40 + constraint_rule = re.compile(r""" 41 + ^ 42 + (?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the env var 43 + (?P<op>[!<=>]{1,2}) # operator 44 + (?P<val> 45 + [0-9]+ | # numerical value 46 + [A-Z_]+\(\) | # macro 47 + [A-Z_]+ | # constant 48 + [a-z_]+\(\) | # function 49 + [a-z_]+ # parameter 50 + ) 51 + (?P<unit>[a-z]{1,2})? # optional unit for numerical values 52 + """, re.VERBOSE) 53 + constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA-Z0-9_]+)\)") 21 54 22 55 def __init__(self, file_path, model_name=None): 23 56 self.__dot_path = file_path 24 57 self.name = model_name or self.__get_model_name() 25 58 self.__dot_lines = self.__open_dot() 26 59 self.states, self.initial_state, self.final_states = self.__get_state_variables() 27 - self.events = self.__get_event_variables() 28 - self.function = self.__create_matrix() 60 + self.env_types = {} 61 + self.env_stored = set() 62 + self.constraint_vars = set() 63 + self.self_loop_reset_events = set() 64 + self.events, self.envs = self.__get_event_variables() 65 + self.function, self.constraints = self.__create_matrix() 29 66 self.events_start, self.events_start_run = self.__store_init_events() 67 + self.env_stored = sorted(self.env_stored) 68 + self.constraint_vars = sorted(self.constraint_vars) 69 + self.self_loop_reset_events = sorted(self.self_loop_reset_events) 30 70 31 71 def __get_model_name(self) -> str: 32 72 basename = ntpath.basename(self.__dot_path) ··· 156 116 157 117 return states, initial_state, final_states 158 118 159 - def __get_event_variables(self) -> list[str]: 119 + def __get_event_variables(self) -> tuple[list[str], list[str]]: 160 120 # here we are at the begin of transitions, take a note, we will return later. 161 121 cursor = self.__get_cursor_begin_events() 162 122 163 123 events = [] 124 + envs = [] 164 125 while self.__dot_lines[cursor].lstrip()[0] == '"': 165 126 # transitions have the format: 166 127 # "all_fired" -> "both_fired" [ label = "disable_irq" ]; 167 128 # ------------ event is here ------------^^^^^ 168 129 if self.__dot_lines[cursor].split()[1] == "->": 169 130 line = self.__dot_lines[cursor].split() 170 - event = "".join(line[line.index("label")+2:-1]).replace('"', '') 131 + event = "".join(line[line.index("label") + 2:-1]).replace('"', '') 171 132 172 133 # when a transition has more than one lables, they are like this 173 134 # "local_irq_enable\nhw_local_irq_enable_n" 174 135 # so split them. 175 136 176 137 for i in event.split("\\n"): 177 - events.append(i) 138 + # if the event contains a constraint (hybrid automata), 139 + # it will be separated by a ";": 140 + # "sched_switch;x<1000;reset(x)" 141 + ev, *constr = i.split(";") 142 + if constr: 143 + if len(constr) > 2: 144 + raise ValueError("Only 1 constraint and 1 reset are supported") 145 + envs += self.__extract_env_var(constr) 146 + events.append(ev) 147 + else: 148 + # state labels have the format: 149 + # "enable_fired" [label = "enable_fired\ncondition"]; 150 + # ----- label is here -----^^^^^ 151 + # label and node name must be the same, condition is optional 152 + state = self.__dot_lines[cursor].split("label")[1].split('"')[1] 153 + _, *constr = state.split("\\n") 154 + if constr: 155 + if len(constr) > 1: 156 + raise ValueError("Only 1 constraint is supported in the state") 157 + envs += self.__extract_env_var([constr[0].replace(" ", "")]) 178 158 cursor += 1 179 159 180 - return sorted(set(events)) 160 + return sorted(set(events)), sorted(set(envs)) 181 161 182 - def __create_matrix(self) -> list[list[str]]: 162 + def _split_constraint_expr(self, constr: list[str]) -> Iterator[tuple[str, 163 + str | None]]: 164 + """ 165 + Get a list of strings of the type constr1 && constr2 and returns a list of 166 + constraints and separators: [[constr1,"&&"],[constr2,None]] 167 + """ 168 + exprs = [] 169 + seps = [] 170 + for c in constr: 171 + while "&&" in c or "||" in c: 172 + a = c.find("&&") 173 + o = c.find("||") 174 + pos = a if o < 0 or 0 < a < o else o 175 + exprs.append(c[:pos].replace(" ", "")) 176 + seps.append(c[pos:pos + 2].replace(" ", "")) 177 + c = c[pos + 2:].replace(" ", "") 178 + exprs.append(c) 179 + seps.append(None) 180 + return zip(exprs, seps) 181 + 182 + def __extract_env_var(self, constraint: list[str]) -> list[str]: 183 + env = [] 184 + for c, _ in self._split_constraint_expr(constraint): 185 + rule = self.constraint_rule.search(c) 186 + reset = self.constraint_reset.search(c) 187 + if rule: 188 + env.append(rule["env"]) 189 + if rule.groupdict().get("unit"): 190 + self.env_types[rule["env"]] = rule["unit"] 191 + if rule["val"][0].isalpha(): 192 + self.constraint_vars.add(rule["val"]) 193 + # try to infer unit from constants or parameters 194 + val_for_unit = rule["val"].lower().replace("()", "") 195 + if val_for_unit.endswith("_ns"): 196 + self.env_types[rule["env"]] = "ns" 197 + if val_for_unit.endswith("_jiffies"): 198 + self.env_types[rule["env"]] = "j" 199 + if reset: 200 + env.append(reset["env"]) 201 + # environment variables that are reset need a storage 202 + self.env_stored.add(reset["env"]) 203 + return env 204 + 205 + def __create_matrix(self) -> tuple[list[list[str]], dict[_ConstraintKey, list[str]]]: 183 206 # transform the array into a dictionary 184 207 events = self.events 185 208 states = self.states ··· 260 157 261 158 # declare the matrix.... 262 159 matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)] 160 + constraints: dict[_ConstraintKey, list[str]] = {} 263 161 264 162 # and we are back! Let's fill the matrix 265 163 cursor = self.__get_cursor_begin_events() ··· 270 166 line = self.__dot_lines[cursor].split() 271 167 origin_state = line[0].replace('"','').replace(',','_') 272 168 dest_state = line[2].replace('"','').replace(',','_') 273 - possible_events = "".join(line[line.index("label")+2:-1]).replace('"', '') 169 + possible_events = "".join(line[line.index("label") + 2:-1]).replace('"', '') 274 170 for event in possible_events.split("\\n"): 171 + event, *constr = event.split(";") 172 + if constr: 173 + key = _EventConstraintKey(states_dict[origin_state], events_dict[event]) 174 + constraints[key] = constr 175 + # those events reset also on self loops 176 + if origin_state == dest_state and "reset" in "".join(constr): 177 + self.self_loop_reset_events.add(event) 275 178 matrix[states_dict[origin_state]][events_dict[event]] = dest_state 179 + else: 180 + state = self.__dot_lines[cursor].split("label")[1].split('"')[1] 181 + state, *constr = state.replace(" ", "").split("\\n") 182 + if constr: 183 + constraints[_StateConstraintKey(states_dict[state])] = constr 276 184 cursor += 1 277 185 278 - return matrix 186 + return matrix, constraints 279 187 280 188 def __store_init_events(self) -> tuple[list[bool], list[bool]]: 281 189 events_start = [False] * len(self.events) ··· 319 203 if any(self.events_start): 320 204 return False 321 205 return self.events_start_run[self.events.index(event)] 206 + 207 + def is_hybrid_automata(self) -> bool: 208 + return bool(self.envs) 209 + 210 + def is_event_constraint(self, key: _ConstraintKey) -> bool: 211 + """ 212 + Given the key in self.constraints return true if it is an event 213 + constraint, false if it is a state constraint 214 + """ 215 + return isinstance(key, _EventConstraintKey)

+47

tools/verification/rvgen/rvgen/dot2c.py

··· 19 19 enum_suffix = "" 20 20 enum_states_def = "states" 21 21 enum_events_def = "events" 22 + enum_envs_def = "envs" 22 23 struct_automaton_def = "automaton" 23 24 var_automaton_def = "aut" 24 25 ··· 62 61 63 62 return buff 64 63 64 + def __get_non_stored_envs(self) -> list[str]: 65 + return [e for e in self.envs if e not in self.env_stored] 66 + 67 + def __get_enum_envs_content(self) -> list[str]: 68 + buff = [] 69 + # We first place env variables that have a u64 storage. 70 + # Those are limited by MAX_HA_ENV_LEN, other variables 71 + # are read only and don't require a storage. 72 + unstored = self.__get_non_stored_envs() 73 + for env in list(self.env_stored) + unstored: 74 + buff.append(f"\t{env}{self.enum_suffix},") 75 + 76 + buff.append(f"\tenv_max{self.enum_suffix},") 77 + max_stored = unstored[0] if len(unstored) else "env_max" 78 + buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},") 79 + 80 + return buff 81 + 82 + def format_envs_enum(self) -> list[str]: 83 + buff = [] 84 + if self.is_hybrid_automata(): 85 + buff.append(f"enum {self.enum_envs_def} {{") 86 + buff += self.__get_enum_envs_content() 87 + buff.append("};\n") 88 + buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN," 89 + ' "Not enough slots");') 90 + if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()): 91 + buff.append("#define HA_CLK_NS") 92 + buff.append("") 93 + return buff 94 + 65 95 def get_minimun_type(self) -> str: 66 96 min_type = "unsigned char" 67 97 ··· 113 81 buff.append("struct %s {" % self.struct_automaton_def) 114 82 buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix)) 115 83 buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix)) 84 + if self.is_hybrid_automata(): 85 + buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];") 116 86 buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix)) 117 87 buff.append("\t%s initial_state;" % min_type) 118 88 buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix)) ··· 144 110 buff.append("\t.state_names = {") 145 111 buff.append(self.__get_string_vector_per_line_content(self.states)) 146 112 buff.append("\t},") 113 + 114 + return buff 115 + 116 + def format_aut_init_envs_string(self) -> list[str]: 117 + buff = [] 118 + if self.is_hybrid_automata(): 119 + buff.append("\t.env_names = {") 120 + # maintain consistent order with the enum 121 + ordered_envs = list(self.env_stored) + self.__get_non_stored_envs() 122 + buff.append(self.__get_string_vector_per_line_content(ordered_envs)) 123 + buff.append("\t},") 147 124 148 125 return buff 149 126 ··· 250 205 buff += self.format_states_enum() 251 206 buff += self.format_invalid_state() 252 207 buff += self.format_events_enum() 208 + buff += self.format_envs_enum() 253 209 buff += self.format_automaton_definition() 254 210 buff += self.format_aut_init_header() 255 211 buff += self.format_aut_init_states_string() 256 212 buff += self.format_aut_init_events_string() 213 + buff += self.format_aut_init_envs_string() 257 214 buff += self.format_aut_init_function() 258 215 buff += self.format_aut_init_initial_state() 259 216 buff += self.format_aut_init_final_states()

+472 -2

tools/verification/rvgen/rvgen/dot2k.py

··· 8 8 # For further information, see: 9 9 # Documentation/trace/rv/da_monitor_synthesis.rst 10 10 11 + from collections import deque 11 12 from .dot2c import Dot2c 12 13 from .generator import Monitor 14 + from .automata import _EventConstraintKey, _StateConstraintKey 13 15 14 16 15 17 class dot2k(Monitor, Dot2c): ··· 22 20 Monitor.__init__(self, extra_params) 23 21 Dot2c.__init__(self, file_path, extra_params.get("model_name")) 24 22 self.enum_suffix = "_%s" % self.name 23 + self.monitor_class = extra_params["monitor_class"] 25 24 26 25 def fill_monitor_type(self) -> str: 27 - return self.monitor_type.upper() 26 + buff = [ self.monitor_type.upper() ] 27 + buff += self._fill_timer_type() 28 + return "\n".join(buff) 28 29 29 30 def fill_tracepoint_handlers_skel(self) -> str: 30 31 buff = [] 32 + buff += self._fill_hybrid_definitions() 31 33 for event in self.events: 32 34 buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) 33 35 buff.append("{") ··· 83 77 # 84 78 self.enum_states_def = "states_%s" % self.name 85 79 self.enum_events_def = "events_%s" % self.name 80 + self.enum_envs_def = f"envs_{self.name}" 86 81 self.struct_automaton_def = "automaton_%s" % self.name 87 82 self.var_automaton_def = "automaton_%s" % self.name 88 83 ··· 114 107 ("char *", "state"), 115 108 ("char *", "event"), 116 109 ] 110 + tp_args_error_env = tp_args_error + [("char *", "env")] 111 + tp_args_dict = { 112 + "event": tp_args_event, 113 + "error": tp_args_error, 114 + "error_env": tp_args_error_env 115 + } 117 116 tp_args_id = ("int ", "id") 118 - tp_args = tp_args_event if tp_type == "event" else tp_args_error 117 + tp_args = tp_args_dict[tp_type] 119 118 if self.monitor_type == "per_task": 120 119 tp_args.insert(0, tp_args_id) 121 120 tp_proto_c = ", ".join([a+b for a,b in tp_args]) ··· 129 116 buff.append(" TP_PROTO(%s)," % tp_proto_c) 130 117 buff.append(" TP_ARGS(%s)" % tp_args_c) 131 118 return '\n'.join(buff) 119 + 120 + def _fill_hybrid_definitions(self) -> list: 121 + """Stub, not valid for deterministic automata""" 122 + return [] 123 + 124 + def _fill_timer_type(self) -> list: 125 + """Stub, not valid for deterministic automata""" 126 + return [] 132 127 133 128 def fill_main_c(self) -> str: 134 129 main_c = super().fill_main_c() ··· 148 127 main_c = main_c.replace("%%MIN_TYPE%%", min_type) 149 128 main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) 150 129 main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) 130 + main_c = main_c.replace("%%MONITOR_CLASS%%", self.monitor_class) 151 131 152 132 return main_c 133 + 134 + class da2k(dot2k): 135 + """Deterministic automata only""" 136 + def __init__(self, *args, **kwargs): 137 + super().__init__(*args, **kwargs) 138 + if self.is_hybrid_automata(): 139 + raise ValueError("Detected hybrid automata, use the 'ha' class") 140 + 141 + class ha2k(dot2k): 142 + """Hybrid automata only""" 143 + def __init__(self, *args, **kwargs): 144 + super().__init__(*args, **kwargs) 145 + if not self.is_hybrid_automata(): 146 + raise ValueError("Detected deterministic automata, use the 'da' class") 147 + self.trace_h = self._read_template_file("trace_hybrid.h") 148 + self.__parse_constraints() 149 + 150 + def fill_monitor_class_type(self) -> str: 151 + if self.monitor_type == "per_task": 152 + return "HA_MON_EVENTS_ID" 153 + return "HA_MON_EVENTS_IMPLICIT" 154 + 155 + def fill_monitor_class(self) -> str: 156 + """ 157 + Used for tracepoint classes, since they are shared we keep da 158 + instead of ha (also for the ha specific tracepoints). 159 + The tracepoint class is not visible to the tools. 160 + """ 161 + return super().fill_monitor_class() 162 + 163 + def __adjust_value(self, value: str | int, unit: str | None) -> str: 164 + """Adjust the value in ns""" 165 + try: 166 + value = int(value) 167 + except ValueError: 168 + # it's a constant, a parameter or a function 169 + if value.endswith("()"): 170 + return value.replace("()", "(ha_mon)") 171 + return value 172 + match unit: 173 + case "us": 174 + value *= 10**3 175 + case "ms": 176 + value *= 10**6 177 + case "s": 178 + value *= 10**9 179 + return str(value) + "ull" 180 + 181 + def __parse_single_constraint(self, rule: dict, value: str) -> str: 182 + return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, time_ns) {rule["op"]} {value}" 183 + 184 + def __get_constraint_env(self, constr: str) -> str: 185 + """Extract the second argument from an ha_ function""" 186 + env = constr.split("(")[1].split()[1].rstrip(")").rstrip(",") 187 + assert env.rstrip(f"_{self.name}") in self.envs 188 + return env 189 + 190 + def __start_to_invariant_check(self, constr: str) -> str: 191 + # by default assume the timer has ns expiration 192 + env = self.__get_constraint_env(constr) 193 + clock_type = "ns" 194 + if self.env_types.get(env.rstrip(f"_{self.name}")) == "j": 195 + clock_type = "jiffy" 196 + 197 + return f"return ha_check_invariant_{clock_type}(ha_mon, {env}, time_ns)" 198 + 199 + def __start_to_conv(self, constr: str) -> str: 200 + """ 201 + Undo the storage conversion done by ha_start_timer_ 202 + """ 203 + return "ha_inv_to_guard" + constr[constr.find("("):] 204 + 205 + def __parse_timer_constraint(self, rule: dict, value: str) -> str: 206 + # by default assume the timer has ns expiration 207 + clock_type = "ns" 208 + if self.env_types.get(rule["env"]) == "j": 209 + clock_type = "jiffy" 210 + 211 + return (f"ha_start_timer_{clock_type}(ha_mon, {rule["env"]}{self.enum_suffix}," 212 + f" {value}, time_ns)") 213 + 214 + def __format_guard_rules(self, rules: list[str]) -> list[str]: 215 + """ 216 + Merge guard constraints as a single C return statement. 217 + If the rules include a stored env, also check its validity. 218 + Break lines in a best effort way that tries to keep readability. 219 + """ 220 + if not rules: 221 + return [] 222 + 223 + invalid_checks = [f"ha_monitor_env_invalid(ha_mon, {env}{self.enum_suffix}) ||" 224 + for env in self.env_stored if any(env in rule for rule in rules)] 225 + if invalid_checks and len(rules) > 1: 226 + rules[0] = "(" + rules[0] 227 + rules[-1] = rules[-1] + ")" 228 + rules = invalid_checks + rules 229 + 230 + separator = "\n\t\t " if sum(len(r) for r in rules) > 80 else " " 231 + return ["res = " + separator.join(rules)] 232 + 233 + def __validate_constraint(self, key: tuple[int, int] | int, constr: str, 234 + rule, reset) -> None: 235 + # event constrains are tuples and allow both rules and reset 236 + # state constraints are only used for expirations (e.g. clk<N) 237 + if self.is_event_constraint(key): 238 + if not rule and not reset: 239 + raise ValueError("Unrecognised event constraint " 240 + f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})") 241 + if rule and (rule["env"] in self.env_types and 242 + rule["env"] not in self.env_stored): 243 + raise ValueError("Clocks in hybrid automata always require a storage" 244 + f" ({rule["env"]})") 245 + else: 246 + if not rule: 247 + raise ValueError("Unrecognised state constraint " 248 + f"({self.states[key]}: {constr})") 249 + if rule["env"] not in self.env_stored: 250 + raise ValueError("State constraints always require a storage " 251 + f"({rule["env"]})") 252 + if rule["op"] not in ["<", "<="]: 253 + raise ValueError("State constraints must be clock expirations like" 254 + f" clk<N ({rule.string})") 255 + 256 + def __parse_constraints(self) -> None: 257 + self.guards: dict[_EventConstraintKey, str] = {} 258 + self.invariants: dict[_StateConstraintKey, str] = {} 259 + for key, constraint in self.constraints.items(): 260 + rules = [] 261 + resets = [] 262 + for c, sep in self._split_constraint_expr(constraint): 263 + rule = self.constraint_rule.search(c) 264 + reset = self.constraint_reset.search(c) 265 + self.__validate_constraint(key, c, rule, reset) 266 + if rule: 267 + value = rule["val"] 268 + value_len = len(rule["val"]) 269 + unit = None 270 + if rule.groupdict().get("unit"): 271 + value_len += len(rule["unit"]) 272 + unit = rule["unit"] 273 + c = c[:-(value_len)] 274 + value = self.__adjust_value(value, unit) 275 + if self.is_event_constraint(key): 276 + c = self.__parse_single_constraint(rule, value) 277 + if sep: 278 + c += f" {sep}" 279 + else: 280 + c = self.__parse_timer_constraint(rule, value) 281 + rules.append(c) 282 + if reset: 283 + c = f"ha_reset_env(ha_mon, {reset["env"]}{self.enum_suffix}, time_ns)" 284 + resets.append(c) 285 + if self.is_event_constraint(key): 286 + res = self.__format_guard_rules(rules) + resets 287 + self.guards[key] = ";".join(res) 288 + else: 289 + self.invariants[key] = rules[0] 290 + 291 + def __fill_verify_invariants_func(self) -> list[str]: 292 + buff = [] 293 + if not self.invariants: 294 + return [] 295 + 296 + buff.append( 297 + f"""static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, 298 + \t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, 299 + \t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) 300 + {{""") 301 + 302 + _else = "" 303 + for state, constr in sorted(self.invariants.items()): 304 + check_str = self.__start_to_invariant_check(constr) 305 + buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})") 306 + buff.append(f"\t\t{check_str};") 307 + _else = "else " 308 + 309 + buff.append("\treturn true;\n}\n") 310 + return buff 311 + 312 + def __fill_convert_inv_guard_func(self) -> list[str]: 313 + buff = [] 314 + if not self.invariants: 315 + return [] 316 + 317 + conflict_guards, conflict_invs = self.__find_inv_conflicts() 318 + if not conflict_guards and not conflict_invs: 319 + return [] 320 + 321 + buff.append( 322 + f"""static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon, 323 + \t\t\t\t\tenum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, 324 + \t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) 325 + {{""") 326 + buff.append("\tif (curr_state == next_state)\n\t\treturn;") 327 + 328 + _else = "" 329 + for state, constr in sorted(self.invariants.items()): 330 + # a state with invariant can reach us without reset 331 + # multiple conflicts must have the same invariant, otherwise we cannot 332 + # know how to reset the value 333 + conf_i = [start for start, end in conflict_invs if end == state] 334 + # we can reach a guard without reset 335 + conf_g = [e for s, e in conflict_guards if s == state] 336 + if not conf_i and not conf_g: 337 + continue 338 + buff.append(f"\t{_else}if (curr_state == {self.states[state]}{self.enum_suffix})") 339 + 340 + buff.append(f"\t\t{self.__start_to_conv(constr)};") 341 + _else = "else " 342 + 343 + buff.append("}\n") 344 + return buff 345 + 346 + def __fill_verify_guards_func(self) -> list[str]: 347 + buff = [] 348 + if not self.guards: 349 + return [] 350 + 351 + buff.append( 352 + f"""static inline bool ha_verify_guards(struct ha_monitor *ha_mon, 353 + \t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, 354 + \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) 355 + {{ 356 + \tbool res = true; 357 + """) 358 + 359 + _else = "" 360 + for edge, constr in sorted(self.guards.items()): 361 + buff.append(f"\t{_else}if (curr_state == " 362 + f"{self.states[edge[0]]}{self.enum_suffix} && " 363 + f"event == {self.events[edge[1]]}{self.enum_suffix})") 364 + if constr.count(";") > 0: 365 + buff[-1] += " {" 366 + buff += [f"\t\t{c};" for c in constr.split(";")] 367 + if constr.count(";") > 0: 368 + _else = "} else " 369 + else: 370 + _else = "else " 371 + if _else[0] == "}": 372 + buff.append("\t}") 373 + buff.append("\treturn res;\n}\n") 374 + return buff 375 + 376 + def __find_inv_conflicts(self) -> tuple[set[tuple[int, _EventConstraintKey]], 377 + set[tuple[int, _StateConstraintKey]]]: 378 + """ 379 + Run a breadth first search from all states with an invariant. 380 + Find any conflicting constraints reachable from there, this can be 381 + another state with an invariant or an edge with a non-reset guard. 382 + Stop when we find a reset. 383 + 384 + Return the set of conflicting guards and invariants as tuples of 385 + conflicting state and constraint key. 386 + """ 387 + conflict_guards: set[tuple[int, _EventConstraintKey]] = set() 388 + conflict_invs: set[tuple[int, _StateConstraintKey]] = set() 389 + for start_idx in self.invariants: 390 + queue = deque([(start_idx, 0)]) # (state_idx, distance) 391 + env = self.__get_constraint_env(self.invariants[start_idx]) 392 + 393 + while queue: 394 + curr_idx, distance = queue.popleft() 395 + 396 + # Check state condition 397 + if curr_idx != start_idx and curr_idx in self.invariants: 398 + conflict_invs.add((start_idx, _StateConstraintKey(curr_idx))) 399 + continue 400 + 401 + # Check if we should stop 402 + if distance > len(self.states): 403 + break 404 + if curr_idx != start_idx and distance > 1: 405 + continue 406 + 407 + for event_idx, next_state_name in enumerate(self.function[curr_idx]): 408 + if next_state_name == self.invalid_state_str: 409 + continue 410 + curr_guard = self.guards.get((curr_idx, event_idx), "") 411 + if "reset" in curr_guard and env in curr_guard: 412 + continue 413 + 414 + if env in curr_guard: 415 + conflict_guards.add((start_idx, 416 + _EventConstraintKey(curr_idx, event_idx))) 417 + continue 418 + 419 + next_idx = self.states.index(next_state_name) 420 + queue.append((next_idx, distance + 1)) 421 + 422 + return conflict_guards, conflict_invs 423 + 424 + def __fill_setup_invariants_func(self) -> list[str]: 425 + buff = [] 426 + if not self.invariants: 427 + return [] 428 + 429 + buff.append( 430 + f"""static inline void ha_setup_invariants(struct ha_monitor *ha_mon, 431 + \t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, 432 + \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) 433 + {{""") 434 + 435 + conditions = ["next_state == curr_state"] 436 + conditions += [f"event != {e}{self.enum_suffix}" 437 + for e in self.self_loop_reset_events] 438 + condition_str = " && ".join(conditions) 439 + buff.append(f"\tif ({condition_str})\n\t\treturn;") 440 + 441 + _else = "" 442 + for state, constr in sorted(self.invariants.items()): 443 + buff.append(f"\t{_else}if (next_state == {self.states[state]}{self.enum_suffix})") 444 + buff.append(f"\t\t{constr};") 445 + _else = "else " 446 + 447 + for state in self.invariants: 448 + buff.append(f"\telse if (curr_state == {self.states[state]}{self.enum_suffix})") 449 + buff.append("\t\tha_cancel_timer(ha_mon);") 450 + 451 + buff.append("}\n") 452 + return buff 453 + 454 + def __fill_constr_func(self) -> list[str]: 455 + buff = [] 456 + if not self.constraints: 457 + return [] 458 + 459 + buff.append( 460 + """/* 461 + * These functions are used to validate state transitions. 462 + * 463 + * They are generated by parsing the model, there is usually no need to change them. 464 + * If the monitor requires a timer, there are functions responsible to arm it when 465 + * the next state has a constraint, cancel it in any other case and to check 466 + * that it didn't expire before the callback run. Transitions to the same state 467 + * without a reset never affect timers. 468 + * Due to the different representations between invariants and guards, there is 469 + * a function to convert it in case invariants or guards are reachable from 470 + * another invariant without reset. Those are not present if not required in 471 + * the model. This is all automatic but is worth checking because it may show 472 + * errors in the model (e.g. missing resets). 473 + */""") 474 + 475 + buff += self.__fill_verify_invariants_func() 476 + inv_conflicts = self.__fill_convert_inv_guard_func() 477 + buff += inv_conflicts 478 + buff += self.__fill_verify_guards_func() 479 + buff += self.__fill_setup_invariants_func() 480 + 481 + buff.append( 482 + f"""static bool ha_verify_constraint(struct ha_monitor *ha_mon, 483 + \t\t\t\t enum {self.enum_states_def} curr_state, enum {self.enum_events_def} event, 484 + \t\t\t\t enum {self.enum_states_def} next_state, u64 time_ns) 485 + {{""") 486 + 487 + if self.invariants: 488 + buff.append("\tif (!ha_verify_invariants(ha_mon, curr_state, " 489 + "event, next_state, time_ns))\n\t\treturn false;\n") 490 + if inv_conflicts: 491 + buff.append("\tha_convert_inv_guard(ha_mon, curr_state, event, " 492 + "next_state, time_ns);\n") 493 + 494 + if self.guards: 495 + buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, event, " 496 + "next_state, time_ns))\n\t\treturn false;\n") 497 + 498 + if self.invariants: 499 + buff.append("\tha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns);\n") 500 + 501 + buff.append("\treturn true;\n}\n") 502 + return buff 503 + 504 + def __fill_env_getter(self, env: str) -> str: 505 + if env in self.env_types: 506 + match self.env_types[env]: 507 + case "ns" | "us" | "ms" | "s": 508 + return "ha_get_clk_ns(ha_mon, env, time_ns);" 509 + case "j": 510 + return "ha_get_clk_jiffy(ha_mon, env);" 511 + return f"/* XXX: how do I read {env}? */" 512 + 513 + def __fill_env_resetter(self, env: str) -> str: 514 + if env in self.env_types: 515 + match self.env_types[env]: 516 + case "ns" | "us" | "ms" | "s": 517 + return "ha_reset_clk_ns(ha_mon, env, time_ns);" 518 + case "j": 519 + return "ha_reset_clk_jiffy(ha_mon, env);" 520 + return f"/* XXX: how do I reset {env}? */" 521 + 522 + def __fill_hybrid_get_reset_functions(self) -> list[str]: 523 + buff = [] 524 + if self.is_hybrid_automata(): 525 + for var in self.constraint_vars: 526 + if var.endswith("()"): 527 + func_name = var.replace("()", "") 528 + if func_name.isupper(): 529 + buff.append(f"#define {func_name}(ha_mon) " 530 + f"/* XXX: what is {func_name}(ha_mon)? */\n") 531 + else: 532 + buff.append(f"static inline u64 {func_name}(struct ha_monitor *ha_mon)\n{{") 533 + buff.append(f"\treturn /* XXX: what is {func_name}(ha_mon)? */;") 534 + buff.append("}\n") 535 + elif var.isupper(): 536 + buff.append(f"#define {var} /* XXX: what is {var}? */\n") 537 + else: 538 + buff.append(f"static u64 {var} = /* XXX: default value */;") 539 + buff.append(f"module_param({var}, ullong, 0644);\n") 540 + buff.append("""/* 541 + * These functions define how to read and reset the environment variable. 542 + * 543 + * Common environment variables like ns-based and jiffy-based clocks have 544 + * pre-define getters and resetters you can use. The parser can infer the type 545 + * of the environment variable if you supply a measure unit in the constraint. 546 + * If you define your own functions, make sure to add appropriate memory 547 + * barriers if required. 548 + * Some environment variables don't require a storage as they read a system 549 + * state (e.g. preemption count). Those variables are never reset, so we don't 550 + * define a reset function on monitors only relying on this type of variables. 551 + */""") 552 + buff.append("static u64 ha_get_env(struct ha_monitor *ha_mon, " 553 + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") 554 + _else = "" 555 + for env in self.envs: 556 + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") 557 + buff.append(f"\t\treturn {self.__fill_env_getter(env)}") 558 + _else = "else " 559 + buff.append("\treturn ENV_INVALID_VALUE;\n}\n") 560 + if len(self.env_stored): 561 + buff.append("static void ha_reset_env(struct ha_monitor *ha_mon, " 562 + f"enum envs{self.enum_suffix} env, u64 time_ns)\n{{") 563 + _else = "" 564 + for env in self.env_stored: 565 + buff.append(f"\t{_else}if (env == {env}{self.enum_suffix})") 566 + buff.append(f"\t\t{self.__fill_env_resetter(env)}") 567 + _else = "else " 568 + buff.append("}\n") 569 + return buff 570 + 571 + def _fill_hybrid_definitions(self) -> list[str]: 572 + return self.__fill_hybrid_get_reset_functions() + self.__fill_constr_func() 573 + 574 + def _fill_timer_type(self) -> list: 575 + if self.invariants: 576 + return [ 577 + "/* XXX: If the monitor has several instances, consider HA_TIMER_WHEEL */", 578 + "#define HA_TIMER_TYPE HA_TIMER_HRTIMER" 579 + ] 580 + return []

+2

tools/verification/rvgen/rvgen/generator.py

··· 255 255 monitor_class_type = self.fill_monitor_class_type() 256 256 tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") 257 257 tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") 258 + tracepoint_args_skel_error_env = self.fill_tracepoint_args_skel("error_env") 258 259 trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) 259 260 trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) 260 261 trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) 261 262 trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) 262 263 trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) 263 264 trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) 265 + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%", tracepoint_args_skel_error_env) 264 266 return trace_h 265 267 266 268 def print_files(self):

+1 -1

tools/verification/rvgen/rvgen/templates/dot2k/main.c

··· 21 21 */ 22 22 #define RV_MON_TYPE RV_MON_%%MONITOR_TYPE%% 23 23 #include "%%MODEL_NAME%%.h" 24 - #include <rv/da_monitor.h> 24 + #include <rv/%%MONITOR_CLASS%%_monitor.h> 25 25 26 26 /* 27 27 * This is the instrumentation part of the monitor.

+16

tools/verification/rvgen/rvgen/templates/dot2k/trace_hybrid.h

··· 1 + /* SPDX-License-Identifier: GPL-2.0 */ 2 + 3 + /* 4 + * Snippet to be included in rv_trace.h 5 + */ 6 + 7 + #ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% 8 + DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, 9 + %%TRACEPOINT_ARGS_SKEL_EVENT%%); 10 + 11 + DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, 12 + %%TRACEPOINT_ARGS_SKEL_ERROR%%); 13 + 14 + DEFINE_EVENT(error_env_%%MONITOR_CLASS%%, error_env_%%MODEL_NAME%%, 15 + %%TRACEPOINT_ARGS_SKEL_ERROR_ENV%%); 16 + #endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */

Configure Feed

Configure Feed