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