![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to Trace CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10no / cmd / trace|
Return to Trace CVS log | Up to [Research Unix] / researchv10no / cmd / trace |
1.1 root 1: # To unbundle, sh this file
2: echo assert.c 1>&2
3: sed 's/.//' >assert.c <<'//GO.SYSIN DD assert.c'
4: -#include "trace.h"
5: -#include "trace.d"
6: -
7: - extern struct TBL *tbl;
8: - extern int *globvars, nrvars;
9: - extern int assertbl, abase, errortbl, ebase;
10: -
11: -require(TT, stuff, by)
12: -{
13: - if (assertbl != NONE)
14: - assert(TT, stuff, by);
15: - if (errortbl != NONE)
16: - errort(TT, stuff, by);
17: -}
18: -
19: -inscope(TT, stuff, by)
20: -{ register int i;
21: -
22: - for (i = 0; i < tbl[assertbl].nrcols; i++)
23: - if (TT == tbl[assertbl].coltyp[i]
24: - && stuff == tbl[assertbl].colmap[i]
25: - && by == tbl[assertbl].colorg[i])
26: - return 1;
27: -
28: - return 0;
29: -}
30: -
31: -assert(TT, stuff, by)
32: -{ int h, i, j, x, frst;
33: -
34: - for (frst = 0; frst < tbl[assertbl].nrcols; frst++)
35: - if (tbl[assertbl].coltyp[frst] == TT
36: - && stuff == tbl[assertbl].colmap[frst]
37: - && by == tbl[assertbl].colorg[frst])
38: - break;
39: -
40: - if (frst == tbl[assertbl].nrcols)
41: - return; /* not within assertion's scope */
42: -
43: - for (i = 0; i < tbl[assertbl].nrrows; i++)
44: - {
45: - if (globvars[i+abase] != 1)
46: - continue;
47: -
48: - for (j = frst; j < tbl[assertbl].nrcols; j++)
49: - {
50: - if (TT == tbl[assertbl].coltyp[j]
51: - && stuff == tbl[assertbl].colmap[j]
52: - && by == tbl[assertbl].colorg[j])
53: - {
54: - if (tbl[assertbl].ptr[i][j].nrpils == 0)
55: - output("assertion violated: ", 1);
56: - else
57: - for (h = 0; h < tbl[assertbl].ptr[i][j].nrpils; h++)
58: - { x = tbl[assertbl].ptr[i][j].one[h].transf;
59: - globvars[x+abase] = 2;
60: - globvars[i+abase] = 0;
61: - } } }}
62: - for (i = abase; i < nrvars; i++)
63: - if (globvars[i] == 2)
64: - globvars[i] = 1;
65: -}
66: -
67: -assertholds()
68: -{ int i;
69: - if (assertbl == NONE)
70: - return 1;
71: -
72: - for (i = abase; i < nrvars; i++)
73: - if (globvars[i] && tbl[assertbl].endrow[i-abase])
74: - return 1;
75: - return 0;
76: -}
77: -
78: -errort(TT, stuff, by)
79: -{ int h, i, j, x, frst;
80: -
81: - for (frst = 0; frst < tbl[errortbl].nrcols; frst++)
82: - if (tbl[errortbl].coltyp[frst] == TT
83: - && stuff == tbl[errortbl].colmap[frst]
84: - && by == tbl[errortbl].colorg[frst])
85: - break;
86: -
87: - if (frst == tbl[errortbl].nrcols)
88: - return; /* not within assertion's scope */
89: -
90: - for (i = 0; i < tbl[errortbl].nrrows; i++)
91: - {
92: - if (globvars[i+ebase] != 1)
93: - continue;
94: -
95: - for (j = frst; j < tbl[errortbl].nrcols; j++)
96: - {
97: - if (TT == tbl[errortbl].coltyp[j]
98: - && stuff == tbl[errortbl].colmap[j]
99: - && by == tbl[errortbl].colorg[j])
100: - {
101: - if (tbl[errortbl].ptr[i][j].nrpils == 0)
102: - globvars[i+ebase] = 0;
103: - else
104: - for (h = 0; h < tbl[errortbl].ptr[i][j].nrpils; h++)
105: - { x = tbl[errortbl].ptr[i][j].one[h].transf;
106: - globvars[x+ebase] = 2;
107: - globvars[i+ebase] = 0;
108: - }
109: - }
110: - }
111: - }
112: - for (i = ebase; i < nrvars; i++)
113: - if (globvars[i] == 2)
114: - { globvars[i] = 1;
115: - if (tbl[errortbl].endrow[i-ebase])
116: - output("error matched: ", 2);
117: - }
118: - globvars[ebase] = 1;
119: -}
120: -
121: -peekassert(ice)
122: - struct FREEZE *ice;
123: -{ register int i;
124: - if (assertbl != NONE)
125: - for (i = abase; i < nrvars; i++)
126: - globvars[i] = ice->varsaved[i];
127: - else if (errortbl != NONE)
128: - for (i = ebase; i < nrvars; i++)
129: - globvars[i] = ice->varsaved[i];
130: -}
131: //GO.SYSIN DD assert.c
132: echo cmalloc.c 1>&2
133: sed 's/.//' >cmalloc.c <<'//GO.SYSIN DD cmalloc.c'
134: -#ifdef debug
135: -#define ASSERT(p) if(!(p))botch("p");else
136: -botch(s)
137: -char *s;
138: -{
139: - printf("assertion botched: %s\n",s);
140: - abort();
141: -}
142: -#else
143: -#define ASSERT(p)
144: -#endif
145: -
146: -/* C storage allocator
147: - * circular first-fit strategy
148: - * works with noncontiguous, but monotonically linked, arena
149: - * each block is preceded by a ptr to the (pointer of)
150: - * the next following block
151: - * blocks are exact number of words long
152: - * aligned to the data type requirements of ALIGN
153: - * pointers to blocks must have BUSY bit 0
154: - * bit in ptr is 1 for busy, 0 for idle
155: - * gaps in arena are merely noted as busy blocks
156: - * last block of arena is empty and
157: - * has a pointer to first
158: - * idle blocks are coalesced during space search
159: - *
160: - * a different implementation may need to redefine
161: - * ALIGN, NALIGN, BLOCK, BUSY, INT
162: - * where INT is integer type to which a pointer can be cast
163: -*/
164: -#define INT int
165: -#define ALIGN int
166: -#define NALIGN 1
167: -#define WORD sizeof(union store)
168: -#define BLOCK 1024
169: -#define BUSY 1
170: -#define NULL 0
171: -#define testbusy(p) ((INT)(p)&BUSY)
172: -#define setbusy(p) (union store *)((INT)(p)|BUSY)
173: -#define clearbusy(p) (union store *)((INT)(p)&~BUSY)
174: -
175: -union store {
176: - union store *ptr;
177: - ALIGN dummy[NALIGN];
178: - int calloc; /*calloc clears an array of integers*/
179: -};
180: -
181: -static union store alloca; /* initial arena */
182: -static union store *allocb = &alloca; /*arena base*/
183: -static union store *allocp = &alloca; /*search ptr*/
184: -static union store *alloct = &alloca; /*arena top; for speedier ialloc*/
185: -static union store allocx, allocy; /*for benefit of realloc*/
186: -extern char *sbrk();
187: -
188: -/* a cache list of frequently-used sizes is maintained. From each
189: - * cache entry hangs a chain of available blocks (marked busy
190: - * to keep out of the first fit search)
191: -*/
192: -#define CACHEMAX 100 /* largest block to be cached (in words) */
193: -#ifndef pdp11
194: -#define CACHESIZ 13 /* number of entries (prime) */
195: -#else
196: -#define CACHESIZ 0
197: -#endif
198: -static struct cache {
199: - int size;
200: - union store *chain;
201: -} cache[CACHESIZ];
202: -
203: -char *
204: -malloc(nbytes)
205: -unsigned nbytes;
206: -{
207: - register union store *p, *q;
208: - register nw;
209: - register temp;
210: - register struct cache *cp;
211: -
212: - ASSERT(allock(allocp)&1);
213: - nw = (nbytes+WORD+WORD-1)/WORD;
214: - if(CACHESIZ && nw<CACHEMAX && nw>2) { /* see note + below */
215: - cp = cache + nw%CACHESIZ;
216: - p = cp->chain;
217: - if(p && nw==cp->size) {
218: - cp->chain = p[1].ptr;
219: - ASSERT(testbusy(p->ptr));
220: - ASSERT(clearbusy(p->ptr)-p==nw);
221: - return (char*)(p+1);
222: - }
223: - }
224: - ASSERT(allock(allocp)&3);
225: - for(; ; ) { /* done at most twice */
226: - p = allocp;
227: - if(alloca.ptr!=0) /*C can't initialize union*/
228: - for(temp=0; ; ) {
229: - if(!testbusy(p->ptr)) {
230: - while(!testbusy((q=p->ptr)->ptr)) {
231: - ASSERT(q>p);
232: - p->ptr = q->ptr;
233: - }
234: - allocp = p;
235: - if(q>=p+nw && p+nw>=p) /*room; no wrap*/
236: - goto found;
237: - }
238: - q = p;
239: - p = clearbusy(p->ptr);
240: - if(p <= q) {
241: - ASSERT(p==allocb);
242: - if(++temp>1)
243: - break;
244: - }
245: - }
246: - temp = nw;
247: - p = (union store *)sbrk(0);
248: - q = allocp->ptr;
249: - if(!testbusy(q) && q+1 == p)
250: - temp -= p - allocp;
251: - temp = ((temp+BLOCK/WORD)/(BLOCK/WORD))*(BLOCK/WORD);
252: - if(p+temp <= p)
253: - return(NULL);
254: - for( ; ; ) {
255: - register s;
256: - q = (union store *)sbrk(temp*WORD);
257: - if((INT)q != -1)
258: - break;
259: - for(cp=cache; cp<cache+CACHESIZ; cp++) {
260: - for(p=cp->chain; p; p=p[1].ptr) {
261: - ASSERT(testbusy(p->ptr));
262: - p->ptr = clearbusy(p->ptr);
263: - ASSERT(p->ptr-p==cp->size);
264: - }
265: - cp->chain = 0;
266: - }
267: - s = (temp-nw)/2;
268: - if(s <= 0)
269: - return(NULL);
270: - temp -= s;
271: - }
272: - ialloc((char *)q, (unsigned)temp*WORD);
273: - }
274: -found:
275: - q = p + nw;
276: - if(p->ptr > q) {
277: - allocx = *q;
278: - q->ptr = p->ptr;
279: - }
280: - p->ptr = setbusy(q);
281: - ASSERT(allock(allocp)&7);
282: - return((char *)(p+1));
283: -}
284: -/* + note CACHESIZ is tested for conditional compilation; nw>2 assumes there's
285: - * no point in caching smaller sizes (they are rarely used and always
286: - * can be allocated) and protects against the old storage compaction trick:
287: - * free(p); free(dummy);dummy=malloc(1);realloc(p)
288: - * (otherwise free(dummy) would destroy allocy, which pertains to p)
289: -*/
290: -
291: -/* freeing strategy tuned for LIFO allocation
292: -*/
293: -free(ap)
294: -char *ap;
295: -{
296: - register union store *p = (union store *)ap, *q;
297: - register nw;
298: - register struct cache *cp;
299: -
300: - --p;
301: - ASSERT(allock(p));
302: - ASSERT(testbusy(p->ptr));
303: - nw = clearbusy(p->ptr) - p;
304: - ASSERT(nw>0);
305: - if(CACHESIZ && nw<CACHEMAX && nw>2) {
306: - cp = cache + nw%CACHESIZ;
307: - if(nw != cp->size) {
308: - q = cp->chain;
309: - if(q) {
310: - ASSERT(testbusy(q->ptr));
311: - q->ptr = clearbusy(q->ptr);
312: - ASSERT(q->ptr-q==cp->size);
313: - cp->chain = q[1].ptr;
314: - }
315: - if(!q)
316: - cp->size = nw;
317: - else
318: - goto nocache;
319: - }
320: - allocy = p[1];
321: - p[1].ptr = cp->chain;
322: - cp->chain = p;
323: - ASSERT(allock(allocp)&017);
324: - return;
325: - }
326: -nocache:
327: - allocp = p;
328: - p->ptr = clearbusy(p->ptr);
329: - ASSERT(allock(allocp)&037);
330: - ASSERT(p->ptr<=alloct);
331: -}
332: -
333: -/* ialloc(q, nbytes) inserts a block that did not come
334: - * from malloc into the arena
335: - *
336: - * q points to new block
337: - * r points to last of new block
338: - * p points to last cell of arena before new block
339: - * s points to first cell of arena after new block
340: -*/
341: -ialloc(qq, nbytes)
342: -char *qq;
343: -unsigned nbytes;
344: -{
345: - register union store *p, *q, *s;
346: - union store *r;
347: -
348: - q = (union store *)qq;
349: - r = q + (nbytes/WORD) - 1;
350: - q->ptr = r;
351: - if(alloca.ptr==0) /*C can't initialize union*/
352: - alloca.ptr = &alloca;
353: - if(q > alloct) {
354: - p = alloct;
355: - alloct = r;
356: - } else
357: - allocp = p = allocb;
358: - for( ; ; p=s) {
359: - s = clearbusy(p->ptr);
360: - if(s==allocb)
361: - break;
362: - ASSERT(s>p);
363: - if(s>r) {
364: - if(p<q)
365: - break;
366: - else
367: - ASSERT(p>r);
368: - }
369: - }
370: - p->ptr = q==p+1? q: setbusy(q);
371: - r->ptr = s==r+1? s: setbusy(s);
372: - if(allocb > q)
373: - allocp = allocb = q;
374: -}
375: -
376: -/* realloc(p, nbytes) reallocates a block obtained from malloc()
377: - * and freed since last call of malloc()
378: - * to have new size nbytes, and old content
379: - * returns new location, or 0 on failure
380: -*/
381: -
382: -char *
383: -realloc(pp, nbytes)
384: -char *pp;
385: -unsigned nbytes;
386: -{
387: - register union store *q;
388: - register union store *p = (union store *)pp;
389: - register union store *s, *t;
390: - register unsigned nw;
391: - struct cache *cp;
392: - unsigned onw;
393: -
394: - q = p-1;
395: - ASSERT(allock(q));
396: - if(testbusy(q->ptr)) {
397: - allocp = q;
398: - q->ptr = clearbusy(q->ptr);
399: - if(CACHESIZ) {
400: - nw = q->ptr - q;
401: - cp = cache + nw%CACHESIZ;
402: - if(cp->chain==q) {
403: - ASSERT(cp->size==nw);
404: - cp->chain = p->ptr; /*p->ptr==q[1].ptr*/
405: - *p = allocy;
406: - } else
407: - ASSERT(notonchain(q,cp->chain));
408: - }
409: - }
410: - onw = q->ptr - p;
411: - q = (union store *)malloc(nbytes);
412: - if(q==NULL || q==p)
413: - return((char *)q);
414: - ASSERT(q<p||q>p[-1].ptr);
415: - s = p;
416: - t = q;
417: - nw = (nbytes+WORD-1)/WORD;
418: - if(nw<onw)
419: - onw = nw;
420: - while(onw--!=0)
421: - *t++ = *s++;
422: - ASSERT(clearbusy(q[-1].ptr)-q==nw);
423: - if(q<p && q+nw>=p)
424: - q[q+nw-p] = allocx;
425: - ASSERT(allock(q-1));
426: - return((char *)q);
427: -}
428: -
429: -#ifdef debug
430: -
431: -notonchain(p,q)
432: -union store *p, *q;
433: -{
434: - for(;q; q=clearbusy(q->ptr))
435: - if(q==p)
436: - return 0;
437: - return 1;
438: -}
439: -
440: -allock(q)
441: -union store *q;
442: -{
443: -#ifdef longdebug
444: - register union store *p, *r;
445: - int x;
446: - for(x=0; x<CACHESIZ; x++) {
447: - p = cache[x].chain;
448: - if(p==0)
449: - continue;
450: - for( ; p; p=p[1].ptr) {
451: - ASSERT(testbusy(p->ptr));
452: - ASSERT(clearbusy(p->ptr)-p==cache[x].size);
453: - }
454: - }
455: - x = 0;
456: - p = allocb;
457: - if(alloca.ptr==0)
458: - return(1);
459: - for( ; (r=clearbusy(p->ptr)) > p; p=r) {
460: - if(p==q)
461: - x++;
462: - }
463: - return(r==allocb&(x==1|p==q));
464: -#else
465: - return(q>=allocb);
466: -#endif
467: -}
468: -#endif
469: //GO.SYSIN DD cmalloc.c
470: echo makefile 1>&2
471: sed 's/.//' >makefile <<'//GO.SYSIN DD makefile'
472: -CFLAGS = -g
473: -OBJS = malloc_t.o cmalloc.o trace.expr.o trace1.o trace2.o trace3.o trace4.o trace5.o trace6.o trace7.o trace8.o trace9.o assert.o
474: -
475: -# FILES:
476: -# trace.h constants and macro definitions
477: -# trace.d data structures
478: -# trace1.c reads in the tables, sets up data structures
479: -# trace2.c memory allocation
480: -# trace3.c the symbolic execution procedures
481: -# trace4.c state space handler
482: -# trace5.c lookup table for system states
483: -# trace6.c lookup table for queue states
484: -# trace7.c lookup table for leaf-states
485: -# trace8.c lookup table for variable & parameter states
486: -# trace9.c lookup table for process states
487: -# trace.expr.c evaluation of expressions
488: -# malloc_t.c memory allocation interface to cmalloc.c
489: -# assert.c assertion primitives
490: -
491: -trace: $(OBJS)
492: - cc $(CFLAGS) $(OBJS) -o trace
493: -
494: -%.o: %.c trace.d trace.h
495: - cc $(CFLAGS) -c $%.c
496: -
497: -clean:
498: - rm -f *.o pret.* mon.out core a.out
499: -
500: -install:
501: - cp trace /usr/bin
502: -
503: //GO.SYSIN DD makefile
504: echo malloc_t.c 1>&2
505: sed 's/.//' >malloc_t.c <<'//GO.SYSIN DD malloc_t.c'
506: -#include <stdio.h>
507: -#include "trace.h"
508: -
509: -#define DEBUG 0
510: -
511: -#if DEBUG
512: -#define log(e, u, d) event[e][u] += (long) d;
513: -#else
514: -#define log(e, u, d)
515: -#endif
516: -
517: -#define A_LARGE 64
518: -#define A_USER 0x55000000
519: -
520: -#define POOL 0
521: -#define ALLOC 1
522: -#define FREE 2
523: -#define NREVENT 3
524: -
525: - union M {
526: - long size;
527: - union M *link;
528: - };
529: -
530: - union M *freelist[A_LARGE];
531: - long req[A_LARGE];
532: - long event[NREVENT][A_LARGE];
533: -
534: -char *
535: -talloc(u)
536: - long u;
537: -{ union M *m;
538: - register r;
539: - char *Smalloc();
540: -
541: - u = ((u-1)/sizeof(union M) + 2);
542: -
543: - if( u >= A_LARGE )
544: - { log(ALLOC, 0, (long) 1);
545: - m = (union M *) malloc( u * sizeof(union M) );
546: - if (m == NULL)
547: - whoops("malloc fault");
548: - } else
549: - { if( freelist[u] == NULL )
550: - { r = req[u] += req[u] ? req[u] : 1;
551: - if (r > NOTOOBIG)
552: - r = req[u] = NOTOOBIG+1;
553: - log(POOL, (int) u, (long) r);
554: - freelist[u] = (union M *) Smalloc( r*u*sizeof(union M) );
555: - if (freelist[u] == NULL)
556: - whoops("malloc fault");
557: -
558: - (freelist[u] + u*(r-1))->link = 0;
559: - for (m = freelist[u] + u*(r-2); m >= freelist[u]; m -= u)
560: - m->link = m+u;
561: - }
562: - log(ALLOC, (int) u, (long) 1);
563: -
564: - m = freelist[u];
565: - freelist[u] = m->link;
566: - }
567: - m->size = u | A_USER;
568: -/*
569: - for (r = 1; r < u; )
570: - (&m->size)[r++] = 0;
571: -*/
572: - return (char *) (m+1);
573: -}
574: -
575: -tfree(v)
576: - char *v;
577: -{ register union M *m = (union M *) v;
578: - register long u;
579: -
580: - --m;
581: - if ( (m->size&0xFF000000) != A_USER)
582: - { fprintf(stderr, "panic: releasing a free block\n");
583: - kill(getpid(), 3);
584: - }
585: -
586: - u = (m->size &= 0xFFFFFF);
587: - if ( u >= A_LARGE )
588: - { log(FREE, (int) 0, (long) 1);
589: - free(m);
590: - }
591: - else
592: - { log(FREE, (int) u, (long) 1);
593: - m->link = freelist[u];
594: - freelist[u] = m;
595: - }
596: -}
597: -
598: -#if DEBUG
599: -double
600: -a_stats()
601: -{ register int i;
602: - long p, a, f, j;
603: - long sum = 0;
604: -
605: - fprintf(stderr, "chunk\t pool\tallocs\t frees\t spill\n");
606: - for (i = 0; i < A_LARGE; i++)
607: - {
608: - p = event[POOL][i];
609: - a = event[ALLOC][i];
610: - f = event[FREE][i];
611: -
612: - if( !(p|a|f) )
613: - continue;
614: -
615: - j = (long) (i * sizeof(union M));
616: - fprintf(stderr, "%5d\t%6ld\t%6ld\t%6ld\t%6ld\n", j, p, a, f, a-f);
617: -
618: - sum += p*j;
619: - }
620: - fprintf(stderr, "total pools %7u\n", sum);
621: -
622: - return (double) sum;
623: -}
624: -#endif
625: //GO.SYSIN DD malloc_t.c
626: echo trace.d 1>&2
627: sed 's/.//' >trace.d <<'//GO.SYSIN DD trace.d'
628: - struct ELM {
629: - short transf; /* next state function */
630: - short valtrans; /* value transferred */
631: - };
632: -
633: - struct IND {
634: - short nrpils;
635: - struct ELM *one;
636: - };
637: -
638: - struct VARPARS {
639: - short nrms, *ms; /* message parameters */
640: - short nrvs, *vs; /* pvar parameters */
641: - short nrlvars, *lvarvals; /* local variables */
642: - };
643: -
644: - struct TBLPARS {
645: - short nrms;
646: - short nrvs; /* max available space for params */
647: - short nrlvars; /* max available space for locvars */
648: - };
649: -
650: - struct LOCVARS {
651: - short nrlvars, *lvarvals;
652: - };
653: -
654: - struct CPARS {
655: - short callwhat;
656: - short nrms, *ms; /* message parameters */
657: - short nrvs, *vs; /* pvar parameters */
658: - };
659: -
660: - struct LBT {
661: - int *mapcol, *orgcol; /* mapped versions of colmap and colorg */
662: - };
663: -
664: -/*
665: - * endrow: proper endstates of the process table
666: - * deadrow: set if deadend (eg return state)
667: - * badrow: row with at least one output option
668: - * labrow: labeled row (potential start of a loop)
669: - */
670: -
671: - struct TBL {
672: - int nrrows, nrcols;
673: - int *endrow, *deadrow, *badrow, *labrow;
674: - int *colmap, *colorg, *coltyp;
675: - char **rowname;
676: -
677: - struct IND **ptr;
678: - struct CPARS *calls;
679: - };
680: -
681: - struct MBOX {
682: - char limit; /* length of queue */
683: - char owner; /* the process reading from this queue */
684: - char qname[PLENTY]; /* user-level name for the queue */
685: - };
686: -
687: - struct MNAME {
688: - char mname[PLENTY];
689: - };
690: -
691: - struct BLTIN {
692: - short target;
693: - short type;
694: - short value;
695: - };
696: -
697: - struct REVPOL {
698: - char toktyp;
699: - short tokval;
700: - };
701: -
702: - struct PROCSTACK {
703: - short uptable; /* table where we come from */
704: - short uptransf; /* pending transition in that table */
705: -
706: - struct VARPARS *varparsaved; /* saves parameters and locals */
707: - struct PROCSTACK *follow; /* next stackframe */
708: - };
709: -
710: -#define USED 32768
711: -#define PASSED 16384
712: -#define TRAIL 1
713: -
714: - struct QUEUE {
715: - short mesg; /* on rcv PASSED is OR'ed in */
716: - unsigned short cargo; /* when set USED is OR'ed in */
717: -#if TRAIL
718: - short tstate[2]; /* linecode reference */
719: -#endif TRAIL
720: - struct QUEUE *next;
721: - struct QUEUE *last;
722: - struct QUEUE *s_forw;
723: - struct QUEUE *s_back;
724: - };
725: -
726: - struct CONTS {
727: - short mesg;
728: - unsigned short cargo;
729: - };
730: -
731: - struct TEMPLATE {
732: - short *g_vars; /* current globals */
733: - struct LOCVARS **l_vars; /* current local vars */
734: - struct PROCSTACK **traceback; /* traceback of complete stack */
735: - };
736: -
737: - struct STATE {
738: - unsigned short *pstate; /* old states & maps */
739: - struct TEMPLATE *pcon; /* variables and stacks */
740: - struct VISIT *next;
741: - };
742: -
743: -#define ANALYZED 16384
744: -
745: - struct VISIT {
746: - unsigned int howmany; /* which queues are nonempty */
747: - struct CONTS **c; /* queue contents */
748: - union {
749: - struct QUEUE *s; /* when searching, last message sent */
750: - short countme; /* when analyzed, counts nr of returns */
751: - } prop;
752: - unsigned short depth; /* level of first visit, ANALYZED is OR'ed in */
753: - struct VISIT *next;
754: - };
755: -
756: -#define ISANA(x) (x->depth & ANALYZED)
757: -#define DEPTH(x) (x->depth & ~ANALYZED)
758: -
759: -/*
760: - * normal ppushes (via forward()) save the parameters in the procstack
761: - * so that the corresponding ppop (via backup()) can reset them properly
762: - *
763: - * series of ppushes and ppops, performed in a single freeze() call
764: - * (via the retable() and dotable() subroutines) are different:
765: - *
766: - * additional ppushes are no problem, since they save the
767: - * proper state information via the normal route
768: - *
769: - * additional ppops however would lose the procstacked info
770: - * that info is stored in the CUBE structure so that when
771: - * a ppop from freeze() is undone in unfreeze()
772: - * the proper state information can be restored onto the procstack
773: - */
774: -
775: - struct CUBE {
776: - short poporpush;
777: - short which;
778: - short procsaved;
779: - short transfsaved;
780: -
781: - struct VARPARS *varparsaved; /* parameter map and local var map */
782: -
783: - struct CUBE *pntr;
784: - struct CUBE *rtnp;
785: - };
786: -
787: - struct FREEZE {
788: - short lastsav;
789: - short *statsaved; /* save states of tables */
790: - short *varsaved; /* save global variables */
791: - short whichvar; /* set if a var changed */
792: - short oldvalue; /* of that loc var */
793: -
794: - struct CUBE *cube; /* place to save stackframe */
795: - };
796: -
797: - struct Swiffle {
798: - struct STATE *st;
799: - struct VISIT *vi;
800: - struct Swiffle *next;
801: - struct Swiffle *last;
802: - };
803: //GO.SYSIN DD trace.d
804: echo trace.expr.c 1>&2
805: sed 's/.//' >trace.expr.c <<'//GO.SYSIN DD trace.expr.c'
806: -#include <stdio.h>
807: -#include <math.h>
808: -#include "trace.h"
809: -#include "trace.d"
810: -
811: -#define DEBUG 0
812: -
813: -#define setv 1
814: -#define addeq 2
815: -#define subeq 3
816: -#define muleq 4
817: -#define diveq 5
818: -#define modeq 6
819: -#define plus 7
820: -#define minus 8
821: -#define times 9
822: -#define div 10
823: -#define mod 11
824: -#define power 12
825: -#define uminus 13
826: -#define gt 14
827: -#define lt 15
828: -#define ge 16
829: -#define le 17
830: -#define eq 18
831: -#define ne 19
832: -#define land 20
833: -#define lor 21
834: -#define lnot 22
835: -#define princ 23
836: -#define prdec 24
837: -#define poinc 25
838: -#define podec 26
839: -
840: -#define OP 0
841: -#define NM 1
842: -
843: -#define unary(c) (c == uminus || c == lnot || c >= princ)
844: -#define binary(c) !unary(c)
845: -
846: - extern struct REVPOL **expr;
847: - extern int nexpr, nrvars, *globvars;
848: - extern struct VARPARS *procpars;
849: -
850: - struct REVPOL *rev;
851: - int curproc, revp;
852: -
853: - struct {
854: - char how;
855: - short whichvar;
856: - short oldvalue;
857: - } storewhere;
858: -
859: -evalexpr(n, pr, b)
860: - struct FREEZE *b;
861: -{ int i;
862: - if (n == NONE)
863: - return 0;
864: - if (n < 0 || n >= nexpr)
865: - whoops("unknown expression");
866: -
867: - rev = expr[n];
868: - revp = 0;
869: - curproc = pr;
870: - storewhere.how = 0;
871: -
872: - if ((i = getval()) < 0)
873: - i += 3*MANY;
874: - else
875: - i -= 3*MANY; /* should return stripped constant */
876: -#if DEBUG
877: - fprintf(stderr, "evaluated expr %d, process %d, result %d\n", n, pr, i);
878: -#endif
879: -
880: - b->whichvar = storewhere.whichvar;
881: - b->oldvalue = storewhere.oldvalue;
882: -
883: - return storewhere.how;
884: -}
885: -
886: -evalcond(n, pr)
887: -{ int i;
888: - if (n < 0 || n >= nexpr)
889: - { fprintf(stderr, "%d\n", n);
890: - whoops("unknown expression - evalcond");
891: - }
892: -
893: - rev = expr[n];
894: - revp = 0;
895: - curproc = pr;
896: - storewhere.how = 0;
897: -
898: - if ((i = getval()) < 0)
899: - i += 3*MANY;
900: - else
901: - i -= 3*MANY; /* should return stripped constant */
902: -#if DEBUG
903: - fprintf(stderr, "evaluated cond %d, process %d, result %d\n", n, pr, i);
904: -#endif
905: - if (storewhere.how != 0)
906: - whoops("illegal assignment in expression");
907: -
908: - return i;
909: -}
910: -
911: -unoper(c, n)
912: -{ int i = convert(n, curproc);
913: - switch (c)
914: - { case uminus: return (-i);
915: - case lnot : return (!i);
916: - case princ : remem(n); setvar(n, i+1); return i;
917: - case prdec : remem(n); setvar(n, i-1); return i;
918: - case poinc : remem(n); return setvar(n, i+1);
919: - case podec : remem(n); return setvar(n, i-1);
920: - default : whoops("unknown unary operator");
921: - }
922: -}
923: -
924: -bioper(c, n, m)
925: -{ int i, j;
926: - double a, b;
927: -
928: - if (c != setv)
929: - i = convert(n, curproc);
930: - j = convert(m, curproc);
931: - switch (c)
932: - { case setv: remem(n); return setvar(n, j);
933: - case addeq: remem(n); return setvar(n, i+j);
934: - case subeq: remem(n); return setvar(n, i-j);
935: - case muleq: remem(n); return setvar(n, i*j);
936: - case diveq: remem(n); return setvar(n, i/j);
937: - case modeq: remem(n); return setvar(n, i%j);
938: - case plus: return (i+j);
939: - case minus: return (i-j);
940: - case times: return (i*j);
941: - case div: return (i/j);
942: - case mod: return (i%j);
943: - case gt : return (i>j);
944: - case lt : return (i<j);
945: - case ge : return (i>=j);
946: - case le : return (i<=j);
947: - case eq : return (i==j);
948: - case ne : return (i!=j);
949: - case land: return (i&&j);
950: - case lor: return (i||j);
951: - default: whoops("unkown binary operator");
952: - }
953: -}
954: -
955: -getval()
956: -{ int tok = revp++;
957: - int res;
958: -
959: - if (rev[tok].toktyp == NM)
960: - res = rev[tok].tokval;
961: - else
962: - { if (unary(rev[tok].tokval))
963: - res = unoper(rev[tok].tokval, getval());
964: - else
965: - res = bioper(rev[tok].tokval, getval(), getval());
966: -
967: - if (res < 0)
968: - res -= 3*MANY;
969: - else
970: - res += 3*MANY;
971: - }
972: -
973: - return res;
974: -}
975: -
976: -setvar(which, v)
977: -{ int u = wapper(which, curproc);
978: - int towhat = v;
979: -
980: - if (u >= 2*MANY || u < 0)
981: - whoops("lhs of assignment not a variable");
982: -
983: - if (u < MANY)
984: - { if (u >= nrvars)
985: - { fprintf(stderr, "setvar %d %d %d\n", which, v, u);
986: - whoops("illegal assignment");
987: - }
988: -
989: - globvars[u] = (short) towhat;
990: - }
991: - else
992: - { u -= MANY;
993: - if (u >= (int) procpars[curproc].nrlvars)
994: - whoops("unknown local variable");
995: - procpars[curproc].lvarvals[u] = (short) towhat;
996: - }
997: -
998: - return towhat;
999: -}
1000: -
1001: -remem(u)
1002: -{ if (storewhere.how != 0)
1003: - whoops("multiple assignment in expression");
1004: -
1005: - if (u < MANY)
1006: - {
1007: -#if DEBUG
1008: - fprintf(stderr, "setting global %d\n", u);
1009: -#endif
1010: - storewhere.whichvar = (short) u;
1011: - storewhere.oldvalue = globvars[u];
1012: - storewhere.how = GV;
1013: - }
1014: - else
1015: - { storewhere.whichvar = (short) u;
1016: -
1017: - u -= MANY;
1018: -#if DEBUG
1019: - fprintf(stderr, "setting local %d\n", u);
1020: -#endif
1021: - storewhere.oldvalue = procpars[curproc].lvarvals[u];
1022: - storewhere.how = LV;
1023: - }
1024: -}
1025: //GO.SYSIN DD trace.expr.c
1026: echo trace.h 1>&2
1027: sed 's/.//' >trace.h <<'//GO.SYSIN DD trace.h'
1028: -#define NONE -1
1029: -#define MAXPROC 16
1030: -#define PLENTY 16 /* max namelength */
1031: -
1032: -#define MANY 512 /* range globals: 0 - MANY */
1033: - /* range locals : MANY - 2*MANY */
1034: - /* range params : 2*MANY and 3*MANY */
1035: - /* range constants: 3*MANY++ or 3*MANY-- */
1036: -
1037: - /* `column types:' */
1038: -#define INP 10 /* recv specific message */
1039: -#define DFL 11 /* default input from q */
1040: -#define TMO 12 /* transition on timeout */
1041: -#define OUTP 13 /* append message to a q */
1042: -#define SPN 14 /* builtin call or transit state */
1043: -#define CND 15 /* conditional */
1044: -#define FCT 16 /* function call */
1045: -
1046: -#define INCR 16 /* increment a sequence number */
1047: -#define DECR 17 /* decrement a sequence number */
1048: -#define SUBT 18 /* subtract */
1049: -#define ADDT 19 /* add */
1050: -#define SETV 32 /* set seq. number to initial value */
1051: -#define ISEQ 256 /* compare two variables (s.numbers) */
1052: -#define NTEQ 257 /* != */
1053: -#define GREQ 258 /* >= */
1054: -#define SMEQ 259 /* <= */
1055: -#define GRNQ 260 /* > */
1056: -#define SMNQ 261 /* < */
1057: -
1058: -#define POP 1
1059: -#define PUSH -1
1060: -
1061: -#define SO 2 /* send only */
1062: -#define RO 4 /* recv only */
1063: -#define SR 6 /* send & recv */
1064: -#define TC 8 /* reftask call */
1065: -#define TO 16 /* timeout */
1066: -#define LV 32 /* local var updated */
1067: -#define GV 64 /* global var updated */
1068: -
1069: -#define FAIL -1 /* backward receive: cargo mismatch */
1070: -
1071: -#define NOREF(i) (i < 0 || i >= MAXPROC)
1072: -#define NOTOOBIG 16383 /* was 32767 */
1073: //GO.SYSIN DD trace.h
1074: echo trace1.c 1>&2
1075: sed 's/.//' >trace1.c <<'//GO.SYSIN DD trace1.c'
1076: -#include <stdio.h>
1077: -#include <signal.h>
1078: -#include "trace.h"
1079: -#include "trace.d"
1080: -
1081: -#if 0
1082: -#define debug(s1, s2, s3, s4, s5) printf(s1, s2, s3, s4, s5)
1083: -#else
1084: -#define debug(s1, s2, s3, s4, s5)
1085: -#endif
1086: -
1087: - struct TBL *tbl;
1088: - struct LBT *lbt;
1089: - struct MBOX *mbox;
1090: - struct MNAME *fullname;
1091: -
1092: - struct REVPOL **expr;
1093: - struct PROCSTACK **procstack;
1094: -
1095: - struct VARPARS *procpars;
1096: - struct TBLPARS *tblpars;
1097: - struct LOCVARS *tblvars;
1098: - struct TBLPARS *tablpars;
1099: -
1100: - struct QUEUE **starter, **head, **tail;
1101: - struct QUEUE *s_first, *s_last;
1102: -
1103: -/*
1104: - * reftasks : mapping of logic reftask id to table number
1105: - * processes: mapping of logic process id to table number
1106: - * basics : initial process table
1107: - */
1108: -
1109: - int *state, *reftasks, *processes, *basics;
1110: - int *qsize, *globvars, *inits, *xob;
1111: -
1112: - /*
1113: - * the state-set of an assertion table is mapped
1114: - * onto the global variables (to simplify state checking)
1115: - * the first global that is an element from the state set
1116: - * is given by integer `abase'
1117: - */
1118: -
1119: - int abase = -1; /* base of assertion table state set */
1120: - int ebase = -1; /* base of error table state set */
1121: - int assertbl = -1; /* table used for assertion checking */
1122: - int errortbl = -1; /* table used for assertion checking */
1123: - int msgbase = -1, maxlevel = -1, maxreached = -1;
1124: -
1125: - int maxcol=0, nrtbl=0, nrqs=0, nrprocs=0, nrrefs=0;
1126: - int nrinit=0, nrvars=0, nexpr=0, nrmesgs=0, linecode=0;
1127: - int QMAX=2;
1128: -
1129: - char qoverride = 0;
1130: - char noshortcut = 0; /* disable timeout heuristics */
1131: - char prbyq = 2; /* controls output format */
1132: - char blast = 0; /* blast search mode */
1133: - char qandirty = 0; /* scatter search mode */
1134: - char lockplus = 0; /* report both buffer locks and loops */
1135: - char firstlock = 0; /* stop at first buffer lock found */
1136: - char maxxed = 0; /* bound on search depth */
1137: - char prefix = 0; /* print all prefixes too */
1138: - char timedd = 0; /* verbose mode */
1139: - char completed = 0; /* not interrupted */
1140: - char muststore = 0; /* must perform loop check and store state */
1141: - char sensible = 0; /* default mode: try a sensible partial search */
1142: -
1143: - double zapper = (double) 30000;
1144: - double tryswiff=0, noswiff=0, cannot=0;
1145: -
1146: - long zapped = 0, locksf = 0, loopsf = 0;
1147: - long normf = 0, callno = 0;
1148: -
1149: - int *effnrstates; /* effective nr of table states per process */
1150: - int aperiod = 120;
1151: -
1152: - char *topofmem, *sbrk(), *Smalloc();
1153: - char fname[64];
1154: -
1155: - FILE *mb;
1156: -
1157: - extern double iseen, ireseen, painful, kurshan;
1158: -
1159: -onalarm()
1160: -{ float t;
1161: - struct { long u, p, cu, cp; } tim;
1162: -
1163: - times(&tim);
1164: - t = (float) (tim.u + tim.p)/ (float) 60.0;
1165: -
1166: - if (++callno%10 == 1)
1167: - { fprintf(stderr, " seconds depth states zapped");
1168: - fprintf(stderr, " prefix terms loops locks memory\n");
1169: - }
1170: - fprintf(stderr, "%8.2f %6d ", t, maxreached);
1171: - fprintf(stderr, "%6g %8ld %7g ", iseen+ireseen, zapped, kurshan);
1172: - fprintf(stderr, "%5ld %5ld ", normf, loopsf);
1173: - fprintf(stderr, "%5ld %8u\n", locksf, sbrk(0) - topofmem);
1174: - signal(SIGALRM, onalarm);
1175: - alarm(aperiod);
1176: -}
1177: -
1178: -postlude()
1179: -{ struct { long u, p, cu, cp; } tim;
1180: - extern double COUNT;
1181: - float u, s;
1182: -
1183: - fflush(stdout);
1184: - if (!completed)
1185: - fprintf(stderr, "trace: interrupted\n");
1186: -
1187: - if (timedd)
1188: - { times(&tim);
1189: - u = (float) tim.u / (float) 60.0;
1190: - s = (float) tim.p / (float) 60.0;
1191: -
1192: - fprintf(stderr, "\ttime: %.2fs u + ", u);
1193: - fprintf(stderr, "%.2fs sys = %.2fs\n\n", s, u+s);
1194: - fprintf(stderr, "\t%g states cached, ", iseen+ireseen);
1195: - fprintf(stderr, "%ld states zapped\n", zapped);
1196: - fprintf(stderr, "\tsearch depth reached: %d; ", maxreached);
1197: - fprintf(stderr, "memory used: %u\n\t", sbrk(0) - topofmem );
1198: - fprintf(stderr, "%ld deadlocks, ", locksf);
1199: - fprintf(stderr, "%ld loops, ", loopsf);
1200: - fprintf(stderr, "%ld terminating executions, and ", normf);
1201: - fprintf(stderr, "%g prefixes\n", kurshan);
1202: - fprintf(stderr, "\t%g edges traversed", COUNT);
1203: - fprintf(stderr, ", %g states analyzed twice\n", painful);
1204: - if (cannot > 0)
1205: - fprintf(stderr, "\t%g cache replacements failed\n", cannot);
1206: - if (tryswiff > 0)
1207: - fprintf(stderr, "\ttryswiff %5g noswiff %g\n",tryswiff,noswiff);
1208: - }
1209: - exit(completed == 0);
1210: -}
1211: -
1212: -wisdom()
1213: -{
1214: - if (sensible)
1215: - { timedd = firstlock = qandirty = 1;
1216: - fprintf(stderr, "default search: ");
1217: - fprintf(stderr, "-vxjqm %d %d\n", QMAX, maxlevel);
1218: - } else
1219: - { fprintf(stderr, "%s search, ", (blast) ? "blast" :
1220: - (qandirty) ? "scatter" : "exhaustive");
1221: - fprintf(stderr, "depth bound %d\n", maxlevel);
1222: - }
1223: -}
1224: -
1225: -main(argc, argv)
1226: - char **argv;
1227: -{
1228: - char c;
1229: - int i=1, j, base=2;
1230: -
1231: - strcpy(fname, "pret.out");
1232: - if (argc > 1 && argv[1][0] == '-')
1233: - { base++;
1234: - while ((c = argv[1][i++]) != '\0')
1235: - switch (c) {
1236: - case 'a': prefix = 1; break;
1237: - case 'b': blast = qandirty = 1; break;
1238: - case 'c': if (argc >= base)
1239: - { sscanf(argv[base-1], "%d", &j);
1240: - base++;
1241: - } else
1242: - usage("missing argument for `c' flag");
1243: - firstlock = lockplus = timedd = 1;
1244: - switch (j) {
1245: - case 0: blast = qandirty = 1; break;
1246: - case 1: maxxed = 3; /* fall through */
1247: - case 2: qandirty = 1; break;
1248: - case 3: maxxed = 2; break; /* 1{ x effnr */
1249: - case 4: maxxed = 3; /* 2 x effnr */
1250: - case 5: break; /* 8 x effnr */
1251: - default: usage("unknown validation class");
1252: - }
1253: - break;
1254: - case 'f': prbyq = 1; break;
1255: - case 'F': prbyq = 0; break;
1256: - case 'j': firstlock = 1; break;
1257: - case 'k': if (argc >= base)
1258: - { sscanf(argv[base-1], "%d", &j);
1259: - zapper = (double) (j * 1000);
1260: - base++;
1261: - } else
1262: - usage("missing argument for `k' flag");
1263: - break;
1264: - case 'l': lockplus = 1; break;
1265: - case 'm': maxxed = 1;
1266: - if (argc >= base)
1267: - { sscanf(argv[base-1], "%d", &maxlevel);
1268: - base++;
1269: - } else
1270: - usage("missing argument for `m' flag");
1271: - break;
1272: - case 'n': noshortcut = 1; break;
1273: - case 'q': qoverride = 1;
1274: - if (argc >= base)
1275: - { sscanf(argv[base-1], "%d", &QMAX);
1276: - base++;
1277: - } else
1278: - usage("missing argument for `q' flag");
1279: - break;
1280: - case 'r': if (argc >= base)
1281: - { sscanf(argv[base-1], "%d", &j);
1282: - base++;
1283: - } else
1284: - usage("missing argument for `r' flag");
1285: - signal(SIGALRM, postlude);
1286: - aperiod = 0;
1287: - alarm(j*60);
1288: - break;
1289: - case 'R': if (argc >= base)
1290: - { sscanf(argv[base-1], "%d", &j);
1291: - base++;
1292: - } else
1293: - usage("missing argument for `R' flag");
1294: - aperiod = j*60;
1295: - break;
1296: - case 's': setup(); showtables(timedd); exit(0);
1297: - break;
1298: - case 'v': timedd = 1; break;
1299: - case 'x': qandirty = 1; break;
1300: - default : usage("unknown option");
1301: - }
1302: - } else
1303: - { sensible = qoverride = 1;
1304: - }
1305: -
1306: - if (argc >= base-1)
1307: - sscanf(argv[base-1], "%s", fname);
1308: - else
1309: - strcpy(fname, "pret.out");
1310: -
1311: - setup();
1312: - init();
1313: - topofmem = sbrk(0);
1314: -
1315: - if (maxxed != 1)
1316: - {
1317: - for (j = maxlevel = 0; j < nrprocs; j++)
1318: - maxlevel += effnrstates[processes[j]];
1319: -
1320: - switch (maxxed) {
1321: - case 3: maxlevel *= 2; break;
1322: - case 2: maxlevel = (3*maxlevel)/2; break;
1323: - case 0: if (sensible)
1324: - maxlevel *= 2;
1325: - else
1326: - maxlevel *= 8; /* avoid pathetic cases */
1327: - break;
1328: - default: whoops("cannot happen - main");
1329: - }
1330: - maxxed = 1;
1331: - }
1332: - if (aperiod > 0)
1333: - { signal(SIGALRM, onalarm);
1334: - alarm(aperiod);
1335: - } signal(SIGINT, postlude);
1336: -
1337: - wisdom();
1338: - muststore = 1; /* must always store initial state */
1339: - FSE(0);
1340: - completed = 1;
1341: - postlude();
1342: -}
1343: -
1344: -setup()
1345: -{
1346: - if ((mb = fopen(fname, "r")) == NULL)
1347: - { fprintf(stderr, "cannot find `%s'\n", fname);
1348: - exit(1);
1349: - }
1350: -
1351: - getglobals();
1352: - gettables();
1353: - getexprs();
1354: -
1355: - fclose(mb);
1356: -}
1357: -
1358: -getglobals()
1359: -{ register int i, j;
1360: - int a, b, c, x, y, z;
1361: -
1362: - if (fscanf(mb, "%d linecode\n", &linecode) != 1)
1363: - badinput("linecode");
1364: - a = fscanf(mb, "%d procedures (assert %d/%d)\n", &x, &assertbl, &errortbl);
1365: - if (a != 3)
1366: - badinput("procedures");
1367: - if (fscanf(mb, "%d processes\n", &y) != 1)
1368: - badinput("processes");
1369: - if (fscanf(mb, "%d queues:\n", &z) != 1)
1370: - badinput("queues");
1371: -
1372: - debug("%d procs, %d functions, %d queues, assert %d\n", y, x, z, assertbl);
1373: -
1374: - nrtbl = x + y;
1375: - nrqs = z;
1376: - alloc1(x, y, z);
1377: -
1378: - getmesnames();
1379: -
1380: - for (i = 0; i < z; i++)
1381: - { if (fscanf(mb, "%s\t%d/%d/%d: ", mbox[i].qname, &b, &a, &c) != 4)
1382: - badinput("queue sorts");
1383: - alloc2(i, a, b);
1384: - for (j = 0; j < c; j++)
1385: - { fscanf(mb, "%d,", &b);
1386: - xob[b] = i;
1387: - }
1388: - }
1389: -
1390: - if (fscanf(mb, "%d inits:\n", &nrinit) != 1)
1391: - badinput("queue inits");
1392: -
1393: - alloc3(nrinit);
1394: - for (i = 0; i < nrinit; i++)
1395: - fscanf(mb, "%d,", &(inits[i]));
1396: -
1397: - if (fscanf(mb, "%d g-variables: ", &nrvars) != 1)
1398: - badinput("g-variables");
1399: -
1400: - alloc4(nrvars);
1401: -
1402: - for (i = 0; i < nrvars; i++)
1403: - if (fscanf(mb, "%d,", &a) != 1)
1404: - badinput("g-var-inits");
1405: - else
1406: - { if ((b = determine(a)) == 1 || b == 2)
1407: - badinput("g-var bad init");
1408: - else
1409: - globvars[i] = (short) a;
1410: - }
1411: -}
1412: -
1413: -getmesnames()
1414: -{ register int i;
1415: - if (fscanf(mb, "%d messages, base %d:\n", &nrmesgs, &msgbase) != 2)
1416: - badinput("messages");
1417: -
1418: - alloc45(nrmesgs);
1419: -
1420: - for (i = 0; i < nrmesgs; i++)
1421: - if (fscanf(mb, "%s ", fullname[i].mname) != 1)
1422: - badinput("mesg");
1423: -}
1424: -
1425: -gettables()
1426: -{ register int i, j;
1427: - int a, b, c, d;
1428: - char name[32];
1429: -
1430: - processes[0] = -1;
1431: - if (nrtbl >= 64)
1432: - badinput("too many process tables...");
1433: - for (i = 0; i < nrtbl; i++)
1434: - { if ((j = fscanf(mb, "%s %d:%d/%d:", name, &a, &b, &c)) != 4)
1435: - { printf("matched %d: %s %d\n", j, name, a);
1436: - badinput("table header");
1437: - }
1438: -
1439: - debug("table %d: %s (%d) ", i, name, a, 0);
1440: - debug("r/c: %d/%d\n", b, c, 0, 0);
1441: -
1442: - if (b >= 1024)
1443: - badinput("too many states");
1444: - if ((tbl[i].nrrows = b) == 0)
1445: - badinput("empty table");
1446: - tbl[i].nrcols = c;
1447: -
1448: - if (strcmp(name, "REF") == 0)
1449: - { reftasks[a] = i;
1450: - nrrefs++;
1451: - } else
1452: - { processes[a] = basics[a] = i;
1453: - nrprocs++;
1454: - effnrstates[i] = b;
1455: - }
1456: -
1457: - if (b > 0)
1458: - { alloc5(i);
1459: - for (j = 0; j < c; j++)
1460: - { if (fscanf(mb, "%d(%d),", &b, &d) != 2)
1461: - badinput("column header");
1462: -
1463: - debug("%d(%d),\n", b, d, 0, 0);
1464: -
1465: - tbl[i].coltyp[j] = d;
1466: - tbl[i].colmap[j] = b;
1467: - if (d != FCT && d != SPN && d != CND)
1468: - tbl[i].colorg[j] = whichq(b);
1469: - else
1470: - tbl[i].colorg[j] = -1;
1471: - }
1472: - getrows(i);
1473: - getspecials(i);
1474: - getcalls(i);
1475: - getparams(a, i);
1476: - getlocvars(a, i);
1477: -} } }
1478: -
1479: -getrows(nn)
1480: -{ int a, b, c;
1481: - int n = nn;
1482: - char tmp[128];
1483: -
1484: - for (;;)
1485: - { if (fscanf(mb, "%d/%d (%d) ", &a, &b, &c) != 3)
1486: - badinput("row");
1487: -
1488: - if (a == 0 && b == 0 && c == 0)
1489: - break;
1490: -
1491: - debug("row %d, col %d, size %d:\n", a, b, c, 0);
1492: -
1493: - if (c == 0)
1494: - continue;
1495: -
1496: - tbl[n].deadrow[a] = 0;
1497: - getentries(n, a, b, c);
1498: - }
1499: - if (!linecode) return;
1500: -
1501: - if (fscanf(mb, "%s\n", tmp) != 1 || strcmp(tmp, "rownames:") != 0)
1502: - badinput("rownames");
1503: - for (a = 0; a < tbl[n].nrrows; a++)
1504: - { for (b = 0; (tbl[n].rowname[a][b] = getc(mb)) != '\n'; b++) ;
1505: - tbl[n].rowname[a][b] = '\0';
1506: - }
1507: -}
1508: -
1509: -getentries(nn, m, p, q)
1510: -{ register int i;
1511: - int x, y, n = nn;
1512: -
1513: - tbl[n].ptr[m][p].nrpils = (short) q;
1514: -
1515: - alloc6(n, m, p, q);
1516: -
1517: - for (i = 0; i < q; i++)
1518: - { if (fscanf(mb, "[%d,%d] ", &x, &y) != 2)
1519: - badinput("table entry");
1520: - tbl[n].ptr[m][p].one[i].transf = (short) x;
1521: - tbl[n].ptr[m][p].one[i].valtrans = (short) y;
1522: -
1523: - debug("\t[%d,%d] \n", x, y, 0, 0);
1524: - }
1525: -}
1526: -
1527: -getspecials(in)
1528: -{ register int i;
1529: - int n, m;
1530: - char stri[64];
1531: - if (fscanf(mb, "ENDSTATES %d: ", &n) != 1)
1532: - badinput("endstates");
1533: -
1534: - for (i = 0; i < n; i++)
1535: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows)
1536: - badinput("endstate");
1537: - tbl[in].endrow[m] = 1;
1538: - }
1539: - if ((m = fscanf(mb, "%s %d: ", stri, &n)) != 2 ||
1540: - strcmp(stri, "BADSTATES") != 0)
1541: - { printf("read %s %d\n", stri, n);
1542: - badinput("badstates");
1543: - }
1544: -
1545: - for (i = 0; i < n; i++)
1546: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows)
1547: - badinput("badstate");
1548: - tbl[in].badrow[m] = 1;
1549: - }
1550: -
1551: - if ((m = fscanf(mb, "%s %d: ", stri, &n)) != 2 ||
1552: - strcmp(stri, "LABSTATES") != 0)
1553: - { printf("read %s %d\n", stri, n);
1554: - badinput("labstates");
1555: - }
1556: -
1557: - for (i = 0; i < n; i++)
1558: - { if (fscanf(mb, "%d,", &m) != 1 || m < 0 || m >= tbl[in].nrrows)
1559: - badinput("labstate");
1560: - tbl[in].labrow[m] = 1;
1561: - }
1562: - debug("specials:\n", 0, 0, 0, 0);
1563: - for (i = 0; i < tbl[in].nrrows; i++)
1564: - { n = tbl[in].endrow[i];
1565: - m = tbl[in].badrow[i];
1566: - debug("\t%d: %d/%d/%d\n", i, n, m, tbl[in].labrow[i]);
1567: - }
1568: -}
1569: -
1570: -getparams(pr, tb)
1571: -{ int n, m;
1572: - char stri[64];
1573: - if (fscanf(mb, "%s %d/%d", stri, &n, &m) != 3)
1574: - { printf("read %s %d/%d\n", stri, n, m);
1575: - badinput("parameters");
1576: - }
1577: -
1578: - tblpars[tb].nrms = (short) n; /* required sizes */
1579: - tblpars[tb].nrvs = (short) m;
1580: -
1581: - if (processes[pr] == tb)
1582: - alloc8(pr, 2*n, 2*m); /* avalaible sizes */
1583: -}
1584: -
1585: -getlocvars(p, tb)
1586: -{ register int i;
1587: - int n, m;
1588: - if (fscanf(mb, "%d l-variables: ", &n) != 1)
1589: - badinput("l-variables");
1590: -
1591: - if (processes[p] != tb)
1592: - { tblvars[tb].nrlvars = (short) n; /* required size */
1593: - if (n > 0)
1594: - tblvars[tb].lvarvals = (short *)
1595: - Smalloc(n * sizeof(short));
1596: - for (i = 0; i < n; i++)
1597: - if (fscanf(mb, "%d,", &m) != 1)
1598: - badinput("l-vars");
1599: - else
1600: - tblvars[tb].lvarvals[i] = (short) m;
1601: - } else
1602: - { tablpars[p].nrlvars = (short) (2*n); /* available size */
1603: - procpars[p].nrlvars = (short) n; /* actually used */
1604: - if (n > 0)
1605: - procpars[p].lvarvals = (short *)
1606: - Emalloc((2*n) * sizeof(short));
1607: - for (i = 0; i < n; i++)
1608: - if (fscanf(mb, "%d,", &m) != 1)
1609: - badinput("lvar-inits");
1610: - else
1611: - procpars[p].lvarvals[i] = (short) m;
1612: - }
1613: -}
1614: -
1615: -getcalls(in)
1616: -{ register int i, j;
1617: - int k, n, m, a, b, N;
1618: - char stri[64];
1619: - if (fscanf(mb, "%s %d", stri, &n) != 2) /* FCTS */
1620: - { printf("read %s %d\n", stri, n);
1621: - badinput("function calls");
1622: - }
1623: - alloc9(in, n);
1624: - for (i = 0, N = n; i < N; i++)
1625: - { if (fscanf(mb, "%d-%d/%d: ", &n, &m, &k) != 3)
1626: - badinput("fct call");
1627: -
1628: - alloc10(in, i, n, m, k);
1629: -
1630: - effnrstates[in] += tbl[reftasks[n]].nrrows;
1631: -
1632: - for (j = m+k, a = b = 0; j > 0; j--)
1633: - { if (fscanf(mb, "%d/%d", &n, &m) != 2)
1634: - badinput("fct call entry");
1635: - if (n == 0)
1636: - tbl[in].calls[i].ms[a++] = (short) m;
1637: - else
1638: - tbl[in].calls[i].vs[b++] = (short) m;
1639: - } }
1640: -}
1641: -
1642: -getexprs()
1643: -{ int i, j, a, b, c;
1644: - char name[32];
1645: -
1646: - if (fscanf(mb, "%s %d\n", name, &nexpr) != 2)
1647: - badinput("nexpr");
1648: - if (strcmp(name, "EXPR") != 0)
1649: - badinput("expressions");
1650: -
1651: - expr = (struct REVPOL **)
1652: - Smalloc(nexpr * sizeof(struct REVPOL *));
1653: -
1654: - for (i = 0; i < nexpr; i++)
1655: - { fscanf(mb, "%d: ", &a);
1656: -
1657: - expr[i] = (struct REVPOL *)
1658: - Smalloc(a * sizeof(struct REVPOL));
1659: -
1660: - for (j = 0; j < a; j++)
1661: - { fscanf(mb, "%d/%d: %d\n", &b, &c);
1662: - expr[i][j].toktyp = b;
1663: - expr[i][j].tokval = c;
1664: - } }
1665: -}
1666: -
1667: -showtables(how)
1668: -{ register int i, j;
1669: - int k, n, m, p;
1670: - char table[2*MAXPROC][64];
1671: -
1672: - for (i = 0; i < nrprocs; i++)
1673: - { j = processes[i];
1674: - sprintf(table[j], "process %d", i);
1675: - }
1676: - for (i = 0; i < nrrefs; i++)
1677: - { j = reftasks[i];
1678: - sprintf(table[j], "reftask %d", i);
1679: - }
1680: -
1681: - for (i = 0; i < nrtbl; i++)
1682: - {
1683: - printf("\n%s (table %d):\n", table[i], i);
1684: - if (how && linecode)
1685: - { for (j = 2+strlen(tbl[i].rowname[0]); j > 0; j--)
1686: - putchar(' ');
1687: - } else printf(" ");
1688: - putchar('\t');
1689: - for (k = 0; k < tbl[i].nrcols; k++)
1690: - { switch(tbl[i].coltyp[k]) {
1691: - case INP: printf("I:"); break;
1692: - case DFL: printf("D:"); break;
1693: - case TMO: printf("T:"); break;
1694: - case OUTP: printf("O:"); break;
1695: - case SPN: printf("S:"); break;
1696: - case CND: printf("C:"); break;
1697: - case FCT: printf("F:"); break;
1698: - }
1699: - if (tbl[i].colorg[k] != -1)
1700: - printf("%d/%d\t", tbl[i].colmap[k], tbl[i].colorg[k]);
1701: - else
1702: - printf("%d \t", tbl[i].colmap[k]);
1703: - }
1704: -
1705: - for (j = 0; j < tbl[i].nrrows; j++)
1706: - { if (!how || !linecode)
1707: - printf("\n%2d\t", j);
1708: - else
1709: - printf("\n%2d/%s\t", j, tbl[i].rowname[j]);
1710: - for (k = 0; k < tbl[i].nrcols; k++)
1711: - { if (how)
1712: - {
1713: - for (p = 0; p < tbl[i].ptr[j][k].nrpils; p++)
1714: - { n = (int) tbl[i].ptr[j][k].one[p].transf;
1715: - printf("%d,", n);
1716: - }
1717: - } else
1718: - {
1719: - if (tbl[i].ptr[j][k].nrpils > 0)
1720: - { n = (int) tbl[i].ptr[j][k].one[0].transf;
1721: - m = (int) tbl[i].ptr[j][k].one[0].valtrans;
1722: - printf("%d(%d)", n, m);
1723: - }
1724: - if (tbl[i].ptr[j][k].nrpils > 1)
1725: - putchar('+');
1726: - }
1727: - putchar('\t');
1728: - }
1729: - } }
1730: - putchar('\n');
1731: -}
1732: -
1733: -whichq(n)
1734: -{ int i;
1735: - if (n < 0 || n >= MANY)
1736: - return -1;
1737: -
1738: - if ((i = xob[n]) == -1)
1739: - badinput("mbox sort incomplete");
1740: -
1741: - return i;
1742: -}
1743: -
1744: -init()
1745: -{ register int i, m;
1746: - state = (int *)
1747: - Smalloc(nrprocs * sizeof(int));
1748: - qsize = (int *)
1749: - Smalloc(nrqs * sizeof(int));
1750: - head = (struct QUEUE **)
1751: - Smalloc(nrqs * sizeof(struct QUEUE *));
1752: - tail = (struct QUEUE **)
1753: - Smalloc(nrqs * sizeof(struct QUEUE *));
1754: - starter = (struct QUEUE **)
1755: - Smalloc(nrqs * sizeof(struct QUEUE *));
1756: -
1757: -
1758: - for (i = 0; i < nrqs; i++)
1759: - { starter[i] = (struct QUEUE *)
1760: - Smalloc(sizeof(struct QUEUE));
1761: - starter[i]->next = NULL;
1762: - qsize[i] = 0;
1763: - head[i] = tail[i] = starter[i];
1764: - }
1765: -
1766: - decode();
1767: - initable(); /* do not change the order of inits */
1768: - iniqtable();
1769: - inihash();
1770: -
1771: - for (i = 0; i < nrprocs; i++)
1772: - { state[i] = 0;
1773: - procstack[i] = NULL;
1774: -
1775: - lbt[i].mapcol = (int *)
1776: - Smalloc(maxcol * sizeof(int));
1777: - lbt[i].orgcol = (int *)
1778: - Smalloc(maxcol * sizeof(int));
1779: - fiddler(i);
1780: - }
1781: -
1782: - s_last = NULL;
1783: -
1784: - for (i = 0; i < nrinit; i++)
1785: - { m = inits[i];
1786: - if (send(m, whichq(m), NONE, NONE, 0) == 0)
1787: - badinput("qsize too small for initial string...");
1788: - }
1789: - if (assertbl != NONE)
1790: - { assertbl = reftasks[assertbl];
1791: -
1792: - abase = nrvars;
1793: - nrvars += tbl[assertbl].nrrows;
1794: -
1795: - if (abase > 0)
1796: - globvars = (int *)
1797: - Realloc(globvars, nrvars * sizeof(int));
1798: - else
1799: - globvars = (int *)
1800: - Smalloc(nrvars * sizeof(int));
1801: -
1802: - globvars[abase] = 1;
1803: - for (i = abase+1; i < nrvars; i++)
1804: - globvars[i] = 0;
1805: - }
1806: - if (errortbl != NONE)
1807: - { errortbl = reftasks[errortbl];
1808: -
1809: - ebase = nrvars;
1810: - nrvars += tbl[errortbl].nrrows;
1811: -
1812: - if (ebase > 0)
1813: - globvars = (int *)
1814: - Realloc(globvars, nrvars * sizeof(int));
1815: - else
1816: - globvars = (int *)
1817: - Smalloc(nrvars * sizeof(int));
1818: -
1819: - globvars[ebase] = 1;
1820: - for (i = ebase+1; i < nrvars; i++)
1821: - globvars[i] = 0;
1822: - }
1823: -}
1824: -
1825: -decode()
1826: -{ register int i, j, m;
1827: -
1828: - for (i = 0; i < nrvars; i++)
1829: - { m = convert(globvars[i], NONE);
1830: - globvars[i] = (short) m;
1831: - }
1832: - for (i = 0; i < nrprocs; i++)
1833: - for (j = 0; j < procpars[i].nrlvars; j++)
1834: - { m = convert(procpars[i].lvarvals[j], i);
1835: - procpars[i].lvarvals[j] = (short) m;
1836: - }
1837: -}
1838: //GO.SYSIN DD trace1.c
1839: echo trace2.c 1>&2
1840: sed 's/.//' >trace2.c <<'//GO.SYSIN DD trace2.c'
1841: -#include <stdio.h>
1842: -#include <errno.h>
1843: -#include "trace.h"
1844: -#include "trace.d"
1845: -
1846: - extern struct TBL *tbl;
1847: - extern struct LBT *lbt;
1848: - extern struct MBOX *mbox;
1849: - extern struct MNAME *fullname;
1850: - extern struct REVPOL **expr;
1851: - extern struct PROCSTACK **procstack;
1852: -
1853: - extern struct VARPARS *procpars;
1854: - extern struct TBLPARS *tblpars;
1855: -
1856: - extern struct LOCVARS *tblvars;
1857: - extern struct TBLPARS *tablpars;
1858: -
1859: - extern int *reftasks, *processes, *basics;
1860: - extern int *globvars, *inits, *xob, *effnrstates;
1861: -
1862: - extern char qoverride;
1863: - extern int QMAX, msgbase, maxcol, assertbl, errortbl;
1864: -
1865: -#define tell(s) fprintf(stderr, s)
1866: -
1867: -usage(str)
1868: - char *str;
1869: -{ fprintf(stderr, "trace: %s\n", str);
1870: - tell("usage: trace [-?] [N]\n");
1871: - tell("\t-a show all prefixes leading into old states\n");
1872: - tell("\t-b `blast mode' (quick, very partial search)\n");
1873: - tell("\t-c N perform class N validation (N: 0..5) \n");
1874: - tell("\t-f or -F alternative formats for printing queue histories\n");
1875: - tell("\t-j stop at the first buffer lock found\n");
1876: - tell("\t-k N restrict the state space cache to N thousand states\n");
1877: - tell("\t-l show normal execution sequences and loops, but no prefixes\n");
1878: - tell("\t-m N restrict search depth to N steps\n");
1879: - tell("\t-n don't use timeout heuristics\n");
1880: - tell("\t-q N set bound N on maximum queue size used\n");
1881: - tell("\t-r N restrict the runtime to N minutes\n");
1882: - tell("\t-R N report on progress every N minutes\n");
1883: - tell("\t-s show the transition tables (different if combined with `v')\n");
1884: - tell("\t-v verbose - print execution times, etc.\n");
1885: - tell("\t-x perform a scatter search\n");
1886: - tell("\tno flag: try a sensible partial search\n");
1887: - exit(1);
1888: -}
1889: -
1890: -/*
1891: - * calls on Emalloc and Realloc go straight to the library malloc
1892: - * it is used for data that may be realloced but is never released
1893: - * - Smalloc claims memory that is never realloced and never released
1894: - * - emalloc and efree handle memory that is never realloced but often released
1895: - * - talloc and tfree are direct calls on the tac-package (used via emalloc)
1896: - */
1897: -
1898: -char *
1899: -Stake(n)
1900: -{ char *try, *sbrk(), *Emalloc();
1901: - extern int errno;
1902: -
1903: - do {
1904: - try = sbrk(n);
1905: - } while ((int) try == -1 && errno == EINTR);
1906: -
1907: - if ((int) try == -1)
1908: - return Emalloc(n); /* maybe some mem left here */
1909: -
1910: - return try;
1911: -}
1912: -
1913: -#define CHUNK 4096
1914: -
1915: -char *have;
1916: -long left = 0;
1917: -
1918: -char *
1919: -Smalloc(n)
1920: - unsigned n;
1921: -{ char *try;
1922: -
1923: - if (n == 0)
1924: - return (char *) NULL;
1925: - if (left < n)
1926: - { unsigned grow = (n < CHUNK) ? CHUNK : n;
1927: - have = Stake(grow);
1928: - left = grow;
1929: - }
1930: - try = have;
1931: - have += n;
1932: - left -= n;
1933: -
1934: - return try;
1935: -}
1936: -
1937: -char *
1938: -Emalloc(n)
1939: - unsigned n;
1940: -{ char *try, *malloc();
1941: -
1942: - if (n == 0)
1943: - return (char *) NULL;
1944: - if ((try = malloc(n)) == NULL)
1945: - whoops("malloc fault");
1946: -
1947: - return try;
1948: -}
1949: -
1950: -char *
1951: -Realloc(a, b)
1952: - char *a; unsigned b;
1953: -{ char *try, *realloc();
1954: -
1955: - if (b == 0)
1956: - return (char *) NULL;
1957: - if ((try = realloc(a, b)) == NULL)
1958: - whoops("realloc returns 0");
1959: -
1960: - return try;
1961: -}
1962: -
1963: -char *
1964: -emalloc(n)
1965: - unsigned n;
1966: -{ char *try;
1967: - char *talloc();
1968: -
1969: - if (n == 0)
1970: - return (char *) NULL;
1971: - if ((try = talloc(n)) == NULL)
1972: - whoops("talloc fault");
1973: -
1974: - return try;
1975: -}
1976: -
1977: -efree(at)
1978: - char *at;
1979: -{
1980: - if (at) tfree(at);
1981: -}
1982: -
1983: -alloc1(x, y, z)
1984: -{ int n = x+y;
1985: - tbl = (struct TBL *)
1986: - Smalloc(n * sizeof(struct TBL));
1987: - tblpars = (struct TBLPARS *)
1988: - Smalloc(n * sizeof(struct TBLPARS));
1989: - tblvars = (struct LOCVARS *)
1990: - Smalloc(n * sizeof(struct LOCVARS));
1991: - reftasks = (int *)
1992: - Smalloc(x * sizeof(int));
1993: - processes = (int *)
1994: - Smalloc(y * sizeof(int));
1995: - lbt = (struct LBT *)
1996: - Smalloc(y * sizeof(struct LBT));
1997: - procpars = (struct VARPARS *)
1998: - Smalloc(y * sizeof(struct VARPARS));
1999: -
2000: - tablpars = (struct TBLPARS *)
2001: - Smalloc(y * sizeof(struct TBLPARS));
2002: -
2003: - basics = (int *)
2004: - Smalloc(y * sizeof(int));
2005: - procstack = (struct PROCSTACK **)
2006: - Smalloc(y * sizeof(struct PROCSTACK *));
2007: - mbox = (struct MBOX *)
2008: - Smalloc(z * sizeof(struct MBOX));
2009: -
2010: - effnrstates = (int *)
2011: - Smalloc(n * sizeof(int));
2012: -}
2013: -
2014: -alloc2(n, p, who)
2015: -{ char x;
2016: -
2017: - x = (qoverride && p > QMAX)? QMAX : p;
2018: -
2019: - if (x >= 256)
2020: - whoops("illegal queue size");
2021: - if (x >= 16)
2022: - fprintf(stderr, "warning, very large qsize (%d), queue %d\n", x, n);
2023: -
2024: - mbox[n].limit = x;
2025: - mbox[n].owner = (who >= 0) ? who : 0;
2026: -}
2027: -
2028: -alloc3(n)
2029: -{ inits = (int *)
2030: - Smalloc(n * sizeof(int));
2031: -}
2032: -
2033: -alloc4(n)
2034: -{ if (assertbl == NONE && errortbl == NONE)
2035: - globvars = (int *)
2036: - Smalloc(n * sizeof(int));
2037: - else
2038: - globvars = (int *)
2039: - Emalloc(n * sizeof(int));
2040: -}
2041: -
2042: -alloc45(n)
2043: -{ register int i;
2044: - fullname = (struct MNAME *)
2045: - Smalloc(n * sizeof(struct MNAME));
2046: - xob = (int *)
2047: - Smalloc((n+msgbase) * sizeof(int));
2048: - for (i = 0; i < n+msgbase; i++)
2049: - xob[i] = -1;
2050: -}
2051: -
2052: -alloc5(n)
2053: -{ register int i, j, r, c;
2054: -
2055: - r = tbl[n].nrrows;
2056: - if ((c = tbl[n].nrcols) > maxcol)
2057: - maxcol = c;
2058: -
2059: - tbl[n].endrow = (int *) Smalloc(r * sizeof(int));
2060: - tbl[n].deadrow = (int *) Smalloc(r * sizeof(int));
2061: - tbl[n].badrow = (int *) Smalloc(r * sizeof(int));
2062: - tbl[n].labrow = (int *) Smalloc(r * sizeof(int));
2063: - tbl[n].colmap = (int *) Smalloc(c * sizeof(int));
2064: - tbl[n].colorg = (int *) Smalloc(c * sizeof(int));
2065: - tbl[n].coltyp = (int *) Smalloc(c * sizeof(int));
2066: - tbl[n].ptr = (struct IND **) Smalloc(r * sizeof(struct IND *));
2067: - tbl[n].rowname = (char **) Smalloc(r * sizeof(char *));
2068: -
2069: - for (i = 0; i < r; i++)
2070: - { tbl[n].ptr[i] = (struct IND *)
2071: - Smalloc(c * sizeof(struct IND));
2072: - tbl[n].rowname[i] = (char *)
2073: - Smalloc(128 * sizeof(char));
2074: -
2075: - for (j = 0; j < c; j++)
2076: - tbl[n].ptr[i][j].nrpils = 0;
2077: - tbl[n].deadrow[i] = 1;
2078: - tbl[n].endrow[i] = tbl[n].badrow[i] = 0;
2079: - tbl[n].labrow[i] = 0;
2080: - }
2081: - tbl[n].labrow[0] = 1; /* make sure initial state is always checked */
2082: -}
2083: -
2084: -alloc6(n, m, p, q)
2085: -{ tbl[n].ptr[m][p].one = (struct ELM *)
2086: - Smalloc(q * sizeof(struct ELM));
2087: -}
2088: -
2089: -alloc8(pr, p, q)
2090: -{
2091: - tablpars[pr].nrms = (short) p; /* available */
2092: - tablpars[pr].nrvs = (short) q;
2093: -
2094: - procpars[pr].ms = (short *)
2095: - Emalloc(p * sizeof(short));
2096: - procpars[pr].vs = (short *)
2097: - Emalloc(q * sizeof(short));
2098: -
2099: - procpars[pr].nrms = 0; /* actually used */
2100: - procpars[pr].nrvs = 0;
2101: -}
2102: -
2103: -alloc9(in, p)
2104: -{
2105: - tbl[in].calls = (struct CPARS *)
2106: - Smalloc(p * sizeof(struct CPARS));
2107: -}
2108: -
2109: -alloc10(in, cn, p, q, r)
2110: -{
2111: - tbl[in].calls[cn].callwhat = (short) p;
2112: - tbl[in].calls[cn].nrms = (short) q;
2113: - tbl[in].calls[cn].nrvs = (short) r;
2114: -
2115: - tbl[in].calls[cn].ms = (short *)
2116: - Smalloc(q * sizeof (short));
2117: -
2118: - tbl[in].calls[cn].vs = (short *)
2119: - Smalloc(r * sizeof (short));
2120: -}
2121: -
2122: -whoops(s)
2123: - char *s;
2124: -{
2125: - fprintf(stderr, "trace: %s\n", s);
2126: - postlude();
2127: - exit(1);
2128: -}
2129: -
2130: -badinput(s)
2131: - char *s;
2132: -{ extern char fname[];
2133: -
2134: - fflush(stdout);
2135: - fprintf(stderr, "trace: read error `%s': %s\n", s, fname);
2136: - exit(1);
2137: -}
2138: //GO.SYSIN DD trace2.c
2139: echo trace3.c 1>&2
2140: sed 's/.//' >trace3.c <<'//GO.SYSIN DD trace3.c'
2141: -#include <stdio.h>
2142: -#include "trace.h"
2143: -#include "trace.d"
2144: -
2145: -#define DEBUG 0
2146: -
2147: -#define BS(n) ((n) & ~(PASSED))
2148: -
2149: - extern struct TBL *tbl;
2150: - extern struct LBT *lbt;
2151: - extern struct MBOX *mbox;
2152: - extern struct MNAME *fullname;
2153: - extern struct PROCSTACK **procstack;
2154: -
2155: - extern struct VARPARS *procpars;
2156: - extern struct TBLPARS *tblpars;
2157: -
2158: - extern struct LOCVARS *tblvars;
2159: - extern struct TBLPARS *tablpars;
2160: -
2161: - extern struct QUEUE **starter, **head, **tail;
2162: - extern struct QUEUE *s_first, *s_last;
2163: - extern struct VISIT *lastvisit;
2164: -
2165: - extern int *reftasks, *processes, *basics;
2166: - extern int *globvars, *inits, *state, *qsize;
2167: -
2168: - extern int nrtbl, nrqs, nrrefs, nrprocs, nrinit;
2169: - extern int nrvars, nrmesgs, msgbase;
2170: - extern int maxlevel, maxreached;
2171: -
2172: - extern char noshortcut, prbyq, timedd, blast, qandirty, muststore;
2173: - extern char maxxed, completed, lockplus, firstlock;
2174: -
2175: - extern long locksf, normf, loopsf;
2176: - extern double zapper;
2177: -
2178: - short lastqueue; /* the last queue addressed */
2179: - int level = 0;
2180: - double COUNT = 0;
2181: -
2182: - char *emalloc(), *Realloc(), *Emalloc();
2183: -
2184: -determine(m)
2185: -{
2186: - if (m >= 3*MANY) return 0; /* constant */
2187: - else if (m >= 2*MANY) return 1; /* parameter */
2188: - else if (m >= MANY) return 2; /* local */
2189: - else if (m >= 0) return 3; /* global */
2190: - else if (m < -3*MANY) return 5; /* negative number */
2191: - else if (m <= -2) return 4; /* expression */
2192: - else
2193: - whoops("cannot happen - determine");
2194: -}
2195: -
2196: -convert(m, pr)
2197: -{ int res, n = m;
2198: -
2199: - /* convert a pvar: global, local, parameter, or a constant */
2200: -
2201: - switch (determine(n)) {
2202: - case 5: res = n + 3*MANY; break;
2203: - case 4: res = evalcond(-(m+2), pr); break;
2204: - case 0: res = n - 3*MANY; break;
2205: - case 1: res = wapper(m, pr); break;
2206: - case 2: n -= MANY;
2207: - if (n >= 0 && n < (int) procpars[pr].nrlvars)
2208: - res = (int) procpars[pr].lvarvals[n];
2209: - else
2210: - whoops("reference to non-existing local var");
2211: - break;
2212: - case 3: if (n >= 0 && n < nrvars)
2213: - res = globvars[n];
2214: - else
2215: - whoops("reference to non-existing global var");
2216: - break;
2217: - default:
2218: - whoops("cannot happen - convert"); /* got a parameter */
2219: - break;
2220: - }
2221: - return res;
2222: -}
2223: -
2224: -wapper(n, pr)
2225: -{ int x = n - 2*MANY;
2226: - int y;
2227: - if (x < 0 || x >= MANY)
2228: - return n; /* not a parameter */
2229: - else
2230: - { if (x >= procpars[pr].nrvs)
2231: - whoops("unknown parameter of type pvar");
2232: - y = (int) procpars[pr].vs[x];
2233: - if (y >= 2*MANY && y < 3*MANY)
2234: - whoops("unresolved parameter reference");
2235: - return y;
2236: - }
2237: -}
2238: -
2239: -mapper(n, pr) /* convert a message parameter */
2240: -{ register int x = n - MANY;
2241: -
2242: - if (x < 0 || x >= MANY)
2243: - return n; /* not a parameter */
2244: - else
2245: - { if (x >= procpars[pr].nrms)
2246: - whoops("bad news: illegal message parameter");
2247: - return ((int)procpars[pr].ms[x]);
2248: - }
2249: -}
2250: -
2251: -matchon(n, m, t, trial, TT, pr)
2252: -{
2253: -#if DEBUG
2254: - printf("trial %d, pr %d; ", trial, pr);
2255: - if (TT == INP || TT == OUTP)
2256: - printf("msg %s, ", fullname[n-msgbase].mname);
2257: - else
2258: - printf("code %d, ", n);
2259: - printf("q %d, tbl %d, type %d\n", m, t, TT);
2260: -#endif
2261: -
2262: - if (trial == 2)
2263: - return (TT == TMO && qsize[m] == 0);
2264: - else
2265: - {
2266: - switch (TT) {
2267: - case FCT :
2268: - case SPN : return 1;
2269: - case CND : return (evalcond(n, pr));
2270: - case DFL : return (qsize[m] > 0 && no_other(t,head[m]->mesg,pr));
2271: - case INP : return (qsize[m] > 0 && BS(head[m]->mesg) == n);
2272: - case TMO : return (noshortcut && qsize[m] == 0);
2273: - case OUTP: return (qsize[m] < mbox[m].limit);
2274: - default : whoops("unknown type in column head");
2275: - }
2276: - }
2277: -}
2278: -
2279: -no_other(x, yy, pr)
2280: -{ struct TBL *tmp = &(tbl[x]);
2281: - int y = BS(yy);
2282: - int j = tmp->nrcols;
2283: - int h = state[pr];
2284: - int i;
2285: -
2286: - for (i = 0; i < j; i++)
2287: - { if (tmp->coltyp[i] == INP
2288: - && tmp->ptr[h][i].nrpils > 0
2289: - && y == lbt[pr].mapcol[i])
2290: - return 0;
2291: - }
2292: - return 1;
2293: -}
2294: -
2295: -send(m, to, with, pr, nst)
2296: -{ struct QUEUE *tmp;
2297: - register struct QUEUE *hook = tail[to];
2298: - int what = NONE;
2299: -
2300: - if (with != NONE)
2301: - { if ((what = convert(with, pr)) >= USED - 1 || what < 0)
2302: - { output("aborted: ", 0);
2303: - whoops("cargo too large or negative");
2304: - }
2305: - hook->cargo = (unsigned short) ( what | USED );
2306: - } else
2307: - hook->cargo = (unsigned short) 0;
2308: -
2309: - if (qsize[to] >= mbox[to].limit)
2310: - whoops("cannot happen - send");
2311: -
2312: - tmp = (struct QUEUE *) emalloc(sizeof(struct QUEUE));
2313: - tmp->last = hook;
2314: -#if TRAIL
2315: - hook->tstate[0] = (short) processes[pr];
2316: - hook->tstate[1] = (short) nst;
2317: -#endif TRAIL
2318: -
2319: - hook->mesg = (short) m;
2320: - hook->next = tmp;
2321: - hook->s_back = s_last;
2322: - hook->s_forw = NULL;
2323: - if (s_last == NULL)
2324: - s_first = hook;
2325: - else
2326: - s_last->s_forw = hook;
2327: -
2328: - s_last = hook;
2329: - tail[to] = tmp;
2330: - qsize[to]++;
2331: -#if DEBUG
2332: - printf("\tsent %d to %d, size %d, ", m, to, qsize[to]);
2333: - printf("cargo %d [%d]\n", what, hook->cargo);
2334: -#endif
2335: - require(OUTP, m, to);
2336: -
2337: - return 1;
2338: -}
2339: -
2340: -receive(from, with, pr, ice)
2341: - struct FREEZE *ice;
2342: -{ struct QUEUE *hook;
2343: - int what=NONE, wither;
2344: -
2345: - if (qsize[from] <= 0)
2346: - whoops("trying to receive from empty queue");
2347: -
2348: - hook = head[from];
2349: - if (hook->cargo & USED)
2350: - { what = (int) ((hook->cargo) & (~USED));
2351: - if (with == NONE)
2352: - { fprintf(stderr, "value %d sent (msg: ", what);
2353: - putname(hook, 1);
2354: - fprintf(stderr, ") but not expected\n");
2355: - }
2356: - else
2357: - { ice->whichvar = wither = wapper(with, pr);
2358: - if (wither >= 3*MANY || wither <= -3*MANY)
2359: - whoops("receiving into a constant...");
2360: - if (wither < MANY)
2361: - { ice->oldvalue = globvars[wither];
2362: - globvars[wither] = what;
2363: - } else
2364: - { int n = wither - MANY;
2365: - if (n >= 0 && n < (int) procpars[pr].nrlvars)
2366: - { ice->oldvalue = procpars[pr].lvarvals[n];
2367: - procpars[pr].lvarvals[n] = (short) what;
2368: - } else
2369: - whoops("unknown local var");
2370: - }
2371: - }
2372: - } else
2373: - { if (with != NONE)
2374: - { fprintf(stderr, "value %d expected (msg: ", with);
2375: - putname(hook, 1);
2376: - fprintf(stderr, ") but not sent\n");
2377: - }
2378: - }
2379: -
2380: - hook->mesg |= PASSED;
2381: -#if DEBUG
2382: - printf("\trecv %d from queue %d, ", head[from]->mesg & (~PASSED), from);
2383: - printf("cargo %d [%d], into var %d\n", what, hook->cargo, with);
2384: -#endif
2385: -
2386: - head[from] = hook->next;
2387: - qsize[from]--;
2388: -
2389: - require(INP, (hook->mesg & (~PASSED)), from);
2390: -
2391: - return 1;
2392: -}
2393: -
2394: -unrecv(from)
2395: -{
2396: - if (head[from] == starter[from])
2397: - whoops("unreceiving beyond initial state");
2398: -
2399: - head[from] = head[from]->last;
2400: - head[from]->mesg &= (~PASSED);
2401: -
2402: - qsize[from]++;
2403: -}
2404: -
2405: -unsend()
2406: -{ short i = lastqueue;
2407: -
2408: - if (tail[i] == starter[i])
2409: - whoops("unsending beyond initial state");
2410: - if ((tail[i] = tail[i]->last) != s_last)
2411: - whoops("unsend: tail not last sent message");
2412: -
2413: - if ((s_last = s_last->s_back) != NULL)
2414: - s_last->s_forw = NULL;
2415: - else
2416: - s_first = NULL;
2417: - efree(tail[i]->next);
2418: -
2419: - qsize[i]--;
2420: -}
2421: -
2422: -output(tag, willabort)
2423: - char *tag;
2424: -{ struct QUEUE *tmp;
2425: -
2426: - printf("%s", tag);
2427: -
2428: - if ((tmp = s_first) != NULL)
2429: - { formatted((struct QUEUE *) 0);
2430: - if (prbyq != 2)
2431: - do putname(tmp, 0); while ((tmp = tmp->s_forw) != NULL);
2432: - putchar('\n');
2433: - } else
2434: - printf("null output\n");
2435: -
2436: - if (willabort == 2 || (firstlock && willabort == 1))
2437: - { completed = 1;
2438: - postlude();
2439: - }
2440: -}
2441: -
2442: -putname(tmp, how)
2443: - struct QUEUE *tmp;
2444: -{ int i, k = (int) (BS(tmp->mesg)) - msgbase;
2445: - char nnn[128];
2446: -
2447: - i = strlen(fullname[k].mname);
2448: - if (tmp->mesg & PASSED)
2449: - sprintf(nnn, "%s", fullname[k].mname);
2450: - else
2451: - { sprintf(nnn, "[%s]", fullname[k].mname);
2452: - i += 2;
2453: - }
2454: -
2455: - if (tmp->cargo & USED)
2456: - sprintf(&nnn[i], "(%d),", (tmp->cargo & (~USED)));
2457: - else
2458: - sprintf(&nnn[i], ",");
2459: -
2460: - if (how)
2461: - fprintf(stderr, "%s", nnn);
2462: - else
2463: - printf("%s", nnn);
2464: -
2465: - return strlen(nnn);
2466: -}
2467: -
2468: -inendstate()
2469: -{ int i, j, k;
2470: -
2471: - for (i = 0, k = nrprocs; i < nrprocs; i++)
2472: - { j = processes[i];
2473: - if (j != basics[i] || tbl[j].endrow[state[i]] != 1)
2474: - k--;
2475: - }
2476: - return k;
2477: -}
2478: -
2479: -formatted(at)
2480: - struct QUEUE *at;
2481: -{ struct QUEUE *tmp = s_first;
2482: - int i, j; extern int linecode;
2483: -
2484: - if (tmp == NULL)
2485: - return;
2486: -
2487: - switch((int) prbyq) {
2488: - case 0: break;
2489: - case 1:
2490: - for (i = 0; i < nrqs; i++)
2491: - { printf("\n\t%s = {", mbox[i].qname);
2492: - for (tmp = starter[i]; tmp != tail[i]; tmp = tmp->next)
2493: - putname(tmp, 0);
2494: - printf("}");
2495: - }
2496: - printf("\nexecution sequence:\n\t");
2497: - break;
2498: - case 2: putchar('\n');
2499: - for (i = 0; i < nrqs; i++)
2500: - printf("%2d = %s\n", i, mbox[i].qname);
2501: - for (i = 0; i < nrqs; i++)
2502: - printf("\t%2d", i);
2503: -#if TRAIL
2504: - if (linecode)
2505: - printf(" \tsource");
2506: -#endif TRAIL
2507: - putchar('\n');
2508: - do
2509: - { if (tmp == at)
2510: - printf(" >>");
2511: - for (i = j = whichq(BS(tmp->mesg)); i >= 0; i--)
2512: - putchar('\t');
2513: - i = putname(tmp, 0);
2514: -#if TRAIL
2515: - if (linecode)
2516: - { for (i = 16-i; i > 0; i--) putchar(' ');
2517: - for (j = nrqs-j; j > 0; j--) putchar('\t');
2518: - printf("%s", tbl[tmp->tstate[0]].rowname[tmp->tstate[1]]);
2519: - }
2520: -#endif TRAIL
2521: - putchar('\n');
2522: - } while ((tmp = tmp->s_forw) != NULL);
2523: - if (at != NULL)
2524: - printf(" >>\n");
2525: - break;
2526: - }
2527: -}
2528: -
2529: -putloop(at, aa)
2530: - struct QUEUE *at;
2531: - char aa;
2532: -{ register struct QUEUE *tmp = s_first;
2533: -
2534: - if (aa)
2535: - printf("loop:\t");
2536: - else
2537: - printf("assertion violated: ");
2538: -
2539: - if (s_first != NULL)
2540: - { formatted(at);
2541: - if (prbyq != 2)
2542: - { do
2543: - { putname(tmp, 0);
2544: - if (tmp == at)
2545: - printf("//");
2546: - } while ((tmp = tmp->s_forw) != NULL);
2547: - printf("//\n");
2548: - }
2549: - } else
2550: - printf("null output\n");
2551: -}
2552: -
2553: -ppop(pr)
2554: -{ struct PROCSTACK *tmp = procstack[pr];
2555: - int i = (int) procstack[pr]->uptable;
2556: -
2557: - if (procstack[pr] == NULL)
2558: - whoops("null stack");
2559: -
2560: - restorvarpars(tmp->varparsaved, pr);
2561: - procstack[pr] = procstack[pr]->follow;
2562: -
2563: - efree(tmp->varparsaved);
2564: - efree(tmp);
2565: -
2566: - return i; /* we're returing to this table */
2567: -}
2568: -
2569: -ppush(pr, what, tr)
2570: -{ struct PROCSTACK *tmp;
2571: -
2572: - tmp = (struct PROCSTACK *)
2573: - emalloc(sizeof(struct PROCSTACK));
2574: -
2575: - tmp->varparsaved = (struct VARPARS *)
2576: - emalloc(sizeof(struct VARPARS));
2577: -
2578: - savevarpars (tmp->varparsaved, pr);
2579: -
2580: - tmp->uptable = (short) what;
2581: - tmp->uptransf = (short) tr;
2582: - tmp->follow = procstack[pr];
2583: - procstack[pr] = tmp;
2584: -}
2585: -
2586: -setlvars(to, pr)
2587: -{ register int i;
2588: - short z = tblvars[to].nrlvars;
2589: -
2590: - if (z > tablpars[pr].nrlvars)
2591: - { if (tablpars[pr].nrlvars > 0)
2592: - procpars[pr].lvarvals = (short *)
2593: - Realloc(procpars[pr].lvarvals, z * sizeof(short));
2594: - else
2595: - procpars[pr].lvarvals = (short *)
2596: - Emalloc(z * sizeof(short));
2597: -
2598: - tablpars[pr].nrlvars = z;
2599: - }
2600: -
2601: - procpars[pr].nrlvars = z;
2602: -
2603: - for (i = 0; i < z; i++)
2604: - procpars[pr].lvarvals[i] = convert(tblvars[to].lvarvals[i], pr);
2605: -}
2606: -
2607: -setpars(from, to, pr)
2608: - struct CPARS *from;
2609: -{ struct VARPARS tbuff;
2610: - register int i;
2611: - short x = tblpars[to].nrms;
2612: - short y = tblpars[to].nrvs;
2613: -
2614: - savemapped(&tbuff, from, pr); /* mapper() needs old nrms & nrvs */
2615: -
2616: - if (x > tablpars[pr].nrms)
2617: - { if (tablpars[pr].nrms > 0)
2618: - procpars[pr].ms = (short *)
2619: - Realloc(procpars[pr].ms, x * sizeof(short));
2620: - else
2621: - procpars[pr].ms = (short *)
2622: - Emalloc(x * sizeof(short));
2623: -
2624: - tablpars[pr].nrms = x;
2625: - }
2626: - if (y > tablpars[pr].nrvs)
2627: - { if (tablpars[pr].nrvs > 0)
2628: - procpars[pr].vs = (short *)
2629: - Realloc(procpars[pr].vs, y * sizeof(short));
2630: - else
2631: - procpars[pr].vs = (short *)
2632: - Emalloc(y * sizeof(short));
2633: -
2634: - tablpars[pr].nrvs = y;
2635: - }
2636: -
2637: - procpars[pr].nrms = tbuff.nrms;
2638: - procpars[pr].nrvs = tbuff.nrvs;
2639: -
2640: - for (i = 0; i < procpars[pr].nrms; i++)
2641: - procpars[pr].ms[i] = tbuff.ms[i];
2642: -
2643: - for (i = 0; i < procpars[pr].nrvs; i++)
2644: - procpars[pr].vs[i] = tbuff.vs[i];
2645: -
2646: - efree(tbuff.ms); efree(tbuff.vs);
2647: -}
2648: -
2649: -#if DEBUG
2650: -showstate()
2651: -{ int i, j;
2652: - printf("%2d: S:", level);
2653: - for (i = 0; i < nrprocs; i++)
2654: - printf("%d,", state[i]);
2655: - printf("M:");
2656: - for (i = 0; i < nrprocs; i++)
2657: - printf("%d,", processes[i]);
2658: - printf("Q:");
2659: - for (i = 0; i < nrqs; i++)
2660: - printf("%d,", qsize[i]);
2661: - printf("H:");
2662: - for (i = 0; i < nrqs; i++)
2663: - if (qsize[i] == 0)
2664: - printf("-,");
2665: - else
2666: - { j = (int) BS(head[i]->mesg);
2667: - printf("%s,", fullname[j-msgbase].mname);
2668: - }
2669: - printf("\tV:");
2670: - for (i = 0; i < nrprocs; i++)
2671: - { for (j = 0; j < procpars[i].nrlvars; j++)
2672: - printf("%d ", procpars[i].lvarvals[j]);
2673: - putchar(';');
2674: - }
2675: - putchar('\n');
2676: -}
2677: -#endif
2678: -
2679: -retable(prc, ice)
2680: - struct FREEZE *ice;
2681: -{ struct CUBE *it, *here;
2682: - int t = processes[prc];
2683: -
2684: - if (ice->cube == NULL)
2685: - { here = ice->cube = (struct CUBE *)
2686: - emalloc(sizeof(struct CUBE));
2687: - here->pntr = here->rtnp = NULL;
2688: - } else
2689: - { for (it = ice->cube; it->pntr != NULL; it = it->pntr)
2690: - ;
2691: - it->pntr = (struct CUBE *)
2692: - emalloc(sizeof(struct CUBE));
2693: - it->pntr->rtnp = it;
2694: - here = it->pntr;
2695: - here->pntr = NULL;
2696: - }
2697: - here->poporpush = POP;
2698: - here->which = (short) prc;
2699: - here->procsaved = (short) t;
2700: - here->transfsaved = procstack[prc]->uptransf;
2701: - here->varparsaved = (struct VARPARS *)
2702: - emalloc(sizeof(struct VARPARS));
2703: -
2704: - savevarpars(here->varparsaved, prc);
2705: - processes[prc] = ppop(prc);
2706: - fiddler(prc);
2707: - state[prc] = (int) here->transfsaved;
2708: - muststore = tbl[processes[prc]].labrow[state[prc]];
2709: -}
2710: -
2711: -savevarpars(at, j)
2712: - struct VARPARS *at;
2713: -{ register int i;
2714: - struct VARPARS *it;
2715: -
2716: - it = &(procpars[j]);
2717: - at->nrms = it->nrms;
2718: - at->nrvs = it->nrvs;
2719: - at->nrlvars = it->nrlvars;
2720: -
2721: - at->ms = (short *) emalloc(it->nrms * sizeof(short));
2722: - at->vs = (short *) emalloc(it->nrvs * sizeof(short));
2723: - at->lvarvals = (short *) emalloc(it->nrlvars * sizeof(short));
2724: -
2725: - for (i = 0; i < at->nrms; i++)
2726: - at->ms[i] = it->ms[i];
2727: - for (i = 0; i < at->nrvs; i++)
2728: - at->vs[i] = it->vs[i];
2729: - for (i = 0; i < it->nrlvars; i++)
2730: - at->lvarvals[i] = it->lvarvals[i];
2731: -}
2732: -
2733: -savemapped(at, it, j)
2734: - struct VARPARS *at;
2735: - struct CPARS *it;
2736: -{ register int i;
2737: -
2738: - at->nrms = it->nrms;
2739: - at->nrvs = it->nrvs;
2740: -
2741: - at->ms = (short *)
2742: - emalloc(it->nrms * sizeof(short));
2743: - at->vs = (short *)
2744: - emalloc(it->nrvs * sizeof(short));
2745: -
2746: - for (i = 0; i < at->nrms; i++)
2747: - at->ms[i] = (short) mapper(it->ms[i], j);
2748: -
2749: - for (i = 0; i < at->nrvs; i++)
2750: - at->vs[i] = (short) convert(it->vs[i], j);
2751: -}
2752: -
2753: -restorvarpars(at, pr)
2754: - struct VARPARS *at;
2755: -{ register int i;
2756: -
2757: - procpars[pr].nrms = at->nrms;
2758: - procpars[pr].nrvs = at->nrvs;
2759: - procpars[pr].nrlvars = at->nrlvars;
2760: -
2761: - for (i = 0; i < at->nrms; i++)
2762: - procpars[pr].ms[i] = at->ms[i];
2763: -
2764: - for (i = 0; i < at->nrvs; i++)
2765: - procpars[pr].vs[i] = at->vs[i];
2766: -
2767: - for (i = 0; i < at->nrlvars; i++)
2768: - procpars[pr].lvarvals[i] = at->lvarvals[i];
2769: -
2770: - efree(at->ms);
2771: - efree(at->vs);
2772: - efree(at->lvarvals);
2773: -}
2774: -
2775: -freeze(icy)
2776: - struct FREEZE *icy;
2777: -{ register int i;
2778: - struct FREEZE *ice = icy;
2779: -
2780: - ice->statsaved = (short *) emalloc(nrprocs * sizeof(short));
2781: - ice->varsaved = (short *) emalloc(nrvars * sizeof(short));
2782: -
2783: - ice->lastsav = lastqueue;
2784: - ice->cube = NULL;
2785: -
2786: - for (i = 0; i < nrvars; i++)
2787: - ice->varsaved[i] = (short) globvars[i];
2788: -
2789: - for (i = 0; i < nrprocs; i++)
2790: - {
2791: - ice->statsaved[i] = (short) state[i];
2792: -
2793: - while (tbl[processes[i]].deadrow[state[i]] && procstack[i] != NULL)
2794: - retable(i, ice);
2795: - }
2796: -}
2797: -
2798: -unfreeze(ice)
2799: - struct FREEZE *ice;
2800: -{ struct CUBE *here;
2801: - register int i;
2802: -
2803: - lastqueue = ice->lastsav;
2804: -
2805: - for (i = 0; i < nrprocs; i++)
2806: - state[i] = (int) ice->statsaved[i];
2807: - for (i = 0; i < nrvars; i++)
2808: - globvars[i] = (int) ice->varsaved[i];
2809: -
2810: - if ((here = ice->cube) != NULL)
2811: - while (here->pntr != NULL)
2812: - here = here->pntr;
2813: -
2814: - for (; here != NULL;)
2815: - { i = (int) here->which;
2816: - if (here->poporpush == PUSH)
2817: - { processes[i] = ppop(i);
2818: - } else
2819: - { /* use cube to restore the values from before the ppop */
2820: - ppush(i, processes[i], (int) here->transfsaved);
2821: - restorvarpars (here->varparsaved, i);
2822: - processes[i] = (int) here->procsaved;
2823: - efree(here->varparsaved);
2824: - }
2825: - efree(here);
2826: - fiddler(i);
2827: -
2828: - if (here == ice->cube)
2829: - break;
2830: - else
2831: - here = here->rtnp;
2832: - }
2833: - efree(ice->statsaved);
2834: - efree(ice->varsaved);
2835: -}
2836: -
2837: -FSE(I)
2838: -{ short g, h, i, j, k, t, x, y, z, X, Y, how;
2839: - char progress = 0, internal;
2840: - struct FREEZE *delta = (struct FREEZE *) emalloc(sizeof(struct FREEZE));
2841: - struct STATE *iam = NULL, *inloop();
2842: - struct VISIT *ticket;
2843: -
2844: - if (level >= maxreached)
2845: - { if (maxxed && level >= maxlevel)
2846: - { efree(delta);
2847: - return;
2848: - }
2849: - if (level > maxreached)
2850: - maxreached = level;
2851: - }
2852: - freeze(delta);
2853: -
2854: - if (muststore && (iam = inloop()) == NULL)
2855: - { unfreeze(delta);
2856: - efree(delta);
2857: - return;
2858: - }
2859: -
2860: -/*
2861: - * this state has not been seen before; the state
2862: - * information has been saved in the structure
2863: - * `STATE'; queue information has been saved in the
2864: - * last `VISIT' template of this state;
2865: - * we save a pointer to this template in a local variable:
2866: - * to be able to mark the state `analyzed' when we return
2867: - * for efficiency a pointer to the last visit is kept in a global `lastvisit'
2868: - */
2869: - ticket = lastvisit;
2870: - level++;
2871: - COUNT += (double) 1;
2872: -
2873: -/* three tries:
2874: - * 1st try accepts internal moves (no timeouts, no outputs),
2875: - * 2nd try accepts any moves except timeouts,
2876: - * 3rd try accepts only timeouts.
2877: - */
2878: -
2879: - for (X = 0; X <= 2; X++)
2880: - { internal = 0;
2881: - for (g = 0, i = I; g < nrprocs; g++, i = (i+1)%nrprocs)
2882: - { t = processes[i];
2883: - k = state[i];
2884: -
2885: - if (X == 0 && tbl[t].badrow[k])
2886: - continue; /* first try: skip fsm without receives */
2887: -
2888: - for (j = 0; j < tbl[t].nrcols; j++)
2889: - { if ((z = tbl[t].ptr[k][j].nrpils) == 0)
2890: - continue;
2891: -
2892: - x = lbt[i].mapcol[j];
2893: - y = lbt[i].orgcol[j];
2894: - Y = tbl[t].coltyp[j];
2895: -
2896: - if (matchon(x, y, t, X, Y, i))
2897: - { for (h = 0; h < z; h++)
2898: - { how = forward(t, k, j, h, x, y, i, Y, delta);
2899: -
2900: - if (qandirty || how == 0 || how >= LV || how == TC)
2901: - internal = 1;
2902: -
2903: - progress++;
2904: -#if DEBUG
2905: - printf("\tdown - %d/%d/%d\n", t, j, h);
2906: - showstate();
2907: -#endif
2908: - /* FSE(mbox[lastqueue].owner); */
2909: - FSE(0);
2910: -
2911: - backup(k, how, y, i, delta);
2912: -#if DEBUG
2913: - printf("\tup - %d/%d/%d\n", t, j, h);
2914: - showstate();
2915: -#endif
2916: - } } /* innermost loop: non-determinism */
2917: - if (blast && progress > 0)
2918: - break;
2919: - } /* inner loop: options per process */
2920: - if (internal)
2921: - break;
2922: - } /* outer loop: parallelism */
2923: - if (progress)
2924: - break; /* normal exit */
2925: - } /* outermost loop: 2 trials */
2926: - if (progress == 0)
2927: - {
2928: - if ((k = inendstate()) == nrprocs)
2929: - { normf++;
2930: - if (assertholds())
2931: - { if (lockplus) output("endstate: ", 0);
2932: - } else
2933: - output("assertion violated: ", 0);
2934: - }
2935: - else
2936: - { locksf++;
2937: - if (k == 0)
2938: - output("deadlock: ", 1);
2939: - else
2940: - output("partial lock: ", 1);
2941: - if (linecode)
2942: - { printf("State at time of lock:\n");
2943: - for (i = 0; i < nrprocs; i++)
2944: - printf("\tprocess %3d: state %s\n", i,
2945: - tbl[processes[i]].rowname[state[i]]);
2946: - putchar('\n');
2947: - } } }
2948: -
2949: - level--;
2950: -
2951: - unfreeze(delta); efree(delta);
2952: - if (iam != NULL)
2953: - { mark(iam, ticket);
2954: - if (zapper > 0 && (progress == 0 || level >= maxlevel-3))
2955: - swiffle(iam, ticket);
2956: - }
2957: -}
2958: -
2959: -forward(tb, k, j, h, m, from, pr, TT, ice)
2960: - struct FREEZE *ice;
2961: -{ int how=0, n=m;
2962: - struct ELM *at;
2963: -
2964: - ice->whichvar = NONE;
2965: -
2966: - at = &(tbl[tb].ptr[k][j].one[h]);
2967: -
2968: - switch (TT) {
2969: - case SPN: how = evalexpr(at->valtrans, pr, ice);
2970: - break;
2971: - case CND: break; /* `matchon()' already checked it */
2972: - case FCT: m = (int) tbl[tb].calls[n].callwhat;
2973: - ppush(pr, processes[pr], (int) at->transf);
2974: - setpars(&(tbl[tb].calls[n]), reftasks[m], pr);
2975: - setlvars(reftasks[m], pr);
2976: - processes[pr] = reftasks[m];
2977: - fiddler(pr);
2978: - state[pr] = 0;
2979: - muststore = tbl[processes[pr]].labrow[0];
2980: - return TC;
2981: - case TMO: send(m, from, NONE, pr, at->transf);
2982: - receive(from, NONE, pr, ice);
2983: - lastqueue = (short) from;
2984: - how = TO;
2985: - break;
2986: - case DFL:
2987: - case INP: receive(from, (int) at->valtrans, pr, ice);
2988: - how = RO;
2989: - break;
2990: - case OUTP: send(m, from, (int) at->valtrans, pr, at->transf);
2991: - lastqueue = (short) from;
2992: - how |= SO;
2993: - break;
2994: - }
2995: - state[pr] = (int) at->transf;
2996: - muststore = tbl[processes[pr]].labrow[state[pr]];
2997: -
2998: - return (how);
2999: -}
3000: -
3001: -backup(k, how, bx, i, ice)
3002: - struct FREEZE *ice;
3003: -{ int u = (int) ice->whichvar;
3004: -
3005: - if (u != NONE)
3006: - { if (u >= MANY)
3007: - procpars[i].lvarvals[u-MANY] = ice->oldvalue;
3008: - else
3009: - globvars[u] = ice->oldvalue;
3010: - }
3011: - switch (how) {
3012: - case TC: u = processes[i];
3013: - processes[i] = ppop(i);
3014: - fiddler(i);
3015: - break;
3016: - case TO: unrecv(bx);
3017: - case SO: unsend();
3018: - peekassert(ice);
3019: - break;
3020: - case SR: unsend();
3021: - case RO: unrecv(bx);
3022: - peekassert(ice);
3023: - default: break;
3024: - } state[i] = k;
3025: -}
3026: -
3027: -fiddler(pr)
3028: -{ register int i, t = processes[pr];
3029: -
3030: - for (i = 0; i < tbl[t].nrcols; i++)
3031: - if (tbl[t].colmap[i] >= MANY)
3032: - { lbt[pr].mapcol[i] = mapper(tbl[t].colmap[i], pr);
3033: - lbt[pr].orgcol[i] = whichq(lbt[pr].mapcol[i]);
3034: - } else
3035: - { lbt[pr].mapcol[i] = tbl[t].colmap[i];
3036: - lbt[pr].orgcol[i] = tbl[t].colorg[i];
3037: - }
3038: -
3039: -}
3040: //GO.SYSIN DD trace3.c
3041: echo trace4.c 1>&2
3042: sed 's/.//' >trace4.c <<'//GO.SYSIN DD trace4.c'
3043: -#include <stdio.h>
3044: -#include "trace.h"
3045: -#include "trace.d"
3046: -
3047: - extern char lockplus, prefix;
3048: - extern struct QUEUE *s_last;
3049: - extern int *processes, *globvars, *state, *qsize;
3050: - extern int nrprocs, nrrefs, nrvars, nrqs, level, assertbl, nrtbl;
3051: - extern long loopsf, zapped;
3052: - extern struct TBL *tbl;
3053: - extern struct PROCSTACK **procstack;
3054: - extern struct VARPARS *procpars;
3055: -
3056: - short *Factor, maxr = 0;
3057: - double iseen=0, ireseen=0, painful=0, kurshan=0;
3058: -
3059: - struct VISIT *lastvisit;
3060: - struct STATE *giveme(), *setstate();
3061: - char *Smalloc(), *emalloc();
3062: -
3063: -struct STATE *
3064: -inloop()
3065: -{ struct STATE *tmp;
3066: - register struct VISIT *hook;
3067: - register int x; char aa;
3068: - int i, nrnonempty=0, nrnon=0;
3069: - short h, hashvalue();
3070: -
3071: - for (i = 0; i < nrqs; i++)
3072: - if (qsize[i] > 0)
3073: - { nrnonempty += (1<<i);
3074: - nrnon++;
3075: - }
3076: - h = hashvalue(nrnonempty);
3077: - for (x = member(h); x > 0; x--)
3078: - { tmp = giveme(h, x);
3079: - if (samestate(tmp))
3080: - { for (hook = tmp->next; hook != NULL; hook = hook->next)
3081: - {
3082: - if (hook->howmany != nrnonempty
3083: - || !Queuesmatch(hook, nrnon))
3084: - continue;
3085: -
3086: - if (ISANA(hook))
3087: - { if (DEPTH(hook) > level)
3088: - { painful += 1;
3089: - continue;
3090: - }
3091: - if (prefix)
3092: - output("prefix: ", 0);
3093: - hook->prop.countme += 1;
3094: - kurshan += (double) 1;
3095: - return NULL;
3096: - } else
3097: - { loopsf++;
3098: - aa = (assertbl == NONE)? 1 : assertholds();
3099: - if (aa == 0 || lockplus)
3100: - putloop(hook->prop.s, aa);
3101: - return NULL;
3102: - } }
3103: - return setstate(tmp, h);
3104: - }
3105: - }
3106: - return setstate((struct STATE *) NULL, h);
3107: -}
3108: -
3109: -cmplvars(one, two)
3110: - struct LOCVARS *one;
3111: - struct VARPARS *two;
3112: -{ int i;
3113: -
3114: - if (one->nrlvars != two->nrlvars)
3115: - return 0;
3116: -
3117: - for (i = 0; i < one->nrlvars; i++)
3118: - if (one->lvarvals[i] != two->lvarvals[i])
3119: - return 0;
3120: -
3121: - return 1;
3122: -}
3123: -
3124: -cmplocals(one, two)
3125: - struct VARPARS *one, *two;
3126: -{ int i;
3127: -
3128: - if (one->nrlvars != two->nrlvars)
3129: - return 0;
3130: -
3131: - for (i = 0; i < one->nrlvars; i++)
3132: - if (one->lvarvals[i] != two->lvarvals[i])
3133: - return 0;
3134: -
3135: - return 1;
3136: -}
3137: -
3138: -cmparams(one, two)
3139: - struct VARPARS *one, *two;
3140: -{ int i;
3141: -
3142: - if (one->nrms != two->nrms || one->nrvs != two->nrvs)
3143: - whoops("cannot happen - cmparams");
3144: -
3145: - for (i = 0; i < one->nrms; i++)
3146: - if (one->ms[i] != two->ms[i])
3147: - return 0;
3148: -
3149: - for (i = 0; i < one->nrvs; i++)
3150: - if (one->vs[i] != two->vs[i])
3151: - return 0;
3152: -
3153: - return 1;
3154: -}
3155: -
3156: -cmpstacks(older, newer)
3157: - struct PROCSTACK *older, *newer;
3158: -{ struct PROCSTACK *tmp1 = older;
3159: - struct PROCSTACK *tmp2 = newer;
3160: -
3161: - while (tmp2 != NULL)
3162: - {
3163: - if (tmp1->uptable != tmp2->uptable
3164: - || tmp1->uptransf != tmp2->uptransf)
3165: - return 0;
3166: -
3167: - if (cmplocals(tmp1->varparsaved, tmp2->varparsaved) == 0
3168: - || cmparams (tmp1->varparsaved, tmp2->varparsaved) == 0)
3169: - return 0;
3170: -
3171: - tmp1 = tmp1->follow;
3172: - tmp2 = tmp2->follow;
3173: - }
3174: - return 1;
3175: -}
3176: -
3177: -samestate(at)
3178: - struct STATE *at;
3179: -{
3180: - return (sameP(at->pstate) && sametempl(at->pcon));
3181: -}
3182: -
3183: -cpylvars(into, from)
3184: - struct LOCVARS *into;
3185: - struct VARPARS *from;
3186: -{ register int i;
3187: -
3188: - into->nrlvars = from->nrlvars;
3189: - into->lvarvals = (short *)
3190: - Smalloc(from->nrlvars * sizeof(short));
3191: - for (i = 0; i < from->nrlvars; i++)
3192: - into->lvarvals[i] = from->lvarvals[i];
3193: -}
3194: -
3195: -cpylocals(into, from)
3196: - struct VARPARS *into, *from;
3197: -{ register int i;
3198: -
3199: - into->nrlvars = from->nrlvars;
3200: - into->lvarvals = (short *)
3201: - Smalloc(from->nrlvars * sizeof(short));
3202: - for (i = 0; i < from->nrlvars; i++)
3203: - into->lvarvals[i] = from->lvarvals[i];
3204: -}
3205: -
3206: -cpyparams(into, from)
3207: - struct VARPARS *into, *from;
3208: -{ int i;
3209: -
3210: - into->nrms = from->nrms;
3211: - into->ms = (short *)
3212: - Smalloc(from->nrms * sizeof(short));
3213: - for (i = 0; i < from->nrms; i++)
3214: - into->ms[i] = from->ms[i];
3215: -
3216: - into->nrvs = from->nrvs;
3217: - into->vs = (short *)
3218: - Smalloc(from->nrvs * sizeof(short));
3219: - for (i = 0; i < from->nrvs; i++)
3220: - into->vs[i] = from->vs[i];
3221: -}
3222: -
3223: -cpystacks(left, right)
3224: - struct PROCSTACK *left, *right;
3225: -{ struct PROCSTACK *into = left;
3226: - struct PROCSTACK *from = right;
3227: -
3228: - while (from != NULL)
3229: - { into->varparsaved = (struct VARPARS *)
3230: - Smalloc(sizeof(struct VARPARS));
3231: - cpylocals(into->varparsaved, from->varparsaved);
3232: - cpyparams(into->varparsaved, from->varparsaved);
3233: -
3234: - into->uptable = from->uptable;
3235: - into->uptransf = from->uptransf;
3236: -
3237: - if ((from = from->follow) != NULL)
3238: - { into->follow = (struct PROCSTACK *)
3239: - Smalloc(sizeof(struct PROCSTACK));
3240: - into = into->follow;
3241: - } }
3242: -}
3243: -
3244: -struct STATE *
3245: -newstate(pha)
3246: - int pha;
3247: -{ struct STATE *hook;
3248: - struct VISIT *findastate();
3249: - struct TEMPLATE *inTtable();
3250: - unsigned short *inPtable();
3251: -
3252: - hook = (struct STATE *) Smalloc(sizeof(struct STATE));
3253: - hook->pstate = inPtable();
3254: - hook->pcon = inTtable();
3255: - hook->next = findastate(hook); /* first visit */
3256: -
3257: - insert(pha, hook);
3258: -
3259: - return hook;
3260: -}
3261: -
3262: -struct VISIT *
3263: -oldstate(where)
3264: - struct STATE *where;
3265: -{ register struct VISIT *tmp;
3266: - struct VISIT *try, *findastate();
3267: -
3268: - ireseen += (double)1;
3269: - try = findastate(where);
3270: -
3271: - if (where->next == NULL)
3272: - where->next = try;
3273: - else
3274: - { for (tmp = where->next; tmp->next != NULL; tmp = tmp->next)
3275: - ;
3276: - tmp->next = try;
3277: - }
3278: -
3279: - return try;
3280: -}
3281: -
3282: -struct STATE *
3283: -setstate(where, ha)
3284: - struct STATE *where;
3285: -{ struct STATE *tmp;
3286: - struct VISIT *work;
3287: -
3288: - if (where == NULL)
3289: - { tmp = newstate(ha);
3290: - work = tmp->next;
3291: - } else
3292: - { tmp = where;
3293: - work = oldstate(where);
3294: - }
3295: -
3296: - work->prop.s = s_last;
3297: - work->depth = (short) level;
3298: -
3299: - lastvisit = work;
3300: - relink(work);
3301: -
3302: - return tmp;
3303: -}
3304: -
3305: -struct VISIT *
3306: -pickstate(at)
3307: - struct STATE *at;
3308: -{ struct VISIT *latter = NULL;
3309: - register struct VISIT *hook = at->next;
3310: -
3311: - for (hook = at->next; hook != NULL; hook = hook->next)
3312: - { if (ISANA(hook))
3313: - { if (latter == NULL)
3314: - at->next = hook->next;
3315: - else
3316: - latter->next = hook->next;
3317: -
3318: - efree(hook->c);
3319: - hook->next = NULL;
3320: - zapped++;
3321: -
3322: - return hook;
3323: - }
3324: - latter = hook;
3325: - }
3326: - return NULL;
3327: -}
3328: -
3329: -struct VISIT *
3330: -picknown(at, want)
3331: - struct STATE *at;
3332: - struct VISIT *want;
3333: -{ struct VISIT *latter = NULL;
3334: - register struct VISIT *hook;
3335: -
3336: - for (hook = at->next; hook != NULL; hook = hook->next)
3337: - { if (hook == want)
3338: - break;
3339: - latter = hook;
3340: - }
3341: - if (hook == NULL)
3342: - whoops("cannot happen - picknown");
3343: -
3344: - if (latter == NULL)
3345: - at->next = hook->next;
3346: - else
3347: - latter->next = hook->next;
3348: -
3349: - efree(hook->c);
3350: - hook->next = NULL;
3351: -
3352: - zapped++;
3353: - return hook;
3354: -}
3355: -
3356: -inihash()
3357: -{ register int i;
3358: - char *Smalloc();
3359: -
3360: - for (i = 0; i < nrtbl; i++)
3361: - if (tbl[i].nrrows > maxr)
3362: - maxr = tbl[i].nrrows;
3363: -
3364: - Factor = (short *)
3365: - Smalloc(maxr * sizeof(short));
3366: -
3367: - for (i = 0; i < maxr; i++)
3368: - Factor[i] = rand()%NOTOOBIG; /* number between 0 and 16k */
3369: -}
3370: -
3371: -short
3372: -hashvalue(g)
3373: -{ register int i, h;
3374: -
3375: - for (i = h = 0; i < nrprocs; i++)
3376: - { h = ((h << 2) | (h >> 13)); /* rotate */
3377: - h ^= Factor[state[i]] ^ Factor[processes[i]];
3378: - }
3379: - h += g;
3380: - return (h & NOTOOBIG);
3381: -}
3382: //GO.SYSIN DD trace4.c
3383: echo trace5.c 1>&2
3384: sed 's/.//' >trace5.c <<'//GO.SYSIN DD trace5.c'
3385: -#include <stdio.h>
3386: -#include "trace.h"
3387: -#include "trace.d"
3388: -
3389: - extern struct QUEUE **head, **tail;
3390: - extern int *qsize, nrqs, level, maxreached;
3391: - extern double iseen, ireseen, zapper;
3392: - extern double tryswiff, noswiff, cannot;
3393: - char *Realloc(), *Emalloc(), *Smalloc(), *emalloc();
3394: -
3395: - struct HTABLE {
3396: - struct STATE **index; /* index [h] [ibound] */
3397: - short ibound; /* nr of available slots */
3398: - short nr; /* nr of occupied slots */
3399: - } oldstates[NOTOOBIG+1]; /* index of hash values */
3400: -
3401: - int hbound=0, hlast=0;
3402: -
3403: -growindex(h)
3404: -{ int nsz = (int) oldstates[h].ibound + 8;
3405: -
3406: - if (nsz == 8)
3407: - oldstates[h].index = (struct STATE **)
3408: - Emalloc(nsz * sizeof(struct STATE *));
3409: - else
3410: - oldstates[h].index = (struct STATE **)
3411: - Realloc(oldstates[h].index, nsz * sizeof(struct STATE *));
3412: -
3413: - oldstates[h].ibound = (short) nsz;
3414: -}
3415: -
3416: -initable()
3417: -{ register int i;
3418: -
3419: - for (i = 0; i < NOTOOBIG+1; i++)
3420: - { oldstates[i].nr = 0;
3421: - oldstates[i].ibound = 0;
3422: - }
3423: - hbound = NOTOOBIG+1;
3424: -}
3425: -
3426: -insert(h, pnt) /* enter state pointer into the table at hash value h */
3427: - struct STATE *pnt;
3428: -{ short cin;
3429: -
3430: - if (h >= hbound)
3431: - { fprintf(stderr, "h %d, hbound %d, NOTOOBIG %d\n",h,hbound,NOTOOBIG);
3432: - whoops("cannot happen - insert");
3433: - }
3434: - cin = oldstates[h].nr++;
3435: - iseen += (double) 1;
3436: -
3437: - if (cin >= oldstates[h].ibound)
3438: - growindex(h);
3439: -
3440: - oldstates[h].index[cin] = pnt;
3441: -}
3442: -
3443: -mark(stt, vis)
3444: - struct STATE *stt;
3445: - struct VISIT *vis;
3446: -{
3447: - vis->prop.countme = 0;
3448: - vis->depth |= ANALYZED;
3449: -}
3450: -
3451: -relink(vis)
3452: - struct VISIT *vis;
3453: -{ struct CONTS *inqtable();
3454: - register int i, j, k;
3455: -
3456: - for (i = j = k = 0; i < nrqs ; i++)
3457: - if (qsize[i] > 0)
3458: - { j++;
3459: - k += (1 << i);
3460: - }
3461: - vis->howmany = k;
3462: -
3463: - if (zapper == 0) /* grow without bound */
3464: - vis->c = (struct CONTS **)
3465: - Smalloc(j * sizeof(struct CONTS *));
3466: - else
3467: - vis->c = (struct CONTS **)
3468: - emalloc(j * sizeof(struct CONTS *));
3469: -
3470: - for (i = k = 0; i < nrqs; i++)
3471: - { if (qsize[i] == 0)
3472: - continue;
3473: -
3474: - vis->c[k++] = inqtable(i);
3475: - }
3476: -}
3477: -
3478: -member(h) { return (h < hbound) ? oldstates[h].nr : 0; }
3479: -
3480: -struct STATE *
3481: -giveme(h, n)
3482: -{ int m = n - 1;
3483: - if (h >= hbound || oldstates[h].nr <= m || oldstates[h].index[m] == NULL)
3484: - whoops("cannot happen - giveme");
3485: -
3486: - return oldstates[h].index[m];
3487: -}
3488: -
3489: -struct VISIT *
3490: -findany(avoid)
3491: - struct STATE *avoid;
3492: -{ register int i, j;
3493: - struct VISIT *try, *pickstate();
3494: -
3495: - for (i = (hlast+1)%hbound; i != hlast; i++, i %= hbound)
3496: - for (j = 0; j < oldstates[i].nr; j++)
3497: - if (oldstates[i].index[j] != avoid
3498: - && (try = pickstate(oldstates[i].index[j])) != NULL)
3499: - { hlast = i;
3500: - return try;
3501: - }
3502: -
3503: - cannot += (double) 1; /* couldn't find a victim */
3504: - try = (struct VISIT *) Smalloc(sizeof(struct VISIT));
3505: - try->next = NULL;
3506: -
3507: - return try;
3508: -}
3509: -
3510: -struct VISIT *
3511: -findastate(avoid)
3512: - struct STATE *avoid;
3513: -{ struct VISIT *try = NULL;
3514: - struct VISIT *findany(), *picknown();
3515: - struct Swiffle *unswiffle(), *trs;
3516: -
3517: - if (ireseen < zapper || zapper == 0)
3518: - { try = (struct VISIT *) Smalloc(sizeof(struct VISIT));
3519: - try->next = NULL;
3520: - return try;
3521: - }
3522: - tryswiff += (double) 1;
3523: - if ((trs = unswiffle(avoid)) != NULL
3524: - && (try = picknown(trs->st, trs->vi)) != NULL)
3525: - return try;
3526: - noswiff += (double) 1;
3527: -
3528: - return findany(avoid);
3529: -}
3530: //GO.SYSIN DD trace5.c
3531: echo trace6.c 1>&2
3532: sed 's/.//' >trace6.c <<'//GO.SYSIN DD trace6.c'
3533: -#include <stdio.h>
3534: -#include "trace.h"
3535: -#include "trace.d"
3536: -
3537: - extern struct QUEUE **head, **tail;
3538: - extern int *qsize, nrqs, level;
3539: -
3540: - char *Realloc(), *Emalloc(), *Smalloc();
3541: -
3542: - struct CONTS ***oldqueues; /* index of queue states */
3543: - long *nrqstates, *qbound;
3544: -
3545: -iniqtable()
3546: -{ register int i;
3547: - nrqstates = (long *)
3548: - Smalloc(nrqs * sizeof(long));
3549: - qbound = (long *)
3550: - Smalloc(nrqs * sizeof(long));
3551: -
3552: - oldqueues = (struct CONTS ***)
3553: - Smalloc(nrqs * sizeof(struct CONTS **));
3554: -
3555: - for (i = 0; i < nrqs; i++)
3556: - nrqstates[i] = qbound[i] = 0;
3557: -}
3558: -
3559: -growqtable(p)
3560: -{ int nsz = qbound[p] + 32;
3561: -
3562: - if (nsz == 32)
3563: - oldqueues[p] = (struct CONTS **)
3564: - Emalloc(nsz * sizeof(struct CONTS *));
3565: - else
3566: - oldqueues[p] = (struct CONTS **)
3567: - Realloc(oldqueues[p], nsz * sizeof(struct CONTS *));
3568: -
3569: - qbound[p] = nsz;
3570: -}
3571: -
3572: -struct CONTS *
3573: -Qinsert(p)
3574: -{ struct CONTS * try;
3575: - struct QUEUE * tmp;
3576: - register int i, j;
3577: -
3578: - i = p;
3579: - j = qsize[p];
3580: -
3581: - if (nrqstates[p] >= qbound[p])
3582: - growqtable(p);
3583: -
3584: - try = (struct CONTS *)
3585: - Smalloc((j+1) * sizeof(struct CONTS));
3586: -
3587: - try[0].mesg = i;
3588: - try[0].cargo = j;
3589: -
3590: - for (tmp = head[i], j = 1; tmp != tail[i]; tmp = tmp->next, j++)
3591: - { try[j].mesg = (tmp->mesg & ~PASSED);
3592: - try[j].cargo = tmp->cargo;
3593: - }
3594: -
3595: - if (--j != qsize[p])
3596: - whoops("cannot happen - Qinsert");
3597: -
3598: - oldqueues[p][nrqstates[p]] = try;
3599: - nrqstates[p] += 1;
3600: -
3601: - return try;
3602: -}
3603: -
3604: -struct CONTS *
3605: -inqtable(p)
3606: -{ register int i;
3607: -
3608: - if (qsize[p] == 0)
3609: - whoops("cannot happen - inqtable");
3610: -
3611: - for (i = 0; i < nrqstates[p]; i++)
3612: - if (samequeue(oldqueues[p][i]))
3613: - return oldqueues[p][i];
3614: -
3615: - return Qinsert(p);
3616: -}
3617: -
3618: -samequeue(at)
3619: - struct CONTS *at;
3620: -{
3621: - register struct QUEUE *tmp;
3622: - register int j, k, m;
3623: -
3624: - k = at[0].mesg; /* which queue is this */
3625: - m = at[0].cargo; /* how many elements are here */
3626: -
3627: - if (qsize[k] != m)
3628: - return 0;
3629: -
3630: - for (tmp = head[k], j = 1; tmp != tail[k]; tmp = tmp->next, j++)
3631: - { if (at[j].mesg != (tmp->mesg & ~PASSED)
3632: - || at[j].cargo != tmp->cargo)
3633: - return 0;
3634: - }
3635: - return 1;
3636: -}
3637: -
3638: -Queuesmatch(vis, k)
3639: - struct VISIT *vis;
3640: - register int k;
3641: -{
3642: - register int i;
3643: -
3644: - for (i = 0; i < k; i++)
3645: - if (samequeue(vis->c[i]) == 0)
3646: - return 0;
3647: - return 1;
3648: -}
3649: //GO.SYSIN DD trace6.c
3650: echo trace7.c 1>&2
3651: sed 's/.//' >trace7.c <<'//GO.SYSIN DD trace7.c'
3652: -#include <stdio.h>
3653: -#include "trace.h"
3654: -#include "trace.d"
3655: -
3656: -struct Swiffle *slist, *slast, *flast;
3657: -int nswiff = 0, fswiff = 0;
3658: -
3659: -struct Swiffle *
3660: -unswiffle(avoid)
3661: - struct STATE *avoid;
3662: -{
3663: - register struct Swiffle *try;
3664: - register int i;
3665: - struct Swiffle *result = (struct Swiffle *) NULL;
3666: -
3667: - for (i = nswiff, try = slist; i > 0; i--, try = try->next)
3668: - if (try->st != avoid)
3669: - { result = try;
3670: - getput(try, i);
3671: - break;
3672: - }
3673: -
3674: - return result;
3675: -}
3676: -
3677: -swiffle(this, that)
3678: - struct STATE *this;
3679: - struct VISIT *that;
3680: -{
3681: - struct Swiffle *getswiff(), *try;
3682: -
3683: - try = getswiff();
3684: - try->st = this;
3685: - try->vi = that;
3686: -
3687: - if (nswiff++ == 0)
3688: - slist = try;
3689: - else
3690: - { slast->next = try;
3691: - try->last = slast;
3692: - }
3693: - slast = try;
3694: -}
3695: -
3696: -getput(try, n)
3697: - struct Swiffle *try;
3698: -{
3699: -/* unlink from slist: */
3700: - if (try == slist)
3701: - slist = try->next;
3702: - else
3703: - try->last->next = try->next;
3704: -
3705: - if (n > 1)
3706: - try->next->last = try->last;
3707: -
3708: - if (try == slast)
3709: - { if (try == slist)
3710: - slast = (struct Swiffle *) NULL;
3711: - else
3712: - slast = try->last;
3713: - }
3714: - nswiff--;
3715: -
3716: -/* relink in flist: */
3717: -
3718: - try->next = (struct Swiffle *) NULL;
3719: -
3720: - if (fswiff++ == 0)
3721: - try->last = (struct Swiffle *) NULL;
3722: - else
3723: - { flast->next = try;
3724: - try->last = flast;
3725: - }
3726: - flast = try;
3727: -}
3728: -
3729: -struct Swiffle *
3730: -getswiff()
3731: -{ struct Swiffle *try;
3732: - char *Smalloc();
3733: -
3734: - if (fswiff == 0)
3735: - try = (struct Swiffle *) Smalloc(sizeof(struct Swiffle));
3736: - else
3737: - { fswiff--;
3738: - try = flast;
3739: - if ((flast = try->last) != NULL)
3740: - flast->next = (struct Swiffle *) NULL;
3741: - }
3742: - try->next = try->last = (struct Swiffle *) NULL;
3743: -
3744: - return try;
3745: -}
3746: //GO.SYSIN DD trace7.c
3747: echo trace8.c 1>&2
3748: sed 's/.//' >trace8.c <<'//GO.SYSIN DD trace8.c'
3749: -#include <stdio.h>
3750: -#include "trace.h"
3751: -#include "trace.d"
3752: -
3753: - extern int *globvars;
3754: - extern int nrprocs, nrrefs, nrvars;
3755: - extern struct PROCSTACK **procstack;
3756: - extern struct VARPARS *procpars;
3757: -
3758: - char *Realloc(), *Emalloc(), *Smalloc();
3759: -
3760: - struct TEMPLATE **templates;
3761: - int nrtemplates = 0, tbound = 0;
3762: -
3763: -growttable()
3764: -{ int nsz = tbound + 32;
3765: -
3766: - if (nsz == 32)
3767: - templates = (struct TEMPLATE **)
3768: - Emalloc(nsz * sizeof(struct TEMPLATE *));
3769: - else
3770: - templates = (struct TEMPLATE **)
3771: - Realloc(templates, nsz * sizeof(struct TEMPLATE *));
3772: -
3773: - tbound = nsz;
3774: -
3775: -}
3776: -
3777: -struct TEMPLATE *
3778: -Tinsert()
3779: -{ struct TEMPLATE *try;
3780: - register int i;
3781: -
3782: - if (nrtemplates >= tbound)
3783: - growttable();
3784: -
3785: - try = (struct TEMPLATE *)
3786: - Smalloc(sizeof(struct TEMPLATE));
3787: - try->l_vars = (struct LOCVARS **)
3788: - Smalloc(nrprocs * sizeof(struct LOCVARS *));
3789: - try->g_vars = (short *)
3790: - Smalloc(nrvars * sizeof(short));
3791: -
3792: - for (i = 0; i < nrvars; i++)
3793: - try->g_vars[i] = (short) globvars[i];
3794: -
3795: - if (nrrefs > 0)
3796: - try->traceback = (struct PROCSTACK **)
3797: - Smalloc(nrprocs * sizeof(struct PROCSTACK *));
3798: -
3799: - for (i = 0; i < nrprocs; i++)
3800: - { try->l_vars[i] = (struct LOCVARS *)
3801: - Smalloc(sizeof(struct LOCVARS));
3802: -
3803: - cpylvars(try->l_vars[i], &(procpars[i]));
3804: -
3805: - if (nrrefs > 0)
3806: - { if (procstack[i] == NULL)
3807: - { try->traceback[i] = NULL;
3808: - continue;
3809: - }
3810: - try->traceback[i] = (struct PROCSTACK *)
3811: - Smalloc(sizeof(struct PROCSTACK));
3812: - cpystacks(try->traceback[i], procstack[i]);
3813: - } }
3814: -
3815: - templates[nrtemplates] = try;
3816: - nrtemplates++;
3817: -
3818: - return try;
3819: -}
3820: -
3821: -struct TEMPLATE *
3822: -inTtable()
3823: -{ register int i;
3824: -
3825: - for (i = 0; i < nrtemplates; i++)
3826: - if (sametempl(templates[i]))
3827: - return templates[i];
3828: -
3829: - return Tinsert();
3830: -}
3831: -
3832: -sametempl(at)
3833: - struct TEMPLATE *at;
3834: -{ register int i;
3835: -
3836: - for (i = 0; i < nrprocs; i++)
3837: - { if (cmplvars(at->l_vars[i], &(procpars[i])) == 0 ||
3838: - (nrrefs > 0 && cmpstacks(at->traceback[i], procstack[i]) == 0))
3839: - return 0;
3840: - }
3841: -
3842: - for (i = 0; i < nrvars; i++)
3843: - if (at->g_vars[i] != (short) globvars[i])
3844: - return 0;
3845: -
3846: - return 1;
3847: -}
3848: //GO.SYSIN DD trace8.c
3849: echo trace9.c 1>&2
3850: sed 's/.//' >trace9.c <<'//GO.SYSIN DD trace9.c'
3851: -#include <stdio.h>
3852: -#include "trace.h"
3853: -#include "trace.d"
3854: -
3855: - extern int nrprocs, *processes, *state;
3856: -
3857: - char *Realloc(), *Emalloc(), *Smalloc();
3858: -
3859: - unsigned short **pstates;
3860: - int pgrowth = 32;
3861: - int nrpstates = 0;
3862: - int pbound = 0;
3863: -
3864: -growPtable()
3865: -{ int p = pbound + pgrowth;
3866: -
3867: - if (p == pgrowth)
3868: - pstates = (unsigned short **)
3869: - Emalloc(p * sizeof(unsigned short *));
3870: - else
3871: - pstates = (unsigned short **)
3872: - Realloc(pstates, p * sizeof(unsigned short *));
3873: - pbound = p;
3874: -}
3875: -
3876: -unsigned short *
3877: -Pinsert()
3878: -{ unsigned short *try;
3879: - register int i;
3880: -
3881: - if (nrpstates >= pbound)
3882: - growPtable();
3883: -
3884: - try = (unsigned short *)
3885: - Smalloc(nrprocs * sizeof(unsigned short));
3886: -
3887: - for (i = 0; i < nrprocs; i++)
3888: - try[i] = (unsigned short) (state[i] + (processes[i]<<10));
3889: -
3890: - pstates[nrpstates++] = try;
3891: -
3892: - return try;
3893: -}
3894: -
3895: -unsigned short *
3896: -inPtable()
3897: -{ register int i;
3898: -
3899: - for (i = 0; i < nrpstates; i++)
3900: - if (sameP(pstates[i]))
3901: - return pstates[i];
3902: -
3903: - return Pinsert();
3904: -}
3905: -
3906: -sameP(at)
3907: - unsigned short *at;
3908: -{ register int i;
3909: -
3910: - for (i = 0; i < nrprocs; i++)
3911: - { if ((at[i]&1023) != (unsigned short) state[i]
3912: - || at[i]>>10 != (unsigned short) processes[i])
3913: - return 0;
3914: - }
3915: - return 1;
3916: -}
3917: //GO.SYSIN DD trace9.c
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.