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