trunk/verif/Spin/Src5.1.6/pc_zpp.c

   1 /***** spin: pc_zpp.c *****/
   2
   3 /* Copyright (c) 1997-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 /* pc_zpp.c is only used in the PC version of Spin                        */
  13 /* it is included to avoid too great a reliance on an external cpp        */
  14
  15 #include <stdlib.h>
  16 #include <stdio.h>
  17 #include <string.h>
  18 #include <ctype.h>
  19
  20 #ifdef PC
  21 enum cstate { PLAIN, IN_STRING, IN_QUOTE, S_COMM, COMMENT, E_COMM };
  22
  23 #define MAXNEST 32
  24 #define MAXDEF  128
  25 #define MAXLINE 2048
  26 #define GENEROUS 8192
  27
  28 #define debug(x,y)      if (verbose) printf(x,y)
  29
  30 static FILE *outpp /* = stdout */;
  31
  32 static int if_truth[MAXNEST];
  33 static int printing[MAXNEST];
  34 static int if_depth, nr_defs, verbose = 0;
  35 static enum cstate state = PLAIN;
  36 static char Out1[GENEROUS], Out2[GENEROUS];
  37
  38 static struct Defines {
  39         int exists;
  40         char *src, *trg;
  41 } d[MAXDEF];
  42
  43 static int process(char *, int, char *);
  44 static int zpp_do(char *);
  45
  46 extern char *emalloc(size_t);   /* main.c */
  47
  48 static int
  49 do_define(char *p)
  50 {       char *q, *r, *s;
  51
  52         for (q = p+strlen(p)-1; q > p; q--)
  53                 if (*q == '\n' || *q == '\t' || *q == ' ')
  54                         *q = '\0';
  55                 else
  56                         break;
  57
  58         q = p + strspn(p, " \t");
  59         if (!(r = strchr(q, '\t')))
  60                 r = strchr(q, ' ');
  61         if (!r) { s = ""; goto adddef; }
  62         s = r + strspn(r, " \t");
  63         *r = '\0';
  64         if (strchr(q, '('))
  65         {       debug("zpp: #define with arguments %s\n", q);
  66                 return 0;
  67         }
  68         for (r = q+strlen(q)-1; r > q; r--)
  69                 if (*r == ' ' || *r == '\t')
  70                         *r = '\0';
  71                 else
  72                         break;
  73         if (nr_defs >= MAXDEF)
  74         {       debug("zpp: too many #defines (max %d)\n", nr_defs);
  75                 return 0;
  76         }
  77         if (strcmp(q, s) != 0)
  78         {       int j;
  79 adddef:         for (j = 0; j < nr_defs; j++)
  80                         if (!strcmp(d[j].src, q))
  81                                 d[j].exists = 0;
  82                 d[nr_defs].src = emalloc(strlen(q)+1);
  83                 d[nr_defs].trg = emalloc(strlen(s)+1);
  84                 strcpy(d[nr_defs].src, q);
  85                 strcpy(d[nr_defs].trg, s);
  86                 d[nr_defs++].exists = 1;
  87         }
  88         return 1;
  89 }
  90
  91 static int
  92 isvalid(int c)
  93 {
  94         return (isalnum(c) || c == '_');
  95 }
  96
  97 static char *
  98 apply(char *p0)
  99 {       char *out, *in1, *in2, *startat;
 100         int i, j;
 101
 102         startat = in1 = Out2; strcpy(Out2, p0);
 103         out = Out1; *out = '\0';
 104
 105         for (i = nr_defs-1; i >= 0; i--)
 106         {       if (!d[i].exists) continue;
 107                 j = (int) strlen(d[i].src);
 108 more:           in2 = strstr(startat, d[i].src);
 109                 if (!in2)       /* no more matches */
 110                 {       startat = in1;
 111                         continue;
 112                 }
 113                 if ((in2 == in1 || !isvalid(*(in2-1)))
 114                 &&  (in2+j == '\0' || !isvalid(*(in2+j))))
 115                 {       *in2 = '\0';
 116
 117                         if (strlen(in1)+strlen(d[i].trg)+strlen(in2+j) >= GENEROUS)
 118                         {
 119                                 printf("spin: macro expansion overflow %s -> %s ?\n",
 120                                         d[i].src, d[i].trg);
 121                                 return in1;
 122                         }
 123                         strcat(out, in1);
 124                         strcat(out, d[i].trg);
 125                         strcat(out, in2+j);
 126                         if (in1 == Out2)
 127                         {       startat = in1 = Out1;
 128                                 out = Out2;
 129                         } else
 130                         {       startat = in1 = Out2;
 131                                 out = Out1;
 132                         }
 133                         *out = '\0';
 134                 } else
 135                 {       startat = in2+1;        /* +1 not +j.. */
 136                 }
 137                 goto more; /* recursive defines */
 138         }
 139         return in1;
 140 }
 141
 142 static char *
 143 do_common(char *p)
 144 {       char *q, *s;
 145
 146         q = p + strspn(p, " \t");
 147         for (s = (q + strlen(q) - 1); s > q; s--)
 148                 if (*s == ' ' || *s == '\t' || *s == '\n')
 149                         *s = '\0';
 150                 else
 151                         break;
 152         return q;
 153 }
 154
 155 static int
 156 do_undefine(char *p)
 157 {       int i; char *q = do_common(p);
 158
 159         for (i = 0; i < nr_defs; i++)
 160                 if (!strcmp(d[i].src, q))
 161                         d[i].exists = 0;
 162         return 1;
 163 }
 164
 165 static char *
 166 check_ifdef(char *p)
 167 {       int i; char *q = do_common(p);
 168
 169         for (i = 0; i < nr_defs; i++)
 170                 if (d[i].exists
 171                 &&  !strcmp(d[i].src, q))
 172                         return d[i].trg;
 173         return (char *) 0;
 174 }
 175
 176 static int
 177 do_ifdef(char *p)
 178 {
 179         if (++if_depth >= MAXNEST)
 180         {       debug("zpp: too deeply nested (max %d)\n", MAXNEST);
 181                 return 0;
 182         }
 183         if_truth[if_depth] = (check_ifdef(p) != (char *)0);
 184         printing[if_depth] = printing[if_depth-1]&&if_truth[if_depth];
 185
 186         return 1;
 187 }
 188
 189 static int
 190 do_ifndef(char *p)
 191 {
 192         if (++if_depth >= MAXNEST)
 193         {       debug("zpp: too deeply nested (max %d)\n", MAXNEST);
 194                 return 0;
 195         }
 196         if_truth[if_depth] = (check_ifdef(p) == (char *)0);
 197         printing[if_depth] = printing[if_depth-1]&&if_truth[if_depth];
 198
 199         return 1;
 200 }
 201
 202 static int
 203 is_simple(char *q)
 204 {
 205         if (!q) return 0;
 206         if (strcmp(q, "0") == 0)
 207                 if_truth[if_depth] = 0;
 208         else if (strcmp(q, "1") == 0)
 209                 if_truth[if_depth] = 1;
 210         else
 211                 return 0;
 212         return 1;
 213 }
 214
 215 static int
 216 do_if(char *p)
 217 {       char *q = do_common(p);
 218         if (++if_depth >= MAXNEST)
 219         {       debug("zpp: too deeply nested (max %d)\n", MAXNEST);
 220                 return 0;
 221         }
 222         if (!is_simple(q)
 223         &&  !is_simple(check_ifdef(q)))
 224         {       debug("zpp: cannot handle #if %s\n", q);
 225                 return 0;
 226         }
 227         printing[if_depth] = printing[if_depth-1]&&if_truth[if_depth];
 228
 229         return 1;
 230 }
 231
 232 static int
 233 do_else(char *unused)
 234 {
 235         if_truth[if_depth] = 1-if_truth[if_depth];
 236         printing[if_depth] = printing[if_depth-1]&&if_truth[if_depth];
 237
 238         return 1;
 239 }
 240
 241 static int
 242 do_endif(char *p)
 243 {
 244         if (--if_depth < 0)
 245         {       debug("zpp: unbalanced #endif %s\n", p);
 246                 return 0;
 247         }
 248         return 1;
 249 }
 250
 251 static int
 252 do_include(char *p)
 253 {       char *r, *q;
 254
 255         q = strchr(p, '<');
 256         r = strrchr(p, '>');
 257         if (!q || !r)
 258         {       q = strchr (p, '\"');
 259                 r = strrchr(p, '\"');
 260                 if (!q || !r || q == r)
 261                 {       debug("zpp: malformed #include %s", p);
 262                         return 0;
 263         }       }
 264         *r = '\0';
 265         return zpp_do(++q);
 266 }
 267
 268 static int
 269 in_comment(char *p)
 270 {       char *q = p;
 271
 272         for (q = p; *q != '\n' && *q != '\0'; q++)
 273                 switch (state) {
 274                 case PLAIN:
 275                         switch (*q) {
 276                         case  '"': state = IN_STRING; break;
 277                         case '\'': state = IN_QUOTE; break;
 278                         case  '/': state = S_COMM; break;
 279                         case '\\': q++; break;
 280                         }
 281                         break;
 282                 case IN_STRING:
 283                         if (*q == '"') state = PLAIN;
 284                         else if (*q == '\\') q++;
 285                         break;
 286                 case IN_QUOTE:
 287                         if (*q == '\'') state = PLAIN;
 288                         else if (*q == '\\') q++;
 289                         break;
 290                 case S_COMM:
 291                         if (*q == '*')
 292                         {       *(q-1) = *q = ' ';
 293                                 state = COMMENT;
 294                         } else if (*q != '/')
 295                                 state = PLAIN;
 296                         break;
 297                 case COMMENT:
 298                         state = (*q == '*') ? E_COMM: COMMENT;
 299                         *q = ' ';
 300                         break;
 301                 case E_COMM:
 302                         if (*q == '/')
 303                                 state = PLAIN;
 304                         else if (*q != '*')
 305                                 state = COMMENT;
 306                         *q = ' ';
 307                         break;
 308                 }
 309         if (state == S_COMM) state = PLAIN;
 310         else if (state == E_COMM) state = COMMENT;
 311         return (state == COMMENT);
 312 }
 313
 314 static int
 315 zpp_do(char *fnm)
 316 {       char buf[2048], buf2[MAXLINE], *p; int n, on;
 317         FILE *inp; int lno = 0, nw_lno = 0;
 318
 319         if ((inp = fopen(fnm, "r")) == NULL)
 320         {       fprintf(stdout, "spin: error, '%s': No such file\n", fnm);
 321                 return 0;       /* 4.1.2 was stderr */
 322         }
 323         printing[0] = if_truth[0] = 1;
 324         fprintf(outpp, "#line %d \"%s\"\n", lno+1, fnm);
 325         while (fgets(buf, MAXLINE, inp))
 326         {       lno++; n = (int) strlen(buf);
 327                 on = 0; nw_lno = 0;
 328                 while (n > 2 && buf[n-2] == '\\')
 329                 {       buf[n-2] = '\0';
 330 feedme:                 if (!fgets(buf2, MAXLINE, inp))
 331                         {       debug("zpp: unexpected EOF ln %d\n", lno);
 332                                 return 0;       /* switch to cpp */
 333                         }
 334                         lno++;
 335                         if (n + (int) strlen(buf2) >= 2048)
 336                         {       debug("zpp: line %d too long\n", lno);
 337                                 return 0;
 338                         }
 339                         strcat(buf, buf2);
 340                         n = (int) strlen(buf);
 341                 }
 342                 if (in_comment(&buf[on]))
 343                 {       buf[n-1] = '\0'; /* eat newline */
 344                         on = n-1; nw_lno = 1;
 345                         goto feedme;
 346                 }
 347                 p = buf + strspn(buf, " \t");
 348                 if (nw_lno && *p != '#')
 349                         fprintf(outpp, "#line %d \"%s\"\n", lno, fnm);
 350                 if (*p == '#')
 351                 {       if (!process(p+1, lno+1, fnm))
 352                                 return 0;
 353                 } else if (printing[if_depth])
 354                         fprintf(outpp, "%s", apply(buf));
 355         }
 356         fclose(inp);
 357         return 1;
 358 }
 359
 360 int
 361 try_zpp(char *fnm, char *onm)
 362 {       int r;
 363         if ((outpp = fopen(onm, "w")) == NULL)
 364                 return 0;
 365         r = zpp_do(fnm);
 366         fclose(outpp);
 367         return r;       /* 1 = ok; 0 = use cpp */
 368 }
 369
 370 static struct Directives {
 371         int len;
 372         char *directive;
 373         int (*handler)(char *);
 374         int interp;
 375 } s[] = {
 376         { 6, "define",   do_define,     1 },
 377         { 4, "else",     do_else,       0 },
 378         { 5, "endif",    do_endif,      0 },
 379         { 5, "ifdef",    do_ifdef,      0 },
 380         { 6, "ifndef",   do_ifndef,     0 },
 381         { 2, "if",       do_if,         0 },
 382         { 7, "include",  do_include,    1 },
 383         { 8, "undefine", do_undefine,   1 },
 384 };
 385
 386 static int
 387 process(char *q, int lno, char *fnm)
 388 {       char *p; int i, r;
 389
 390         for (p = q; *p; p++)
 391                 if (*p != ' ' && *p != '\t')
 392                         break;
 393         for (i = 0; i < (int) (sizeof(s)/sizeof(struct Directives)); i++)
 394                 if (!strncmp(s[i].directive, p, s[i].len))
 395                 {       if (s[i].interp
 396                         &&  !printing[if_depth])
 397                                 return 1;
 398                         fprintf(outpp, "#line %d \"%s\"\n", lno, fnm);
 399                         r = s[i].handler(p +  s[i].len);
 400                         if (i == 6)     /* include */
 401                                 fprintf(outpp, "#line %d \"%s\"\n", lno, fnm);
 402                         return r;
 403                 }
 404
 405         debug("zpp: unrecognized directive: %s", p);
 406         return 0;
 407 }
 408 #endif