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} 377