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 dot2.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):
 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))