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