1 /***** spin: pangen3.c *****/
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
14 extern int eventmapnr, old_priority_rules;
17 int ln, st; /* linenr, statenr */
18 Symbol *fn; /* filename */
23 static Symbol *lastfnm;
24 static Symbol lastdef;
26 static SRC *frst = (SRC *) 0;
27 static SRC *skip = (SRC *) 0;
31 extern void sr_mesg(FILE *, int, int);
37 { fprintf(tc, "\n\t"); /* was th */
40 fprintf(tc, "%3d, ", n); /* was th */
44 putfnm(int j, Symbol *s)
46 if (lastfnm && lastfnm == s && j != -1)
50 fprintf(tc, "{ \"%s\", %d, %d },\n\t", /* was th */
62 fprintf(tc, "{ \"%s\", %d, %d }\n", /* was th */
70 tmp = (SRC *) emalloc(sizeof(SRC));
77 putskip(int m) /* states that need not be reached */
78 { SRC *tmp, *lst = (SRC *)0;
79 /* 6.4.0: now an ordered list */
80 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
84 if (tmp->st > m) /* insert before */
86 { tmp = newsrc(m, skip);
90 tmp = newsrc(m, lst->nxt);
95 /* insert at the end */
97 { lst->nxt = newsrc(m, 0);
98 } else /* empty list */
99 { skip = newsrc(m, 0);
104 unskip(int m) /* a state that needs to be reached after all */
105 { SRC *tmp, *lst = (SRC *)0;
107 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
111 else if (lst) /* always true, but helps coverity */
116 { break; /* m is not in list */
121 putsrc(Element *e) /* match states to source lines */
122 { SRC *tmp, *lst = (SRC *)0;
125 if (!e || !e->n) return;
129 /* 6.4.0: now an ordered list */
130 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
132 { if (tmp->ln != n || tmp->fn != e->n->fn)
133 printf("putsrc mismatch seqno %d, line %d - %d, file %s\n", m, n,
134 tmp->ln, tmp->fn->name);
137 if (tmp->st > m) /* insert before */
139 { tmp = newsrc(m, frst);
143 tmp = newsrc(m, lst->nxt);
150 /* insert at the end */
151 tmp = newsrc(m, lst?lst->nxt:0);
162 dumpskip(int n, int m)
164 FILE *tz = tc; /* was th */
167 fprintf(tz, "uchar reached%d [] = {\n\t", m);
170 for (j = 0, col = 0; j <= n; j++)
171 { /* find j in the sorted list */
172 for ( ; tmp; lst = tmp, tmp = tmp->nxt)
183 break; /* j is not in the list */
190 fprintf(tz, "uchar *loopstate%d;\n", m);
193 fprintf(th, "#define reached_event reached%d\n", m);
199 dumpsrc(int n, int m)
202 static int did_claim = 0;
203 FILE *tz = tc; /* was th */
205 fprintf(tz, "\nshort src_ln%d [] = {\n\t", m);
207 for (j = 0, col = 0; j <= n; j++)
208 { for ( ; tmp; tmp = tmp->nxt)
222 lastfnm = (Symbol *) 0;
224 fprintf(tz, "S_F_MAP src_file%d [] = {\n\t", m);
227 for (j = 0, col = 0; j <= n; j++)
228 { for ( ; tmp; lst = tmp, tmp = tmp->nxt)
230 { putfnm(j, tmp->fn);
238 { putfnm(j, &lastdef);
242 { putfnm(j, &lastdef);
247 if (pid_is_claim(m) && !did_claim)
248 { fprintf(tz, "short *src_claim;\n");
252 fprintf(th, "#define src_event src_ln%d\n", m);
258 #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \
259 comwork(fd,now->rgt,m)
260 #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")")
261 #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m)
262 #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z)
265 symbolic(FILE *fd, Lextok *tv)
266 { Lextok *n; extern Lextok *Mtype;
270 for (n = Mtype; n; n = n->rgt, cnt++)
272 { fprintf(fd, "%s", n->lft->sym->name);
279 comwork(FILE *fd, Lextok *now, int m)
283 if (!now) { fprintf(fd, "0"); return; }
285 case CONST: sr_mesg(fd, now->val, now->ismtyp); break;
286 case '!': Cat3("!(", now->lft, ")"); break;
287 case UMIN: Cat3("-(", now->lft, ")"); break;
288 case '~': Cat3("~(", now->lft, ")"); break;
290 case '/': Cat1("/"); break;
291 case '*': Cat1("*"); break;
292 case '-': Cat1("-"); break;
293 case '+': Cat1("+"); break;
294 case '%': Cat1("%%"); break;
295 case '&': Cat1("&"); break;
296 case '^': Cat1("^"); break;
297 case '|': Cat1("|"); break;
298 case LE: Cat1("<="); break;
299 case GE: Cat1(">="); break;
300 case GT: Cat1(">"); break;
301 case LT: Cat1("<"); break;
302 case NE: Cat1("!="); break;
305 && now->lft->ntyp == 'p'
306 && now->rgt->ntyp == 'q') /* remote ref */
307 { Lextok *p = now->lft->lft;
310 fprintf(fd, "%s", p->sym->name);
313 putstmnt(fd, p->lft, 0); /* pid */
317 fprintf(fd, "%s", now->rgt->sym->name);
324 case OR: Cat1("||"); break;
325 case AND: Cat1("&&"); break;
326 case LSHIFT: Cat1("<<"); break;
327 case RSHIFT: Cat1(">>"); break;
329 case RUN: fprintf(fd, "run %s(", now->sym->name);
330 for (v = now->lft; v; v = v->rgt)
332 { comwork(fd, v->lft, m);
339 case LEN: putname(fd, "len(", now->lft, m, ")");
341 case FULL: putname(fd, "full(", now->lft, m, ")");
343 case EMPTY: putname(fd, "empty(", now->lft, m, ")");
345 case NFULL: putname(fd, "nfull(", now->lft, m, ")");
347 case NEMPTY: putname(fd, "nempty(", now->lft, m, ")");
350 case 's': putname(fd, "", now->lft, m, now->val?"!!":"!");
351 for (v = now->rgt, i=0; v; v = v->rgt, i++)
352 { if (v != now->rgt) fprintf(fd,",");
353 if (!symbolic(fd, v->lft))
354 comwork(fd,v->lft,m);
357 case 'r': putname(fd, "", now->lft, m, "?");
360 case 1: fprintf(fd, "?"); break;
361 case 2: fprintf(fd, "<"); break;
362 case 3: fprintf(fd, "?<"); break;
364 for (v = now->rgt, i=0; v; v = v->rgt, i++)
365 { if (v != now->rgt) fprintf(fd,",");
366 if (!symbolic(fd, v->lft))
367 comwork(fd,v->lft,m);
372 case 'R': putname(fd, "", now->lft, m, now->val?"??[":"?[");
373 for (v = now->rgt, i=0; v; v = v->rgt, i++)
374 { if (v != now->rgt) fprintf(fd,",");
375 if (!symbolic(fd, v->lft))
376 comwork(fd,v->lft,m);
381 case ENABLED: Cat3("enabled(", now->lft, ")");
384 case GET_P: if (old_priority_rules)
387 { Cat3("get_priority(", now->lft, ")");
391 case SET_P: if (!old_priority_rules)
392 { fprintf(fd, "set_priority(");
393 comwork(fd, now->lft->lft, m);
395 comwork(fd, now->lft->rgt, m);
400 case EVAL: Cat3("eval(", now->lft, ")");
407 case PC_VAL: Cat3("pc_value(", now->lft, ")");
410 case 'c': Cat3("(", now->lft, ")");
413 case '?': if (now->lft)
414 { Cat3("( (", now->lft, ") -> ");
417 { Cat3("(", now->rgt->lft, ") : ");
418 Cat3("(", now->rgt->rgt, ") )");
423 if (check_track(now) == STRUCT) { break; }
424 comwork(fd,now->lft,m);
426 comwork(fd,now->rgt,m);
429 case PRINT: { char c, buf[1024];
430 strncpy(buf, now->sym->name, 510);
431 for (i = j = 0; i < 510; i++, j++)
432 { c = now->sym->name[i];
434 if (c == '\\') buf[++j] = c;
435 if (c == '\"') buf[j] = '\'';
436 if (c == '\0') break;
438 if (now->ntyp == PRINT)
439 fprintf(fd, "printf");
441 fprintf(fd, "annotate");
442 fprintf(fd, "(%s", buf);
444 for (v = now->lft; v; v = v->rgt)
449 case PRINTM: fprintf(fd, "printm(");
450 comwork(fd, now->lft, m);
454 putname(fd, "", now, m, "");
459 { fprintf(fd, "%s", now->lft->sym->name); /* proctype */
462 putstmnt(fd, now->lft->lft, 0); /* pid */
465 fprintf(fd, ":"); /* remote varref */
466 fprintf(fd, "%s", now->sym->name); /* varname */
469 putremote(fd, now, m);
471 case 'q': fprintf(fd, "%s", now->sym->name);
474 case C_CODE: fprintf(fd, "{%s}", now->sym->name);
476 case ASSERT: Cat3("assert(", now->lft, ")");
478 case '.': fprintf(fd, ".(goto)"); break;
479 case GOTO: fprintf(fd, "goto %s", now->sym->name); break;
480 case BREAK: fprintf(fd, "break"); break;
481 case ELSE: fprintf(fd, "else"); break;
482 case '@': fprintf(fd, "-end-"); break;
484 case D_STEP: fprintf(fd, "D_STEP%d", now->ln); break;
485 case ATOMIC: fprintf(fd, "ATOMIC"); break;
486 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
487 case IF: fprintf(fd, "IF"); break;
488 case DO: fprintf(fd, "DO"); break;
489 case UNLESS: fprintf(fd, "unless"); break;
490 case TIMEOUT: fprintf(fd, "timeout"); break;
491 default: if (isprint(now->ntyp))
492 fprintf(fd, "'%c'", now->ntyp);
494 fprintf(fd, "%d", now->ntyp);
500 comment(FILE *fd, Lextok *now, int m)
501 { extern short terse, nocast;