1 /***** spin: pangen4.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 extern FILE *tc, *tb; 17 extern Queue *qtab; 18 extern Symbol *Fname; 19 extern int lineno, nocast; 20 extern char *R13[], *R14[], *R15[]; 21 22 void 23 undostmnt(Lextok *now, int m) 24 { Lextok *v; 25 int i, j; extern int m_loss; 26 27 if (!now) 28 { fprintf(tb, "0"); 29 return; 30 } 31 lineno = now->ln; 32 Fname = now->fn; 33 switch (now->ntyp) { 34 case CONST: case '!': case UMIN: 35 case '~': case '/': case '*': 36 case '-': case '+': case '%': 37 case LT: case GT: case '&': 38 case '|': case LE: case GE: 39 case NE: case EQ: case OR: 40 case AND: case LSHIFT: case RSHIFT: 41 case TIMEOUT: case LEN: case NAME: 42 case FULL: case EMPTY: case 'R': 43 case NFULL: case NEMPTY: case ENABLED: 44 case '?': case PC_VAL: 45 putstmnt(tb, now, m); 46 break; 47 case RUN: fprintf(tb, "delproc(0, now._nr_pr-1)"); 48 break; 49 case 's': if (m_loss) 50 { fprintf(tb, "if (m == 2) m = unsend"); 51 putname(tb, "(", now->lft, m, ")"); 52 } else 53 { fprintf(tb, "m = unsend"); 54 putname(tb, "(", now->lft, m, ")"); 55 } 56 break; 57 case 'r': for (v = now->rgt, i=j=0; v; v = v->rgt, i++) 58 if (v->lft->ntyp != CONST) 59 j++; 60 fprintf(tb, ";\n"); 61 if (j == 0) 62 { fprintf(tb, "\t\tif (q_flds"); 63 putname(tb, "[((Q0 *)qptr(", now->lft, m, "-1))->_t]"); 64 fprintf(tb, " != %d)\n", i); 65 } else 66 fprintf(tb, "\t\tif (1)\n"); 67 fprintf(tb, "#if defined(FULLSTACK) && defined(NOCOMP)\n"); 68 fprintf(tb, "\t\t sv_restor(!(t->atom&2));\n"); 69 fprintf(tb, "#else\n"); 70 fprintf(tb, "\t\t sv_restor(0);\n"); 71 fprintf(tb, "#endif\n\t\t"); 72 if (j == 0) 73 { fprintf(tb, "else {\n\t\t"); 74 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 75 { fprintf(tb, "\tunrecv"); 76 putname(tb, "(", now->lft, m, ", 0, "); 77 fprintf(tb, "%d, ", i); 78 undostmnt(v->lft, m); 79 fprintf(tb, ", %d);\n\t\t", (i==0)?1:0); 80 } 81 fprintf(tb, "}\n\t\t"); 82 } 83 break; 84 case '@': fprintf(tb, "p_restor(II)"); 85 break; 86 case ASGN: nocast=1; putstmnt(tb,now->lft,m); 87 nocast=0; fprintf(tb, " = trpt->oval"); 88 check_proc(now->rgt, m); 89 break; 90 case 'c': check_proc(now->lft, m); 91 break; 92 case '.': 93 case GOTO: 94 case ELSE: 95 case BREAK: break; 96 case ASSERT: 97 case PRINT: check_proc(now, m); 98 break; 99 default: printf("spin: bad node type %d (.b)\n", 100 now->ntyp); 101 exit(1); 102 } 103 } 104 105 int 106 any_undo(Lextok *now) 107 { /* is there anything to undo on a return move? */ 108 if (!now) return 1; 109 switch (now->ntyp) { 110 case 'c': return any_oper(now->lft, RUN); 111 case ASSERT: 112 case PRINT: return any_oper(now, RUN); 113 114 case '.': 115 case GOTO: 116 case ELSE: 117 case BREAK: return 0; 118 default: return 1; 119 } 120 } 121 122 int 123 any_oper(Lextok *now, int oper) 124 { /* check if an expression contains oper operator */ 125 if (!now) return 0; 126 if (now->ntyp == oper) 127 return 1; 128 return (any_oper(now->lft, oper) || any_oper(now->rgt, oper)); 129 } 130 131 void 132 check_proc(Lextok *now, int m) 133 { 134 if (!now) 135 return; 136 if (now->ntyp == '@' || now->ntyp == RUN) 137 { fprintf(tb, ";\n\t\t"); 138 undostmnt(now, m); 139 } 140 check_proc(now->lft, m); 141 check_proc(now->rgt, m); 142 } 143 144 void 145 genunio(void) 146 { char *buf1; 147 Queue *q; int i; extern int has_sorted; 148 149 buf1 = (char *) emalloc(128); 150 ntimes(tc, 0, 1, R13); 151 for (q = qtab; q; q = q->nxt) 152 { fprintf(tc, "\tcase %d:\n", q->qid); 153 154 if (has_sorted) 155 { sprintf(buf1, "((Q%d *)z)->contents", q->qid); 156 fprintf(tc, "\t\tj = trpt->oval;\n"); 157 fprintf(tc, "\t\tfor (k = j; k < ((Q%d *)z)->Qlen; k++)\n", q->qid); 158 fprintf(tc, "\t\t{\n"); 159 for (i = 0; i < q->nflds; i++) 160 fprintf(tc, "\t\t\t%s[k].fld%d = %s[k+1].fld%d;\n", 161 buf1, i, buf1, i); 162 fprintf(tc, "\t\t}\n"); 163 fprintf(tc, "\t\tj = ((Q0 *)z)->Qlen;\n"); 164 } 165 166 sprintf(buf1, "((Q%d *)z)->contents[j].fld", q->qid); 167 for (i = 0; i < q->nflds; i++) 168 fprintf(tc, "\t\t%s%d = 0;\n", buf1, i); 169 if (q->nslots==0) 170 { /* check if rendezvous succeeded, 1 level down */ 171 fprintf(tc, "\t\tm = (trpt+1)->o_m;\n"); 172 fprintf(tc, "\t\tif (m) trpt->o_pm |= 1;\n"); 173 fprintf(tc, "\t\tUnBlock;\n"); 174 } else 175 fprintf(tc, "\t\tm = trpt->o_m;\n"); 176 fprintf(tc, "\t\tbreak;\n"); 177 } 178 ntimes(tc, 0, 1, R14); 179 for (q = qtab; q; q = q->nxt) 180 { sprintf(buf1, "((Q%d *)z)->contents", q->qid); 181 fprintf(tc, " case %d:\n", q->qid); 182 if (q->nslots == 0) 183 fprintf(tc, "\t\tif (strt) boq = from+1;\n"); 184 else if (q->nslots > 1) /* shift */ 185 { fprintf(tc, "\t\tif (strt && slot<%d)\n", 186 q->nslots-1); 187 fprintf(tc, "\t\t{\tfor (j--; j>=slot; j--)\n"); 188 fprintf(tc, "\t\t\t{"); 189 for (i = 0; i < q->nflds; i++) 190 { fprintf(tc, "\t%s[j+1].fld%d =\n\t\t\t", 191 buf1, i); 192 fprintf(tc, "\t%s[j].fld%d;\n\t\t\t", 193 buf1, i); 194 } 195 fprintf(tc, "}\n\t\t}\n"); 196 } 197 strcat(buf1, "[slot].fld"); 198 fprintf(tc, "\t\tif (strt) {\n"); 199 for (i = 0; i < q->nflds; i++) 200 fprintf(tc, "\t\t\t%s%d = 0;\n", buf1, i); 201 fprintf(tc, "\t\t}\n"); 202 if (q->nflds == 1) /* set */ 203 fprintf(tc, "\t\tif (fld == 0) %s0 = fldvar;\n", 204 buf1); 205 else 206 { fprintf(tc, "\t\tswitch (fld) {\n"); 207 for (i = 0; i < q->nflds; i++) 208 { fprintf(tc, "\t\tcase %d:\t%s", i, buf1); 209 fprintf(tc, "%d = fldvar; break;\n", i); 210 } 211 fprintf(tc, "\t\t}\n"); 212 } 213 fprintf(tc, "\t\tbreak;\n"); 214 } 215 ntimes(tc, 0, 1, R15); 216 } 217