1 /***** spin: pangen5.h *****/ 2 3 /* 4 * This file is part of the public release of Spin. It is subject to the 5 * terms in the LICENSE file that is included in this source directory. 6 * Tool documentation is available at http://spinroot.com 7 */ 8 9 static const char *Xpt[] = { 10 "#if defined(MA) && (defined(W_XPT) || defined(R_XPT))", 11 "static Vertex **temptree;", 12 "static char wbuf[4096];", 13 "static int WCNT = 4096, wcnt=0;", 14 "static uchar stacker[MA+1];", 15 "static ulong stackcnt = 0;", 16 "extern double nstates, nlinks, truncs, truncs2;", 17 "", 18 "static void", 19 "xwrite(int fd, char *b, int n)", 20 "{", 21 " if (wcnt+n >= 4096)", 22 " { write(fd, wbuf, wcnt);", 23 " wcnt = 0;", 24 " }", 25 " memcpy(&wbuf[wcnt], b, n);", 26 " wcnt += n;", 27 "}", 28 "", 29 "static void", 30 "wclose(int fd)", 31 "{", 32 " if (wcnt > 0)", 33 " write(fd, wbuf, wcnt);", 34 " wcnt = 0;", 35 " close(fd);", 36 "}", 37 "", 38 "static void", 39 "w_vertex(int fd, Vertex *v)", 40 "{ char t[3]; int i; Edge *e;", 41 "", 42 " xwrite(fd, (char *) &v, sizeof(Vertex *));", 43 " t[0] = 0;", 44 " for (i = 0; i < 2; i++)", 45 " if (v->dst[i])", 46 " { t[1] = v->from[i], t[2] = v->to[i];", 47 " xwrite(fd, t, 3);", 48 " xwrite(fd, (char *) &(v->dst[i]), sizeof(Vertex *));", 49 " }", 50 " for (e = v->Succ; e; e = e->Nxt)", 51 " { t[1] = e->From, t[2] = e->To;", 52 " xwrite(fd, t, 3);", 53 " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));", 54 "", 55 " if (e->s)", 56 " { t[1] = t[2] = e->S;", 57 " xwrite(fd, t, 3);", 58 " xwrite(fd, (char *) &(e->Dst), sizeof(Vertex *));", 59 " } }", 60 "}", 61 "", 62 "static void", 63 "w_layer(int fd, Vertex *v)", 64 "{ uchar c=1;", 65 "", 66 " if (!v) return;", 67 " xwrite(fd, (char *) &c, 1);", 68 " w_vertex(fd, v);", 69 " w_layer(fd, v->lnk);", 70 " w_layer(fd, v->left);", 71 " w_layer(fd, v->right);", 72 "}", 73 "", 74 "void", 75 "w_xpoint(void)", 76 "{ int fd; char nm[64];", 77 " int i, j; uchar c;", 78 " static uchar xwarned = 0;", 79 "", 80 " sprintf(nm, \"%%s.xpt\", PanSource);", 81 " if ((fd = creat(nm, 0666)) <= 0)", 82 " if (!xwarned)", 83 " { xwarned = 1;", 84 " printf(\"cannot creat checkpoint file\\n\");", 85 " return;", 86 " }", 87 " xwrite(fd, (char *) &nstates, sizeof(double));", 88 " xwrite(fd, (char *) &truncs, sizeof(double));", 89 " xwrite(fd, (char *) &truncs2, sizeof(double));", 90 " xwrite(fd, (char *) &nlinks, sizeof(double));", 91 " xwrite(fd, (char *) &dfa_depth, sizeof(int));", 92 " xwrite(fd, (char *) &R, sizeof(Vertex *));", 93 " xwrite(fd, (char *) &F, sizeof(Vertex *));", 94 " xwrite(fd, (char *) &NF, sizeof(Vertex *));", 95 "", 96 " for (j = 0; j < TWIDTH; j++)", 97 " for (i = 0; i < dfa_depth+1; i++)", 98 " { w_layer(fd, layers[i*TWIDTH+j]);", 99 " c = 2; xwrite(fd, (char *) &c, 1);", 100 " }", 101 " wclose(fd);", 102 "}", 103 "", 104 "static void", 105 "xread(int fd, char *b, int n)", 106 "{ int m = wcnt; int delta = 0;", 107 " if (m < n)", 108 " { if (m > 0) memcpy(b, &wbuf[WCNT-m], m);", 109 " delta = m;", 110 " WCNT = wcnt = read(fd, wbuf, 4096);", 111 " if (wcnt < n-m)", 112 " Uerror(\"xread failed -- insufficient data\");", 113 " n -= m;", 114 " }", 115 " memcpy(&b[delta], &wbuf[WCNT-wcnt], n);", 116 " wcnt -= n;", 117 "}", 118 "", 119 "static void", 120 "x_cleanup(Vertex *c)", 121 "{ Edge *e; /* remove the tree and edges from c */", 122 " if (!c) return;", 123 " for (e = c->Succ; e; e = e->Nxt)", 124 " x_cleanup(e->Dst);", 125 " recyc_vertex(c);", 126 "}", 127 "", 128 "static void", 129 "x_remove(void)", 130 "{ Vertex *tmp; int i, s;", 131 " int r, j;", 132 " /* double-check: */", 133 " stacker[dfa_depth-1] = 0; r = dfa_store(stacker);", 134 " stacker[dfa_depth-1] = 4; j = dfa_member(dfa_depth-1);", 135 " if (r != 1 || j != 0)", 136 " { printf(\"%%lu: \", stackcnt);", 137 " for (i = 0; i < dfa_depth; i++)", 138 " printf(\"%%d,\", stacker[i]);", 139 " printf(\" -- not a stackstate <o:%%d,4:%%d>\\n\", r, j);", 140 " return;", 141 " }", 142 " stacker[dfa_depth-1] = 1;", 143 " s = dfa_member(dfa_depth-1);", 144 "", 145 " { tmp = F; F = NF; NF = tmp; } /* complement */", 146 " if (s) dfa_store(stacker);", 147 " stacker[dfa_depth-1] = 0;", 148 " dfa_store(stacker);", 149 " stackcnt++;", 150 " { tmp = F; F = NF; NF = tmp; }", 151 "}", 152 "", 153 "static void", 154 "x_rm_stack(Vertex *t, int k)", 155 "{ int j; Edge *e;", 156 "", 157 " if (k == 0)", 158 " { x_remove();", 159 " return;", 160 " }", 161 " if (t)", 162 " for (e = t->Succ; e; e = e->Nxt)", 163 " { for (j = e->From; j <= (int) e->To; j++)", 164 " { stacker[k] = (uchar) j;", 165 " x_rm_stack(e->Dst, k-1);", 166 " }", 167 " if (e->s)", 168 " { stacker[k] = e->S;", 169 " x_rm_stack(e->Dst, k-1);", 170 " } }", 171 "}", 172 "", 173 "static Vertex *", 174 "insert_withkey(Vertex *v, int L)", 175 "{ Vertex *new, *t = temptree[L];", 176 "", 177 " if (!t) { temptree[L] = v; return v; }", 178 " t = splay(v->key, t);", 179 " if (v->key < t->key)", 180 " { new = v;", 181 " new->left = t->left;", 182 " new->right = t;", 183 " t->left = (Vertex *) 0;", 184 " } else if (v->key > t->key)", 185 " { new = v;", 186 " new->right = t->right;", 187 " new->left = t;", 188 " t->right = (Vertex *) 0;", 189 " } else", 190 " { if (t != R && t != F && t != NF)", 191 " Uerror(\"double insert, bad checkpoint data\");", 192 " else", 193 " { recyc_vertex(v);", 194 " new = t;", 195 " } }", 196 " temptree[L] = new;", 197 "", 198 " return new;", 199 "}", 200 "", 201 "static Vertex *", 202 "find_withkey(Vertex *v, int L)", 203 "{ Vertex *t = temptree[L];", 204 " if (t)", 205 " { temptree[L] = t = splay((ulong) v, t);", 206 " if (t->key == (ulong) v)", 207 " return t;", 208 " }", 209 " Uerror(\"not found error, bad checkpoint data\");", 210 " return (Vertex *) 0;", 211 "}", 212 "", 213 "void", 214 "r_layer(int fd, int n)", 215 "{ Vertex *v;", 216 " Edge *e;", 217 " char c, t[2];", 218 "", 219 " for (;;)", 220 " { xread(fd, &c, 1);", 221 " if (c == 2) break;", 222 " if (c == 1)", 223 " { v = new_vertex();", 224 " xread(fd, (char *) &(v->key), sizeof(Vertex *));", 225 " v = insert_withkey(v, n);", 226 " } else /* c == 0 */", 227 " { e = new_edge((Vertex *) 0);", 228 " xread(fd, t, 2);", 229 " e->From = t[0];", 230 " e->To = t[1];", 231 " xread(fd, (char *) &(e->Dst), sizeof(Vertex *));", 232 " insert_edge(v, e);", 233 " } }", 234 "}", 235 "", 236 "static void", 237 "v_fix(Vertex *t, int nr)", 238 "{ int i; Edge *e;", 239 "", 240 " if (!t) return;", 241 "", 242 " for (i = 0; i < 2; i++)", 243 " if (t->dst[i])", 244 " t->dst[i] = find_withkey(t->dst[i], nr);", 245 "", 246 " for (e = t->Succ; e; e = e->Nxt)", 247 " e->Dst = find_withkey(e->Dst, nr);", 248 " ", 249 " v_fix(t->left, nr);", 250 " v_fix(t->right, nr);", 251 "}", 252 "", 253 "static void", 254 "v_insert(Vertex *t, int nr)", 255 "{ Edge *e; int i;", 256 "", 257 " if (!t) return;", 258 " v_insert(t->left, nr);", 259 " v_insert(t->right, nr);", 260 "", 261 " /* remove only leafs from temptree */", 262 " t->left = t->right = t->lnk = (Vertex *) 0;", 263 " insert_it(t, nr); /* into layers */", 264 " for (i = 0; i < 2; i++)", 265 " if (t->dst[i])", 266 " t->dst[i]->num += (t->to[i] - t->from[i] + 1);", 267 " for (e = t->Succ; e; e = e->Nxt)", 268 " e->Dst->num += (e->To - e->From + 1 + e->s);", 269 "}", 270 "", 271 "static void", 272 "x_fixup(void)", 273 "{ int i;", 274 "", 275 " for (i = 0; i < dfa_depth; i++)", 276 " v_fix(temptree[i], (i+1));", 277 "", 278 " for (i = dfa_depth; i >= 0; i--)", 279 " v_insert(temptree[i], i);", 280 "}", 281 "", 282 "static Vertex *", 283 "x_tail(Vertex *t, ulong want)", 284 "{ int i, yes, no; Edge *e; Vertex *v = (Vertex *) 0;", 285 "", 286 " if (!t) return v;", 287 "", 288 " yes = no = 0;", 289 " for (i = 0; i < 2; i++)", 290 " if ((ulong) t->dst[i] == want)", 291 " { /* was t->from[i] <= 0 && t->to[i] >= 0 */", 292 " /* but from and to are uchar */", 293 " if (t->from[i] == 0)", 294 " yes = 1;", 295 " else", 296 " if (t->from[i] <= 4 && t->to[i] >= 4)", 297 " no = 1;", 298 " }", 299 "", 300 " for (e = t->Succ; e; e = e->Nxt)", 301 " if ((ulong) e->Dst == want)", 302 " { /* was INRANGE(e,0) but From and To are uchar */", 303 " if ((e->From == 0) || (e->s==1 && e->S==0))", 304 " yes = 1;", 305 " else if (INRANGE(e, 4))", 306 " no = 1;", 307 " }", 308 " if (yes && !no) return t;", 309 " v = x_tail(t->left, want); if (v) return v;", 310 " v = x_tail(t->right, want); if (v) return v;", 311 " return (Vertex *) 0;", 312 "}", 313 "", 314 "static void", 315 "x_anytail(Vertex *t, Vertex *c, int nr)", 316 "{ int i; Edge *e, *f; Vertex *v;", 317 "", 318 " if (!t) return;", 319 "", 320 " for (i = 0; i < 2; i++)", 321 " if ((ulong) t->dst[i] == c->key)", 322 " { v = new_vertex(); v->key = t->key;", 323 " f = new_edge(v);", 324 " f->From = t->from[i];", 325 " f->To = t->to[i];", 326 " f->Nxt = c->Succ;", 327 " c->Succ = f;", 328 " if (nr > 0)", 329 " x_anytail(temptree[nr-1], v, nr-1);", 330 " }", 331 "", 332 " for (e = t->Succ; e; e = e->Nxt)", 333 " if ((ulong) e->Dst == c->key)", 334 " { v = new_vertex(); v->key = t->key;", 335 " f = new_edge(v);", 336 " f->From = e->From;", 337 " f->To = e->To;", 338 " f->s = e->s;", 339 " f->S = e->S;", 340 " f->Nxt = c->Succ;", 341 " c->Succ = f;", 342 " x_anytail(temptree[nr-1], v, nr-1);", 343 " }", 344 "", 345 " x_anytail(t->left, c, nr);", 346 " x_anytail(t->right, c, nr);", 347 "}", 348 "", 349 "static Vertex *", 350 "x_cpy_rev(void)", 351 "{ Vertex *c, *v; /* find 0 and !4 predecessor of F */", 352 "", 353 " v = x_tail(temptree[dfa_depth-1], F->key);", 354 " if (!v) return (Vertex *) 0;", 355 "", 356 " c = new_vertex(); c->key = v->key;", 357 "", 358 " /* every node on dfa_depth-2 that has v->key as succ */", 359 " /* make copy and let c point to these (reversing ptrs) */", 360 "", 361 " x_anytail(temptree[dfa_depth-2], c, dfa_depth-2);", 362 " ", 363 " return c;", 364 "}", 365 "", 366 "void", 367 "r_xpoint(void)", 368 "{ int fd; char nm[64]; Vertex *d;", 369 " int i, j;", 370 "", 371 " wcnt = 0;", 372 " sprintf(nm, \"%%s.xpt\", PanSource);", 373 " if ((fd = open(nm, 0)) < 0) /* O_RDONLY */", 374 " Uerror(\"cannot open checkpoint file\");", 375 "", 376 " xread(fd, (char *) &nstates, sizeof(double));", 377 " xread(fd, (char *) &truncs, sizeof(double));", 378 " xread(fd, (char *) &truncs2, sizeof(double));", 379 " xread(fd, (char *) &nlinks, sizeof(double));", 380 " xread(fd, (char *) &dfa_depth, sizeof(int));", 381 "", 382 " if (dfa_depth != MA+a_cycles)", 383 " Uerror(\"bad dfa_depth in checkpoint file\");", 384 "", 385 " path = (Vertex **) emalloc((dfa_depth+1)*sizeof(Vertex *));", 386 " layers = (Vertex **) emalloc(TWIDTH*(dfa_depth+1)*sizeof(Vertex *));", 387 " temptree = (Vertex **) emalloc((dfa_depth+2)*sizeof(Vertex *));", 388 " lastword = (uchar *) emalloc((dfa_depth+1)*sizeof(uchar));", 389 " lastword[dfa_depth] = lastword[0] = 255; ", 390 "", 391 " path[0] = R = new_vertex();", 392 " xread(fd, (char *) &R->key, sizeof(Vertex *));", 393 " R = insert_withkey(R, 0);", 394 "", 395 " F = new_vertex();", 396 " xread(fd, (char *) &F->key, sizeof(Vertex *));", 397 " F = insert_withkey(F, dfa_depth);", 398 "", 399 " NF = new_vertex();", 400 " xread(fd, (char *) &NF->key, sizeof(Vertex *));", 401 " NF = insert_withkey(NF, dfa_depth);", 402 "", 403 " for (j = 0; j < TWIDTH; j++)", 404 " for (i = 0; i < dfa_depth+1; i++)", 405 " r_layer(fd, i);", 406 "", 407 " if (wcnt != 0) Uerror(\"bad count in checkpoint file\");", 408 "", 409 " d = x_cpy_rev();", 410 " x_fixup();", 411 " stacker[dfa_depth-1] = 0;", 412 " x_rm_stack(d, dfa_depth-2);", 413 " x_cleanup(d);", 414 " close(fd);", 415 "", 416 " printf(\"pan: removed %%lu stackstates\\n\", stackcnt);", 417 " nstates -= (double) stackcnt;", 418 "}", 419 "#endif", 420 0, 421 }; 422