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