1#!/usr/bin/env python3 2# SPDX-License-Identifier: GPL-2.0-only 3# 4# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> 5# 6# dot2c: parse an automaton in dot file digraph format into a C 7# 8# This program was written in the development of this paper: 9# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S. 10# "Efficient Formal Verification for the Linux Kernel." International 11# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. 12# 13# For further information, see: 14# Documentation/trace/rv/deterministic_automata.rst 15 16from .automata import Automata, AutomataError 17 18class Dot2c(Automata): 19 enum_suffix = "" 20 enum_states_def = "states" 21 enum_events_def = "events" 22 enum_envs_def = "envs" 23 struct_automaton_def = "automaton" 24 var_automaton_def = "aut" 25 26 def __init__(self, file_path, model_name=None): 27 super().__init__(file_path, model_name) 28 self.line_length = 100 29 30 def __get_enum_states_content(self) -> list[str]: 31 buff = [] 32 buff.append(f"\t{self.initial_state}{self.enum_suffix},") 33 for state in self.states: 34 if state != self.initial_state: 35 buff.append(f"\t{state}{self.enum_suffix},") 36 buff.append(f"\tstate_max{self.enum_suffix},") 37 38 return buff 39 40 def format_states_enum(self) -> list[str]: 41 buff = [] 42 buff.append(f"enum {self.enum_states_def} {{") 43 buff += self.__get_enum_states_content() 44 buff.append("};\n") 45 46 return buff 47 48 def __get_enum_events_content(self) -> list[str]: 49 buff = [] 50 for event in self.events: 51 buff.append(f"\t{event}{self.enum_suffix},") 52 53 buff.append(f"\tevent_max{self.enum_suffix},") 54 55 return buff 56 57 def format_events_enum(self) -> list[str]: 58 buff = [] 59 buff.append(f"enum {self.enum_events_def} {{") 60 buff += self.__get_enum_events_content() 61 buff.append("};\n") 62 63 return buff 64 65 def __get_non_stored_envs(self) -> list[str]: 66 return [e for e in self.envs if e not in self.env_stored] 67 68 def __get_enum_envs_content(self) -> list[str]: 69 buff = [] 70 # We first place env variables that have a u64 storage. 71 # Those are limited by MAX_HA_ENV_LEN, other variables 72 # are read only and don't require a storage. 73 unstored = self.__get_non_stored_envs() 74 for env in list(self.env_stored) + unstored: 75 buff.append(f"\t{env}{self.enum_suffix},") 76 77 buff.append(f"\tenv_max{self.enum_suffix},") 78 max_stored = unstored[0] if len(unstored) else "env_max" 79 buff.append(f"\tenv_max_stored{self.enum_suffix} = {max_stored}{self.enum_suffix},") 80 81 return buff 82 83 def format_envs_enum(self) -> list[str]: 84 buff = [] 85 if self.is_hybrid_automata(): 86 buff.append(f"enum {self.enum_envs_def} {{") 87 buff += self.__get_enum_envs_content() 88 buff.append("};\n") 89 buff.append(f"_Static_assert(env_max_stored{self.enum_suffix} <= MAX_HA_ENV_LEN," 90 ' "Not enough slots");') 91 if {"ns", "us", "ms", "s"}.intersection(self.env_types.values()): 92 buff.append("#define HA_CLK_NS") 93 buff.append("") 94 return buff 95 96 def get_minimun_type(self) -> str: 97 min_type = "unsigned char" 98 99 if len(self.states) > 255: 100 min_type = "unsigned short" 101 102 if len(self.states) > 65535: 103 min_type = "unsigned int" 104 105 if len(self.states) > 1000000: 106 raise AutomataError(f"Too many states: {len(self.states)}") 107 108 return min_type 109 110 def format_automaton_definition(self) -> list[str]: 111 min_type = self.get_minimun_type() 112 buff = [] 113 buff.append(f"struct {self.struct_automaton_def} {{") 114 buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];") 115 buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];") 116 if self.is_hybrid_automata(): 117 buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];") 118 buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];") 119 buff.append(f"\t{min_type} initial_state;") 120 buff.append(f"\tbool final_states[state_max{self.enum_suffix}];") 121 buff.append("};\n") 122 return buff 123 124 def format_aut_init_header(self) -> list[str]: 125 buff = [] 126 buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{") 127 return buff 128 129 def __get_string_vector_per_line_content(self, entries: list[str]) -> str: 130 buff = [] 131 for entry in entries: 132 buff.append(f"\t\t\"{entry}\",") 133 return "\n".join(buff) 134 135 def format_aut_init_events_string(self) -> list[str]: 136 buff = [] 137 buff.append("\t.event_names = {") 138 buff.append(self.__get_string_vector_per_line_content(self.events)) 139 buff.append("\t},") 140 return buff 141 142 def format_aut_init_states_string(self) -> list[str]: 143 buff = [] 144 buff.append("\t.state_names = {") 145 buff.append(self.__get_string_vector_per_line_content(self.states)) 146 buff.append("\t},") 147 148 return buff 149 150 def format_aut_init_envs_string(self) -> list[str]: 151 buff = [] 152 if self.is_hybrid_automata(): 153 buff.append("\t.env_names = {") 154 # maintain consistent order with the enum 155 ordered_envs = list(self.env_stored) + self.__get_non_stored_envs() 156 buff.append(self.__get_string_vector_per_line_content(ordered_envs)) 157 buff.append("\t},") 158 159 return buff 160 161 def __get_max_strlen_of_states(self) -> int: 162 max_state_name = len(max(self.states, key=len)) 163 return max(max_state_name, len(self.invalid_state_str)) 164 165 def get_aut_init_function(self) -> str: 166 nr_states = len(self.states) 167 nr_events = len(self.events) 168 buff = [] 169 170 maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) 171 tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" 172 comma_space = 2 # ", " count last comma here 173 linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length 174 for x in range(nr_states): 175 line = "\t\t{\n" if linetoolong else "\t\t{ " 176 for y in range(nr_events): 177 next_state = self.function[x][y] 178 if next_state != self.invalid_state_str: 179 next_state = self.function[x][y] + self.enum_suffix 180 181 if linetoolong: 182 line += f"\t\t\t{next_state}" 183 else: 184 line += f"{next_state:>{maxlen}}" 185 if y != nr_events - 1: 186 line += ",\n" if linetoolong else ", " 187 else: 188 line += ",\n\t\t}," if linetoolong else " }," 189 buff.append(line) 190 191 return '\n'.join(buff) 192 193 def format_aut_init_function(self) -> list[str]: 194 buff = [] 195 buff.append("\t.function = {") 196 buff.append(self.get_aut_init_function()) 197 buff.append("\t},") 198 199 return buff 200 201 def get_aut_init_initial_state(self) -> str: 202 return self.initial_state 203 204 def format_aut_init_initial_state(self) -> list[str]: 205 buff = [] 206 initial_state = self.get_aut_init_initial_state() 207 buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",") 208 209 return buff 210 211 def get_aut_init_final_states(self) -> str: 212 line = "" 213 first = True 214 for state in self.states: 215 if not first: 216 line = line + ', ' 217 else: 218 first = False 219 220 if state in self.final_states: 221 line = line + '1' 222 else: 223 line = line + '0' 224 return line 225 226 def format_aut_init_final_states(self) -> list[str]: 227 buff = [] 228 buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},") 229 230 return buff 231 232 def __get_automaton_initialization_footer_string(self) -> str: 233 footer = "};\n" 234 return footer 235 236 def format_aut_init_footer(self) -> list[str]: 237 buff = [] 238 buff.append(self.__get_automaton_initialization_footer_string()) 239 240 return buff 241 242 def format_invalid_state(self) -> list[str]: 243 buff = [] 244 buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n") 245 246 return buff 247 248 def format_model(self) -> list[str]: 249 buff = [] 250 buff += self.format_states_enum() 251 buff += self.format_invalid_state() 252 buff += self.format_events_enum() 253 buff += self.format_envs_enum() 254 buff += self.format_automaton_definition() 255 buff += self.format_aut_init_header() 256 buff += self.format_aut_init_states_string() 257 buff += self.format_aut_init_events_string() 258 buff += self.format_aut_init_envs_string() 259 buff += self.format_aut_init_function() 260 buff += self.format_aut_init_initial_state() 261 buff += self.format_aut_init_final_states() 262 buff += self.format_aut_init_footer() 263 264 return buff 265 266 def print_model_classic(self): 267 buff = self.format_model() 268 print('\n'.join(buff)) 269