~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

TOMOYO Linux Cross Reference
Linux/tools/verification/dot2/dot2c.py

Version: ~ [ linux-6.11.5 ] ~ [ linux-6.10.14 ] ~ [ linux-6.9.12 ] ~ [ linux-6.8.12 ] ~ [ linux-6.7.12 ] ~ [ linux-6.6.58 ] ~ [ linux-6.5.13 ] ~ [ linux-6.4.16 ] ~ [ linux-6.3.13 ] ~ [ linux-6.2.16 ] ~ [ linux-6.1.114 ] ~ [ linux-6.0.19 ] ~ [ linux-5.19.17 ] ~ [ linux-5.18.19 ] ~ [ linux-5.17.15 ] ~ [ linux-5.16.20 ] ~ [ linux-5.15.169 ] ~ [ linux-5.14.21 ] ~ [ linux-5.13.19 ] ~ [ linux-5.12.19 ] ~ [ linux-5.11.22 ] ~ [ linux-5.10.228 ] ~ [ linux-5.9.16 ] ~ [ linux-5.8.18 ] ~ [ linux-5.7.19 ] ~ [ linux-5.6.19 ] ~ [ linux-5.5.19 ] ~ [ linux-5.4.284 ] ~ [ linux-5.3.18 ] ~ [ linux-5.2.21 ] ~ [ linux-5.1.21 ] ~ [ linux-5.0.21 ] ~ [ linux-4.20.17 ] ~ [ linux-4.19.322 ] ~ [ linux-4.18.20 ] ~ [ linux-4.17.19 ] ~ [ linux-4.16.18 ] ~ [ linux-4.15.18 ] ~ [ linux-4.14.336 ] ~ [ linux-4.13.16 ] ~ [ linux-4.12.14 ] ~ [ linux-4.11.12 ] ~ [ linux-4.10.17 ] ~ [ linux-4.9.337 ] ~ [ linux-4.4.302 ] ~ [ linux-3.10.108 ] ~ [ linux-2.6.32.71 ] ~ [ linux-2.6.0 ] ~ [ linux-2.4.37.11 ] ~ [ unix-v6-master ] ~ [ ccs-tools-1.8.9 ] ~ [ policy-sample ] ~
Architecture: ~ [ i386 ] ~ [ alpha ] ~ [ m68k ] ~ [ mips ] ~ [ ppc ] ~ [ sparc ] ~ [ sparc64 ] ~

  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))

~ [ source navigation ] ~ [ diff markup ] ~ [ identifier search ] ~

kernel.org | git.kernel.org | LWN.net | Project Home | SVN repository | Mail admin

Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.

sflogo.php