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 automata 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 17 18class Dot2c(Automata): 19 enum_suffix = "" 20 enum_states_def = "states" 21 enum_events_def = "events" 22 struct_automaton_def = "automaton" 23 var_automaton_def = "aut" 24 25 def __init__(self, file_path, model_name=None): 26 super().__init__(file_path, model_name) 27 self.line_length = 100 28 29 def __buff_to_string(self, buff): 30 string = "" 31 32 for line in buff: 33 string = string + line + "\n" 34 35 # cut off the last \n 36 return string[:-1] 37 38 def __get_enum_states_content(self): 39 buff = [] 40 buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix)) 41 for state in self.states: 42 if state != self.initial_state: 43 buff.append("\t%s%s," % (state, self.enum_suffix)) 44 buff.append("\tstate_max%s" % (self.enum_suffix)) 45 46 return buff 47 48 def get_enum_states_string(self): 49 buff = self.__get_enum_states_content() 50 return self.__buff_to_string(buff) 51 52 def format_states_enum(self): 53 buff = [] 54 buff.append("enum %s {" % self.enum_states_def) 55 buff.append(self.get_enum_states_string()) 56 buff.append("};\n") 57 58 return buff 59 60 def __get_enum_events_content(self): 61 buff = [] 62 first = True 63 for event in self.events: 64 if first: 65 buff.append("\t%s%s = 0," % (event, self.enum_suffix)) 66 first = False 67 else: 68 buff.append("\t%s%s," % (event, self.enum_suffix)) 69 70 buff.append("\tevent_max%s" % self.enum_suffix) 71 72 return buff 73 74 def get_enum_events_string(self): 75 buff = self.__get_enum_events_content() 76 return self.__buff_to_string(buff) 77 78 def format_events_enum(self): 79 buff = [] 80 buff.append("enum %s {" % self.enum_events_def) 81 buff.append(self.get_enum_events_string()) 82 buff.append("};\n") 83 84 return buff 85 86 def get_minimun_type(self): 87 min_type = "unsigned char" 88 89 if self.states.__len__() > 255: 90 min_type = "unsigned short" 91 92 if self.states.__len__() > 65535: 93 min_type = "unsigned int" 94 95 if self.states.__len__() > 1000000: 96 raise Exception("Too many states: %d" % self.states.__len__()) 97 98 return min_type 99 100 def format_automaton_definition(self): 101 min_type = self.get_minimun_type() 102 buff = [] 103 buff.append("struct %s {" % self.struct_automaton_def) 104 buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix)) 105 buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix)) 106 buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix)) 107 buff.append("\t%s initial_state;" % min_type) 108 buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix)) 109 buff.append("};\n") 110 return buff 111 112 def format_aut_init_header(self): 113 buff = [] 114 buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def)) 115 return buff 116 117 def __get_string_vector_per_line_content(self, buff): 118 first = True 119 string = "" 120 for entry in buff: 121 if first: 122 string = string + "\t\t\"" + entry 123 first = False; 124 else: 125 string = string + "\",\n\t\t\"" + entry 126 string = string + "\"" 127 128 return string 129 130 def get_aut_init_events_string(self): 131 return self.__get_string_vector_per_line_content(self.events) 132 133 def get_aut_init_states_string(self): 134 return self.__get_string_vector_per_line_content(self.states) 135 136 def format_aut_init_events_string(self): 137 buff = [] 138 buff.append("\t.event_names = {") 139 buff.append(self.get_aut_init_events_string()) 140 buff.append("\t},") 141 return buff 142 143 def format_aut_init_states_string(self): 144 buff = [] 145 buff.append("\t.state_names = {") 146 buff.append(self.get_aut_init_states_string()) 147 buff.append("\t},") 148 149 return buff 150 151 def __get_max_strlen_of_states(self): 152 max_state_name = max(self.states, key = len).__len__() 153 return max(max_state_name, self.invalid_state_str.__len__()) 154 155 def get_aut_init_function(self): 156 nr_states = self.states.__len__() 157 nr_events = self.events.__len__() 158 buff = [] 159 160 maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) 161 tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" 162 comma_space = 2 # ", " count last comma here 163 linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length 164 for x in range(nr_states): 165 line = "\t\t{\n" if linetoolong else "\t\t{ " 166 for y in range(nr_events): 167 next_state = self.function[x][y] 168 if next_state != self.invalid_state_str: 169 next_state = self.function[x][y] + self.enum_suffix 170 171 if linetoolong: 172 line += "\t\t\t%s" % next_state 173 else: 174 line += "%*s" % (maxlen, next_state) 175 if y != nr_events-1: 176 line += ",\n" if linetoolong else ", " 177 else: 178 line += "\n\t\t}," if linetoolong else " }," 179 buff.append(line) 180 181 return self.__buff_to_string(buff) 182 183 def format_aut_init_function(self): 184 buff = [] 185 buff.append("\t.function = {") 186 buff.append(self.get_aut_init_function()) 187 buff.append("\t},") 188 189 return buff 190 191 def get_aut_init_initial_state(self): 192 return self.initial_state 193 194 def format_aut_init_initial_state(self): 195 buff = [] 196 initial_state = self.get_aut_init_initial_state() 197 buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",") 198 199 return buff 200 201 def get_aut_init_final_states(self): 202 line = "" 203 first = True 204 for state in self.states: 205 if first == False: 206 line = line + ', ' 207 else: 208 first = False 209 210 if self.final_states.__contains__(state): 211 line = line + '1' 212 else: 213 line = line + '0' 214 return line 215 216 def format_aut_init_final_states(self): 217 buff = [] 218 buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states()) 219 220 return buff 221 222 def __get_automaton_initialization_footer_string(self): 223 footer = "};\n" 224 return footer 225 226 def format_aut_init_footer(self): 227 buff = [] 228 buff.append(self.__get_automaton_initialization_footer_string()) 229 230 return buff 231 232 def format_invalid_state(self): 233 buff = [] 234 buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix)) 235 236 return buff 237 238 def format_model(self): 239 buff = [] 240 buff += self.format_states_enum() 241 buff += self.format_invalid_state() 242 buff += self.format_events_enum() 243 buff += self.format_automaton_definition() 244 buff += self.format_aut_init_header() 245 buff += self.format_aut_init_states_string() 246 buff += self.format_aut_init_events_string() 247 buff += self.format_aut_init_function() 248 buff += self.format_aut_init_initial_state() 249 buff += self.format_aut_init_final_states() 250 buff += self.format_aut_init_footer() 251 252 return buff 253 254 def print_model_classic(self): 255 buff = self.format_model() 256 print(self.__buff_to_string(buff)) 257