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