tools/testing/selftests/rcutorture/formal/srcu-cbmc/modify_srcu.awk

   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
   8 BEGIN {
   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.
  66 function 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.
  84 function combine_backslashes() {
  85         while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
  86                 combine_line();
  87         }
  88 }
  89
  90 function 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.
  98 function 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.
 140 function 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.
 157 function 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
 365 END {
 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 }