1 /***** spin: main.c *****/
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 #include <stdlib.h>
10 #include <assert.h>
11 #include "spin.h"
12 #include "version.h"
13 #include <sys/types.h>
14 #include <sys/stat.h>
15 #include <signal.h>
16 #include <time.h>
17 #ifdef PC
18 #include <io.h>
19 #else
20 #include <unistd.h>
21 #endif
22 #include "y.tab.h"
23
24 extern int DstepStart, lineno, tl_terse;
25 extern FILE *yyin, *yyout, *tl_out;
26 extern Symbol *context;
27 extern char *claimproc;
28 extern void repro_src(void);
29 extern void qhide(int);
30 extern char CurScope[MAXSCOPESZ];
31 extern short has_provided, has_code, has_ltl, has_accept;
32 extern int realread, buzzed;
33 extern void ana_src(int, int);
34 extern void putprelude(void);
35
36 static void add_comptime(char *);
37 static void add_runtime(char *);
38
39 Symbol *Fname, *oFname;
40
41 int Etimeouts; /* nr timeouts in program */
42 int Ntimeouts; /* nr timeouts in never claim */
43 int analyze, columns, dumptab, has_remote, has_remvar;
44 int interactive, jumpsteps, m_loss, nr_errs, cutoff;
45 int s_trail, ntrail, verbose, xspin, notabs, rvopt;
46 int no_print, no_wrapup, Caccess, limited_vis, like_java;
47 int separate; /* separate compilation */
48 int export_ast; /* pangen5.c */
49 int norecompile; /* main.c */
50 int old_scope_rules; /* use pre 5.3.0 rules */
51 int old_priority_rules; /* use pre 6.2.0 rules */
52 int product, Strict;
53 short replay;
54
55 int merger = 1, deadvar = 1, implied_semis = 1;
56 int ccache = 0; /* oyvind teig: 5.2.0 case caching off by default */
57
58 static int preprocessonly, SeedUsed, itsr, itsr_n, sw_or_bt;
59 static int seedy; /* be verbose about chosen seed */
60 static int inlineonly; /* show inlined code */
61 static int dataflow = 1;
62
63 #if 0
64 meaning of flags on verbose:
65 1 -g global variable values
66 2 -l local variable values
67 4 -p all process actions
68 8 -r receives
69 16 -s sends
70 32 -v verbose
71 64 -w very verbose
72 #endif
73
74 static char Operator[] = "operator: ";
75 static char Keyword[] = "keyword: ";
76 static char Function[] = "function-name: ";
77 static char **add_ltl = (char **) 0;
78 static char **ltl_file = (char **) 0;
79 static char **nvr_file = (char **) 0;
80 static char *ltl_claims = (char *) 0;
81 static char *pan_runtime = "";
82 static char *pan_comptime = "";
83 static char *formula = NULL;
84 static FILE *fd_ltl = (FILE *) 0;
85 static char *PreArg[64];
86 static int PreCnt = 0;
87 static char out1[64];
88
89 char **trailfilename; /* new option 'k' */
90
91 void explain(int);
92
93 #ifndef CPP
94 /* to use visual C++:
95 #define CPP "cl -E/E"
96 or call spin as: spin -P"CL -E/E"
97
98 on OS2:
99 #define CPP "icc -E/Pd+ -E/Q+"
100 or call spin as: spin -P"icc -E/Pd+ -E/Q+"
101 make sure the -E arg is always at the end,
102 in each case, because the command line
103 can later be truncated at that point
104 */
105 #if 1
106 #define CPP "gcc -std=gnu99 -Wformat-overflow=0 -E -x c"
107 /* if gcc-4 is available, this setting is modified below */
108 #else
109 #if defined(PC) || defined(MAC)
110 #define CPP "gcc -std=gnu99 -E -x c"
111 #else
112 #ifdef SOLARIS
113 #define CPP "/usr/ccs/lib/cpp"
114 #else
115 #define CPP "cpp" /* sometimes: "/lib/cpp" */
116 #endif
117 #endif
118 #endif
119 #endif
120
121 static char PreProc[512];
122 extern int depth; /* at least some steps were made */
123
124 int
WhatSeed(void)125 WhatSeed(void)
126 {
127 return SeedUsed;
128 }
129
130 void
final_fiddle(void)131 final_fiddle(void)
132 { char *has_a, *has_l, *has_f;
133
134 /* no -a or -l but has_accept: add -a */
135 /* no -a or -l in pan_runtime: add -DSAFETY to pan_comptime */
136 /* -a or -l but no -f then add -DNOFAIR */
137
138 has_a = strstr(pan_runtime, "-a");
139 has_l = strstr(pan_runtime, "-l");
140 has_f = strstr(pan_runtime, "-f");
141
142 if (!has_l && !has_a && strstr(pan_comptime, "-DNP"))
143 { add_runtime("-l");
144 has_l = strstr(pan_runtime, "-l");
145 }
146
147 if (!has_a && !has_l
148 && !strstr(pan_comptime, "-DSAFETY"))
149 { if (has_accept
150 && !strstr(pan_comptime, "-DBFS")
151 && !strstr(pan_comptime, "-DNOCLAIM"))
152 { add_runtime("-a");
153 has_a = pan_runtime;
154 } else
155 { add_comptime("-DSAFETY");
156 } }
157
158 if ((has_a || has_l) && !has_f
159 && !strstr(pan_comptime, "-DNOFAIR"))
160 { add_comptime("-DNOFAIR");
161 }
162 }
163
164 static int
change_param(char * t,char * what,int range,int bottom)165 change_param(char *t, char *what, int range, int bottom)
166 { char *ptr;
167 int v;
168
169 assert(range < 1000 && range > 0);
170 if ((ptr = strstr(t, what)) != NULL)
171 { ptr += strlen(what);
172 if (!isdigit((int) *ptr))
173 { return 0;
174 }
175 v = atoi(ptr) + 1; /* was: v = (atoi(ptr)+1)%range */
176 if (v >= range)
177 { v = bottom;
178 }
179 if (v >= 100)
180 { *ptr++ = '0' + (v/100); v %= 100;
181 *ptr++ = '0' + (v/10);
182 *ptr = '0' + (v%10);
183 } else if (v >= 10)
184 { *ptr++ = '0' + (v/10);
185 *ptr++ = '0' + (v%10);
186 *ptr = ' ';
187 } else
188 { *ptr++ = '0' + v;
189 *ptr++ = ' ';
190 *ptr = ' ';
191 } }
192 return 1;
193 }
194
195 static void
change_rs(char * t)196 change_rs(char *t)
197 { char *ptr;
198 int cnt = 0;
199 long v;
200
201 if ((ptr = strstr(t, "-RS")) != NULL)
202 { ptr += 3;
203 /* room for at least 10 digits */
204 v = Rand()%1000000000L;
205 while (v/10 > 0)
206 { *ptr++ = '0' + v%10;
207 v /= 10;
208 cnt++;
209 }
210 *ptr++ = '0' + v;
211 cnt++;
212 while (cnt++ < 10)
213 { *ptr++ = ' ';
214 } }
215 }
216
217 int
omit_str(char * in,char * s)218 omit_str(char *in, char *s)
219 { char *ptr = strstr(in, s);
220 int i, nr = -1;
221
222 if (ptr)
223 { for (i = 0; i < (int) strlen(s); i++)
224 { *ptr++ = ' ';
225 }
226 if (isdigit((int) *ptr))
227 { nr = atoi(ptr);
228 while (isdigit((int) *ptr))
229 { *ptr++ = ' ';
230 } } }
231 return nr;
232 }
233
234 void
string_trim(char * t)235 string_trim(char *t)
236 { int n = strlen(t) - 1;
237
238 while (n > 0 && t[n] == ' ')
239 { t[n--] = '\0';
240 }
241 }
242
243 int
e_system(int v,const char * s)244 e_system(int v, const char *s)
245 { static int count = 1;
246
247 /* v == 0 : checks to find non-linked version of gcc */
248 /* v == 1 : all other commands */
249 /* v == 2 : preprocessing the promela input */
250
251 if (v == 1)
252 { if (verbose&(32|64)) /* -v or -w */
253 { printf("cmd%02d: %s\n", count++, s);
254 fflush(stdout);
255 }
256 if (verbose&64) /* only -w */
257 { return 0; /* suppress the call to system(s) */
258 } }
259 return system(s);
260 }
261
262 void
alldone(int estatus)263 alldone(int estatus)
264 { char *ptr;
265 #if defined(WIN32) || defined(WIN64)
266 struct _stat x;
267 #else
268 struct stat x;
269 #endif
270 if (preprocessonly == 0 && strlen(out1) > 0)
271 { (void) unlink((const char *) out1);
272 }
273
274 (void) unlink(TMP_FILE1);
275 (void) unlink(TMP_FILE2);
276
277 if (!buzzed && seedy && !analyze && !export_ast
278 && !s_trail && !preprocessonly && depth > 0)
279 { printf("seed used: %d\n", SeedUsed);
280 }
281
282 if (!buzzed && xspin && (analyze || s_trail))
283 { if (estatus)
284 { printf("spin: %d error(s) - aborting\n",
285 estatus);
286 } else
287 { printf("Exit-Status 0\n");
288 } }
289
290 if (buzzed && replay && !has_code && !estatus)
291 { extern QH *qh_lst;
292 QH *j;
293 int i;
294
295 pan_runtime = (char *) emalloc(2048); /* more than enough */
296 sprintf(pan_runtime, "-n%d ", SeedUsed);
297 if (jumpsteps)
298 { sprintf(&pan_runtime[strlen(pan_runtime)], "-j%d ", jumpsteps);
299 }
300 if (trailfilename)
301 { sprintf(&pan_runtime[strlen(pan_runtime)], "-k%s ", *trailfilename);
302 }
303 if (cutoff)
304 { sprintf(&pan_runtime[strlen(pan_runtime)], "-u%d ", cutoff);
305 }
306 for (i = 1; i <= PreCnt; i++)
307 { strcat(pan_runtime, PreArg[i]);
308 strcat(pan_runtime, " ");
309 }
310 for (j = qh_lst; j; j = j->nxt)
311 { sprintf(&pan_runtime[strlen(pan_runtime)], "-q%d ", j->n);
312 }
313 if (strcmp(PreProc, CPP) != 0)
314 { sprintf(&pan_runtime[strlen(pan_runtime)], "\"-P%s\" ", PreProc);
315 }
316 /* -oN options 1..5 are ignored in simulations */
317 if (old_priority_rules) strcat(pan_runtime, "-o6 ");
318 if (!implied_semis) strcat(pan_runtime, "-o7 ");
319 if (no_print) strcat(pan_runtime, "-b ");
320 if (no_wrapup) strcat(pan_runtime, "-B ");
321 if (columns == 1) strcat(pan_runtime, "-c ");
322 if (columns == 2) strcat(pan_runtime, "-M ");
323 if (seedy == 1) strcat(pan_runtime, "-h ");
324 if (like_java == 1) strcat(pan_runtime, "-J ");
325 if (old_scope_rules) strcat(pan_runtime, "-O ");
326 if (notabs) strcat(pan_runtime, "-T ");
327 if (verbose&1) strcat(pan_runtime, "-g ");
328 if (verbose&2) strcat(pan_runtime, "-l ");
329 if (verbose&4) strcat(pan_runtime, "-p ");
330 if (verbose&8) strcat(pan_runtime, "-r ");
331 if (verbose&16) strcat(pan_runtime, "-s ");
332 if (verbose&32) strcat(pan_runtime, "-v ");
333 if (verbose&64) strcat(pan_runtime, "-w ");
334 if (m_loss) strcat(pan_runtime, "-m ");
335
336 char *tmp = (char *) emalloc(strlen("spin -t") +
337 strlen(pan_runtime) + strlen(Fname->name) + 8);
338
339 sprintf(tmp, "spin -t %s %s", pan_runtime, Fname->name);
340 estatus = e_system(1, tmp); /* replay */
341 exit(estatus); /* replay without c_code */
342 }
343
344 if (buzzed && (!replay || has_code) && !estatus)
345 { char *tmp, *tmp2 = NULL, *P_X;
346 char *C_X = (buzzed == 2) ? "-O" : "";
347
348 if (replay && strlen(pan_comptime) == 0)
349 {
350 #if defined(WIN32) || defined(WIN64)
351 P_X = "pan";
352 #else
353 P_X = "./pan";
354 #endif
355 if (stat(P_X, (struct stat *)&x) < 0)
356 { goto recompile; /* no executable pan for replay */
357 }
358 tmp = (char *) emalloc(8 + strlen(P_X) + strlen(pan_runtime) +4);
359 /* the final +4 is too allow adding " &" in some cases */
360 sprintf(tmp, "%s %s", P_X, pan_runtime);
361 goto runit;
362 }
363 #if defined(WIN32) || defined(WIN64)
364 P_X = "-o pan pan.c && pan";
365 #else
366 P_X = "-o pan pan.c && ./pan";
367 #endif
368 /* swarm and biterate randomization additions */
369 if (!replay && itsr) /* iterative search refinement */
370 { if (!strstr(pan_comptime, "-DBITSTATE"))
371 { add_comptime("-DBITSTATE");
372 }
373 if (!strstr(pan_comptime, "-DPUTPID"))
374 { add_comptime("-DPUTPID");
375 }
376 if (!strstr(pan_comptime, "-DT_RAND")
377 && !strstr(pan_comptime, "-DT_REVERSE"))
378 { add_runtime("-T0 "); /* controls t_reverse */
379 }
380 if (!strstr(pan_runtime, "-P") /* runtime flag */
381 || pan_runtime[2] < '0'
382 || pan_runtime[2] > '1') /* no -P0 or -P1 */
383 { add_runtime("-P0 "); /* controls p_reverse */
384 }
385 if (!strstr(pan_runtime, "-w"))
386 { add_runtime("-w18 "); /* -w18 = 256K */
387 } else
388 { char nv[32];
389 int x;
390 x = omit_str(pan_runtime, "-w");
391 if (x >= 0)
392 { sprintf(nv, "-w%d ", x);
393 add_runtime(nv); /* added spaces */
394 } }
395 if (!strstr(pan_runtime, "-h"))
396 { add_runtime("-h0 "); /* 0..499 */
397 /* leave 2 spaces for increments up to -h499 */
398 } else if (!strstr(pan_runtime, "-hash"))
399 { char nv[32];
400 int x;
401 x = omit_str(pan_runtime, "-h");
402 if (x >= 0)
403 { sprintf(nv, "-h%d ", x%500);
404 add_runtime(nv); /* added spaces */
405 } }
406 if (!strstr(pan_runtime, "-k"))
407 { add_runtime("-k1 "); /* 1..3 */
408 } else
409 { char nv[32];
410 int x;
411 x = omit_str(pan_runtime, "-k");
412 if (x >= 0)
413 { sprintf(nv, "-k%d ", x%4);
414 add_runtime(nv); /* added spaces */
415 } }
416 if (strstr(pan_runtime, "-p_rotate"))
417 { char nv[32];
418 int x;
419 x = omit_str(pan_runtime, "-p_rotate");
420 if (x < 0)
421 { x = 0;
422 }
423 sprintf(nv, "-p_rotate%d ", x%256);
424 add_runtime(nv); /* added spaces */
425 } else if (strstr(pan_runtime, "-p_permute") == 0)
426 { add_runtime("-p_rotate0 ");
427 }
428 if (strstr(pan_runtime, "-RS"))
429 { (void) omit_str(pan_runtime, "-RS");
430 }
431 /* need room for at least 10 digits */
432 add_runtime("-RS1234567890 ");
433 change_rs(pan_runtime);
434 }
435 recompile:
436 if (strstr(PreProc, "cpp")) /* unix/linux */
437 { strcpy(PreProc, "gcc"); /* need compiler */
438 } else if ((tmp = strstr(PreProc, "-E")) != NULL)
439 { *tmp = '\0'; /* strip preprocessing flags */
440 }
441
442 final_fiddle();
443 tmp = (char *) emalloc(8 + /* account for alignment */
444 strlen(PreProc) +
445 strlen(C_X) +
446 strlen(pan_comptime) +
447 strlen(P_X) +
448 strlen(pan_runtime) +
449 strlen(" -p_reverse & "));
450 tmp2 = tmp;
451
452 /* P_X ends with " && ./pan " */
453 sprintf(tmp, "%s %s %s %s %s",
454 PreProc, C_X, pan_comptime, P_X, pan_runtime);
455
456 if (!replay)
457 { if (itsr < 0) /* swarm only */
458 { strcat(tmp, " &"); /* after ./pan */
459 itsr = -itsr; /* now same as biterate */
460 }
461 /* do compilation first
462 * split cc command from run command
463 * leave cc in tmp, and set tmp2 to run
464 */
465 if ((ptr = strstr(tmp, " && ")) != NULL)
466 { tmp2 = ptr + 4; /* first run */
467 *ptr = '\0';
468 } }
469
470 if (has_ltl)
471 { (void) unlink("_spin_nvr.tmp");
472 }
473
474 if (!norecompile)
475 { /* make sure that if compilation fails we do not continue */
476 #ifdef PC
477 (void) unlink("./pan.exe");
478 #else
479 (void) unlink("./pan");
480 #endif
481 }
482 runit:
483 if (norecompile && tmp != tmp2)
484 { estatus = 0;
485 } else
486 { estatus = e_system(1, tmp); /* compile or run */
487 }
488 if (replay || estatus < 0)
489 { goto skipahead;
490 }
491 /* !replay */
492 if (itsr == 0 && !sw_or_bt) /* single run */
493 { estatus = e_system(1, tmp2);
494 } else if (itsr > 0) /* iterative search refinement */
495 { int is_swarm = 0;
496 if (tmp2 != tmp) /* swarm: did only compilation so far */
497 { tmp = tmp2; /* now we point to the run command */
498 estatus = e_system(1, tmp); /* first run */
499 itsr--;
500 }
501 itsr--; /* count down */
502
503 /* the following are added back randomly later */
504 (void) omit_str(tmp, "-p_reverse"); /* replaced by spaces */
505 (void) omit_str(tmp, "-p_normal");
506
507 if (strstr(tmp, " &") != NULL)
508 { (void) omit_str(tmp, " &");
509 is_swarm = 1;
510 }
511
512 /* increase -w every itsr_n-th run */
513 if ((itsr_n > 0 && (itsr == 0 || (itsr%itsr_n) != 0))
514 || (change_param(tmp, "-w", 36, 18) >= 0)) /* max 4G bit statespace */
515 { (void) change_param(tmp, "-h", 500, 0); /* hash function 0.499 */
516 (void) change_param(tmp, "-p_rotate", 256, 0); /* if defined */
517 (void) change_param(tmp, "-k", 4, 1); /* nr bits per state 0->1,2,3 */
518 (void) change_param(tmp, "-T", 2, 0); /* with or without t_reverse*/
519 (void) change_param(tmp, "-P", 2, 0); /* -P 0..1 != p_reverse */
520 change_rs(tmp); /* change random seed */
521 string_trim(tmp);
522 if (rand()%5 == 0) /* 20% of all runs */
523 { strcat(tmp, " -p_reverse ");
524 /* at end, so this overrides -p_rotateN, if there */
525 /* but -P0..1 disable this in 50% of the cases */
526 /* so its really activated in 10% of all runs */
527 } else if (rand()%6 == 0) /* override p_rotate and p_reverse */
528 { strcat(tmp, " -p_normal ");
529 }
530 if (is_swarm)
531 { strcat(tmp, " &");
532 }
533 goto runit;
534 } }
535 skipahead:
536 (void) unlink("pan.b");
537 (void) unlink("pan.c");
538 (void) unlink("pan.h");
539 (void) unlink("pan.m");
540 (void) unlink("pan.p");
541 (void) unlink("pan.t");
542 }
543 exit(estatus);
544 }
545 #if 0
546 -P0 normal active process creation
547 -P1 reversed order for *active* process creation != p_reverse
548
549 -T0 normal transition exploration
550 -T1 reversed order of transition exploration
551
552 -DP_RAND (random starting point +- -DP_REVERSE)
553 -DPERMUTED (also enables -p_rotateN and -p_reverse)
554 -DP_REVERSE (same as -DPERMUTED with -p_reverse, but 7% faster)
555
556 -DT_RAND (random starting point -- optionally with -T0..1)
557 -DT_REVERSE (superseded by -T0..1 options)
558
559 -hash generates new hash polynomial for -h0
560
561 permutation modes:
562 -permuted (adds -DPERMUTED) -- this is also the default with -swarm
563 -t_reverse (same as -T1)
564 -p_reverse (similar to -P1)
565 -p_rotateN
566 -p_normal
567
568 less useful would be (since there is less non-determinism in transitions):
569 -t_rotateN -- a controlled version of -DT_RAND
570
571 compiling with -DPERMUTED enables a number of new runtime options,
572 that -swarmN,M will also exploit:
573 -p_permute (default)
574 -p_rotateN
575 -p_reverse
576 #endif
577
578 void
preprocess(char * a,char * b,int a_tmp)579 preprocess(char *a, char *b, int a_tmp)
580 { char precmd[1024], cmd[2048];
581 int i;
582 #ifdef PC
583 /* gcc is sometimes a symbolic link to gcc-4
584 that does not work well in cygwin, so we try
585 to use the actual executable that is used.
586 the code below assumes we are on a cygwin-like system
587 */
588 if (strncmp(PreProc, "gcc ", strlen("gcc ")) == 0)
589 { if (e_system(0, "gcc-4 --version > pan.pre 2>&1") == 0)
590 { strcpy(PreProc, "gcc-4 -std=gnu99 -Wformat-overflow=0 -E -x c");
591 } else if (e_system(0, "gcc-3 --version > pan.pre 2>&1") == 0)
592 { strcpy(PreProc, "gcc-3 -std=gnu99 -Wformat-overflow=0 -E -x c");
593 } }
594 #endif
595
596 assert(strlen(PreProc) < sizeof(precmd));
597 strcpy(precmd, PreProc);
598 for (i = 1; i <= PreCnt; i++)
599 { strcat(precmd, " ");
600 strcat(precmd, PreArg[i]);
601 }
602 if (strlen(precmd) > sizeof(precmd))
603 { fprintf(stdout, "spin: too many -D args, aborting\n");
604 alldone(1);
605 }
606 sprintf(cmd, "%s \"%s\" > \"%s\"", precmd, a, b);
607 if (e_system(2, (const char *)cmd)) /* preprocessing step */
608 { (void) unlink((const char *) b);
609 if (a_tmp) (void) unlink((const char *) a);
610 fprintf(stdout, "spin: preprocessing failed %s\n", cmd);
611 alldone(1); /* no return, error exit */
612 }
613 if (a_tmp) (void) unlink((const char *) a);
614 }
615
616 void
usage(void)617 usage(void)
618 {
619 printf("use: spin [-option] ... [-option] file\n");
620 printf("\tNote: file must always be the last argument\n");
621 printf("\t-A apply slicing algorithm\n");
622 printf("\t-a generate a verifier in pan.c\n");
623 printf("\t-B no final state details in simulations\n");
624 printf("\t-b don't execute printfs in simulation\n");
625 printf("\t-C print channel access info (combine with -g etc.)\n");
626 printf("\t-c columnated -s -r simulation output\n");
627 printf("\t-d produce symbol-table information\n");
628 printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
629 printf("\t-Eyyy pass yyy to the preprocessor\n");
630 printf("\t-e compute synchronous product of multiple never claims (modified by -L)\n");
631 printf("\t-f \"..formula..\" translate LTL ");
632 printf("into never claim\n");
633 printf("\t-F file like -f, but with the LTL formula stored in a 1-line file\n");
634 printf("\t-g print all global variables\n");
635 printf("\t-h at end of run, print value of seed for random nr generator used\n");
636 printf("\t-i interactive (random simulation)\n");
637 printf("\t-I show result of inlining and preprocessing\n");
638 printf("\t-J reverse eval order of nested unlesses\n");
639 printf("\t-jN skip the first N steps ");
640 printf("in simulation trail\n");
641 printf("\t-k fname use the trailfile stored in file fname, see also -t\n");
642 printf("\t-L when using -e, use strict language intersection\n");
643 printf("\t-l print all local variables\n");
644 printf("\t-M generate msc-flow in tcl/tk format\n");
645 printf("\t-m lose msgs sent to full queues\n");
646 printf("\t-N fname use never claim stored in file fname\n");
647 printf("\t-nN seed for random nr generator\n");
648 printf("\t-O use old scope rules (pre 5.3.0)\n");
649 printf("\t-o1 turn off dataflow-optimizations in verifier\n");
650 printf("\t-o2 don't hide write-only variables in verifier\n");
651 printf("\t-o3 turn off statement merging in verifier\n");
652 printf("\t-o4 turn on rendezvous optiomizations in verifier\n");
653 printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\n");
654 printf("\t-o6 revert to the old rules for interpreting priority tags (pre version 6.2)\n");
655 printf("\t-o7 revert to the old rules for semi-colon usage (pre version 6.3)\n");
656 printf("\t-Pxxx use xxx for preprocessing\n");
657 printf("\t-p print all statements\n");
658 printf("\t-pp pretty-print (reformat) stdin, write stdout\n");
659 printf("\t-qN suppress io for queue N in printouts\n");
660 printf("\t-r print receive events\n");
661 printf("\t-replay replay an error trail-file found earlier\n");
662 printf("\t if the model contains embedded c-code, the ./pan executable is used\n");
663 printf("\t otherwise spin itself is used to replay the trailfile\n");
664 printf("\t note that pan recognizes different runtime options than spin itself\n");
665 printf("\t-run (or -search) generate a verifier, and compile and run it\n");
666 printf("\t options before -search are interpreted by spin to parse the input\n");
667 printf("\t options following a -search are used to compile and run the verifier pan\n");
668 printf("\t valid options that can follow a -search argument include:\n");
669 printf("\t -bfs perform a breadth-first search\n");
670 printf("\t -bfspar perform a parallel breadth-first search\n");
671 printf("\t -dfspar perform a parallel depth-first search, same as -DNCORE=4\n");
672 printf("\t -bcs use the bounded-context-switching algorithm\n");
673 printf("\t -bitstate or -bit, use bitstate storage\n");
674 printf("\t -biterateN,M use bitstate with iterative search refinement (-w18..-w35)\n");
675 printf("\t perform N randomized runs and increment -w every M runs\n");
676 printf("\t default value for N is 10, default for M is 1\n");
677 printf("\t (use N,N to keep -w fixed for all runs)\n");
678 printf("\t (add -w to see which commands will be executed)\n");
679 printf("\t (add -W if ./pan exists and need not be recompiled)\n");
680 printf("\t -swarmN,M like -biterate, but running all iterations in parallel\n");
681 printf("\t -link file.c link executable pan to file.c\n");
682 printf("\t -collapse use collapse state compression\n");
683 printf("\t -noreduce do not use partial order reduction\n");
684 printf("\t -hc use hash-compact storage\n");
685 printf("\t -noclaim ignore all ltl and never claims\n");
686 printf("\t -p_permute use process scheduling order random permutation\n");
687 printf("\t -p_rotateN use process scheduling order rotation by N\n");
688 printf("\t -p_reverse use process scheduling order reversal\n");
689 printf("\t -rhash randomly pick one of the -p_... options\n");
690 printf("\t -ltl p verify the ltl property named p\n");
691 printf("\t -safety compile for safety properties only\n");
692 printf("\t -i use the dfs iterative shortening algorithm\n");
693 printf("\t -a search for acceptance cycles\n");
694 printf("\t -l search for non-progress cycles\n");
695 printf("\t similarly, a -D... parameter can be specified to modify the compilation\n");
696 printf("\t and any valid runtime pan argument can be specified for the verification\n");
697 printf("\t-S1 and -S2 separate pan source for claim and model\n");
698 printf("\t-s print send events\n");
699 printf("\t-T do not indent printf output\n");
700 printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
701 printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
702 printf("\t-uN stop a simulation run after N steps\n");
703 printf("\t-v verbose, more warnings\n");
704 printf("\t-w very verbose (when combined with -l or -g)\n");
705 printf("\t-[XYZ] reserved for use by xspin interface\n");
706 printf("\t-V print version number and exit\n");
707 alldone(1);
708 }
709
710 int
optimizations(int nr)711 optimizations(int nr)
712 {
713 switch (nr) {
714 case '1':
715 dataflow = 1 - dataflow; /* dataflow */
716 if (verbose&32)
717 printf("spin: dataflow optimizations turned %s\n",
718 dataflow?"on":"off");
719 break;
720 case '2':
721 /* dead variable elimination */
722 deadvar = 1 - deadvar;
723 if (verbose&32)
724 printf("spin: dead variable elimination turned %s\n",
725 deadvar?"on":"off");
726 break;
727 case '3':
728 /* statement merging */
729 merger = 1 - merger;
730 if (verbose&32)
731 printf("spin: statement merging turned %s\n",
732 merger?"on":"off");
733 break;
734
735 case '4':
736 /* rv optimization */
737 rvopt = 1 - rvopt;
738 if (verbose&32)
739 printf("spin: rendezvous optimization turned %s\n",
740 rvopt?"on":"off");
741 break;
742 case '5':
743 /* case caching */
744 ccache = 1 - ccache;
745 if (verbose&32)
746 printf("spin: case caching turned %s\n",
747 ccache?"on":"off");
748 break;
749 case '6':
750 old_priority_rules = 1;
751 if (verbose&32)
752 printf("spin: using old priority rules (pre version 6.2)\n");
753 return 0; /* no break */
754 case '7':
755 implied_semis = 0;
756 if (verbose&32)
757 printf("spin: no implied semi-colons (pre version 6.3)\n");
758 return 0; /* no break */
759 default:
760 printf("spin: bad or missing parameter on -o\n");
761 usage();
762 break;
763 }
764 return 1;
765 }
766
767 static void
add_comptime(char * s)768 add_comptime(char *s)
769 { char *tmp;
770
771 if (!s || strstr(pan_comptime, s))
772 { return;
773 }
774
775 tmp = (char *) emalloc(strlen(pan_comptime)+strlen(s)+2);
776 sprintf(tmp, "%s %s", pan_comptime, s);
777 pan_comptime = tmp;
778 }
779
780 static struct {
781 char *ifsee, *thendo;
782 int keeparg;
783 } pats[] = {
784 { "-bfspar", "-DBFS_PAR", 0 },
785 { "-bfs", "-DBFS", 0 },
786 { "-bcs", "-DBCS", 0 },
787 { "-bitstate", "-DBITSTATE", 0 },
788 { "-bit", "-DBITSTATE", 0 },
789 { "-hc", "-DHC4", 0 },
790 { "-collapse", "-DCOLLAPSE", 0 },
791 { "-noclaim", "-DNOCLAIM", 0 },
792 { "-noreduce", "-DNOREDUCE", 0 },
793 { "-np", "-DNP", 0 },
794 { "-permuted", "-DPERMUTED", 0 },
795 { "-p_permute", "-DPERMUTED", 1 },
796 { "-p_rotate", "-DPERMUTED", 1 },
797 { "-p_reverse", "-DPERMUTED", 1 },
798 { "-rhash", "-DPERMUTED", 1 },
799 { "-safety", "-DSAFETY", 0 },
800 { "-i", "-DREACH", 1 },
801 { "-l", "-DNP", 1 },
802 { 0, 0 }
803 };
804
805 static void
set_itsr_n(char * s)806 set_itsr_n(char *s) /* e.g., -swarm12,3 */
807 { char *tmp;
808
809 if ((tmp = strchr(s, ',')) != NULL)
810 { tmp++;
811 if (*tmp != '\0' && isdigit((int) *tmp))
812 { itsr_n = atoi(tmp);
813 if (itsr_n < 2)
814 { itsr_n = 0;
815 } } }
816 }
817
818 static void
add_runtime(char * s)819 add_runtime(char *s)
820 { char *tmp;
821 int i;
822
823 if (strncmp(s, "-biterate", strlen("-biterate")) == 0)
824 { itsr = 10; /* default nr of sequential iterations */
825 sw_or_bt = 1;
826 if (isdigit((int) s[9]))
827 { itsr = atoi(&s[9]);
828 if (itsr < 1)
829 { itsr = 1;
830 }
831 set_itsr_n(s);
832 }
833 return;
834 }
835 if (strncmp(s, "-swarm", strlen("-swarm")) == 0)
836 { itsr = -10; /* parallel iterations */
837 sw_or_bt = 1;
838 if (isdigit((int) s[6]))
839 { itsr = atoi(&s[6]);
840 if (itsr < 1)
841 { itsr = 1;
842 }
843 itsr = -itsr;
844 set_itsr_n(s);
845 }
846 return;
847 }
848
849 for (i = 0; pats[i].ifsee; i++)
850 { if (strncmp(s, pats[i].ifsee, strlen(pats[i].ifsee)) == 0)
851 { add_comptime(pats[i].thendo);
852 if (pats[i].keeparg)
853 { break;
854 }
855 return;
856 } }
857 if (strncmp(s, "-dfspar", strlen("-dfspar")) == 0)
858 { add_comptime("-DNCORE=4");
859 return;
860 }
861
862 tmp = (char *) emalloc(strlen(pan_runtime)+strlen(s)+2);
863 sprintf(tmp, "%s %s", pan_runtime, s);
864 pan_runtime = tmp;
865 }
866
867 ssize_t
getline(char ** lineptr,size_t * n,FILE * stream)868 getline(char **lineptr, size_t *n, FILE *stream)
869 { static char buffer[8192];
870
871 *lineptr = (char *) &buffer;
872
873 if (!fgets(buffer, sizeof(buffer), stream))
874 { return 0;
875 }
876 return 1;
877 }
878
879 int
main(int argc,char * argv[])880 main(int argc, char *argv[])
881 { Symbol *s;
882 int T = (int) time((time_t *)0);
883 int usedopts = 0;
884
885 yyin = stdin;
886 yyout = stdout;
887 tl_out = stdout;
888 strcpy(CurScope, "_");
889
890 assert(strlen(CPP) < sizeof(PreProc));
891 strcpy(PreProc, CPP);
892
893 /* unused flags: y, z, G, L, Q, R, W */
894 while (argc > 1 && argv[1][0] == '-')
895 { switch (argv[1][1]) {
896 case 'A': export_ast = 1; break;
897 case 'a': analyze = 1; break;
898 case 'B': no_wrapup = 1; break;
899 case 'b': no_print = 1; break;
900 case 'C': Caccess = 1; break;
901 case 'c': columns = 1; break;
902 case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
903 break; /* define */
904 case 'd': dumptab = 1; break;
905 case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
906 break;
907 case 'e': product++; break; /* see also 'L' */
908 case 'F': ltl_file = (char **) (argv+2);
909 argc--; argv++; break;
910 case 'f': add_ltl = (char **) argv;
911 argc--; argv++; break;
912 case 'g': verbose += 1; break;
913 case 'h': seedy = 1; break;
914 case 'i': interactive = 1; break;
915 case 'I': inlineonly = 1; break;
916 case 'J': like_java = 1; break;
917 case 'j': jumpsteps = atoi(&argv[1][2]); break;
918 case 'k': s_trail = 1;
919 trailfilename = (char **) (argv+2);
920 argc--; argv++; break;
921 case 'L': Strict++; break; /* modified -e */
922 case 'l': verbose += 2; break;
923 case 'M': columns = 2; break;
924 case 'm': m_loss = 1; break;
925 case 'N': nvr_file = (char **) (argv+2);
926 argc--; argv++; break;
927 case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
928 case 'O': old_scope_rules = 1; break;
929 case 'o': usedopts += optimizations(argv[1][2]); break;
930 case 'P': assert(strlen((const char *) &argv[1][2]) < sizeof(PreProc));
931 strcpy(PreProc, (const char *) &argv[1][2]);
932 break;
933 case 'p': if (argv[1][2] == 'p')
934 { pretty_print();
935 alldone(0);
936 }
937 verbose += 4; break;
938 case 'q': if (isdigit((int) argv[1][2]))
939 qhide(atoi(&argv[1][2]));
940 break;
941 case 'r':
942 if (strcmp(&argv[1][1], "run") == 0)
943 { Srand((unsigned int) T);
944 samecase: if (buzzed != 0)
945 { fatal("cannot combine -x with -run -replay or -search", (char *)0);
946 }
947 buzzed = 2;
948 analyze = 1;
949 argc--; argv++;
950 /* process all remaining arguments, except -w/-W, as relating to pan: */
951 while (argc > 1 && argv[1][0] == '-')
952 { switch (argv[1][1]) {
953 case 'D': /* eg -DNP */
954 /* case 'E': conflicts with runtime arg */
955 case 'O': /* eg -O2 */
956 case 'U': /* to undefine a macro */
957 add_comptime(argv[1]);
958 break;
959 #if 0
960 case 'w': /* conflicts with bitstate runtime arg */
961 verbose += 64;
962 break;
963 #endif
964 case 'W':
965 norecompile = 1;
966 break;
967 case 'l':
968 if (strcmp(&argv[1][1], "ltl") == 0)
969 { add_runtime("-N");
970 argc--; argv++;
971 add_runtime(argv[1]); /* prop name */
972 break;
973 }
974 if (strcmp(&argv[1][1], "link") == 0)
975 { argc--; argv++;
976 add_comptime(argv[1]);
977 break;
978 }
979 /* else fall through */
980 default:
981 add_runtime(argv[1]); /* -bfs etc. */
982 break;
983 }
984 argc--; argv++;
985 }
986 argc++; argv--;
987 } else if (strcmp(&argv[1][1], "replay") == 0)
988 { replay = 1;
989 add_runtime("-r");
990 goto samecase;
991 } else
992 { verbose += 8;
993 }
994 break;
995 case 'S': separate = atoi(&argv[1][2]); /* S1 or S2 */
996 /* generate code for separate compilation */
997 analyze = 1; break;
998 case 's':
999 if (strcmp(&argv[1][1], "simulate") == 0)
1000 { break; /* ignore */
1001 }
1002 if (strcmp(&argv[1][1], "search") == 0)
1003 { goto samecase;
1004 }
1005 verbose += 16; break;
1006 case 'T': notabs = 1; break;
1007 case 't': s_trail = 1;
1008 if (isdigit((int)argv[1][2]))
1009 { ntrail = atoi(&argv[1][2]);
1010 }
1011 break;
1012 case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
1013 break; /* undefine */
1014 case 'u': cutoff = atoi(&argv[1][2]); break;
1015 case 'v': verbose += 32; break;
1016 case 'V': printf("%s\n", SpinVersion);
1017 alldone(0);
1018 break;
1019 case 'w': verbose += 64; break;
1020 case 'W': norecompile = 1; break; /* 6.4.7: for swarm/biterate */
1021 case 'x': /* internal - reserved use */
1022 if (buzzed != 0)
1023 { fatal("cannot combine -x with -run -search or -replay", (char *)0);
1024 }
1025 buzzed = 1; /* implies also -a -o3 */
1026 pan_runtime = "-d";
1027 analyze = 1;
1028 usedopts += optimizations('3');
1029 break;
1030 case 'X': xspin = notabs = 1;
1031 #ifndef PC
1032 signal(SIGPIPE, alldone); /* not posix... */
1033 #endif
1034 break;
1035 case 'Y': limited_vis = 1; break; /* used by xspin */
1036 case 'Z': preprocessonly = 1; break; /* used by xspin */
1037
1038 default : usage(); break;
1039 }
1040 argc--; argv++;
1041 }
1042
1043 if (columns == 2 && !cutoff)
1044 { cutoff = 1024;
1045 }
1046
1047 if (usedopts && !analyze)
1048 printf("spin: warning -o[1..5] option ignored in simulations\n");
1049
1050 if (ltl_file)
1051 { add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
1052 if (!(tl_out = fopen(*ltl_file, "r")))
1053 { printf("spin: cannot open %s\n", *ltl_file);
1054 alldone(1);
1055 }
1056 size_t linebuffsize = 0;
1057 ssize_t length = getline(&formula, &linebuffsize, tl_out);
1058 if (!formula || !length)
1059 { printf("spin: cannot read %s\n", *ltl_file);
1060 }
1061 fclose(tl_out);
1062 tl_out = stdout;
1063 *ltl_file = formula;
1064 }
1065 if (argc > 1)
1066 { FILE *fd = stdout;
1067 char cmd[512], out2[512];
1068
1069 /* must remain in current dir */
1070 strcpy(out1, "pan.pre");
1071
1072 if (add_ltl || nvr_file)
1073 { assert(strlen(argv[1]) < sizeof(out2));
1074 sprintf(out2, "%s.nvr", argv[1]);
1075 if ((fd = fopen(out2, MFLAGS)) == NULL)
1076 { printf("spin: cannot create tmp file %s\n",
1077 out2);
1078 alldone(1);
1079 }
1080 fprintf(fd, "#include \"%s\"\n", argv[1]);
1081 }
1082
1083 if (add_ltl)
1084 { tl_out = fd;
1085 nr_errs = tl_main(2, add_ltl);
1086 fclose(fd);
1087 preprocess(out2, out1, 1);
1088 } else if (nvr_file)
1089 { fprintf(fd, "#include \"%s\"\n", *nvr_file);
1090 fclose(fd);
1091 preprocess(out2, out1, 1);
1092 } else
1093 { preprocess(argv[1], out1, 0);
1094 }
1095
1096 if (preprocessonly)
1097 { alldone(0);
1098 }
1099
1100 if (!(yyin = fopen(out1, "r")))
1101 { printf("spin: cannot open %s\n", out1);
1102 alldone(1);
1103 }
1104
1105 assert(strlen(argv[1])+1 < sizeof(cmd));
1106
1107 if (strncmp(argv[1], "progress", (size_t) 8) == 0
1108 || strncmp(argv[1], "accept", (size_t) 6) == 0)
1109 { sprintf(cmd, "_%s", argv[1]);
1110 } else
1111 { strcpy(cmd, argv[1]);
1112 }
1113 oFname = Fname = lookup(cmd);
1114 if (oFname->name[0] == '\"')
1115 { int i = (int) strlen(oFname->name);
1116 oFname->name[i-1] = '\0';
1117 oFname = lookup(&oFname->name[1]);
1118 }
1119 } else
1120 { oFname = Fname = lookup("<stdin>");
1121 if (add_ltl)
1122 { if (argc > 0)
1123 exit(tl_main(2, add_ltl));
1124 printf("spin: missing argument to -f\n");
1125 alldone(1);
1126 }
1127 printf("%s\n", SpinVersion);
1128 fprintf(stderr, "spin: error, no filename specified\n");
1129 fflush(stdout);
1130 alldone(1);
1131 }
1132 if (columns == 2)
1133 { if (xspin || (verbose & (1|4|8|16|32)))
1134 { printf("spin: -c precludes all flags except -t\n");
1135 alldone(1);
1136 }
1137 putprelude();
1138 }
1139 if (columns && !(verbose&8) && !(verbose&16))
1140 { verbose += (8+16);
1141 }
1142 if (columns == 2 && limited_vis)
1143 { verbose += (1+4);
1144 }
1145
1146 Srand((unsigned int) T); /* defined in run.c */
1147 SeedUsed = T;
1148 s = lookup("_"); s->type = PREDEF; /* write-only global var */
1149 s = lookup("_p"); s->type = PREDEF;
1150 s = lookup("_pid"); s->type = PREDEF;
1151 s = lookup("_last"); s->type = PREDEF;
1152 s = lookup("_nr_pr"); s->type = PREDEF; /* new 3.3.10 */
1153 s = lookup("_priority"); s->type = PREDEF; /* new 6.2.0 */
1154
1155 yyparse();
1156 fclose(yyin);
1157
1158 if (ltl_claims)
1159 { Symbol *r;
1160 fclose(fd_ltl);
1161 if (!(yyin = fopen(ltl_claims, "r")))
1162 { fatal("cannot open %s", ltl_claims);
1163 }
1164 r = oFname;
1165 oFname = Fname = lookup(ltl_claims);
1166 lineno = 0;
1167 yyparse();
1168 fclose(yyin);
1169 oFname = Fname = r;
1170 if (0)
1171 { (void) unlink(ltl_claims);
1172 } }
1173
1174 loose_ends();
1175
1176 if (inlineonly)
1177 { repro_src();
1178 return 0;
1179 }
1180
1181 chanaccess();
1182 if (!Caccess)
1183 { if (has_provided && merger)
1184 { merger = 0; /* cannot use statement merging in this case */
1185 }
1186 if (!s_trail && (dataflow || merger) && (!replay || has_code))
1187 { ana_src(dataflow, merger);
1188 }
1189 sched();
1190 alldone(nr_errs);
1191 }
1192
1193 return 0;
1194 }
1195
1196 void
ltl_list(char * nm,char * fm)1197 ltl_list(char *nm, char *fm)
1198 {
1199 if (s_trail
1200 || analyze
1201 || dumptab) /* when generating pan.c or replaying a trace */
1202 { if (!ltl_claims)
1203 { ltl_claims = "_spin_nvr.tmp";
1204 if ((fd_ltl = fopen(ltl_claims, MFLAGS)) == NULL)
1205 { fatal("cannot open tmp file %s", ltl_claims);
1206 }
1207 tl_out = fd_ltl;
1208 }
1209 add_ltl = (char **) emalloc(5 * sizeof(char *));
1210 add_ltl[1] = "-c";
1211 add_ltl[2] = nm;
1212 add_ltl[3] = "-f";
1213 add_ltl[4] = (char *) emalloc(strlen(fm)+4);
1214 strcpy(add_ltl[4], "!(");
1215 strcat(add_ltl[4], fm);
1216 strcat(add_ltl[4], ")");
1217 /* add_ltl[4] = fm; */
1218 nr_errs += tl_main(4, add_ltl);
1219
1220 fflush(tl_out);
1221 /* should read this file after the main file is read */
1222 }
1223 }
1224
1225 void
non_fatal(char * s1,char * s2)1226 non_fatal(char *s1, char *s2)
1227 { extern char yytext[];
1228
1229 printf("spin: %s:%d, Error: ",
1230 Fname?Fname->name:(oFname?oFname->name:"nofilename"), lineno);
1231 #if 1
1232 printf(s1, s2); /* avoids a gcc warning */
1233 #else
1234 if (s2)
1235 printf(s1, s2);
1236 else
1237 printf(s1);
1238 #endif
1239 if (strlen(yytext)>1)
1240 printf(" near '%s'", yytext);
1241 printf("\n");
1242 nr_errs++;
1243 }
1244
1245 void
fatal(char * s1,char * s2)1246 fatal(char *s1, char *s2)
1247 {
1248 non_fatal(s1, s2);
1249 (void) unlink("pan.b");
1250 (void) unlink("pan.c");
1251 (void) unlink("pan.h");
1252 (void) unlink("pan.m");
1253 (void) unlink("pan.t");
1254 (void) unlink("pan.p");
1255 (void) unlink("pan.pre");
1256 if (!(verbose&32))
1257 { (void) unlink("_spin_nvr.tmp");
1258 }
1259 alldone(1);
1260 }
1261
1262 char *
emalloc(size_t n)1263 emalloc(size_t n)
1264 { char *tmp;
1265 static unsigned long cnt = 0;
1266
1267 if (n == 0)
1268 return NULL; /* robert shelton 10/20/06 */
1269
1270 if (!(tmp = (char *) malloc(n)))
1271 { printf("spin: allocated %ld Gb, wanted %d bytes more\n",
1272 cnt/(1024*1024*1024), (int) n);
1273 fatal("not enough memory", (char *)0);
1274 }
1275 cnt += (unsigned long) n;
1276 memset(tmp, 0, n);
1277 return tmp;
1278 }
1279
1280 void
trapwonly(Lextok * n)1281 trapwonly(Lextok *n /* , char *unused */)
1282 { short i;
1283
1284 if (!n)
1285 { fatal("unexpected error,", (char *) 0);
1286 }
1287
1288 i = (n->sym)?n->sym->type:0;
1289
1290 /* printf("%s realread %d type %d\n", n->sym?n->sym->name:"--", realread, i); */
1291
1292 if (realread
1293 && (i == MTYPE
1294 || i == BIT
1295 || i == BYTE
1296 || i == SHORT
1297 || i == INT
1298 || i == UNSIGNED))
1299 { n->sym->hidden |= 128; /* var is read at least once */
1300 }
1301 }
1302
1303 void
setaccess(Symbol * sp,Symbol * what,int cnt,int t)1304 setaccess(Symbol *sp, Symbol *what, int cnt, int t)
1305 { Access *a;
1306
1307 for (a = sp->access; a; a = a->lnk)
1308 if (a->who == context
1309 && a->what == what
1310 && a->cnt == cnt
1311 && a->typ == t)
1312 return;
1313
1314 a = (Access *) emalloc(sizeof(Access));
1315 a->who = context;
1316 a->what = what;
1317 a->cnt = cnt;
1318 a->typ = t;
1319 a->lnk = sp->access;
1320 sp->access = a;
1321 }
1322
1323 Lextok *
nn(Lextok * s,int t,Lextok * ll,Lextok * rl)1324 nn(Lextok *s, int t, Lextok *ll, Lextok *rl)
1325 { Lextok *n = (Lextok *) emalloc(sizeof(Lextok));
1326 static int warn_nn = 0;
1327
1328 n->uiid = is_inline(); /* record origin of the statement */
1329 n->ntyp = (unsigned short) t;
1330 if (s && s->fn)
1331 { n->ln = s->ln;
1332 n->fn = s->fn;
1333 } else if (rl && rl->fn)
1334 { n->ln = rl->ln;
1335 n->fn = rl->fn;
1336 } else if (ll && ll->fn)
1337 { n->ln = ll->ln;
1338 n->fn = ll->fn;
1339 } else
1340 { n->ln = lineno;
1341 n->fn = Fname;
1342 }
1343 if (s) n->sym = s->sym;
1344 n->lft = ll;
1345 n->rgt = rl;
1346 n->indstep = DstepStart;
1347
1348 if (t == TIMEOUT) Etimeouts++;
1349
1350 if (!context) return n;
1351
1352 if (t == 'r' || t == 's')
1353 setaccess(n->sym, ZS, 0, t);
1354 if (t == 'R')
1355 setaccess(n->sym, ZS, 0, 'P');
1356
1357 if (context->name == claimproc)
1358 { int forbidden = separate;
1359 switch (t) {
1360 case ASGN:
1361 printf("spin: Warning, never claim has side-effect\n");
1362 break;
1363 case 'r': case 's':
1364 non_fatal("never claim contains i/o stmnts",(char *)0);
1365 break;
1366 case TIMEOUT:
1367 /* never claim polls timeout */
1368 if (Ntimeouts && Etimeouts)
1369 forbidden = 0;
1370 Ntimeouts++; Etimeouts--;
1371 break;
1372 case LEN: case EMPTY: case FULL:
1373 case 'R': case NFULL: case NEMPTY:
1374 /* status becomes non-exclusive */
1375 if (n->sym && !(n->sym->xu&XX))
1376 { n->sym->xu |= XX;
1377 if (separate == 2) {
1378 printf("spin: warning, make sure that the S1 model\n");
1379 printf(" also polls channel '%s' in its claim\n",
1380 n->sym->name);
1381 } }
1382 forbidden = 0;
1383 break;
1384 case 'c':
1385 AST_track(n, 0); /* register as a slice criterion */
1386 /* fall thru */
1387 default:
1388 forbidden = 0;
1389 break;
1390 }
1391 if (forbidden)
1392 { printf("spin: never, saw "); explain(t); printf("\n");
1393 fatal("incompatible with separate compilation",(char *)0);
1394 }
1395 } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t))
1396 { printf("spin: Warning, using %s outside never claim\n",
1397 (t == ENABLED)?"enabled()":"pc_value()");
1398 warn_nn |= t;
1399 } else if (t == NONPROGRESS)
1400 { fatal("spin: Error, using np_ outside never claim\n", (char *)0);
1401 }
1402 return n;
1403 }
1404
1405 Lextok *
rem_lab(Symbol * a,Lextok * b,Symbol * c)1406 rem_lab(Symbol *a, Lextok *b, Symbol *c) /* proctype name, pid, label name */
1407 { Lextok *tmp1, *tmp2, *tmp3;
1408
1409 has_remote++;
1410 c->type = LABEL; /* refered to in global context here */
1411 fix_dest(c, a); /* in case target of rem_lab is jump */
1412 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
1413 tmp1 = nn(ZN, 'p', tmp1, ZN);
1414 tmp1->sym = lookup("_p");
1415 tmp2 = nn(ZN, NAME, ZN, ZN); tmp2->sym = a;
1416 tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c;
1417 return nn(ZN, EQ, tmp1, tmp3);
1418 #if 0
1419 .---------------EQ-------.
1420 / \
1421 'p' -sym-> _p 'q' -sym-> c (label name)
1422 / /
1423 '?' -sym-> a (proctype) NAME -sym-> a (proctype name)
1424 /
1425 b (pid expr)
1426 #endif
1427 }
1428
1429 Lextok *
rem_var(Symbol * a,Lextok * b,Symbol * c,Lextok * ndx)1430 rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx)
1431 { Lextok *tmp1;
1432
1433 has_remote++;
1434 has_remvar++;
1435 dataflow = 0; /* turn off dead variable resets 4.2.5 */
1436 merger = 0; /* turn off statement merging for locals 6.4.9 */
1437 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
1438 tmp1 = nn(ZN, 'p', tmp1, ndx);
1439 tmp1->sym = c;
1440 return tmp1;
1441 #if 0
1442 cannot refer to struct elements
1443 only to scalars and arrays
1444
1445 'p' -sym-> c (variable name)
1446 / \______ possible arrayindex on c
1447 /
1448 '?' -sym-> a (proctype)
1449 /
1450 b (pid expr)
1451 #endif
1452 }
1453
1454 void
explain(int n)1455 explain(int n)
1456 { FILE *fd = stdout;
1457 switch (n) {
1458 default: if (n > 0 && n < 256)
1459 fprintf(fd, "'%c' = ", n);
1460 fprintf(fd, "%d", n);
1461 break;
1462 case '\b': fprintf(fd, "\\b"); break;
1463 case '\t': fprintf(fd, "\\t"); break;
1464 case '\f': fprintf(fd, "\\f"); break;
1465 case '\n': fprintf(fd, "\\n"); break;
1466 case '\r': fprintf(fd, "\\r"); break;
1467 case 'c': fprintf(fd, "condition"); break;
1468 case 's': fprintf(fd, "send"); break;
1469 case 'r': fprintf(fd, "recv"); break;
1470 case 'R': fprintf(fd, "recv poll %s", Operator); break;
1471 case '@': fprintf(fd, "@"); break;
1472 case '?': fprintf(fd, "(x->y:z)"); break;
1473 #if 1
1474 case NEXT: fprintf(fd, "X"); break;
1475 case ALWAYS: fprintf(fd, "[]"); break;
1476 case EVENTUALLY: fprintf(fd, "<>"); break;
1477 case IMPLIES: fprintf(fd, "->"); break;
1478 case EQUIV: fprintf(fd, "<->"); break;
1479 case UNTIL: fprintf(fd, "U"); break;
1480 case WEAK_UNTIL: fprintf(fd, "W"); break;
1481 case IN: fprintf(fd, "%sin", Keyword); break;
1482 #endif
1483 case ACTIVE: fprintf(fd, "%sactive", Keyword); break;
1484 case AND: fprintf(fd, "%s&&", Operator); break;
1485 case ASGN: fprintf(fd, "%s=", Operator); break;
1486 case ASSERT: fprintf(fd, "%sassert", Function); break;
1487 case ATOMIC: fprintf(fd, "%satomic", Keyword); break;
1488 case BREAK: fprintf(fd, "%sbreak", Keyword); break;
1489 case C_CODE: fprintf(fd, "%sc_code", Keyword); break;
1490 case C_DECL: fprintf(fd, "%sc_decl", Keyword); break;
1491 case C_EXPR: fprintf(fd, "%sc_expr", Keyword); break;
1492 case C_STATE: fprintf(fd, "%sc_state",Keyword); break;
1493 case C_TRACK: fprintf(fd, "%sc_track",Keyword); break;
1494 case CLAIM: fprintf(fd, "%snever", Keyword); break;
1495 case CONST: fprintf(fd, "a constant"); break;
1496 case DECR: fprintf(fd, "%s--", Operator); break;
1497 case D_STEP: fprintf(fd, "%sd_step", Keyword); break;
1498 case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break;
1499 case DO: fprintf(fd, "%sdo", Keyword); break;
1500 case DOT: fprintf(fd, "."); break;
1501 case ELSE: fprintf(fd, "%selse", Keyword); break;
1502 case EMPTY: fprintf(fd, "%sempty", Function); break;
1503 case ENABLED: fprintf(fd, "%senabled",Function); break;
1504 case EQ: fprintf(fd, "%s==", Operator); break;
1505 case EVAL: fprintf(fd, "%seval", Function); break;
1506 case FI: fprintf(fd, "%sfi", Keyword); break;
1507 case FULL: fprintf(fd, "%sfull", Function); break;
1508 case GE: fprintf(fd, "%s>=", Operator); break;
1509 case GET_P: fprintf(fd, "%sget_priority",Function); break;
1510 case GOTO: fprintf(fd, "%sgoto", Keyword); break;
1511 case GT: fprintf(fd, "%s>", Operator); break;
1512 case HIDDEN: fprintf(fd, "%shidden", Keyword); break;
1513 case IF: fprintf(fd, "%sif", Keyword); break;
1514 case INCR: fprintf(fd, "%s++", Operator); break;
1515 case INAME: fprintf(fd, "inline name"); break;
1516 case INLINE: fprintf(fd, "%sinline", Keyword); break;
1517 case INIT: fprintf(fd, "%sinit", Keyword); break;
1518 case ISLOCAL: fprintf(fd, "%slocal", Keyword); break;
1519 case LABEL: fprintf(fd, "a label-name"); break;
1520 case LE: fprintf(fd, "%s<=", Operator); break;
1521 case LEN: fprintf(fd, "%slen", Function); break;
1522 case LSHIFT: fprintf(fd, "%s<<", Operator); break;
1523 case LT: fprintf(fd, "%s<", Operator); break;
1524 case MTYPE: fprintf(fd, "%smtype", Keyword); break;
1525 case NAME: fprintf(fd, "an identifier"); break;
1526 case NE: fprintf(fd, "%s!=", Operator); break;
1527 case NEG: fprintf(fd, "%s! (not)",Operator); break;
1528 case NEMPTY: fprintf(fd, "%snempty", Function); break;
1529 case NFULL: fprintf(fd, "%snfull", Function); break;
1530 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
1531 case NONPROGRESS: fprintf(fd, "%snp_", Function); break;
1532 case OD: fprintf(fd, "%sod", Keyword); break;
1533 case OF: fprintf(fd, "%sof", Keyword); break;
1534 case OR: fprintf(fd, "%s||", Operator); break;
1535 case O_SND: fprintf(fd, "%s!!", Operator); break;
1536 case PC_VAL: fprintf(fd, "%spc_value",Function); break;
1537 case PNAME: fprintf(fd, "process name"); break;
1538 case PRINT: fprintf(fd, "%sprintf", Function); break;
1539 case PRINTM: fprintf(fd, "%sprintm", Function); break;
1540 case PRIORITY: fprintf(fd, "%spriority", Keyword); break;
1541 case PROCTYPE: fprintf(fd, "%sproctype",Keyword); break;
1542 case PROVIDED: fprintf(fd, "%sprovided",Keyword); break;
1543 case RCV: fprintf(fd, "%s?", Operator); break;
1544 case R_RCV: fprintf(fd, "%s??", Operator); break;
1545 case RSHIFT: fprintf(fd, "%s>>", Operator); break;
1546 case RUN: fprintf(fd, "%srun", Operator); break;
1547 case SEP: fprintf(fd, "token: ::"); break;
1548 case SEMI: fprintf(fd, ";"); break;
1549 case ARROW: fprintf(fd, "->"); break;
1550 case SET_P: fprintf(fd, "%sset_priority",Function); break;
1551 case SHOW: fprintf(fd, "%sshow", Keyword); break;
1552 case SND: fprintf(fd, "%s!", Operator); break;
1553 case STRING: fprintf(fd, "a string"); break;
1554 case TRACE: fprintf(fd, "%strace", Keyword); break;
1555 case TIMEOUT: fprintf(fd, "%stimeout",Keyword); break;
1556 case TYPE: fprintf(fd, "data typename"); break;
1557 case TYPEDEF: fprintf(fd, "%stypedef",Keyword); break;
1558 case XU: fprintf(fd, "%sx[rs]", Keyword); break;
1559 case UMIN: fprintf(fd, "%s- (unary minus)", Operator); break;
1560 case UNAME: fprintf(fd, "a typename"); break;
1561 case UNLESS: fprintf(fd, "%sunless", Keyword); break;
1562 }
1563 }
1564
1565
1566