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