1 /***** spin: pangen3.c *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 */ 8 9 #include "spin.h" 10 #include "y.tab.h" 11 #include <assert.h> 12 13 extern FILE *fd_th, *fd_tc; 14 extern int eventmapnr, old_priority_rules, in_settr; 15 16 typedef struct SRC { 17 int ln, st; /* linenr, statenr */ 18 Symbol *fn; /* filename */ 19 struct SRC *nxt; 20 } SRC; 21 22 static int col; 23 static Symbol *lastfnm; 24 static Symbol lastdef; 25 static int lastfrom; 26 static SRC *frst = (SRC *) 0; 27 static SRC *skip = (SRC *) 0; 28 29 extern int ltl_mode; 30 31 extern void sr_mesg(FILE *, int, int, const char *); 32 extern Lextok **find_mtype_list(const char *); 33 34 static void 35 putnr(int n) 36 { 37 if (col++ == 8) 38 { fprintf(fd_tc, "\n\t"); /* was th */ 39 col = 1; 40 } 41 fprintf(fd_tc, "%3d, ", n); /* was th */ 42 } 43 44 static void 45 putfnm(int j, Symbol *s) 46 { 47 if (lastfnm && lastfnm == s && j != -1) 48 return; 49 50 if (lastfnm) 51 fprintf(fd_tc, "{ \"%s\", %d, %d },\n\t", /* was th */ 52 lastfnm->name, 53 lastfrom, 54 j-1); 55 lastfnm = s; 56 lastfrom = j; 57 } 58 59 static void 60 putfnm_flush(int j) 61 { 62 if (lastfnm) 63 fprintf(fd_tc, "{ \"%s\", %d, %d }\n", /* was th */ 64 lastfnm->name, 65 lastfrom, j); 66 } 67 68 static SRC * 69 newsrc(int m, SRC *n) 70 { SRC *tmp; 71 tmp = (SRC *) emalloc(sizeof(SRC)); 72 tmp->st = m; 73 tmp->nxt = n; 74 return tmp; 75 } 76 77 void 78 putskip(int m) /* states that need not be reached */ 79 { SRC *tmp, *lst = (SRC *)0; 80 /* 6.4.0: now an ordered list */ 81 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) 82 { if (tmp->st == m) 83 { return; 84 } 85 if (tmp->st > m) /* insert before */ 86 { if (tmp == skip) 87 { tmp = newsrc(m, skip); 88 skip = tmp; 89 } else 90 { assert(lst); 91 tmp = newsrc(m, lst->nxt); 92 lst->nxt = tmp; 93 } 94 return; 95 } } 96 /* insert at the end */ 97 if (lst) 98 { lst->nxt = newsrc(m, 0); 99 } else /* empty list */ 100 { skip = newsrc(m, 0); 101 } 102 } 103 104 void 105 unskip(int m) /* a state that needs to be reached after all */ 106 { SRC *tmp, *lst = (SRC *)0; 107 108 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) 109 { if (tmp->st == m) 110 { if (tmp == skip) 111 skip = skip->nxt; 112 else if (lst) /* always true, but helps coverity */ 113 lst->nxt = tmp->nxt; 114 break; 115 } 116 if (tmp->st > m) 117 { break; /* m is not in list */ 118 } } 119 } 120 121 void 122 putsrc(Element *e) /* match states to source lines */ 123 { SRC *tmp, *lst = (SRC *)0; 124 int n, m; 125 126 if (!e || !e->n) return; 127 128 n = e->n->ln; 129 m = e->seqno; 130 /* 6.4.0: now an ordered list */ 131 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt) 132 { if (tmp->st == m) 133 { if (tmp->ln != n || tmp->fn != e->n->fn) 134 printf("putsrc mismatch seqno %d, line %d - %d, file %s\n", m, n, 135 tmp->ln, tmp->fn->name); 136 return; 137 } 138 if (tmp->st > m) /* insert before */ 139 { if (tmp == frst) 140 { tmp = newsrc(m, frst); 141 frst = tmp; 142 } else 143 { assert(lst); 144 tmp = newsrc(m, lst->nxt); 145 lst->nxt = tmp; 146 } 147 tmp->ln = n; 148 tmp->fn = e->n->fn; 149 return; 150 } } 151 /* insert at the end */ 152 tmp = newsrc(m, lst?lst->nxt:0); 153 tmp->ln = n; 154 tmp->fn = e->n->fn; 155 if (lst) 156 { lst->nxt = tmp; 157 } else 158 { frst = tmp; 159 } 160 } 161 162 static void 163 dumpskip(int n, int m) 164 { SRC *tmp, *lst; 165 FILE *tz = fd_tc; /* was fd_th */ 166 int j; 167 168 fprintf(tz, "uchar reached%d [] = {\n\t", m); 169 tmp = skip; 170 lst = (SRC *) 0; 171 for (j = 0, col = 0; j <= n; j++) 172 { /* find j in the sorted list */ 173 for ( ; tmp; lst = tmp, tmp = tmp->nxt) 174 { if (tmp->st == j) 175 { putnr(1); 176 if (lst) 177 lst->nxt = tmp->nxt; 178 else 179 skip = tmp->nxt; 180 break; 181 } 182 if (tmp->st > j) 183 { putnr(0); 184 break; /* j is not in the list */ 185 } } 186 187 if (!tmp) 188 { putnr(0); 189 } } 190 fprintf(tz, "};\n"); 191 fprintf(tz, "uchar *loopstate%d;\n", m); 192 193 if (m == eventmapnr) 194 fprintf(fd_th, "#define reached_event reached%d\n", m); 195 196 skip = (SRC *) 0; 197 } 198 199 void 200 dumpsrc(int n, int m) 201 { SRC *tmp, *lst; 202 int j; 203 static int did_claim = 0; 204 FILE *tz = fd_tc; /* was fd_th */ 205 206 fprintf(tz, "\nshort src_ln%d [] = {\n\t", m); 207 tmp = frst; 208 for (j = 0, col = 0; j <= n; j++) 209 { for ( ; tmp; tmp = tmp->nxt) 210 { if (tmp->st == j) 211 { putnr(tmp->ln); 212 break; 213 } 214 if (tmp->st > j) 215 { putnr(0); 216 break; 217 } } 218 if (!tmp) 219 { putnr(0); 220 } } 221 fprintf(tz, "};\n"); 222 223 lastfnm = (Symbol *) 0; 224 lastdef.name = "-"; 225 fprintf(tz, "S_F_MAP src_file%d [] = {\n\t", m); 226 tmp = frst; 227 lst = (SRC *) 0; 228 for (j = 0, col = 0; j <= n; j++) 229 { for ( ; tmp; lst = tmp, tmp = tmp->nxt) 230 { if (tmp->st == j) 231 { putfnm(j, tmp->fn); 232 if (lst) 233 lst->nxt = tmp->nxt; 234 else 235 frst = tmp->nxt; 236 break; 237 } 238 if (tmp->st > j) 239 { putfnm(j, &lastdef); 240 break; 241 } } 242 if (!tmp) 243 { putfnm(j, &lastdef); 244 } } 245 putfnm_flush(j); 246 fprintf(tz, "};\n"); 247 248 if (pid_is_claim(m) && !did_claim) 249 { fprintf(tz, "short *src_claim;\n"); 250 did_claim++; 251 } 252 if (m == eventmapnr) 253 fprintf(fd_th, "#define src_event src_ln%d\n", m); 254 255 frst = (SRC *) 0; 256 dumpskip(n, m); 257 } 258 259 #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \ 260 comwork(fd,now->rgt,m) 261 #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")") 262 #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m) 263 #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z) 264 265 static int 266 symbolic(FILE *fd, Lextok *tv) 267 { Lextok *n, *Mtype; 268 int cnt = 1; 269 270 if (tv->ismtyp) 271 { char *s = "_unnamed_"; 272 if (tv->sym && tv->sym->mtype_name) 273 { s = tv->sym->mtype_name->name; 274 } 275 Mtype = *find_mtype_list(s); 276 for (n = Mtype; n; n = n->rgt, cnt++) 277 { if (cnt == tv->val) 278 { fprintf(fd, "%s", n->lft->sym->name); 279 return 1; 280 } } } 281 282 return 0; 283 } 284 285 static void 286 comwork(FILE *fd, Lextok *now, int m) 287 { Lextok *v; 288 char *s = 0; 289 int i, j; 290 291 if (!now) { fprintf(fd, "0"); return; } 292 switch (now->ntyp) { 293 case CONST: if (now->ismtyp 294 && now->sym 295 && now->sym->mtype_name) 296 { s = now->sym->mtype_name->name; 297 } 298 sr_mesg(fd, now->val, now->ismtyp, s); 299 break; 300 301 case '!': Cat3("!(", now->lft, ")"); break; 302 case UMIN: Cat3("-(", now->lft, ")"); break; 303 case '~': Cat3("~(", now->lft, ")"); break; 304 305 case '/': Cat1("/"); break; 306 case '*': Cat1("*"); break; 307 case '-': Cat1("-"); break; 308 case '+': Cat1("+"); break; 309 case '%': Cat1("%%"); break; 310 case '&': Cat1("&"); break; 311 case '^': Cat1("^"); break; 312 case '|': Cat1("|"); break; 313 case LE: Cat1("<="); break; 314 case GE: Cat1(">="); break; 315 case GT: Cat1(">"); break; 316 case LT: Cat1("<"); break; 317 case NE: Cat1("!="); break; 318 case EQ: 319 if (ltl_mode 320 && now->lft->ntyp == 'p' 321 && now->rgt->ntyp == 'q') /* remote ref */ 322 { Lextok *p = now->lft->lft; 323 324 fprintf(fd, "("); 325 fprintf(fd, "%s", p->sym->name); 326 if (p->lft) 327 { fprintf(fd, "["); 328 putstmnt(fd, p->lft, 0); /* pid */ 329 fprintf(fd, "]"); 330 } 331 fprintf(fd, "@"); 332 fprintf(fd, "%s", now->rgt->sym->name); 333 fprintf(fd, ")"); 334 break; 335 } 336 Cat1("=="); 337 break; 338 339 case OR: Cat1("||"); break; 340 case AND: Cat1("&&"); break; 341 case LSHIFT: Cat1("<<"); break; 342 case RSHIFT: Cat1(">>"); break; 343 344 case RUN: fprintf(fd, "run %s(", now->sym->name); 345 for (v = now->lft; v; v = v->rgt) 346 if (v == now->lft) 347 { comwork(fd, v->lft, m); 348 } else 349 { Cat2(",", v->lft); 350 } 351 fprintf(fd, ")"); 352 break; 353 354 case LEN: putname(fd, "len(", now->lft, m, ")"); 355 break; 356 case FULL: putname(fd, "full(", now->lft, m, ")"); 357 break; 358 case EMPTY: putname(fd, "empty(", now->lft, m, ")"); 359 break; 360 case NFULL: putname(fd, "nfull(", now->lft, m, ")"); 361 break; 362 case NEMPTY: putname(fd, "nempty(", now->lft, m, ")"); 363 break; 364 365 case 's': putname(fd, "", now->lft, m, now->val?"!!":"!"); 366 for (v = now->rgt, i=0; v; v = v->rgt, i++) 367 { if (v != now->rgt) fprintf(fd,","); 368 if (!symbolic(fd, v->lft)) 369 comwork(fd,v->lft,m); 370 } 371 break; 372 case 'r': putname(fd, "", now->lft, m, "?"); 373 switch (now->val) { 374 case 0: break; 375 case 1: fprintf(fd, "?"); break; 376 case 2: fprintf(fd, "<"); break; 377 case 3: fprintf(fd, "?<"); break; 378 } 379 for (v = now->rgt, i=0; v; v = v->rgt, i++) 380 { if (v != now->rgt) fprintf(fd,","); 381 if (!symbolic(fd, v->lft)) 382 comwork(fd,v->lft,m); 383 } 384 if (now->val >= 2) 385 fprintf(fd, ">"); 386 break; 387 case 'R': putname(fd, "", now->lft, m, now->val?"??[":"?["); 388 for (v = now->rgt, i=0; v; v = v->rgt, i++) 389 { if (v != now->rgt) fprintf(fd,","); 390 if (!symbolic(fd, v->lft)) 391 comwork(fd,v->lft,m); 392 } 393 fprintf(fd, "]"); 394 break; 395 396 case ENABLED: Cat3("enabled(", now->lft, ")"); 397 break; 398 399 case GET_P: if (old_priority_rules) 400 { fprintf(fd, "1"); 401 } else 402 { Cat3("get_priority(", now->lft, ")"); 403 } 404 break; 405 406 case SET_P: if (!old_priority_rules) 407 { fprintf(fd, "set_priority("); 408 comwork(fd, now->lft->lft, m); 409 fprintf(fd, ", "); 410 comwork(fd, now->lft->rgt, m); 411 fprintf(fd, ")"); 412 } 413 break; 414 415 case EVAL: if (now->lft->ntyp == ',') 416 { Cat3("eval(", now->lft->lft, ")"); 417 } else 418 { Cat3("eval(", now->lft, ")"); 419 } 420 break; 421 422 case NONPROGRESS: 423 fprintf(fd, "np_"); 424 break; 425 426 case PC_VAL: Cat3("pc_value(", now->lft, ")"); 427 break; 428 429 case 'c': Cat3("(", now->lft, ")"); 430 break; 431 432 case '?': if (now->lft) 433 { Cat3("( (", now->lft, ") -> "); 434 } 435 if (now->rgt) 436 { Cat3("(", now->rgt->lft, ") : "); 437 Cat3("(", now->rgt->rgt, ") )"); 438 } 439 break; 440 441 case ASGN: 442 if (check_track(now) == STRUCT) { break; } 443 comwork(fd,now->lft,m); 444 fprintf(fd," = "); 445 comwork(fd,now->rgt,m); 446 break; 447 448 case PRINT: { char c, buf[1024]; 449 strncpy(buf, now->sym->name, 510); 450 for (i = j = 0; i < 510; i++, j++) 451 { c = now->sym->name[i]; 452 buf[j] = c; 453 if (c == '\\') buf[++j] = c; 454 if (c == '\"') buf[j] = '\''; 455 if (c == '\0') break; 456 } 457 if (now->ntyp == PRINT) 458 fprintf(fd, "printf"); 459 else 460 fprintf(fd, "annotate"); 461 fprintf(fd, "(%s", buf); 462 } 463 for (v = now->lft; v; v = v->rgt) 464 { Cat2(",", v->lft); 465 } 466 fprintf(fd, ")"); 467 break; 468 case PRINTM: fprintf(fd, "printm("); 469 { char *s = 0; 470 if (now->lft->sym 471 && now->lft->sym->mtype_name) 472 { s = now->lft->sym->mtype_name->name; 473 } 474 475 if (now->lft && now->lft->ismtyp) 476 { fprintf(fd, "%d", now->lft->val); 477 } else 478 { comwork(fd, now->lft, m); 479 } 480 481 if (s) 482 { if (in_settr) 483 { fprintf(fd, ", '%s')", s); 484 } else 485 { fprintf(fd, ", \"%s\")", s); 486 } 487 } else 488 { fprintf(fd, ", 0)"); 489 } 490 } 491 break; 492 case NAME: 493 putname(fd, "", now, m, ""); 494 break; 495 496 case 'p': 497 if (ltl_mode) 498 { fprintf(fd, "%s", now->lft->sym->name); /* proctype */ 499 if (now->lft->lft) 500 { fprintf(fd, "["); 501 putstmnt(fd, now->lft->lft, 0); /* pid */ 502 fprintf(fd, "]"); 503 } 504 fprintf(fd, ":"); /* remote varref */ 505 fprintf(fd, "%s", now->sym->name); /* varname */ 506 break; 507 } 508 putremote(fd, now, m); 509 break; 510 case 'q': fprintf(fd, "%s", now->sym->name); 511 break; 512 case C_EXPR: 513 case C_CODE: fprintf(fd, "{%s}", now->sym->name); 514 break; 515 case ASSERT: Cat3("assert(", now->lft, ")"); 516 break; 517 case '.': fprintf(fd, ".(goto)"); break; 518 case GOTO: fprintf(fd, "goto %s", now->sym->name); break; 519 case BREAK: fprintf(fd, "break"); break; 520 case ELSE: fprintf(fd, "else"); break; 521 case '@': fprintf(fd, "-end-"); break; 522 523 case D_STEP: fprintf(fd, "D_STEP%d", now->ln); break; 524 case ATOMIC: fprintf(fd, "ATOMIC"); break; 525 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break; 526 case IF: fprintf(fd, "IF"); break; 527 case DO: fprintf(fd, "DO"); break; 528 case UNLESS: fprintf(fd, "unless"); break; 529 case TIMEOUT: fprintf(fd, "timeout"); break; 530 default: if (isprint(now->ntyp)) 531 fprintf(fd, "'%c'", now->ntyp); 532 else 533 fprintf(fd, "%d", now->ntyp); 534 break; 535 } 536 } 537 538 void 539 comment(FILE *fd, Lextok *now, int m) 540 { extern short terse, nocast; 541 542 terse=nocast=1; 543 comwork(fd, now, m); 544 terse=nocast=0; 545 } 546