#!/usr/usr/bin/awk -f # SPDX-License-Identifier: GPL-2.0 # Modify SRCU for formal verification. The first argument should be srcu.h and # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the # current directory. BEGIN { if (ARGC != 5) { print "Usange: input.h input.c output.h output.c" > "/dev/stderr"; exit 1; } h_output = ARGV[3]; c_output = ARGV[4]; ARGC = 3; # Tokenize using FS and not RS as FS supports regular expressions. Each # record is one line of source, except that backslashed lines are # combined. Comments are treated as field separators, as are quotes. quote_regexp="\"([^\\\\\"]|\\\\.)*\""; comment_regexp="\\/\\*([^*]|\\*+[^*/])*\\*\\/|\\/\\/.*(\n|$)"; FS="([ \\\\\t\n\v\f;,.=(){}+*/<>&|^-]|\\[|\\]|" comment_regexp "|" quote_regexp ")+"; inside_srcu_struct = 0; inside_srcu_init_def = 0; srcu_init_param_name = ""; in_macro = 0; brace_nesting = 0; paren_nesting = 0; # Allow the manipulation of the last field separator after has been # seen. last_fs = ""; # Whether the last field separator was intended to be output. last_fs_print = 0; # rcu_batches stores the initialization for each instance of struct # rcu_batch in_comment = 0; outputfile = ""; } { prev_outputfile = outputfile; if (FILENAME ~ /\.h$/) { outputfile = h_output; if (FNR != NR) { print "Incorrect file order" > "/dev/stderr"; exit 1; } } else outputfile = c_output; if (prev_outputfile && outputfile != prev_outputfile) { new_outputfile = outputfile; outputfile = prev_outputfile; update_fieldsep("", 0); outputfile = new_outputfile; } } # Combine the next line into $0. function combine_line() { ret = getline next_line; if (ret == 0) { # Don't allow two consecutive getlines at the end of the file if (eof_found) { print "Error: expected more input." > "/dev/stderr"; exit 1; } else { eof_found = 1; } } else if (ret == -1) { print "Error reading next line of file" FILENAME > "/dev/stderr"; exit 1; } $0 = $0 "\n" next_line; } # Combine backslashed lines and multiline comments. function combine_backslashes() { while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) { combine_line(); } } function read_line() { combine_line(); combine_backslashes(); } # Print out field separators and update variables that depend on them. Only # print if p is true. Call with sep="" and p=0 to print out the last field # separator. function update_fieldsep(sep, p) { # Count braces sep_tmp = sep; gsub(quote_regexp "|" comment_regexp, "", sep_tmp); while (1) { if (sub("[^{}()]*\\{", "", sep_tmp)) { brace_nesting++; continue; } if (sub("[^{}()]*\\}", "", sep_tmp)) { brace_nesting--; if (brace_nesting < 0) { print "Unbalanced braces!" > "/dev/stderr"; exit 1; } continue; } if (sub("[^{}()]*\\(", "", sep_tmp)) { paren_nesting++; continue; } if (sub("[^{}()]*\\)", "", sep_tmp)) { paren_nesting--; if (paren_nesting < 0) { print "Unbalanced parenthesis!" > "/dev/stderr"; exit 1; } continue; } break; } if (last_fs_print) printf("%s", last_fs) > outputfile; last_fs = sep; last_fs_print = p; } # Shifts the fields down by n positions. Calls next if there are no more. If p # is true then print out field separators. function shift_fields(n, p) { do { if (match($0, FS) > 0) { update_fieldsep(substr($0, RSTART, RLENGTH), p); if (RSTART + RLENGTH <= length()) $0 = substr($0, RSTART + RLENGTH); else $0 = ""; } else { update_fieldsep("", 0); print "" > outputfile; next; } } while (--n > 0); } # Shifts and prints the first n fields. function print_fields(n) { do { update_fieldsep("", 0); printf("%s", $1) > outputfile; shift_fields(1, 1); } while (--n > 0); } { combine_backslashes(); } # Print leading FS { if (match($0, "^(" FS ")+") > 0) { update_fieldsep(substr($0, RSTART, RLENGTH), 1); if (RSTART + RLENGTH <= length()) $0 = substr($0, RSTART + RLENGTH); else $0 = ""; } } # Parse the line. { while (NF > 0) { if ($1 == "struct" && NF < 3) { read_line(); continue; } if (FILENAME ~ /\.h$/ && !inside_srcu_struct && brace_nesting == 0 && paren_nesting == 0 && $1 == "struct" && $2 == "srcu_struct" && $0 ~ "^struct(" FS ")+srcu_struct(" FS ")+\\{") { inside_srcu_struct = 1; print_fields(2); continue; } if (inside_srcu_struct && brace_nesting == 0 && paren_nesting == 0) { inside_srcu_struct = 0; update_fieldsep("", 0); for (name in rcu_batches) print "extern struct rcu_batch " name ";" > outputfile; } if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") { # Move rcu_batches outside of the struct. rcu_batches[$3] = ""; shift_fields(3, 1); sub(/;[[:space:]]*$/, "", last_fs); continue; } if (FILENAME ~ /\.h$/ && !inside_srcu_init_def && $1 == "#define" && $2 == "__SRCU_STRUCT_INIT") { inside_srcu_init_def = 1; srcu_init_param_name = $3; in_macro = 1; print_fields(3); continue; } if (inside_srcu_init_def && brace_nesting == 0 && paren_nesting == 0) { inside_srcu_init_def = 0; in_macro = 0; continue; } if (inside_srcu_init_def && brace_nesting == 1 && paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ && $1 ~ /^[[:alnum:]_]+$/) { name = $1; if (name in rcu_batches) { # Remove the dot. sub(/\.[[:space:]]*$/, "", last_fs); old_record = $0; do shift_fields(1, 0); while (last_fs !~ /,/ || paren_nesting > 0); end_loc = length(old_record) - length($0); end_loc += index(last_fs, ",") - length(last_fs); last_fs = substr(last_fs, index(last_fs, ",") + 1); last_fs_print = 1; match(old_record, "^"name"("FS")+="); start_loc = RSTART + RLENGTH; len = end_loc - start_loc; initializer = substr(old_record, start_loc, len); gsub(srcu_init_param_name "\\.", "", initializer); rcu_batches[name] = initializer; continue; } } # Don't include a nonexistent file if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) { update_fieldsep("", 0); next; } # Ignore most preprocessor stuff. if (!in_macro && $1 ~ /#/) { break; } if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) { read_line(); continue; } if (brace_nesting > 0 && $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" && $2 in rcu_batches) { # Make uses of rcu_batches global. Somewhat unreliable. shift_fields(1, 0); print_fields(1); continue; } if ($1 == "static" && NF < 3) { read_line(); continue; } if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" || $2 == "void" && $3 == "srcu_flip")) { shift_fields(1, 1); print_fields(2); continue; } # Distinguish between read-side and write-side memory barriers. if ($1 == "smp_mb" && NF < 2) { read_line(); continue; } if (match($0, /^smp_mb[[:space:]();\/*]*[[:alnum:]]/)) { barrier_letter = substr($0, RLENGTH, 1); if (barrier_letter ~ /A|D/) new_barrier_name = "sync_smp_mb"; else if (barrier_letter ~ /B|C/) new_barrier_name = "rs_smp_mb"; else { print "Unrecognized memory barrier." > "/dev/null"; exit 1; } shift_fields(1, 1); printf("%s", new_barrier_name) > outputfile; continue; } # Skip definition of rcu_synchronize, since it is already # defined in misc.h. Only present in old versions of srcu. if (brace_nesting == 0 && paren_nesting == 0 && $1 == "struct" && $2 == "rcu_synchronize" && $0 ~ "^struct(" FS ")+rcu_synchronize(" FS ")+\\{") { shift_fields(2, 0); while (brace_nesting) { if (NF < 2) read_line(); shift_fields(1, 0); } } # Skip definition of wakeme_after_rcu for the same reason if (brace_nesting == 0 && $1 == "static" && $2 == "void" && $3 == "wakeme_after_rcu") { while (NF < 5) read_line(); shift_fields(3, 0); do { while (NF < 3) read_line(); shift_fields(1, 0); } while (paren_nesting || brace_nesting); } if ($1 ~ /^(unsigned|long)$/ && NF < 3) { read_line(); continue; } # Give srcu_batches_completed the correct type for old SRCU. if (brace_nesting == 0 && $1 == "long" && $2 == "srcu_batches_completed") { update_fieldsep("", 0); printf("unsigned ") > outputfile; print_fields(2); continue; } if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" && $3 == "srcu_batches_completed") { print_fields(3); continue; } # Just print out the input code by default. print_fields(1); } update_fieldsep("", 0); print > outputfile; next; } END { update_fieldsep("", 0); if (brace_nesting != 0) { print "Unbalanced braces!" > "/dev/stderr"; exit 1; } # Define the rcu_batches for (name in rcu_batches) print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output; }