cachepc-linux

Fork of AMDESE/linux with modifications for CachePC side-channel attack
git clone https://git.sinitax.com/sinitax/cachepc-linux
Log | Files | Refs | README | LICENSE | sfeed.txt

modify_srcu.awk (8964B)


      1#!/usr/bin/awk -f
      2# SPDX-License-Identifier: GPL-2.0
      3
      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
      6# current directory.
      7
      8BEGIN {
      9	if (ARGC != 5) {
     10		print "Usange: input.h input.c output.h output.c" > "/dev/stderr";
     11		exit 1;
     12	}
     13	h_output = ARGV[3];
     14	c_output = ARGV[4];
     15	ARGC = 3;
     16
     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 ")+";
     23
     24	inside_srcu_struct = 0;
     25	inside_srcu_init_def = 0;
     26	srcu_init_param_name = "";
     27	in_macro = 0;
     28	brace_nesting = 0;
     29	paren_nesting = 0;
     30
     31	# Allow the manipulation of the last field separator after has been
     32	# seen.
     33	last_fs = "";
     34	# Whether the last field separator was intended to be output.
     35	last_fs_print = 0;
     36
     37	# rcu_batches stores the initialization for each instance of struct
     38	# rcu_batch
     39
     40	in_comment = 0;
     41
     42	outputfile = "";
     43}
     44
     45{
     46	prev_outputfile = outputfile;
     47	if (FILENAME ~ /\.h$/) {
     48		outputfile = h_output;
     49		if (FNR != NR) {
     50			print "Incorrect file order" > "/dev/stderr";
     51			exit 1;
     52		}
     53	}
     54	else
     55		outputfile = c_output;
     56
     57	if (prev_outputfile && outputfile != prev_outputfile) {
     58		new_outputfile = outputfile;
     59		outputfile = prev_outputfile;
     60		update_fieldsep("", 0);
     61		outputfile = new_outputfile;
     62	}
     63}
     64
     65# Combine the next line into $0.
     66function combine_line() {
     67	ret = getline next_line;
     68	if (ret == 0) {
     69		# Don't allow two consecutive getlines at the end of the file
     70		if (eof_found) {
     71			print "Error: expected more input." > "/dev/stderr";
     72			exit 1;
     73		} else {
     74			eof_found = 1;
     75		}
     76	} else if (ret == -1) {
     77		print "Error reading next line of file" FILENAME > "/dev/stderr";
     78		exit 1;
     79	}
     80	$0 = $0 "\n" next_line;
     81}
     82
     83# Combine backslashed lines and multiline comments.
     84function combine_backslashes() {
     85	while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
     86		combine_line();
     87	}
     88}
     89
     90function read_line() {
     91	combine_line();
     92	combine_backslashes();
     93}
     94
     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
     97# separator.
     98function update_fieldsep(sep, p) {
     99	# Count braces
    100	sep_tmp = sep;
    101	gsub(quote_regexp "|" comment_regexp, "", sep_tmp);
    102	while (1)
    103	{
    104		if (sub("[^{}()]*\\{", "", sep_tmp)) {
    105			brace_nesting++;
    106			continue;
    107		}
    108		if (sub("[^{}()]*\\}", "", sep_tmp)) {
    109			brace_nesting--;
    110			if (brace_nesting < 0) {
    111				print "Unbalanced braces!" > "/dev/stderr";
    112				exit 1;
    113			}
    114			continue;
    115		}
    116		if (sub("[^{}()]*\\(", "", sep_tmp)) {
    117			paren_nesting++;
    118			continue;
    119		}
    120		if (sub("[^{}()]*\\)", "", sep_tmp)) {
    121			paren_nesting--;
    122			if (paren_nesting < 0) {
    123				print "Unbalanced parenthesis!" > "/dev/stderr";
    124				exit 1;
    125			}
    126			continue;
    127		}
    128
    129		break;
    130	}
    131
    132	if (last_fs_print)
    133		printf("%s", last_fs) > outputfile;
    134	last_fs = sep;
    135	last_fs_print = p;
    136}
    137
    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.
    140function shift_fields(n, p) {
    141	do {
    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);
    146			else
    147				$0 = "";
    148		} else {
    149			update_fieldsep("", 0);
    150			print "" > outputfile;
    151			next;
    152		}
    153	} while (--n > 0);
    154}
    155
    156# Shifts and prints the first n fields.
    157function print_fields(n) {
    158	do {
    159		update_fieldsep("", 0);
    160		printf("%s", $1) > outputfile;
    161		shift_fields(1, 1);
    162	} while (--n > 0);
    163}
    164
    165{
    166	combine_backslashes();
    167}
    168
    169# Print leading FS
    170{
    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);
    175		else
    176			$0 = "";
    177	}
    178}
    179
    180# Parse the line.
    181{
    182	while (NF > 0) {
    183		if ($1 == "struct" && NF < 3) {
    184			read_line();
    185			continue;
    186		}
    187
    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;
    193			print_fields(2);
    194			continue;
    195		}
    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;
    202		}
    203
    204		if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") {
    205			# Move rcu_batches outside of the struct.
    206			rcu_batches[$3] = "";
    207			shift_fields(3, 1);
    208			sub(/;[[:space:]]*$/, "", last_fs);
    209			continue;
    210		}
    211
    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;
    216			in_macro = 1;
    217			print_fields(3);
    218			continue;
    219		}
    220		if (inside_srcu_init_def && brace_nesting == 0 &&
    221		    paren_nesting == 0) {
    222			inside_srcu_init_def = 0;
    223			in_macro = 0;
    224			continue;
    225		}
    226
    227		if (inside_srcu_init_def && brace_nesting == 1 &&
    228		    paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ &&
    229		    $1 ~ /^[[:alnum:]_]+$/) {
    230			name = $1;
    231			if (name in rcu_batches) {
    232				# Remove the dot.
    233				sub(/\.[[:space:]]*$/, "", last_fs);
    234
    235				old_record = $0;
    236				do
    237					shift_fields(1, 0);
    238				while (last_fs !~ /,/ || paren_nesting > 0);
    239				end_loc = length(old_record) - length($0);
    240				end_loc += index(last_fs, ",") - length(last_fs);
    241
    242				last_fs = substr(last_fs, index(last_fs, ",") + 1);
    243				last_fs_print = 1;
    244
    245				match(old_record, "^"name"("FS")+=");
    246				start_loc = RSTART + RLENGTH;
    247
    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;
    252				continue;
    253			}
    254		}
    255
    256		# Don't include a nonexistent file
    257		if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) {
    258			update_fieldsep("", 0);
    259			next;
    260		}
    261
    262		# Ignore most preprocessor stuff.
    263		if (!in_macro && $1 ~ /#/) {
    264			break;
    265		}
    266
    267		if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) {
    268			read_line();
    269			continue;
    270		}
    271		if (brace_nesting > 0 &&
    272		    $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" &&
    273		    $2 in rcu_batches) {
    274			# Make uses of rcu_batches global. Somewhat unreliable.
    275			shift_fields(1, 0);
    276			print_fields(1);
    277			continue;
    278		}
    279
    280		if ($1 == "static" && NF < 3) {
    281			read_line();
    282			continue;
    283		}
    284		if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" ||
    285		                       $2 == "void" && $3 == "srcu_flip")) {
    286			shift_fields(1, 1);
    287			print_fields(2);
    288			continue;
    289		}
    290
    291		# Distinguish between read-side and write-side memory barriers.
    292		if ($1 == "smp_mb" && NF < 2) {
    293			read_line();
    294			continue;
    295		}
    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";
    302			else {
    303				print "Unrecognized memory barrier." > "/dev/null";
    304				exit 1;
    305			}
    306
    307			shift_fields(1, 1);
    308			printf("%s", new_barrier_name) > outputfile;
    309			continue;
    310		}
    311
    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 ")+\\{") {
    317			shift_fields(2, 0);
    318			while (brace_nesting) {
    319				if (NF < 2)
    320					read_line();
    321				shift_fields(1, 0);
    322			}
    323		}
    324
    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") {
    328			while (NF < 5)
    329				read_line();
    330			shift_fields(3, 0);
    331			do {
    332				while (NF < 3)
    333					read_line();
    334				shift_fields(1, 0);
    335			} while (paren_nesting || brace_nesting);
    336		}
    337
    338		if ($1 ~ /^(unsigned|long)$/ && NF < 3) {
    339			read_line();
    340			continue;
    341		}
    342
    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;
    348			print_fields(2);
    349			continue;
    350		}
    351		if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" &&
    352		    $3 == "srcu_batches_completed") {
    353			print_fields(3);
    354			continue;
    355		}
    356
    357		# Just print out the input code by default.
    358		print_fields(1);
    359	}
    360	update_fieldsep("", 0);
    361	print > outputfile;
    362	next;
    363}
    364
    365END {
    366	update_fieldsep("", 0);
    367
    368	if (brace_nesting != 0) {
    369		print "Unbalanced braces!" > "/dev/stderr";
    370		exit 1;
    371	}
    372
    373	# Define the rcu_batches
    374	for (name in rcu_batches)
    375		print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output;
    376}