1 /***** spin: pangen1.c *****/
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 */
19 extern FILE *tc
, *th
, *tt
;
21 extern Ordered
*all_names
;
25 extern int lineno
, verbose
, Pid
, separate
;
26 extern int nrRdy
, nqs
, mst
, Mpars
, claimnr
, eventmapnr
;
27 extern short has_sorted
, has_random
, has_provided
;
30 int Npars
=0, u_sync
=0, u_async
=0, hastrack
= 1;
32 short has_state
=0; /* code contains c_state */
34 static Symbol
*LstSet
=ZS
;
35 static int acceptors
=0, progressors
=0, nBits
=0;
36 static int Types
[] = { UNSIGNED
, BIT
, BYTE
, CHAN
, MTYPE
, SHORT
, INT
, STRUCT
};
38 static int doglobal(char *, int);
39 static void dohidden(void);
40 static void do_init(FILE *, Symbol
*);
41 static void end_labs(Symbol
*, int);
42 static void put_ptype(char *, int, int, int);
43 static void tc_predef_np(void);
44 static void put_pinit(ProcList
*);
45 void walk_struct(FILE *, int, char *, Symbol
*, char *, char *, char *);
48 reverse_names(ProcList
*p
)
51 reverse_names(p
->nxt
);
52 fprintf(th
, " \"%s\",\n", p
->n
->name
);
64 fprintf(th
, "#define SYNC %d\n", u_sync
);
65 fprintf(th
, "#define ASYNC %d\n\n", u_async
);
66 fprintf(th
, "#ifndef NCORE\n");
67 fprintf(th
, " #ifdef DUAL_CORE\n");
68 fprintf(th
, " #define NCORE 2\n");
69 fprintf(th
, " #elif QUAD_CORE\n");
70 fprintf(th
, " #define NCORE 4\n");
71 fprintf(th
, " #else\n");
72 fprintf(th
, " #define NCORE 1\n");
73 fprintf(th
, " #endif\n");
74 fprintf(th
, "#endif\n");
78 fprintf(tc
, "short Air[] = { ");
79 for (p
= rdy
, i
=0; p
; p
= p
->nxt
, i
++)
80 fprintf(tc
, "%s (short) Air%d", (p
!=rdy
)?",":"", i
);
81 fprintf(tc
, ", (short) Air%d", i
); /* np_ */
84 fprintf(th
, "char *procname[] = {\n");
86 fprintf(th
, " \":np_:\",\n");
87 fprintf(th
, "};\n\n");
90 for (p
= rdy
; p
; p
= p
->nxt
)
91 put_ptype(p
->n
->name
, p
->tn
, mst
, nrRdy
+1);
93 put_ptype("np_", nrRdy
, mst
, nrRdy
+1);
95 ntimes(th
, 0, 1, Head0
);
98 { extern void c_add_stack(FILE *);
99 extern void c_stack_size(FILE *);
101 ntimes(th
, 0, 1, Header
);
102 fprintf(th
, "#define StackSize (");
107 ntimes(th
, 0, 1, Header0
);
109 ntimes(th
, 0, 1, Head1
);
112 (void) doglobal("", PUTV
);
114 hastrack
= c_add_sv(th
);
116 fprintf(th
, " uchar sv[VECTORSZ];\n");
117 fprintf(th
, "} State");
119 fprintf(th
,"\n#ifdef GCC\n");
120 fprintf(th
, "\t__attribute__ ((aligned(8)))");
121 fprintf(th
, "\n#endif\n\t");
123 fprintf(th
, ";\n\n");
125 fprintf(th
, "#define HAS_TRACK %d\n", hastrack
);
136 if (separate
==2) goto shortcut
;
138 fprintf(tc
, "int\naddproc(int n");
139 for (/* i = 0 */; i
< Npars
; i
++)
140 fprintf(tc
, ", int par%d", i
);
142 ntimes(tc
, 0, 1, Addp0
);
143 ntimes(tc
, 1, nrRdy
+1, R5
); /* +1 for np_ */
144 ntimes(tc
, 0, 1, Addp1
);
147 { fprintf(tt
, "\nint\nprovided(int II, unsigned char ot, ");
148 fprintf(tt
, "int tt, Trans *t)\n");
149 fprintf(tt
, "{\n\tswitch(ot) {\n");
153 for (p
= rdy
; p
; p
= p
->nxt
)
157 if (separate
== 2) return;
161 { fprintf(tt
, "\tdefault: return 1; /* e.g., a claim */\n");
162 fprintf(tt
, "\t}\n\treturn 0;\n}\n");
165 ntimes(tc
, i
, i
+1, R6
);
167 ntimes(tc
, 1, nrRdy
+1, R5
); /* +1 for np_ */
169 ntimes(tc
, 1, nrRdy
, R5
);
170 ntimes(tc
, 0, 1, R8a
);
174 do_locinits(FILE *fd
)
177 for (p
= rdy
; p
; p
= p
->nxt
)
178 c_add_locinit(fd
, p
->tn
, p
->n
->name
);
188 ntimes(tc
, claimnr
, claimnr
+1, R0
); /* claim only */
191 ntimes(tc
, 0, 1, Code0
);
192 ntimes(tc
, 0, claimnr
, R0
); /* all except claim */
193 ntimes(tc
, claimnr
+1, nrRdy
, R0
);
196 ntimes(tc
, 0, 1, Code0
);
197 ntimes(tc
, 0, nrRdy
+1, R0
); /* +1 for np_ */
201 for (p
= rdy
; p
; p
= p
->nxt
)
202 end_labs(p
->n
, p
->tn
);
207 ntimes(tc
, claimnr
, claimnr
+1, R0a
); /* claim only */
210 ntimes(tc
, 0, claimnr
, R0a
); /* all except claim */
211 ntimes(tc
, claimnr
+1, nrRdy
, R0a
);
212 fprintf(tc
, " if (state_tables)\n");
213 fprintf(tc
, " ini_claim(%d, 0);\n", claimnr
);
216 ntimes(tc
, 0, nrRdy
, R0a
); /* all */
220 ntimes(tc
, 0, 1, R0b
);
221 if (separate
== 1 && acceptors
== 0)
222 acceptors
= 1; /* assume at least 1 acceptstate */
223 ntimes(th
, acceptors
, acceptors
+1, Code1
);
224 ntimes(th
, progressors
, progressors
+1, Code3
);
225 ntimes(th
, nrRdy
+1, nrRdy
+2, R2
); /* +1 for np_ */
227 fprintf(tc
, " iniglobals();\n");
228 ntimes(tc
, 0, 1, Code2a
);
229 ntimes(tc
, 0, 1, Code2b
); /* bfs option */
230 ntimes(tc
, 0, 1, Code2c
);
231 ntimes(tc
, 0, 1, Code2d
);
232 ntimes(tc
, 0, nrRdy
, R4
);
233 fprintf(tc
, "}\n\n");
235 fprintf(tc
, "void\n");
236 fprintf(tc
, "iniglobals(void)\n{\n");
237 if (doglobal("", INIV
) > 0)
238 { fprintf(tc
, "#ifdef VAR_RANGES\n");
239 (void) doglobal("logval(\"", LOGV
);
240 fprintf(tc
, "#endif\n");
242 ntimes(tc
, 1, nqs
+1, R3
);
243 fprintf(tc
, "\tMaxbody = max(Maxbody, sizeof(State)-VECTORSZ);");
244 fprintf(tc
, "\n}\n\n");
250 ntimes(tc
, 0, 1, SvMap
);
254 char *s
, *t
; int n
, m
, p
;
256 {"end", "stopstate", 3, 0, 0},
257 {"progress", "progstate", 8, 0, 1},
258 {"accept", "accpstate", 6, 1, 0},
263 end_labs(Symbol
*s
, int i
)
267 int j
; char foo
[128];
269 if ((i
== claimnr
&& separate
== 1)
270 || (i
!= claimnr
&& separate
== 2))
273 for (l
= labtab
; l
; l
= l
->nxt
)
274 for (j
= 0; ln
[j
].n
; j
++)
275 if (strncmp(l
->s
->name
, ln
[j
].s
, ln
[j
].n
) == 0
276 && strcmp(l
->c
->name
, s
->name
) == 0)
277 { fprintf(tc
, "\t%s[%d][%d] = 1;\n",
278 ln
[j
].t
, i
, l
->e
->seqno
);
279 acceptors
+= ln
[j
].m
;
280 progressors
+= ln
[j
].p
;
281 if (l
->e
->status
& D_ATOM
)
282 { sprintf(foo
, "%s label inside d_step",
286 if (j
> 0 && (l
->e
->status
& ATOM
))
287 { sprintf(foo
, "%s label inside atomic",
289 complain
: lineno
= l
->e
->n
->ln
;
291 printf("spin: %3d:%s, warning, %s - is invisible\n",
292 lineno
, Fname
?Fname
->name
:"-", foo
);
295 /* visible states -- through remote refs: */
296 for (l
= labtab
; l
; l
= l
->nxt
)
298 && strcmp(l
->s
->context
->name
, s
->name
) == 0)
299 fprintf(tc
, "\tvisstate[%d][%d] = 1;\n",
307 ntimes(FILE *fd
, int n
, int m
, char *c
[])
310 for (j
= 0; c
[j
]; j
++)
311 for (i
= n
; i
< m
; i
++)
312 { fprintf(fd
, c
[j
], i
, i
, i
, i
, i
, i
);
321 printf("spin: warning, ");
324 n
= (s
->context
!= ZS
)?s
->context
->ini
:s
->ini
;
326 printf("line %3d %s, ", n
->ln
, n
->fn
->name
);
330 checktype(Symbol
*sp
, char *s
)
331 { char buf
[128]; int i
;
339 if (sp
->hidden
&16) /* formal parameter */
340 { ProcList
*p
; Lextok
*f
, *t
;
342 for (p
= rdy
; p
; p
= p
->nxt
)
344 && strcmp(s
, p
->n
->name
) == 0)
347 for (f
= p
->p
; f
; f
= f
->rgt
) /* list of types */
348 for (t
= f
->lft
; t
; t
= t
->rgt
, posnr
++)
350 && strcmp(t
->sym
->name
, sp
->name
) == 0)
351 { checkrun(sp
, posnr
);
355 } else if (!(sp
->hidden
&4))
356 { if (!(verbose
&32)) return;
357 sputtype(buf
, sp
->type
);
358 i
= (int) strlen(buf
);
359 while (i
> 0 && buf
[--i
] == ' ') buf
[i
] = '\0';
362 printf("proctype %s:", s
);
365 printf(" '%s %s' could be declared 'bit %s'\n",
366 buf
, sp
->name
, sp
->name
);
367 } else if (sp
->type
!= BYTE
&& !(sp
->hidden
&8))
368 { if (!(verbose
&32)) return;
369 sputtype(buf
, sp
->type
);
370 i
= (int) strlen(buf
);
371 while (buf
[--i
] == ' ') buf
[i
] = '\0';
374 printf("proctype %s:", s
);
377 printf(" '%s %s' could be declared 'byte %s'\n",
378 buf
, sp
->name
, sp
->name
);
383 dolocal(FILE *ofd
, char *pre
, int dowhat
, int p
, char *s
)
384 { int h
, j
, k
=0; extern int nr_errs
;
387 char buf
[64], buf2
[128], buf3
[128];
390 { /* initialize in order of declaration */
391 for (walk
= all_names
; walk
; walk
= walk
->next
)
395 && strcmp(s
, sp
->context
->name
) == 0)
396 { checktype(sp
, s
); /* fall through */
397 if (!(sp
->hidden
&16))
398 { sprintf(buf
, "((P%d *)pptr(h))->", p
);
399 do_var(ofd
, dowhat
, buf
, sp
, "", " = ", ";\n");
404 { for (j
= 0; j
< 8; j
++)
405 for (h
= 0; h
<= 1; h
++)
406 for (walk
= all_names
; walk
; walk
= walk
->next
)
410 && sp
->type
== Types
[j
]
411 && ((h
== 0 && sp
->nel
== 1) || (h
== 1 && sp
->nel
> 1))
412 && strcmp(s
, sp
->context
->name
) == 0)
418 sprintf(buf
, "%s%s:", pre
, s
);
419 { sprintf(buf2
, "\", ((P%d *)pptr(h))->", p
);
420 sprintf(buf3
, ");\n");
422 do_var(ofd
, dowhat
, "", sp
, buf
, buf2
, buf3
);
425 sprintf(buf
, "((P%d *)pptr(h))->", p
);
426 do_var(ofd
, dowhat
, buf
, sp
, "", " = ", ";\n");
430 if (strcmp(s
, ":never:") == 0)
431 { printf("error: %s defines local %s\n",
446 { fprintf(fd
, "void\nc_chandump(int unused) ");
447 fprintf(fd
, "{ unused++; /* avoid complaints */ }\n");
451 fprintf(fd
, "void\nc_chandump(int from)\n");
452 fprintf(fd
, "{ uchar *z; int slot;\n");
454 fprintf(fd
, " from--;\n");
455 fprintf(fd
, " if (from >= (int) now._nr_qs || from < 0)\n");
456 fprintf(fd
, " { printf(\"pan: bad qid %%d\\n\", from+1);\n");
457 fprintf(fd
, " return;\n");
459 fprintf(fd
, " z = qptr(from);\n");
460 fprintf(fd
, " switch (((Q0 *)z)->_t) {\n");
462 for (q
= qtab
; q
; q
= q
->nxt
)
463 { fprintf(fd
, " case %d:\n\t\t", q
->qid
);
464 sprintf(buf
, "((Q%d *)z)->", q
->qid
);
466 fprintf(fd
, "for (slot = 0; slot < %sQlen; slot++)\n\t\t", buf
);
467 fprintf(fd
, "{ printf(\" [\");\n\t\t");
468 for (i
= 0; i
< q
->nflds
; i
++)
469 { if (q
->fld_width
[i
] == MTYPE
)
470 { fprintf(fd
, "\tprintm(%scontents[slot].fld%d);\n\t\t",
473 fprintf(fd
, "\tprintf(\"%%d,\", %scontents[slot].fld%d);\n\t\t",
476 fprintf(fd
, " printf(\"],\");\n\t\t");
477 fprintf(fd
, "}\n\t\t");
478 fprintf(fd
, "break;\n");
481 fprintf(fd
, " printf(\"\\n\");\n}\n");
485 c_var(FILE *fd
, char *pref
, Symbol
*sp
)
491 /* c_struct(fd, pref, sp); */
492 fprintf(fd
, "\t\tprintf(\"\t(struct %s)\\n\");\n",
494 sprintf(buf
, "%s%s.", pref
, sp
->name
);
495 c_struct(fd
, buf
, sp
);
498 case SHORT
: case INT
:
500 sputtype(buf
, sp
->type
);
502 { fprintf(fd
, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n",
503 buf
, sp
->name
, pref
, sp
->name
);
505 { fprintf(fd
, "\t{\tint l_in;\n");
506 fprintf(fd
, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp
->nel
);
507 fprintf(fd
, "\t\t{\n");
508 fprintf(fd
, "\t\t\tprintf(\"\t%s %s[%%d]:\t%%d\\n\", l_in, %s%s[l_in]);\n",
509 buf
, sp
->name
, pref
, sp
->name
);
510 fprintf(fd
, "\t\t}\n");
511 fprintf(fd
, "\t}\n");
516 { fprintf(fd
, "\tprintf(\"\tchan %s (=%%d):\tlen %%d:\\t\", ",
518 fprintf(fd
, "%s%s, q_len(%s%s));\n",
519 pref
, sp
->name
, pref
, sp
->name
);
520 fprintf(fd
, "\tc_chandump(%s%s);\n", pref
, sp
->name
);
522 for (i
= 0; i
< sp
->nel
; i
++)
523 { fprintf(fd
, "\tprintf(\"\tchan %s[%d] (=%%d):\tlen %%d:\\t\", ",
525 fprintf(fd
, "%s%s[%d], q_len(%s%s[%d]));\n",
526 pref
, sp
->name
, i
, pref
, sp
->name
, i
);
527 fprintf(fd
, "\tc_chandump(%s%s[%d]);\n",
535 c_splurge_any(ProcList
*p
)
539 if (strcmp(p
->n
->name
, ":never:") != 0
540 && strcmp(p
->n
->name
, ":trace:") != 0
541 && strcmp(p
->n
->name
, ":notrace:") != 0)
542 for (walk
= all_names
; walk
; walk
= walk
->next
)
546 || strcmp(sp
->context
->name
, p
->n
->name
) != 0
547 || sp
->owner
|| (sp
->hidden
&1)
548 || (sp
->type
== MTYPE
&& ismtype(sp
->name
)))
557 c_splurge(FILE *fd
, ProcList
*p
)
562 if (strcmp(p
->n
->name
, ":never:") != 0
563 && strcmp(p
->n
->name
, ":trace:") != 0
564 && strcmp(p
->n
->name
, ":notrace:") != 0)
565 for (walk
= all_names
; walk
; walk
= walk
->next
)
569 || strcmp(sp
->context
->name
, p
->n
->name
) != 0
570 || sp
->owner
|| (sp
->hidden
&1)
571 || (sp
->type
== MTYPE
&& ismtype(sp
->name
)))
574 sprintf(pref
, "((P%d *)pptr(pid))->", p
->tn
);
580 c_wrapper(FILE *fd
) /* allow pan.c to print out global sv entries */
585 extern Lextok
*Mtype
;
588 fprintf(fd
, "void\nc_globals(void)\n{\t/* int i; */\n");
589 fprintf(fd
, " printf(\"global vars:\\n\");\n");
590 for (walk
= all_names
; walk
; walk
= walk
->next
)
592 if (sp
->context
|| sp
->owner
|| (sp
->hidden
&1)
593 || (sp
->type
== MTYPE
&& ismtype(sp
->name
)))
596 c_var(fd
, "now.", sp
);
600 fprintf(fd
, "void\nc_locals(int pid, int tp)\n{\t/* int i; */\n");
601 fprintf(fd
, " switch(tp) {\n");
602 for (p
= rdy
; p
; p
= p
->nxt
)
603 { fprintf(fd
, " case %d:\n", p
->tn
);
604 if (c_splurge_any(p
))
605 { fprintf(fd
, " \tprintf(\"local vars proc %%d (%s):\\n\", pid);\n",
609 { fprintf(fd
, " \t/* none */\n");
611 fprintf(fd
, " \tbreak;\n");
613 fprintf(fd
, " }\n}\n");
615 fprintf(fd
, "void\nprintm(int x)\n{\n");
616 fprintf(fd
, " switch (x) {\n");
617 for (n
= Mtype
, j
= 1; n
&& j
; n
= n
->rgt
, j
++)
618 fprintf(fd
, "\tcase %d: Printf(\"%s\"); break;\n",
619 j
, n
->lft
->sym
->name
);
620 fprintf(fd
, " default: Printf(\"%%d\", x);\n");
626 doglobal(char *pre
, int dowhat
)
631 for (j
= 0; j
< 8; j
++)
632 for (walk
= all_names
; walk
; walk
= walk
->next
)
636 && sp
->type
== Types
[j
])
637 { if (Types
[j
] != MTYPE
|| !ismtype(sp
->name
))
645 do_var(tc
, dowhat
, "", sp
,
646 pre
, "\", now.", ");\n");
649 checktype(sp
, (char *) 0);
650 cnt
++; /* fall through */
652 do_var(tc
, dowhat
, (sp
->hidden
&1)?"":"now.", sp
,
665 for (j
= 0; j
< 8; j
++)
666 for (walk
= all_names
; walk
; walk
= walk
->next
)
669 && sp
->type
== Types
[j
])
670 { if (sp
->context
|| sp
->owner
)
671 fatal("cannot hide non-globals (%s)", sp
->name
);
672 if (sp
->type
== CHAN
)
673 fatal("cannot hide channels (%s)", sp
->name
);
674 fprintf(th
, "/* hidden variable: */");
677 fprintf(th
, "int _; /* a predefined write-only variable */\n\n");
681 do_var(FILE *ofd
, int dowhat
, char *s
, Symbol
*sp
,
682 char *pre
, char *sep
, char *ter
)
688 if (sp
->hidden
&1) break;
694 if (sp
->type
== STRUCT
)
695 { /* struct may contain a chan */
696 walk_struct(ofd
, dowhat
, s
, sp
, pre
, sep
, ter
);
699 if (!sp
->ini
&& dowhat
!= LOGV
) /* it defaults to 0 */
702 { fprintf(ofd
, "\t\t%s%s%s%s",
703 pre
, s
, sp
->name
, sep
);
705 fprintf(ofd
, "%s%s", s
, sp
->name
);
708 fprintf(ofd
, "%s", ter
);
710 { if (sp
->ini
&& sp
->ini
->ntyp
== CHAN
)
711 { for (i
= 0; i
< sp
->nel
; i
++)
712 { fprintf(ofd
, "\t\t%s%s%s[%d]%s",
713 pre
, s
, sp
->name
, i
, sep
);
715 fprintf(ofd
, "%s%s[%d]",
719 fprintf(ofd
, "%s", ter
);
722 { fprintf(ofd
, "\t{\tint l_in;\n");
723 fprintf(ofd
, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp
->nel
);
724 fprintf(ofd
, "\t\t{\n");
725 fprintf(ofd
, "\t\t\t%s%s%s[l_in]%s",
726 pre
, s
, sp
->name
, sep
);
728 fprintf(ofd
, "%s%s[l_in]", s
, sp
->name
);
730 putstmnt(ofd
, sp
->ini
, 0);
731 fprintf(ofd
, "%s", ter
);
732 fprintf(ofd
, "\t\t}\n");
733 fprintf(ofd
, "\t}\n");
740 do_init(FILE *ofd
, Symbol
*sp
)
745 && ((i
= qmake(sp
)) > 0))
746 { if (sp
->ini
->ntyp
== CHAN
)
747 fprintf(ofd
, "addqueue(%d, %d)",
748 i
, ltab
[i
-1]->nslots
== 0);
750 fprintf(ofd
, "%d", i
);
752 putstmnt(ofd
, sp
->ini
, 0);
756 blog(int n
) /* for small log2 without rounding problems */
759 while (r
< n
) { m
++; r
*= 2; }
764 put_ptype(char *s
, int i
, int m0
, int m1
)
767 if (strcmp(s
, ":init:") == 0)
768 fprintf(th
, "#define Pinit ((P%d *)this)\n", i
);
770 if (strcmp(s
, ":never:") != 0
771 && strcmp(s
, ":trace:") != 0
772 && strcmp(s
, ":notrace:") != 0
773 && strcmp(s
, ":init:") != 0
774 && strcmp(s
, "_:never_template:_") != 0
775 && strcmp(s
, "np_") != 0)
776 fprintf(th
, "#define P%s ((P%d *)this)\n", s
, i
);
778 fprintf(th
, "typedef struct P%d { /* %s */\n", i
, s
);
779 fprintf(th
, " unsigned _pid : 8; /* 0..255 */\n");
780 fprintf(th
, " unsigned _t : %d; /* proctype */\n", blog(m1
));
781 fprintf(th
, " unsigned _p : %d; /* state */\n", blog(m0
));
783 nBits
= 8 + blog(m1
) + blog(m0
);
784 k
= dolocal(tc
, "", PUTV
, i
, s
); /* includes pars */
788 fprintf(th
, "} P%d;\n", i
);
789 if ((!LstSet
&& k
> 0) || has_state
)
790 fprintf(th
, "#define Air%d 0\n", i
);
791 else if (LstSet
|| k
== 0) /* 5.0, added condition */
792 { fprintf(th
, "#define Air%d (sizeof(P%d) - ", i
, i
);
794 { fprintf(th
, "%d", (nBits
+7)/8);
797 if ((LstSet
->type
!= BIT
&& LstSet
->type
!= UNSIGNED
)
799 { fprintf(th
, "Offsetof(P%d, %s) - %d*sizeof(",
800 i
, LstSet
->name
, LstSet
->nel
);
802 switch(LstSet
->type
) {
804 fprintf(th
, "%d", (nBits
+7)/8);
807 if (LstSet
->nel
== 1)
808 { fprintf(th
, "%d", (nBits
+7)/8);
810 } /* else fall through */
811 case MTYPE
: case BYTE
: case CHAN
:
812 fprintf(th
, "uchar)"); break;
814 fprintf(th
, "short)"); break;
816 fprintf(th
, "int)"); break;
818 fatal("cannot happen Air %s",
821 done
: fprintf(th
, ")\n");
827 { int i
= nrRdy
; /* 1+ highest proctype nr */
829 fprintf(th
, "#define _NP_ %d\n", i
);
830 /* if (separate == 2) fprintf(th, "extern "); */
831 fprintf(th
, "uchar reached%d[3]; /* np_ */\n", i
);
832 fprintf(th
, "uchar *loopstate%d; /* np_ */\n", i
);
834 fprintf(th
, "#define nstates%d 3 /* np_ */\n", i
);
835 fprintf(th
, "#define endstate%d 2 /* np_ */\n\n", i
);
836 fprintf(th
, "#define start%d 0 /* np_ */\n", i
);
838 fprintf(tc
, "\tcase %d: /* np_ */\n", i
);
840 { fprintf(tc
, "\t\tini_claim(%d, h);\n", i
);
842 { fprintf(tc
, "\t\t((P%d *)pptr(h))->_t = %d;\n", i
, i
);
843 fprintf(tc
, "\t\t((P%d *)pptr(h))->_p = 0;\n", i
);
844 fprintf(tc
, "\t\treached%d[0] = 1;\n", i
);
845 fprintf(tc
, "\t\taccpstate[%d][1] = 1;\n", i
);
847 fprintf(tc
, "\t\tbreak;\n");
851 put_pinit(ProcList
*P
)
852 { Lextok
*fp
, *fpt
, *t
;
853 Element
*e
= P
->s
->frst
;
861 { fprintf(tc
, "\tcase %d: /* %s */\n", i
, s
->name
);
862 fprintf(tc
, "\t\tini_claim(%d, h);\n", i
);
863 fprintf(tc
, "\t\tbreak;\n");
870 ini
= huntele(e
, e
->status
, -1)->seqno
;
871 fprintf(th
, "#define start%d %d\n", i
, ini
);
873 fprintf(th
, "#define start_claim %d\n", ini
);
875 fprintf(th
, "#define start_event %d\n", ini
);
877 fprintf(tc
, "\tcase %d: /* %s */\n", i
, s
->name
);
879 fprintf(tc
, "\t\t((P%d *)pptr(h))->_t = %d;\n", i
, i
);
880 fprintf(tc
, "\t\t((P%d *)pptr(h))->_p = %d;", i
, ini
);
881 fprintf(tc
, " reached%d[%d]=1;\n", i
, ini
);
884 { fprintf(tt
, "\tcase %d: /* %s */\n\t\t", i
, s
->name
);
886 { fprintf(tt
, "if (");
887 putstmnt(tt
, P
->prov
, 0);
888 fprintf(tt
, ")\n\t\t\t");
890 fprintf(tt
, "return 1;\n");
892 fprintf(tt
, "\t\tbreak;\n");
895 fprintf(tc
, "\t\t/* params: */\n");
896 for (fp
= p
, j
=0; fp
; fp
= fp
->rgt
)
897 for (fpt
= fp
->lft
; fpt
; fpt
= fpt
->rgt
, j
++)
898 { t
= (fpt
->ntyp
== ',') ? fpt
->lft
: fpt
;
899 if (t
->sym
->nel
!= 1)
902 fatal("array in parameter list, %s",
905 fprintf(tc
, "\t\t((P%d *)pptr(h))->", i
);
906 if (t
->sym
->type
== STRUCT
)
907 { if (full_name(tc
, t
, t
->sym
, 1))
910 fatal("hidden array in parameter %s",
914 fprintf(tc
, "%s", t
->sym
->name
);
915 fprintf(tc
, " = par%d;\n", j
);
917 fprintf(tc
, "\t\t/* locals: */\n");
918 k
= dolocal(tc
, "", INIV
, i
, s
->name
);
920 { fprintf(tc
, "#ifdef VAR_RANGES\n");
921 (void) dolocal(tc
, "logval(\"", LOGV
, i
, s
->name
);
922 fprintf(tc
, "#endif\n");
925 fprintf(tc
, "#ifdef HAS_CODE\n");
926 fprintf(tc
, "\t\tlocinit%d(h);\n", i
);
927 fprintf(tc
, "#endif\n");
929 dumpclaims(tc
, i
, s
->name
);
930 fprintf(tc
, "\t break;\n");
934 huntstart(Element
*f
)
936 Element
*elast
= (Element
*) 0;
939 while (elast
!= e
&& cnt
++ < 200) /* new 4.0.8 */
942 { if (e
->n
->ntyp
== '.' && e
->nxt
)
944 else if (e
->n
->ntyp
== UNLESS
)
945 e
= e
->sub
->this->frst
;
948 if (cnt
>= 200 || !e
)
949 fatal("confusing control structure", (char *) 0);
954 huntele(Element
*f
, int o
, int stopat
)
955 { Element
*g
, *e
= f
;
956 int cnt
=0; /* a precaution against loops */
959 for ( ; cnt
< 200 && e
->n
; cnt
++)
961 if (e
->seqno
== stopat
)
964 switch (e
->n
->ntyp
) {
967 cross_dsteps(e
->n
, g
->n
);
976 g
= huntele(e
->sub
->this->frst
, o
, stopat
);
984 if ((o
& ATOM
) && !(g
->status
& ATOM
))
988 if (cnt
>= 200 || !e
)
989 fatal("confusing control structure", (char *) 0);
995 { int wsbits
= sizeof(long)*8; /* wordsize in bits */
999 fprintf(th
, "\tuchar %s;", sp
->name
);
1001 fprintf(th
, "\tunsigned %s : %d",
1002 sp
->name
, sp
->nbits
);
1004 if (nBits
%wsbits
> 0
1005 && wsbits
- nBits
%wsbits
< sp
->nbits
)
1006 { /* must padd to a word-boundary */
1007 nBits
+= wsbits
- nBits
%wsbits
;
1012 if (sp
->nel
== 1 && !(sp
->hidden
&1))
1013 { fprintf(th
, "\tunsigned %s : 1", sp
->name
);
1017 } /* else fall through */
1018 if (!(sp
->hidden
&1) && (verbose
&32))
1019 printf("spin: warning: bit-array %s[%d] mapped to byte-array\n",
1021 nBits
+= 8*sp
->nel
; /* mapped onto array of uchars */
1024 case CHAN
: /* good for up to 255 channels */
1025 fprintf(th
, "\tuchar %s", sp
->name
);
1029 fprintf(th
, "\tshort %s", sp
->name
);
1033 fprintf(th
, "\tint %s", sp
->name
);
1038 fatal("undeclared structure element %s", sp
->name
);
1039 fprintf(th
, "\tstruct %s %s",
1048 fatal("variable %s undeclared", sp
->name
);
1052 fprintf(th
, "[%d]", sp
->nel
);
1057 ncases(FILE *fd
, int p
, int n
, int m
, char *c
[])
1060 for (j
= 0; c
[j
]; j
++)
1061 for (i
= n
; i
< m
; i
++)
1062 { fprintf(fd
, c
[j
], i
, p
, i
);
1072 fprintf(th
, "uchar");
1073 else if (qmax
< 65535)
1074 fprintf(th
, "ushort");
1076 fprintf(th
, "uint");
1077 fprintf(th
, " Qlen; /* q_size */\n");
1086 ntimes(tc
, 0, 1, Addq0
);
1088 fprintf(th
, "#define NQS 1 /* nqs=%d, but has_io */\n", nqs
);
1090 fprintf(th
, "#define NQS %d\n", nqs
);
1091 fprintf(th
, "short q_flds[%d];\n", nqs
+1);
1092 fprintf(th
, "short q_max[%d];\n", nqs
+1);
1094 for (q
= qtab
; q
; q
= q
->nxt
)
1095 if (q
->nslots
> qmax
)
1098 for (q
= qtab
; q
; q
= q
->nxt
)
1100 fprintf(tc
, "\tcase %d: j = sizeof(Q%d);", j
, j
);
1101 fprintf(tc
, " q_flds[%d] = %d;", j
, q
->nflds
);
1102 fprintf(tc
, " q_max[%d] = %d;", j
, max(1,q
->nslots
));
1103 fprintf(tc
, " break;\n");
1105 fprintf(th
, "typedef struct Q%d {\n", j
);
1106 qlen_type(qmax
); /* 4.2.2 */
1107 fprintf(th
, " uchar _t; /* q_type */\n");
1108 fprintf(th
, " struct {\n");
1110 for (j
= 0; j
< q
->nflds
; j
++)
1111 { switch (q
->fld_width
[j
]) {
1114 { fprintf(th
, "\t\tunsigned");
1115 fprintf(th
, " fld%d : 1;\n", j
);
1117 } /* else fall through: smaller struct */
1121 fprintf(th
, "\t\tuchar fld%d;\n", j
);
1124 fprintf(th
, "\t\tshort fld%d;\n", j
);
1127 fprintf(th
, "\t\tint fld%d;\n", j
);
1130 fatal("bad channel spec", "");
1133 fprintf(th
, " } contents[%d];\n", max(1, q
->nslots
));
1134 fprintf(th
, "} Q%d;\n", q
->qid
);
1137 fprintf(th
, "typedef struct Q0 {\t/* generic q */\n");
1138 qlen_type(qmax
); /* 4.2.2 */
1139 fprintf(th
, " uchar _t;\n");
1140 fprintf(th
, "} Q0;\n");
1142 ntimes(tc
, 0, 1, Addq1
);
1145 { fprintf(th
, "int Q_has(int");
1146 for (j
= 0; j
< Mpars
; j
++)
1147 fprintf(th
, ", int, int");
1148 fprintf(th
, ");\n");
1150 fprintf(tc
, "int\nQ_has(int into");
1151 for (j
= 0; j
< Mpars
; j
++)
1152 fprintf(tc
, ", int want%d, int fld%d", j
, j
);
1154 fprintf(tc
, "{ int i;\n\n");
1155 fprintf(tc
, " if (!into--)\n");
1156 fprintf(tc
, " uerror(\"ref to unknown chan ");
1157 fprintf(tc
, "(recv-poll)\");\n\n");
1158 fprintf(tc
, " if (into >= now._nr_qs || into < 0)\n");
1159 fprintf(tc
, " Uerror(\"qrecv bad queue#\");\n\n");
1160 fprintf(tc
, " for (i = 0; i < ((Q0 *)qptr(into))->Qlen;");
1161 fprintf(tc
, " i++)\n");
1162 fprintf(tc
, " {\n");
1163 for (j
= 0; j
< Mpars
; j
++)
1164 { fprintf(tc
, " if (want%d && ", j
);
1165 fprintf(tc
, "qrecv(into+1, i, %d, 0) != fld%d)\n",
1167 fprintf(tc
, " continue;\n");
1169 fprintf(tc
, " return i+1;\n");
1170 fprintf(tc
, " }\n");
1171 fprintf(tc
, " return 0;\n");
1175 fprintf(tc
, "#if NQS>0\n");
1176 fprintf(tc
, "void\nqsend(int into, int sorted");
1177 for (j
= 0; j
< Mpars
; j
++)
1178 fprintf(tc
, ", int fld%d", j
);
1179 fprintf(tc
, ", int args_given)\n");
1180 ntimes(tc
, 0, 1, Addq11
);
1182 for (q
= qtab
; q
; q
= q
->nxt
)
1183 { sprintf(buf0
, "((Q%d *)z)->", q
->qid
);
1184 fprintf(tc
, "\tcase %d:%s\n", q
->qid
,
1185 (q
->nslots
)?"":" /* =rv= */");
1186 if (q
->nslots
== 0) /* reset handshake point */
1187 fprintf(tc
, "\t\t(trpt+2)->o_m = 0;\n");
1190 { fprintf(tc
, "\t\tif (!sorted) goto append%d;\n", q
->qid
);
1191 fprintf(tc
, "\t\tfor (j = 0; j < %sQlen; j++)\n", buf0
);
1192 fprintf(tc
, "\t\t{\t/* find insertion point */\n");
1193 sprintf(buf0
, "((Q%d *)z)->contents[j].fld", q
->qid
);
1194 for (j
= 0; j
< q
->nflds
; j
++)
1195 { fprintf(tc
, "\t\t\tif (fld%d > %s%d) continue;\n",
1197 fprintf(tc
, "\t\t\tif (fld%d < %s%d) ", j
, buf0
, j
);
1198 fprintf(tc
, "goto found%d;\n\n", q
->qid
);
1200 fprintf(tc
, "\t\t}\n");
1201 fprintf(tc
, "\tfound%d:\n", q
->qid
);
1202 sprintf(buf0
, "((Q%d *)z)->", q
->qid
);
1203 fprintf(tc
, "\t\tfor (k = %sQlen - 1; k >= j; k--)\n", buf0
);
1204 fprintf(tc
, "\t\t{\t/* shift up */\n");
1205 for (j
= 0; j
< q
->nflds
; j
++)
1206 { fprintf(tc
, "\t\t\t%scontents[k+1].fld%d = ",
1208 fprintf(tc
, "%scontents[k].fld%d;\n",
1211 fprintf(tc
, "\t\t}\n");
1212 fprintf(tc
, "\tappend%d:\t/* insert in slot j */\n", q
->qid
);
1215 fprintf(tc
, "#ifdef HAS_SORTED\n");
1216 fprintf(tc
, "\t\t(trpt+1)->ipt = j;\n"); /* ipt was bup.oval */
1217 fprintf(tc
, "#endif\n");
1218 fprintf(tc
, "\t\t%sQlen = %sQlen + 1;\n", buf0
, buf0
);
1219 sprintf(buf0
, "((Q%d *)z)->contents[j].fld", q
->qid
);
1220 for (j
= 0; j
< q
->nflds
; j
++)
1221 fprintf(tc
, "\t\t%s%d = fld%d;\n", buf0
, j
, j
);
1222 fprintf(tc
, "\t\tif (args_given != %d)\n", q
->nflds
);
1223 fprintf(tc
, "\t\t{ if (args_given > %d)\n", q
->nflds
);
1224 fprintf(tc
, "\t\t uerror(\"too many parameters in send stmnt\");\n");
1225 fprintf(tc
, "\t\t else\n");
1226 fprintf(tc
, "\t\t uerror(\"too few parameters in send stmnt\");\n");
1227 fprintf(tc
, "\t\t}\n");
1228 fprintf(tc
, "\t\tbreak;\n");
1230 ntimes(tc
, 0, 1, Addq2
);
1232 for (q
= qtab
; q
; q
= q
->nxt
)
1233 fprintf(tc
, "\tcase %d: return %d;\n", q
->qid
, (!q
->nslots
));
1235 ntimes(tc
, 0, 1, Addq3
);
1237 for (q
= qtab
; q
; q
= q
->nxt
)
1238 fprintf(tc
, "\tcase %d: return (q_sz(from) == %d);\n",
1239 q
->qid
, max(1, q
->nslots
));
1241 ntimes(tc
, 0, 1, Addq4
);
1242 for (q
= qtab
; q
; q
= q
->nxt
)
1243 { sprintf(buf0
, "((Q%d *)z)->", q
->qid
);
1244 fprintf(tc
, " case %d:%s\n\t\t",
1245 q
->qid
, (q
->nslots
)?"":" /* =rv= */");
1247 { fprintf(tc
, "if (fld == 0) r = %s", buf0
);
1248 fprintf(tc
, "contents[slot].fld0;\n");
1250 { fprintf(tc
, "switch (fld) {\n");
1251 ncases(tc
, q
->qid
, 0, q
->nflds
, R12
);
1252 fprintf(tc
, "\t\tdefault: Uerror");
1253 fprintf(tc
, "(\"too many fields in recv\");\n");
1254 fprintf(tc
, "\t\t}\n");
1256 fprintf(tc
, "\t\tif (done)\n");
1258 { fprintf(tc
, "\t\t{ j = %sQlen - 1;\n", buf0
);
1259 fprintf(tc
, "\t\t %sQlen = 0;\n", buf0
);
1260 sprintf(buf0
, "\t\t\t((Q%d *)z)->contents", q
->qid
);
1262 { fprintf(tc
, "\t\t{ j = %sQlen;\n", buf0
);
1263 fprintf(tc
, "\t\t %sQlen = --j;\n", buf0
);
1264 fprintf(tc
, "\t\t for (k=slot; k<j; k++)\n");
1265 fprintf(tc
, "\t\t {\n");
1266 sprintf(buf0
, "\t\t\t((Q%d *)z)->contents", q
->qid
);
1267 for (j
= 0; j
< q
->nflds
; j
++)
1268 { fprintf(tc
, "\t%s[k].fld%d = \n", buf0
, j
);
1269 fprintf(tc
, "\t\t%s[k+1].fld%d;\n", buf0
, j
);
1271 fprintf(tc
, "\t\t }\n");
1274 for (j
= 0; j
< q
->nflds
; j
++)
1275 fprintf(tc
, "%s[j].fld%d = 0;\n", buf0
, j
);
1276 fprintf(tc
, "\t\t\tif (fld+1 != %d)\n\t\t\t", q
->nflds
);
1277 fprintf(tc
, "\tuerror(\"missing pars in receive\");\n");
1278 /* incompletely received msgs cannot be unrecv'ed */
1279 fprintf(tc
, "\t\t}\n");
1280 fprintf(tc
, "\t\tbreak;\n");
1282 ntimes(tc
, 0, 1, Addq5
);
1283 for (q
= qtab
; q
; q
= q
->nxt
)
1284 fprintf(tc
, " case %d: j = sizeof(Q%d); break;\n",
1286 ntimes(tc
, 0, 1, R8b
);
1288 ntimes(th
, 0, 1, Proto
); /* tag on function prototypes */
1289 fprintf(th
, "void qsend(int, int");
1290 for (j
= 0; j
< Mpars
; j
++)
1291 fprintf(th
, ", int");
1292 fprintf(th
, ", int);\n");
1294 fprintf(th
, "#define Addproc(x) addproc(x");
1295 for (j
= 0; j
< Npars
; j
++)
This page took 0.065057 seconds and 4 git commands to generate.