2 # SPDX-License-Identifier: GPL-2.0
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
10 print "Usange: input.h input.c output.h output.c" > "/dev/stderr";
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 ")+";
24 inside_srcu_struct = 0;
25 inside_srcu_init_def = 0;
26 srcu_init_param_name = "";
31 # Allow the manipulation of the last field separator after has been
34 # Whether the last field separator was intended to be output.
37 # rcu_batches stores the initialization for each instance of struct
46 prev_outputfile = outputfile;
47 if (FILENAME ~ /\.h$/) {
48 outputfile = h_output;
50 print "Incorrect file order" > "/dev/stderr";
55 outputfile = c_output;
57 if (prev_outputfile && outputfile != prev_outputfile) {
58 new_outputfile = outputfile;
59 outputfile = prev_outputfile;
60 update_fieldsep("", 0);
61 outputfile = new_outputfile;
65 # Combine the next line into $0.
66 function combine_line() {
67 ret = getline next_line;
69 # Don't allow two consecutive getlines at the end of the file
71 print "Error: expected more input." > "/dev/stderr";
76 } else if (ret == -1) {
77 print "Error reading next line of file" FILENAME > "/dev/stderr";
80 $0 = $0 "\n" next_line;
83 # Combine backslashed lines and multiline comments.
84 function combine_backslashes() {
85 while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
90 function read_line() {
92 combine_backslashes();
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
98 function update_fieldsep(sep, p) {
101 gsub(quote_regexp "|" comment_regexp, "", sep_tmp);
104 if (sub("[^{}()]*\\{", "", sep_tmp)) {
108 if (sub("[^{}()]*\\}", "", sep_tmp)) {
110 if (brace_nesting < 0) {
111 print "Unbalanced braces!" > "/dev/stderr";
116 if (sub("[^{}()]*\\(", "", sep_tmp)) {
120 if (sub("[^{}()]*\\)", "", sep_tmp)) {
122 if (paren_nesting < 0) {
123 print "Unbalanced parenthesis!" > "/dev/stderr";
133 printf("%s", last_fs) > outputfile;
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.
140 function shift_fields(n, p) {
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);
149 update_fieldsep("", 0);
150 print "" > outputfile;
156 # Shifts and prints the first n fields.
157 function print_fields(n) {
159 update_fieldsep("", 0);
160 printf("%s", $1) > outputfile;
166 combine_backslashes();
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);
183 if ($1 == "struct" && NF < 3) {
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;
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;
204 if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") {
205 # Move rcu_batches outside of the struct.
206 rcu_batches[$3] = "";
208 sub(/;[[:space:]]*$/, "", last_fs);
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;
220 if (inside_srcu_init_def && brace_nesting == 0 &&
221 paren_nesting == 0) {
222 inside_srcu_init_def = 0;
227 if (inside_srcu_init_def && brace_nesting == 1 &&
228 paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ &&
229 $1 ~ /^[[:alnum:]_]+$/) {
231 if (name in rcu_batches) {
233 sub(/\.[[:space:]]*$/, "", last_fs);
238 while (last_fs !~ /,/ || paren_nesting > 0);
239 end_loc = length(old_record) - length($0);
240 end_loc += index(last_fs, ",") - length(last_fs);
242 last_fs = substr(last_fs, index(last_fs, ",") + 1);
245 match(old_record, "^"name"("FS")+=");
246 start_loc = RSTART + RLENGTH;
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;
256 # Don't include a nonexistent file
257 if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) {
258 update_fieldsep("", 0);
262 # Ignore most preprocessor stuff.
263 if (!in_macro && $1 ~ /#/) {
267 if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) {
271 if (brace_nesting > 0 &&
272 $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" &&
274 # Make uses of rcu_batches global. Somewhat unreliable.
280 if ($1 == "static" && NF < 3) {
284 if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" ||
285 $2 == "void" && $3 == "srcu_flip")) {
291 # Distinguish between read-side and write-side memory barriers.
292 if ($1 == "smp_mb" && NF < 2) {
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";
303 print "Unrecognized memory barrier." > "/dev/null";
308 printf("%s", new_barrier_name) > outputfile;
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 ")+\\{") {
318 while (brace_nesting) {
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") {
335 } while (paren_nesting || brace_nesting);
338 if ($1 ~ /^(unsigned|long)$/ && NF < 3) {
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;
351 if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" &&
352 $3 == "srcu_batches_completed") {
357 # Just print out the input code by default.
360 update_fieldsep("", 0);
366 update_fieldsep("", 0);
368 if (brace_nesting != 0) {
369 print "Unbalanced braces!" > "/dev/stderr";
373 # Define the rcu_batches
374 for (name in rcu_batches)
375 print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output;