0b55f123 |
1 | /***** spin: pangen3.c *****/ |
2 | |
3 | /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | #include "spin.h" |
13 | #include "y.tab.h" |
14 | |
15 | extern FILE *th; |
16 | extern int claimnr, eventmapnr; |
17 | |
18 | typedef struct SRC { |
19 | short ln, st; /* linenr, statenr */ |
20 | Symbol *fn; /* filename */ |
21 | struct SRC *nxt; |
22 | } SRC; |
23 | |
24 | static int col; |
25 | static Symbol *lastfnm; |
26 | static Symbol lastdef; |
27 | static int lastfrom; |
28 | static SRC *frst = (SRC *) 0; |
29 | static SRC *skip = (SRC *) 0; |
30 | |
31 | extern void sr_mesg(FILE *, int, int); |
32 | |
33 | static void |
34 | putnr(int n) |
35 | { |
36 | if (col++ == 8) |
37 | { fprintf(th, "\n\t"); |
38 | col = 1; |
39 | } |
40 | fprintf(th, "%3d, ", n); |
41 | } |
42 | |
43 | static void |
44 | putfnm(int j, Symbol *s) |
45 | { |
46 | if (lastfnm && lastfnm == s && j != -1) |
47 | return; |
48 | |
49 | if (lastfnm) |
50 | fprintf(th, "{ %s, %d, %d },\n\t", |
51 | lastfnm->name, |
52 | lastfrom, |
53 | j-1); |
54 | lastfnm = s; |
55 | lastfrom = j; |
56 | } |
57 | |
58 | static void |
59 | putfnm_flush(int j) |
60 | { |
61 | if (lastfnm) |
62 | fprintf(th, "{ %s, %d, %d }\n", |
63 | lastfnm->name, |
64 | lastfrom, j); |
65 | } |
66 | |
67 | void |
68 | putskip(int m) /* states that need not be reached */ |
69 | { SRC *tmp; |
70 | |
71 | for (tmp = skip; tmp; tmp = tmp->nxt) |
72 | if (tmp->st == m) |
73 | return; |
74 | tmp = (SRC *) emalloc(sizeof(SRC)); |
75 | tmp->st = (short) m; |
76 | tmp->nxt = skip; |
77 | skip = tmp; |
78 | } |
79 | |
80 | void |
81 | unskip(int m) /* a state that needs to be reached after all */ |
82 | { SRC *tmp, *lst=(SRC *)0; |
83 | |
84 | for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) |
85 | if (tmp->st == m) |
86 | { if (tmp == skip) |
87 | skip = skip->nxt; |
88 | else if (lst) /* always true, but helps coverity */ |
89 | lst->nxt = tmp->nxt; |
90 | break; |
91 | } |
92 | } |
93 | |
94 | void |
95 | putsrc(Element *e) /* match states to source lines */ |
96 | { SRC *tmp; |
97 | int n, m; |
98 | |
99 | if (!e || !e->n) return; |
100 | |
101 | n = e->n->ln; |
102 | m = e->seqno; |
103 | |
104 | for (tmp = frst; tmp; tmp = tmp->nxt) |
105 | if (tmp->st == m) |
106 | { if (tmp->ln != n || tmp->fn != e->n->fn) |
107 | printf("putsrc mismatch %d - %d, file %s\n", n, |
108 | tmp->ln, tmp->fn->name); |
109 | return; |
110 | } |
111 | tmp = (SRC *) emalloc(sizeof(SRC)); |
112 | tmp->ln = (short) n; |
113 | tmp->st = (short) m; |
114 | tmp->fn = e->n->fn; |
115 | tmp->nxt = frst; |
116 | frst = tmp; |
117 | } |
118 | |
119 | static void |
120 | dumpskip(int n, int m) |
121 | { SRC *tmp, *lst; |
122 | int j; |
123 | |
124 | fprintf(th, "uchar reached%d [] = {\n\t", m); |
125 | for (j = 0, col = 0; j <= n; j++) |
126 | { lst = (SRC *) 0; |
127 | for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) |
128 | if (tmp->st == j) |
129 | { putnr(1); |
130 | if (lst) |
131 | lst->nxt = tmp->nxt; |
132 | else |
133 | skip = tmp->nxt; |
134 | break; |
135 | } |
136 | if (!tmp) |
137 | putnr(0); |
138 | } |
139 | fprintf(th, "};\n"); |
140 | |
141 | fprintf(th, "uchar *loopstate%d;\n", m); |
142 | |
143 | if (m == claimnr) |
144 | fprintf(th, "#define reached_claim reached%d\n", m); |
145 | if (m == eventmapnr) |
146 | fprintf(th, "#define reached_event reached%d\n", m); |
147 | |
148 | skip = (SRC *) 0; |
149 | } |
150 | |
151 | void |
152 | dumpsrc(int n, int m) |
153 | { SRC *tmp, *lst; |
154 | int j; |
155 | |
156 | fprintf(th, "short src_ln%d [] = {\n\t", m); |
157 | for (j = 0, col = 0; j <= n; j++) |
158 | { lst = (SRC *) 0; |
159 | for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt) |
160 | if (tmp->st == j) |
161 | { putnr(tmp->ln); |
162 | break; |
163 | } |
164 | if (!tmp) |
165 | putnr(0); |
166 | } |
167 | fprintf(th, "};\n"); |
168 | |
169 | lastfnm = (Symbol *) 0; |
170 | lastdef.name = "\"-\""; |
171 | fprintf(th, "S_F_MAP src_file%d [] = {\n\t", m); |
172 | for (j = 0, col = 0; j <= n; j++) |
173 | { lst = (SRC *) 0; |
174 | for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt) |
175 | if (tmp->st == j) |
176 | { putfnm(j, tmp->fn); |
177 | if (lst) |
178 | lst->nxt = tmp->nxt; |
179 | else |
180 | frst = tmp->nxt; |
181 | break; |
182 | } |
183 | if (!tmp) |
184 | putfnm(j, &lastdef); |
185 | } |
186 | putfnm_flush(j); |
187 | fprintf(th, "};\n"); |
188 | |
189 | if (m == claimnr) |
190 | fprintf(th, "#define src_claim src_ln%d\n", m); |
191 | if (m == eventmapnr) |
192 | fprintf(th, "#define src_event src_ln%d\n", m); |
193 | |
194 | frst = (SRC *) 0; |
195 | dumpskip(n, m); |
196 | } |
197 | |
198 | #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \ |
199 | comwork(fd,now->rgt,m) |
200 | #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")") |
201 | #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m) |
202 | #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z) |
203 | |
204 | static int |
205 | symbolic(FILE *fd, Lextok *tv) |
206 | { Lextok *n; extern Lextok *Mtype; |
207 | int cnt = 1; |
208 | |
209 | if (tv->ismtyp) |
210 | for (n = Mtype; n; n = n->rgt, cnt++) |
211 | if (cnt == tv->val) |
212 | { fprintf(fd, "%s", n->lft->sym->name); |
213 | return 1; |
214 | } |
215 | return 0; |
216 | } |
217 | |
218 | static void |
219 | comwork(FILE *fd, Lextok *now, int m) |
220 | { Lextok *v; |
221 | int i, j; |
222 | |
223 | if (!now) { fprintf(fd, "0"); return; } |
224 | switch (now->ntyp) { |
225 | case CONST: sr_mesg(fd, now->val, now->ismtyp); break; |
226 | case '!': Cat3("!(", now->lft, ")"); break; |
227 | case UMIN: Cat3("-(", now->lft, ")"); break; |
228 | case '~': Cat3("~(", now->lft, ")"); break; |
229 | |
230 | case '/': Cat1("/"); break; |
231 | case '*': Cat1("*"); break; |
232 | case '-': Cat1("-"); break; |
233 | case '+': Cat1("+"); break; |
234 | case '%': Cat1("%%"); break; |
235 | case '&': Cat1("&"); break; |
236 | case '^': Cat1("^"); break; |
237 | case '|': Cat1("|"); break; |
238 | case LE: Cat1("<="); break; |
239 | case GE: Cat1(">="); break; |
240 | case GT: Cat1(">"); break; |
241 | case LT: Cat1("<"); break; |
242 | case NE: Cat1("!="); break; |
243 | case EQ: Cat1("=="); break; |
244 | case OR: Cat1("||"); break; |
245 | case AND: Cat1("&&"); break; |
246 | case LSHIFT: Cat1("<<"); break; |
247 | case RSHIFT: Cat1(">>"); break; |
248 | |
249 | case RUN: fprintf(fd, "run %s(", now->sym->name); |
250 | for (v = now->lft; v; v = v->rgt) |
251 | if (v == now->lft) |
252 | { comwork(fd, v->lft, m); |
253 | } else |
254 | { Cat2(",", v->lft); |
255 | } |
256 | fprintf(fd, ")"); |
257 | break; |
258 | |
259 | case LEN: putname(fd, "len(", now->lft, m, ")"); |
260 | break; |
261 | case FULL: putname(fd, "full(", now->lft, m, ")"); |
262 | break; |
263 | case EMPTY: putname(fd, "empty(", now->lft, m, ")"); |
264 | break; |
265 | case NFULL: putname(fd, "nfull(", now->lft, m, ")"); |
266 | break; |
267 | case NEMPTY: putname(fd, "nempty(", now->lft, m, ")"); |
268 | break; |
269 | |
270 | case 's': putname(fd, "", now->lft, m, now->val?"!!":"!"); |
271 | for (v = now->rgt, i=0; v; v = v->rgt, i++) |
272 | { if (v != now->rgt) fprintf(fd,","); |
273 | if (!symbolic(fd, v->lft)) |
274 | comwork(fd,v->lft,m); |
275 | } |
276 | break; |
277 | case 'r': putname(fd, "", now->lft, m, "?"); |
278 | switch (now->val) { |
279 | case 0: break; |
280 | case 1: fprintf(fd, "?"); break; |
281 | case 2: fprintf(fd, "<"); break; |
282 | case 3: fprintf(fd, "?<"); break; |
283 | } |
284 | for (v = now->rgt, i=0; v; v = v->rgt, i++) |
285 | { if (v != now->rgt) fprintf(fd,","); |
286 | if (!symbolic(fd, v->lft)) |
287 | comwork(fd,v->lft,m); |
288 | } |
289 | if (now->val >= 2) |
290 | fprintf(fd, ">"); |
291 | break; |
292 | case 'R': putname(fd, "", now->lft, m, now->val?"??[":"?["); |
293 | for (v = now->rgt, i=0; v; v = v->rgt, i++) |
294 | { if (v != now->rgt) fprintf(fd,","); |
295 | if (!symbolic(fd, v->lft)) |
296 | comwork(fd,v->lft,m); |
297 | } |
298 | fprintf(fd, "]"); |
299 | break; |
300 | |
301 | case ENABLED: Cat3("enabled(", now->lft, ")"); |
302 | break; |
303 | |
304 | case EVAL: Cat3("eval(", now->lft, ")"); |
305 | break; |
306 | |
307 | case NONPROGRESS: |
308 | fprintf(fd, "np_"); |
309 | break; |
310 | |
311 | case PC_VAL: Cat3("pc_value(", now->lft, ")"); |
312 | break; |
313 | |
314 | case 'c': Cat3("(", now->lft, ")"); |
315 | break; |
316 | |
317 | case '?': if (now->lft) |
318 | { Cat3("( (", now->lft, ") -> "); |
319 | } |
320 | if (now->rgt) |
321 | { Cat3("(", now->rgt->lft, ") : "); |
322 | Cat3("(", now->rgt->rgt, ") )"); |
323 | } |
324 | break; |
325 | |
326 | case ASGN: comwork(fd,now->lft,m); |
327 | fprintf(fd," = "); |
328 | comwork(fd,now->rgt,m); |
329 | break; |
330 | |
331 | case PRINT: { char c, buf[512]; |
332 | strncpy(buf, now->sym->name, 510); |
333 | for (i = j = 0; i < 510; i++, j++) |
334 | { c = now->sym->name[i]; |
335 | buf[j] = c; |
336 | if (c == '\\') buf[++j] = c; |
337 | if (c == '\"') buf[j] = '\''; |
338 | if (c == '\0') break; |
339 | } |
340 | if (now->ntyp == PRINT) |
341 | fprintf(fd, "printf"); |
342 | else |
343 | fprintf(fd, "annotate"); |
344 | fprintf(fd, "(%s", buf); |
345 | } |
346 | for (v = now->lft; v; v = v->rgt) |
347 | { Cat2(",", v->lft); |
348 | } |
349 | fprintf(fd, ")"); |
350 | break; |
351 | case PRINTM: fprintf(fd, "printm("); |
352 | comwork(fd, now->lft, m); |
353 | fprintf(fd, ")"); |
354 | break; |
355 | case NAME: putname(fd, "", now, m, ""); |
356 | break; |
357 | case 'p': putremote(fd, now, m); |
358 | break; |
359 | case 'q': fprintf(fd, "%s", now->sym->name); |
360 | break; |
361 | case C_EXPR: |
362 | case C_CODE: fprintf(fd, "{%s}", now->sym->name); |
363 | break; |
364 | case ASSERT: Cat3("assert(", now->lft, ")"); |
365 | break; |
366 | case '.': fprintf(fd, ".(goto)"); break; |
367 | case GOTO: fprintf(fd, "goto %s", now->sym->name); break; |
368 | case BREAK: fprintf(fd, "break"); break; |
369 | case ELSE: fprintf(fd, "else"); break; |
370 | case '@': fprintf(fd, "-end-"); break; |
371 | |
372 | case D_STEP: fprintf(fd, "D_STEP"); break; |
373 | case ATOMIC: fprintf(fd, "ATOMIC"); break; |
374 | case NON_ATOMIC: fprintf(fd, "sub-sequence"); break; |
375 | case IF: fprintf(fd, "IF"); break; |
376 | case DO: fprintf(fd, "DO"); break; |
377 | case UNLESS: fprintf(fd, "unless"); break; |
378 | case TIMEOUT: fprintf(fd, "timeout"); break; |
379 | default: if (isprint(now->ntyp)) |
380 | fprintf(fd, "'%c'", now->ntyp); |
381 | else |
382 | fprintf(fd, "%d", now->ntyp); |
383 | break; |
384 | } |
385 | } |
386 | |
387 | void |
388 | comment(FILE *fd, Lextok *now, int m) |
389 | { extern short terse, nocast; |
390 | |
391 | terse=nocast=1; |
392 | comwork(fd, now, m); |
393 | terse=nocast=0; |
394 | } |