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