1 /***** spin: pangen3.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 <ctype.h> 15 #include "y.tab.h" 16 17 extern FILE *th; 18 19 typedef struct SRC { 20 short ln, st; 21 struct SRC *nxt; 22 } SRC; 23 24 SRC *frst = (SRC *) 0; 25 SRC *skip = (SRC *) 0; 26 int col; 27 28 extern int claimnr; 29 30 void 31 putskip(int m) /* states that need not be reached */ 32 { SRC *tmp; 33 34 for (tmp = skip; tmp; tmp = tmp->nxt) 35 if (tmp->st == m) 36 return; 37 tmp = (SRC *) emalloc(sizeof(SRC)); 38 tmp->st = (short) m; 39 tmp->nxt = skip; 40 skip = tmp; 41 } 42 43 void 44 unskip(int m) /* a state that needs to be reached after all */ 45 { SRC *tmp, *lst=(SRC *)0; 46 47 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) 48 if (tmp->st == m) 49 { if (tmp == skip) 50 skip = skip->nxt; 51 else 52 lst->nxt = tmp->nxt; 53 break; 54 } 55 } 56 57 void 58 putsrc(int n, int m) /* match states to source lines */ 59 { SRC *tmp; 60 61 for (tmp = frst; tmp; tmp = tmp->nxt) 62 if (tmp->st == m) 63 { if (tmp->ln != n) 64 printf("putsrc mismatch %d - %d\n", n, tmp->ln); 65 return; 66 } 67 tmp = (SRC *) emalloc(sizeof(SRC)); 68 tmp->ln = (short) n; 69 tmp->st = (short) m; 70 tmp->nxt = frst; 71 frst = tmp; 72 } 73 74 void 75 dumpskip(int n, int m) 76 { SRC *tmp, *lst; 77 int j; 78 79 fprintf(th, "uchar reached%d [] = {\n\t", m); 80 for (j = 0, col = 0; j <= n; j++) 81 { lst = (SRC *) 0; 82 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt) 83 if (tmp->st == j) 84 { putnr(1); 85 if (lst) 86 lst->nxt = tmp->nxt; 87 else 88 skip = tmp->nxt; 89 break; 90 } 91 if (!tmp) 92 putnr(0); 93 } 94 fprintf(th, "};\n"); 95 if (m == claimnr) 96 fprintf(th, "#define reached_claim reached%d\n", m); 97 98 skip = (SRC *) 0; 99 } 100 101 void 102 dumpsrc(int n, int m) 103 { SRC *tmp, *lst; 104 int j; 105 106 fprintf(th, "short src_ln%d [] = {\n\t", m); 107 for (j = 0, col = 0; j <= n; j++) 108 { lst = (SRC *) 0; 109 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt) 110 if (tmp->st == j) 111 { putnr(tmp->ln); 112 if (lst) 113 lst->nxt = tmp->nxt; 114 else 115 frst = tmp->nxt; 116 break; 117 } 118 if (!tmp) 119 putnr(0); 120 } 121 fprintf(th, "};\n"); 122 123 if (m == claimnr) 124 fprintf(th, "#define src_claim src_ln%d\n", m); 125 126 frst = (SRC *) 0; 127 dumpskip(n, m); 128 } 129 130 void 131 putnr(int n) 132 { 133 if (col++ == 8) 134 { fprintf(th, "\n\t"); 135 col = 1; 136 } 137 fprintf(th, "%3d, ", n); 138 } 139 140 #define Cat0(x) comwork(fd,now->lft,m); fprintf(fd, x); \ 141 comwork(fd,now->rgt,m) 142 #define Cat1(x) fprintf(fd,"("); Cat0(x); fprintf(fd,")") 143 #define Cat2(x,y) fprintf(fd,x); comwork(fd,y,m) 144 #define Cat3(x,y,z) fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z) 145 146 int 147 symbolic(FILE *fd, Lextok *tv) 148 { Lextok *n; extern Lextok *Mtype; 149 int cnt = 1; 150 151 if (tv->ismtyp) 152 for (n = Mtype; n; n = n->rgt, cnt++) 153 if (cnt == tv->val) 154 { fprintf(fd, "%s", n->lft->sym->name); 155 return 1; 156 } 157 return 0; 158 } 159 160 void 161 comwork(FILE *fd, Lextok *now, int m) 162 { Lextok *v; 163 int i, j; extern int Mpars; 164 165 if (!now) { fprintf(fd, "0"); return; } 166 switch (now->ntyp) { 167 case CONST: fprintf(fd, "%d", now->val); break; 168 case '!': Cat3("!(", now->lft, ")"); break; 169 case UMIN: Cat3("-(", now->lft, ")"); break; 170 case '~': Cat3("~(", now->lft, ")"); break; 171 172 case '/': Cat1("/"); break; 173 case '*': Cat1("*"); break; 174 case '-': Cat1("-"); break; 175 case '+': Cat1("+"); break; 176 case '%': Cat1("%%"); break; 177 case '&': Cat1("&"); break; 178 case '|': Cat1("|"); break; 179 case LE: Cat1("<="); break; 180 case GE: Cat1(">="); break; 181 case GT: Cat1(">"); break; 182 case LT: Cat1("<"); break; 183 case NE: Cat1("!="); break; 184 case EQ: Cat1("=="); break; 185 case OR: Cat1("||"); break; 186 case AND: Cat1("&&"); break; 187 case LSHIFT: Cat1("<<"); break; 188 case RSHIFT: Cat1(">>"); break; 189 190 case RUN: fprintf(fd, "run %s(", now->sym->name); 191 for (v = now->lft; v; v = v->rgt) 192 if (v == now->lft) 193 { Cat2("", v->lft); 194 } else 195 { Cat2(",", v->lft); 196 } 197 fprintf(fd, ")"); 198 break; 199 200 case LEN: putname(fd, "len(", now->lft, m, ")"); 201 break; 202 case FULL: putname(fd, "full(", now->lft, m, ")"); 203 break; 204 case EMPTY: putname(fd, "empty(", now->lft, m, ")"); 205 break; 206 case NFULL: putname(fd, "nfull(", now->lft, m, ")"); 207 break; 208 case NEMPTY: putname(fd, "nempty(", now->lft, m, ")"); 209 break; 210 211 case 's': putname(fd, "", now->lft, m, now->val?"!!":"!"); 212 for (v = now->rgt, i=0; v; v = v->rgt, i++) 213 { if (v != now->rgt) fprintf(fd,","); 214 if (!symbolic(fd, v->lft)) 215 comwork(fd,v->lft,m); 216 } 217 break; 218 case 'r': putname(fd, "", now->lft, m, now->val?"??":"?"); 219 for (v = now->rgt, i=0; v; v = v->rgt, i++) 220 { if (v != now->rgt) fprintf(fd,","); 221 if (!symbolic(fd, v->lft)) 222 comwork(fd,v->lft,m); 223 } 224 break; 225 case 'R': putname(fd, "", now->lft, m, now->val?"??[":"?["); 226 for (v = now->rgt, i=0; v; v = v->rgt, i++) 227 { if (v != now->rgt) fprintf(fd,","); 228 if (!symbolic(fd, v->lft)) 229 comwork(fd,v->lft,m); 230 } 231 fprintf(fd, "]"); 232 break; 233 234 case ENABLED: Cat3("enabled(", now->lft, ")"); 235 break; 236 237 case PC_VAL: Cat3("pc_value(", now->lft, ")"); 238 break; 239 240 case 'c': Cat3("(", now->lft, ")"); 241 break; 242 243 case '?': Cat3("( (", now->lft, ") -> "); 244 Cat3("(", now->rgt->lft, ") : "); 245 Cat3("(", now->rgt->rgt, ") )"); 246 break; 247 248 case ASGN: comwork(fd,now->lft,m); 249 fprintf(fd," = "); 250 comwork(fd,now->rgt,m); 251 break; 252 253 case PRINT: { char c, buf[512]; 254 strncpy(buf, now->sym->name, 510); 255 for (i = j = 0; i < 510; i++, j++) 256 { c = now->sym->name[i]; 257 buf[j] = c; 258 if (c == '\\') buf[++j] = c; 259 if (c == '\"') buf[j] = '\''; 260 if (c == '\0') break; 261 } 262 fprintf(fd, "printf(%s", buf); 263 } 264 for (v = now->lft; v; v = v->rgt) 265 { Cat2(",", v->lft); 266 } 267 fprintf(fd, ")"); 268 break; 269 case NAME: putname(fd, "", now, m, ""); 270 break; 271 case 'p': putremote(fd, now, m); 272 break; 273 case 'q': fprintf(fd, "%s", now->sym->name); 274 break; 275 case ASSERT: Cat3("assert(", now->lft, ")"); 276 break; 277 case '.': fprintf(fd, ".(goto)"); break; 278 case GOTO: fprintf(fd, "goto"); break; 279 case BREAK: fprintf(fd, "break"); break; 280 case ELSE: fprintf(fd, "else"); break; 281 case '@': fprintf(fd, "-end-"); break; 282 283 case D_STEP: fprintf(fd, "D_STEP"); break; 284 case ATOMIC: fprintf(fd, "ATOMIC"); break; 285 case NON_ATOMIC: fprintf(fd, "sub-sequence"); break; 286 case IF: fprintf(fd, "IF"); break; 287 case DO: fprintf(fd, "DO"); break; 288 case UNLESS: fprintf(fd, "unless"); break; 289 case TIMEOUT: fprintf(fd, "timeout"); break; 290 default: if (isprint(now->ntyp)) 291 fprintf(fd, "'%c'", now->ntyp); 292 else 293 fprintf(fd, "%d", now->ntyp); 294 break; 295 } 296 } 297 298 void 299 comment(FILE *fd, Lextok *now, int m) 300 { extern int terse, nocast; 301 302 terse=nocast=1; 303 comwork(fd, now, m); 304 terse=nocast=0; 305 } 306