1 /***** spin: spin.y *****/ 2 3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* No guarantee whatsoever is expressed or implied by the distribution of */ 6 /* this code. Permission is given to distribute this code provided that */ 7 /* this introductory message is not removed and no monies are exchanged. */ 8 /* Software written by Gerard J. Holzmann. For tool documentation see: */ 9 /* http://spinroot.com/ */ 10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */ 11 12 %{ 13 #include "spin.h" 14 #include <sys/types.h> 15 #ifndef PC 16 #include <unistd.h> 17 #endif 18 #include <stdarg.h> 19 20 #define YYDEBUG 0 21 #define Stop nn(ZN,'@',ZN,ZN) 22 #define PART0 "place initialized var decl of " 23 #define PART1 "place initialized chan decl of " 24 #define PART2 " at start of proctype " 25 26 static Lextok *ltl_to_string(Lextok *); 27 28 extern Symbol *context, *owner; 29 extern Lextok *for_body(Lextok *, int); 30 extern void for_setup(Lextok *, Lextok *, Lextok *); 31 extern Lextok *for_index(Lextok *, Lextok *); 32 extern Lextok *sel_index(Lextok *, Lextok *, Lextok *); 33 extern int u_sync, u_async, dumptab, scope_level; 34 extern int initialization_ok, split_decl; 35 extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np; 36 extern short has_code, has_state, has_io; 37 extern void count_runs(Lextok *); 38 extern void no_internals(Lextok *); 39 extern void any_runs(Lextok *); 40 extern void ltl_list(char *, char *); 41 extern void validref(Lextok *, Lextok *); 42 extern char yytext[]; 43 44 int Mpars = 0; /* max nr of message parameters */ 45 int nclaims = 0; /* nr of never claims */ 46 int ltl_mode = 0; /* set when parsing an ltl formula */ 47 int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0; 48 int in_for = 0; 49 char *claimproc = (char *) 0; 50 char *eventmap = (char *) 0; 51 static char *ltl_name; 52 53 static int Embedded = 0, inEventMap = 0, has_ini = 0; 54 55 %} 56 57 %token ASSERT PRINT PRINTM 58 %token C_CODE C_DECL C_EXPR C_STATE C_TRACK 59 %token RUN LEN ENABLED EVAL PC_VAL 60 %token TYPEDEF MTYPE INLINE LABEL OF 61 %token GOTO BREAK ELSE SEMI 62 %token IF FI DO OD FOR SELECT IN SEP DOTDOT 63 %token ATOMIC NON_ATOMIC D_STEP UNLESS 64 %token TIMEOUT NONPROGRESS 65 %token ACTIVE PROCTYPE D_PROCTYPE 66 %token HIDDEN SHOW ISLOCAL 67 %token PRIORITY PROVIDED 68 %token FULL EMPTY NFULL NEMPTY 69 %token CONST TYPE XU /* val */ 70 %token NAME UNAME PNAME INAME /* sym */ 71 %token STRING CLAIM TRACE INIT LTL /* sym */ 72 73 %right ASGN 74 %left SND O_SND RCV R_RCV /* SND doubles as boolean negation */ 75 %left IMPLIES EQUIV /* ltl */ 76 %left OR 77 %left AND 78 %left ALWAYS EVENTUALLY /* ltl */ 79 %left UNTIL WEAK_UNTIL RELEASE /* ltl */ 80 %right NEXT /* ltl */ 81 %left '|' 82 %left '^' 83 %left '&' 84 %left EQ NE 85 %left GT LT GE LE 86 %left LSHIFT RSHIFT 87 %left '+' '-' 88 %left '*' '/' '%' 89 %left INCR DECR 90 %right '~' UMIN NEG 91 %left DOT 92 %% 93 94 /** PROMELA Grammar Rules **/ 95 96 program : units { yytext[0] = '\0'; } 97 ; 98 99 units : unit 100 | units unit 101 ; 102 103 unit : proc /* proctype { } */ 104 | init /* init { } */ 105 | claim /* never claim */ 106 | ltl /* ltl formula */ 107 | events /* event assertions */ 108 | one_decl /* variables, chans */ 109 | utype /* user defined types */ 110 | c_fcts /* c functions etc. */ 111 | ns /* named sequence */ 112 | SEMI /* optional separator */ 113 | error 114 ; 115 116 proc : inst /* optional instantiator */ 117 proctype NAME { 118 setptype($3, PROCTYPE, ZN); 119 setpname($3); 120 context = $3->sym; 121 context->ini = $2; /* linenr and file */ 122 Expand_Ok++; /* expand struct names in decl */ 123 has_ini = 0; 124 } 125 '(' decl ')' { Expand_Ok--; 126 if (has_ini) 127 fatal("initializer in parameter list", (char *) 0); 128 } 129 Opt_priority 130 Opt_enabler 131 body { ProcList *rl; 132 if ($1 != ZN && $1->val > 0) 133 { int j; 134 rl = ready($3->sym, $6, $11->sq, $2->val, $10, A_PROC); 135 for (j = 0; j < $1->val; j++) 136 { runnable(rl, $9?$9->val:1, 1); 137 } 138 announce(":root:"); 139 if (dumptab) $3->sym->ini = $1; 140 } else 141 { rl = ready($3->sym, $6, $11->sq, $2->val, $10, P_PROC); 142 } 143 if (rl && has_ini == 1) /* global initializations, unsafe */ 144 { /* printf("proctype %s has initialized data\n", 145 $3->sym->name); 146 */ 147 rl->unsafe = 1; 148 } 149 context = ZS; 150 } 151 ; 152 153 proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; } 154 | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; } 155 ; 156 157 inst : /* empty */ { $$ = ZN; } 158 | ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; } 159 | ACTIVE '[' CONST ']' { 160 $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val; 161 if ($3->val > 255) 162 non_fatal("max nr of processes is 255\n", ""); 163 } 164 | ACTIVE '[' NAME ']' { 165 $$ = nn(ZN,CONST,ZN,ZN); 166 $$->val = 0; 167 if (!$3->sym->type) 168 fatal("undeclared variable %s", 169 $3->sym->name); 170 else if ($3->sym->ini->ntyp != CONST) 171 fatal("need constant initializer for %s\n", 172 $3->sym->name); 173 else 174 $$->val = $3->sym->ini->val; 175 } 176 ; 177 178 init : INIT { context = $1->sym; } 179 Opt_priority 180 body { ProcList *rl; 181 rl = ready(context, ZN, $4->sq, 0, ZN, I_PROC); 182 runnable(rl, $3?$3->val:1, 1); 183 announce(":root:"); 184 context = ZS; 185 } 186 ; 187 188 ltl : LTL optname2 { ltl_mode = 1; ltl_name = $2->sym->name; } 189 ltl_body { if ($4) ltl_list($2->sym->name, $4->sym->name); 190 ltl_mode = 0; 191 } 192 ; 193 194 ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); } 195 | error { $$ = NULL; } 196 ; 197 198 claim : CLAIM optname { if ($2 != ZN) 199 { $1->sym = $2->sym; /* new 5.3.0 */ 200 } 201 nclaims++; 202 context = $1->sym; 203 if (claimproc && !strcmp(claimproc, $1->sym->name)) 204 { fatal("claim %s redefined", claimproc); 205 } 206 claimproc = $1->sym->name; 207 } 208 body { (void) ready($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM); 209 context = ZS; 210 } 211 ; 212 213 optname : /* empty */ { char tb[32]; 214 memset(tb, 0, 32); 215 sprintf(tb, "never_%d", nclaims); 216 $$ = nn(ZN, NAME, ZN, ZN); 217 $$->sym = lookup(tb); 218 } 219 | NAME { $$ = $1; } 220 ; 221 222 optname2 : /* empty */ { char tb[32]; static int nltl = 0; 223 memset(tb, 0, 32); 224 sprintf(tb, "ltl_%d", nltl++); 225 $$ = nn(ZN, NAME, ZN, ZN); 226 $$->sym = lookup(tb); 227 } 228 | NAME { $$ = $1; } 229 ; 230 231 events : TRACE { context = $1->sym; 232 if (eventmap) 233 non_fatal("trace %s redefined", eventmap); 234 eventmap = $1->sym->name; 235 inEventMap++; 236 } 237 body { 238 if (strcmp($1->sym->name, ":trace:") == 0) 239 { (void) ready($1->sym, ZN, $3->sq, 0, ZN, E_TRACE); 240 } else 241 { (void) ready($1->sym, ZN, $3->sq, 0, ZN, N_TRACE); 242 } 243 context = ZS; 244 inEventMap--; 245 } 246 ; 247 248 utype : TYPEDEF NAME { if (context) 249 fatal("typedef %s must be global", 250 $2->sym->name); 251 owner = $2->sym; 252 } 253 '{' decl_lst '}' { setuname($5); owner = ZS; } 254 ; 255 256 nm : NAME { $$ = $1; } 257 | INAME { $$ = $1; 258 if (IArgs) 259 fatal("invalid use of '%s'", $1->sym->name); 260 } 261 ; 262 263 ns : INLINE nm '(' { NamesNotAdded++; } 264 args ')' { prep_inline($2->sym, $5); 265 NamesNotAdded--; 266 } 267 ; 268 269 c_fcts : ccode { /* leaves pseudo-inlines with sym of 270 * type CODE_FRAG or CODE_DECL in global context 271 */ 272 } 273 | cstate 274 ; 275 276 cstate : C_STATE STRING STRING { 277 c_state($2->sym, $3->sym, ZS); 278 has_code = has_state = 1; 279 } 280 | C_TRACK STRING STRING { 281 c_track($2->sym, $3->sym, ZS); 282 has_code = has_state = 1; 283 } 284 | C_STATE STRING STRING STRING { 285 c_state($2->sym, $3->sym, $4->sym); 286 has_code = has_state = 1; 287 } 288 | C_TRACK STRING STRING STRING { 289 c_track($2->sym, $3->sym, $4->sym); 290 has_code = has_state = 1; 291 } 292 ; 293 294 ccode : C_CODE { Symbol *s; 295 NamesNotAdded++; 296 s = prep_inline(ZS, ZN); 297 NamesNotAdded--; 298 $$ = nn(ZN, C_CODE, ZN, ZN); 299 $$->sym = s; 300 has_code = 1; 301 } 302 | C_DECL { Symbol *s; 303 NamesNotAdded++; 304 s = prep_inline(ZS, ZN); 305 NamesNotAdded--; 306 s->type = CODE_DECL; 307 $$ = nn(ZN, C_CODE, ZN, ZN); 308 $$->sym = s; 309 has_code = 1; 310 } 311 ; 312 cexpr : C_EXPR { Symbol *s; 313 NamesNotAdded++; 314 s = prep_inline(ZS, ZN); 315 NamesNotAdded--; 316 $$ = nn(ZN, C_EXPR, ZN, ZN); 317 $$->sym = s; 318 no_side_effects(s->name); 319 has_code = 1; 320 } 321 ; 322 323 body : '{' { open_seq(1); } 324 sequence OS { add_seq(Stop); } 325 '}' { $$->sq = close_seq(0); 326 if (scope_level != 0) 327 { non_fatal("missing '}' ?", 0); 328 scope_level = 0; 329 } 330 } 331 ; 332 333 sequence: step { if ($1) add_seq($1); } 334 | sequence MS step { if ($3) add_seq($3); } 335 ; 336 337 step : one_decl { $$ = ZN; } 338 | XU vref_lst { setxus($2, $1->val); $$ = ZN; } 339 | NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); } 340 | NAME ':' XU { fatal("label predecing xr/xs claim,", 0); } 341 | stmnt { $$ = $1; } 342 | stmnt UNLESS stmnt { $$ = do_unless($1, $3); } 343 ; 344 345 vis : /* empty */ { $$ = ZN; } 346 | HIDDEN { $$ = $1; } 347 | SHOW { $$ = $1; } 348 | ISLOCAL { $$ = $1; } 349 ; 350 351 asgn: /* empty */ 352 | ASGN 353 ; 354 355 one_decl: vis TYPE var_list { setptype($3, $2->val, $1); 356 $$ = $3; 357 } 358 | vis UNAME var_list { setutype($3, $2->sym, $1); 359 $$ = expand($3, Expand_Ok); 360 } 361 | vis TYPE asgn '{' nlst '}' { 362 if ($2->val != MTYPE) 363 fatal("malformed declaration", 0); 364 setmtype($5); 365 if ($1) 366 non_fatal("cannot %s mtype (ignored)", 367 $1->sym->name); 368 if (context != ZS) 369 fatal("mtype declaration must be global", 0); 370 } 371 ; 372 373 decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); } 374 | one_decl SEMI 375 decl_lst { $$ = nn(ZN, ',', $1, $3); } 376 ; 377 378 decl : /* empty */ { $$ = ZN; } 379 | decl_lst { $$ = $1; } 380 ; 381 382 vref_lst: varref { $$ = nn($1, XU, $1, ZN); } 383 | varref ',' vref_lst { $$ = nn($1, XU, $1, $3); } 384 ; 385 386 var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); } 387 | ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); } 388 ; 389 390 ivar : vardcl { $$ = $1; 391 $1->sym->ini = nn(ZN,CONST,ZN,ZN); 392 $1->sym->ini->val = 0; 393 } 394 | vardcl ASGN expr { $$ = $1; 395 $1->sym->ini = $3; 396 trackvar($1,$3); 397 if ($3->ntyp == CONST 398 || ($3->ntyp == NAME && $3->sym->context)) 399 { has_ini = 2; /* local init */ 400 } else 401 { has_ini = 1; /* possibly global */ 402 } 403 if (!initialization_ok && split_decl) 404 { nochan_manip($1, $3, 0); 405 no_internals($1); 406 non_fatal(PART0 "'%s'" PART2, $1->sym->name); 407 } 408 } 409 | vardcl ASGN ch_init { $1->sym->ini = $3; 410 $$ = $1; has_ini = 1; 411 if (!initialization_ok && split_decl) 412 { non_fatal(PART1 "'%s'" PART2, $1->sym->name); 413 } 414 } 415 ; 416 417 ch_init : '[' CONST ']' OF 418 '{' typ_list '}' { if ($2->val) 419 u_async++; 420 else 421 u_sync++; 422 { int i = cnt_mpars($6); 423 Mpars = max(Mpars, i); 424 } 425 $$ = nn(ZN, CHAN, ZN, $6); 426 $$->val = $2->val; 427 } 428 ; 429 430 vardcl : NAME { $1->sym->nel = 1; $$ = $1; } 431 | NAME ':' CONST { $1->sym->nbits = $3->val; 432 if ($3->val >= 8*sizeof(long)) 433 { non_fatal("width-field %s too large", 434 $1->sym->name); 435 $3->val = 8*sizeof(long)-1; 436 } 437 $1->sym->nel = 1; $$ = $1; 438 } 439 | NAME '[' CONST ']' { $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; } 440 ; 441 442 varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); } 443 ; 444 445 pfld : NAME { $$ = nn($1, NAME, ZN, ZN); 446 if ($1->sym->isarray && !in_for) 447 { non_fatal("missing array index for '%s'", 448 $1->sym->name); 449 } 450 } 451 | NAME { owner = ZS; } 452 '[' expr ']' { $$ = nn($1, NAME, $4, ZN); } 453 ; 454 455 cmpnd : pfld { Embedded++; 456 if ($1->sym->type == STRUCT) 457 owner = $1->sym->Snm; 458 } 459 sfld { $$ = $1; $$->rgt = $3; 460 if ($3 && $1->sym->type != STRUCT) 461 $1->sym->type = STRUCT; 462 Embedded--; 463 if (!Embedded && !NamesNotAdded 464 && !$1->sym->type) 465 fatal("undeclared variable: %s", 466 $1->sym->name); 467 if ($3) validref($1, $3->lft); 468 owner = ZS; 469 } 470 ; 471 472 sfld : /* empty */ { $$ = ZN; } 473 | '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); } 474 ; 475 476 stmnt : Special { $$ = $1; initialization_ok = 0; } 477 | Stmnt { $$ = $1; initialization_ok = 0; 478 if (inEventMap) 479 non_fatal("not an event", (char *)0); 480 } 481 ; 482 483 for_pre : FOR '(' { in_for = 1; } 484 varref { $$ = $4; } 485 ; 486 487 for_post: '{' sequence OS '}' ; 488 489 Special : varref RCV { Expand_Ok++; } 490 rargs { Expand_Ok--; has_io++; 491 $$ = nn($1, 'r', $1, $4); 492 trackchanuse($4, ZN, 'R'); 493 } 494 | varref SND { Expand_Ok++; } 495 margs { Expand_Ok--; has_io++; 496 $$ = nn($1, 's', $1, $4); 497 $$->val=0; trackchanuse($4, ZN, 'S'); 498 any_runs($4); 499 } 500 | for_pre ':' expr DOTDOT expr ')' { 501 for_setup($1, $3, $5); in_for = 0; 502 } 503 for_post { $$ = for_body($1, 1); 504 } 505 | for_pre IN varref ')' { $$ = for_index($1, $3); in_for = 0; 506 } 507 for_post { $$ = for_body($5, 1); 508 } 509 | SELECT '(' varref ':' expr DOTDOT expr ')' { 510 $$ = sel_index($3, $5, $7); 511 } 512 | IF options FI { $$ = nn($1, IF, ZN, ZN); 513 $$->sl = $2->sl; 514 prune_opts($$); 515 } 516 | DO { pushbreak(); } 517 options OD { $$ = nn($1, DO, ZN, ZN); 518 $$->sl = $3->sl; 519 prune_opts($$); 520 } 521 | BREAK { $$ = nn(ZN, GOTO, ZN, ZN); 522 $$->sym = break_dest(); 523 } 524 | GOTO NAME { $$ = nn($2, GOTO, ZN, ZN); 525 if ($2->sym->type != 0 526 && $2->sym->type != LABEL) { 527 non_fatal("bad label-name %s", 528 $2->sym->name); 529 } 530 $2->sym->type = LABEL; 531 } 532 | NAME ':' stmnt { $$ = nn($1, ':',$3, ZN); 533 if ($1->sym->type != 0 534 && $1->sym->type != LABEL) { 535 non_fatal("bad label-name %s", 536 $1->sym->name); 537 } 538 $1->sym->type = LABEL; 539 } 540 ; 541 542 Stmnt : varref ASGN full_expr { $$ = nn($1, ASGN, $1, $3); 543 trackvar($1, $3); 544 nochan_manip($1, $3, 0); 545 no_internals($1); 546 } 547 | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1; 548 $$ = nn(ZN, '+', $1, $$); 549 $$ = nn($1, ASGN, $1, $$); 550 trackvar($1, $1); 551 no_internals($1); 552 if ($1->sym->type == CHAN) 553 fatal("arithmetic on chan", (char *)0); 554 } 555 | varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1; 556 $$ = nn(ZN, '-', $1, $$); 557 $$ = nn($1, ASGN, $1, $$); 558 trackvar($1, $1); 559 no_internals($1); 560 if ($1->sym->type == CHAN) 561 fatal("arithmetic on chan id's", (char *)0); 562 } 563 | PRINT '(' STRING { realread = 0; } 564 prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; } 565 | PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); } 566 | PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); } 567 | ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); } 568 | ccode { $$ = $1; } 569 | varref R_RCV { Expand_Ok++; } 570 rargs { Expand_Ok--; has_io++; 571 $$ = nn($1, 'r', $1, $4); 572 $$->val = has_random = 1; 573 trackchanuse($4, ZN, 'R'); 574 } 575 | varref RCV { Expand_Ok++; } 576 LT rargs GT { Expand_Ok--; has_io++; 577 $$ = nn($1, 'r', $1, $5); 578 $$->val = 2; /* fifo poll */ 579 trackchanuse($5, ZN, 'R'); 580 } 581 | varref R_RCV { Expand_Ok++; } 582 LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */ 583 $$ = nn($1, 'r', $1, $5); 584 $$->val = 3; has_random = 1; 585 trackchanuse($5, ZN, 'R'); 586 } 587 | varref O_SND { Expand_Ok++; } 588 margs { Expand_Ok--; has_io++; 589 $$ = nn($1, 's', $1, $4); 590 $$->val = has_sorted = 1; 591 trackchanuse($4, ZN, 'S'); 592 any_runs($4); 593 } 594 | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); } 595 | ELSE { $$ = nn(ZN,ELSE,ZN,ZN); 596 } 597 | ATOMIC '{' { open_seq(0); } 598 sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN); 599 $$->sl = seqlist(close_seq(3), 0); 600 make_atomic($$->sl->this, 0); 601 } 602 | D_STEP '{' { open_seq(0); 603 rem_Seq(); 604 } 605 sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN); 606 $$->sl = seqlist(close_seq(4), 0); 607 make_atomic($$->sl->this, D_ATOM); 608 unrem_Seq(); 609 } 610 | '{' { open_seq(0); } 611 sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN); 612 $$->sl = seqlist(close_seq(5), 0); 613 } 614 | INAME { IArgs++; } 615 '(' args ')' { pickup_inline($1->sym, $4); IArgs--; } 616 Stmnt { $$ = $7; } 617 ; 618 619 options : option { $$->sl = seqlist($1->sq, 0); } 620 | option options { $$->sl = seqlist($1->sq, $2->sl); } 621 ; 622 623 option : SEP { open_seq(0); } 624 sequence OS { $$ = nn(ZN,0,ZN,ZN); 625 $$->sq = close_seq(6); } 626 ; 627 628 OS : /* empty */ 629 | SEMI { /* redundant semi at end of sequence */ } 630 ; 631 632 MS : SEMI { /* at least one semi-colon */ } 633 | MS SEMI { /* but more are okay too */ } 634 ; 635 636 aname : NAME { $$ = $1; } 637 | PNAME { $$ = $1; } 638 ; 639 640 expr : '(' expr ')' { $$ = $2; } 641 | expr '+' expr { $$ = nn(ZN, '+', $1, $3); } 642 | expr '-' expr { $$ = nn(ZN, '-', $1, $3); } 643 | expr '*' expr { $$ = nn(ZN, '*', $1, $3); } 644 | expr '/' expr { $$ = nn(ZN, '/', $1, $3); } 645 | expr '%' expr { $$ = nn(ZN, '%', $1, $3); } 646 | expr '&' expr { $$ = nn(ZN, '&', $1, $3); } 647 | expr '^' expr { $$ = nn(ZN, '^', $1, $3); } 648 | expr '|' expr { $$ = nn(ZN, '|', $1, $3); } 649 | expr GT expr { $$ = nn(ZN, GT, $1, $3); } 650 | expr LT expr { $$ = nn(ZN, LT, $1, $3); } 651 | expr GE expr { $$ = nn(ZN, GE, $1, $3); } 652 | expr LE expr { $$ = nn(ZN, LE, $1, $3); } 653 | expr EQ expr { $$ = nn(ZN, EQ, $1, $3); } 654 | expr NE expr { $$ = nn(ZN, NE, $1, $3); } 655 | expr AND expr { $$ = nn(ZN, AND, $1, $3); } 656 | expr OR expr { $$ = nn(ZN, OR, $1, $3); } 657 | expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); } 658 | expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); } 659 | '~' expr { $$ = nn(ZN, '~', $2, ZN); } 660 | '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); } 661 | SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); } 662 663 | '(' expr SEMI expr ':' expr ')' { 664 $$ = nn(ZN, OR, $4, $6); 665 $$ = nn(ZN, '?', $2, $$); 666 } 667 668 | RUN aname { Expand_Ok++; 669 if (!context) 670 fatal("used 'run' outside proctype", 671 (char *) 0); 672 } 673 '(' args ')' 674 Opt_priority { Expand_Ok--; 675 $$ = nn($2, RUN, $5, ZN); 676 $$->val = ($7) ? $7->val : 1; 677 trackchanuse($5, $2, 'A'); trackrun($$); 678 } 679 | LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); } 680 | ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN); 681 has_enabled++; 682 } 683 | varref RCV { Expand_Ok++; } 684 '[' rargs ']' { Expand_Ok--; has_io++; 685 $$ = nn($1, 'R', $1, $5); 686 } 687 | varref R_RCV { Expand_Ok++; } 688 '[' rargs ']' { Expand_Ok--; has_io++; 689 $$ = nn($1, 'R', $1, $5); 690 $$->val = has_random = 1; 691 } 692 | varref { $$ = $1; trapwonly($1 /*, "varref" */); } 693 | cexpr { $$ = $1; } 694 | CONST { $$ = nn(ZN,CONST,ZN,ZN); 695 $$->ismtyp = $1->ismtyp; 696 $$->val = $1->val; 697 } 698 | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); } 699 | NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN); 700 has_np++; 701 } 702 | PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN); 703 has_pcvalue++; 704 } 705 | PNAME '[' expr ']' '@' NAME 706 { $$ = rem_lab($1->sym, $3, $6->sym); } 707 | PNAME '[' expr ']' ':' pfld 708 { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); } 709 | PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); } 710 | PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); } 711 | ltl_expr { $$ = $1; } 712 ; 713 714 Opt_priority: /* none */ { $$ = ZN; } 715 | PRIORITY CONST { $$ = $2; } 716 ; 717 718 full_expr: expr { $$ = $1; } 719 | Expr { $$ = $1; } 720 ; 721 722 ltl_expr: expr UNTIL expr { $$ = nn(ZN, UNTIL, $1, $3); } 723 | expr RELEASE expr { $$ = nn(ZN, RELEASE, $1, $3); } 724 | expr WEAK_UNTIL expr { $$ = nn(ZN, ALWAYS, $1, ZN); 725 $$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3)); 726 } 727 | expr IMPLIES expr { 728 $$ = nn(ZN, '!', $1, ZN); 729 $$ = nn(ZN, OR, $$, $3); 730 } 731 | expr EQUIV expr { $$ = nn(ZN, EQUIV, $1, $3); } 732 | NEXT expr %prec NEG { $$ = nn(ZN, NEXT, $2, ZN); } 733 | ALWAYS expr %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); } 734 | EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); } 735 ; 736 737 /* an Expr cannot be negated - to protect Probe expressions */ 738 Expr : Probe { $$ = $1; } 739 | '(' Expr ')' { $$ = $2; } 740 | Expr AND Expr { $$ = nn(ZN, AND, $1, $3); } 741 | Expr AND expr { $$ = nn(ZN, AND, $1, $3); } 742 | expr AND Expr { $$ = nn(ZN, AND, $1, $3); } 743 | Expr OR Expr { $$ = nn(ZN, OR, $1, $3); } 744 | Expr OR expr { $$ = nn(ZN, OR, $1, $3); } 745 | expr OR Expr { $$ = nn(ZN, OR, $1, $3); } 746 ; 747 748 Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); } 749 | NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); } 750 | EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); } 751 | NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); } 752 ; 753 754 Opt_enabler: /* none */ { $$ = ZN; } 755 | PROVIDED '(' full_expr ')' { if (!proper_enabler($3)) 756 { non_fatal("invalid PROVIDED clause", 757 (char *)0); 758 $$ = ZN; 759 } else 760 $$ = $3; 761 } 762 | PROVIDED error { $$ = ZN; 763 non_fatal("usage: provided ( ..expr.. )", 764 (char *)0); 765 } 766 ; 767 768 basetype: TYPE { $$->sym = ZS; 769 $$->val = $1->val; 770 if ($$->val == UNSIGNED) 771 fatal("unsigned cannot be used as mesg type", 0); 772 } 773 | UNAME { $$->sym = $1->sym; 774 $$->val = STRUCT; 775 } 776 | error /* e.g., unsigned ':' const */ 777 ; 778 779 typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); } 780 | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); } 781 ; 782 783 args : /* empty */ { $$ = ZN; } 784 | arg { $$ = $1; } 785 ; 786 787 prargs : /* empty */ { $$ = ZN; } 788 | ',' arg { $$ = $2; } 789 ; 790 791 margs : arg { $$ = $1; } 792 | expr '(' arg ')' { if ($1->ntyp == ',') 793 $$ = tail_add($1, $3); 794 else 795 $$ = nn(ZN, ',', $1, $3); 796 } 797 ; 798 799 arg : expr { if ($1->ntyp == ',') 800 $$ = $1; 801 else 802 $$ = nn(ZN, ',', $1, ZN); 803 } 804 | expr ',' arg { if ($1->ntyp == ',') 805 $$ = tail_add($1, $3); 806 else 807 $$ = nn(ZN, ',', $1, $3); 808 } 809 ; 810 811 rarg : varref { $$ = $1; trackvar($1, $1); 812 trapwonly($1 /*, "rarg" */); } 813 | EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN); 814 trapwonly($1 /*, "eval rarg" */); } 815 | CONST { $$ = nn(ZN,CONST,ZN,ZN); 816 $$->ismtyp = $1->ismtyp; 817 $$->val = $1->val; 818 } 819 | '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN); 820 $$->val = - ($2->val); 821 } 822 ; 823 824 rargs : rarg { if ($1->ntyp == ',') 825 $$ = $1; 826 else 827 $$ = nn(ZN, ',', $1, ZN); 828 } 829 | rarg ',' rargs { if ($1->ntyp == ',') 830 $$ = tail_add($1, $3); 831 else 832 $$ = nn(ZN, ',', $1, $3); 833 } 834 | rarg '(' rargs ')' { if ($1->ntyp == ',') 835 $$ = tail_add($1, $3); 836 else 837 $$ = nn(ZN, ',', $1, $3); 838 } 839 | '(' rargs ')' { $$ = $2; } 840 ; 841 842 nlst : NAME { $$ = nn($1, NAME, ZN, ZN); 843 $$ = nn(ZN, ',', $$, ZN); } 844 | nlst NAME { $$ = nn($2, NAME, ZN, ZN); 845 $$ = nn(ZN, ',', $$, $1); 846 } 847 | nlst ',' { $$ = $1; /* commas optional */ } 848 ; 849 %% 850 851 #define binop(n, sop) fprintf(fd, "("); recursive(fd, n->lft); \ 852 fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \ 853 fprintf(fd, ")"); 854 #define unop(n, sop) fprintf(fd, "%s (", sop); recursive(fd, n->lft); \ 855 fprintf(fd, ")"); 856 857 static void 858 recursive(FILE *fd, Lextok *n) 859 { 860 if (n) 861 switch (n->ntyp) { 862 case NEXT: 863 unop(n, "X"); 864 break; 865 case ALWAYS: 866 unop(n, "[]"); 867 break; 868 case EVENTUALLY: 869 unop(n, "<>"); 870 break; 871 case '!': 872 unop(n, "!"); 873 break; 874 case UNTIL: 875 binop(n, "U"); 876 break; 877 case WEAK_UNTIL: 878 binop(n, "W"); 879 break; 880 case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */ 881 binop(n, "V"); 882 break; 883 case OR: 884 binop(n, "||"); 885 break; 886 case AND: 887 binop(n, "&&"); 888 break; 889 case IMPLIES: 890 binop(n, "->"); 891 break; 892 case EQUIV: 893 binop(n, "<->"); 894 break; 895 default: 896 comment(fd, n, 0); 897 break; 898 } 899 } 900 901 #define TMP_FILE "_S_p_I_n_.tmp" 902 903 extern int unlink(const char *); 904 905 static Lextok * 906 ltl_to_string(Lextok *n) 907 { Lextok *m = nn(ZN, 0, ZN, ZN); 908 char *retval; 909 char formula[1024]; 910 FILE *tf = fopen(TMP_FILE, "w+"); /* tmpfile() fails on Windows 7 */ 911 912 /* convert the parsed ltl to a string 913 by writing into a file, using existing functions, 914 and then passing it to the existing interface for 915 conversion into a never claim 916 (this means parsing everything twice, which is 917 a little redundant, but adds only miniscule overhead) 918 */ 919 920 if (!tf) 921 { fatal("cannot create temporary file", (char *) 0); 922 } 923 recursive(tf, n); 924 (void) fseek(tf, 0L, SEEK_SET); 925 926 memset(formula, 0, sizeof(formula)); 927 retval = fgets(formula, sizeof(formula), tf); 928 fclose(tf); 929 (void) unlink(TMP_FILE); 930 931 if (!retval) 932 { printf("%p\n", retval); 933 fatal("could not translate ltl formula", 0); 934 } 935 936 if (1) printf("ltl %s: %s\n", ltl_name, formula); 937 938 m->sym = lookup(formula); 939 940 return m; 941 } 942 943 void 944 yyerror(char *fmt, ...) 945 { 946 non_fatal(fmt, (char *) 0); 947 } 948