verif/Spin/Src5.1.6/pangen3.c

   1 /***** spin: pangen3.c *****/
   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
  12 #include "spin.h"
  13 #include "y.tab.h"
  14
  15 extern FILE     *th;
  16 extern int      claimnr, eventmapnr;
  17
  18 typedef struct SRC {
  19         short ln, st;   /* linenr, statenr */
  20         Symbol *fn;     /* filename */
  21         struct SRC *nxt;
  22 } SRC;
  23
  24 static int      col;
  25 static Symbol   *lastfnm;
  26 static Symbol   lastdef;
  27 static int      lastfrom;
  28 static SRC      *frst = (SRC *) 0;
  29 static SRC      *skip = (SRC *) 0;
  30
  31 extern void     sr_mesg(FILE *, int, int);
  32
  33 static void
  34 putnr(int n)
  35 {
  36         if (col++ == 8)
  37         {       fprintf(th, "\n\t");
  38                 col = 1;
  39         }
  40         fprintf(th, "%3d, ", n);
  41 }
  42
  43 static void
  44 putfnm(int j, Symbol *s)
  45 {
  46         if (lastfnm && lastfnm == s && j != -1)
  47                 return;
  48
  49         if (lastfnm)
  50                 fprintf(th, "{ %s, %d, %d },\n\t",
  51                         lastfnm->name,
  52                         lastfrom,
  53                         j-1);
  54         lastfnm = s;
  55         lastfrom = j;
  56 }
  57
  58 static void
  59 putfnm_flush(int j)
  60 {
  61         if (lastfnm)
  62                 fprintf(th, "{ %s, %d, %d }\n",
  63                         lastfnm->name,
  64                         lastfrom, j);
  65 }
  66
  67 void
  68 putskip(int m)  /* states that need not be reached */
  69 {       SRC *tmp;
  70
  71         for (tmp = skip; tmp; tmp = tmp->nxt)
  72                 if (tmp->st == m)
  73                         return;
  74         tmp = (SRC *) emalloc(sizeof(SRC));
  75         tmp->st = (short) m;
  76         tmp->nxt = skip;
  77         skip = tmp;
  78 }
  79
  80 void
  81 unskip(int m)   /* a state that needs to be reached after all */
  82 {       SRC *tmp, *lst=(SRC *)0;
  83
  84         for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
  85                 if (tmp->st == m)
  86                 {       if (tmp == skip)
  87                                 skip = skip->nxt;
  88                         else if (lst)   /* always true, but helps coverity */
  89                                 lst->nxt = tmp->nxt;
  90                         break;
  91                 }
  92 }
  93
  94 void
  95 putsrc(Element *e)      /* match states to source lines */
  96 {       SRC *tmp;
  97         int n, m;
  98
  99         if (!e || !e->n) return;
 100
 101         n = e->n->ln;
 102         m = e->seqno;
 103
 104         for (tmp = frst; tmp; tmp = tmp->nxt)
 105                 if (tmp->st == m)
 106                 {       if (tmp->ln != n || tmp->fn != e->n->fn)
 107                         printf("putsrc mismatch %d - %d, file %s\n", n,
 108                                 tmp->ln, tmp->fn->name);
 109                         return;
 110                 }
 111         tmp = (SRC *) emalloc(sizeof(SRC));
 112         tmp->ln = (short) n;
 113         tmp->st = (short) m;
 114         tmp->fn = e->n->fn;
 115         tmp->nxt = frst;
 116         frst = tmp;
 117 }
 118
 119 static void
 120 dumpskip(int n, int m)
 121 {       SRC *tmp, *lst;
 122         int j;
 123
 124         fprintf(th, "uchar reached%d [] = {\n\t", m);
 125         for (j = 0, col = 0; j <= n; j++)
 126         {       lst = (SRC *) 0;
 127                 for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
 128                         if (tmp->st == j)
 129                         {       putnr(1);
 130                                 if (lst)
 131                                         lst->nxt = tmp->nxt;
 132                                 else
 133                                         skip = tmp->nxt;
 134                                 break;
 135                         }
 136                 if (!tmp)
 137                         putnr(0);
 138         }
 139         fprintf(th, "};\n");
 140
 141         fprintf(th, "uchar *loopstate%d;\n", m);
 142
 143         if (m == claimnr)
 144                 fprintf(th, "#define reached_claim      reached%d\n", m);
 145         if (m == eventmapnr)
 146                 fprintf(th, "#define reached_event      reached%d\n", m);
 147
 148         skip = (SRC *) 0;
 149 }
 150
 151 void
 152 dumpsrc(int n, int m)
 153 {       SRC *tmp, *lst;
 154         int j;
 155
 156         fprintf(th, "short src_ln%d [] = {\n\t", m);
 157         for (j = 0, col = 0; j <= n; j++)
 158         {       lst = (SRC *) 0;
 159                 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
 160                         if (tmp->st == j)
 161                         {       putnr(tmp->ln);
 162                                 break;
 163                         }
 164                 if (!tmp)
 165                         putnr(0);
 166         }
 167         fprintf(th, "};\n");
 168
 169         lastfnm = (Symbol *) 0;
 170         lastdef.name = "\"-\"";
 171         fprintf(th, "S_F_MAP src_file%d [] = {\n\t", m);
 172         for (j = 0, col = 0; j <= n; j++)
 173         {       lst = (SRC *) 0;
 174                 for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
 175                         if (tmp->st == j)
 176                         {       putfnm(j, tmp->fn);
 177                                 if (lst)
 178                                         lst->nxt = tmp->nxt;
 179                                 else
 180                                         frst = tmp->nxt;
 181                                 break;
 182                         }
 183                 if (!tmp)
 184                         putfnm(j, &lastdef);
 185         }
 186         putfnm_flush(j);
 187         fprintf(th, "};\n");
 188
 189         if (m == claimnr)
 190                 fprintf(th, "#define src_claim  src_ln%d\n", m);
 191         if (m == eventmapnr)
 192                 fprintf(th, "#define src_event  src_ln%d\n", m);
 193
 194         frst = (SRC *) 0;
 195         dumpskip(n, m);
 196 }
 197
 198 #define Cat0(x)         comwork(fd,now->lft,m); fprintf(fd, x); \
 199                         comwork(fd,now->rgt,m)
 200 #define Cat1(x)         fprintf(fd,"("); Cat0(x); fprintf(fd,")")
 201 #define Cat2(x,y)       fprintf(fd,x); comwork(fd,y,m)
 202 #define Cat3(x,y,z)     fprintf(fd,x); comwork(fd,y,m); fprintf(fd,z)
 203
 204 static int
 205 symbolic(FILE *fd, Lextok *tv)
 206 {       Lextok *n; extern Lextok *Mtype;
 207         int cnt = 1;
 208
 209         if (tv->ismtyp)
 210         for (n = Mtype; n; n = n->rgt, cnt++)
 211                 if (cnt == tv->val)
 212                 {       fprintf(fd, "%s", n->lft->sym->name);
 213                         return 1;
 214                 }
 215         return 0;
 216 }
 217
 218 static void
 219 comwork(FILE *fd, Lextok *now, int m)
 220 {       Lextok *v;
 221         int i, j;
 222
 223         if (!now) { fprintf(fd, "0"); return; }
 224         switch (now->ntyp) {
 225         case CONST:     sr_mesg(fd, now->val, now->ismtyp); break;
 226         case '!':       Cat3("!(", now->lft, ")"); break;
 227         case UMIN:      Cat3("-(", now->lft, ")"); break;
 228         case '~':       Cat3("~(", now->lft, ")"); break;
 229
 230         case '/':       Cat1("/");  break;
 231         case '*':       Cat1("*");  break;
 232         case '-':       Cat1("-");  break;
 233         case '+':       Cat1("+");  break;
 234         case '%':       Cat1("%%"); break;
 235         case '&':       Cat1("&");  break;
 236         case '^':       Cat1("^");  break;
 237         case '|':       Cat1("|");  break;
 238         case LE:        Cat1("<="); break;
 239         case GE:        Cat1(">="); break;
 240         case GT:        Cat1(">"); break;
 241         case LT:        Cat1("<"); break;
 242         case NE:        Cat1("!="); break;
 243         case EQ:        Cat1("=="); break;
 244         case OR:        Cat1("||"); break;
 245         case AND:       Cat1("&&"); break;
 246         case LSHIFT:    Cat1("<<"); break;
 247         case RSHIFT:    Cat1(">>"); break;
 248
 249         case RUN:       fprintf(fd, "run %s(", now->sym->name);
 250                         for (v = now->lft; v; v = v->rgt)
 251                                 if (v == now->lft)
 252                                 {       comwork(fd, v->lft, m);
 253                                 } else
 254                                 {       Cat2(",", v->lft);
 255                                 }
 256                         fprintf(fd, ")");
 257                         break;
 258
 259         case LEN:       putname(fd, "len(", now->lft, m, ")");
 260                         break;
 261         case FULL:      putname(fd, "full(", now->lft, m, ")");
 262                         break;
 263         case EMPTY:     putname(fd, "empty(", now->lft, m, ")");
 264                         break;
 265         case NFULL:     putname(fd, "nfull(", now->lft, m, ")");
 266                         break;
 267         case NEMPTY:    putname(fd, "nempty(", now->lft, m, ")");
 268                         break;
 269
 270         case 's':       putname(fd, "", now->lft, m, now->val?"!!":"!");
 271                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
 272                         {       if (v != now->rgt) fprintf(fd,",");
 273                                 if (!symbolic(fd, v->lft))
 274                                         comwork(fd,v->lft,m);
 275                         }
 276                         break;
 277         case 'r':       putname(fd, "", now->lft, m, "?");
 278                         switch (now->val) {
 279                         case 0: break;
 280                         case 1: fprintf(fd, "?");  break;
 281                         case 2: fprintf(fd, "<");  break;
 282                         case 3: fprintf(fd, "?<"); break;
 283                         }
 284                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
 285                         {       if (v != now->rgt) fprintf(fd,",");
 286                                 if (!symbolic(fd, v->lft))
 287                                         comwork(fd,v->lft,m);
 288                         }
 289                         if (now->val >= 2)
 290                                 fprintf(fd, ">");
 291                         break;
 292         case 'R':       putname(fd, "", now->lft, m,  now->val?"??[":"?[");
 293                         for (v = now->rgt, i=0; v; v = v->rgt, i++)
 294                         {       if (v != now->rgt) fprintf(fd,",");
 295                                 if (!symbolic(fd, v->lft))
 296                                         comwork(fd,v->lft,m);
 297                         }
 298                         fprintf(fd, "]");
 299                         break;
 300
 301         case ENABLED:   Cat3("enabled(", now->lft, ")");
 302                         break;
 303
 304         case EVAL:      Cat3("eval(", now->lft, ")");
 305                         break;
 306
 307         case NONPROGRESS:
 308                         fprintf(fd, "np_");
 309                         break;
 310
 311         case PC_VAL:    Cat3("pc_value(", now->lft, ")");
 312                         break;
 313
 314         case 'c':       Cat3("(", now->lft, ")");
 315                         break;
 316
 317         case '?':       if (now->lft)
 318                         {       Cat3("( (", now->lft, ") -> ");
 319                         }
 320                         if (now->rgt)
 321                         {       Cat3("(", now->rgt->lft, ") : ");
 322                                 Cat3("(", now->rgt->rgt, ") )");
 323                         }
 324                         break;
 325
 326         case ASGN:      comwork(fd,now->lft,m);
 327                         fprintf(fd," = ");
 328                         comwork(fd,now->rgt,m);
 329                         break;
 330
 331         case PRINT:     {       char c, buf[512];
 332                                 strncpy(buf, now->sym->name, 510);
 333                                 for (i = j = 0; i < 510; i++, j++)
 334                                 {       c = now->sym->name[i];
 335                                         buf[j] = c;
 336                                         if (c == '\\') buf[++j] = c;
 337                                         if (c == '\"') buf[j] = '\'';
 338                                         if (c == '\0') break;
 339                                 }
 340                                 if (now->ntyp == PRINT)
 341                                         fprintf(fd, "printf");
 342                                 else
 343                                         fprintf(fd, "annotate");
 344                                 fprintf(fd, "(%s", buf);
 345                         }
 346                         for (v = now->lft; v; v = v->rgt)
 347                         {       Cat2(",", v->lft);
 348                         }
 349                         fprintf(fd, ")");
 350                         break;
 351         case PRINTM:    fprintf(fd, "printm(");
 352                         comwork(fd, now->lft, m);
 353                         fprintf(fd, ")");
 354                         break;
 355         case NAME:      putname(fd, "", now, m, "");
 356                         break;
 357         case   'p':     putremote(fd, now, m);
 358                         break;
 359         case   'q':     fprintf(fd, "%s", now->sym->name);
 360                         break;
 361         case C_EXPR:
 362         case C_CODE:    fprintf(fd, "{%s}", now->sym->name);
 363                         break;
 364         case ASSERT:    Cat3("assert(", now->lft, ")");
 365                         break;
 366         case   '.':     fprintf(fd, ".(goto)"); break;
 367         case  GOTO:     fprintf(fd, "goto %s", now->sym->name); break;
 368         case BREAK:     fprintf(fd, "break"); break;
 369         case  ELSE:     fprintf(fd, "else"); break;
 370         case   '@':     fprintf(fd, "-end-"); break;
 371
 372         case D_STEP:    fprintf(fd, "D_STEP"); break;
 373         case ATOMIC:    fprintf(fd, "ATOMIC"); break;
 374         case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
 375         case IF:        fprintf(fd, "IF"); break;
 376         case DO:        fprintf(fd, "DO"); break;
 377         case UNLESS:    fprintf(fd, "unless"); break;
 378         case TIMEOUT:   fprintf(fd, "timeout"); break;
 379         default:        if (isprint(now->ntyp))
 380                                 fprintf(fd, "'%c'", now->ntyp);
 381                         else
 382                                 fprintf(fd, "%d", now->ntyp);
 383                         break;
 384         }
 385 }
 386
 387 void
 388 comment(FILE *fd, Lextok *now, int m)
 389 {       extern short terse, nocast;
 390
 391         terse=nocast=1;
 392         comwork(fd, now, m);
 393         terse=nocast=0;
 394 }