projects / lttv.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Src5.1.6 / pangen3.h
CommitLineData
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
13static 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
53static 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
161static 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
187static 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
230static 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
252static 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
314static 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
327static 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
359static 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
374static 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
395static 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
495static 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
526static 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
544static 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
562static 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
578static char *R0a[] = {
579 " retrans(%d, nstates%d, start%d, src_ln%d, reached%d, loopstate%d);",
580 0,
581};
582static 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
598static 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
634static char *Code3[] = {
635 "#define PROG_LAB %d /* progress labels */",
636 0,
637};
638
639static 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};
652static char *R3[] = {
653 " Maxbody = max(Maxbody, ((int) sizeof(Q%d)));",
654 0,
655};
656static char *R4[] = {
657 " r_ck(reached%d, nstates%d, %d, src_ln%d, src_file%d);",
658 0,
659};
660static char *R5[] = {
661 " case %d: j = sizeof(P%d); break;",
662 0,
663};
664static 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};
689static 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};
708static 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
731static char *R12[] = {
732 "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
733 0,
734};
735char *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};
750char *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};
766char *R15[] = {
767 " default: Uerror(\"bad queue - qrecv\");",
768 " }",
769 "}",
770 0,
771};
772static 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
851static 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};
LTTng 2.x Viewer (LTTV)
This page took 0.060481 seconds and 4 git commands to generate.