1 /***** spin: spin.y *****/
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 */
17 #define Stop nn(ZN,'@',ZN,ZN)
19 extern Symbol *context, *owner;
20 extern int u_sync, u_async, dumptab;
21 extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np;
22 extern short has_code, has_state, has_io;
23 extern void count_runs(Lextok *);
24 extern void no_internals(Lextok *);
25 extern void any_runs(Lextok *);
26 extern void validref(Lextok *, Lextok *);
29 int Mpars = 0; /* max nr of message parameters */
30 int runsafe = 1; /* 1 if all run stmnts are in init */
31 int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
32 char *claimproc = (char *) 0;
33 char *eventmap = (char *) 0;
35 static int Embedded = 0, inEventMap = 0, has_ini = 0;
39 %token ASSERT PRINT PRINTM
40 %token C_CODE C_DECL C_EXPR C_STATE C_TRACK
41 %token RUN LEN ENABLED EVAL PC_VAL
42 %token TYPEDEF MTYPE INLINE LABEL OF
43 %token GOTO BREAK ELSE SEMI
44 %token IF FI DO OD SEP
45 %token ATOMIC NON_ATOMIC D_STEP UNLESS
46 %token TIMEOUT NONPROGRESS
47 %token ACTIVE PROCTYPE D_PROCTYPE
48 %token HIDDEN SHOW ISLOCAL
49 %token PRIORITY PROVIDED
50 %token FULL EMPTY NFULL NEMPTY
51 %token CONST TYPE XU /* val */
52 %token NAME UNAME PNAME INAME /* sym */
53 %token STRING CLAIM TRACE INIT /* sym */
56 %left SND O_SND RCV R_RCV /* SND doubles as boolean negation */
72 /** PROMELA Grammar Rules **/
74 program : units { yytext[0] = '\0'; }
81 unit : proc /* proctype { } */
83 | claim /* never claim */
84 | events /* event assertions */
85 | one_decl /* variables, chans */
86 | utype /* user defined types */
87 | c_fcts /* c functions etc. */
88 | ns /* named sequence */
89 | SEMI /* optional separator */
93 proc : inst /* optional instantiator */
95 setptype($3, PROCTYPE, ZN);
98 context->ini = $2; /* linenr and file */
99 Expand_Ok++; /* expand struct names in decl */
102 '(' decl ')' { Expand_Ok--;
104 fatal("initializer in parameter list", (char *) 0);
109 rl = ready($3->sym, $6, $11->sq, $2->val, $10);
110 if ($1 != ZN && $1->val > 0)
112 for (j = 0; j < $1->val; j++)
113 runnable(rl, $9?$9->val:1, 1);
115 if (dumptab) $3->sym->ini = $1;
121 proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
122 | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
125 inst : /* empty */ { $$ = ZN; }
126 | ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
127 | ACTIVE '[' CONST ']' {
128 $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
130 non_fatal("max nr of processes is 255\n", "");
132 | ACTIVE '[' NAME ']' {
133 $$ = nn(ZN,CONST,ZN,ZN);
136 non_fatal("undeclared variable %s",
138 else if ($3->sym->ini->ntyp != CONST)
139 non_fatal("need constant initializer for %s\n",
142 $$->val = $3->sym->ini->val;
146 init : INIT { context = $1->sym; }
149 rl = ready(context, ZN, $4->sq, 0, ZN);
150 runnable(rl, $3?$3->val:1, 1);
156 claim : CLAIM { context = $1->sym;
158 non_fatal("claim %s redefined", claimproc);
159 claimproc = $1->sym->name;
161 body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
166 events : TRACE { context = $1->sym;
168 non_fatal("trace %s redefined", eventmap);
169 eventmap = $1->sym->name;
172 body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
178 utype : TYPEDEF NAME { if (context)
179 fatal("typedef %s must be global",
183 '{' decl_lst '}' { setuname($5); owner = ZS; }
186 nm : NAME { $$ = $1; }
189 fatal("invalid use of '%s'", $1->sym->name);
193 ns : INLINE nm '(' { NamesNotAdded++; }
194 args ')' { prep_inline($2->sym, $5);
199 c_fcts : ccode { /* leaves pseudo-inlines with sym of
200 * type CODE_FRAG or CODE_DECL in global context
206 cstate : C_STATE STRING STRING {
207 c_state($2->sym, $3->sym, ZS);
208 has_code = has_state = 1;
210 | C_TRACK STRING STRING {
211 c_track($2->sym, $3->sym, ZS);
212 has_code = has_state = 1;
214 | C_STATE STRING STRING STRING {
215 c_state($2->sym, $3->sym, $4->sym);
216 has_code = has_state = 1;
218 | C_TRACK STRING STRING STRING {
219 c_track($2->sym, $3->sym, $4->sym);
220 has_code = has_state = 1;
224 ccode : C_CODE { Symbol *s;
226 s = prep_inline(ZS, ZN);
228 $$ = nn(ZN, C_CODE, ZN, ZN);
232 | C_DECL { Symbol *s;
234 s = prep_inline(ZS, ZN);
237 $$ = nn(ZN, C_CODE, ZN, ZN);
242 cexpr : C_EXPR { Symbol *s;
244 s = prep_inline(ZS, ZN);
246 $$ = nn(ZN, C_EXPR, ZN, ZN);
248 no_side_effects(s->name);
253 body : '{' { open_seq(1); }
254 sequence OS { add_seq(Stop); }
255 '}' { $$->sq = close_seq(0); }
258 sequence: step { if ($1) add_seq($1); }
259 | sequence MS step { if ($3) add_seq($3); }
262 step : one_decl { $$ = ZN; }
263 | XU vref_lst { setxus($2, $1->val); $$ = ZN; }
264 | NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); }
265 | NAME ':' XU { fatal("label predecing xr/xs claim,", 0); }
267 | stmnt UNLESS stmnt { $$ = do_unless($1, $3); }
270 vis : /* empty */ { $$ = ZN; }
271 | HIDDEN { $$ = $1; }
273 | ISLOCAL { $$ = $1; }
280 one_decl: vis TYPE var_list { setptype($3, $2->val, $1); $$ = $3; }
281 | vis UNAME var_list { setutype($3, $2->sym, $1);
282 $$ = expand($3, Expand_Ok);
284 | vis TYPE asgn '{' nlst '}' {
285 if ($2->val != MTYPE)
286 fatal("malformed declaration", 0);
289 non_fatal("cannot %s mtype (ignored)",
292 fatal("mtype declaration must be global", 0);
296 decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); }
298 decl_lst { $$ = nn(ZN, ',', $1, $3); }
301 decl : /* empty */ { $$ = ZN; }
302 | decl_lst { $$ = $1; }
305 vref_lst: varref { $$ = nn($1, XU, $1, ZN); }
306 | varref ',' vref_lst { $$ = nn($1, XU, $1, $3); }
309 var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); }
310 | ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); }
313 ivar : vardcl { $$ = $1;
314 $1->sym->ini = nn(ZN,CONST,ZN,ZN);
315 $1->sym->ini->val = 0;
317 | vardcl ASGN expr { $1->sym->ini = $3; $$ = $1;
318 trackvar($1,$3); has_ini = 1;
320 | vardcl ASGN ch_init { $1->sym->ini = $3;
321 $$ = $1; has_ini = 1;
325 ch_init : '[' CONST ']' OF
326 '{' typ_list '}' { if ($2->val) u_async++;
328 { int i = cnt_mpars($6);
329 Mpars = max(Mpars, i);
331 $$ = nn(ZN, CHAN, ZN, $6);
336 vardcl : NAME { $1->sym->nel = 1; $$ = $1; }
337 | NAME ':' CONST { $1->sym->nbits = $3->val;
338 if ($3->val >= 8*sizeof(long))
339 { non_fatal("width-field %s too large",
341 $3->val = 8*sizeof(long)-1;
343 $1->sym->nel = 1; $$ = $1;
345 | NAME '[' CONST ']' { $1->sym->nel = $3->val; $$ = $1; }
348 varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); }
351 pfld : NAME { $$ = nn($1, NAME, ZN, ZN); }
352 | NAME { owner = ZS; }
353 '[' expr ']' { $$ = nn($1, NAME, $4, ZN); }
356 cmpnd : pfld { Embedded++;
357 if ($1->sym->type == STRUCT)
358 owner = $1->sym->Snm;
360 sfld { $$ = $1; $$->rgt = $3;
361 if ($3 && $1->sym->type != STRUCT)
362 $1->sym->type = STRUCT;
364 if (!Embedded && !NamesNotAdded
366 non_fatal("undeclared variable: %s",
368 if ($3) validref($1, $3->lft);
373 sfld : /* empty */ { $$ = ZN; }
374 | '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); }
377 stmnt : Special { $$ = $1; }
380 non_fatal("not an event", (char *)0);
384 Special : varref RCV { Expand_Ok++; }
385 rargs { Expand_Ok--; has_io++;
386 $$ = nn($1, 'r', $1, $4);
387 trackchanuse($4, ZN, 'R');
389 | varref SND { Expand_Ok++; }
390 margs { Expand_Ok--; has_io++;
391 $$ = nn($1, 's', $1, $4);
392 $$->val=0; trackchanuse($4, ZN, 'S');
395 | IF options FI { $$ = nn($1, IF, ZN, ZN);
399 | DO { pushbreak(); }
400 options OD { $$ = nn($1, DO, ZN, ZN);
404 | BREAK { $$ = nn(ZN, GOTO, ZN, ZN);
405 $$->sym = break_dest();
407 | GOTO NAME { $$ = nn($2, GOTO, ZN, ZN);
408 if ($2->sym->type != 0
409 && $2->sym->type != LABEL) {
410 non_fatal("bad label-name %s",
413 $2->sym->type = LABEL;
415 | NAME ':' stmnt { $$ = nn($1, ':',$3, ZN);
416 if ($1->sym->type != 0
417 && $1->sym->type != LABEL) {
418 non_fatal("bad label-name %s",
421 $1->sym->type = LABEL;
425 Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3);
427 nochan_manip($1, $3, 0);
430 | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
431 $$ = nn(ZN, '+', $1, $$);
432 $$ = nn($1, ASGN, $1, $$);
435 if ($1->sym->type == CHAN)
436 fatal("arithmetic on chan", (char *)0);
438 | varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
439 $$ = nn(ZN, '-', $1, $$);
440 $$ = nn($1, ASGN, $1, $$);
443 if ($1->sym->type == CHAN)
444 fatal("arithmetic on chan id's", (char *)0);
446 | PRINT '(' STRING { realread = 0; }
447 prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
448 | PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
449 | PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
450 | ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
452 | varref R_RCV { Expand_Ok++; }
453 rargs { Expand_Ok--; has_io++;
454 $$ = nn($1, 'r', $1, $4);
455 $$->val = has_random = 1;
456 trackchanuse($4, ZN, 'R');
458 | varref RCV { Expand_Ok++; }
459 LT rargs GT { Expand_Ok--; has_io++;
460 $$ = nn($1, 'r', $1, $5);
461 $$->val = 2; /* fifo poll */
462 trackchanuse($5, ZN, 'R');
464 | varref R_RCV { Expand_Ok++; }
465 LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */
466 $$ = nn($1, 'r', $1, $5);
467 $$->val = 3; has_random = 1;
468 trackchanuse($5, ZN, 'R');
470 | varref O_SND { Expand_Ok++; }
471 margs { Expand_Ok--; has_io++;
472 $$ = nn($1, 's', $1, $4);
473 $$->val = has_sorted = 1;
474 trackchanuse($4, ZN, 'S');
477 | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
478 | ELSE { $$ = nn(ZN,ELSE,ZN,ZN);
480 | ATOMIC '{' { open_seq(0); }
481 sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN);
482 $$->sl = seqlist(close_seq(3), 0);
483 make_atomic($$->sl->this, 0);
485 | D_STEP '{' { open_seq(0); rem_Seq(); }
486 sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN);
487 $$->sl = seqlist(close_seq(4), 0);
488 make_atomic($$->sl->this, D_ATOM);
491 | '{' { open_seq(0); }
492 sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
493 $$->sl = seqlist(close_seq(5), 0);
496 '(' args ')' { pickup_inline($1->sym, $4); IArgs--; }
500 options : option { $$->sl = seqlist($1->sq, 0); }
501 | option options { $$->sl = seqlist($1->sq, $2->sl); }
504 option : SEP { open_seq(0); }
505 sequence OS { $$ = nn(ZN,0,ZN,ZN);
506 $$->sq = close_seq(6); }
510 | SEMI { /* redundant semi at end of sequence */ }
513 MS : SEMI { /* at least one semi-colon */ }
514 | MS SEMI { /* but more are okay too */ }
517 aname : NAME { $$ = $1; }
521 expr : '(' expr ')' { $$ = $2; }
522 | expr '+' expr { $$ = nn(ZN, '+', $1, $3); }
523 | expr '-' expr { $$ = nn(ZN, '-', $1, $3); }
524 | expr '*' expr { $$ = nn(ZN, '*', $1, $3); }
525 | expr '/' expr { $$ = nn(ZN, '/', $1, $3); }
526 | expr '%' expr { $$ = nn(ZN, '%', $1, $3); }
527 | expr '&' expr { $$ = nn(ZN, '&', $1, $3); }
528 | expr '^' expr { $$ = nn(ZN, '^', $1, $3); }
529 | expr '|' expr { $$ = nn(ZN, '|', $1, $3); }
530 | expr GT expr { $$ = nn(ZN, GT, $1, $3); }
531 | expr LT expr { $$ = nn(ZN, LT, $1, $3); }
532 | expr GE expr { $$ = nn(ZN, GE, $1, $3); }
533 | expr LE expr { $$ = nn(ZN, LE, $1, $3); }
534 | expr EQ expr { $$ = nn(ZN, EQ, $1, $3); }
535 | expr NE expr { $$ = nn(ZN, NE, $1, $3); }
536 | expr AND expr { $$ = nn(ZN, AND, $1, $3); }
537 | expr OR expr { $$ = nn(ZN, OR, $1, $3); }
538 | expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); }
539 | expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); }
540 | '~' expr { $$ = nn(ZN, '~', $2, ZN); }
541 | '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); }
542 | SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); }
544 | '(' expr SEMI expr ':' expr ')' {
545 $$ = nn(ZN, OR, $4, $6);
546 $$ = nn(ZN, '?', $2, $$);
549 | RUN aname { Expand_Ok++;
551 fatal("used 'run' outside proctype",
553 if (strcmp(context->name, ":init:") != 0)
557 Opt_priority { Expand_Ok--;
558 $$ = nn($2, RUN, $5, ZN);
559 $$->val = ($7) ? $7->val : 1;
560 trackchanuse($5, $2, 'A'); trackrun($$);
562 | LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); }
563 | ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN);
566 | varref RCV { Expand_Ok++; }
567 '[' rargs ']' { Expand_Ok--; has_io++;
568 $$ = nn($1, 'R', $1, $5);
570 | varref R_RCV { Expand_Ok++; }
571 '[' rargs ']' { Expand_Ok--; has_io++;
572 $$ = nn($1, 'R', $1, $5);
573 $$->val = has_random = 1;
575 | varref { $$ = $1; trapwonly($1, "varref"); }
577 | CONST { $$ = nn(ZN,CONST,ZN,ZN);
578 $$->ismtyp = $1->ismtyp;
581 | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
582 | NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
585 | PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN);
588 | PNAME '[' expr ']' '@' NAME
589 { $$ = rem_lab($1->sym, $3, $6->sym); }
590 | PNAME '[' expr ']' ':' pfld
591 { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
592 | PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); }
593 | PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
596 Opt_priority: /* none */ { $$ = ZN; }
597 | PRIORITY CONST { $$ = $2; }
600 full_expr: expr { $$ = $1; }
604 Opt_enabler: /* none */ { $$ = ZN; }
605 | PROVIDED '(' full_expr ')' { if (!proper_enabler($3))
606 { non_fatal("invalid PROVIDED clause",
612 | PROVIDED error { $$ = ZN;
613 non_fatal("usage: provided ( ..expr.. )",
618 /* an Expr cannot be negated - to protect Probe expressions */
619 Expr : Probe { $$ = $1; }
620 | '(' Expr ')' { $$ = $2; }
621 | Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
622 | Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
623 | Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
624 | Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
625 | expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
626 | expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
629 Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); }
630 | NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); }
631 | EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); }
632 | NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); }
635 basetype: TYPE { $$->sym = ZS;
637 if ($$->val == UNSIGNED)
638 fatal("unsigned cannot be used as mesg type", 0);
640 | UNAME { $$->sym = $1->sym;
643 | error /* e.g., unsigned ':' const */
646 typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); }
647 | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
650 args : /* empty */ { $$ = ZN; }
654 prargs : /* empty */ { $$ = ZN; }
655 | ',' arg { $$ = $2; }
658 margs : arg { $$ = $1; }
659 | expr '(' arg ')' { if ($1->ntyp == ',')
660 $$ = tail_add($1, $3);
662 $$ = nn(ZN, ',', $1, $3);
666 arg : expr { if ($1->ntyp == ',')
669 $$ = nn(ZN, ',', $1, ZN);
671 | expr ',' arg { if ($1->ntyp == ',')
672 $$ = tail_add($1, $3);
674 $$ = nn(ZN, ',', $1, $3);
678 rarg : varref { $$ = $1; trackvar($1, $1);
679 trapwonly($1, "rarg"); }
680 | EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN);
681 trapwonly($1, "eval rarg"); }
682 | CONST { $$ = nn(ZN,CONST,ZN,ZN);
683 $$->ismtyp = $1->ismtyp;
686 | '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN);
687 $$->val = - ($2->val);
691 rargs : rarg { if ($1->ntyp == ',')
694 $$ = nn(ZN, ',', $1, ZN);
696 | rarg ',' rargs { if ($1->ntyp == ',')
697 $$ = tail_add($1, $3);
699 $$ = nn(ZN, ',', $1, $3);
701 | rarg '(' rargs ')' { if ($1->ntyp == ',')
702 $$ = tail_add($1, $3);
704 $$ = nn(ZN, ',', $1, $3);
706 | '(' rargs ')' { $$ = $2; }
709 nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
710 $$ = nn(ZN, ',', $$, ZN); }
711 | nlst NAME { $$ = nn($2, NAME, ZN, ZN);
712 $$ = nn(ZN, ',', $$, $1);
714 | nlst ',' { $$ = $1; /* commas optional */ }
719 yyerror(char *fmt, ...)
721 non_fatal(fmt, (char *) 0);