1 /***** spin: reprosrc.c *****/
2
3 /*
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
7 */
8
9 #include <stdio.h>
10 #include <assert.h>
11 #include "spin.h"
12 #include "y.tab.h"
13
14 static int indent = 1;
15
16 extern YYSTYPE yylval;
17 extern ProcList *ready;
18 static void repro_seq(Sequence *);
19
20 void
doindent(void)21 doindent(void)
22 { int i;
23 for (i = 0; i < indent; i++)
24 printf(" ");
25 }
26
27 void
repro_sub(Element * e)28 repro_sub(Element *e)
29 {
30 doindent();
31 switch (e->n->ntyp) {
32 case D_STEP:
33 printf("d_step {\n");
34 break;
35 case ATOMIC:
36 printf("atomic {\n");
37 break;
38 case NON_ATOMIC:
39 printf(" {\n");
40 break;
41 }
42 indent++;
43 repro_seq(e->n->sl->this);
44 indent--;
45
46 doindent();
47 printf(" };\n");
48 }
49
50 static void
repro_seq(Sequence * s)51 repro_seq(Sequence *s)
52 { Element *e;
53 Symbol *v;
54 SeqList *h;
55
56 for (e = s->frst; e; e = e->nxt)
57 {
58 v = has_lab(e, 0);
59 if (v) printf("%s:\n", v->name);
60
61 if (e->n->ntyp == UNLESS)
62 { printf("/* normal */ {\n");
63 repro_seq(e->n->sl->this);
64 doindent();
65 printf("} unless {\n");
66 repro_seq(e->n->sl->nxt->this);
67 doindent();
68 printf("}; /* end unless */\n");
69 } else if (e->sub)
70 {
71 switch (e->n->ntyp) {
72 case DO: doindent(); printf("do\n"); indent++; break;
73 case IF: doindent(); printf("if\n"); indent++; break;
74 }
75
76 for (h = e->sub; h; h = h->nxt)
77 { indent--; doindent(); indent++; printf("::\n");
78 repro_seq(h->this);
79 printf("\n");
80 }
81
82 switch (e->n->ntyp) {
83 case DO: indent--; doindent(); printf("od;\n"); break;
84 case IF: indent--; doindent(); printf("fi;\n"); break;
85 }
86 } else
87 { if (e->n->ntyp == ATOMIC
88 || e->n->ntyp == D_STEP
89 || e->n->ntyp == NON_ATOMIC)
90 repro_sub(e);
91 else if (e->n->ntyp != '.'
92 && e->n->ntyp != '@'
93 && e->n->ntyp != BREAK)
94 {
95 doindent();
96 if (e->n->ntyp == C_CODE)
97 { printf("c_code ");
98 plunk_inline(stdout, e->n->sym->name, 1, 1);
99 } else if (e->n->ntyp == 'c'
100 && e->n->lft->ntyp == C_EXPR)
101 { printf("c_expr { ");
102 plunk_expr(stdout, e->n->lft->sym->name);
103 printf("} ->\n");
104 } else
105 { comment(stdout, e->n, 0);
106 printf(";\n");
107 } }
108 }
109 if (e == s->last)
110 break;
111 }
112 }
113
114 void
repro_proc(ProcList * p)115 repro_proc(ProcList *p)
116 {
117 if (!p) return;
118 if (p->nxt) repro_proc(p->nxt);
119
120 if (p->det) printf("D"); /* deterministic */
121 printf("proctype %s()", p->n->name);
122 if (p->prov)
123 { printf(" provided ");
124 comment(stdout, p->prov, 0);
125 }
126 printf("\n{\n");
127 repro_seq(p->s);
128 printf("}\n");
129 }
130
131 void
repro_src(void)132 repro_src(void)
133 {
134 repro_proc(ready);
135 }
136
137 static int in_decl;
138 static int in_c_decl;
139 static int in_c_code;
140
141 void
blip(int n,char * b)142 blip(int n, char *b)
143 { char mtxt[1024];
144
145 strcpy(mtxt, "");
146
147 switch (n) {
148 default: if (n > 0 && n < 256)
149 sprintf(mtxt, "%c", n);
150 else
151 sprintf(mtxt, "<%d?>", n);
152
153 break;
154 case '(': strcpy(mtxt, "("); in_decl++; break;
155 case ')': strcpy(mtxt, ")"); in_decl--; break;
156 case '{': strcpy(mtxt, "{"); break;
157 case '}': strcpy(mtxt, "}"); break;
158 case '\t': sprintf(mtxt, "\\t"); break;
159 case '\f': sprintf(mtxt, "\\f"); break;
160 case '\n': sprintf(mtxt, "\\n"); break;
161 case '\r': sprintf(mtxt, "\\r"); break;
162 case 'c': sprintf(mtxt, "condition"); break;
163 case 's': sprintf(mtxt, "send"); break;
164 case 'r': sprintf(mtxt, "recv"); break;
165 case 'R': sprintf(mtxt, "recv poll"); break;
166 case '@': sprintf(mtxt, "@"); break;
167 case '?': sprintf(mtxt, "(x->y:z)"); break;
168 case NEXT: sprintf(mtxt, "X"); break;
169 case ALWAYS: sprintf(mtxt, "[]"); break;
170 case EVENTUALLY: sprintf(mtxt, "<>"); break;
171 case IMPLIES: sprintf(mtxt, "->"); break;
172 case EQUIV: sprintf(mtxt, "<->"); break;
173 case UNTIL: sprintf(mtxt, "U"); break;
174 case WEAK_UNTIL: sprintf(mtxt, "W"); break;
175 case IN: sprintf(mtxt, "in"); break;
176 case ACTIVE: sprintf(mtxt, "active"); break;
177 case AND: sprintf(mtxt, "&&"); break;
178 case ARROW: sprintf(mtxt, "->"); break;
179 case ASGN: sprintf(mtxt, "="); break;
180 case ASSERT: sprintf(mtxt, "assert"); break;
181 case ATOMIC: sprintf(mtxt, "atomic"); break;
182 case BREAK: sprintf(mtxt, "break"); break;
183 case C_CODE: sprintf(mtxt, "c_code"); in_c_code++; break;
184 case C_DECL: sprintf(mtxt, "c_decl"); in_c_decl++; break;
185 case C_EXPR: sprintf(mtxt, "c_expr"); break;
186 case C_STATE: sprintf(mtxt, "c_state"); break;
187 case C_TRACK: sprintf(mtxt, "c_track"); break;
188 case CLAIM: sprintf(mtxt, "never"); break;
189 case CONST: sprintf(mtxt, "%d", yylval->val); break;
190 case DECR: sprintf(mtxt, "--"); break;
191 case D_STEP: sprintf(mtxt, "d_step"); break;
192 case D_PROCTYPE: sprintf(mtxt, "d_proctype"); break;
193 case DO: sprintf(mtxt, "do"); break;
194 case DOT: sprintf(mtxt, "."); break;
195 case ELSE: sprintf(mtxt, "else"); break;
196 case EMPTY: sprintf(mtxt, "empty"); break;
197 case ENABLED: sprintf(mtxt, "enabled"); break;
198 case EQ: sprintf(mtxt, "=="); break;
199 case EVAL: sprintf(mtxt, "eval"); break;
200 case FI: sprintf(mtxt, "fi"); break;
201 case FOR: sprintf(mtxt, "for"); break;
202 case FULL: sprintf(mtxt, "full"); break;
203 case GE: sprintf(mtxt, ">="); break;
204 case GET_P: sprintf(mtxt, "get_priority"); break;
205 case GOTO: sprintf(mtxt, "goto"); break;
206 case GT: sprintf(mtxt, ">"); break;
207 case HIDDEN: sprintf(mtxt, "hidden"); break;
208 case IF: sprintf(mtxt, "if"); break;
209 case INCR: sprintf(mtxt, "++"); break;
210
211 case INLINE: sprintf(mtxt, "inline"); break;
212 case INIT: sprintf(mtxt, "init"); break;
213 case ISLOCAL: sprintf(mtxt, "local"); break;
214
215 case LABEL: sprintf(mtxt, "<label-name>"); break;
216
217 case LE: sprintf(mtxt, "<="); break;
218 case LEN: sprintf(mtxt, "len"); break;
219 case LSHIFT: sprintf(mtxt, "<<"); break;
220 case LT: sprintf(mtxt, "<"); break;
221 case LTL: sprintf(mtxt, "ltl"); break;
222
223 case NAME: sprintf(mtxt, "%s", yylval->sym->name); break;
224
225 case XU: switch (yylval->val) {
226 case XR: sprintf(mtxt, "xr"); break;
227 case XS: sprintf(mtxt, "xs"); break;
228 default: sprintf(mtxt, "<?>"); break;
229 }
230 break;
231
232 case TYPE: switch (yylval->val) {
233 case BIT: sprintf(mtxt, "bit"); break;
234 case BYTE: sprintf(mtxt, "byte"); break;
235 case CHAN: sprintf(mtxt, "chan"); in_decl++; break;
236 case INT: sprintf(mtxt, "int"); break;
237 case MTYPE: sprintf(mtxt, "mtype"); break;
238 case SHORT: sprintf(mtxt, "short"); break;
239 case UNSIGNED: sprintf(mtxt, "unsigned"); break;
240 default: sprintf(mtxt, "<unknown type>"); break;
241 }
242 break;
243
244 case NE: sprintf(mtxt, "!="); break;
245 case NEG: sprintf(mtxt, "!"); break;
246 case NEMPTY: sprintf(mtxt, "nempty"); break;
247 case NFULL: sprintf(mtxt, "nfull"); break;
248
249 case NON_ATOMIC: sprintf(mtxt, "<sub-sequence>"); break;
250
251 case NONPROGRESS: sprintf(mtxt, "np_"); break;
252 case OD: sprintf(mtxt, "od"); break;
253 case OF: sprintf(mtxt, "of"); break;
254 case OR: sprintf(mtxt, "||"); break;
255 case O_SND: sprintf(mtxt, "!!"); break;
256 case PC_VAL: sprintf(mtxt, "pc_value"); break;
257 case PRINT: sprintf(mtxt, "printf"); break;
258 case PRINTM: sprintf(mtxt, "printm"); break;
259 case PRIORITY: sprintf(mtxt, "priority"); break;
260 case PROCTYPE: sprintf(mtxt, "proctype"); break;
261 case PROVIDED: sprintf(mtxt, "provided"); break;
262 case RETURN: sprintf(mtxt, "return"); break;
263 case RCV: sprintf(mtxt, "?"); break;
264 case R_RCV: sprintf(mtxt, "??"); break;
265 case RSHIFT: sprintf(mtxt, ">>"); break;
266 case RUN: sprintf(mtxt, "run"); break;
267 case SEP: sprintf(mtxt, "::"); break;
268 case SEMI: sprintf(mtxt, ";"); break;
269 case SET_P: sprintf(mtxt, "set_priority"); break;
270 case SHOW: sprintf(mtxt, "show"); break;
271 case SND: sprintf(mtxt, "!"); break;
272
273 case INAME:
274 case UNAME:
275 case PNAME:
276 case STRING: sprintf(mtxt, "%s", yylval->sym->name); break;
277
278 case TRACE: sprintf(mtxt, "trace"); break;
279 case TIMEOUT: sprintf(mtxt, "(timeout)"); break;
280 case TYPEDEF: sprintf(mtxt, "typedef"); break;
281 case UMIN: sprintf(mtxt, "-"); break;
282 case UNLESS: sprintf(mtxt, "unless"); break;
283 }
284 strcat(b, mtxt);
285 }
286
287 void
purge(char * b)288 purge(char *b)
289 {
290 if (strlen(b) == 0) return;
291
292 if (b[strlen(b)-1] != ':') /* label? */
293 { if (b[0] == ':' && b[1] == ':')
294 { indent--;
295 doindent();
296 indent++;
297 } else
298 { doindent();
299 }
300 }
301 printf("%s\n", b);
302 strcpy(b, "");
303
304 in_decl = 0;
305 in_c_code = 0;
306 in_c_decl = 0;
307 }
308
309 int pp_mode;
310 extern int lex(void);
311
312 void
pretty_print(void)313 pretty_print(void)
314 { int c, lastc = 0;
315 char buf[1024];
316
317 pp_mode = 1;
318 indent = 0;
319 strcpy(buf, "");
320 while ((c = lex()) != EOF)
321 {
322 if ((lastc == IF || lastc == DO) && c != SEP)
323 { indent--; /* c_code if */
324 }
325 if (c == C_DECL || c == C_STATE
326 || c == C_TRACK || c == SEP
327 || c == DO || c == IF
328 || (c == TYPE && !in_decl))
329 { purge(buf); /* start on new line */
330 }
331
332 if (c == '{'
333 && lastc != OF && lastc != IN
334 && lastc != ATOMIC && lastc != D_STEP
335 && lastc != C_CODE && lastc != C_DECL && lastc != C_EXPR)
336 { purge(buf);
337 }
338
339 if (c == PREPROC)
340 { int oi = indent;
341 purge(buf);
342 assert(strlen(yylval->sym->name) < sizeof(buf));
343 strcpy(buf, yylval->sym->name);
344 indent = 0;
345 purge(buf);
346 indent = oi;
347 continue;
348 }
349
350 if (c != ':' && c != SEMI
351 && c != ',' && c != '('
352 && c != '#' && lastc != '#'
353 && c != ARROW && lastc != ARROW
354 && c != '.' && lastc != '.'
355 && c != '!' && lastc != '!'
356 && c != SND && lastc != SND
357 && c != RCV && lastc != RCV
358 && c != O_SND && lastc != O_SND
359 && c != R_RCV && lastc != R_RCV
360 && (c != ']' || lastc != '[')
361 && (c != '>' || lastc != '<')
362 && (c != GT || lastc != LT)
363 && c != '@' && lastc != '@'
364 && (lastc != '(' || c != ')')
365 && (lastc != '/' || c != '/')
366 && c != DO && c != OD && c != IF && c != FI
367 && c != SEP && strlen(buf) > 0)
368 strcat(buf, " ");
369
370 if (c == '}' || c == OD || c == FI)
371 { purge(buf);
372 indent--;
373 }
374 blip(c, buf);
375
376 if (c == '{' || c == DO || c == IF)
377 { purge(buf);
378 indent++;
379 }
380
381 if (c == '}' || c == BREAK || c == SEMI || c == ELSE
382 || (c == ':' && lastc == NAME))
383 { purge(buf);
384 }
385 lastc = c;
386 }
387 purge(buf);
388 }
389