1#!/usr/bin/awk -f
2# SPDX-License-Identifier: GPL-2.0
3
4# Modify SRCU for formal verification. The first argument should be srcu.h and
5# the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
6# current directory.
7
8BEGIN {
9	if (ARGC != 5) {
10		print "Usange: input.h input.c output.h output.c" > "/dev/stderr";
11		exit 1;
12	}
13	h_output = ARGV[3];
14	c_output = ARGV[4];
15	ARGC = 3;
16
17	# Tokenize using FS and not RS as FS supports regular expressions. Each
18	# record is one line of source, except that backslashed lines are
19	# combined. Comments are treated as field separators, as are quotes.
20	quote_regexp="\"([^\\\\\"]|\\\\.)*\"";
21	comment_regexp="\\/\\*([^*]|\\*+[^*/])*\\*\\/|\\/\\/.*(\n|$)";
22	FS="([ \\\\\t\n\v\f;,.=(){}+*/<>&|^-]|\\[|\\]|" comment_regexp "|" quote_regexp ")+";
23
24	inside_srcu_struct = 0;
25	inside_srcu_init_def = 0;
26	srcu_init_param_name = "";
27	in_macro = 0;
28	brace_nesting = 0;
29	paren_nesting = 0;
30
31	# Allow the manipulation of the last field separator after has been
32	# seen.
33	last_fs = "";
34	# Whether the last field separator was intended to be output.
35	last_fs_print = 0;
36
37	# rcu_batches stores the initialization for each instance of struct
38	# rcu_batch
39
40	in_comment = 0;
41
42	outputfile = "";
43}
44
45{
46	prev_outputfile = outputfile;
47	if (FILENAME ~ /\.h$/) {
48		outputfile = h_output;
49		if (FNR != NR) {
50			print "Incorrect file order" > "/dev/stderr";
51			exit 1;
52		}
53	}
54	else
55		outputfile = c_output;
56
57	if (prev_outputfile && outputfile != prev_outputfile) {
58		new_outputfile = outputfile;
59		outputfile = prev_outputfile;
60		update_fieldsep("", 0);
61		outputfile = new_outputfile;
62	}
63}
64
65# Combine the next line into $0.
66function combine_line() {
67	ret = getline next_line;
68	if (ret == 0) {
69		# Don't allow two consecutive getlines at the end of the file
70		if (eof_found) {
71			print "Error: expected more input." > "/dev/stderr";
72			exit 1;
73		} else {
74			eof_found = 1;
75		}
76	} else if (ret == -1) {
77		print "Error reading next line of file" FILENAME > "/dev/stderr";
78		exit 1;
79	}
80	$0 = $0 "\n" next_line;
81}
82
83# Combine backslashed lines and multiline comments.
84function combine_backslashes() {
85	while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
86		combine_line();
87	}
88}
89
90function read_line() {
91	combine_line();
92	combine_backslashes();
93}
94
95# Print out field separators and update variables that depend on them. Only
96# print if p is true. Call with sep="" and p=0 to print out the last field
97# separator.
98function update_fieldsep(sep, p) {
99	# Count braces
100	sep_tmp = sep;
101	gsub(quote_regexp "|" comment_regexp, "", sep_tmp);
102	while (1)
103	{
104		if (sub("[^{}()]*\\{", "", sep_tmp)) {
105			brace_nesting++;
106			continue;
107		}
108		if (sub("[^{}()]*\\}", "", sep_tmp)) {
109			brace_nesting--;
110			if (brace_nesting < 0) {
111				print "Unbalanced braces!" > "/dev/stderr";
112				exit 1;
113			}
114			continue;
115		}
116		if (sub("[^{}()]*\\(", "", sep_tmp)) {
117			paren_nesting++;
118			continue;
119		}
120		if (sub("[^{}()]*\\)", "", sep_tmp)) {
121			paren_nesting--;
122			if (paren_nesting < 0) {
123				print "Unbalanced parenthesis!" > "/dev/stderr";
124				exit 1;
125			}
126			continue;
127		}
128
129		break;
130	}
131
132	if (last_fs_print)
133		printf("%s", last_fs) > outputfile;
134	last_fs = sep;
135	last_fs_print = p;
136}
137
138# Shifts the fields down by n positions. Calls next if there are no more. If p
139# is true then print out field separators.
140function shift_fields(n, p) {
141	do {
142		if (match($0, FS) > 0) {
143			update_fieldsep(substr($0, RSTART, RLENGTH), p);
144			if (RSTART + RLENGTH <= length())
145				$0 = substr($0, RSTART + RLENGTH);
146			else
147				$0 = "";
148		} else {
149			update_fieldsep("", 0);
150			print "" > outputfile;
151			next;
152		}
153	} while (--n > 0);
154}
155
156# Shifts and prints the first n fields.
157function print_fields(n) {
158	do {
159		update_fieldsep("", 0);
160		printf("%s", $1) > outputfile;
161		shift_fields(1, 1);
162	} while (--n > 0);
163}
164
165{
166	combine_backslashes();
167}
168
169# Print leading FS
170{
171	if (match($0, "^(" FS ")+") > 0) {
172		update_fieldsep(substr($0, RSTART, RLENGTH), 1);
173		if (RSTART + RLENGTH <= length())
174			$0 = substr($0, RSTART + RLENGTH);
175		else
176			$0 = "";
177	}
178}
179
180# Parse the line.
181{
182	while (NF > 0) {
183		if ($1 == "struct" && NF < 3) {
184			read_line();
185			continue;
186		}
187
188		if (FILENAME ~ /\.h$/ && !inside_srcu_struct &&
189		    brace_nesting == 0 && paren_nesting == 0 &&
190		    $1 == "struct" && $2 == "srcu_struct" &&
191		    $0 ~ "^struct(" FS ")+srcu_struct(" FS ")+\\{") {
192			inside_srcu_struct = 1;
193			print_fields(2);
194			continue;
195		}
196		if (inside_srcu_struct && brace_nesting == 0 &&
197		    paren_nesting == 0) {
198			inside_srcu_struct = 0;
199			update_fieldsep("", 0);
200			for (name in rcu_batches)
201				print "extern struct rcu_batch " name ";" > outputfile;
202		}
203
204		if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") {
205			# Move rcu_batches outside of the struct.
206			rcu_batches[$3] = "";
207			shift_fields(3, 1);
208			sub(/;[[:space:]]*$/, "", last_fs);
209			continue;
210		}
211
212		if (FILENAME ~ /\.h$/ && !inside_srcu_init_def &&
213		    $1 == "#define" && $2 == "__SRCU_STRUCT_INIT") {
214			inside_srcu_init_def = 1;
215			srcu_init_param_name = $3;
216			in_macro = 1;
217			print_fields(3);
218			continue;
219		}
220		if (inside_srcu_init_def && brace_nesting == 0 &&
221		    paren_nesting == 0) {
222			inside_srcu_init_def = 0;
223			in_macro = 0;
224			continue;
225		}
226
227		if (inside_srcu_init_def && brace_nesting == 1 &&
228		    paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ &&
229		    $1 ~ /^[[:alnum:]_]+$/) {
230			name = $1;
231			if (name in rcu_batches) {
232				# Remove the dot.
233				sub(/\.[[:space:]]*$/, "", last_fs);
234
235				old_record = $0;
236				do
237					shift_fields(1, 0);
238				while (last_fs !~ /,/ || paren_nesting > 0);
239				end_loc = length(old_record) - length($0);
240				end_loc += index(last_fs, ",") - length(last_fs);
241
242				last_fs = substr(last_fs, index(last_fs, ",") + 1);
243				last_fs_print = 1;
244
245				match(old_record, "^"name"("FS")+=");
246				start_loc = RSTART + RLENGTH;
247
248				len = end_loc - start_loc;
249				initializer = substr(old_record, start_loc, len);
250				gsub(srcu_init_param_name "\\.", "", initializer);
251				rcu_batches[name] = initializer;
252				continue;
253			}
254		}
255
256		# Don't include a nonexistent file
257		if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) {
258			update_fieldsep("", 0);
259			next;
260		}
261
262		# Ignore most preprocessor stuff.
263		if (!in_macro && $1 ~ /#/) {
264			break;
265		}
266
267		if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) {
268			read_line();
269			continue;
270		}
271		if (brace_nesting > 0 &&
272		    $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" &&
273		    $2 in rcu_batches) {
274			# Make uses of rcu_batches global. Somewhat unreliable.
275			shift_fields(1, 0);
276			print_fields(1);
277			continue;
278		}
279
280		if ($1 == "static" && NF < 3) {
281			read_line();
282			continue;
283		}
284		if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" ||
285		                       $2 == "void" && $3 == "srcu_flip")) {
286			shift_fields(1, 1);
287			print_fields(2);
288			continue;
289		}
290
291		# Distinguish between read-side and write-side memory barriers.
292		if ($1 == "smp_mb" && NF < 2) {
293			read_line();
294			continue;
295		}
296		if (match($0, /^smp_mb[[:space:]();\/*]*[[:alnum:]]/)) {
297			barrier_letter = substr($0, RLENGTH, 1);
298			if (barrier_letter ~ /A|D/)
299				new_barrier_name = "sync_smp_mb";
300			else if (barrier_letter ~ /B|C/)
301				new_barrier_name = "rs_smp_mb";
302			else {
303				print "Unrecognized memory barrier." > "/dev/null";
304				exit 1;
305			}
306
307			shift_fields(1, 1);
308			printf("%s", new_barrier_name) > outputfile;
309			continue;
310		}
311
312		# Skip definition of rcu_synchronize, since it is already
313		# defined in misc.h. Only present in old versions of srcu.
314		if (brace_nesting == 0 && paren_nesting == 0 &&
315		    $1 == "struct" && $2 == "rcu_synchronize" &&
316		    $0 ~ "^struct(" FS ")+rcu_synchronize(" FS ")+\\{") {
317			shift_fields(2, 0);
318			while (brace_nesting) {
319				if (NF < 2)
320					read_line();
321				shift_fields(1, 0);
322			}
323		}
324
325		# Skip definition of wakeme_after_rcu for the same reason
326		if (brace_nesting == 0 && $1 == "static" && $2 == "void" &&
327		    $3 == "wakeme_after_rcu") {
328			while (NF < 5)
329				read_line();
330			shift_fields(3, 0);
331			do {
332				while (NF < 3)
333					read_line();
334				shift_fields(1, 0);
335			} while (paren_nesting || brace_nesting);
336		}
337
338		if ($1 ~ /^(unsigned|long)$/ && NF < 3) {
339			read_line();
340			continue;
341		}
342
343		# Give srcu_batches_completed the correct type for old SRCU.
344		if (brace_nesting == 0 && $1 == "long" &&
345		    $2 == "srcu_batches_completed") {
346			update_fieldsep("", 0);
347			printf("unsigned ") > outputfile;
348			print_fields(2);
349			continue;
350		}
351		if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" &&
352		    $3 == "srcu_batches_completed") {
353			print_fields(3);
354			continue;
355		}
356
357		# Just print out the input code by default.
358		print_fields(1);
359	}
360	update_fieldsep("", 0);
361	print > outputfile;
362	next;
363}
364
365END {
366	update_fieldsep("", 0);
367
368	if (brace_nesting != 0) {
369		print "Unbalanced braces!" > "/dev/stderr";
370		exit 1;
371	}
372
373	# Define the rcu_batches
374	for (name in rcu_batches)
375		print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output;
376}
377