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