tools/verification/dot2/dot2c.py

   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
  16 from dot2.automata import Automata
  17
  18 class 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 = 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_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_suffix
 172
 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 buff
 188
 189     def get_aut_init_initial_state(self):
 190         return self.initial_state
 191
 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 buff
 198
 199     def get_aut_init_final_states(self):
 200         line = ""
 201         first = True
 202         for state in self.states:
 203             if first == False:
 204                 line = line + ', '
 205             else:
 206                 first = False
 207
 208             if self.final_states.__contains__(state):
 209                 line = line + '1'
 210             else:
 211                 line = line + '0'
 212         return line
 213
 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 buff
 219
 220     def __get_automaton_initialization_footer_string(self):
 221         footer = "};\n"
 222         return footer
 223
 224     def format_aut_init_footer(self):
 225         buff = []
 226         buff.append(self.__get_automaton_initialization_footer_string())
 227
 228         return buff
 229
 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 buff
 235
 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 buff
 251
 252     def print_model_classic(self):
 253         buff = self.format_model()
 254         print(self.__buff_to_string(buff))