src/cttable.i

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