1 /***** spin: main.c *****/
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 #include <stdlib.h>
13 #include "spin.h"
14 #include "version.h"
15 #include <sys/types.h>
16 #include <sys/stat.h>
17 #include <signal.h>
18 /* #include <malloc.h> */
19 #include <time.h>
20 #ifdef PC
21 #include <io.h>
22 extern int unlink(const char *);
23 #else
24 #include <unistd.h>
25 #endif
26 #include "y.tab.h"
27
28 extern int DstepStart, lineno, tl_terse;
29 extern FILE *yyin, *yyout, *tl_out;
30 extern Symbol *context;
31 extern char *claimproc;
32 extern void repro_src(void);
33 extern void qhide(int);
34 extern char CurScope[MAXSCOPESZ];
35
36 Symbol *Fname, *oFname;
37
38 int Etimeouts; /* nr timeouts in program */
39 int Ntimeouts; /* nr timeouts in never claim */
40 int analyze, columns, dumptab, has_remote, has_remvar;
41 int interactive, jumpsteps, m_loss, nr_errs, cutoff;
42 int s_trail, ntrail, verbose, xspin, notabs, rvopt;
43 int no_print, no_wrapup, Caccess, limited_vis, like_java;
44 int separate; /* separate compilation */
45 int export_ast; /* pangen5.c */
46 int old_scope_rules; /* use pre 5.3.0 rules */
47 int split_decl = 1, product, Strict;
48
49 int merger = 1, deadvar = 1;
50 int ccache = 0; /* oyvind teig: 5.2.0 case caching off by default */
51
52 static int preprocessonly, SeedUsed;
53 static int seedy; /* be verbose about chosen seed */
54 static int inlineonly; /* show inlined code */
55 static int dataflow = 1;
56
57 #if 0
58 meaning of flags on verbose:
59 1 -g global variable values
60 2 -l local variable values
61 4 -p all process actions
62 8 -r receives
63 16 -s sends
64 32 -v verbose
65 64 -w very verbose
66 #endif
67
68 static char Operator[] = "operator: ";
69 static char Keyword[] = "keyword: ";
70 static char Function[] = "function-name: ";
71 static char **add_ltl = (char **) 0;
72 static char **ltl_file = (char **) 0;
73 static char **nvr_file = (char **) 0;
74 static char *ltl_claims = (char *) 0;
75 static FILE *fd_ltl = (FILE *) 0;
76 static char *PreArg[64];
77 static int PreCnt = 0;
78 static char out1[64];
79
80 char **trailfilename; /* new option 'k' */
81
82 void explain(int);
83
84 /* to use visual C++:
85 #define CPP "CL -E/E"
86 or call spin as: "spin -PCL -E/E"
87
88 on OS2:
89 #define CPP "icc -E/Pd+ -E/Q+"
90 or call spin as: "spin -Picc -E/Pd+ -E/Q+"
91 */
92 #ifndef CPP
93 #if defined(PC) || defined(MAC)
94 #define CPP "gcc -E -x c" /* most systems have gcc or cpp */
95 /* if gcc-4 is available, this setting is modified below */
96 #else
97 #ifdef SOLARIS
98 #define CPP "/usr/ccs/lib/cpp"
99 #else
100 #if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)
101 #define CPP "cpp"
102 #else
103 #define CPP "/bin/cpp" /* classic Unix systems */
104 #endif
105 #endif
106 #endif
107 #endif
108
109 static char *PreProc = CPP;
110 extern int depth; /* at least some steps were made */
111
112 void
alldone(int estatus)113 alldone(int estatus)
114 {
115 if (preprocessonly == 0
116 && strlen(out1) > 0)
117 (void) unlink((const char *)out1);
118
119 if (seedy && !analyze && !export_ast
120 && !s_trail && !preprocessonly && depth > 0)
121 printf("seed used: %d\n", SeedUsed);
122
123 if (xspin && (analyze || s_trail))
124 { if (estatus)
125 printf("spin: %d error(s) - aborting\n",
126 estatus);
127 else
128 printf("Exit-Status 0\n");
129 }
130 exit(estatus);
131 }
132
133 void
preprocess(char * a,char * b,int a_tmp)134 preprocess(char *a, char *b, int a_tmp)
135 { char precmd[1024], cmd[2048]; int i;
136 #if defined(WIN32) || defined(WIN64)
137 struct _stat x;
138 /* struct stat x; */
139 #endif
140 #ifdef PC
141 extern int try_zpp(char *, char *);
142 if (PreCnt == 0 && try_zpp(a, b))
143 { goto out;
144 }
145 #endif
146 #if defined(WIN32) || defined(WIN64)
147 if (strncmp(PreProc, "gcc -E -x c", strlen("gcc -E -x c")) == 0)
148 { if (stat("/bin/gcc-4.exe", (struct stat *)&x) == 0 /* for PCs with cygwin */
149 || stat("c:/cygwin/bin/gcc-4.exe", (struct stat *)&x) == 0)
150 { PreProc = "gcc-4 -E -x c";
151 } else if (stat("/bin/gcc-3.exe", (struct stat *)&x) == 0
152 || stat("c:/cygwin/bin/gcc-3.exe", (struct stat *)&x) == 0)
153 { PreProc = "gcc-3 -E -x c";
154 } }
155 #endif
156 strcpy(precmd, PreProc);
157 for (i = 1; i <= PreCnt; i++)
158 { strcat(precmd, " ");
159 strcat(precmd, PreArg[i]);
160 }
161 if (strlen(precmd) > sizeof(precmd))
162 { fprintf(stdout, "spin: too many -D args, aborting\n");
163 alldone(1);
164 }
165 sprintf(cmd, "%s %s > %s", precmd, a, b);
166 if (system((const char *)cmd))
167 { (void) unlink((const char *) b);
168 if (a_tmp) (void) unlink((const char *) a);
169 fprintf(stdout, "spin: preprocessing failed\n"); /* 4.1.2 was stderr */
170 alldone(1); /* no return, error exit */
171 }
172 #ifdef PC
173 out:
174 #endif
175 if (a_tmp) (void) unlink((const char *) a);
176 }
177
178 void
usage(void)179 usage(void)
180 {
181 printf("use: spin [-option] ... [-option] file\n");
182 printf("\tNote: file must always be the last argument\n");
183 printf("\t-A apply slicing algorithm\n");
184 printf("\t-a generate a verifier in pan.c\n");
185 printf("\t-B no final state details in simulations\n");
186 printf("\t-b don't execute printfs in simulation\n");
187 printf("\t-C print channel access info (combine with -g etc.)\n");
188 printf("\t-c columnated -s -r simulation output\n");
189 printf("\t-d produce symbol-table information\n");
190 printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
191 printf("\t-Eyyy pass yyy to the preprocessor\n");
192 printf("\t-e compute synchronous product of multiple never claims (modified by -L)\n");
193 printf("\t-f \"..formula..\" translate LTL ");
194 printf("into never claim\n");
195 printf("\t-F file like -f, but with the LTL formula stored in a 1-line file\n");
196 printf("\t-g print all global variables\n");
197 printf("\t-h at end of run, print value of seed for random nr generator used\n");
198 printf("\t-i interactive (random simulation)\n");
199 printf("\t-I show result of inlining and preprocessing\n");
200 printf("\t-J reverse eval order of nested unlesses\n");
201 printf("\t-jN skip the first N steps ");
202 printf("in simulation trail\n");
203 printf("\t-k fname use the trailfile stored in file fname, see also -t\n");
204 printf("\t-L when using -e, use strict language intersection\n");
205 printf("\t-l print all local variables\n");
206 printf("\t-M print msc-flow in Postscript\n");
207 printf("\t-m lose msgs sent to full queues\n");
208 printf("\t-N fname use never claim stored in file fname\n");
209 printf("\t-nN seed for random nr generator\n");
210 printf("\t-O use old scope rules (pre 5.3.0)\n");
211 printf("\t-o1 turn off dataflow-optimizations in verifier\n");
212 printf("\t-o2 don't hide write-only variables in verifier\n");
213 printf("\t-o3 turn off statement merging in verifier\n");
214 printf("\t-o4 turn on rendezvous optiomizations in verifier\n");
215 printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\n");
216 printf("\t-Pxxx use xxx for preprocessing\n");
217 printf("\t-p print all statements\n");
218 printf("\t-qN suppress io for queue N in printouts\n");
219 printf("\t-r print receive events\n");
220 printf("\t-S1 and -S2 separate pan source for claim and model\n");
221 printf("\t-s print send events\n");
222 printf("\t-T do not indent printf output\n");
223 printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
224 printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
225 printf("\t-uN stop a simulation run after N steps\n");
226 printf("\t-v verbose, more warnings\n");
227 printf("\t-w very verbose (when combined with -l or -g)\n");
228 printf("\t-[XYZ] reserved for use by xspin interface\n");
229 printf("\t-V print version number and exit\n");
230 alldone(1);
231 }
232
233 void
optimizations(int nr)234 optimizations(int nr)
235 {
236 switch (nr) {
237 case '1':
238 dataflow = 1 - dataflow; /* dataflow */
239 if (verbose&32)
240 printf("spin: dataflow optimizations turned %s\n",
241 dataflow?"on":"off");
242 break;
243 case '2':
244 /* dead variable elimination */
245 deadvar = 1 - deadvar;
246 if (verbose&32)
247 printf("spin: dead variable elimination turned %s\n",
248 deadvar?"on":"off");
249 break;
250 case '3':
251 /* statement merging */
252 merger = 1 - merger;
253 if (verbose&32)
254 printf("spin: statement merging turned %s\n",
255 merger?"on":"off");
256 break;
257
258 case '4':
259 /* rv optimization */
260 rvopt = 1 - rvopt;
261 if (verbose&32)
262 printf("spin: rendezvous optimization turned %s\n",
263 rvopt?"on":"off");
264 break;
265 case '5':
266 /* case caching */
267 ccache = 1 - ccache;
268 if (verbose&32)
269 printf("spin: case caching turned %s\n",
270 ccache?"on":"off");
271 break;
272 default:
273 printf("spin: bad or missing parameter on -o\n");
274 usage();
275 break;
276 }
277 }
278
279 int
main(int argc,char * argv[])280 main(int argc, char *argv[])
281 { Symbol *s;
282 int T = (int) time((time_t *)0);
283 int usedopts = 0;
284 extern void ana_src(int, int);
285
286 yyin = stdin;
287 yyout = stdout;
288 tl_out = stdout;
289 strcpy(CurScope, "_");
290
291 /* unused flags: y, z, G, L, Q, R, W */
292 while (argc > 1 && argv[1][0] == '-')
293 { switch (argv[1][1]) {
294 /* generate code for separate compilation: S1 or S2 */
295 case 'S': separate = atoi(&argv[1][2]);
296 /* fall through */
297 case 'a': analyze = 1; break;
298 case 'A': export_ast = 1; break;
299 case 'B': no_wrapup = 1; break;
300 case 'b': no_print = 1; break;
301 case 'C': Caccess = 1; break;
302 case 'c': columns = 1; break;
303 case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
304 break; /* define */
305 case 'd': dumptab = 1; break;
306 case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
307 break;
308 case 'e': product++; break; /* see also 'L' */
309 case 'F': ltl_file = (char **) (argv+2);
310 argc--; argv++; break;
311 case 'f': add_ltl = (char **) argv;
312 argc--; argv++; break;
313 case 'g': verbose += 1; break;
314 case 'h': seedy = 1; break;
315 case 'i': interactive = 1; break;
316 case 'I': inlineonly = 1; break;
317 case 'J': like_java = 1; break;
318 case 'j': jumpsteps = atoi(&argv[1][2]); break;
319 case 'k': s_trail = 1;
320 trailfilename = (char **) (argv+2);
321 argc--; argv++; break;
322 case 'L': Strict++; break; /* modified -e */
323 case 'l': verbose += 2; break;
324 case 'M': columns = 2; break;
325 case 'm': m_loss = 1; break;
326 case 'N': nvr_file = (char **) (argv+2);
327 argc--; argv++; break;
328 case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
329 case 'O': old_scope_rules = 1; break;
330 case 'o': optimizations(argv[1][2]);
331 usedopts = 1; break;
332 case 'P': PreProc = (char *) &argv[1][2]; break;
333 case 'p': verbose += 4; break;
334 case 'q': if (isdigit((int) argv[1][2]))
335 qhide(atoi(&argv[1][2]));
336 break;
337 case 'r': verbose += 8; break;
338 case 's': verbose += 16; break;
339 case 'T': notabs = 1; break;
340 case 't': s_trail = 1;
341 if (isdigit((int)argv[1][2]))
342 ntrail = atoi(&argv[1][2]);
343 break;
344 case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
345 break; /* undefine */
346 case 'u': cutoff = atoi(&argv[1][2]); break; /* new 3.4.14 */
347 case 'v': verbose += 32; break;
348 case 'V': printf("%s\n", SpinVersion);
349 alldone(0);
350 break;
351 case 'w': verbose += 64; break;
352 #if 0
353 case 'x': split_decl = 0; break; /* experimental */
354 #endif
355 case 'X': xspin = notabs = 1;
356 #ifndef PC
357 signal(SIGPIPE, alldone); /* not posix... */
358 #endif
359 break;
360 case 'Y': limited_vis = 1; break; /* used by xspin */
361 case 'Z': preprocessonly = 1; break; /* used by xspin */
362
363 default : usage(); break;
364 }
365 argc--; argv++;
366 }
367
368 if (usedopts && !analyze)
369 printf("spin: warning -o[123] option ignored in simulations\n");
370
371 if (ltl_file)
372 { char formula[4096];
373 add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
374 if (!(tl_out = fopen(*ltl_file, "r")))
375 { printf("spin: cannot open %s\n", *ltl_file);
376 alldone(1);
377 }
378 if (!fgets(formula, 4096, tl_out))
379 { printf("spin: cannot read %s\n", *ltl_file);
380 }
381 fclose(tl_out);
382 tl_out = stdout;
383 *ltl_file = (char *) formula;
384 }
385 if (argc > 1)
386 { FILE *fd = stdout;
387 char cmd[512], out2[512];
388
389 /* must remain in current dir */
390 strcpy(out1, "pan.pre");
391
392 if (add_ltl || nvr_file)
393 { sprintf(out2, "%s.nvr", argv[1]);
394 if ((fd = fopen(out2, MFLAGS)) == NULL)
395 { printf("spin: cannot create tmp file %s\n",
396 out2);
397 alldone(1);
398 }
399 fprintf(fd, "#include \"%s\"\n", argv[1]);
400 }
401
402 if (add_ltl)
403 { tl_out = fd;
404 nr_errs = tl_main(2, add_ltl);
405 fclose(fd);
406 preprocess(out2, out1, 1);
407 } else if (nvr_file)
408 { fprintf(fd, "#include \"%s\"\n", *nvr_file);
409 fclose(fd);
410 preprocess(out2, out1, 1);
411 } else
412 { preprocess(argv[1], out1, 0);
413 }
414
415 if (preprocessonly)
416 alldone(0);
417
418 if (!(yyin = fopen(out1, "r")))
419 { printf("spin: cannot open %s\n", out1);
420 alldone(1);
421 }
422
423 if (strncmp(argv[1], "progress", (size_t) 8) == 0
424 || strncmp(argv[1], "accept", (size_t) 6) == 0)
425 sprintf(cmd, "_%s", argv[1]);
426 else
427 strcpy(cmd, argv[1]);
428 oFname = Fname = lookup(cmd);
429 if (oFname->name[0] == '\"')
430 { int i = (int) strlen(oFname->name);
431 oFname->name[i-1] = '\0';
432 oFname = lookup(&oFname->name[1]);
433 }
434 } else
435 { oFname = Fname = lookup("<stdin>");
436 if (add_ltl)
437 { if (argc > 0)
438 exit(tl_main(2, add_ltl));
439 printf("spin: missing argument to -f\n");
440 alldone(1);
441 }
442 printf("%s\n", SpinVersion);
443 fprintf(stderr, "spin: error, no filename specified");
444 fflush(stdout);
445 alldone(1);
446 }
447 if (columns == 2)
448 { extern void putprelude(void);
449 if (xspin || verbose&(1|4|8|16|32))
450 { printf("spin: -c precludes all flags except -t\n");
451 alldone(1);
452 }
453 putprelude();
454 }
455 if (columns && !(verbose&8) && !(verbose&16))
456 verbose += (8+16);
457 if (columns == 2 && limited_vis)
458 verbose += (1+4);
459 Srand((unsigned int) T); /* defined in run.c */
460 SeedUsed = T;
461 s = lookup("_"); s->type = PREDEF; /* write-only global var */
462 s = lookup("_p"); s->type = PREDEF;
463 s = lookup("_pid"); s->type = PREDEF;
464 s = lookup("_last"); s->type = PREDEF;
465 s = lookup("_nr_pr"); s->type = PREDEF; /* new 3.3.10 */
466
467 yyparse();
468 fclose(yyin);
469
470 if (ltl_claims)
471 { Symbol *r;
472 fclose(fd_ltl);
473 if (!(yyin = fopen(ltl_claims, "r")))
474 { fatal("cannot open %s", ltl_claims);
475 }
476 r = oFname;
477 oFname = Fname = lookup(ltl_claims);
478 lineno = 0;
479 yyparse();
480 fclose(yyin);
481 oFname = Fname = r;
482 if (0)
483 { (void) unlink(ltl_claims);
484 } }
485
486 loose_ends();
487
488 if (inlineonly)
489 { repro_src();
490 return 0;
491 }
492
493 chanaccess();
494 if (!Caccess)
495 { if (!s_trail && (dataflow || merger))
496 ana_src(dataflow, merger);
497 sched();
498 alldone(nr_errs);
499 }
500 return 0;
501 }
502
503 void
ltl_list(char * nm,char * fm)504 ltl_list(char *nm, char *fm)
505 {
506 if (analyze || dumptab) /* when generating pan.c only */
507 { if (!ltl_claims)
508 { ltl_claims = "_spin_nvr.tmp";
509 if ((fd_ltl = fopen(ltl_claims, MFLAGS)) == NULL)
510 { fatal("cannot open tmp file %s", ltl_claims);
511 }
512 tl_out = fd_ltl;
513 }
514
515 add_ltl = (char **) emalloc(5 * sizeof(char *));
516 add_ltl[1] = "-c";
517 add_ltl[2] = nm;
518 add_ltl[3] = "-f";
519 add_ltl[4] = (char *) emalloc(strlen(fm)+4);
520 strcpy(add_ltl[4], "!(");
521 strcat(add_ltl[4], fm);
522 strcat(add_ltl[4], ")");
523 /* add_ltl[4] = fm; */
524
525 nr_errs += tl_main(4, add_ltl);
526
527 fflush(tl_out);
528 /* should read this file after the main file is read */
529 }
530 }
531
532 int
yywrap(void)533 yywrap(void) /* dummy routine */
534 {
535 return 1;
536 }
537
538 void
non_fatal(char * s1,char * s2)539 non_fatal(char *s1, char *s2)
540 { extern char yytext[];
541
542 printf("spin: %s:%d, Error: ",
543 oFname?oFname->name:"nofilename", lineno);
544 if (s2)
545 printf(s1, s2);
546 else
547 printf(s1);
548 if (strlen(yytext)>1)
549 printf(" near '%s'", yytext);
550 printf("\n");
551 nr_errs++;
552 }
553
554 void
fatal(char * s1,char * s2)555 fatal(char *s1, char *s2)
556 {
557 non_fatal(s1, s2);
558 (void) unlink("pan.b");
559 (void) unlink("pan.c");
560 (void) unlink("pan.h");
561 (void) unlink("pan.m");
562 (void) unlink("pan.t");
563 (void) unlink("pan.pre");
564 alldone(1);
565 }
566
567 char *
emalloc(size_t n)568 emalloc(size_t n)
569 { char *tmp;
570 static unsigned long cnt = 0;
571
572 if (n == 0)
573 return NULL; /* robert shelton 10/20/06 */
574
575 if (!(tmp = (char *) malloc(n)))
576 { printf("spin: allocated %ld Gb, wanted %d bytes more\n",
577 cnt/(1024*1024*1024), (int) n);
578 fatal("not enough memory", (char *)0);
579 }
580 cnt += (unsigned long) n;
581 memset(tmp, 0, n);
582 return tmp;
583 }
584
585 void
trapwonly(Lextok * n)586 trapwonly(Lextok *n /* , char *unused */)
587 { extern int realread;
588 short i = (n->sym)?n->sym->type:0;
589
590 if (i != MTYPE
591 && i != BIT
592 && i != BYTE
593 && i != SHORT
594 && i != INT
595 && i != UNSIGNED)
596 return;
597
598 if (realread)
599 n->sym->hidden |= 128; /* var is read at least once */
600 }
601
602 void
setaccess(Symbol * sp,Symbol * what,int cnt,int t)603 setaccess(Symbol *sp, Symbol *what, int cnt, int t)
604 { Access *a;
605
606 for (a = sp->access; a; a = a->lnk)
607 if (a->who == context
608 && a->what == what
609 && a->cnt == cnt
610 && a->typ == t)
611 return;
612
613 a = (Access *) emalloc(sizeof(Access));
614 a->who = context;
615 a->what = what;
616 a->cnt = cnt;
617 a->typ = t;
618 a->lnk = sp->access;
619 sp->access = a;
620 }
621
622 Lextok *
nn(Lextok * s,int t,Lextok * ll,Lextok * rl)623 nn(Lextok *s, int t, Lextok *ll, Lextok *rl)
624 { Lextok *n = (Lextok *) emalloc(sizeof(Lextok));
625 static int warn_nn = 0;
626
627 n->uiid = is_inline(); /* record origin of the statement */
628 n->ntyp = (short) t;
629 if (s && s->fn)
630 { n->ln = s->ln;
631 n->fn = s->fn;
632 } else if (rl && rl->fn)
633 { n->ln = rl->ln;
634 n->fn = rl->fn;
635 } else if (ll && ll->fn)
636 { n->ln = ll->ln;
637 n->fn = ll->fn;
638 } else
639 { n->ln = lineno;
640 n->fn = Fname;
641 }
642 if (s) n->sym = s->sym;
643 n->lft = ll;
644 n->rgt = rl;
645 n->indstep = DstepStart;
646
647 if (t == TIMEOUT) Etimeouts++;
648
649 if (!context) return n;
650
651 if (t == 'r' || t == 's')
652 setaccess(n->sym, ZS, 0, t);
653 if (t == 'R')
654 setaccess(n->sym, ZS, 0, 'P');
655
656 if (context->name == claimproc)
657 { int forbidden = separate;
658 switch (t) {
659 case ASGN:
660 printf("spin: Warning, never claim has side-effect\n");
661 break;
662 case 'r': case 's':
663 non_fatal("never claim contains i/o stmnts",(char *)0);
664 break;
665 case TIMEOUT:
666 /* never claim polls timeout */
667 if (Ntimeouts && Etimeouts)
668 forbidden = 0;
669 Ntimeouts++; Etimeouts--;
670 break;
671 case LEN: case EMPTY: case FULL:
672 case 'R': case NFULL: case NEMPTY:
673 /* status becomes non-exclusive */
674 if (n->sym && !(n->sym->xu&XX))
675 { n->sym->xu |= XX;
676 if (separate == 2) {
677 printf("spin: warning, make sure that the S1 model\n");
678 printf(" also polls channel '%s' in its claim\n",
679 n->sym->name);
680 } }
681 forbidden = 0;
682 break;
683 case 'c':
684 AST_track(n, 0); /* register as a slice criterion */
685 /* fall thru */
686 default:
687 forbidden = 0;
688 break;
689 }
690 if (forbidden)
691 { printf("spin: never, saw "); explain(t); printf("\n");
692 fatal("incompatible with separate compilation",(char *)0);
693 }
694 } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t))
695 { printf("spin: Warning, using %s outside never claim\n",
696 (t == ENABLED)?"enabled()":"pc_value()");
697 warn_nn |= t;
698 } else if (t == NONPROGRESS)
699 { fatal("spin: Error, using np_ outside never claim\n", (char *)0);
700 }
701 return n;
702 }
703
704 Lextok *
rem_lab(Symbol * a,Lextok * b,Symbol * c)705 rem_lab(Symbol *a, Lextok *b, Symbol *c) /* proctype name, pid, label name */
706 { Lextok *tmp1, *tmp2, *tmp3;
707
708 has_remote++;
709 c->type = LABEL; /* refered to in global context here */
710 fix_dest(c, a); /* in case target of rem_lab is jump */
711 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
712 tmp1 = nn(ZN, 'p', tmp1, ZN);
713 tmp1->sym = lookup("_p");
714 tmp2 = nn(ZN, NAME, ZN, ZN); tmp2->sym = a;
715 tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c;
716 return nn(ZN, EQ, tmp1, tmp3);
717 #if 0
718 .---------------EQ-------.
719 / \
720 'p' -sym-> _p 'q' -sym-> c (label name)
721 / /
722 '?' -sym-> a (proctype) NAME -sym-> a (proctype name)
723 /
724 b (pid expr)
725 #endif
726 }
727
728 Lextok *
rem_var(Symbol * a,Lextok * b,Symbol * c,Lextok * ndx)729 rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx)
730 { Lextok *tmp1;
731
732 has_remote++;
733 has_remvar++;
734 dataflow = 0; /* turn off dead variable resets 4.2.5 */
735 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
736 tmp1 = nn(ZN, 'p', tmp1, ndx);
737 tmp1->sym = c;
738 return tmp1;
739 #if 0
740 cannot refer to struct elements
741 only to scalars and arrays
742
743 'p' -sym-> c (variable name)
744 / \______ possible arrayindex on c
745 /
746 '?' -sym-> a (proctype)
747 /
748 b (pid expr)
749 #endif
750 }
751
752 void
explain(int n)753 explain(int n)
754 { FILE *fd = stdout;
755 switch (n) {
756 default: if (n > 0 && n < 256)
757 fprintf(fd, "'%c' = ", n);
758 fprintf(fd, "%d", n);
759 break;
760 case '\b': fprintf(fd, "\\b"); break;
761 case '\t': fprintf(fd, "\\t"); break;
762 case '\f': fprintf(fd, "\\f"); break;
763 case '\n': fprintf(fd, "\\n"); break;
764 case '\r': fprintf(fd, "\\r"); break;
765 case 'c': fprintf(fd, "condition"); break;
766 case 's': fprintf(fd, "send"); break;
767 case 'r': fprintf(fd, "recv"); break;
768 case 'R': fprintf(fd, "recv poll %s", Operator); break;
769 case '@': fprintf(fd, "@"); break;
770 case '?': fprintf(fd, "(x->y:z)"); break;
771 #if 1
772 case NEXT: fprintf(fd, "X"); break;
773 case ALWAYS: fprintf(fd, "[]"); break;
774 case EVENTUALLY: fprintf(fd, "<>"); break;
775 case IMPLIES: fprintf(fd, "->"); break;
776 case EQUIV: fprintf(fd, "<->"); break;
777 case UNTIL: fprintf(fd, "U"); break;
778 case WEAK_UNTIL: fprintf(fd, "W"); break;
779 case IN: fprintf(fd, "%sin", Keyword); break;
780 #endif
781 case ACTIVE: fprintf(fd, "%sactive", Keyword); break;
782 case AND: fprintf(fd, "%s&&", Operator); break;
783 case ASGN: fprintf(fd, "%s=", Operator); break;
784 case ASSERT: fprintf(fd, "%sassert", Function); break;
785 case ATOMIC: fprintf(fd, "%satomic", Keyword); break;
786 case BREAK: fprintf(fd, "%sbreak", Keyword); break;
787 case C_CODE: fprintf(fd, "%sc_code", Keyword); break;
788 case C_DECL: fprintf(fd, "%sc_decl", Keyword); break;
789 case C_EXPR: fprintf(fd, "%sc_expr", Keyword); break;
790 case C_STATE: fprintf(fd, "%sc_state",Keyword); break;
791 case C_TRACK: fprintf(fd, "%sc_track",Keyword); break;
792 case CLAIM: fprintf(fd, "%snever", Keyword); break;
793 case CONST: fprintf(fd, "a constant"); break;
794 case DECR: fprintf(fd, "%s--", Operator); break;
795 case D_STEP: fprintf(fd, "%sd_step", Keyword); break;
796 case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break;
797 case DO: fprintf(fd, "%sdo", Keyword); break;
798 case DOT: fprintf(fd, "."); break;
799 case ELSE: fprintf(fd, "%selse", Keyword); break;
800 case EMPTY: fprintf(fd, "%sempty", Function); break;
801 case ENABLED: fprintf(fd, "%senabled",Function); break;
802 case EQ: fprintf(fd, "%s==", Operator); break;
803 case EVAL: fprintf(fd, "%seval", Function); break;
804 case FI: fprintf(fd, "%sfi", Keyword); break;
805 case FULL: fprintf(fd, "%sfull", Function); break;
806 case GE: fprintf(fd, "%s>=", Operator); break;
807 case GOTO: fprintf(fd, "%sgoto", Keyword); break;
808 case GT: fprintf(fd, "%s>", Operator); break;
809 case HIDDEN: fprintf(fd, "%shidden", Keyword); break;
810 case IF: fprintf(fd, "%sif", Keyword); break;
811 case INCR: fprintf(fd, "%s++", Operator); break;
812 case INAME: fprintf(fd, "inline name"); break;
813 case INLINE: fprintf(fd, "%sinline", Keyword); break;
814 case INIT: fprintf(fd, "%sinit", Keyword); break;
815 case ISLOCAL: fprintf(fd, "%slocal", Keyword); break;
816 case LABEL: fprintf(fd, "a label-name"); break;
817 case LE: fprintf(fd, "%s<=", Operator); break;
818 case LEN: fprintf(fd, "%slen", Function); break;
819 case LSHIFT: fprintf(fd, "%s<<", Operator); break;
820 case LT: fprintf(fd, "%s<", Operator); break;
821 case MTYPE: fprintf(fd, "%smtype", Keyword); break;
822 case NAME: fprintf(fd, "an identifier"); break;
823 case NE: fprintf(fd, "%s!=", Operator); break;
824 case NEG: fprintf(fd, "%s! (not)",Operator); break;
825 case NEMPTY: fprintf(fd, "%snempty", Function); break;
826 case NFULL: fprintf(fd, "%snfull", Function); break;
827 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
828 case NONPROGRESS: fprintf(fd, "%snp_", Function); break;
829 case OD: fprintf(fd, "%sod", Keyword); break;
830 case OF: fprintf(fd, "%sof", Keyword); break;
831 case OR: fprintf(fd, "%s||", Operator); break;
832 case O_SND: fprintf(fd, "%s!!", Operator); break;
833 case PC_VAL: fprintf(fd, "%spc_value",Function); break;
834 case PNAME: fprintf(fd, "process name"); break;
835 case PRINT: fprintf(fd, "%sprintf", Function); break;
836 case PRINTM: fprintf(fd, "%sprintm", Function); break;
837 case PRIORITY: fprintf(fd, "%spriority", Keyword); break;
838 case PROCTYPE: fprintf(fd, "%sproctype",Keyword); break;
839 case PROVIDED: fprintf(fd, "%sprovided",Keyword); break;
840 case RCV: fprintf(fd, "%s?", Operator); break;
841 case R_RCV: fprintf(fd, "%s??", Operator); break;
842 case RSHIFT: fprintf(fd, "%s>>", Operator); break;
843 case RUN: fprintf(fd, "%srun", Operator); break;
844 case SEP: fprintf(fd, "token: ::"); break;
845 case SEMI: fprintf(fd, ";"); break;
846 case SHOW: fprintf(fd, "%sshow", Keyword); break;
847 case SND: fprintf(fd, "%s!", Operator); break;
848 case STRING: fprintf(fd, "a string"); break;
849 case TRACE: fprintf(fd, "%strace", Keyword); break;
850 case TIMEOUT: fprintf(fd, "%stimeout",Keyword); break;
851 case TYPE: fprintf(fd, "data typename"); break;
852 case TYPEDEF: fprintf(fd, "%stypedef",Keyword); break;
853 case XU: fprintf(fd, "%sx[rs]", Keyword); break;
854 case UMIN: fprintf(fd, "%s- (unary minus)", Operator); break;
855 case UNAME: fprintf(fd, "a typename"); break;
856 case UNLESS: fprintf(fd, "%sunless", Keyword); break;
857 }
858 }
859
860
861