spin.y 19 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722
  1. /***** spin: spin.y *****/
  2. /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
  3. /* All Rights Reserved. This software is for educational purposes only. */
  4. /* No guarantee whatsoever is expressed or implied by the distribution of */
  5. /* this code. Permission is given to distribute this code provided that */
  6. /* this introductory message is not removed and no monies are exchanged. */
  7. /* Software written by Gerard J. Holzmann. For tool documentation see: */
  8. /* http://spinroot.com/ */
  9. /* Send all bug-reports and/or questions to: bugs@spinroot.com */
  10. %{
  11. #include "spin.h"
  12. #include <stdarg.h>
  13. #define YYDEBUG 0
  14. #define Stop nn(ZN,'@',ZN,ZN)
  15. extern Symbol *context, *owner;
  16. extern int u_sync, u_async, dumptab;
  17. extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np;
  18. extern short has_code, has_state, has_io;
  19. extern void count_runs(Lextok *);
  20. extern void no_internals(Lextok *);
  21. extern void any_runs(Lextok *);
  22. extern void validref(Lextok *, Lextok *);
  23. extern char yytext[];
  24. int Mpars = 0; /* max nr of message parameters */
  25. int runsafe = 1; /* 1 if all run stmnts are in init */
  26. int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
  27. char *claimproc = (char *) 0;
  28. char *eventmap = (char *) 0;
  29. static int Embedded = 0, inEventMap = 0, has_ini = 0;
  30. %}
  31. %token ASSERT PRINT PRINTM
  32. %token C_CODE C_DECL C_EXPR C_STATE C_TRACK
  33. %token RUN LEN ENABLED EVAL PC_VAL
  34. %token TYPEDEF MTYPE INLINE LABEL OF
  35. %token GOTO BREAK ELSE SEMI
  36. %token IF FI DO OD SEP
  37. %token ATOMIC NON_ATOMIC D_STEP UNLESS
  38. %token TIMEOUT NONPROGRESS
  39. %token ACTIVE PROCTYPE D_PROCTYPE
  40. %token HIDDEN SHOW ISLOCAL
  41. %token PRIORITY PROVIDED
  42. %token FULL EMPTY NFULL NEMPTY
  43. %token CONST TYPE XU /* val */
  44. %token NAME UNAME PNAME INAME /* sym */
  45. %token STRING CLAIM TRACE INIT /* sym */
  46. %right ASGN
  47. %left SND O_SND RCV R_RCV /* SND doubles as boolean negation */
  48. %left OR
  49. %left AND
  50. %left '|'
  51. %left '^'
  52. %left '&'
  53. %left EQ NE
  54. %left GT LT GE LE
  55. %left LSHIFT RSHIFT
  56. %left '+' '-'
  57. %left '*' '/' '%'
  58. %left INCR DECR
  59. %right '~' UMIN NEG
  60. %left DOT
  61. %%
  62. /** PROMELA Grammar Rules **/
  63. program : units { yytext[0] = '\0'; }
  64. ;
  65. units : unit
  66. | units unit
  67. ;
  68. unit : proc /* proctype { } */
  69. | init /* init { } */
  70. | claim /* never claim */
  71. | events /* event assertions */
  72. | one_decl /* variables, chans */
  73. | utype /* user defined types */
  74. | c_fcts /* c functions etc. */
  75. | ns /* named sequence */
  76. | SEMI /* optional separator */
  77. | error
  78. ;
  79. proc : inst /* optional instantiator */
  80. proctype NAME {
  81. setptype($3, PROCTYPE, ZN);
  82. setpname($3);
  83. context = $3->sym;
  84. context->ini = $2; /* linenr and file */
  85. Expand_Ok++; /* expand struct names in decl */
  86. has_ini = 0;
  87. }
  88. '(' decl ')' { Expand_Ok--;
  89. if (has_ini)
  90. fatal("initializer in parameter list", (char *) 0);
  91. }
  92. Opt_priority
  93. Opt_enabler
  94. body { ProcList *rl;
  95. rl = ready($3->sym, $6, $11->sq, $2->val, $10);
  96. if ($1 != ZN && $1->val > 0)
  97. { int j;
  98. for (j = 0; j < $1->val; j++)
  99. runnable(rl, $9?$9->val:1, 1);
  100. announce(":root:");
  101. if (dumptab) $3->sym->ini = $1;
  102. }
  103. context = ZS;
  104. }
  105. ;
  106. proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
  107. | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
  108. ;
  109. inst : /* empty */ { $$ = ZN; }
  110. | ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
  111. | ACTIVE '[' CONST ']' {
  112. $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
  113. if ($3->val > 255)
  114. non_fatal("max nr of processes is 255\n", "");
  115. }
  116. | ACTIVE '[' NAME ']' {
  117. $$ = nn(ZN,CONST,ZN,ZN);
  118. $$->val = 0;
  119. if (!$3->sym->type)
  120. non_fatal("undeclared variable %s",
  121. $3->sym->name);
  122. else if ($3->sym->ini->ntyp != CONST)
  123. non_fatal("need constant initializer for %s\n",
  124. $3->sym->name);
  125. else
  126. $$->val = $3->sym->ini->val;
  127. }
  128. ;
  129. init : INIT { context = $1->sym; }
  130. Opt_priority
  131. body { ProcList *rl;
  132. rl = ready(context, ZN, $4->sq, 0, ZN);
  133. runnable(rl, $3?$3->val:1, 1);
  134. announce(":root:");
  135. context = ZS;
  136. }
  137. ;
  138. claim : CLAIM { context = $1->sym;
  139. if (claimproc)
  140. non_fatal("claim %s redefined", claimproc);
  141. claimproc = $1->sym->name;
  142. }
  143. body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
  144. context = ZS;
  145. }
  146. ;
  147. events : TRACE { context = $1->sym;
  148. if (eventmap)
  149. non_fatal("trace %s redefined", eventmap);
  150. eventmap = $1->sym->name;
  151. inEventMap++;
  152. }
  153. body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
  154. context = ZS;
  155. inEventMap--;
  156. }
  157. ;
  158. utype : TYPEDEF NAME { if (context)
  159. fatal("typedef %s must be global",
  160. $2->sym->name);
  161. owner = $2->sym;
  162. }
  163. '{' decl_lst '}' { setuname($5); owner = ZS; }
  164. ;
  165. nm : NAME { $$ = $1; }
  166. | INAME { $$ = $1;
  167. if (IArgs)
  168. fatal("invalid use of '%s'", $1->sym->name);
  169. }
  170. ;
  171. ns : INLINE nm '(' { NamesNotAdded++; }
  172. args ')' { prep_inline($2->sym, $5);
  173. NamesNotAdded--;
  174. }
  175. ;
  176. c_fcts : ccode { /* leaves pseudo-inlines with sym of
  177. * type CODE_FRAG or CODE_DECL in global context
  178. */
  179. }
  180. | cstate
  181. ;
  182. cstate : C_STATE STRING STRING {
  183. c_state($2->sym, $3->sym, ZS);
  184. has_code = has_state = 1;
  185. }
  186. | C_TRACK STRING STRING {
  187. c_track($2->sym, $3->sym, ZS);
  188. has_code = has_state = 1;
  189. }
  190. | C_STATE STRING STRING STRING {
  191. c_state($2->sym, $3->sym, $4->sym);
  192. has_code = has_state = 1;
  193. }
  194. | C_TRACK STRING STRING STRING {
  195. c_track($2->sym, $3->sym, $4->sym);
  196. has_code = has_state = 1;
  197. }
  198. ;
  199. ccode : C_CODE { Symbol *s;
  200. NamesNotAdded++;
  201. s = prep_inline(ZS, ZN);
  202. NamesNotAdded--;
  203. $$ = nn(ZN, C_CODE, ZN, ZN);
  204. $$->sym = s;
  205. has_code = 1;
  206. }
  207. | C_DECL { Symbol *s;
  208. NamesNotAdded++;
  209. s = prep_inline(ZS, ZN);
  210. NamesNotAdded--;
  211. s->type = CODE_DECL;
  212. $$ = nn(ZN, C_CODE, ZN, ZN);
  213. $$->sym = s;
  214. has_code = 1;
  215. }
  216. ;
  217. cexpr : C_EXPR { Symbol *s;
  218. NamesNotAdded++;
  219. s = prep_inline(ZS, ZN);
  220. NamesNotAdded--;
  221. $$ = nn(ZN, C_EXPR, ZN, ZN);
  222. $$->sym = s;
  223. no_side_effects(s->name);
  224. has_code = 1;
  225. }
  226. ;
  227. body : '{' { open_seq(1); }
  228. sequence OS { add_seq(Stop); }
  229. '}' { $$->sq = close_seq(0); }
  230. ;
  231. sequence: step { if ($1) add_seq($1); }
  232. | sequence MS step { if ($3) add_seq($3); }
  233. ;
  234. step : one_decl { $$ = ZN; }
  235. | XU vref_lst { setxus($2, $1->val); $$ = ZN; }
  236. | NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); }
  237. | NAME ':' XU { fatal("label predecing xr/xs claim,", 0); }
  238. | stmnt { $$ = $1; }
  239. | stmnt UNLESS stmnt { $$ = do_unless($1, $3); }
  240. ;
  241. vis : /* empty */ { $$ = ZN; }
  242. | HIDDEN { $$ = $1; }
  243. | SHOW { $$ = $1; }
  244. | ISLOCAL { $$ = $1; }
  245. ;
  246. asgn: /* empty */
  247. | ASGN
  248. ;
  249. one_decl: vis TYPE var_list { setptype($3, $2->val, $1); $$ = $3; }
  250. | vis UNAME var_list { setutype($3, $2->sym, $1);
  251. $$ = expand($3, Expand_Ok);
  252. }
  253. | vis TYPE asgn '{' nlst '}' {
  254. if ($2->val != MTYPE)
  255. fatal("malformed declaration", 0);
  256. setmtype($5);
  257. if ($1)
  258. non_fatal("cannot %s mtype (ignored)",
  259. $1->sym->name);
  260. if (context != ZS)
  261. fatal("mtype declaration must be global", 0);
  262. }
  263. ;
  264. decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); }
  265. | one_decl SEMI
  266. decl_lst { $$ = nn(ZN, ',', $1, $3); }
  267. ;
  268. decl : /* empty */ { $$ = ZN; }
  269. | decl_lst { $$ = $1; }
  270. ;
  271. vref_lst: varref { $$ = nn($1, XU, $1, ZN); }
  272. | varref ',' vref_lst { $$ = nn($1, XU, $1, $3); }
  273. ;
  274. var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); }
  275. | ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); }
  276. ;
  277. ivar : vardcl { $$ = $1;
  278. $1->sym->ini = nn(ZN,CONST,ZN,ZN);
  279. $1->sym->ini->val = 0;
  280. }
  281. | vardcl ASGN expr { $1->sym->ini = $3; $$ = $1;
  282. trackvar($1,$3); has_ini = 1;
  283. }
  284. | vardcl ASGN ch_init { $1->sym->ini = $3;
  285. $$ = $1; has_ini = 1;
  286. }
  287. ;
  288. ch_init : '[' CONST ']' OF
  289. '{' typ_list '}' { if ($2->val) u_async++;
  290. else u_sync++;
  291. { int i = cnt_mpars($6);
  292. Mpars = max(Mpars, i);
  293. }
  294. $$ = nn(ZN, CHAN, ZN, $6);
  295. $$->val = $2->val;
  296. }
  297. ;
  298. vardcl : NAME { $1->sym->nel = 1; $$ = $1; }
  299. | NAME ':' CONST { $1->sym->nbits = $3->val;
  300. if ($3->val >= 8*sizeof(long))
  301. { non_fatal("width-field %s too large",
  302. $1->sym->name);
  303. $3->val = 8*sizeof(long)-1;
  304. }
  305. $1->sym->nel = 1; $$ = $1;
  306. }
  307. | NAME '[' CONST ']' { $1->sym->nel = $3->val; $$ = $1; }
  308. ;
  309. varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); }
  310. ;
  311. pfld : NAME { $$ = nn($1, NAME, ZN, ZN); }
  312. | NAME { owner = ZS; }
  313. '[' expr ']' { $$ = nn($1, NAME, $4, ZN); }
  314. ;
  315. cmpnd : pfld { Embedded++;
  316. if ($1->sym->type == STRUCT)
  317. owner = $1->sym->Snm;
  318. }
  319. sfld { $$ = $1; $$->rgt = $3;
  320. if ($3 && $1->sym->type != STRUCT)
  321. $1->sym->type = STRUCT;
  322. Embedded--;
  323. if (!Embedded && !NamesNotAdded
  324. && !$1->sym->type)
  325. non_fatal("undeclared variable: %s",
  326. $1->sym->name);
  327. if ($3) validref($1, $3->lft);
  328. owner = ZS;
  329. }
  330. ;
  331. sfld : /* empty */ { $$ = ZN; }
  332. | '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); }
  333. ;
  334. stmnt : Special { $$ = $1; }
  335. | Stmnt { $$ = $1;
  336. if (inEventMap)
  337. non_fatal("not an event", (char *)0);
  338. }
  339. ;
  340. Special : varref RCV { Expand_Ok++; }
  341. rargs { Expand_Ok--; has_io++;
  342. $$ = nn($1, 'r', $1, $4);
  343. trackchanuse($4, ZN, 'R');
  344. }
  345. | varref SND { Expand_Ok++; }
  346. margs { Expand_Ok--; has_io++;
  347. $$ = nn($1, 's', $1, $4);
  348. $$->val=0; trackchanuse($4, ZN, 'S');
  349. any_runs($4);
  350. }
  351. | IF options FI { $$ = nn($1, IF, ZN, ZN);
  352. $$->sl = $2->sl;
  353. prune_opts($$);
  354. }
  355. | DO { pushbreak(); }
  356. options OD { $$ = nn($1, DO, ZN, ZN);
  357. $$->sl = $3->sl;
  358. prune_opts($$);
  359. }
  360. | BREAK { $$ = nn(ZN, GOTO, ZN, ZN);
  361. $$->sym = break_dest();
  362. }
  363. | GOTO NAME { $$ = nn($2, GOTO, ZN, ZN);
  364. if ($2->sym->type != 0
  365. && $2->sym->type != LABEL) {
  366. non_fatal("bad label-name %s",
  367. $2->sym->name);
  368. }
  369. $2->sym->type = LABEL;
  370. }
  371. | NAME ':' stmnt { $$ = nn($1, ':',$3, ZN);
  372. if ($1->sym->type != 0
  373. && $1->sym->type != LABEL) {
  374. non_fatal("bad label-name %s",
  375. $1->sym->name);
  376. }
  377. $1->sym->type = LABEL;
  378. }
  379. ;
  380. Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3);
  381. trackvar($1, $3);
  382. nochan_manip($1, $3, 0);
  383. no_internals($1);
  384. }
  385. | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
  386. $$ = nn(ZN, '+', $1, $$);
  387. $$ = nn($1, ASGN, $1, $$);
  388. trackvar($1, $1);
  389. no_internals($1);
  390. if ($1->sym->type == CHAN)
  391. fatal("arithmetic on chan", (char *)0);
  392. }
  393. | varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
  394. $$ = nn(ZN, '-', $1, $$);
  395. $$ = nn($1, ASGN, $1, $$);
  396. trackvar($1, $1);
  397. no_internals($1);
  398. if ($1->sym->type == CHAN)
  399. fatal("arithmetic on chan id's", (char *)0);
  400. }
  401. | PRINT '(' STRING { realread = 0; }
  402. prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
  403. | PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
  404. | PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
  405. | ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
  406. | ccode { $$ = $1; }
  407. | varref R_RCV { Expand_Ok++; }
  408. rargs { Expand_Ok--; has_io++;
  409. $$ = nn($1, 'r', $1, $4);
  410. $$->val = has_random = 1;
  411. trackchanuse($4, ZN, 'R');
  412. }
  413. | varref RCV { Expand_Ok++; }
  414. LT rargs GT { Expand_Ok--; has_io++;
  415. $$ = nn($1, 'r', $1, $5);
  416. $$->val = 2; /* fifo poll */
  417. trackchanuse($5, ZN, 'R');
  418. }
  419. | varref R_RCV { Expand_Ok++; }
  420. LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */
  421. $$ = nn($1, 'r', $1, $5);
  422. $$->val = 3; has_random = 1;
  423. trackchanuse($5, ZN, 'R');
  424. }
  425. | varref O_SND { Expand_Ok++; }
  426. margs { Expand_Ok--; has_io++;
  427. $$ = nn($1, 's', $1, $4);
  428. $$->val = has_sorted = 1;
  429. trackchanuse($4, ZN, 'S');
  430. any_runs($4);
  431. }
  432. | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
  433. | ELSE { $$ = nn(ZN,ELSE,ZN,ZN);
  434. }
  435. | ATOMIC '{' { open_seq(0); }
  436. sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN);
  437. $$->sl = seqlist(close_seq(3), 0);
  438. make_atomic($$->sl->this, 0);
  439. }
  440. | D_STEP '{' { open_seq(0); rem_Seq(); }
  441. sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN);
  442. $$->sl = seqlist(close_seq(4), 0);
  443. make_atomic($$->sl->this, D_ATOM);
  444. unrem_Seq();
  445. }
  446. | '{' { open_seq(0); }
  447. sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
  448. $$->sl = seqlist(close_seq(5), 0);
  449. }
  450. | INAME { IArgs++; }
  451. '(' args ')' { pickup_inline($1->sym, $4); IArgs--; }
  452. Stmnt { $$ = $7; }
  453. ;
  454. options : option { $$->sl = seqlist($1->sq, 0); }
  455. | option options { $$->sl = seqlist($1->sq, $2->sl); }
  456. ;
  457. option : SEP { open_seq(0); }
  458. sequence OS { $$ = nn(ZN,0,ZN,ZN);
  459. $$->sq = close_seq(6); }
  460. ;
  461. OS : /* empty */
  462. | SEMI { /* redundant semi at end of sequence */ }
  463. ;
  464. MS : SEMI { /* at least one semi-colon */ }
  465. | MS SEMI { /* but more are okay too */ }
  466. ;
  467. aname : NAME { $$ = $1; }
  468. | PNAME { $$ = $1; }
  469. ;
  470. expr : '(' expr ')' { $$ = $2; }
  471. | expr '+' expr { $$ = nn(ZN, '+', $1, $3); }
  472. | expr '-' expr { $$ = nn(ZN, '-', $1, $3); }
  473. | expr '*' expr { $$ = nn(ZN, '*', $1, $3); }
  474. | expr '/' expr { $$ = nn(ZN, '/', $1, $3); }
  475. | expr '%' expr { $$ = nn(ZN, '%', $1, $3); }
  476. | expr '&' expr { $$ = nn(ZN, '&', $1, $3); }
  477. | expr '^' expr { $$ = nn(ZN, '^', $1, $3); }
  478. | expr '|' expr { $$ = nn(ZN, '|', $1, $3); }
  479. | expr GT expr { $$ = nn(ZN, GT, $1, $3); }
  480. | expr LT expr { $$ = nn(ZN, LT, $1, $3); }
  481. | expr GE expr { $$ = nn(ZN, GE, $1, $3); }
  482. | expr LE expr { $$ = nn(ZN, LE, $1, $3); }
  483. | expr EQ expr { $$ = nn(ZN, EQ, $1, $3); }
  484. | expr NE expr { $$ = nn(ZN, NE, $1, $3); }
  485. | expr AND expr { $$ = nn(ZN, AND, $1, $3); }
  486. | expr OR expr { $$ = nn(ZN, OR, $1, $3); }
  487. | expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); }
  488. | expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); }
  489. | '~' expr { $$ = nn(ZN, '~', $2, ZN); }
  490. | '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); }
  491. | SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); }
  492. | '(' expr SEMI expr ':' expr ')' {
  493. $$ = nn(ZN, OR, $4, $6);
  494. $$ = nn(ZN, '?', $2, $$);
  495. }
  496. | RUN aname { Expand_Ok++;
  497. if (!context)
  498. fatal("used 'run' outside proctype",
  499. (char *) 0);
  500. if (strcmp(context->name, ":init:") != 0)
  501. runsafe = 0;
  502. }
  503. '(' args ')'
  504. Opt_priority { Expand_Ok--;
  505. $$ = nn($2, RUN, $5, ZN);
  506. $$->val = ($7) ? $7->val : 1;
  507. trackchanuse($5, $2, 'A'); trackrun($$);
  508. }
  509. | LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); }
  510. | ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN);
  511. has_enabled++;
  512. }
  513. | varref RCV { Expand_Ok++; }
  514. '[' rargs ']' { Expand_Ok--; has_io++;
  515. $$ = nn($1, 'R', $1, $5);
  516. }
  517. | varref R_RCV { Expand_Ok++; }
  518. '[' rargs ']' { Expand_Ok--; has_io++;
  519. $$ = nn($1, 'R', $1, $5);
  520. $$->val = has_random = 1;
  521. }
  522. | varref { $$ = $1; trapwonly($1, "varref"); }
  523. | cexpr { $$ = $1; }
  524. | CONST { $$ = nn(ZN,CONST,ZN,ZN);
  525. $$->ismtyp = $1->ismtyp;
  526. $$->val = $1->val;
  527. }
  528. | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
  529. | NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
  530. has_np++;
  531. }
  532. | PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN);
  533. has_pcvalue++;
  534. }
  535. | PNAME '[' expr ']' '@' NAME
  536. { $$ = rem_lab($1->sym, $3, $6->sym); }
  537. | PNAME '[' expr ']' ':' pfld
  538. { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
  539. | PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); }
  540. | PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
  541. ;
  542. Opt_priority: /* none */ { $$ = ZN; }
  543. | PRIORITY CONST { $$ = $2; }
  544. ;
  545. full_expr: expr { $$ = $1; }
  546. | Expr { $$ = $1; }
  547. ;
  548. Opt_enabler: /* none */ { $$ = ZN; }
  549. | PROVIDED '(' full_expr ')' { if (!proper_enabler($3))
  550. { non_fatal("invalid PROVIDED clause",
  551. (char *)0);
  552. $$ = ZN;
  553. } else
  554. $$ = $3;
  555. }
  556. | PROVIDED error { $$ = ZN;
  557. non_fatal("usage: provided ( ..expr.. )",
  558. (char *)0);
  559. }
  560. ;
  561. /* an Expr cannot be negated - to protect Probe expressions */
  562. Expr : Probe { $$ = $1; }
  563. | '(' Expr ')' { $$ = $2; }
  564. | Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
  565. | Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
  566. | Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
  567. | Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
  568. | expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
  569. | expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
  570. ;
  571. Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); }
  572. | NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); }
  573. | EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); }
  574. | NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); }
  575. ;
  576. basetype: TYPE { $$->sym = ZS;
  577. $$->val = $1->val;
  578. if ($$->val == UNSIGNED)
  579. fatal("unsigned cannot be used as mesg type", 0);
  580. }
  581. | UNAME { $$->sym = $1->sym;
  582. $$->val = STRUCT;
  583. }
  584. | error /* e.g., unsigned ':' const */
  585. ;
  586. typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); }
  587. | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
  588. ;
  589. args : /* empty */ { $$ = ZN; }
  590. | arg { $$ = $1; }
  591. ;
  592. prargs : /* empty */ { $$ = ZN; }
  593. | ',' arg { $$ = $2; }
  594. ;
  595. margs : arg { $$ = $1; }
  596. | expr '(' arg ')' { if ($1->ntyp == ',')
  597. $$ = tail_add($1, $3);
  598. else
  599. $$ = nn(ZN, ',', $1, $3);
  600. }
  601. ;
  602. arg : expr { if ($1->ntyp == ',')
  603. $$ = $1;
  604. else
  605. $$ = nn(ZN, ',', $1, ZN);
  606. }
  607. | expr ',' arg { if ($1->ntyp == ',')
  608. $$ = tail_add($1, $3);
  609. else
  610. $$ = nn(ZN, ',', $1, $3);
  611. }
  612. ;
  613. rarg : varref { $$ = $1; trackvar($1, $1);
  614. trapwonly($1, "rarg"); }
  615. | EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN);
  616. trapwonly($1, "eval rarg"); }
  617. | CONST { $$ = nn(ZN,CONST,ZN,ZN);
  618. $$->ismtyp = $1->ismtyp;
  619. $$->val = $1->val;
  620. }
  621. | '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN);
  622. $$->val = - ($2->val);
  623. }
  624. ;
  625. rargs : rarg { if ($1->ntyp == ',')
  626. $$ = $1;
  627. else
  628. $$ = nn(ZN, ',', $1, ZN);
  629. }
  630. | rarg ',' rargs { if ($1->ntyp == ',')
  631. $$ = tail_add($1, $3);
  632. else
  633. $$ = nn(ZN, ',', $1, $3);
  634. }
  635. | rarg '(' rargs ')' { if ($1->ntyp == ',')
  636. $$ = tail_add($1, $3);
  637. else
  638. $$ = nn(ZN, ',', $1, $3);
  639. }
  640. | '(' rargs ')' { $$ = $2; }
  641. ;
  642. nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
  643. $$ = nn(ZN, ',', $$, ZN); }
  644. | nlst NAME { $$ = nn($2, NAME, ZN, ZN);
  645. $$ = nn(ZN, ',', $$, $1);
  646. }
  647. | nlst ',' { $$ = $1; /* commas optional */ }
  648. ;
  649. %%
  650. void
  651. yyerror(char *fmt, ...)
  652. {
  653. non_fatal(fmt, (char *) 0);
  654. }