src/cttable.i

   1 /* ;-*-C-*-;
   2 ** vim: set syntax=c filetype=c shiftwidth=2 softtabstop=2 expandtab:
   3 **
   4 ** Splint - annotation-assisted static program checker
   5 ** Copyright (C) 1994-2003 University of Virginia,
   6 **         Massachusetts Institute of Technology
   7 **
   8 ** This program is free software; you can redistribute it and/or modify it
   9 ** under the terms of the GNU General Public License as published by the
  10 ** Free Software Foundation; either version 2 of the License, or (at your
  11 ** option) any later version.
  12 **
  13 ** This program is distributed in the hope that it will be useful, but
  14 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  15 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  16 ** General Public License for more details.
  17 **
  18 ** The GNU General Public License is available from http://www.gnu.org/ or
  19 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20 ** MA 02111-1307, USA.
  21 **
  22 ** For information on splint: info@splint.org
  23 ** To report a bug: splint-bug@splint.org
  24 ** For more information: http://www.splint.org
  25 */
  26 /*
  27 ** cttable.i
  28 **
  29 ** NOTE: This is not a stand-alone source file, but is included in ctype.c.
  30 **       (This is necessary becuase there is no other way in C to have a
  31 **       hidden scope, besides at the file level.)
  32 */
  33
  34 /*@access ctype@*/
  35
  36 /*
  37 ** type definitions and forward declarations in ctbase.i
  38 */
  39
  40 static void
  41 ctentry_free (/*@only@*/ ctentry c)
  42 {
  43   ctbase_free (c->ctbase);
  44   cstring_free (c->unparse);
  45   sfree (c);
  46 }
  47
  48 static void cttable_reset (void)
  49    /*@globals cttab@*/
  50    /*@modifies cttab@*/
  51 {
  52   if (cttab.entries != NULL)
  53     {
  54       int i;
  55
  56       for (i = 0; i < cttab.size; i++)
  57         {
  58           /*drl bee: si*/   ctentry_free (cttab.entries[i]);
  59         }
  60
  61       /*@-compdestroy@*/
  62       sfree (cttab.entries);
  63       /*@=compdestroy@*/
  64
  65       cttab.entries = NULL;
  66     }
  67
  68   cttab.size = 0 ;
  69   cttab.nspace = 0 ;
  70 }
  71
  72 static ctentry
  73 ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c)
  74 {
  75
  76   return (ctentry_make (ctk, c, ctype_dne, ctype_dne, ctype_dne, cstring_undefined));
  77 }
  78
  79 static /*@only@*/ ctentry
  80 ctentry_make (ctkind ctk,
  81               /*@keep@*/ ctbase c, ctype base,
  82               ctype ptr, ctype array,
  83               /*@keep@*/ cstring unparse) /*@*/
  84 {
  85   ctentry cte = (ctentry) dmalloc (sizeof (*cte));
  86   cte->kind = ctk;
  87   cte->ctbase = c;
  88   cte->base = base;
  89   cte->ptr = ptr;
  90   cte->array = array;
  91   cte->unparse = unparse;
  92   return cte;
  93 }
  94
  95 static cstring
  96 ctentry_unparse (ctentry c)
  97 {
  98   return (message
  99           ("%20s [%d] [%d] [%d]",
 100            (cstring_isDefined (c->unparse) ? c->unparse : cstring_makeLiteral ("<no name>")),
 101            c->base,
 102            c->ptr,
 103            c->array));
 104 }
 105
 106 static bool
 107 ctentry_isInteresting (ctentry c)
 108 {
 109   return (cstring_isNonEmpty (c->unparse));
 110 }
 111
 112 static /*@only@*/ cstring
 113 ctentry_dump (ctentry c)
 114 {
 115   DPRINTF (("Dumping: %s", ctentry_unparse (c)));
 116
 117   if (c->ptr == ctype_dne
 118       && c->array == ctype_dne
 119       && c->base == ctype_dne)
 120     {
 121       return (message ("%d %q&",
 122                        ctkind_toInt (c->kind),
 123                        ctbase_dump (c->ctbase)));
 124     }
 125   else if (c->base == ctype_undefined
 126            && c->array == ctype_dne)
 127     {
 128       if (c->ptr == ctype_dne)
 129         {
 130           return (message ("%d %q!",
 131                            ctkind_toInt (c->kind),
 132                            ctbase_dump (c->ctbase)));
 133         }
 134       else
 135         {
 136           return (message ("%d %q^%d",
 137                            ctkind_toInt (c->kind),
 138                            ctbase_dump (c->ctbase),
 139                            c->ptr));
 140         }
 141     }
 142   else if (c->ptr == ctype_dne
 143            && c->array == ctype_dne)
 144     {
 145       return (message ("%d %q%d&",
 146                        ctkind_toInt (c->kind),
 147                        ctbase_dump (c->ctbase),
 148                        c->base));
 149     }
 150   else
 151     {
 152       return (message ("%d %q%d %d %d",
 153                        ctkind_toInt (c->kind),
 154                        ctbase_dump (c->ctbase),
 155                        c->base, c->ptr, c->array));
 156     }
 157 }
 158
 159
 160 static /*@only@*/ ctentry
 161 ctentry_undump (/*@dependent@*/ char *s) /*@requires maxRead(s) >= 2 @*/
 162 {
 163   int base, ptr, array;
 164   ctkind kind;
 165   ctbase ct;
 166
 167   kind = ctkind_fromInt (reader_getInt (&s));
 168   ct = ctbase_undump (&s);
 169
 170   if (reader_optCheckChar (&s, '&'))
 171     {
 172       base = ctype_dne;
 173       ptr = ctype_dne;
 174       array = ctype_dne;
 175     }
 176   else if (reader_optCheckChar (&s, '!'))
 177     {
 178       base = ctype_undefined;
 179       ptr = ctype_dne;
 180       array = ctype_dne;
 181     }
 182   else if (reader_optCheckChar (&s, '^'))
 183     {
 184       base = ctype_undefined;
 185       ptr = reader_getInt (&s);
 186       array = ctype_dne;
 187     }
 188   else
 189     {
 190       base = reader_getInt (&s);
 191
 192       if (reader_optCheckChar (&s, '&'))
 193         {
 194           ptr = ctype_dne;
 195           array = ctype_dne;
 196         }
 197       else
 198         {
 199           ptr = reader_getInt (&s);
 200           array = reader_getInt (&s);
 201         }
 202     }
 203
 204   /* can't unparse w/o typeTable */
 205   return (ctentry_make (kind, ct, base, ptr, array, cstring_undefined));
 206 }
 207
 208 static /*@observer@*/ cstring
 209 ctentry_doUnparse (ctentry c) /*@modifies c@*/
 210 {
 211   if (cstring_isDefined (c->unparse))
 212     {
 213       return (c->unparse);
 214     }
 215   else
 216     {
 217       cstring s = ctbase_unparse (c->ctbase);
 218
 219       if (!cstring_isEmpty (s) && !cstring_containsChar (s, '<'))
 220         {
 221           c->unparse = s;
 222         }
 223       else
 224         {
 225           cstring_markOwned (s);
 226         }
 227
 228       return (s);
 229     }
 230 }
 231
 232 static /*@observer@*/ cstring
 233 ctentry_doUnparseDeep (ctentry c)
 234 {
 235   if (cstring_isDefined (c->unparse))
 236     {
 237       return (c->unparse);
 238     }
 239   else
 240     {
 241       c->unparse = ctbase_unparseDeep (c->ctbase);
 242       return (c->unparse);
 243     }
 244 }
 245
 246 /*
 247 ** cttable operations
 248 */
 249
 250 static /*@only@*/ cstring
 251 cttable_unparse (void)
 252 {
 253   int i;
 254   cstring s = cstring_undefined;
 255
 256   /*@access ctbase@*/
 257   for (i = 0; i < cttab.size; i++)
 258     {
 259      /*drl bee: si*/    ctentry cte = cttab.entries[i];
 260       if (ctentry_isInteresting (cte))
 261         {
 262           if (ctbase_isUA (cte->ctbase))
 263             {
 264               s = message ("%s%d\t%q [%d]\n", s, i, ctentry_unparse (cttab.entries[i]),
 265                            cte->ctbase->contents.tid);
 266             }
 267           else
 268             {
 269               s = message ("%s%d\t%q\n", s, i, ctentry_unparse (cttab.entries[i]));
 270             }
 271         }
 272     }
 273   /*@noaccess ctbase@*/
 274   return (s);
 275 }
 276
 277 #if 0
 278 void
 279 cttable_print (void)
 280 {
 281   int i;
 282
 283   /*@access ctbase@*/
 284   for (i = 0; i < cttab.size; i++)
 285     {
 286    /*drl bee: si*/     ctentry cte = cttab.entries[i];
 287
 288       if (TRUE) /* ctentry_isInteresting (cte)) */
 289         {
 290           if (ctbase_isUA (cte->ctbase))
 291             {
 292               fprintf (g_warningstream, "%3d: %s [%d]\n", i,
 293                        cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])),
 294                        cte->ctbase->contents.tid);
 295             }
 296           else
 297             {
 298               fprintf (g_warningstream, "%3d: %s\n", i,
 299                        cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])));
 300             }
 301         }
 302       else
 303         {
 304           /* fprintf (g_warningstream, "%3d: <no name>\n", i); */
 305         }
 306     }
 307   /*@noaccess ctbase@*/
 308 }
 309 #endif
 310
 311 /*
 312 ** cttable_dump
 313 **
 314 ** Output cttable for dump file
 315 */
 316
 317 static void
 318 cttable_dump (FILE *fout)
 319 {
 320   bool showdots = FALSE;
 321   int showdotstride = 0;
 322   int i;
 323
 324   if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000)
 325     {
 326       displayScanClose ();
 327       displayScanOpen (message ("Dumping type table (%d types)", cttab.size));
 328       showdotstride = cttab.size / 5;
 329       showdots = TRUE;
 330     }
 331
 332   for (i = 0; i < cttab.size; i++)
 333     {
 334       cstring s;
 335
 336    /*drl bee: si*/     s = ctentry_dump (cttab.entries[i]);
 337       DPRINTF (("[%d] = %s", i, ctentry_unparse (cttab.entries[i])));
 338       llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH);
 339       fputline (fout, cstring_toCharsSafe (s));
 340       cstring_free (s);
 341
 342       if (showdots && (i != 0 && ((i - 1) % showdotstride == 0)))
 343         {
 344           (void) fflush (g_warningstream);
 345           displayScanContinue (cstring_makeLiteralTemp ("."));
 346           (void) fflush (stderr);
 347         }
 348     }
 349
 350   if (showdots)
 351     {
 352       displayScanClose ();
 353       displayScanOpen (cstring_makeLiteral ("Continuing dump "));
 354     }
 355
 356 }
 357
 358 /*
 359 ** load cttable from init file
 360 */
 361
 362 static void cttable_load (FILE *f)
 363   /*@globals cttab @*/
 364   /*@modifies cttab, f @*/
 365 {
 366   char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
 367   char *os = s;
 368   ctentry cte;
 369
 370   cttable_reset ();
 371
 372   /*
 373   DPRINTF (("Loading cttable: "));
 374   cttable_print ();
 375   */
 376
 377   while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';')
 378     {
 379       ;
 380     }
 381
 382   if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1))
 383     {
 384       llbug (message ("Library line too long: %s\n", cstring_fromChars (s)));
 385     }
 386
 387   while (s != NULL && *s != ';' && *s != '\0')
 388     {
 389       ctype ct;
 390
 391       /*drl bee: tcf*/      cte = ctentry_undump (s);
 392       ct = cttable_addFull (cte);
 393
 394       DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct)));
 395
 396       if (ctbase_isConj (cte->ctbase)
 397           && !(ctbase_isExplicitConj (cte->ctbase)))
 398         {
 399           ctype_recordConj (ct);
 400         }
 401
 402       s = reader_readLine (f, s, MAX_DUMP_LINE_LENGTH);
 403     }
 404
 405   sfree (os);
 406
 407   /*
 408   DPRINTF (("Done loading cttable: "));
 409   cttable_print ();
 410   */
 411 }
 412
 413 /*
 414 ** cttable_init
 415 **
 416 ** fill up the cttable with basic types, and first order derivations.
 417 ** this is done without using our constructors for efficiency reasons
 418 ** (probably bogus)
 419 **
 420 */
 421
 422 /*@access cprim@*/
 423 static void cttable_init (void)
 424    /*@globals cttab@*/ /*@modifies cttab@*/
 425 {
 426   ctkind i;
 427   cprim  j;
 428   ctbase ct = ctbase_undefined;
 429
 430   llassert (cttab.size == 0);
 431
 432   /* do for plain, pointer, arrayof */
 433   for (i = CTK_PLAIN; i <= CTK_ARRAY; i++)
 434     {
 435       for (j = CTX_UNKNOWN; j <= CTX_LAST; j++)
 436         {
 437           if (i == CTK_PLAIN)
 438             {
 439               if (j == CTX_BOOL)
 440                 {
 441                   ct = ctbase_createBool (); /* why different? */
 442                 }
 443               else if (j == CTX_UNKNOWN)
 444                 {
 445                   ct = ctbase_createUnknown ();
 446                 }
 447               else
 448                 {
 449                   ct = ctbase_createPrim ((cprim)j);
 450                 }
 451
 452               (void) cttable_addFull
 453                 (ctentry_make (CTK_PLAIN,
 454                                ct, ctype_undefined,
 455                                j + CTK_PREDEFINED, j + CTK_PREDEFINED2,
 456                                ctbase_unparse (ct)));
 457             }
 458           else
 459             {
 460               switch (i)
 461                 {
 462                 case CTK_PTR:
 463                   ct = ctbase_makePointer (j);
 464                   /*@switchbreak@*/ break;
 465                 case CTK_ARRAY:
 466                   ct = ctbase_makeArray (j);
 467                   /*@switchbreak@*/ break;
 468                 default:
 469                   llbugexitlit ("cttable_init: base case");
 470                 }
 471
 472               (void) cttable_addDerived (i, ct, j);
 473             }
 474         }
 475     }
 476
 477   /**** reserve a slot for userBool ****/
 478   (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined,
 479                                         ctype_undefined, ctype_dne, ctype_dne,
 480                                         cstring_undefined));
 481 }
 482
 483 /*@noaccess cprim@*/
 484
 485 static void
 486 cttable_grow (void)
 487 {
 488   int i;
 489   o_ctentry *newentries ;
 490
 491   cttab.nspace = CTK_BASESIZE;
 492   newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace));
 493
 494   if (newentries == NULL)
 495     {
 496       llfatalerror (message ("cttable_grow: out of memory.  Size: %d",
 497                              cttab.size));
 498     }
 499
 500   for (i = 0; i < cttab.size; i++)
 501     {
 502       /*drl bee: dm*/  /*drl bee: si*/  newentries[i] = cttab.entries[i];
 503     }
 504
 505   /*@-compdestroy@*/
 506   sfree (cttab.entries);
 507   /*@=compdestroy@*/
 508
 509   cttab.entries = newentries;
 510 /*@-compdef@*/
 511 } /*@=compdef@*/
 512
 513 static ctype
 514 cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base)
 515 {
 516   if (cttab.nspace == 0)
 517     cttable_grow ();
 518
 519   /*drl bee: si*/  cttab.entries[cttab.size] =
 520     ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined);
 521
 522   cttab.nspace--;
 523
 524   return (cttab.size++);
 525 }
 526
 527 static ctype
 528 cttable_addComplex (/*@only@*/ ctbase cnew)
 529    /*@modifies cttab; @*/
 530 {
 531   /*@access ctbase@*/
 532   if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN)
 533     {
 534       ctype i;
 535       int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL;
 536
 537       if (ctstop < LAST_PREDEFINED)
 538         {
 539           ctstop = LAST_PREDEFINED;
 540         }
 541
 542       for (i = cttable_lastIndex (); i >= ctstop; i--)  /* better to go from back... */
 543         {
 544           ctbase ctb;
 545
 546           ctb = ctype_getCtbase (i);
 547
 548           /* is this optimization really worthwhile? */
 549
 550           if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb))
 551             {
 552               DPRINTF (("EQUIV!! %s / %s",
 553                         ctbase_unparse (cnew),
 554                         ctbase_unparse (ctb)));
 555
 556               ctbase_free (cnew);
 557               return i;
 558             }
 559         }
 560     }
 561
 562   if (cttab.nspace == 0)
 563     cttable_grow ();
 564
 565   /*drl bee: si*/  cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined,
 566                                             ctype_dne, ctype_dne,
 567                                             cstring_undefined);
 568   cttab.nspace--;
 569
 570   return (cttab.size++);
 571   /*@noaccess ctbase@*/
 572 }
 573
 574 static ctype
 575 cttable_addFull (ctentry cnew)
 576 {
 577   if (cttab.nspace == 0)
 578     {
 579       cttable_grow ();
 580     }
 581
 582   /*drl bee: si*/  cttab.entries[cttab.size] = cnew;
 583   cttab.nspace--;
 584
 585   return (cttab.size++);
 586 }
 587
 588 static ctype
 589 cttable_addFullSafe (/*@only@*/ ctentry cnew)
 590 {
 591   int i;
 592   ctbase cnewbase = cnew->ctbase;
 593
 594   llassert (ctbase_isDefined (cnewbase));
 595
 596   for (i = cttable_lastIndex (); i >= CT_FIRST; i--)
 597     {
 598       ctbase ctb = ctype_getCtbase (i);
 599
 600       if (ctbase_isDefined (ctb)
 601           && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i)))
 602         {
 603           ctentry_free (cnew);
 604           return i;
 605         }
 606     }
 607
 608   if (cttab.nspace == 0)
 609     cttable_grow ();
 610
 611   /*drl bee: si*/  cttab.entries[cttab.size] = cnew;
 612
 613   cttab.nspace--;
 614
 615   return (cttab.size++);
 616 }
 617