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

   1 #!/bin/awk -f
   2
   3 # Modify SRCU for formal verification. The first argument should be srcu.h and
   4 # the second should be srcu.c. Outputs modified srcu.h and srcu.c into the
   5 # current directory.
   6
   7 BEGIN {
   8         if (ARGC != 5) {
   9                 print "Usange: input.h input.c output.h output.c" > "/dev/stderr";
  10                 exit 1;
  11         }
  12         h_output = ARGV[3];
  13         c_output = ARGV[4];
  14         ARGC = 3;
  15
  16         # Tokenize using FS and not RS as FS supports regular expressions. Each
  17         # record is one line of source, except that backslashed lines are
  18         # combined. Comments are treated as field separators, as are quotes.
  19         quote_regexp="\"([^\\\\\"]|\\\\.)*\"";
  20         comment_regexp="\\/\\*([^*]|\\*+[^*/])*\\*\\/|\\/\\/.*(\n|$)";
  21         FS="([ \\\\\t\n\v\f;,.=(){}+*/<>&|^-]|\\[|\\]|" comment_regexp "|" quote_regexp ")+";
  22
  23         inside_srcu_struct = 0;
  24         inside_srcu_init_def = 0;
  25         srcu_init_param_name = "";
  26         in_macro = 0;
  27         brace_nesting = 0;
  28         paren_nesting = 0;
  29
  30         # Allow the manipulation of the last field separator after has been
  31         # seen.
  32         last_fs = "";
  33         # Whether the last field separator was intended to be output.
  34         last_fs_print = 0;
  35
  36         # rcu_batches stores the initialization for each instance of struct
  37         # rcu_batch
  38
  39         in_comment = 0;
  40
  41         outputfile = "";
  42 }
  43
  44 {
  45         prev_outputfile = outputfile;
  46         if (FILENAME ~ /\.h$/) {
  47                 outputfile = h_output;
  48                 if (FNR != NR) {
  49                         print "Incorrect file order" > "/dev/stderr";
  50                         exit 1;
  51                 }
  52         }
  53         else
  54                 outputfile = c_output;
  55
  56         if (prev_outputfile && outputfile != prev_outputfile) {
  57                 new_outputfile = outputfile;
  58                 outputfile = prev_outputfile;
  59                 update_fieldsep("", 0);
  60                 outputfile = new_outputfile;
  61         }
  62 }
  63
  64 # Combine the next line into $0.
  65 function combine_line() {
  66         ret = getline next_line;
  67         if (ret == 0) {
  68                 # Don't allow two consecutive getlines at the end of the file
  69                 if (eof_found) {
  70                         print "Error: expected more input." > "/dev/stderr";
  71                         exit 1;
  72                 } else {
  73                         eof_found = 1;
  74                 }
  75         } else if (ret == -1) {
  76                 print "Error reading next line of file" FILENAME > "/dev/stderr";
  77                 exit 1;
  78         }
  79         $0 = $0 "\n" next_line;
  80 }
  81
  82 # Combine backslashed lines and multiline comments.
  83 function combine_backslashes() {
  84         while (/\\$|\/\*([^*]|\*+[^*\/])*\**$/) {
  85                 combine_line();
  86         }
  87 }
  88
  89 function read_line() {
  90         combine_line();
  91         combine_backslashes();
  92 }
  93
  94 # Print out field separators and update variables that depend on them. Only
  95 # print if p is true. Call with sep="" and p=0 to print out the last field
  96 # separator.
  97 function update_fieldsep(sep, p) {
  98         # Count braces
  99         sep_tmp = sep;
 100         gsub(quote_regexp "|" comment_regexp, "", sep_tmp);
 101         while (1)
 102         {
 103                 if (sub("[^{}()]*\\{", "", sep_tmp)) {
 104                         brace_nesting++;
 105                         continue;
 106                 }
 107                 if (sub("[^{}()]*\\}", "", sep_tmp)) {
 108                         brace_nesting--;
 109                         if (brace_nesting < 0) {
 110                                 print "Unbalanced braces!" > "/dev/stderr";
 111                                 exit 1;
 112                         }
 113                         continue;
 114                 }
 115                 if (sub("[^{}()]*\\(", "", sep_tmp)) {
 116                         paren_nesting++;
 117                         continue;
 118                 }
 119                 if (sub("[^{}()]*\\)", "", sep_tmp)) {
 120                         paren_nesting--;
 121                         if (paren_nesting < 0) {
 122                                 print "Unbalanced parenthesis!" > "/dev/stderr";
 123                                 exit 1;
 124                         }
 125                         continue;
 126                 }
 127
 128                 break;
 129         }
 130
 131         if (last_fs_print)
 132                 printf("%s", last_fs) > outputfile;
 133         last_fs = sep;
 134         last_fs_print = p;
 135 }
 136
 137 # Shifts the fields down by n positions. Calls next if there are no more. If p
 138 # is true then print out field separators.
 139 function shift_fields(n, p) {
 140         do {
 141                 if (match($0, FS) > 0) {
 142                         update_fieldsep(substr($0, RSTART, RLENGTH), p);
 143                         if (RSTART + RLENGTH <= length())
 144                                 $0 = substr($0, RSTART + RLENGTH);
 145                         else
 146                                 $0 = "";
 147                 } else {
 148                         update_fieldsep("", 0);
 149                         print "" > outputfile;
 150                         next;
 151                 }
 152         } while (--n > 0);
 153 }
 154
 155 # Shifts and prints the first n fields.
 156 function print_fields(n) {
 157         do {
 158                 update_fieldsep("", 0);
 159                 printf("%s", $1) > outputfile;
 160                 shift_fields(1, 1);
 161         } while (--n > 0);
 162 }
 163
 164 {
 165         combine_backslashes();
 166 }
 167
 168 # Print leading FS
 169 {
 170         if (match($0, "^(" FS ")+") > 0) {
 171                 update_fieldsep(substr($0, RSTART, RLENGTH), 1);
 172                 if (RSTART + RLENGTH <= length())
 173                         $0 = substr($0, RSTART + RLENGTH);
 174                 else
 175                         $0 = "";
 176         }
 177 }
 178
 179 # Parse the line.
 180 {
 181         while (NF > 0) {
 182                 if ($1 == "struct" && NF < 3) {
 183                         read_line();
 184                         continue;
 185                 }
 186
 187                 if (FILENAME ~ /\.h$/ && !inside_srcu_struct &&
 188                     brace_nesting == 0 && paren_nesting == 0 &&
 189                     $1 == "struct" && $2 == "srcu_struct" &&
 190                     $0 ~ "^struct(" FS ")+srcu_struct(" FS ")+\\{") {
 191                         inside_srcu_struct = 1;
 192                         print_fields(2);
 193                         continue;
 194                 }
 195                 if (inside_srcu_struct && brace_nesting == 0 &&
 196                     paren_nesting == 0) {
 197                         inside_srcu_struct = 0;
 198                         update_fieldsep("", 0);
 199                         for (name in rcu_batches)
 200                                 print "extern struct rcu_batch " name ";" > outputfile;
 201                 }
 202
 203                 if (inside_srcu_struct && $1 == "struct" && $2 == "rcu_batch") {
 204                         # Move rcu_batches outside of the struct.
 205                         rcu_batches[$3] = "";
 206                         shift_fields(3, 1);
 207                         sub(/;[[:space:]]*$/, "", last_fs);
 208                         continue;
 209                 }
 210
 211                 if (FILENAME ~ /\.h$/ && !inside_srcu_init_def &&
 212                     $1 == "#define" && $2 == "__SRCU_STRUCT_INIT") {
 213                         inside_srcu_init_def = 1;
 214                         srcu_init_param_name = $3;
 215                         in_macro = 1;
 216                         print_fields(3);
 217                         continue;
 218                 }
 219                 if (inside_srcu_init_def && brace_nesting == 0 &&
 220                     paren_nesting == 0) {
 221                         inside_srcu_init_def = 0;
 222                         in_macro = 0;
 223                         continue;
 224                 }
 225
 226                 if (inside_srcu_init_def && brace_nesting == 1 &&
 227                     paren_nesting == 0 && last_fs ~ /\.[[:space:]]*$/ &&
 228                     $1 ~ /^[[:alnum:]_]+$/) {
 229                         name = $1;
 230                         if (name in rcu_batches) {
 231                                 # Remove the dot.
 232                                 sub(/\.[[:space:]]*$/, "", last_fs);
 233
 234                                 old_record = $0;
 235                                 do
 236                                         shift_fields(1, 0);
 237                                 while (last_fs !~ /,/ || paren_nesting > 0);
 238                                 end_loc = length(old_record) - length($0);
 239                                 end_loc += index(last_fs, ",") - length(last_fs);
 240
 241                                 last_fs = substr(last_fs, index(last_fs, ",") + 1);
 242                                 last_fs_print = 1;
 243
 244                                 match(old_record, "^"name"("FS")+=");
 245                                 start_loc = RSTART + RLENGTH;
 246
 247                                 len = end_loc - start_loc;
 248                                 initializer = substr(old_record, start_loc, len);
 249                                 gsub(srcu_init_param_name "\\.", "", initializer);
 250                                 rcu_batches[name] = initializer;
 251                                 continue;
 252                         }
 253                 }
 254
 255                 # Don't include a nonexistent file
 256                 if (!in_macro && $1 == "#include" && /^#include[[:space:]]+"rcu\.h"/) {
 257                         update_fieldsep("", 0);
 258                         next;
 259                 }
 260
 261                 # Ignore most preprocessor stuff.
 262                 if (!in_macro && $1 ~ /#/) {
 263                         break;
 264                 }
 265
 266                 if (brace_nesting > 0 && $1 ~ "^[[:alnum:]_]+$" && NF < 2) {
 267                         read_line();
 268                         continue;
 269                 }
 270                 if (brace_nesting > 0 &&
 271                     $0 ~ "^[[:alnum:]_]+[[:space:]]*(\\.|->)[[:space:]]*[[:alnum:]_]+" &&
 272                     $2 in rcu_batches) {
 273                         # Make uses of rcu_batches global. Somewhat unreliable.
 274                         shift_fields(1, 0);
 275                         print_fields(1);
 276                         continue;
 277                 }
 278
 279                 if ($1 == "static" && NF < 3) {
 280                         read_line();
 281                         continue;
 282                 }
 283                 if ($1 == "static" && ($2 == "bool" && $3 == "try_check_zero" ||
 284                                        $2 == "void" && $3 == "srcu_flip")) {
 285                         shift_fields(1, 1);
 286                         print_fields(2);
 287                         continue;
 288                 }
 289
 290                 # Distinguish between read-side and write-side memory barriers.
 291                 if ($1 == "smp_mb" && NF < 2) {
 292                         read_line();
 293                         continue;
 294                 }
 295                 if (match($0, /^smp_mb[[:space:]();\/*]*[[:alnum:]]/)) {
 296                         barrier_letter = substr($0, RLENGTH, 1);
 297                         if (barrier_letter ~ /A|D/)
 298                                 new_barrier_name = "sync_smp_mb";
 299                         else if (barrier_letter ~ /B|C/)
 300                                 new_barrier_name = "rs_smp_mb";
 301                         else {
 302                                 print "Unrecognized memory barrier." > "/dev/null";
 303                                 exit 1;
 304                         }
 305
 306                         shift_fields(1, 1);
 307                         printf("%s", new_barrier_name) > outputfile;
 308                         continue;
 309                 }
 310
 311                 # Skip definition of rcu_synchronize, since it is already
 312                 # defined in misc.h. Only present in old versions of srcu.
 313                 if (brace_nesting == 0 && paren_nesting == 0 &&
 314                     $1 == "struct" && $2 == "rcu_synchronize" &&
 315                     $0 ~ "^struct(" FS ")+rcu_synchronize(" FS ")+\\{") {
 316                         shift_fields(2, 0);
 317                         while (brace_nesting) {
 318                                 if (NF < 2)
 319                                         read_line();
 320                                 shift_fields(1, 0);
 321                         }
 322                 }
 323
 324                 # Skip definition of wakeme_after_rcu for the same reason
 325                 if (brace_nesting == 0 && $1 == "static" && $2 == "void" &&
 326                     $3 == "wakeme_after_rcu") {
 327                         while (NF < 5)
 328                                 read_line();
 329                         shift_fields(3, 0);
 330                         do {
 331                                 while (NF < 3)
 332                                         read_line();
 333                                 shift_fields(1, 0);
 334                         } while (paren_nesting || brace_nesting);
 335                 }
 336
 337                 if ($1 ~ /^(unsigned|long)$/ && NF < 3) {
 338                         read_line();
 339                         continue;
 340                 }
 341
 342                 # Give srcu_batches_completed the correct type for old SRCU.
 343                 if (brace_nesting == 0 && $1 == "long" &&
 344                     $2 == "srcu_batches_completed") {
 345                         update_fieldsep("", 0);
 346                         printf("unsigned ") > outputfile;
 347                         print_fields(2);
 348                         continue;
 349                 }
 350                 if (brace_nesting == 0 && $1 == "unsigned" && $2 == "long" &&
 351                     $3 == "srcu_batches_completed") {
 352                         print_fields(3);
 353                         continue;
 354                 }
 355
 356                 # Just print out the input code by default.
 357                 print_fields(1);
 358         }
 359         update_fieldsep("", 0);
 360         print > outputfile;
 361         next;
 362 }
 363
 364 END {
 365         update_fieldsep("", 0);
 366
 367         if (brace_nesting != 0) {
 368                 print "Unbalanced braces!" > "/dev/stderr";
 369                 exit 1;
 370         }
 371
 372         # Define the rcu_batches
 373         for (name in rcu_batches)
 374                 print "struct rcu_batch " name " = " rcu_batches[name] ";" > c_output;
 375 }