#!/usr/bin/awk -f

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