Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 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
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
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
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
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
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
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
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
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
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
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
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 
}