0b55f123 |
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 <stdarg.h> |
15 | |
16 | #define YYDEBUG 0 |
17 | #define Stop nn(ZN,'@',ZN,ZN) |
18 | |
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 *); |
27 | extern char yytext[]; |
28 | |
29 | int Mpars = 0; /* max nr of message parameters */ |
30 | int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0; |
31 | char *claimproc = (char *) 0; |
32 | char *eventmap = (char *) 0; |
33 | |
34 | static int Embedded = 0, inEventMap = 0, has_ini = 0; |
35 | |
36 | %} |
37 | |
38 | %token ASSERT PRINT PRINTM |
39 | %token C_CODE C_DECL C_EXPR C_STATE C_TRACK |
40 | %token RUN LEN ENABLED EVAL PC_VAL |
41 | %token TYPEDEF MTYPE INLINE LABEL OF |
42 | %token GOTO BREAK ELSE SEMI |
43 | %token IF FI DO OD SEP |
44 | %token ATOMIC NON_ATOMIC D_STEP UNLESS |
45 | %token TIMEOUT NONPROGRESS |
46 | %token ACTIVE PROCTYPE D_PROCTYPE |
47 | %token HIDDEN SHOW ISLOCAL |
48 | %token PRIORITY PROVIDED |
49 | %token FULL EMPTY NFULL NEMPTY |
50 | %token CONST TYPE XU /* val */ |
51 | %token NAME UNAME PNAME INAME /* sym */ |
52 | %token STRING CLAIM TRACE INIT /* sym */ |
53 | |
54 | %right ASGN |
55 | %left SND O_SND RCV R_RCV /* SND doubles as boolean negation */ |
56 | %left OR |
57 | %left AND |
58 | %left '|' |
59 | %left '^' |
60 | %left '&' |
61 | %left EQ NE |
62 | %left GT LT GE LE |
63 | %left LSHIFT RSHIFT |
64 | %left '+' '-' |
65 | %left '*' '/' '%' |
66 | %left INCR DECR |
67 | %right '~' UMIN NEG |
68 | %left DOT |
69 | %% |
70 | |
71 | /** PROMELA Grammar Rules **/ |
72 | |
73 | program : units { yytext[0] = '\0'; } |
74 | ; |
75 | |
76 | units : unit |
77 | | units unit |
78 | ; |
79 | |
80 | unit : proc /* proctype { } */ |
81 | | init /* init { } */ |
82 | | claim /* never claim */ |
83 | | events /* event assertions */ |
84 | | one_decl /* variables, chans */ |
85 | | utype /* user defined types */ |
86 | | c_fcts /* c functions etc. */ |
87 | | ns /* named sequence */ |
88 | | SEMI /* optional separator */ |
89 | | error |
90 | ; |
91 | |
92 | proc : inst /* optional instantiator */ |
93 | proctype NAME { |
94 | setptype($3, PROCTYPE, ZN); |
95 | setpname($3); |
96 | context = $3->sym; |
97 | context->ini = $2; /* linenr and file */ |
98 | Expand_Ok++; /* expand struct names in decl */ |
99 | has_ini = 0; |
100 | } |
101 | '(' decl ')' { Expand_Ok--; |
102 | if (has_ini) |
103 | fatal("initializer in parameter list", (char *) 0); |
104 | } |
105 | Opt_priority |
106 | Opt_enabler |
107 | body { ProcList *rl; |
108 | rl = ready($3->sym, $6, $11->sq, $2->val, $10); |
109 | if ($1 != ZN && $1->val > 0) |
110 | { int j; |
111 | for (j = 0; j < $1->val; j++) |
112 | runnable(rl, $9?$9->val:1, 1); |
113 | announce(":root:"); |
114 | if (dumptab) $3->sym->ini = $1; |
115 | } |
116 | if (rl && has_ini == 1) /* global initializations, unsafe */ |
117 | { /* printf("proctype %s has initialized data\n", |
118 | $3->sym->name); |
119 | */ |
120 | rl->unsafe = 1; |
121 | } |
122 | context = ZS; |
123 | } |
124 | ; |
125 | |
126 | proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; } |
127 | | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; } |
128 | ; |
129 | |
130 | inst : /* empty */ { $$ = ZN; } |
131 | | ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; } |
132 | | ACTIVE '[' CONST ']' { |
133 | $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val; |
134 | if ($3->val > 255) |
135 | non_fatal("max nr of processes is 255\n", ""); |
136 | } |
137 | | ACTIVE '[' NAME ']' { |
138 | $$ = nn(ZN,CONST,ZN,ZN); |
139 | $$->val = 0; |
140 | if (!$3->sym->type) |
141 | non_fatal("undeclared variable %s", |
142 | $3->sym->name); |
143 | else if ($3->sym->ini->ntyp != CONST) |
144 | non_fatal("need constant initializer for %s\n", |
145 | $3->sym->name); |
146 | else |
147 | $$->val = $3->sym->ini->val; |
148 | } |
149 | ; |
150 | |
151 | init : INIT { context = $1->sym; } |
152 | Opt_priority |
153 | body { ProcList *rl; |
154 | rl = ready(context, ZN, $4->sq, 0, ZN); |
155 | runnable(rl, $3?$3->val:1, 1); |
156 | announce(":root:"); |
157 | context = ZS; |
158 | } |
159 | ; |
160 | |
161 | claim : CLAIM { context = $1->sym; |
162 | if (claimproc) |
163 | non_fatal("claim %s redefined", claimproc); |
164 | claimproc = $1->sym->name; |
165 | } |
166 | body { (void) ready($1->sym, ZN, $3->sq, 0, ZN); |
167 | context = ZS; |
168 | } |
169 | ; |
170 | |
171 | events : TRACE { context = $1->sym; |
172 | if (eventmap) |
173 | non_fatal("trace %s redefined", eventmap); |
174 | eventmap = $1->sym->name; |
175 | inEventMap++; |
176 | } |
177 | body { (void) ready($1->sym, ZN, $3->sq, 0, ZN); |
178 | context = ZS; |
179 | inEventMap--; |
180 | } |
181 | ; |
182 | |
183 | utype : TYPEDEF NAME { if (context) |
184 | fatal("typedef %s must be global", |
185 | $2->sym->name); |
186 | owner = $2->sym; |
187 | } |
188 | '{' decl_lst '}' { setuname($5); owner = ZS; } |
189 | ; |
190 | |
191 | nm : NAME { $$ = $1; } |
192 | | INAME { $$ = $1; |
193 | if (IArgs) |
194 | fatal("invalid use of '%s'", $1->sym->name); |
195 | } |
196 | ; |
197 | |
198 | ns : INLINE nm '(' { NamesNotAdded++; } |
199 | args ')' { prep_inline($2->sym, $5); |
200 | NamesNotAdded--; |
201 | } |
202 | ; |
203 | |
204 | c_fcts : ccode { /* leaves pseudo-inlines with sym of |
205 | * type CODE_FRAG or CODE_DECL in global context |
206 | */ |
207 | } |
208 | | cstate |
209 | ; |
210 | |
211 | cstate : C_STATE STRING STRING { |
212 | c_state($2->sym, $3->sym, ZS); |
213 | has_code = has_state = 1; |
214 | } |
215 | | C_TRACK STRING STRING { |
216 | c_track($2->sym, $3->sym, ZS); |
217 | has_code = has_state = 1; |
218 | } |
219 | | C_STATE STRING STRING STRING { |
220 | c_state($2->sym, $3->sym, $4->sym); |
221 | has_code = has_state = 1; |
222 | } |
223 | | C_TRACK STRING STRING STRING { |
224 | c_track($2->sym, $3->sym, $4->sym); |
225 | has_code = has_state = 1; |
226 | } |
227 | ; |
228 | |
229 | ccode : C_CODE { Symbol *s; |
230 | NamesNotAdded++; |
231 | s = prep_inline(ZS, ZN); |
232 | NamesNotAdded--; |
233 | $$ = nn(ZN, C_CODE, ZN, ZN); |
234 | $$->sym = s; |
235 | has_code = 1; |
236 | } |
237 | | C_DECL { Symbol *s; |
238 | NamesNotAdded++; |
239 | s = prep_inline(ZS, ZN); |
240 | NamesNotAdded--; |
241 | s->type = CODE_DECL; |
242 | $$ = nn(ZN, C_CODE, ZN, ZN); |
243 | $$->sym = s; |
244 | has_code = 1; |
245 | } |
246 | ; |
247 | cexpr : C_EXPR { Symbol *s; |
248 | NamesNotAdded++; |
249 | s = prep_inline(ZS, ZN); |
250 | NamesNotAdded--; |
251 | $$ = nn(ZN, C_EXPR, ZN, ZN); |
252 | $$->sym = s; |
253 | no_side_effects(s->name); |
254 | has_code = 1; |
255 | } |
256 | ; |
257 | |
258 | body : '{' { open_seq(1); } |
259 | sequence OS { add_seq(Stop); } |
260 | '}' { $$->sq = close_seq(0); } |
261 | ; |
262 | |
263 | sequence: step { if ($1) add_seq($1); } |
264 | | sequence MS step { if ($3) add_seq($3); } |
265 | ; |
266 | |
267 | step : one_decl { $$ = ZN; } |
268 | | XU vref_lst { setxus($2, $1->val); $$ = ZN; } |
269 | | NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); } |
270 | | NAME ':' XU { fatal("label predecing xr/xs claim,", 0); } |
271 | | stmnt { $$ = $1; } |
272 | | stmnt UNLESS stmnt { $$ = do_unless($1, $3); } |
273 | ; |
274 | |
275 | vis : /* empty */ { $$ = ZN; } |
276 | | HIDDEN { $$ = $1; } |
277 | | SHOW { $$ = $1; } |
278 | | ISLOCAL { $$ = $1; } |
279 | ; |
280 | |
281 | asgn: /* empty */ |
282 | | ASGN |
283 | ; |
284 | |
285 | one_decl: vis TYPE var_list { setptype($3, $2->val, $1); $$ = $3; } |
286 | | vis UNAME var_list { setutype($3, $2->sym, $1); |
287 | $$ = expand($3, Expand_Ok); |
288 | } |
289 | | vis TYPE asgn '{' nlst '}' { |
290 | if ($2->val != MTYPE) |
291 | fatal("malformed declaration", 0); |
292 | setmtype($5); |
293 | if ($1) |
294 | non_fatal("cannot %s mtype (ignored)", |
295 | $1->sym->name); |
296 | if (context != ZS) |
297 | fatal("mtype declaration must be global", 0); |
298 | } |
299 | ; |
300 | |
301 | decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); } |
302 | | one_decl SEMI |
303 | decl_lst { $$ = nn(ZN, ',', $1, $3); } |
304 | ; |
305 | |
306 | decl : /* empty */ { $$ = ZN; } |
307 | | decl_lst { $$ = $1; } |
308 | ; |
309 | |
310 | vref_lst: varref { $$ = nn($1, XU, $1, ZN); } |
311 | | varref ',' vref_lst { $$ = nn($1, XU, $1, $3); } |
312 | ; |
313 | |
314 | var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); } |
315 | | ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); } |
316 | ; |
317 | |
318 | ivar : vardcl { $$ = $1; |
319 | $1->sym->ini = nn(ZN,CONST,ZN,ZN); |
320 | $1->sym->ini->val = 0; |
321 | } |
322 | | vardcl ASGN expr { $1->sym->ini = $3; $$ = $1; |
323 | trackvar($1,$3); |
324 | if ($3->ntyp == CONST |
325 | || ($3->ntyp == NAME && $3->sym->context)) |
326 | { has_ini = 2; /* local init */ |
327 | } else |
328 | { has_ini = 1; /* possibly global */ |
329 | } |
330 | } |
331 | | vardcl ASGN ch_init { $1->sym->ini = $3; |
332 | $$ = $1; has_ini = 1; |
333 | } |
334 | ; |
335 | |
336 | ch_init : '[' CONST ']' OF |
337 | '{' typ_list '}' { if ($2->val) u_async++; |
338 | else u_sync++; |
339 | { int i = cnt_mpars($6); |
340 | Mpars = max(Mpars, i); |
341 | } |
342 | $$ = nn(ZN, CHAN, ZN, $6); |
343 | $$->val = $2->val; |
344 | } |
345 | ; |
346 | |
347 | vardcl : NAME { $1->sym->nel = 1; $$ = $1; } |
348 | | NAME ':' CONST { $1->sym->nbits = $3->val; |
349 | if ($3->val >= 8*sizeof(long)) |
350 | { non_fatal("width-field %s too large", |
351 | $1->sym->name); |
352 | $3->val = 8*sizeof(long)-1; |
353 | } |
354 | $1->sym->nel = 1; $$ = $1; |
355 | } |
356 | | NAME '[' CONST ']' { $1->sym->nel = $3->val; $$ = $1; } |
357 | ; |
358 | |
359 | varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); } |
360 | ; |
361 | |
362 | pfld : NAME { $$ = nn($1, NAME, ZN, ZN); } |
363 | | NAME { owner = ZS; } |
364 | '[' expr ']' { $$ = nn($1, NAME, $4, ZN); } |
365 | ; |
366 | |
367 | cmpnd : pfld { Embedded++; |
368 | if ($1->sym->type == STRUCT) |
369 | owner = $1->sym->Snm; |
370 | } |
371 | sfld { $$ = $1; $$->rgt = $3; |
372 | if ($3 && $1->sym->type != STRUCT) |
373 | $1->sym->type = STRUCT; |
374 | Embedded--; |
375 | if (!Embedded && !NamesNotAdded |
376 | && !$1->sym->type) |
377 | non_fatal("undeclared variable: %s", |
378 | $1->sym->name); |
379 | if ($3) validref($1, $3->lft); |
380 | owner = ZS; |
381 | } |
382 | ; |
383 | |
384 | sfld : /* empty */ { $$ = ZN; } |
385 | | '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); } |
386 | ; |
387 | |
388 | stmnt : Special { $$ = $1; } |
389 | | Stmnt { $$ = $1; |
390 | if (inEventMap) |
391 | non_fatal("not an event", (char *)0); |
392 | } |
393 | ; |
394 | |
395 | Special : varref RCV { Expand_Ok++; } |
396 | rargs { Expand_Ok--; has_io++; |
397 | $$ = nn($1, 'r', $1, $4); |
398 | trackchanuse($4, ZN, 'R'); |
399 | } |
400 | | varref SND { Expand_Ok++; } |
401 | margs { Expand_Ok--; has_io++; |
402 | $$ = nn($1, 's', $1, $4); |
403 | $$->val=0; trackchanuse($4, ZN, 'S'); |
404 | any_runs($4); |
405 | } |
406 | | IF options FI { $$ = nn($1, IF, ZN, ZN); |
407 | $$->sl = $2->sl; |
408 | prune_opts($$); |
409 | } |
410 | | DO { pushbreak(); } |
411 | options OD { $$ = nn($1, DO, ZN, ZN); |
412 | $$->sl = $3->sl; |
413 | prune_opts($$); |
414 | } |
415 | | BREAK { $$ = nn(ZN, GOTO, ZN, ZN); |
416 | $$->sym = break_dest(); |
417 | } |
418 | | GOTO NAME { $$ = nn($2, GOTO, ZN, ZN); |
419 | if ($2->sym->type != 0 |
420 | && $2->sym->type != LABEL) { |
421 | non_fatal("bad label-name %s", |
422 | $2->sym->name); |
423 | } |
424 | $2->sym->type = LABEL; |
425 | } |
426 | | NAME ':' stmnt { $$ = nn($1, ':',$3, ZN); |
427 | if ($1->sym->type != 0 |
428 | && $1->sym->type != LABEL) { |
429 | non_fatal("bad label-name %s", |
430 | $1->sym->name); |
431 | } |
432 | $1->sym->type = LABEL; |
433 | } |
434 | ; |
435 | |
436 | Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3); |
437 | trackvar($1, $3); |
438 | nochan_manip($1, $3, 0); |
439 | no_internals($1); |
440 | } |
441 | | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1; |
442 | $$ = nn(ZN, '+', $1, $$); |
443 | $$ = nn($1, ASGN, $1, $$); |
444 | trackvar($1, $1); |
445 | no_internals($1); |
446 | if ($1->sym->type == CHAN) |
447 | fatal("arithmetic on chan", (char *)0); |
448 | } |
449 | | varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1; |
450 | $$ = nn(ZN, '-', $1, $$); |
451 | $$ = nn($1, ASGN, $1, $$); |
452 | trackvar($1, $1); |
453 | no_internals($1); |
454 | if ($1->sym->type == CHAN) |
455 | fatal("arithmetic on chan id's", (char *)0); |
456 | } |
457 | | PRINT '(' STRING { realread = 0; } |
458 | prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; } |
459 | | PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); } |
460 | | PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); } |
461 | | ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); } |
462 | | ccode { $$ = $1; } |
463 | | varref R_RCV { Expand_Ok++; } |
464 | rargs { Expand_Ok--; has_io++; |
465 | $$ = nn($1, 'r', $1, $4); |
466 | $$->val = has_random = 1; |
467 | trackchanuse($4, ZN, 'R'); |
468 | } |
469 | | varref RCV { Expand_Ok++; } |
470 | LT rargs GT { Expand_Ok--; has_io++; |
471 | $$ = nn($1, 'r', $1, $5); |
472 | $$->val = 2; /* fifo poll */ |
473 | trackchanuse($5, ZN, 'R'); |
474 | } |
475 | | varref R_RCV { Expand_Ok++; } |
476 | LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */ |
477 | $$ = nn($1, 'r', $1, $5); |
478 | $$->val = 3; has_random = 1; |
479 | trackchanuse($5, ZN, 'R'); |
480 | } |
481 | | varref O_SND { Expand_Ok++; } |
482 | margs { Expand_Ok--; has_io++; |
483 | $$ = nn($1, 's', $1, $4); |
484 | $$->val = has_sorted = 1; |
485 | trackchanuse($4, ZN, 'S'); |
486 | any_runs($4); |
487 | } |
488 | | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); } |
489 | | ELSE { $$ = nn(ZN,ELSE,ZN,ZN); |
490 | } |
491 | | ATOMIC '{' { open_seq(0); } |
492 | sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN); |
493 | $$->sl = seqlist(close_seq(3), 0); |
494 | make_atomic($$->sl->this, 0); |
495 | } |
496 | | D_STEP '{' { open_seq(0); rem_Seq(); } |
497 | sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN); |
498 | $$->sl = seqlist(close_seq(4), 0); |
499 | make_atomic($$->sl->this, D_ATOM); |
500 | unrem_Seq(); |
501 | } |
502 | | '{' { open_seq(0); } |
503 | sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN); |
504 | $$->sl = seqlist(close_seq(5), 0); |
505 | } |
506 | | INAME { IArgs++; } |
507 | '(' args ')' { pickup_inline($1->sym, $4); IArgs--; } |
508 | Stmnt { $$ = $7; } |
509 | ; |
510 | |
511 | options : option { $$->sl = seqlist($1->sq, 0); } |
512 | | option options { $$->sl = seqlist($1->sq, $2->sl); } |
513 | ; |
514 | |
515 | option : SEP { open_seq(0); } |
516 | sequence OS { $$ = nn(ZN,0,ZN,ZN); |
517 | $$->sq = close_seq(6); } |
518 | ; |
519 | |
520 | OS : /* empty */ |
521 | | SEMI { /* redundant semi at end of sequence */ } |
522 | ; |
523 | |
524 | MS : SEMI { /* at least one semi-colon */ } |
525 | | MS SEMI { /* but more are okay too */ } |
526 | ; |
527 | |
528 | aname : NAME { $$ = $1; } |
529 | | PNAME { $$ = $1; } |
530 | ; |
531 | |
532 | expr : '(' expr ')' { $$ = $2; } |
533 | | expr '+' expr { $$ = nn(ZN, '+', $1, $3); } |
534 | | expr '-' expr { $$ = nn(ZN, '-', $1, $3); } |
535 | | expr '*' expr { $$ = nn(ZN, '*', $1, $3); } |
536 | | expr '/' expr { $$ = nn(ZN, '/', $1, $3); } |
537 | | expr '%' expr { $$ = nn(ZN, '%', $1, $3); } |
538 | | expr '&' expr { $$ = nn(ZN, '&', $1, $3); } |
539 | | expr '^' expr { $$ = nn(ZN, '^', $1, $3); } |
540 | | expr '|' expr { $$ = nn(ZN, '|', $1, $3); } |
541 | | expr GT expr { $$ = nn(ZN, GT, $1, $3); } |
542 | | expr LT expr { $$ = nn(ZN, LT, $1, $3); } |
543 | | expr GE expr { $$ = nn(ZN, GE, $1, $3); } |
544 | | expr LE expr { $$ = nn(ZN, LE, $1, $3); } |
545 | | expr EQ expr { $$ = nn(ZN, EQ, $1, $3); } |
546 | | expr NE expr { $$ = nn(ZN, NE, $1, $3); } |
547 | | expr AND expr { $$ = nn(ZN, AND, $1, $3); } |
548 | | expr OR expr { $$ = nn(ZN, OR, $1, $3); } |
549 | | expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); } |
550 | | expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); } |
551 | | '~' expr { $$ = nn(ZN, '~', $2, ZN); } |
552 | | '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); } |
553 | | SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); } |
554 | |
555 | | '(' expr SEMI expr ':' expr ')' { |
556 | $$ = nn(ZN, OR, $4, $6); |
557 | $$ = nn(ZN, '?', $2, $$); |
558 | } |
559 | |
560 | | RUN aname { Expand_Ok++; |
561 | if (!context) |
562 | fatal("used 'run' outside proctype", |
563 | (char *) 0); |
564 | } |
565 | '(' args ')' |
566 | Opt_priority { Expand_Ok--; |
567 | $$ = nn($2, RUN, $5, ZN); |
568 | $$->val = ($7) ? $7->val : 1; |
569 | trackchanuse($5, $2, 'A'); trackrun($$); |
570 | } |
571 | | LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); } |
572 | | ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN); |
573 | has_enabled++; |
574 | } |
575 | | varref RCV { Expand_Ok++; } |
576 | '[' rargs ']' { Expand_Ok--; has_io++; |
577 | $$ = nn($1, 'R', $1, $5); |
578 | } |
579 | | varref R_RCV { Expand_Ok++; } |
580 | '[' rargs ']' { Expand_Ok--; has_io++; |
581 | $$ = nn($1, 'R', $1, $5); |
582 | $$->val = has_random = 1; |
583 | } |
584 | | varref { $$ = $1; trapwonly($1 /*, "varref" */); } |
585 | | cexpr { $$ = $1; } |
586 | | CONST { $$ = nn(ZN,CONST,ZN,ZN); |
587 | $$->ismtyp = $1->ismtyp; |
588 | $$->val = $1->val; |
589 | } |
590 | | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); } |
591 | | NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN); |
592 | has_np++; |
593 | } |
594 | | PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN); |
595 | has_pcvalue++; |
596 | } |
597 | | PNAME '[' expr ']' '@' NAME |
598 | { $$ = rem_lab($1->sym, $3, $6->sym); } |
599 | | PNAME '[' expr ']' ':' pfld |
600 | { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); } |
601 | | PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); } |
602 | | PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); } |
603 | ; |
604 | |
605 | Opt_priority: /* none */ { $$ = ZN; } |
606 | | PRIORITY CONST { $$ = $2; } |
607 | ; |
608 | |
609 | full_expr: expr { $$ = $1; } |
610 | | Expr { $$ = $1; } |
611 | ; |
612 | |
613 | Opt_enabler: /* none */ { $$ = ZN; } |
614 | | PROVIDED '(' full_expr ')' { if (!proper_enabler($3)) |
615 | { non_fatal("invalid PROVIDED clause", |
616 | (char *)0); |
617 | $$ = ZN; |
618 | } else |
619 | $$ = $3; |
620 | } |
621 | | PROVIDED error { $$ = ZN; |
622 | non_fatal("usage: provided ( ..expr.. )", |
623 | (char *)0); |
624 | } |
625 | ; |
626 | |
627 | /* an Expr cannot be negated - to protect Probe expressions */ |
628 | Expr : Probe { $$ = $1; } |
629 | | '(' Expr ')' { $$ = $2; } |
630 | | Expr AND Expr { $$ = nn(ZN, AND, $1, $3); } |
631 | | Expr AND expr { $$ = nn(ZN, AND, $1, $3); } |
632 | | Expr OR Expr { $$ = nn(ZN, OR, $1, $3); } |
633 | | Expr OR expr { $$ = nn(ZN, OR, $1, $3); } |
634 | | expr AND Expr { $$ = nn(ZN, AND, $1, $3); } |
635 | | expr OR Expr { $$ = nn(ZN, OR, $1, $3); } |
636 | ; |
637 | |
638 | Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); } |
639 | | NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); } |
640 | | EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); } |
641 | | NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); } |
642 | ; |
643 | |
644 | basetype: TYPE { $$->sym = ZS; |
645 | $$->val = $1->val; |
646 | if ($$->val == UNSIGNED) |
647 | fatal("unsigned cannot be used as mesg type", 0); |
648 | } |
649 | | UNAME { $$->sym = $1->sym; |
650 | $$->val = STRUCT; |
651 | } |
652 | | error /* e.g., unsigned ':' const */ |
653 | ; |
654 | |
655 | typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); } |
656 | | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); } |
657 | ; |
658 | |
659 | args : /* empty */ { $$ = ZN; } |
660 | | arg { $$ = $1; } |
661 | ; |
662 | |
663 | prargs : /* empty */ { $$ = ZN; } |
664 | | ',' arg { $$ = $2; } |
665 | ; |
666 | |
667 | margs : arg { $$ = $1; } |
668 | | expr '(' arg ')' { if ($1->ntyp == ',') |
669 | $$ = tail_add($1, $3); |
670 | else |
671 | $$ = nn(ZN, ',', $1, $3); |
672 | } |
673 | ; |
674 | |
675 | arg : expr { if ($1->ntyp == ',') |
676 | $$ = $1; |
677 | else |
678 | $$ = nn(ZN, ',', $1, ZN); |
679 | } |
680 | | expr ',' arg { if ($1->ntyp == ',') |
681 | $$ = tail_add($1, $3); |
682 | else |
683 | $$ = nn(ZN, ',', $1, $3); |
684 | } |
685 | ; |
686 | |
687 | rarg : varref { $$ = $1; trackvar($1, $1); |
688 | trapwonly($1 /*, "rarg" */); } |
689 | | EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN); |
690 | trapwonly($1 /*, "eval rarg" */); } |
691 | | CONST { $$ = nn(ZN,CONST,ZN,ZN); |
692 | $$->ismtyp = $1->ismtyp; |
693 | $$->val = $1->val; |
694 | } |
695 | | '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN); |
696 | $$->val = - ($2->val); |
697 | } |
698 | ; |
699 | |
700 | rargs : rarg { if ($1->ntyp == ',') |
701 | $$ = $1; |
702 | else |
703 | $$ = nn(ZN, ',', $1, ZN); |
704 | } |
705 | | rarg ',' rargs { if ($1->ntyp == ',') |
706 | $$ = tail_add($1, $3); |
707 | else |
708 | $$ = nn(ZN, ',', $1, $3); |
709 | } |
710 | | rarg '(' rargs ')' { if ($1->ntyp == ',') |
711 | $$ = tail_add($1, $3); |
712 | else |
713 | $$ = nn(ZN, ',', $1, $3); |
714 | } |
715 | | '(' rargs ')' { $$ = $2; } |
716 | ; |
717 | |
718 | nlst : NAME { $$ = nn($1, NAME, ZN, ZN); |
719 | $$ = nn(ZN, ',', $$, ZN); } |
720 | | nlst NAME { $$ = nn($2, NAME, ZN, ZN); |
721 | $$ = nn(ZN, ',', $$, $1); |
722 | } |
723 | | nlst ',' { $$ = $1; /* commas optional */ } |
724 | ; |
725 | %% |
726 | |
727 | void |
728 | yyerror(char *fmt, ...) |
729 | { |
730 | non_fatal(fmt, (char *) 0); |
731 | } |