main.c 24 KB

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