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