255 lines · python
1#!/usr/bin/env python32# SPDX-License-Identifier: GPL-2.0-only3#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 C7#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." International11# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.12#13# For further information, see:14# Documentation/trace/rv/deterministic_automata.rst15 16from dot2.automata import Automata17 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):26 super().__init__(file_path)27 self.line_length = 10028 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 \n36 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 buff47 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 buff59 60 def __get_enum_events_content(self):61 buff = []62 first = True63 for event in self.events:64 if first:65 buff.append("\t%s%s = 0," % (event, self.enum_suffix))66 first = False67 else:68 buff.append("\t%s%s," % (event, self.enum_suffix))69 70 buff.append("\tevent_max%s" % self.enum_suffix)71 72 return buff73 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 buff85 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_type99 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 buff111 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 buff116 117 def __get_string_vector_per_line_content(self, buff):118 first = True119 string = ""120 for entry in buff:121 if first:122 string = string + "\t\t\"" + entry123 first = False;124 else:125 string = string + "\",\n\t\t\"" + entry126 string = string + "\""127 128 return string129 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 buff142 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 buff150 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_state_string_length(self):156 maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__()157 return "%" + str(maxlen) + "s"158 159 def get_aut_init_function(self):160 nr_states = self.states.__len__()161 nr_events = self.events.__len__()162 buff = []163 164 strformat = self.__get_state_string_length()165 166 for x in range(nr_states):167 line = "\t\t{ "168 for y in range(nr_events):169 next_state = self.function[x][y]170 if next_state != self.invalid_state_str:171 next_state = self.function[x][y] + self.enum_suffix172 173 if y != nr_events-1:174 line = line + strformat % next_state + ", "175 else:176 line = line + strformat % next_state + " },"177 buff.append(line)178 179 return self.__buff_to_string(buff)180 181 def format_aut_init_function(self):182 buff = []183 buff.append("\t.function = {")184 buff.append(self.get_aut_init_function())185 buff.append("\t},")186 187 return buff188 189 def get_aut_init_initial_state(self):190 return self.initial_state191 192 def format_aut_init_initial_state(self):193 buff = []194 initial_state = self.get_aut_init_initial_state()195 buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")196 197 return buff198 199 def get_aut_init_final_states(self):200 line = ""201 first = True202 for state in self.states:203 if first == False:204 line = line + ', '205 else:206 first = False207 208 if self.final_states.__contains__(state):209 line = line + '1'210 else:211 line = line + '0'212 return line213 214 def format_aut_init_final_states(self):215 buff = []216 buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())217 218 return buff219 220 def __get_automaton_initialization_footer_string(self):221 footer = "};\n"222 return footer223 224 def format_aut_init_footer(self):225 buff = []226 buff.append(self.__get_automaton_initialization_footer_string())227 228 return buff229 230 def format_invalid_state(self):231 buff = []232 buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix))233 234 return buff235 236 def format_model(self):237 buff = []238 buff += self.format_states_enum()239 buff += self.format_invalid_state()240 buff += self.format_events_enum()241 buff += self.format_automaton_definition()242 buff += self.format_aut_init_header()243 buff += self.format_aut_init_states_string()244 buff += self.format_aut_init_events_string()245 buff += self.format_aut_init_function()246 buff += self.format_aut_init_initial_state()247 buff += self.format_aut_init_final_states()248 buff += self.format_aut_init_footer()249 250 return buff251 252 def print_model_classic(self):253 buff = self.format_model()254 print(self.__buff_to_string(buff))255