sys/src/cmd/spin/pangen3.h

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