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