|
|
1.1 root 1: #include <stdio.h>
2: #include <errno.h>
3: #include "trace.h"
4: #include "trace.d"
5:
6: extern struct TBL *tbl;
7: extern struct LBT *lbt;
8: extern struct MBOX *mbox;
9: extern struct MNAME *fullname;
10: extern struct REVPOL **expr;
11: extern struct PROCSTACK **procstack;
12:
13: extern struct VARPARS *procpars;
14: extern struct TBLPARS *tblpars;
15:
16: extern struct LOCVARS *tblvars;
17: extern struct TBLPARS *tablpars;
18:
19: extern int *reftasks, *processes, *basics;
20: extern int *globvars, *inits, *xob, *effnrstates;
21:
22: extern char qoverride;
23: extern int QMAX, msgbase, maxcol, assertbl, errortbl;
24: extern int errno;
25:
26: #define tell(s) fprintf(stderr, s)
27:
28: usage(str)
29: char *str;
30: { fprintf(stderr, "trace: %s\n", str);
31: tell("usage: trace [-?] [N]\n");
32: tell("\t-a report on prefixes leading into old states\n");
33: tell("\t-b `blast mode' (quick, very partial search)\n");
34: tell("\t-c N perform class N validation (N: 0..5) \n");
35: tell("\t-f or -F format queue histories (two choices)\n");
36: tell("\t-i ignore pvar values in the analysis (rarely useful)\n");
37: tell("\t-j stop at the first buffer lock found\n");
38: tell("\t-k N restrict the state space cache to N thousand states\n");
39: tell("\t-l report also normal execution sequences and loops\n");
40: tell("\t-m N set bound N on the search depth\n");
41: tell("\t-n don't use timeout heuristics\n");
42: tell("\t-q N set bound N on maximum queue size used\n");
43: tell("\t-r N restrict the runtime to N minutes (overrides -R)\n");
44: tell("\t-R N report on progress every N minutes (overrides -r)\n");
45: tell("\t-s show only the transition tables\n");
46: tell("\t-t N ignore the state of process N (rarely useful)\n");
47: tell("\t-v verbose - print execution times, etc.\n");
48: tell("\t-x perform quick partial search\n");
49: tell("\t-y ignore the queues in the analysis (rarely useful)\n");
50: tell("\t-z (or no flag) guess parameters for a partial search\n");
51: exit(1);
52: }
53:
54: /*
55: * calls on Emalloc and Realloc go straight to the library malloc
56: * it is used for data that may be realloced but is never released
57: *
58: * Smalloc claims memory that is never realloced and never released
59: *
60: * emalloc and efree handle memory that is never realloced but often released
61: *
62: * talloc and tfree are direct calls on the tac-package (used via emalloc)
63: */
64:
65: char *
66: Stake(n)
67: { char * sbrk();
68: char * try;
69: do {
70: try = sbrk(n);
71: } while ((int) try == -1 && errno == EINTR);
72:
73:
74: if ((int) try == -1)
75: whoops("sbrk fault");
76:
77: return try;
78: }
79:
80: #define CHUNK 4096
81:
82: char *have;
83: long left = 0;
84:
85: char *
86: Smalloc(n)
87: unsigned n;
88: { char *try;
89:
90: if (n == 0)
91: return (char *) NULL;
92:
93: if (left < n)
94: { unsigned grow = (n < CHUNK) ? CHUNK : n;
95: have = Stake(grow);
96: left = grow;
97: }
98: try = have;
99: have += n;
100: left -= n;
101:
102: return try;
103: }
104:
105: char *
106: Emalloc(n)
107: unsigned n;
108: { char *try;
109: char *malloc();
110:
111: if (n == 0)
112: return (char *) NULL;
113:
114: if ((try = malloc(n)) == NULL)
115: whoops("malloc fault"); /* to be reallocated */
116: return try;
117: }
118:
119: char *
120: Realloc(a, b)
121: char *a; unsigned b;
122: { char *try, *realloc();
123:
124: if (b == 0)
125: return (char *) NULL;
126:
127: try = realloc(a, b); /* standard realloc: never released again */
128: if (try == NULL)
129: whoops("realloc returns 0");
130:
131: return try;
132: }
133:
134: char *
135: emalloc(n)
136: unsigned n;
137: { char *try;
138: char *talloc();
139:
140: if (n == 0)
141: return (char *) NULL;
142: if ((try = talloc(n)) == NULL)
143: whoops("talloc fault");
144: return try;
145: }
146:
147: efree(at)
148: char *at;
149: {
150: if (at == NULL)
151: return;
152: tfree(at);
153: }
154:
155: alloc1(x, y, z)
156: { int n = x+y;
157: tbl = (struct TBL *)
158: Smalloc(n * sizeof(struct TBL));
159: tblpars = (struct TBLPARS *)
160: Smalloc(n * sizeof(struct TBLPARS));
161: tblvars = (struct LOCVARS *)
162: Smalloc(n * sizeof(struct LOCVARS));
163: reftasks = (int *)
164: Smalloc(x * sizeof(int));
165: processes = (int *)
166: Smalloc(y * sizeof(int));
167: lbt = (struct LBT *)
168: Smalloc(y * sizeof(struct LBT));
169: procpars = (struct VARPARS *)
170: Smalloc(y * sizeof(struct VARPARS));
171:
172: tablpars = (struct TBLPARS *)
173: Smalloc(y * sizeof(struct TBLPARS));
174:
175: basics = (int *)
176: Smalloc(y * sizeof(int));
177: procstack = (struct PROCSTACK **)
178: Smalloc(y * sizeof(struct PROCSTACK *));
179: mbox = (struct MBOX *)
180: Smalloc(z * sizeof(struct MBOX));
181:
182: effnrstates = (int *)
183: Smalloc(n * sizeof(int));
184: }
185:
186: alloc2(n, m, p, who)
187: { char x;
188: if (qoverride && p > QMAX)
189: x = QMAX;
190: else
191: x = p;
192:
193: if (x >= 256)
194: whoops("illegal queue size");
195: if (x >= 16)
196: fprintf(stderr, "warning, very large qsize (%d), queue %d\n", x, n);
197:
198: mbox[n].limit = x;
199: if (who >= 0)
200: mbox[n].owner = who;
201: else
202: mbox[n].owner = 0;
203: }
204:
205: alloc3(n)
206: { inits = (int *)
207: Smalloc(n * sizeof(int));
208: }
209:
210: alloc4(n)
211: { if (assertbl == NONE && errortbl == NONE)
212: globvars = (int *)
213: Smalloc(n * sizeof(int));
214: else
215: globvars = (int *)
216: Emalloc(n * sizeof(int));
217: }
218:
219: alloc45(n)
220: { register int i;
221: fullname = (struct MNAME *)
222: Smalloc(n * sizeof(struct MNAME));
223: xob = (int *)
224: Smalloc((n+msgbase) * sizeof(int));
225: for (i = 0; i < n+msgbase; i++)
226: xob[i] = -1;
227: }
228:
229: alloc5(n)
230: { register int i, j, r, c;
231:
232:
233: r = tbl[n].nrrows;
234: if ((c = tbl[n].nrcols) > maxcol)
235: maxcol = c;
236:
237: tbl[n].endrow = (int *)
238: Smalloc(r * sizeof(int));
239: tbl[n].deadrow = (int *)
240: Smalloc(r * sizeof(int));
241: tbl[n].badrow = (int *)
242: Smalloc(r * sizeof(int));
243: tbl[n].labrow = (int *)
244: Smalloc(r * sizeof(int));
245: tbl[n].colmap = (int *)
246: Smalloc(c * sizeof(int));
247: tbl[n].colorg = (int *)
248: Smalloc(c * sizeof(int));
249:
250: tbl[n].coltyp = (int *)
251: Smalloc(c * sizeof(int));
252: tbl[n].ptr = (struct IND **)
253: Smalloc(r * sizeof(struct IND *));
254:
255: for (i = 0; i < r; i++)
256: { tbl[n].ptr[i] = (struct IND *)
257: Smalloc(c * sizeof(struct IND));
258:
259: for (j = 0; j < c; j++)
260: tbl[n].ptr[i][j].nrpils = 0;
261: tbl[n].deadrow[i] = 1;
262: tbl[n].endrow[i] = tbl[n].badrow[i] = 0;
263: tbl[n].labrow[i] = 0;
264: }
265: tbl[n].labrow[0] = 1; /* make sure initial state is always checked */
266: }
267:
268: alloc6(n, m, p, q)
269: { tbl[n].ptr[m][p].one = (struct ELM *)
270: Smalloc(q * sizeof(struct ELM));
271: }
272:
273: alloc8(pr, p, q)
274: {
275: tablpars[pr].nrms = (short) p; /* available */
276: tablpars[pr].nrvs = (short) q;
277:
278: procpars[pr].ms = (short *)
279: Emalloc(p * sizeof(short));
280: procpars[pr].vs = (short *)
281: Emalloc(q * sizeof(short));
282:
283: procpars[pr].nrms = 0; /* actually used */
284: procpars[pr].nrvs = 0;
285: }
286:
287: alloc9(in, p)
288: {
289: tbl[in].calls = (struct CPARS *)
290: Smalloc(p * sizeof(struct CPARS));
291: }
292:
293: alloc10(in, cn, p, q, r)
294: {
295: tbl[in].calls[cn].callwhat = (short) p;
296: tbl[in].calls[cn].nrms = (short) q;
297: tbl[in].calls[cn].nrvs = (short) r;
298:
299: tbl[in].calls[cn].ms = (short *)
300: Smalloc(q * sizeof (short));
301:
302: tbl[in].calls[cn].vs = (short *)
303: Smalloc(r * sizeof (short));
304: }
305:
306: whoops(s)
307: char *s;
308: {
309: fprintf(stderr, "trace: %s\n", s);
310: output("in sequence: ", 0);
311: postlude();
312: exit(1);
313: }
314:
315: badinput(s)
316: char *s;
317: {
318: fflush(stdout);
319: fprintf(stderr, "trace: bad file `pret.out': %s\n", s);
320: exit(1);
321: }
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.