tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk - linux-mtk - Git at Google

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