verification/dot2/dot2c.py

0001 #!/usr/bin/env python3
0002 # SPDX-License-Identifier: GPL-2.0-only
0003 #
0004 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
0005 #
0006 # dot2c: parse an automata in dot file digraph format into a C
0007 #
0008 # This program was written in the development of this paper:
0009 #  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
0010 #  "Efficient Formal Verification for the Linux Kernel." International
0011 #  Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
0012 #
0013 # For further information, see:
0014 #   Documentation/trace/rv/deterministic_automata.rst
0015
0016 from dot2.automata import Automata
0017
0018 class Dot2c(Automata):
0019     enum_suffix = ""
0020     enum_states_def = "states"
0021     enum_events_def = "events"
0022     struct_automaton_def = "automaton"
0023     var_automaton_def = "aut"
0024
0025     def __init__(self, file_path):
0026         super().__init__(file_path)
0027         self.line_length = 100
0028
0029     def __buff_to_string(self, buff):
0030         string = ""
0031
0032         for line in buff:
0033             string = string + line + "\n"
0034
0035         # cut off the last \n
0036         return string[:-1]
0037
0038     def __get_enum_states_content(self):
0039         buff = []
0040         buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix))
0041         for state in self.states:
0042             if state != self.initial_state:
0043                 buff.append("\t%s%s," % (state, self.enum_suffix))
0044         buff.append("\tstate_max%s" % (self.enum_suffix))
0045
0046         return buff
0047
0048     def get_enum_states_string(self):
0049         buff = self.__get_enum_states_content()
0050         return self.__buff_to_string(buff)
0051
0052     def format_states_enum(self):
0053         buff = []
0054         buff.append("enum %s {" % self.enum_states_def)
0055         buff.append(self.get_enum_states_string())
0056         buff.append("};\n")
0057
0058         return buff
0059
0060     def __get_enum_events_content(self):
0061         buff = []
0062         first = True
0063         for event in self.events:
0064             if first:
0065                 buff.append("\t%s%s = 0," % (event, self.enum_suffix))
0066                 first = False
0067             else:
0068                 buff.append("\t%s%s," % (event, self.enum_suffix))
0069
0070         buff.append("\tevent_max%s" % self.enum_suffix)
0071
0072         return buff
0073
0074     def get_enum_events_string(self):
0075         buff = self.__get_enum_events_content()
0076         return self.__buff_to_string(buff)
0077
0078     def format_events_enum(self):
0079         buff = []
0080         buff.append("enum %s {" % self.enum_events_def)
0081         buff.append(self.get_enum_events_string())
0082         buff.append("};\n")
0083
0084         return buff
0085
0086     def get_minimun_type(self):
0087         min_type = "unsigned char"
0088
0089         if self.states.__len__() > 255:
0090             min_type = "unsigned short"
0091
0092         if self.states.__len__() > 65535:
0093             min_type = "unsigned int"
0094
0095         if self.states.__len__() > 1000000:
0096             raise Exception("Too many states: %d" % self.states.__len__())
0097
0098         return min_type
0099
0100     def format_automaton_definition(self):
0101         min_type = self.get_minimun_type()
0102         buff = []
0103         buff.append("struct %s {" % self.struct_automaton_def)
0104         buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
0105         buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
0106         buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix))
0107         buff.append("\t%s initial_state;" % min_type)
0108         buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
0109         buff.append("};\n")
0110         return buff
0111
0112     def format_aut_init_header(self):
0113         buff = []
0114         buff.append("struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
0115         return buff
0116
0117     def __get_string_vector_per_line_content(self, buff):
0118         first = True
0119         string = ""
0120         for entry in buff:
0121             if first:
0122                 string = string + "\t\t\"" + entry
0123                 first = False;
0124             else:
0125                 string = string + "\",\n\t\t\"" + entry
0126         string = string + "\""
0127
0128         return string
0129
0130     def get_aut_init_events_string(self):
0131         return self.__get_string_vector_per_line_content(self.events)
0132
0133     def get_aut_init_states_string(self):
0134         return self.__get_string_vector_per_line_content(self.states)
0135
0136     def format_aut_init_events_string(self):
0137         buff = []
0138         buff.append("\t.event_names = {")
0139         buff.append(self.get_aut_init_events_string())
0140         buff.append("\t},")
0141         return buff
0142
0143     def format_aut_init_states_string(self):
0144         buff = []
0145         buff.append("\t.state_names = {")
0146         buff.append(self.get_aut_init_states_string())
0147         buff.append("\t},")
0148
0149         return buff
0150
0151     def __get_max_strlen_of_states(self):
0152         max_state_name = max(self.states, key = len).__len__()
0153         return max(max_state_name, self.invalid_state_str.__len__())
0154
0155     def __get_state_string_length(self):
0156         maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__()
0157         return "%" + str(maxlen) + "s"
0158
0159     def get_aut_init_function(self):
0160         nr_states = self.states.__len__()
0161         nr_events = self.events.__len__()
0162         buff = []
0163
0164         strformat = self.__get_state_string_length()
0165
0166         for x in range(nr_states):
0167             line = "\t\t{ "
0168             for y in range(nr_events):
0169                 next_state = self.function[x][y]
0170                 if next_state != self.invalid_state_str:
0171                     next_state = self.function[x][y] + self.enum_suffix
0172
0173                 if y != nr_events-1:
0174                     line = line + strformat % next_state + ", "
0175                 else:
0176                     line = line + strformat % next_state + " },"
0177             buff.append(line)
0178
0179         return self.__buff_to_string(buff)
0180
0181     def format_aut_init_function(self):
0182         buff = []
0183         buff.append("\t.function = {")
0184         buff.append(self.get_aut_init_function())
0185         buff.append("\t},")
0186
0187         return buff
0188
0189     def get_aut_init_initial_state(self):
0190         return self.initial_state
0191
0192     def format_aut_init_initial_state(self):
0193         buff = []
0194         initial_state = self.get_aut_init_initial_state()
0195         buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")
0196
0197         return buff
0198
0199     def get_aut_init_final_states(self):
0200         line = ""
0201         first = True
0202         for state in self.states:
0203             if first == False:
0204                 line = line + ', '
0205             else:
0206                 first = False
0207
0208             if self.final_states.__contains__(state):
0209                 line = line + '1'
0210             else:
0211                 line = line + '0'
0212         return line
0213
0214     def format_aut_init_final_states(self):
0215        buff = []
0216        buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
0217
0218        return buff
0219
0220     def __get_automaton_initialization_footer_string(self):
0221         footer = "};\n"
0222         return footer
0223
0224     def format_aut_init_footer(self):
0225         buff = []
0226         buff.append(self.__get_automaton_initialization_footer_string())
0227
0228         return buff
0229
0230     def format_invalid_state(self):
0231         buff = []
0232         buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix))
0233
0234         return buff
0235
0236     def format_model(self):
0237         buff = []
0238         buff += self.format_states_enum()
0239         buff += self.format_invalid_state()
0240         buff += self.format_events_enum()
0241         buff += self.format_automaton_definition()
0242         buff += self.format_aut_init_header()
0243         buff += self.format_aut_init_states_string()
0244         buff += self.format_aut_init_events_string()
0245         buff += self.format_aut_init_function()
0246         buff += self.format_aut_init_initial_state()
0247         buff += self.format_aut_init_final_states()
0248         buff += self.format_aut_init_footer()
0249
0250         return buff
0251
0252     def print_model_classic(self):
0253         buff = self.format_model()
0254         print(self.__buff_to_string(buff))