1 /***** spin: pangen3.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 "spin.h"
10 #include "y.tab.h"
11 #include <assert.h>
12
13 extern FILE *fd_th, *fd_tc;
14 extern int eventmapnr, old_priority_rules, in_settr;
15
16 typedef struct SRC {
17 int ln, st; /* linenr, statenr */
18 Symbol *fn; /* filename */
19 struct SRC *nxt;
20 } SRC;
21
22 static int col;
23 static Symbol *lastfnm;
24 static Symbol lastdef;
25 static int lastfrom;
26 static SRC *frst = (SRC *) 0;
27 static SRC *skip = (SRC *) 0;
28
29 extern int ltl_mode;
30
31 extern void sr_mesg(FILE *, int, int, const char *);
32 extern Lextok **find_mtype_list(const char *);
33
34 static void
putnr(int n)35 putnr(int n)
36 {
37 if (col++ == 8)
38 { fprintf(fd_tc, "\n\t"); /* was th */
39 col = 1;
40 }
41 fprintf(fd_tc, "%3d, ", n); /* was th */
42 }
43
44 static void
putfnm(int j,Symbol * s)45 putfnm(int j, Symbol *s)
46 {
47 if (lastfnm && lastfnm == s && j != -1)
48 return;
49
50 if (lastfnm)
51 fprintf(fd_tc, "{ \"%s\", %d, %d },\n\t", /* was th */
52 lastfnm->name,
53 lastfrom,
54 j-1);
55 lastfnm = s;
56 lastfrom = j;
57 }
58
59 static void
putfnm_flush(int j)60 putfnm_flush(int j)
61 {
62 if (lastfnm)
63 fprintf(fd_tc, "{ \"%s\", %d, %d }\n", /* was th */
64 lastfnm->name,
65 lastfrom, j);
66 }
67
68 static SRC *
newsrc(int m,SRC * n)69 newsrc(int m, SRC *n)
70 { SRC *tmp;
71 tmp = (SRC *) emalloc(sizeof(SRC));
72 tmp->st = m;
73 tmp->nxt = n;
74 return tmp;
75 }
76
77 void
putskip(int m)78 putskip(int m) /* states that need not be reached */
79 { SRC *tmp, *lst = (SRC *)0;
80 /* 6.4.0: now an ordered list */
81 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
82 { if (tmp->st == m)
83 { return;
84 }
85 if (tmp->st > m) /* insert before */
86 { if (tmp == skip)
87 { tmp = newsrc(m, skip);
88 skip = tmp;
89 } else
90 { assert(lst);
91 tmp = newsrc(m, lst->nxt);
92 lst->nxt = tmp;
93 }
94 return;
95 } }
96 /* insert at the end */
97 if (lst)
98 { lst->nxt = newsrc(m, 0);
99 } else /* empty list */
100 { skip = newsrc(m, 0);
101 }
102 }
103
104 void
unskip(int m)105 unskip(int m) /* a state that needs to be reached after all */
106 { SRC *tmp, *lst = (SRC *)0;
107
108 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
109 { if (tmp->st == m)
110 { if (tmp == skip)
111 skip = skip->nxt;
112 else if (lst) /* always true, but helps coverity */
113 lst->nxt = tmp->nxt;
114 break;
115 }
116 if (tmp->st > m)
117 { break; /* m is not in list */
118 } }
119 }
120
121 void
putsrc(Element * e)122 putsrc(Element *e) /* match states to source lines */
123 { SRC *tmp, *lst = (SRC *)0;
124 int n, m;
125
126 if (!e || !e->n) return;
127
128 n = e->n->ln;
129 m = e->seqno;
130 /* 6.4.0: now an ordered list */
131 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
132 { if (tmp->st == m)
133 { if (tmp->ln != n || tmp->fn != e->n->fn)
134 printf("putsrc mismatch seqno %d, line %d - %d, file %s\n", m, n,
135 tmp->ln, tmp->fn->name);
136 return;
137 }
138 if (tmp->st > m) /* insert before */
139 { if (tmp == frst)
140 { tmp = newsrc(m, frst);
141 frst = tmp;
142 } else
143 { assert(lst);
144 tmp = newsrc(m, lst->nxt);
145 lst->nxt = tmp;
146 }
147 tmp->ln = n;
148 tmp->fn = e->n->fn;
149 return;
150 } }
151 /* insert at the end */
152 tmp = newsrc(m, lst?lst->nxt:0);
153 tmp->ln = n;
154 tmp->fn = e->n->fn;
155 if (lst)
156 { lst->nxt = tmp;
157 } else
158 { frst = tmp;
159 }
160 }
161
162 static void
dumpskip(int n,int m)163 dumpskip(int n, int m)
164 { SRC *tmp, *lst;
165 FILE *tz = fd_tc; /* was fd_th */
166 int j;
167
168 fprintf(tz, "uchar reached%d [] = {\n\t", m);
169 tmp = skip;
170 lst = (SRC *) 0;
171 for (j = 0, col = 0; j <= n; j++)
172 { /* find j in the sorted list */
173 for ( ; tmp; lst = tmp, tmp = tmp->nxt)
174 { if (tmp->st == j)
175 { putnr(1);
176 if (lst)
177 lst->nxt = tmp->nxt;
178 else
179 skip = tmp->nxt;
180 break;
181 }
182 if (tmp->st > j)
183 { putnr(0);
184 break; /* j is not in the list */
185 } }
186
187 if (!tmp)
188 { putnr(0);
189 } }
190 fprintf(tz, "};\n");
191 fprintf(tz, "uchar *loopstate%d;\n", m);
192
193 if (m == eventmapnr)
194 fprintf(fd_th, "#define reached_event reached%d\n", m);
195
196 skip = (SRC *) 0;
197 }
198
199 void
dumpsrc(int n,int m)200 dumpsrc(int n, int m)
201 { SRC *tmp, *lst;
202 int j;
203 static int did_claim = 0;
204 FILE *tz = fd_tc; /* was fd_th */
205
206 fprintf(tz, "\nshort src_ln%d [] = {\n\t", m);
207 tmp = frst;
208 for (j = 0, col = 0; j <= n; j++)
209 { for ( ; tmp; tmp = tmp->nxt)
210 { if (tmp->st == j)
211 { putnr(tmp->ln);
212 break;
213 }
214 if (tmp->st > j)
215 { putnr(0);
216 break;
217 } }
218 if (!tmp)
219 { putnr(0);
220 } }
221 fprintf(tz, "};\n");
222
223 lastfnm = (Symbol *) 0;
224 lastdef.name = "-";
225 fprintf(tz, "S_F_MAP src_file%d [] = {\n\t", m);
226 tmp = frst;
227 lst = (SRC *) 0;
228 for (j = 0, col = 0; j <= n; j++)
229 { for ( ; tmp; lst = tmp, tmp = tmp->nxt)
230 { if (tmp->st == j)
231 { putfnm(j, tmp->fn);
232 if (lst)
233 lst->nxt = tmp->nxt;
234 else
235 frst = tmp->nxt;
236 break;
237 }
238 if (tmp->st > j)
239 { putfnm(j, &lastdef);
240 break;
241 } }
242 if (!tmp)
243 { putfnm(j, &lastdef);
244 } }
245 putfnm_flush(j);
246 fprintf(tz, "};\n");
247
248 if (pid_is_claim(m) && !did_claim)
249 { fprintf(tz, "short *src_claim;\n");
250 did_claim++;
251 }
252 if (m == eventmapnr)
253 fprintf(fd_th, "#define src_event src_ln%d\n", m);
254
255 frst = (SRC *) 0;
256 dumpskip(n, m);
257 }
258
259 #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \
260 comwork(fd,now->rgt,m)
261 #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")")
262 #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m)
263 #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z)
264
265 static int
symbolic(FILE * fd,Lextok * tv)266 symbolic(FILE *fd, Lextok *tv)
267 { Lextok *n, *Mtype;
268 int cnt = 1;
269
270 if (tv->ismtyp)
271 { char *s = "_unnamed_";
272 if (tv->sym && tv->sym->mtype_name)
273 { s = tv->sym->mtype_name->name;
274 }
275 Mtype = *find_mtype_list(s);
276 for (n = Mtype; n; n = n->rgt, cnt++)
277 { if (cnt == tv->val)
278 { fprintf(fd, "%s", n->lft->sym->name);
279 return 1;
280 } } }
281
282 return 0;
283 }
284
285 static void
comwork(FILE * fd,Lextok * now,int m)286 comwork(FILE *fd, Lextok *now, int m)
287 { Lextok *v;
288 char *s = 0;
289 int i, j;
290
291 if (!now) { fprintf(fd, "0"); return; }
292 switch (now->ntyp) {
293 case CONST: if (now->ismtyp
294 && now->sym
295 && now->sym->mtype_name)
296 { s = now->sym->mtype_name->name;
297 }
298 sr_mesg(fd, now->val, now->ismtyp, s);
299 break;
300
301 case '!': Cat3("!(", now->lft, ")"); break;
302 case UMIN: Cat3("-(", now->lft, ")"); break;
303 case '~': Cat3("~(", now->lft, ")"); break;
304
305 case '/': Cat1("/"); break;
306 case '*': Cat1("*"); break;
307 case '-': Cat1("-"); break;
308 case '+': Cat1("+"); break;
309 case '%': Cat1("%%"); break;
310 case '&': Cat1("&"); break;
311 case '^': Cat1("^"); break;
312 case '|': Cat1("|"); break;
313 case LE: Cat1("<="); break;
314 case GE: Cat1(">="); break;
315 case GT: Cat1(">"); break;
316 case LT: Cat1("<"); break;
317 case NE: Cat1("!="); break;
318 case EQ:
319 if (ltl_mode
320 && now->lft->ntyp == 'p'
321 && now->rgt->ntyp == 'q') /* remote ref */
322 { Lextok *p = now->lft->lft;
323
324 fprintf(fd, "(");
325 fprintf(fd, "%s", p->sym->name);
326 if (p->lft)
327 { fprintf(fd, "[");
328 putstmnt(fd, p->lft, 0); /* pid */
329 fprintf(fd, "]");
330 }
331 fprintf(fd, "@");
332 fprintf(fd, "%s", now->rgt->sym->name);
333 fprintf(fd, ")");
334 break;
335 }
336 Cat1("==");
337 break;
338
339 case OR: Cat1("||"); break;
340 case AND: Cat1("&&"); break;
341 case LSHIFT: Cat1("<<"); break;
342 case RSHIFT: Cat1(">>"); break;
343
344 case RUN: fprintf(fd, "run %s(", now->sym->name);
345 for (v = now->lft; v; v = v->rgt)
346 if (v == now->lft)
347 { comwork(fd, v->lft, m);
348 } else
349 { Cat2(",", v->lft);
350 }
351 fprintf(fd, ")");
352 break;
353
354 case LEN: putname(fd, "len(", now->lft, m, ")");
355 break;
356 case FULL: putname(fd, "full(", now->lft, m, ")");
357 break;
358 case EMPTY: putname(fd, "empty(", now->lft, m, ")");
359 break;
360 case NFULL: putname(fd, "nfull(", now->lft, m, ")");
361 break;
362 case NEMPTY: putname(fd, "nempty(", now->lft, m, ")");
363 break;
364
365 case 's': putname(fd, "", now->lft, m, now->val?"!!":"!");
366 for (v = now->rgt, i=0; v; v = v->rgt, i++)
367 { if (v != now->rgt) fprintf(fd,",");
368 if (!symbolic(fd, v->lft))
369 comwork(fd,v->lft,m);
370 }
371 break;
372 case 'r': putname(fd, "", now->lft, m, "?");
373 switch (now->val) {
374 case 0: break;
375 case 1: fprintf(fd, "?"); break;
376 case 2: fprintf(fd, "<"); break;
377 case 3: fprintf(fd, "?<"); break;
378 }
379 for (v = now->rgt, i=0; v; v = v->rgt, i++)
380 { if (v != now->rgt) fprintf(fd,",");
381 if (!symbolic(fd, v->lft))
382 comwork(fd,v->lft,m);
383 }
384 if (now->val >= 2)
385 fprintf(fd, ">");
386 break;
387 case 'R': putname(fd, "", now->lft, m, now->val?"??[":"?[");
388 for (v = now->rgt, i=0; v; v = v->rgt, i++)
389 { if (v != now->rgt) fprintf(fd,",");
390 if (!symbolic(fd, v->lft))
391 comwork(fd,v->lft,m);
392 }
393 fprintf(fd, "]");
394 break;
395
396 case ENABLED: Cat3("enabled(", now->lft, ")");
397 break;
398
399 case GET_P: if (old_priority_rules)
400 { fprintf(fd, "1");
401 } else
402 { Cat3("get_priority(", now->lft, ")");
403 }
404 break;
405
406 case SET_P: if (!old_priority_rules)
407 { fprintf(fd, "set_priority(");
408 comwork(fd, now->lft->lft, m);
409 fprintf(fd, ", ");
410 comwork(fd, now->lft->rgt, m);
411 fprintf(fd, ")");
412 }
413 break;
414
415 case EVAL: if (now->lft->ntyp == ',')
416 { Cat3("eval(", now->lft->lft, ")");
417 } else
418 { Cat3("eval(", now->lft, ")");
419 }
420 break;
421
422 case NONPROGRESS:
423 fprintf(fd, "np_");
424 break;
425
426 case PC_VAL: Cat3("pc_value(", now->lft, ")");
427 break;
428
429 case 'c': Cat3("(", now->lft, ")");
430 break;
431
432 case '?': if (now->lft)
433 { Cat3("( (", now->lft, ") -> ");
434 }
435 if (now->rgt)
436 { Cat3("(", now->rgt->lft, ") : ");
437 Cat3("(", now->rgt->rgt, ") )");
438 }
439 break;
440
441 case ASGN:
442 if (check_track(now) == STRUCT) { break; }
443 comwork(fd,now->lft,m);
444 fprintf(fd," = ");
445 comwork(fd,now->rgt,m);
446 break;
447
448 case PRINT: { char c, buf[1024];
449 strncpy(buf, now->sym->name, 510);
450 for (i = j = 0; i < 510; i++, j++)
451 { c = now->sym->name[i];
452 buf[j] = c;
453 if (c == '\\') buf[++j] = c;
454 if (c == '\"') buf[j] = '\'';
455 if (c == '\0') break;
456 }
457 if (now->ntyp == PRINT)
458 fprintf(fd, "printf");
459 else
460 fprintf(fd, "annotate");
461 fprintf(fd, "(%s", buf);
462 }
463 for (v = now->lft; v; v = v->rgt)
464 { Cat2(",", v->lft);
465 }
466 fprintf(fd, ")");
467 break;
468 case PRINTM: fprintf(fd, "printm(");
469 { char *s = 0;
470 if (now->lft->sym
471 && now->lft->sym->mtype_name)
472 { s = now->lft->sym->mtype_name->name;
473 }
474
475 if (now->lft && now->lft->ismtyp)
476 { fprintf(fd, "%d", now->lft->val);
477 } else
478 { comwork(fd, now->lft, m);
479 }
480
481 if (s)
482 { if (in_settr)
483 { fprintf(fd, ", '%s')", s);
484 } else
485 { fprintf(fd, ", \"%s\")", s);
486 }
487 } else
488 { fprintf(fd, ", 0)");
489 }
490 }
491 break;
492 case NAME:
493 putname(fd, "", now, m, "");
494 break;
495
496 case 'p':
497 if (ltl_mode)
498 { fprintf(fd, "%s", now->lft->sym->name); /* proctype */
499 if (now->lft->lft)
500 { fprintf(fd, "[");
501 putstmnt(fd, now->lft->lft, 0); /* pid */
502 fprintf(fd, "]");
503 }
504 fprintf(fd, ":"); /* remote varref */
505 fprintf(fd, "%s", now->sym->name); /* varname */
506 break;
507 }
508 putremote(fd, now, m);
509 break;
510 case 'q': fprintf(fd, "%s", now->sym->name);
511 break;
512 case C_EXPR:
513 case C_CODE: fprintf(fd, "{%s}", now->sym->name);
514 break;
515 case ASSERT: Cat3("assert(", now->lft, ")");
516 break;
517 case '.': fprintf(fd, ".(goto)"); break;
518 case GOTO: fprintf(fd, "goto %s", now->sym->name); break;
519 case BREAK: fprintf(fd, "break"); break;
520 case ELSE: fprintf(fd, "else"); break;
521 case '@': fprintf(fd, "-end-"); break;
522
523 case D_STEP: fprintf(fd, "D_STEP%d", now->ln); break;
524 case ATOMIC: fprintf(fd, "ATOMIC"); break;
525 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
526 case IF: fprintf(fd, "IF"); break;
527 case DO: fprintf(fd, "DO"); break;
528 case UNLESS: fprintf(fd, "unless"); break;
529 case TIMEOUT: fprintf(fd, "timeout"); break;
530 default: if (isprint(now->ntyp))
531 fprintf(fd, "'%c'", now->ntyp);
532 else
533 fprintf(fd, "%d", now->ntyp);
534 break;
535 }
536 }
537
538 void
comment(FILE * fd,Lextok * now,int m)539 comment(FILE *fd, Lextok *now, int m)
540 { extern short terse, nocast;
541
542 terse=nocast=1;
543 comwork(fd, now, m);
544 terse=nocast=0;
545 }
546