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 *
ltl_to_string(Lextok * n)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
yyerror(char * fmt,...)944 yyerror(char *fmt, ...)
945 {
946 non_fatal(fmt, (char *) 0);
947 }
948