--- /dev/null
+/***** spin: pangen3.h *****/
+
+/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
+/* All Rights Reserved. This software is for educational purposes only. */
+/* No guarantee whatsoever is expressed or implied by the distribution of */
+/* this code. Permission is given to distribute this code provided that */
+/* this introductory message is not removed and no monies are exchanged. */
+/* Software written by Gerard J. Holzmann. For tool documentation see: */
+/* http://spinroot.com/ */
+/* Send all bug-reports and/or questions to: bugs@spinroot.com */
+/* (c) 2007: small additions for V5.0 to support multi-core verifications */
+
+static char *Head0[] = {
+ "#if defined(BFS) && defined(REACH)",
+ "#undef REACH", /* redundant with bfs */
+ "#endif",
+ "#ifdef VERI",
+ "#define BASE 1",
+ "#else",
+ "#define BASE 0",
+ "#endif",
+ "typedef struct Trans {",
+ " short atom; /* if &2 = atomic trans; if &8 local */",
+ "#ifdef HAS_UNLESS",
+ " short escp[HAS_UNLESS]; /* lists the escape states */",
+ " short e_trans; /* if set, this is an escp-trans */",
+ "#endif",
+ " short tpe[2]; /* class of operation (for reduction) */",
+ " short qu[6]; /* for conditional selections: qid's */",
+ " uchar ty[6]; /* ditto: type's */",
+ "#ifdef NIBIS",
+ " short om; /* completion status of preselects */",
+ "#endif",
+ " char *tp; /* src txt of statement */",
+ " int st; /* the nextstate */",
+ " int t_id; /* transition id, unique within proc */",
+ " int forw; /* index forward transition */",
+ " int back; /* index return transition */",
+ " struct Trans *nxt;",
+ "} Trans;\n",
+ "#define qptr(x) (((uchar *)&now)+(int)q_offset[x])",
+ "#define pptr(x) (((uchar *)&now)+(int)proc_offset[x])",
+/* "#define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", */
+ "extern uchar *Pptr(int);",
+
+ "#define q_sz(x) (((Q0 *)qptr(x))->Qlen)\n",
+ "#ifndef VECTORSZ",
+ "#define VECTORSZ 1024 /* sv size in bytes */",
+ "#endif\n",
+ 0,
+};
+
+static char *Header[] = {
+ "#ifdef VERBOSE",
+ "#ifndef CHECK",
+ "#define CHECK",
+ "#endif",
+ "#ifndef DEBUG",
+ "#define DEBUG",
+ "#endif",
+ "#endif",
+ "#ifdef SAFETY",
+ "#ifndef NOFAIR",
+ "#define NOFAIR",
+ "#endif",
+ "#endif",
+ "#ifdef NOREDUCE",
+ "#ifndef XUSAFE",
+ "#define XUSAFE",
+ "#endif",
+ "#if !defined(SAFETY) && !defined(MA)",
+ "#define FULLSTACK",
+ "#endif",
+ "#else",
+ "#ifdef BITSTATE",
+ "#if defined(SAFETY) && !defined(HASH64)",
+ "#define CNTRSTACK",
+ "#else",
+ "#define FULLSTACK",
+ "#endif",
+ "#else",
+ "#define FULLSTACK",
+ "#endif",
+ "#endif",
+ "#ifdef BITSTATE",
+ "#ifndef NOCOMP",
+ "#define NOCOMP",
+ "#endif",
+ "#if !defined(LC) && defined(SC)",
+ "#define LC",
+ "#endif",
+ "#endif",
+ "#if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)",
+ "/* accept the above for backward compatibility */",
+ "#define COLLAPSE",
+ "#endif",
+ "#ifdef HC",
+ "#undef HC",
+ "#define HC4",
+ "#endif",
+ "#ifdef HC0", /* 32 bits */
+ "#define HC 0",
+ "#endif",
+ "#ifdef HC1", /* 32+8 bits */
+ "#define HC 1",
+ "#endif",
+ "#ifdef HC2", /* 32+16 bits */
+ "#define HC 2",
+ "#endif",
+ "#ifdef HC3", /* 32+24 bits */
+ "#define HC 3",
+ "#endif",
+ "#ifdef HC4", /* 32+32 bits - combine with -DMA=8 */
+ "#define HC 4",
+ "#endif",
+ "#ifdef COLLAPSE",
+ "#if NCORE>1 && !defined(SEP_STATE)",
+ "unsigned long *ncomps; /* in shared memory */",
+ "#else",
+ "unsigned long ncomps[256+2];",
+ "#endif",
+ "#endif",
+
+ "#define MAXQ 255",
+ "#define MAXPROC 255",
+ "#define WS sizeof(void *) /* word size in bytes */",
+ "typedef struct Stack { /* for queues and processes */",
+ "#if VECTORSZ>32000",
+ " int o_delta;",
+ " int o_offset;",
+ " int o_skip;",
+ " int o_delqs;",
+ "#else",
+ " short o_delta;",
+ " short o_offset;",
+ " short o_skip;",
+ " short o_delqs;",
+ "#endif",
+ " short o_boq;",
+ "#ifndef XUSAFE",
+ " char *o_name;",
+ "#endif",
+ " char *body;",
+ " struct Stack *nxt;",
+ " struct Stack *lst;",
+ "} Stack;\n",
+ "typedef struct Svtack { /* for complete state vector */",
+ "#if VECTORSZ>32000",
+ " int o_delta;",
+ " int m_delta;",
+ "#else",
+ " short o_delta; /* current size of frame */",
+ " short m_delta; /* maximum size of frame */",
+ "#endif",
+ "#if SYNC",
+ " short o_boq;",
+ "#endif",
+ 0,
+};
+
+static char *Header0[] = {
+ " char *body;",
+ " struct Svtack *nxt;",
+ " struct Svtack *lst;",
+ "} Svtack;\n",
+ "Trans ***trans; /* 1 ptr per state per proctype */\n",
+ "struct H_el *Lstate;",
+ "int depthfound = -1; /* loop detection */",
+ "#if VECTORSZ>32000",
+ "int proc_offset[MAXPROC];",
+ "int q_offset[MAXQ];",
+ "#else",
+ "short proc_offset[MAXPROC];",
+ "short q_offset[MAXQ];",
+ "#endif",
+ "uchar proc_skip[MAXPROC];",
+ "uchar q_skip[MAXQ];",
+ "unsigned long vsize; /* vector size in bytes */",
+ "#ifdef SVDUMP",
+ "int vprefix=0, svfd; /* runtime option -pN */",
+ "#endif",
+ "char *tprefix = \"trail\"; /* runtime option -tsuffix */",
+ "short boq = -1; /* blocked_on_queue status */",
+ 0,
+};
+
+static char *Head1[] = {
+ "typedef struct State {",
+ " uchar _nr_pr;",
+ " uchar _nr_qs;",
+ " uchar _a_t; /* cycle detection */",
+#if 0
+ in _a_t: bits 0,4, and 5 =(1|16|32) are set during a 2nd dfs
+ bit 1 is used as the A-bit for fairness
+ bit 7 (128) is the proviso bit, for reduced 2nd dfs (acceptance)
+#endif
+ "#ifndef NOFAIR",
+ " uchar _cnt[NFAIR]; /* counters, weak fairness */",
+ "#endif",
+
+ "#ifndef NOVSZ",
+#ifdef SOLARIS
+ "#if 0",
+ /* v3.4
+ * noticed alignment problems with some Solaris
+ * compilers, if widest field isn't wordsized
+ */
+#else
+ "#if VECTORSZ<65536",
+#endif
+ " unsigned short _vsz;",
+ "#else",
+ " unsigned long _vsz;",
+ "#endif",
+ "#endif",
+
+ "#ifdef HAS_LAST", /* cannot go before _cnt - see hstore() */
+ " uchar _last; /* pid executed in last step */",
+ "#endif",
+ "#ifdef EVENT_TRACE",
+ "#if nstates_event<256",
+ " uchar _event;",
+ "#else",
+ " unsigned short _event;",
+ "#endif",
+ "#endif",
+ 0,
+};
+
+static char *Addp0[] = {
+ /* addproc(....parlist... */ ")",
+ "{ int j, h = now._nr_pr;",
+ "#ifndef NOCOMP",
+ " int k;",
+ "#endif",
+ " uchar *o_this = this;\n",
+ "#ifndef INLINE",
+ " if (TstOnly) return (h < MAXPROC);",
+ "#endif",
+ "#ifndef NOBOUNDCHECK",
+ "/* redefine Index only within this procedure */",
+ "#undef Index",
+ "#define Index(x, y) Boundcheck(x, y, 0, 0, 0)",
+ "#endif",
+ " if (h >= MAXPROC)",
+ " Uerror(\"too many processes\");",
+ " switch (n) {",
+ " case 0: j = sizeof(P0); break;",
+ 0,
+};
+
+static char *Addp1[] = {
+ " default: Uerror(\"bad proc - addproc\");",
+ " }",
+ " if (vsize%%WS)",
+ " proc_skip[h] = WS-(vsize%%WS);",
+ " else",
+ " proc_skip[h] = 0;",
+ "#ifndef NOCOMP",
+ " for (k = vsize + (int) proc_skip[h]; k > vsize; k--)",
+ " Mask[k-1] = 1; /* align */",
+ "#endif",
+ " vsize += (int) proc_skip[h];",
+ " proc_offset[h] = vsize;",
+ "#ifdef SVDUMP",
+ " if (vprefix > 0)",
+ " { int dummy = 0;",
+ " write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */",
+ " write(svfd, (uchar *) &h, sizeof(int));",
+ " write(svfd, (uchar *) &n, sizeof(int));",
+ "#if VECTORSZ>32000",
+ " write(svfd, (uchar *) &proc_offset[h], sizeof(int));",
+ "#else",
+ " write(svfd, (uchar *) &proc_offset[h], sizeof(short));",
+ "#endif",
+ " write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */",
+ " }",
+ "#endif",
+ " now._nr_pr += 1;",
+ " if (fairness && ((int) now._nr_pr + 1 >= (8*NFAIR)/2))",
+ " { printf(\"pan: error: too many processes -- current\");",
+ " printf(\" max is %%d procs (-DNFAIR=%%d)\\n\",",
+ " (8*NFAIR)/2 - 2, NFAIR);",
+ " printf(\"\\trecompile with -DNFAIR=%%d\\n\",",
+ " NFAIR+1);",
+ " pan_exit(1);",
+ " }",
+
+ " vsize += j;",
+ "#ifndef NOVSZ",
+ " now._vsz = vsize;",
+ "#endif",
+ "#ifndef NOCOMP",
+ " for (k = 1; k <= Air[n]; k++)",
+ " Mask[vsize - k] = 1; /* pad */",
+ " Mask[vsize-j] = 1; /* _pid */",
+ "#endif",
+ " hmax = max(hmax, vsize);",
+ " if (vsize >= VECTORSZ)",
+ " { printf(\"pan: error, VECTORSZ too small, recompile pan.c\");",
+ " printf(\" with -DVECTORSZ=N with N>%%d\\n\", (int) vsize);",
+ " Uerror(\"aborting\");",
+ " }",
+ " memset((char *)pptr(h), 0, j);",
+ " this = pptr(h);",
+ " if (BASE > 0 && h > 0)",
+ " ((P0 *)this)->_pid = h-BASE;",
+ " else",
+ " ((P0 *)this)->_pid = h;",
+ " switch (n) {",
+ 0,
+};
+
+static char *Addq0[] = {
+ "int",
+ "addqueue(int n, int is_rv)",
+ "{ int j=0, i = now._nr_qs;",
+ "#ifndef NOCOMP",
+ " int k;",
+ "#endif",
+ " if (i >= MAXQ)",
+ " Uerror(\"too many queues\");",
+ " switch (n) {",
+ 0,
+};
+
+static char *Addq1[] = {
+ " default: Uerror(\"bad queue - addqueue\");",
+ " }",
+ " if (vsize%%WS)",
+ " q_skip[i] = WS-(vsize%%WS);",
+ " else",
+ " q_skip[i] = 0;",
+ "#ifndef NOCOMP",
+ " k = vsize;",
+ "#ifndef BFS",
+ " if (is_rv) k += j;",
+ "#endif",
+ " for (k += (int) q_skip[i]; k > vsize; k--)",
+ " Mask[k-1] = 1;",
+ "#endif",
+ " vsize += (int) q_skip[i];",
+ " q_offset[i] = vsize;",
+ " now._nr_qs += 1;",
+ " vsize += j;",
+ "#ifndef NOVSZ",
+ " now._vsz = vsize;",
+ "#endif",
+ " hmax = max(hmax, vsize);",
+ " if (vsize >= VECTORSZ)",
+ " Uerror(\"VECTORSZ is too small, edit pan.h\");",
+ " memset((char *)qptr(i), 0, j);",
+ " ((Q0 *)qptr(i))->_t = n;",
+ " return i+1;",
+ "}\n",
+ 0,
+};
+
+static char *Addq11[] = {
+ "{ int j; uchar *z;\n",
+ "#ifdef HAS_SORTED",
+ " int k;",
+ "#endif",
+ " if (!into--)",
+ " uerror(\"ref to uninitialized chan name (sending)\");",
+ " if (into >= (int) now._nr_qs || into < 0)",
+ " Uerror(\"qsend bad queue#\");",
+ " z = qptr(into);",
+ " j = ((Q0 *)qptr(into))->Qlen;",
+ " switch (((Q0 *)qptr(into))->_t) {",
+ 0,
+};
+
+static char *Addq2[] = {
+ " case 0: printf(\"queue %%d was deleted\\n\", into+1);",
+ " default: Uerror(\"bad queue - qsend\");",
+ " }",
+ "#ifdef EVENT_TRACE",
+ " if (in_s_scope(into+1))",
+ " require('s', into);",
+ "#endif",
+ "}",
+ "#endif\n",
+ "#if SYNC",
+ "int",
+ "q_zero(int from)",
+ "{ if (!from--)",
+ " { uerror(\"ref to uninitialized chan name (q_zero)\");",
+ " return 0;",
+ " }",
+ " switch(((Q0 *)qptr(from))->_t) {",
+ 0,
+};
+
+static char *Addq3[] = {
+ " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
+ " }",
+ " Uerror(\"bad queue q-zero\");",
+ " return -1;",
+ "}",
+ "int",
+ "not_RV(int from)",
+ "{ if (q_zero(from))",
+ " { printf(\"==>> a test of the contents of a rv \");",
+ " printf(\"channel always returns FALSE\\n\");",
+ " uerror(\"error to poll rendezvous channel\");",
+ " }",
+ " return 1;",
+ "}",
+ "#endif",
+ "#ifndef XUSAFE",
+ "void",
+ "setq_claim(int x, int m, char *s, int y, char *p)",
+ "{ if (x == 0)",
+ " uerror(\"x[rs] claim on uninitialized channel\");",
+ " if (x < 0 || x > MAXQ)",
+ " Uerror(\"cannot happen setq_claim\");",
+ " q_claim[x] |= m;",
+ " p_name[y] = p;",
+ " q_name[x] = s;",
+ " if (m&2) q_S_check(x, y);",
+ " if (m&1) q_R_check(x, y);",
+ "}",
+ "short q_sender[MAXQ+1];",
+ "int",
+ "q_S_check(int x, int who)",
+ "{ if (!q_sender[x])",
+ " { q_sender[x] = who+1;",
+ "#if SYNC",
+ " if (q_zero(x))",
+ " { printf(\"chan %%s (%%d), \",",
+ " q_name[x], x-1);",
+ " printf(\"sndr proc %%s (%%d)\\n\",",
+ " p_name[who], who);",
+ " uerror(\"xs chans cannot be used for rv\");",
+ " }",
+ "#endif",
+ " } else",
+ " if (q_sender[x] != who+1)",
+ " { printf(\"pan: xs assertion violated: \");",
+ " printf(\"access to chan <%%s> (%%d)\\npan: by \",",
+ " q_name[x], x-1);",
+ " if (q_sender[x] > 0 && p_name[q_sender[x]-1])",
+ " printf(\"%%s (proc %%d) and by \",",
+ " p_name[q_sender[x]-1], q_sender[x]-1);",
+ " printf(\"%%s (proc %%d)\\n\",",
+ " p_name[who], who);",
+ " uerror(\"error, partial order reduction invalid\");",
+ " }",
+ " return 1;",
+ "}",
+ "short q_recver[MAXQ+1];",
+ "int",
+ "q_R_check(int x, int who)",
+ "{ if (!q_recver[x])",
+ " { q_recver[x] = who+1;",
+ "#if SYNC",
+ " if (q_zero(x))",
+ " { printf(\"chan %%s (%%d), \",",
+ " q_name[x], x-1);",
+ " printf(\"recv proc %%s (%%d)\\n\",",
+ " p_name[who], who);",
+ " uerror(\"xr chans cannot be used for rv\");",
+ " }",
+ "#endif",
+ " } else",
+ " if (q_recver[x] != who+1)",
+ " { printf(\"pan: xr assertion violated: \");",
+ " printf(\"access to chan %%s (%%d)\\npan: \",",
+ " q_name[x], x-1);",
+ " if (q_recver[x] > 0 && p_name[q_recver[x]-1])",
+ " printf(\"by %%s (proc %%d) and \",",
+ " p_name[q_recver[x]-1], q_recver[x]-1);",
+ " printf(\"by %%s (proc %%d)\\n\",",
+ " p_name[who], who);",
+ " uerror(\"error, partial order reduction invalid\");",
+ " }",
+ " return 1;",
+ "}",
+ "#endif",
+ "int",
+ "q_len(int x)",
+ "{ if (!x--)",
+ " uerror(\"ref to uninitialized chan name (len)\");",
+ " return ((Q0 *)qptr(x))->Qlen;",
+ "}\n",
+ "int",
+ "q_full(int from)",
+ "{ if (!from--)",
+ " uerror(\"ref to uninitialized chan name (qfull)\");",
+ " switch(((Q0 *)qptr(from))->_t) {",
+ 0,
+};
+
+static char *Addq4[] = {
+ " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
+ " }",
+ " Uerror(\"bad queue - q_full\");",
+ " return 0;",
+ "}\n",
+ "#ifdef HAS_UNLESS",
+ "int",
+ "q_e_f(int from)",
+ "{ /* empty or full */",
+ " return !q_len(from) || q_full(from);",
+ "}",
+ "#endif",
+ "#if NQS>0",
+ "int",
+ "qrecv(int from, int slot, int fld, int done)",
+ "{ uchar *z;",
+ " int j, k, r=0;\n",
+ " if (!from--)",
+ " uerror(\"ref to uninitialized chan name (receiving)\");",
+ " if (from >= (int) now._nr_qs || from < 0)",
+ " Uerror(\"qrecv bad queue#\");",
+ " z = qptr(from);",
+ "#ifdef EVENT_TRACE",
+ " if (done && (in_r_scope(from+1)))",
+ " require('r', from);",
+ "#endif",
+ " switch (((Q0 *)qptr(from))->_t) {",
+ 0,
+};
+
+static char *Addq5[] = {
+ " case 0: printf(\"queue %%d was deleted\\n\", from+1);",
+ " default: Uerror(\"bad queue - qrecv\");",
+ " }",
+ " return r;",
+ "}",
+ "#endif\n",
+ "#ifndef BITSTATE",
+ "#ifdef COLLAPSE",
+ "long",
+ "col_q(int i, char *z)",
+ "{ int j=0, k;",
+ " char *x, *y;",
+ " Q0 *ptr = (Q0 *) qptr(i);",
+ " switch (ptr->_t) {",
+ 0,
+};
+
+static char *Code0[] = {
+ "void",
+ "run(void)",
+ "{ /* int i; */",
+ " memset((char *)&now, 0, sizeof(State));",
+ " vsize = (unsigned long) (sizeof(State) - VECTORSZ);",
+ "#ifndef NOVSZ",
+ " now._vsz = vsize;",
+ "#endif",
+ "/* optional provisioning statements, e.g. to */",
+ "/* set hidden variables, used as constants */",
+ "#ifdef PROV",
+ "#include PROV",
+ "#endif",
+ " settable();",
+ 0,
+};
+
+static char *R0[] = {
+ " Maxbody = max(Maxbody, ((int) sizeof(P%d)));",
+ " reached[%d] = reached%d;",
+ " accpstate[%d] = (uchar *) emalloc(nstates%d);",
+ " progstate[%d] = (uchar *) emalloc(nstates%d);",
+ " loopstate%d = loopstate[%d] = (uchar *) emalloc(nstates%d);",
+ " stopstate[%d] = (uchar *) emalloc(nstates%d);",
+ " visstate[%d] = (uchar *) emalloc(nstates%d);",
+ " mapstate[%d] = (short *) emalloc(nstates%d * sizeof(short));",
+ "#ifdef HAS_CODE",
+ " NrStates[%d] = nstates%d;",
+ "#endif",
+ " stopstate[%d][endstate%d] = 1;",
+ 0,
+};
+
+static char *R0a[] = {
+ " retrans(%d, nstates%d, start%d, src_ln%d, reached%d, loopstate%d);",
+ 0,
+};
+static char *R0b[] = {
+ " if (state_tables)",
+ " { printf(\"\\nTransition Type: \");",
+ " printf(\"A=atomic; D=d_step; L=local; G=global\\n\");",
+ " printf(\"Source-State Labels: \");",
+ " printf(\"p=progress; e=end; a=accept;\\n\");",
+ "#ifdef MERGED",
+ " printf(\"Note: statement merging was used. Only the first\\n\");",
+ " printf(\" stmnt executed in each merge sequence is shown\\n\");",
+ " printf(\" (use spin -a -o3 to disable statement merging)\\n\");",
+ "#endif",
+ " pan_exit(0);",
+ " }",
+ 0,
+};
+
+static char *Code1[] = {
+ "#ifdef NP",
+ " #define ACCEPT_LAB 1 /* at least 1 in np_ */",
+ "#else",
+ " #define ACCEPT_LAB %d /* user-defined accept labels */",
+ "#endif",
+ "#ifdef MEMCNT",
+ " #ifdef MEMLIM",
+ " #warning -DMEMLIM takes precedence over -DMEMCNT",
+ " #undef MEMCNT",
+ " #else",
+ " #if MEMCNT<20",
+ " #warning using minimal value -DMEMCNT=20 (=1MB)",
+ " #define MEMLIM (1)",
+ " #undef MEMCNT",
+ " #else",
+ " #if MEMCNT==20",
+ " #define MEMLIM (1)",
+ " #undef MEMCNT",
+ " #else",
+ " #if MEMCNT>=50",
+ " #error excessive value for MEMCNT",
+ " #else",
+ " #define MEMLIM (1<<(MEMCNT-20))",
+ " #endif",
+ " #endif",
+ " #endif",
+ " #endif",
+ "#endif",
+
+ "#if NCORE>1 && !defined(MEMLIM)",
+ " #define MEMLIM (2048) /* need a default, using 2 GB */",
+ "#endif",
+ 0,
+};
+
+static char *Code3[] = {
+ "#define PROG_LAB %d /* progress labels */",
+ 0,
+};
+
+static char *R2[] = {
+ "uchar *accpstate[%d];",
+ "uchar *progstate[%d];",
+ "uchar *loopstate[%d];",
+ "uchar *reached[%d];",
+ "uchar *stopstate[%d];",
+ "uchar *visstate[%d];",
+ "short *mapstate[%d];",
+ "#ifdef HAS_CODE",
+ "int NrStates[%d];",
+ "#endif",
+ 0,
+};
+static char *R3[] = {
+ " Maxbody = max(Maxbody, ((int) sizeof(Q%d)));",
+ 0,
+};
+static char *R4[] = {
+ " r_ck(reached%d, nstates%d, %d, src_ln%d, src_file%d);",
+ 0,
+};
+static char *R5[] = {
+ " case %d: j = sizeof(P%d); break;",
+ 0,
+};
+static char *R6[] = {
+ " }",
+ " this = o_this;",
+ " return h-BASE;",
+ "#ifndef NOBOUNDCHECK",
+ "#undef Index",
+ "#define Index(x, y) Boundcheck(x, y, II, tt, t)",
+ "#endif",
+ "}\n",
+ "#if defined(BITSTATE) && defined(COLLAPSE)",
+ "/* just to allow compilation, to generate the error */",
+ "long col_p(int i, char *z) { return 0; }",
+ "long col_q(int i, char *z) { return 0; }",
+ "#endif",
+ "#ifndef BITSTATE",
+ "#ifdef COLLAPSE",
+ "long",
+ "col_p(int i, char *z)",
+ "{ int j, k; unsigned long ordinal(char *, long, short);",
+ " char *x, *y;",
+ " P0 *ptr = (P0 *) pptr(i);",
+ " switch (ptr->_t) {",
+ " case 0: j = sizeof(P0); break;",
+ 0,
+};
+static char *R8a[] = {
+ " default: Uerror(\"bad proctype - collapse\");",
+ " }",
+ " if (z) x = z; else x = scratch;",
+ " y = (char *) ptr; k = proc_offset[i];",
+
+ " for ( ; j > 0; j--, y++)",
+ " if (!Mask[k++]) *x++ = *y;",
+
+ " for (j = 0; j < WS-1; j++)",
+ " *x++ = 0;",
+ " x -= j;",
+ " if (z) return (long) (x - z);",
+ " return ordinal(scratch, x-scratch, (short) (2+ptr->_t));",
+ "}",
+ "#endif",
+ "#endif",
+ 0,
+};
+static char *R8b[] = {
+ " default: Uerror(\"bad qtype - collapse\");",
+ " }",
+ " if (z) x = z; else x = scratch;",
+ " y = (char *) ptr; k = q_offset[i];",
+
+ " /* no need to store the empty slots at the end */",
+ " j -= (q_max[ptr->_t] - ptr->Qlen) * ((j - 2)/q_max[ptr->_t]);",
+
+ " for ( ; j > 0; j--, y++)",
+ " if (!Mask[k++]) *x++ = *y;",
+
+ " for (j = 0; j < WS-1; j++)",
+ " *x++ = 0;",
+ " x -= j;",
+ " if (z) return (long) (x - z);",
+ " return ordinal(scratch, x-scratch, 1); /* chan */",
+ "}",
+ "#endif",
+ "#endif",
+ 0,
+};
+
+static char *R12[] = {
+ "\t\tcase %d: r = ((Q%d *)z)->contents[slot].fld%d; break;",
+ 0,
+};
+char *R13[] = {
+ "int ",
+ "unsend(int into)",
+ "{ int _m=0, j; uchar *z;\n",
+ "#ifdef HAS_SORTED",
+ " int k;",
+ "#endif",
+ " if (!into--)",
+ " uerror(\"ref to uninitialized chan (unsend)\");",
+ " z = qptr(into);",
+ " j = ((Q0 *)z)->Qlen;",
+ " ((Q0 *)z)->Qlen = --j;",
+ " switch (((Q0 *)qptr(into))->_t) {",
+ 0,
+};
+char *R14[] = {
+ " default: Uerror(\"bad queue - unsend\");",
+ " }",
+ " return _m;",
+ "}\n",
+ "void",
+ "unrecv(int from, int slot, int fld, int fldvar, int strt)",
+ "{ int j; uchar *z;\n",
+ " if (!from--)",
+ " uerror(\"ref to uninitialized chan (unrecv)\");",
+ " z = qptr(from);",
+ " j = ((Q0 *)z)->Qlen;",
+ " if (strt) ((Q0 *)z)->Qlen = j+1;",
+ " switch (((Q0 *)qptr(from))->_t) {",
+ 0,
+};
+char *R15[] = {
+ " default: Uerror(\"bad queue - qrecv\");",
+ " }",
+ "}",
+ 0,
+};
+static char *Proto[] = {
+ "",
+ "/** function prototypes **/",
+ "char *emalloc(unsigned long);",
+ "char *Malloc(unsigned long);",
+ "int Boundcheck(int, int, int, int, Trans *);",
+ "int addqueue(int, int);",
+ "/* int atoi(char *); */",
+ "/* int abort(void); */",
+ "int close(int);", /* should probably remove this */
+#if 0
+ "#ifndef SC",
+ "int creat(char *, unsigned short);",
+ "int write(int, void *, unsigned);",
+ "#endif",
+#endif
+ "int delproc(int, int);",
+ "int endstate(void);",
+ "int hstore(char *, int);",
+"#ifdef MA",
+ "int gstore(char *, int, uchar);",
+"#endif",
+ "int q_cond(short, Trans *);",
+ "int q_full(int);",
+ "int q_len(int);",
+ "int q_zero(int);",
+ "int qrecv(int, int, int, int);",
+ "int unsend(int);",
+ "/* void *sbrk(int); */",
+ "void Uerror(char *);",
+ "void assert(int, char *, int, int, Trans *);",
+ "void c_chandump(int);",
+ "void c_globals(void);",
+ "void c_locals(int, int);",
+ "void checkcycles(void);",
+ "void crack(int, int, Trans *, short *);",
+ "void d_sfh(const char *, int);",
+ "void sfh(const char *, int);",
+ "void d_hash(uchar *, int);",
+ "void s_hash(uchar *, int);",
+ "void r_hash(uchar *, int);",
+ "void delq(int);",
+ "void do_reach(void);",
+ "void pan_exit(int);",
+ "void exit(int);",
+ "void hinit(void);",
+ "void imed(Trans *, int, int, int);",
+ "void new_state(void);",
+ "void p_restor(int);",
+ "void putpeg(int, int);",
+ "void putrail(void);",
+ "void q_restor(void);",
+ "void retrans(int, int, int, short *, uchar *, uchar *);",
+ "void settable(void);",
+ "void setq_claim(int, int, char *, int, char *);",
+ "void sv_restor(void);",
+ "void sv_save(void);",
+ "void tagtable(int, int, int, short *, uchar *);",
+ "void do_dfs(int, int, int, short *, uchar *, uchar *);",
+ "void uerror(char *);",
+ "void unrecv(int, int, int, int, int);",
+ "void usage(FILE *);",
+ "void wrap_stats(void);",
+ "#if defined(FULLSTACK) && defined(BITSTATE)",
+ "int onstack_now(void);",
+ "void onstack_init(void);",
+ "void onstack_put(void);",
+ "void onstack_zap(void);",
+ "#endif",
+ "#ifndef XUSAFE",
+ "int q_S_check(int, int);",
+ "int q_R_check(int, int);",
+ "uchar q_claim[MAXQ+1];",
+ "char *q_name[MAXQ+1];",
+ "char *p_name[MAXPROC+1];",
+ "#endif",
+ 0,
+};
+
+static char *SvMap[] = {
+ "void",
+ "to_compile(void)",
+ "{ char ctd[1024], carg[64];",
+ "#ifdef BITSTATE",
+ " strcpy(ctd, \"-DBITSTATE \");",
+ "#else",
+ " strcpy(ctd, \"\");",
+ "#endif",
+ "#ifdef NOVSZ",
+ " strcat(ctd, \"-DNOVSZ \");",
+ "#endif",
+ "#ifdef REVERSE",
+ " strcat(ctd, \"-DREVERSE \");",
+ "#endif",
+ "#ifdef T_REVERSE",
+ " strcat(ctd, \"-DT_REVERSE \");",
+ "#endif",
+ "#ifdef RANDOMIZE",
+ " #if RANDOMIZE>0",
+ " sprintf(carg, \"-DRANDOMIZE=%%d \", RANDOMIZE);",
+ " strcat(ctd, carg);",
+ " #else",
+ " strcat(ctd, \"-DRANDOMIZE \");",
+ " #endif",
+ "#endif",
+ "#ifdef SCHED",
+ " sprintf(carg, \"-DSCHED=%%d \", SCHED);",
+ " strcat(ctd, carg);",
+ "#endif",
+ "#ifdef BFS",
+ " strcat(ctd, \"-DBFS \");",
+ "#endif",
+ "#ifdef MEMLIM",
+ " sprintf(carg, \"-DMEMLIM=%%d \", MEMLIM);",
+ " strcat(ctd, carg);",
+ "#else",
+ "#ifdef MEMCNT",
+ " sprintf(carg, \"-DMEMCNT=%%d \", MEMCNT);",
+ " strcat(ctd, carg);",
+ "#endif",
+ "#endif",
+ "#ifdef NOCLAIM",
+ " strcat(ctd, \"-DNOCLAIM \");",
+ "#endif",
+ "#ifdef SAFETY",
+ " strcat(ctd, \"-DSAFETY \");",
+ "#else",
+ "#ifdef NOFAIR",
+ " strcat(ctd, \"-DNOFAIR \");",
+ "#else",
+ "#ifdef NFAIR",
+ " if (NFAIR != 2)",
+ " { sprintf(carg, \"-DNFAIR=%%d \", NFAIR);",
+ " strcat(ctd, carg);",
+ " }",
+ "#endif",
+ "#endif",
+ "#endif",
+ "#ifdef NOREDUCE",
+ " strcat(ctd, \"-DNOREDUCE \");",
+ "#else",
+ "#ifdef XUSAFE",
+ " strcat(ctd, \"-DXUSAFE \");",
+ "#endif",
+ "#endif",
+ "#ifdef NP",
+ " strcat(ctd, \"-DNP \");",
+ "#endif",
+ "#ifdef PEG",
+ " strcat(ctd, \"-DPEG \");",
+ "#endif",
+ "#ifdef VAR_RANGES",
+ " strcat(ctd, \"-DVAR_RANGES \");",
+ "#endif",
+ "#ifdef HC0",
+ " strcat(ctd, \"-DHC0 \");",
+ "#endif",
+ "#ifdef HC1",
+ " strcat(ctd, \"-DHC1 \");",
+ "#endif",
+ "#ifdef HC2",
+ " strcat(ctd, \"-DHC2 \");",
+ "#endif",
+ "#ifdef HC3",
+ " strcat(ctd, \"-DHC3 \");",
+ "#endif",
+ "#ifdef HC4",
+ " strcat(ctd, \"-DHC4 \");",
+ "#endif",
+ "#ifdef CHECK",
+ " strcat(ctd, \"-DCHECK \");",
+ "#endif",
+ "#ifdef CTL",
+ " strcat(ctd, \"-DCTL \");",
+ "#endif",
+ "#ifdef NIBIS",
+ " strcat(ctd, \"-DNIBIS \");",
+ "#endif",
+ "#ifdef NOBOUNDCHECK",
+ " strcat(ctd, \"-DNOBOUNDCHECK \");",
+ "#endif",
+ "#ifdef NOSTUTTER",
+ " strcat(ctd, \"-DNOSTUTTER \");",
+ "#endif",
+ "#ifdef REACH",
+ " strcat(ctd, \"-DREACH \");",
+ "#endif",
+ "#ifdef PRINTF",
+ " strcat(ctd, \"-DPRINTF \");",
+ "#endif",
+ "#ifdef OTIM",
+ " strcat(ctd, \"-DOTIM \");",
+ "#endif",
+ "#ifdef COLLAPSE",
+ " strcat(ctd, \"-DCOLLAPSE \");",
+ "#endif",
+ "#ifdef MA",
+ " sprintf(carg, \"-DMA=%%d \", MA);",
+ " strcat(ctd, carg);",
+ "#endif",
+ "#ifdef SVDUMP",
+ " strcat(ctd, \"-DSVDUMP \");",
+ "#endif",
+ "#ifdef VECTORSZ",
+ " if (VECTORSZ != 1024)",
+ " { sprintf(carg, \"-DVECTORSZ=%%d \", VECTORSZ);",
+ " strcat(ctd, carg);",
+ " }",
+ "#endif",
+ "#ifdef VERBOSE",
+ " strcat(ctd, \"-DVERBOSE \");",
+ "#endif",
+ "#ifdef CHECK",
+ " strcat(ctd, \"-DCHECK \");",
+ "#endif",
+ "#ifdef SDUMP",
+ " strcat(ctd, \"-DSDUMP \");",
+ "#endif",
+ "#if NCORE>1",
+ " sprintf(carg, \"-DNCORE=%%d \", NCORE);",
+ " strcat(ctd, carg);",
+ "#endif",
+ "#ifdef SFH",
+ " sprintf(carg, \"-DSFH \");",
+ " strcat(ctd, carg);",
+ "#endif",
+ "#ifdef VMAX",
+ " if (VMAX != 256)",
+ " { sprintf(carg, \"-DVMAX=%%d \", VMAX);",
+ " strcat(ctd, carg);",
+ " }",
+ "#endif",
+ "#ifdef PMAX",
+ " if (PMAX != 16)",
+ " { sprintf(carg, \"-DPMAX=%%d \", PMAX);",
+ " strcat(ctd, carg);",
+ " }",
+ "#endif",
+ "#ifdef QMAX",
+ " if (QMAX != 16)",
+ " { sprintf(carg, \"-DQMAX=%%d \", QMAX);",
+ " strcat(ctd, carg);",
+ " }",
+ "#endif",
+ "#ifdef SET_WQ_SIZE",
+ " sprintf(carg, \"-DSET_WQ_SIZE=%%d \", SET_WQ_SIZE);",
+ " strcat(ctd, carg);",
+ "#endif",
+ " printf(\"Compiled as: cc -o pan %%span.c\\n\", ctd);",
+ "}",
+ 0,
+};