#!/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;
|
}
|
