xref: /plan9/sys/src/cmd/spin/pangen3.h (revision 00d970127b9d44d2b22f4f656717a212dec1f1d2)
1 /***** spin: pangen3.h *****/
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 /* (c) 2007: small additions for V5.0 to support multi-core verifications */
12 
13 static char *Head0[] = {
14 	"#if defined(BFS) && defined(REACH)",
15 	"	#undef REACH",	/* redundant with bfs */
16 	"#endif",
17 	"#ifdef VERI",
18 	"	#define BASE	1",
19 	"#else",
20 	"	#define BASE	0",
21 	"#endif",
22 	"typedef struct Trans {",
23 	"	short atom;	/* if &2 = atomic trans; if &8 local */",
24 	"#ifdef HAS_UNLESS",
25 	"	short escp[HAS_UNLESS];	/* lists the escape states */",
26 	"	short e_trans;	/* if set, this is an escp-trans */",
27 	"#endif",
28 	"	short tpe[2];	/* class of operation (for reduction) */",
29 	"	short qu[6];	/* for conditional selections: qid's  */",
30 	"	uchar ty[6];	/* ditto: type's */",
31 	"#ifdef NIBIS",
32 	"	short om;	/* completion status of preselects */",
33 	"#endif",
34 	"	char *tp;	/* src txt of statement */",
35 	"	int st;		/* the nextstate */",
36 	"	int t_id;	/* transition id, unique within proc */",
37 	"	int forw;	/* index forward transition */",
38 	"	int back;	/* index return  transition */",
39 	"	struct Trans *nxt;",
40 	"} Trans;\n",
41 
42 	"#ifdef TRIX",
43 	"	#define qptr(x)	(channels[x]->body)",
44 	"	#define pptr(x)	(processes[x]->body)",
45 	"#else",
46 	"	#define qptr(x)	(((uchar *)&now)+(int)q_offset[x])",
47 	"	#define pptr(x)	(((uchar *)&now)+(int)proc_offset[x])",
48 /*	"	#define Pptr(x)	((proc_offset[x])?pptr(x):noptr)",	*/
49 	"#endif",
50 	"extern uchar *Pptr(int);",
51 	"extern uchar *Qptr(int);",
52 
53 	"#define q_sz(x)	(((Q0 *)qptr(x))->Qlen)",
54 	"",
55 	"#ifdef TRIX",
56 	"	#ifdef VECTORSZ",
57 	"		#undef VECTORSZ",	/* backward compatibility */
58 	"	#endif",
59 	"	#if WS==4",
60 	"		#define VECTORSZ	2056	/* ((MAXPROC+MAXQ+4)*sizeof(uchar *)) */",
61 	"	#else",
62 	"		#define VECTORSZ	4112	/* the formula causes probs in preprocessing */",
63 	"	#endif",
64 	"#else",
65 	"	#ifndef VECTORSZ",
66 	"		#define VECTORSZ	1024	/* sv size in bytes */",
67 	"	#endif",
68 	"#endif\n",
69 	0,
70 };
71 
72 static char *Header[] = {
73 	"#ifdef VERBOSE",
74 	"	#ifndef CHECK",
75 	"		#define CHECK",
76 	"	#endif",
77 	"	#ifndef DEBUG",
78 	"		#define DEBUG",
79 	"	#endif",
80 	"#endif",
81 	"#ifdef SAFETY",
82 	"	#ifndef NOFAIR",
83 	"		#define NOFAIR",
84 	"	#endif",
85 	"#endif",
86 	"#ifdef NOREDUCE",
87 	"	#ifndef XUSAFE",
88 	"		#define XUSAFE",
89 	"	#endif",
90 	"	#if !defined(SAFETY) && !defined(MA)",
91 	"		#define FULLSTACK",
92 	"	#endif",
93 	"#else",
94 	"	#ifdef BITSTATE",
95 	"		#if defined(SAFETY) && !defined(HASH64)",
96 	"			#define CNTRSTACK",
97 	"		#else",
98 	"			#define FULLSTACK",
99 	"		#endif",
100 	"	#else",
101 	"		#define FULLSTACK",
102 	"	#endif",
103 	"#endif",
104 	"#ifdef BITSTATE",
105 	"	#ifndef NOCOMP",
106 	"		#define NOCOMP",
107 	"	#endif",
108 	"	#if !defined(LC) && defined(SC)",
109 	"		#define LC",
110 	"	#endif",
111 	"#endif",
112 	"#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)",
113 	"	/* accept the above for backward compatibility */",
114 	"	#define COLLAPSE",
115 	"#endif",
116 	"#ifdef HC",
117 	"	#undef HC",
118 	"	#define HC4",
119 	"#endif",
120 	"#ifdef HC0",	/* 32 bits */
121 	"	#define HC	0",
122 	"#endif",
123 	"#ifdef HC1",	/* 32+8 bits */
124 	"	#define HC	1",
125 	"#endif",
126 	"#ifdef HC2",	/* 32+16 bits */
127 	"	#define HC	2",
128 	"#endif",
129 	"#ifdef HC3",	/* 32+24 bits */
130 	"	#define HC	3",
131 	"#endif",
132 	"#ifdef HC4",	/* 32+32 bits - combine with -DMA=8 */
133 	"	#define HC	4",
134 	"#endif",
135 	"#ifdef COLLAPSE",
136 	"	#if NCORE>1 && !defined(SEP_STATE)",
137 	"		unsigned long *ncomps;	/* in shared memory */",
138 	"	#else",
139 	"		unsigned long ncomps[256+2];",
140 	"	#endif",
141 	"#endif",
142 
143 	"#define MAXQ   	255",
144 	"#define MAXPROC	255",
145 	"",
146 	"typedef struct _Stack  {	 /* for queues and processes */",
147 	"#if VECTORSZ>32000",
148 	"	int o_delta;",
149 	"	#ifndef TRIX",
150 	"		int o_offset;",
151 	"		int o_skip;",
152 	"	#endif",
153 	"	int o_delqs;",
154 	"#else",
155 	"	short o_delta;",
156 	"	#ifndef TRIX",
157 	"		short o_offset;",
158 	"		short o_skip;",
159 	"	#endif",
160 	"	short o_delqs;",
161 	"#endif",
162 	"	short o_boq;",
163 	"#ifdef TRIX",
164 	"	short parent;",
165 	"	char *b_ptr;",	/* used in delq/q_restor and delproc/p_restor */
166 	"#else",
167 	"	char *body;",	/* full copy of state vector in non-trix mode */
168 	"#endif",
169 	"#ifndef XUSAFE",
170 	"	char *o_name;",
171 	"#endif",
172 	"	struct _Stack *nxt;",
173 	"	struct _Stack *lst;",
174 	"} _Stack;\n",
175 	"typedef struct Svtack { /* for complete state vector */",
176 	"#if VECTORSZ>32000",
177 	"	int o_delta;",
178 	"	int m_delta;",
179 	"#else",
180 	"	short o_delta;	 /* current size of frame */",
181 	"	short m_delta;	 /* maximum size of frame */",
182 	"#endif",
183 	"#if SYNC",
184 	"	short o_boq;",
185 	"#endif",
186 	0,
187 };
188 
189 static char *Header0[] = {
190 	"	char *body;",
191 	"	struct Svtack *nxt;",
192 	"	struct Svtack *lst;",
193 	"} Svtack;\n",
194 	"Trans ***trans;	/* 1 ptr per state per proctype */\n",
195 	"struct H_el *Lstate;",
196 	"int depthfound = -1;	/* loop detection */",
197 
198 	"#ifndef TRIX",
199 	"	#if VECTORSZ>32000",
200 	"		int proc_offset[MAXPROC];",
201 	"		int q_offset[MAXQ];",
202 	"	#else",
203 	"		short proc_offset[MAXPROC];",
204 	"		short q_offset[MAXQ];",
205 	"	#endif",
206 	"	uchar proc_skip[MAXPROC];",
207 	"	uchar q_skip[MAXQ];",
208 	"#endif",
209 
210 	"unsigned long  vsize;	/* vector size in bytes */",
211 	"#ifdef SVDUMP",
212 	"	int vprefix=0, svfd;	/* runtime option -pN */",
213 	"#endif",
214 	"char *tprefix = \"trail\";	/* runtime option -tsuffix */",
215 	"short boq = -1;		/* blocked_on_queue status */",
216 	0,
217 };
218 
219 static char *Head1[] = {
220 	"typedef struct State {",
221 	"	uchar _nr_pr;",
222 	"	uchar _nr_qs;",
223 	"	uchar   _a_t;	/* cycle detection */",
224 #if 0
225 	in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs
226 	bit 1 is used as the A-bit for fairness
227 	bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance)
228 #endif
229 	"#ifndef NOFAIR",
230 	"	uchar   _cnt[NFAIR];	/* counters, weak fairness */",
231 	"#endif",
232 
233 	"#ifndef NOVSZ",
234 #ifdef SOLARIS
235 		"#if 0",
236 		/* v3.4
237 		 * noticed alignment problems with some Solaris
238 		 * compilers, if widest field isn't wordsized
239 		 */
240 #else
241 		"#if VECTORSZ<65536",
242 #endif
243 		"	unsigned short _vsz;",
244 		"#else",
245 		"	unsigned long  _vsz;",
246 		"#endif",
247 	"#endif",
248 
249 	"#ifdef HAS_LAST",	/* cannot go before _cnt - see hstore() */
250 	"	uchar  _last;	/* pid executed in last step */",
251 	"#endif",
252 
253 	"#if defined(BITSTATE) && defined(BCS) && defined(STORE_CTX)",
254 	"	uchar  _ctx;	/* nr of context switches so far */",
255 	"#endif",
256 
257 	"#ifdef EVENT_TRACE",
258 	"	#if nstates_event<256",
259 	"		uchar _event;",
260 	"	#else",
261 	"		unsigned short _event;",
262 	"	#endif",
263 	"#endif",
264 	0,
265 };
266 
267 static char *Addp0[] = {
268 	/* addproc(....parlist... */ ")",
269 	"{	int j, h = now._nr_pr;",
270 	"#ifndef NOCOMP",
271 	"	int k;",
272 	"#endif",
273 	"	uchar *o_this = this;\n",
274 	"#ifndef INLINE",
275 	"	if (TstOnly) return (h < MAXPROC);",
276 	"#endif",
277 	"#ifndef NOBOUNDCHECK",
278 	"	/* redefine Index only within this procedure */",
279 	"	#undef Index",
280 	"	#define Index(x, y)	Boundcheck(x, y, 0, 0, 0)",
281 	"#endif",
282 	"	if (h >= MAXPROC)",
283 	"		Uerror(\"too many processes\");",
284 	"#ifdef V_TRIX",
285 	"	printf(\"%%4d: add process %%d\\n\", depth, h);",
286 	"#endif",
287 	"	switch (n) {",
288 	"	case 0: j = sizeof(P0); break;",
289 	0,
290 };
291 
292 static char *Addp1[] = {
293 	"	default: Uerror(\"bad proc - addproc\");",
294 	"	}",
295 
296 	"#ifdef TRIX",
297 	"	vsize += sizeof(struct H_el *);",
298 	"#else",
299 	"	if (vsize%%WS)",
300 	"		proc_skip[h] = WS-(vsize%%WS);",
301 	"	else",
302 	"		proc_skip[h] = 0;",
303 	"	#ifndef NOCOMP",
304 	"		for (k = vsize + (int) proc_skip[h]; k > vsize; k--)",
305 	"			Mask[k-1] = 1; /* align */",
306 	"	#endif",
307 	"	vsize += (int) proc_skip[h];",
308 	"	proc_offset[h] = vsize;",
309 	"	vsize += j;",
310 	"	#if defined(SVDUMP) && defined(VERBOSE)",
311 	"	if (vprefix > 0)",
312 	"	{	int dummy = 0;",
313 	"		write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */",
314 	"		write(svfd, (uchar *) &h, sizeof(int));",
315 	"		write(svfd, (uchar *) &n, sizeof(int));",
316 	"	#if VECTORSZ>32000",
317 	"		write(svfd, (uchar *) &proc_offset[h], sizeof(int));",
318 	"		write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
319 	"	#else",
320 	"		write(svfd, (uchar *) &proc_offset[h], sizeof(short));",
321 	"		write(svfd, (uchar *) &now, vprefix-3*sizeof(int)-sizeof(short)); /* padd */",
322 	"	#endif",
323 	"	}",
324 	"	#endif",
325 	"#endif",
326 
327 	"	now._nr_pr += 1;",
328 	"#if defined(BCS) && defined(CONSERVATIVE)",
329 	"	if (now._nr_pr >= CONSERVATIVE*8)",
330 	"	{	printf(\"pan: error: too many processes -- recompile with \");",
331 	"		printf(\"-DCONSERVATIVE=%%d\\n\", CONSERVATIVE+1);",
332 	"		pan_exit(1);",
333 	"	}",
334 	"#endif",
335 	"	if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))",
336 	"	{	printf(\"pan: error: too many processes -- current\");",
337 	"		printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",",
338 	"			(8*NFAIR)/2 - 2, NFAIR);",
339 	"		printf(\"\\trecompile with -DNFAIR=%%d\\n\",",
340 	"			NFAIR+1);",
341 	"		pan_exit(1);",
342 	"	}",
343 	"#ifndef NOVSZ",
344 	"	now._vsz = vsize;",
345 	"#endif",
346 	"	hmax = max(hmax, vsize);",
347 
348 	"#ifdef TRIX",
349 	"	#ifndef BFS",
350 	"		if (freebodies)",
351 	"		{	processes[h] = freebodies;",
352 	"			freebodies = freebodies->nxt;",
353 	"		} else",
354 	"		{	processes[h] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
355 	"			processes[h]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
356 	"		}",
357 	"		processes[h]->modified = 1;	/* addproc */",
358 	"	#endif",
359 	"	processes[h]->psize = j;",
360 	"	processes[h]->parent_pid = calling_pid;",
361 	"	processes[h]->nxt = (TRIX_v6 *) 0;",
362 	"#else",
363 	"	#ifndef NOCOMP",
364 	"		for (k = 1; k <= Air[n]; k++)",
365 	"			Mask[vsize - k] = 1; /* pad */",
366 	"		Mask[vsize-j] = 1; /* _pid */",
367 	"	#endif",
368 	"	if (vsize >= VECTORSZ)",
369 	"	{	printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",
370 	"		printf(\" with -DVECTORSZ=N with N>%%d\\n\", (int) vsize);",
371 	"		Uerror(\"aborting\");",
372 	"	}",
373 	"#endif",
374 
375 	"	memset((char *)pptr(h), 0, j);",
376 	"	this = pptr(h);",
377 	"	if (BASE > 0 && h > 0)",
378 	"		((P0 *)this)->_pid = h-BASE;",
379 	"	else",
380 	"		((P0 *)this)->_pid = h;",
381 	"	switch (n) {",
382 	0,
383 };
384 
385 static char *Addq0[] = {
386 	"int",
387 	"addqueue(int calling_pid, int n, int is_rv)",
388 	"{	int j=0, i = now._nr_qs;",
389 	"#if !defined(NOCOMP) && !defined(TRIX)",
390 	"	int k;",
391 	"#endif",
392 	"	if (i >= MAXQ)",
393 	"		Uerror(\"too many queues\");",
394 	"#ifdef V_TRIX",
395 	"	printf(\"%%4d: add queue %%d\\n\", depth, i);",
396 	"#endif",
397 	"	switch (n) {",
398 	0,
399 };
400 
401 static char *Addq1[] = {
402 	"	default: Uerror(\"bad queue - addqueue\");",
403 	"	}",
404 
405 	"#ifdef TRIX",
406 	"	vsize += sizeof(struct H_el *);",
407 	"#else",
408 	"	if (vsize%%WS)",
409 	"		q_skip[i] = WS-(vsize%%WS);",
410 	"	else",
411 	"		q_skip[i] = 0;",
412 	"	#ifndef NOCOMP",
413 	"		k = vsize;",
414 	"		#ifndef BFS",
415 	"			if (is_rv) k += j;",
416 	"		#endif",
417 	"		for (k += (int) q_skip[i]; k > vsize; k--)",
418 	"			Mask[k-1] = 1;",
419 	"	#endif",
420 	"	vsize += (int) q_skip[i];",
421 	"	q_offset[i] = vsize;",
422 	"	vsize += j;",
423 	"#endif",
424 
425 	"	now._nr_qs += 1;",
426 	"#ifndef NOVSZ",
427 	"	now._vsz = vsize;",
428 	"#endif",
429 	"	hmax = max(hmax, vsize);",
430 
431 	"#ifdef TRIX",
432 	"	#ifndef BFS",
433 	"		if (freebodies)",
434 	"		{	channels[i] = freebodies;",
435 	"			freebodies = freebodies->nxt;",
436 	"		} else",
437 	"		{	channels[i] = (TRIX_v6 *) emalloc(sizeof(TRIX_v6));",
438 	"			channels[i]->body = (uchar *) emalloc(Maxbody * sizeof(char));",
439 	"		}",
440 	"		channels[i]->modified = 1;	/* addq */",
441 	"	#endif",
442 	"	channels[i]->psize = j;",
443 	"	channels[i]->parent_pid = calling_pid;",
444 	"	channels[i]->nxt = (TRIX_v6 *) 0;",
445 	"#else",
446 	"	if (vsize >= VECTORSZ)",
447 	"		Uerror(\"VECTORSZ is too small, edit pan.h\");",
448 	"#endif",
449 
450 	"	if (j > 0)", /* zero if there are no queues */
451 	"	{	memset((char *)qptr(i), 0, j);",
452 	"	}",
453 	"	((Q0 *)qptr(i))->_t = n;",
454 	"	return i+1;",
455 	"}\n",
456 	0,
457 };
458 
459 static char *Addq11[] = {
460 	"{	int j; uchar *z;\n",
461 	"#ifdef HAS_SORTED",
462 	"	int k;",
463 	"#endif",
464 	"	if (!into--)",
465 	"	uerror(\"ref to uninitialized chan name (sending)\");",
466 	"	if (into >= (int) now._nr_qs || into < 0)",
467 	"		Uerror(\"qsend bad queue#\");",
468 	"#if defined(TRIX) && !defined(BFS)",
469 	"	#ifndef TRIX_ORIG",
470 	"		(trpt+1)->q_bup = now._ids_[now._nr_pr+into];",
471 	"		#ifdef V_TRIX",
472 	"			printf(\"%%4d: channel %%d s save %%p from %%d\\n\",",
473 	"			depth, into, (trpt+1)->q_bup, now._nr_pr+into);",
474 	"		#endif",
475 	"	#endif",
476 	"	channels[into]->modified = 1;	/* qsend */",
477 	"	#ifdef V_TRIX",
478 	"		printf(\"%%4d: channel %%d modified\\n\", depth, into);",
479 	"	#endif",
480 	"#endif",
481 	"	z = qptr(into);",
482 	"	j = ((Q0 *)qptr(into))->Qlen;",
483 	"	switch (((Q0 *)qptr(into))->_t) {",
484 	0,
485 };
486 
487 static char *Addq2[] = {
488 	"	case 0: printf(\"queue %%d was deleted\\n\", into+1);",
489 	"	default: Uerror(\"bad queue - qsend\");",
490 	"	}",
491 	"#ifdef EVENT_TRACE",
492 	"	if (in_s_scope(into+1))",
493 	"		require('s', into);",
494 	"#endif",
495 	"}",
496 	"#endif\n",
497 	"#if SYNC",
498 	"int",
499 	"q_zero(int from)",
500 	"{	if (!from--)",
501 	"	{	uerror(\"ref to uninitialized chan name (q_zero)\");",
502 	"		return 0;",
503 	"	}",
504 	"	switch(((Q0 *)qptr(from))->_t) {",
505 	0,
506 };
507 
508 static char *Addq3[] = {
509 	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
510 	"	}",
511 	"	Uerror(\"bad queue q-zero\");",
512 	"	return -1;",
513 	"}",
514 	"int",
515 	"not_RV(int from)",
516 	"{	if (q_zero(from))",
517 	"	{	printf(\"==>> a test of the contents of a rv \");",
518 	"		printf(\"channel always returns FALSE\\n\");",
519 	"		uerror(\"error to poll rendezvous channel\");",
520 	"	}",
521 	"	return 1;",
522 	"}",
523 	"#endif",
524 	"#ifndef XUSAFE",
525 	"void",
526 	"setq_claim(int x, int m, char *s, int y, char *p)",
527 	"{	if (x == 0)",
528 	"	uerror(\"x[rs] claim on uninitialized channel\");",
529 	"	if (x < 0 || x > MAXQ)",
530 	"		Uerror(\"cannot happen setq_claim\");",
531 	"	q_claim[x] |= m;",
532 	"	p_name[y] = p;",
533 	"	q_name[x] = s;",
534 	"	if (m&2) q_S_check(x, y);",
535 	"	if (m&1) q_R_check(x, y);",
536 	"}",
537 	"short q_sender[MAXQ+1];",
538 	"int",
539 	"q_S_check(int x, int who)",
540 	"{	if (!q_sender[x])",
541 	"	{	q_sender[x] = who+1;",
542 	"#if SYNC",
543 	"		if (q_zero(x))",
544 	"		{	printf(\"chan %%s (%%d), \",",
545 	"				q_name[x], x-1);",
546 	"			printf(\"sndr proc %%s (%%d)\\n\",",
547 	"				p_name[who], who);",
548 	"			uerror(\"xs chans cannot be used for rv\");",
549 	"		}",
550 	"#endif",
551 	"	} else",
552 	"	if (q_sender[x] != who+1)",
553 	"	{	printf(\"pan: xs assertion violated: \");",
554 	"		printf(\"access to chan <%%s> (%%d)\\npan: by \",",
555 	"			q_name[x], x-1);",
556 	"		if (q_sender[x] > 0 && p_name[q_sender[x]-1])",
557 	"			printf(\"%%s (proc %%d) and by \",",
558 	"			p_name[q_sender[x]-1], q_sender[x]-1);",
559 	"		printf(\"%%s (proc %%d)\\n\",",
560 	"			p_name[who], who);",
561 	"		uerror(\"error, partial order reduction invalid\");",
562 	"	}",
563 	"	return 1;",
564 	"}",
565 	"short q_recver[MAXQ+1];",
566 	"int",
567 	"q_R_check(int x, int who)",
568 	"{	if (!q_recver[x])",
569 	"	{	q_recver[x] = who+1;",
570 	"#if SYNC",
571 	"		if (q_zero(x))",
572 	"		{	printf(\"chan %%s (%%d), \",",
573 	"				q_name[x], x-1);",
574 	"			printf(\"recv proc %%s (%%d)\\n\",",
575 	"				p_name[who], who);",
576 	"			uerror(\"xr chans cannot be used for rv\");",
577 	"		}",
578 	"#endif",
579 	"	} else",
580 	"	if (q_recver[x] != who+1)",
581 	"	{	printf(\"pan: xr assertion violated: \");",
582 	"		printf(\"access to chan %%s (%%d)\\npan: \",",
583 	"			q_name[x], x-1);",
584 	"		if (q_recver[x] > 0 && p_name[q_recver[x]-1])",
585 	"			printf(\"by %%s (proc %%d) and \",",
586 	"			p_name[q_recver[x]-1], q_recver[x]-1);",
587 	"		printf(\"by %%s (proc %%d)\\n\",",
588 	"			p_name[who], who);",
589 	"		uerror(\"error, partial order reduction invalid\");",
590 	"	}",
591 	"	return 1;",
592 	"}",
593 	"#endif",
594 	"int",
595 	"q_len(int x)",
596 	"{	if (!x--)",
597 	"	uerror(\"ref to uninitialized chan name (len)\");",
598 	"	return ((Q0 *)qptr(x))->Qlen;",
599 	"}\n",
600 	"int",
601 	"q_full(int from)",
602 	"{	if (!from--)",
603 	"	uerror(\"ref to uninitialized chan name (qfull)\");",
604 	"	switch(((Q0 *)qptr(from))->_t) {",
605 	0,
606 };
607 
608 static char *Addq4[] = {
609 	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
610 	"	}",
611 	"	Uerror(\"bad queue - q_full\");",
612 	"	return 0;",
613 	"}\n",
614 	"#ifdef HAS_UNLESS",
615 	"int",
616 	"q_e_f(int from)",
617 	"{	/* empty or full */",
618 	"	return !q_len(from) || q_full(from);",
619 	"}",
620 	"#endif",
621 	"#if NQS>0",
622 	"int",
623 	"qrecv(int from, int slot, int fld, int done)",
624 	"{	uchar *z;",
625 	"	int j, k, r=0;\n",
626 	"	if (!from--)",
627 	"	uerror(\"ref to uninitialized chan name (receiving)\");",
628 	"#if defined(TRIX) && !defined(BFS)",
629 	"	#ifndef TRIX_ORIG",
630 	"		(trpt+1)->q_bup = now._ids_[now._nr_pr+from];",
631 	"		#ifdef V_TRIX",
632 	"			printf(\"%%4d: channel %%d r save %%p from %%d\\n\",",
633 	"			depth, from, (trpt+1)->q_bup, now._nr_pr+from);",
634 	"		#endif",
635 	"	#endif",
636 	"	channels[from]->modified = 1;	/* qrecv */",
637 	"	#ifdef V_TRIX",
638 	"		printf(\"%%4d: channel %%d modified\\n\", depth, from);",
639 	"	#endif",
640 	"#endif",
641 	"	if (from >= (int) now._nr_qs || from < 0)",
642 	"		Uerror(\"qrecv bad queue#\");",
643 	"	z = qptr(from);",
644 	"#ifdef EVENT_TRACE",
645 	"	if (done && (in_r_scope(from+1)))",
646 	"		require('r', from);",
647 	"#endif",
648 	"	switch (((Q0 *)qptr(from))->_t) {",
649 	0,
650 };
651 
652 static char *Addq5[] = {
653 	"	case 0: printf(\"queue %%d was deleted\\n\", from+1);",
654 	"	default: Uerror(\"bad queue - qrecv\");",
655 	"	}",
656 	"	return r;",
657 	"}",
658 	"#endif\n",
659 	"#ifndef BITSTATE",
660 	"#ifdef COLLAPSE",
661 	"long",
662 	"col_q(int i, char *z)",
663 	"{	int j=0, k;",
664 	"	char *x, *y;",
665 	"	Q0 *ptr = (Q0 *) qptr(i);",
666 	"	switch (ptr->_t) {",
667 	0,
668 };
669 
670 static char *Code0[] = {
671 	"void",
672 	"run(void)",
673 	"{	/* int i; */",
674 	"	memset((char *)&now, 0, sizeof(State));",
675 	"	vsize = (unsigned long) (sizeof(State) - VECTORSZ);",
676 	"#ifndef NOVSZ",
677 	"	now._vsz = vsize;",
678 	"#endif",
679 	"#ifdef TRIX",
680 	"	if (VECTORSZ != sizeof(now._ids_))",
681 	"	{	printf(\"VECTORSZ is %%d, but should be %%d in this mode\\n\",",
682 	"			VECTORSZ, sizeof(now._ids_));",
683 	"		Uerror(\"VECTORSZ set incorrectly, recompile Spin (not pan.c)\");",
684 	"	}",
685 	"#endif",
686 	"/* optional provisioning statements, e.g. to */",
687 	"/* set hidden variables, used as constants */",
688 	"#ifdef PROV",
689 	"#include PROV",
690 	"#endif",
691 	"	settable();",
692 	0,
693 };
694 
695 static char *R0[] = {
696 	"	Maxbody = max(Maxbody, ((int) sizeof(P%d)));",
697 	"	reached[%d] = reached%d;",
698 	"	accpstate[%d] = (uchar *) emalloc(nstates%d);",
699 	"	progstate[%d] = (uchar *) emalloc(nstates%d);",
700 	"	loopstate%d = loopstate[%d] = (uchar *) emalloc(nstates%d);",
701 	"	stopstate[%d] = (uchar *) emalloc(nstates%d);",
702 	"	visstate[%d] = (uchar *) emalloc(nstates%d);",
703 	"	mapstate[%d] = (short *) emalloc(nstates%d * sizeof(short));",
704 	"#ifdef HAS_CODE",
705 	"	NrStates[%d] = nstates%d;",
706 	"#endif",
707 	"	stopstate[%d][endstate%d] = 1;",
708 	0,
709 };
710 
711 static char *R0a[] = {
712 	"	retrans(%d, nstates%d, start%d, src_ln%d, reached%d, loopstate%d);",
713 	0,
714 };
715 
716 static char *Code1[] = {
717 	"#ifdef NP",
718 	"	#define ACCEPT_LAB	1 /* at least 1 in np_ */",
719 	"#else",
720 	"	#define ACCEPT_LAB	%d /* user-defined accept labels */",
721 	"#endif",
722 	"#ifdef MEMCNT",
723 	"	#ifdef MEMLIM",
724 	"		#warning -DMEMLIM takes precedence over -DMEMCNT",
725 	"		#undef MEMCNT",
726 	"	#else",
727 	"		#if MEMCNT<20",
728 	"			#warning using minimal value -DMEMCNT=20 (=1MB)",
729 	"			#define MEMLIM	(1)",
730 	"			#undef MEMCNT",
731 	"		#else",
732 	"			#if MEMCNT==20",
733 	"				#define MEMLIM	(1)",
734 	"				#undef MEMCNT",
735 	"			#else",
736 	"			 #if MEMCNT>=50",
737 	"				#error excessive value for MEMCNT",
738 	"			 #else",
739 	"				#define MEMLIM	(1<<(MEMCNT-20))",
740 	"			 #endif",
741 	"			#endif",
742 	"		#endif",
743 	"	#endif",
744 	"#endif",
745 
746 	"#if NCORE>1 && !defined(MEMLIM)",
747 	"	#define MEMLIM	(2048)	/* need a default, using 2 GB */",
748 	"#endif",
749 	0,
750 };
751 
752 static char *Code3[] = {
753 	"#define PROG_LAB	%d /* progress labels */",
754 	0,
755 };
756 
757 static char *R2[] = {
758 	"uchar *accpstate[%d];",
759 	"uchar *progstate[%d];",
760 	"uchar *loopstate[%d];",
761 	"uchar *reached[%d];",
762 	"uchar *stopstate[%d];",
763 	"uchar *visstate[%d];",
764 	"short *mapstate[%d];",
765 	"#ifdef HAS_CODE",
766 	"	int NrStates[%d];",
767 	"#endif",
768 	0,
769 };
770 static char *R3[] = {
771 	"	Maxbody = max(Maxbody, ((int) sizeof(Q%d)));",
772 	0,
773 };
774 static char *R4[] = {
775 	"	r_ck(reached%d, nstates%d, %d, src_ln%d, src_file%d);",
776 	0,
777 };
778 static char *R5[] = {
779 	"	case %d: j = sizeof(P%d); break;",
780 	0,
781 };
782 static char *R6[] = {
783 	"	}",
784 	"	this = o_this;",
785 	"#ifdef TRIX",
786 	"	re_mark_all(1); /* addproc */",
787 	"#endif",
788 	"	return h-BASE;",
789 	"#ifndef NOBOUNDCHECK",
790 	"	#undef Index",
791 	"	#define Index(x, y)	Boundcheck(x, y, II, tt, t)",
792 	"#endif",
793 	"}\n",
794 	"#if defined(BITSTATE) && defined(COLLAPSE)",
795 	"	/* just to allow compilation, to generate the error */",
796 	"	long col_p(int i, char *z) { return 0; }",
797 	"	long col_q(int i, char *z) { return 0; }",
798 	"#endif",
799 	"#ifndef BITSTATE",
800 	"	#ifdef COLLAPSE",
801 	"long",
802 	"col_p(int i, char *z)",
803 	"{	int j, k; unsigned long ordinal(char *, long, short);",
804 	"	char *x, *y;",
805 	"	P0 *ptr = (P0 *) pptr(i);",
806 	"	switch (ptr->_t) {",
807 	"	case 0: j = sizeof(P0); break;",
808 	0,
809 };
810 static char *R8a[] = {
811 	"	default: Uerror(\"bad proctype - collapse\");",
812 	"	}",
813 	"	if (z) x = z; else x = scratch;",
814 	"	y = (char *) ptr; k = proc_offset[i];",
815 
816 	"	for ( ; j > 0; j--, y++)",
817 	"		if (!Mask[k++]) *x++ = *y;",
818 
819 	"	for (j = 0; j < WS-1; j++)",
820 	"		*x++ = 0;",
821 	"	x -= j;",
822 	"	if (z) return (long) (x - z);",
823 	"	return ordinal(scratch, x-scratch, (short) (2+ptr->_t));",
824 	"}",
825 	"	#endif",
826 	"#endif",
827 	0,
828 };
829 static char *R8b[] = {
830 	"	default: Uerror(\"bad qtype - collapse\");",
831 	"	}",
832 	"	if (z) x = z; else x = scratch;",
833 	"	y = (char *) ptr; k = q_offset[i];",
834 
835 	"	/* no need to store the empty slots at the end */",
836 	"	j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);",
837 
838 	"	for ( ; j > 0; j--, y++)",
839 	"		if (!Mask[k++]) *x++ = *y;",
840 
841 	"	for (j = 0; j < WS-1; j++)",
842 	"		*x++ = 0;",
843 	"	x -= j;",
844 	"	if (z) return (long) (x - z);",
845 	"	return ordinal(scratch, x-scratch, 1); /* chan */",
846 	"}",
847 	"	#endif",
848 	"#endif",
849 	0,
850 };
851 
852 static char *R12[] = {
853 	"\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
854 	0,
855 };
856 char *R13[] = {
857 	"int ",
858 	"unsend(int into)",
859 	"{	int _m=0, j; uchar *z;\n",
860 	"#ifdef HAS_SORTED",
861 	"	int k;",
862 	"#endif",
863 	"	if (!into--)",
864 	"		uerror(\"ref to uninitialized chan (unsend)\");",
865 	"#if defined(TRIX) && !defined(BFS)",
866 	"	#ifndef TRIX_ORIG",
867 	"		now._ids_[now._nr_pr+into] = trpt->q_bup;",
868 	"		#ifdef V_TRIX",
869 	"			printf(\"%%4d: channel %%d s restore %%p into %%d\\n\",",
870 	"				depth, into, trpt->q_bup, now._nr_pr+into);",
871 	"		#endif",
872 	"	#else",
873 	"		channels[into]->modified = 1;	/* unsend */",
874 	"		#ifdef V_TRIX",
875 	"			printf(\"%%4d: channel %%d unmodify\\n\", depth, into);",
876 	"		#endif",
877 	"	#endif",
878 	"#endif",
879 	"	z = qptr(into);",
880 	"	j = ((Q0 *)z)->Qlen;",
881 	"	((Q0 *)z)->Qlen = --j;",
882 	"	switch (((Q0 *)qptr(into))->_t) {",
883 	0,
884 };
885 char *R14[] = {
886 	"	default: Uerror(\"bad queue - unsend\");",
887 	"	}",
888 	"	return _m;",
889 	"}\n",
890 	"void",
891 	"unrecv(int from, int slot, int fld, int fldvar, int strt)",
892 	"{	int j; uchar *z;\n",
893 	"	if (!from--)",
894 	"		uerror(\"ref to uninitialized chan (unrecv)\");",
895 	"#if defined(TRIX) && !defined(BFS)",
896 	"	#ifndef TRIX_ORIG",
897 	"		now._ids_[now._nr_pr+from] = trpt->q_bup;",
898 	"		#ifdef V_TRIX",
899 	"			printf(\"%%4d: channel %%d r restore %%p into %%d\\n\",",
900 	"				depth, from, trpt->q_bup, now._nr_pr+from);",
901 	"		#endif",
902 	"	#else",
903 	"		channels[from]->modified = 1;	/* unrecv */",
904 	"		#ifdef V_TRIX",
905 	"			printf(\"%%4d: channel %%d unmodify\\n\", depth, from);",
906 	"		#endif",
907 	"	#endif",
908 	"#endif",
909 	"	z = qptr(from);",
910 	"	j = ((Q0 *)z)->Qlen;",
911 	"	if (strt) ((Q0 *)z)->Qlen = j+1;",
912 	"	switch (((Q0 *)qptr(from))->_t) {",
913 	0,
914 };
915 char *R15[] = {
916 	"	default: Uerror(\"bad queue - qrecv\");",
917 	"	}",
918 	"}",
919 	0,
920 };
921 static char *Proto[] = {
922 	"",
923 	"/** function prototypes **/",
924 	"char *emalloc(unsigned long);",
925 	"char *Malloc(unsigned long);",
926 	"int Boundcheck(int, int, int, int, Trans *);",
927 	"int addqueue(int, int, int);",
928 	"/* int atoi(char *); */",
929 	"/* int abort(void); */",
930 	"int close(int);",	/* should probably remove this */
931 #if 0
932 	"#ifndef SC",
933 	"	int creat(char *, unsigned short);",
934 	"	int write(int, void *, unsigned);",
935 	"#endif",
936 #endif
937 	"int delproc(int, int);",
938 	"int endstate(void);",
939 	"int hstore(char *, int);",
940 "#ifdef MA",
941 	"int gstore(char *, int, uchar);",
942 "#endif",
943 	"int q_cond(short, Trans *);",
944 	"int q_full(int);",
945 	"int q_len(int);",
946 	"int q_zero(int);",
947 	"int qrecv(int, int, int, int);",
948 	"int unsend(int);",
949 	"/* void *sbrk(int); */",
950 	"void Uerror(char *);",
951 	"void spin_assert(int, char *, int, int, Trans *);",
952 	"void c_chandump(int);",
953 	"void c_globals(void);",
954 	"void c_locals(int, int);",
955 	"void checkcycles(void);",
956 	"void crack(int, int, Trans *, short *);",
957 	"void d_sfh(const char *, int);",
958 	"void sfh(const char *, int);",
959 	"void d_hash(uchar *, int);",
960 	"void s_hash(uchar *, int);",
961 	"void r_hash(uchar *, int);",
962 	"void delq(int);",
963 	"void dot_crack(int, int, Trans *);",
964 	"void do_reach(void);",
965 	"void pan_exit(int);",
966 	"void exit(int);",
967 	"void hinit(void);",
968 	"void imed(Trans *, int, int, int);",
969 	"void new_state(void);",
970 	"void p_restor(int);",
971 	"void putpeg(int, int);",
972 	"void putrail(void);",
973 	"void q_restor(void);",
974 	"void retrans(int, int, int, short *, uchar *, uchar *);",
975 	"void settable(void);",
976 	"void setq_claim(int, int, char *, int, char *);",
977 	"void sv_restor(void);",
978 	"void sv_save(void);",
979 	"void tagtable(int, int, int, short *, uchar *);",
980 	"void do_dfs(int, int, int, short *, uchar *, uchar *);",
981 	"void uerror(char *);",
982 	"void unrecv(int, int, int, int, int);",
983 	"void usage(FILE *);",
984 	"void wrap_stats(void);",
985 	"#if defined(FULLSTACK) && defined(BITSTATE)",
986 	"	int  onstack_now(void);",
987 	"	void onstack_init(void);",
988 	"	void onstack_put(void);",
989 	"	void onstack_zap(void);",
990 	"#endif",
991 	"#ifndef XUSAFE",
992 	"	int q_S_check(int, int);",
993 	"	int q_R_check(int, int);",
994 	"	uchar q_claim[MAXQ+1];",
995 	"	char *q_name[MAXQ+1];",
996 	"	char *p_name[MAXPROC+1];",
997 	"#endif",
998 	0,
999 };
1000 
1001 static char *SvMap[] = {
1002 	"void",
1003 	"to_compile(void)",
1004 	"{	char ctd[1024], carg[64];",
1005 	"#ifdef BITSTATE",
1006 	"	strcpy(ctd, \"-DBITSTATE \");",
1007 	"#else",
1008 	"	strcpy(ctd, \"\");",
1009 	"#endif",
1010 	"#ifdef NOVSZ",
1011 	"	strcat(ctd, \"-DNOVSZ \");",
1012 	"#endif",
1013 	"#ifdef REVERSE",
1014 	"	strcat(ctd, \"-DREVERSE \");",
1015 	"#endif",
1016 	"#ifdef T_REVERSE",
1017 	"	strcat(ctd, \"-DT_REVERSE \");",
1018 	"#endif",
1019 	"#ifdef T_RAND",
1020 	"	#if T_RAND>0",
1021 	"	sprintf(carg, \"-DT_RAND=%%d \", T_RAND);",
1022 	"	strcat(ctd, carg);",
1023 	"	#else",
1024 	"	strcat(ctd, \"-DT_RAND \");",
1025 	"	#endif",
1026 	"#endif",
1027 	"#ifdef P_RAND",
1028 	"	#if P_RAND>0",
1029 	"	sprintf(carg, \"-DP_RAND=%%d \", P_RAND);",
1030 	"	strcat(ctd, carg);",
1031 	"	#else",
1032 	"	strcat(ctd, \"-DP_RAND \");",
1033 	"	#endif",
1034 	"#endif",
1035 	"#ifdef BCS",
1036 	"	sprintf(carg, \"-DBCS=%%d \", BCS);",
1037 	"	strcat(ctd, carg);",
1038 	"#endif",
1039 	"#ifdef BFS",
1040 	"	strcat(ctd, \"-DBFS \");",
1041 	"#endif",
1042 	"#ifdef MEMLIM",
1043 	"	sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);",
1044 	"	strcat(ctd, carg);",
1045 	"#else",
1046 	"#ifdef MEMCNT",
1047 	"	sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);",
1048 	"	strcat(ctd, carg);",
1049 	"#endif",
1050 	"#endif",
1051 	"#ifdef NOCLAIM",
1052 	"	strcat(ctd, \"-DNOCLAIM \");",
1053 	"#endif",
1054 	"#ifdef SAFETY",
1055 	"	strcat(ctd, \"-DSAFETY \");",
1056 	"#else",
1057 		"#ifdef NOFAIR",
1058 		"	strcat(ctd, \"-DNOFAIR \");",
1059 		"#else",
1060 			"#ifdef NFAIR",
1061 		"	if (NFAIR != 2)",
1062 		"	{	sprintf(carg, \"-DNFAIR=%%d \", NFAIR);",
1063 		"		strcat(ctd, carg);",
1064 		"	}",
1065 			"#endif",
1066 		"#endif",
1067 	"#endif",
1068 	"#ifdef NOREDUCE",
1069 	"	strcat(ctd, \"-DNOREDUCE \");",
1070 	"#else",
1071 		"#ifdef XUSAFE",
1072 		"	strcat(ctd, \"-DXUSAFE \");",
1073 		"#endif",
1074 	"#endif",
1075 	"#ifdef NP",
1076 	"	strcat(ctd, \"-DNP \");",
1077 	"#endif",
1078 	"#ifdef PEG",
1079 	"	strcat(ctd, \"-DPEG \");",
1080 	"#endif",
1081 	"#ifdef VAR_RANGES",
1082 	"	strcat(ctd, \"-DVAR_RANGES \");",
1083 	"#endif",
1084 	"#ifdef HC0",
1085 	"	strcat(ctd, \"-DHC0 \");",
1086 	"#endif",
1087 	"#ifdef HC1",
1088 	"	strcat(ctd, \"-DHC1 \");",
1089 	"#endif",
1090 	"#ifdef HC2",
1091 	"	strcat(ctd, \"-DHC2 \");",
1092 	"#endif",
1093 	"#ifdef HC3",
1094 	"	strcat(ctd, \"-DHC3 \");",
1095 	"#endif",
1096 	"#ifdef HC4",
1097 	"	strcat(ctd, \"-DHC4 \");",
1098 	"#endif",
1099 	"#ifdef CHECK",
1100 	"	strcat(ctd, \"-DCHECK \");",
1101 	"#endif",
1102 	"#ifdef CTL",
1103 	"	strcat(ctd, \"-DCTL \");",
1104 	"#endif",
1105 	"#ifdef TRIX",
1106 	"	strcat(ctd, \"-DTRIX \");",
1107 	"#endif",
1108 	"#ifdef NIBIS",
1109 	"	strcat(ctd, \"-DNIBIS \");",
1110 	"#endif",
1111 	"#ifdef NOBOUNDCHECK",
1112 	"	strcat(ctd, \"-DNOBOUNDCHECK \");",
1113 	"#endif",
1114 	"#ifdef NOSTUTTER",
1115 	"	strcat(ctd, \"-DNOSTUTTER \");",
1116 	"#endif",
1117 	"#ifdef REACH",
1118 	"	strcat(ctd, \"-DREACH \");",
1119 	"#endif",
1120 	"#ifdef PRINTF",
1121 	"	strcat(ctd, \"-DPRINTF \");",
1122 	"#endif",
1123 	"#ifdef OTIM",
1124 	"	strcat(ctd, \"-DOTIM \");",
1125 	"#endif",
1126 	"#ifdef COLLAPSE",
1127 	"	strcat(ctd, \"-DCOLLAPSE \");",
1128 	"#endif",
1129 	"#ifdef MA",
1130 	"	sprintf(carg, \"-DMA=%%d \", MA);",
1131 	"	strcat(ctd, carg);",
1132 	"#endif",
1133 	"#ifdef SVDUMP",
1134 	"	strcat(ctd, \"-DSVDUMP \");",
1135 	"#endif",
1136 	"#if defined(VECTORSZ) && !defined(TRIX)",
1137 	"	if (VECTORSZ != 1024)",
1138 	"	{	sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);",
1139 	"		strcat(ctd, carg);",
1140 	"	}",
1141 	"#endif",
1142 	"#ifdef VERBOSE",
1143 	"	strcat(ctd, \"-DVERBOSE \");",
1144 	"#endif",
1145 	"#ifdef CHECK",
1146 	"	strcat(ctd, \"-DCHECK \");",
1147 	"#endif",
1148 	"#ifdef SDUMP",
1149 	"	strcat(ctd, \"-DSDUMP \");",
1150 	"#endif",
1151 	"#if NCORE>1",
1152 	"	sprintf(carg, \"-DNCORE=%%d \", NCORE);",
1153 	"	strcat(ctd, carg);",
1154 	"#endif",
1155 	"#ifdef SFH",
1156 	"	sprintf(carg, \"-DSFH \");",
1157 	"	strcat(ctd, carg);",
1158 	"#endif",
1159 	"#ifdef VMAX",
1160 	"	if (VMAX != 256)",
1161 	"	{	sprintf(carg, \"-DVMAX=%%d \", VMAX);",
1162 	"		strcat(ctd, carg);",
1163 	"	}",
1164 	"#endif",
1165 	"#ifdef PMAX",
1166 	"	if (PMAX != 16)",
1167 	"	{	sprintf(carg, \"-DPMAX=%%d \", PMAX);",
1168 	"		strcat(ctd, carg);",
1169 	"	}",
1170 	"#endif",
1171 	"#ifdef QMAX",
1172 	"	if (QMAX != 16)",
1173 	"	{	sprintf(carg, \"-DQMAX=%%d \", QMAX);",
1174 	"		strcat(ctd, carg);",
1175 	"	}",
1176 	"#endif",
1177 	"#ifdef SET_WQ_SIZE",
1178 	"	sprintf(carg, \"-DSET_WQ_SIZE=%%d \", SET_WQ_SIZE);",
1179 	"	strcat(ctd, carg);",
1180 	"#endif",
1181 	"	printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);",
1182 	"}",
1183 	0,
1184 };
1185