src/symtable.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
  21 ** To report a bug: lclint-bug@cs.virginia.edu
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** symtable.c
  26 **
  27 ** Symbol table abstraction
  28 **
  29 **  AUTHORS:
  30 **
  31 **      Gary Feldman, Technical Languages and Environments, DECspec project
  32 **      Steve Garland,
  33 **         Massachusetts Institute of Technology
  34 **      Joe Wild, Technical Languages and Environments, DECspec project
  35 **      Yang Meng Tan,
  36 **         Massachusetts Institute of Technology
  37 **
  38 **  CREATION DATE:
  39 **
  40 **      20 January 1991
  41 */
  42
  43 # include "lclintMacros.nf"
  44 # include "llbasic.h"
  45 # include "gram.h"
  46 # include "lclscan.h"
  47 # include "lclsyntable.h"
  48 # include "lslparse.h"
  49
  50 /*@+ignorequals@*/
  51
  52 static bool isBlankLine (char *p_line);
  53 static bool inImport = FALSE;
  54
  55 /*@constant static int MAXBUFFLEN;@*/
  56 # define MAXBUFFLEN 512
  57 /*@constant static int DELTA;@*/
  58 # define DELTA 100
  59
  60 static void symHashTable_dump (symHashTable * p_t, FILE * p_f, bool p_lco);
  61
  62 static void tagInfo_free (/*@only@*/ tagInfo p_tag);
  63 static /*@observer@*/ scopeInfo symtable_scopeInfo (symtable p_stable);
  64
  65 static void symtable_dumpId (symtable p_stable, FILE *p_f, bool p_lco);
  66 static lsymbol nameNode2key (nameNode p_n);
  67
  68 typedef enum
  69 {
  70   SYMK_FCN, SYMK_SCOPE, SYMK_TYPE, SYMK_VAR
  71 } symKind;
  72
  73 typedef struct
  74 {
  75   symKind kind;
  76   union
  77   {
  78     /*@only@*/ fctInfo fct;
  79     /*@only@*/ scopeInfo scope;
  80     /*@only@*/ typeInfo type;
  81     /*@only@*/ varInfo var;
  82   } info;
  83 } idTableEntry;
  84
  85 typedef struct
  86 {
  87   unsigned int size;
  88   unsigned int allocated;
  89   /*@relnull@*/ idTableEntry *entries;
  90   bool exporting;
  91 } idTable;
  92
  93 struct s_symtableStruct
  94 {
  95   idTable *idTable;             /* data is idTableEntry */
  96   symHashTable *hTable;         /* data is htData */
  97   mapping type2sort;            /* maps LCL type symbol to LSL sort */
  98 } ;
  99
 100 static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *p_x);
 101 static /*@out@*/ /*@exposed@*/ idTableEntry *nextFree (idTable * p_st);
 102 static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookup (idTable * p_st, lsymbol p_id);
 103 static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookupInScope (idTable * p_st, lsymbol p_id);
 104
 105 static /*@only@*/ idTable *symtable_newIdTable (void);
 106 static void idTableEntry_free (idTableEntry p_x);
 107
 108 /* Local implementatio of hash table */
 109
 110 static bool allowed_redeclaration = FALSE;
 111 static symbolKey htData_key (htData *p_x);
 112
 113 static void symHashTable_free (/*@only@*/ symHashTable *p_h);
 114 static /*@only@*/ symHashTable *symHashTable_create (unsigned int p_size);
 115 static /*@null@*/ /*@exposed@*/ htData *
 116   symHashTable_get (symHashTable * p_t, symbolKey p_key, infoKind p_kind,
 117                  /*@null@*/ nameNode p_n);
 118 static bool symHashTable_put (symHashTable *p_t, /*@only@*/ htData *p_data);
 119 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
 120   symHashTable_forcePut (symHashTable * p_t, /*@only@*/ htData *p_data);
 121 /* static unsigned int symHashTable_count (symHashTable * t); */
 122
 123 static void idTable_free (/*@only@*/ idTable *p_st);
 124
 125 void varInfo_free (/*@only@*/ varInfo v)
 126 {
 127   ltoken_free (v->id);
 128   sfree (v);
 129 }
 130
 131 static /*@only@*/ varInfo varInfo_copy (varInfo v)
 132 {
 133   varInfo ret = (varInfo) dmalloc (sizeof (*ret));
 134
 135   ret->id = ltoken_copy (v->id);
 136   ret->sort = v->sort;
 137   ret->kind = v->kind;
 138   ret->export = v->export;
 139
 140   return ret;
 141 }
 142
 143 void symtable_free (symtable stable)
 144 {
 145   /* symtable_printStats (stable); */
 146
 147   idTable_free (stable->idTable);
 148   symHashTable_free (stable->hTable);
 149   mapping_free (stable->type2sort);
 150   sfree (stable);
 151 }
 152
 153 static void idTable_free (idTable *st)
 154 {
 155   unsigned int i;
 156
 157   for (i = 0; i < st->size; i++)
 158     {
 159       idTableEntry_free (st->entries[i]);
 160     }
 161
 162   sfree (st->entries);
 163   sfree (st);
 164 }
 165
 166 static void fctInfo_free (/*@only@*/ fctInfo f)
 167 {
 168   signNode_free (f->signature);
 169   pairNodeList_free (f->globals);
 170   ltoken_free (f->id);
 171   sfree (f);
 172 }
 173
 174 static void typeInfo_free (/*@only@*/ typeInfo t)
 175 {
 176   ltoken_free (t->id);
 177   sfree (t);
 178 }
 179
 180 static void scopeInfo_free (/*@only@*/ scopeInfo s)
 181 {
 182   sfree (s);
 183 }
 184
 185 static void idTableEntry_free (idTableEntry x)
 186 {
 187   switch (x.kind)
 188     {
 189     case SYMK_FCN:
 190       fctInfo_free (x.info.fct);
 191       break;
 192     case SYMK_SCOPE:
 193       scopeInfo_free (x.info.scope);
 194       break;
 195     case SYMK_TYPE:
 196       typeInfo_free (x.info.type);
 197       break;
 198     case SYMK_VAR:
 199       varInfo_free (x.info.var);
 200       break;
 201     }
 202 }
 203
 204 static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *x)
 205 {
 206   switch (x->kind)
 207     {
 208     case SYMK_FCN:
 209       return (x->info.fct->id);
 210     case SYMK_SCOPE:
 211       return ltoken_undefined;
 212     case SYMK_TYPE:
 213       return (x->info.type->id);
 214     case SYMK_VAR:
 215       return (x->info.var->id);
 216     }
 217
 218   BADBRANCHRET (ltoken_undefined);
 219 }
 220
 221 /*@only@*/ symtable
 222 symtable_new (void)
 223 {
 224   symtable stable = (symtable) dmalloc (sizeof (*stable));
 225   idTableEntry *e;
 226
 227   stable->idTable = symtable_newIdTable ();
 228   stable->hTable = symHashTable_create (HT_MAXINDEX);
 229   stable->type2sort = mapping_create ();
 230
 231   /* add builtin synonym:  Bool -> bool */
 232
 233   mapping_bind (stable->type2sort, lsymbol_getBool (), lsymbol_getbool ());
 234
 235   /*
 236   ** done by symtable_newIdTable
 237   ** st->allocated = 0;
 238   ** st->entries = (idTableEntry *) 0;
 239   ** st->exporting = TRUE;
 240   */
 241
 242   /* this is global scope */
 243   e = nextFree (stable->idTable);
 244   e->kind = SYMK_SCOPE;
 245   (e->info).scope = (scopeInfo) dmalloc (sizeof (*((e->info).scope)));
 246   (e->info).scope->kind = SPE_GLOBAL;
 247
 248   return stable;
 249 }
 250
 251 static /*@only@*/ idTable *symtable_newIdTable (void)
 252 {
 253   idTable *st = (idTable *) dmalloc (sizeof (*st));
 254
 255   st->size = 0;
 256   st->allocated = 0;
 257   st->entries = (idTableEntry *) 0;
 258   st->exporting = TRUE;
 259
 260   /* this was being done twice!
 261      e = nextFree (st);
 262      e->kind = SYMK_SCOPE;
 263      (e->info).scope.kind = globScope;
 264      */
 265
 266   return st;
 267 }
 268
 269 static lsymbol
 270 nameNode2key (nameNode n)
 271 {
 272   unsigned int ret;
 273
 274   if (n->isOpId)
 275     {
 276       ret =  ltoken_getText (n->content.opid);
 277     }
 278   else
 279     {
 280       /* use opForm's key as its Identifier */
 281       llassert (n->content.opform != NULL);
 282       ret = (n->content.opform)->key;
 283     }
 284
 285   return ret;
 286 }
 287
 288 /*
 289 ** requires: nameNode n is already in st.
 290 */
 291
 292 static bool
 293 htData_insertSignature (htData *d, /*@owned@*/ sigNode oi)
 294 {
 295   sigNodeSet set = d->content.op->signatures;
 296
 297
 298   if (oi != (sigNode) 0)
 299     {
 300       return (sigNodeSet_insert (set, oi));
 301     }
 302   return FALSE;
 303 }
 304
 305 void
 306 symtable_enterOp (symtable st, /*@only@*/ /*@notnull@*/ nameNode n,
 307                   /*@owned@*/ sigNode oi)
 308 {
 309   /*
 310   ** Operators are overloaded, we allow entering opInfo more than once,
 311   ** even if it's the same signature.
 312   **
 313   ** Assumes all sorts are already entered into the symbol table
 314   */
 315
 316   symHashTable *ht = st->hTable;
 317   htData *d;
 318   lsymbol id;
 319
 320
 321
 322   id = nameNode2key (n);
 323
 324   d = symHashTable_get (ht, id, IK_OP, n);
 325
 326   if (d == (htData *) 0)
 327     {                           /* first signature of this operator */
 328       opInfo op = (opInfo) dmalloc (sizeof (*op));
 329       htData *nd = (htData *) dmalloc (sizeof (*nd));
 330
 331       op->name = n;
 332
 333       if (oi != (sigNode) 0)
 334         {
 335           op->signatures = sigNodeSet_singleton (oi);
 336           ht->count++;
 337         }
 338       else
 339         {
 340           op->signatures = sigNodeSet_new ();
 341           sigNode_markOwned (oi);
 342         }
 343
 344       nd->kind = IK_OP;
 345       nd->content.op = op;
 346       (void) symHashTable_put (ht, nd);
 347     }
 348   else
 349     {
 350
 351       nameNode_free (n);  /*<<<??? */
 352
 353       if (htData_insertSignature (d, oi))
 354         {
 355           ht->count++;
 356         }
 357     }
 358 }
 359
 360 bool
 361   symtable_enterTag (symtable st, tagInfo ti)
 362 {
 363   /* put ti only if it is not already in symtable */
 364   symHashTable *ht = st->hTable;
 365   htData *d;
 366   symbolKey key = ltoken_getText (ti->id);
 367
 368   d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);
 369   if (d == (htData *) 0)
 370     {
 371       d = (htData *) dmalloc (sizeof (*d));
 372       d->kind = IK_TAG;
 373       d->content.tag = ti;
 374       d->content.tag->imported = context_inImport ();
 375       (void) symHashTable_put (ht, d);
 376       return TRUE;
 377     }
 378   else
 379     {
 380       if (d->content.tag->imported)
 381         {
 382           d->content.tag = ti;
 383           d->content.tag->imported = context_inImport ();
 384           return TRUE;
 385         }
 386       else
 387         {
 388           tagInfo_free (ti);
 389           return FALSE;
 390         }
 391     }
 392 }
 393
 394 bool
 395 symtable_enterTagForce (symtable st, tagInfo ti)
 396 {
 397  /* put ti, force-put if necessary */
 398   symHashTable *ht = st->hTable;
 399   htData *d;
 400   symbolKey key = ltoken_getText (ti->id);
 401
 402   d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);
 403
 404   if (d == (htData *) 0)
 405     {
 406       d = (htData *) dmalloc (sizeof (*d));
 407
 408       d->kind = IK_TAG;
 409       d->content.tag = ti;
 410       d->content.tag->imported = context_inImport ();
 411       (void) symHashTable_put (ht, d);
 412       return TRUE;
 413     }
 414   else
 415     {
 416
 417       d->kind = IK_TAG;
 418       d->content.tag = ti;
 419       d->content.tag->imported = context_inImport ();
 420       /* interpret return data later, htData * */
 421       /*@i@*/ (void) symHashTable_forcePut (ht, d);
 422       return FALSE;
 423     }
 424 }
 425
 426 /*@null@*/ opInfo
 427 symtable_opInfo (symtable st, /*@notnull@*/ nameNode n)
 428 {
 429   symHashTable *ht = st->hTable;
 430   lsymbol i = nameNode2key (n);
 431
 432   htData *d;
 433   d = symHashTable_get (ht, i, IK_OP, n);
 434   if (d == (htData *) 0)
 435     {
 436       return (opInfo)NULL;
 437     }
 438
 439   return (d->content.op);
 440 }
 441
 442 /*@null@*/ tagInfo
 443 symtable_tagInfo (symtable st, lsymbol i)
 444 {
 445   symHashTable *ht = st->hTable;
 446   htData *d;
 447   d = symHashTable_get (ht, i, IK_TAG, 0);
 448
 449   if (d == (htData *) 0)
 450     {
 451       return (tagInfo) NULL;
 452     }
 453
 454   return (d->content.tag);
 455 }
 456
 457 void
 458   symtable_enterScope (symtable stable, scopeInfo si)
 459 {
 460   idTable *st = stable->idTable;
 461   idTableEntry *e = nextFree (st);
 462   if (si->kind == SPE_GLOBAL)
 463     llbuglit ("symtable_enterScope: SPE_GLOBAL");
 464   e->kind = SYMK_SCOPE;
 465   (e->info).scope = si;
 466 }
 467
 468 void
 469 symtable_exitScope (symtable stable)
 470 {
 471   idTable *st = stable->idTable;
 472   int n;
 473
 474   if (st->entries != NULL)
 475     {
 476       for (n = st->size - 1; (st->entries[n]).kind != SYMK_SCOPE; n--)
 477         {
 478           ;
 479         }
 480     }
 481   else
 482     {
 483       llcontbuglit ("symtable_exitScope: no scope to exit");
 484       n = 0;
 485     }
 486
 487   st->size = n;
 488 }
 489
 490 bool
 491 symtable_enterFct (symtable stable, fctInfo fi)
 492 {
 493   idTable *st = stable->idTable;
 494   idTableEntry *e;
 495   bool redecl = FALSE;
 496
 497   if (!allowed_redeclaration &&
 498       symtable_lookup (st, ltoken_getText (fi->id)) != (idTableEntry *) 0)
 499     {
 500       lclRedeclarationError (fi->id);
 501       redecl = TRUE;
 502     }
 503
 504   e = nextFree (st);
 505   e->kind = SYMK_FCN;
 506   fi->export = st->exporting;   /* && !fi->private; */
 507   (e->info).fct = fi;
 508
 509   return redecl;
 510 }
 511
 512 void
 513 symtable_enterType (symtable stable, /*@only@*/ typeInfo ti)
 514 {
 515   idTable *st = stable->idTable;
 516   idTableEntry *e;
 517   bool insertp = TRUE;
 518   scopeKind k = (symtable_scopeInfo (stable))->kind;
 519
 520   /* symtable_disp (stable); */
 521
 522   if (k != SPE_GLOBAL && k != SPE_INVALID)      /* fixed for Splint */
 523     {
 524       llbug (message ("%q: symtable_enterType: expect global scope. (type: %s)",
 525                       ltoken_unparseLoc (ti->id),
 526                       ltoken_getRawString (ti->id)));
 527     }
 528
 529   if (!allowed_redeclaration &&
 530       symtable_lookup (st, ltoken_getText (ti->id)) != (idTableEntry *) 0)
 531     {
 532      /* ignore if Bool is re-entered */
 533       if (ltoken_getText (ti->id) == lsymbol_getBool () ||
 534           ltoken_getText (ti->id) == lsymbol_getbool ())
 535         {
 536           insertp = FALSE;
 537         }
 538       else
 539         {
 540           lclRedeclarationError (ti->id);
 541         }
 542     }
 543   if (insertp)
 544     {
 545       /* make sure it is a type TYPEDEF_NAME; */
 546
 547       if (ltoken_getCode (ti->id) != LLT_TYPEDEF_NAME)
 548         {
 549           lclbug (message ("symtable_enterType: gets a simpleId, expect a type: %s",
 550                            ltoken_getRawString (ti->id)));
 551         }
 552
 553       e = nextFree (st);
 554       e->kind = SYMK_TYPE;
 555       ti->export = st->exporting;/* && !ti->private; */
 556       (e->info).type = ti;
 557       mapping_bind (stable->type2sort, ltoken_getText (ti->id),
 558                     sort_getLsymbol (sort_makeVal (sort_getUnderlying (ti->basedOn))));
 559     }
 560   else
 561     {
 562       typeInfo_free (ti);
 563     }
 564 }
 565
 566 lsymbol
 567 lsymbol_sortFromType (symtable s, lsymbol typename)
 568 {
 569   lsymbol inter;
 570   lsymbol out;
 571   ltoken tok;
 572  /* check the synonym table first */
 573   if (LCLIsSyn (typename))
 574     {
 575       tok = LCLGetTokenForSyn (typename);
 576       inter = ltoken_getText (tok);
 577      /*    printf ("In lsymbol_sortFromType: %s -> %s\n",
 578                 lsymbol_toChars (typename), lsymbol_toChars (inter)); */
 579     }
 580   else
 581     {
 582       inter = typename;
 583     }
 584
 585   /* now map LCL type to sort */
 586   out = mapping_find (s->type2sort, inter);
 587
 588   if (out == lsymbol_undefined)
 589     {
 590       return inter;
 591     }
 592
 593   return out;
 594 }
 595
 596 /* really temp! */
 597
 598 /*
 599 ** returns true is vi is a redeclaration
 600 */
 601
 602 bool
 603 symtable_enterVar (symtable stable, /*@temp@*/ varInfo vi)
 604 {
 605   idTable *st = stable->idTable;
 606   bool insertp = TRUE;
 607   bool redecl = FALSE;
 608
 609
 610   /* symtable_disp (symtab); */
 611
 612   if (!allowed_redeclaration &&
 613       (symtable_lookupInScope (st, ltoken_getText (vi->id)) != (idTableEntry *) 0))
 614     {
 615       if (ltoken_getText (vi->id) == lsymbol_getTRUE () ||
 616           ltoken_getText (vi->id) == lsymbol_getFALSE ())
 617         {
 618           insertp = FALSE;
 619         }
 620       else
 621         {
 622           if (usymtab_existsEither (ltoken_getRawString (vi->id)))
 623             {
 624                       lclRedeclarationError (vi->id);
 625               redecl = TRUE;
 626             }
 627           else
 628             {
 629               llbuglit ("redeclared somethingerother?!");
 630             }
 631         }
 632     }
 633
 634   if (insertp)
 635     {
 636       idTableEntry *e = nextFree (st);
 637
 638       e->kind = SYMK_VAR;
 639       vi->export = st->exporting &&     /* !vi.private && */
 640         (vi->kind == VRK_VAR || vi->kind == VRK_CONST || vi->kind == VRK_ENUM);
 641       (e->info).var = varInfo_copy (vi);
 642     }
 643
 644     return (redecl);
 645 }
 646
 647 bool
 648 symtable_exists (symtable stable, lsymbol i)
 649 {
 650   idTable *st = stable->idTable;
 651   return symtable_lookup (st, i) != (idTableEntry *) 0;
 652 }
 653
 654 /*@null@*/ typeInfo
 655 symtable_typeInfo (symtable stable, lsymbol i)
 656 {
 657   idTable *st;
 658   idTableEntry *e;
 659
 660   st = stable->idTable;
 661   e = symtable_lookup (st, i);
 662
 663   if (e == (idTableEntry *) 0 || e->kind != SYMK_TYPE)
 664     {
 665       return (typeInfo) NULL;
 666     }
 667
 668   return (e->info).type;
 669 }
 670
 671 /*@null@*/ varInfo
 672 symtable_varInfo (symtable stable, lsymbol i)
 673 {
 674   idTable *st = stable->idTable;
 675   idTableEntry *e;
 676
 677   e = symtable_lookup (st, i);
 678
 679   if (e == (idTableEntry *) 0 || e->kind != SYMK_VAR)
 680     {
 681       return (varInfo) NULL;
 682     }
 683
 684   return (e->info).var;
 685 }
 686
 687 /*@null@*/ varInfo
 688 symtable_varInfoInScope (symtable stable, lsymbol id)
 689 {
 690   /* if current scope is a SPE_QUANT, can go beyond current scope */
 691   idTable *st = stable->idTable;
 692   idTableEntry *e2 = (idTableEntry *) 0;
 693   int n;
 694
 695   for (n = st->size - 1; n >= 0; n--)
 696     {
 697       ltoken tok;
 698
 699       e2 = &(st->entries[n]);
 700
 701       if (e2->kind == SYMK_SCOPE && e2->info.scope->kind != SPE_QUANT)
 702         {
 703           return (varInfo) NULL;
 704         }
 705
 706       tok = idTableEntry_getId (e2);
 707
 708       if (e2->kind == SYMK_VAR && ltoken_getText (tok) == id)
 709         {
 710           return (e2->info).var;
 711         }
 712     }
 713
 714   return (varInfo) NULL;
 715 }
 716
 717 scopeInfo
 718 symtable_scopeInfo (symtable stable)
 719 {
 720   idTable *st = stable->idTable;
 721   int n;
 722   idTableEntry *e;
 723
 724   for (n = st->size - 1; n >= 0; n--)
 725     {
 726       e = &(st->entries[n]);
 727       if (e->kind == SYMK_SCOPE)
 728         return (e->info).scope;
 729     }
 730
 731   lclfatalbug ("symtable_scopeInfo: not found");
 732   BADEXIT;
 733 }
 734
 735 void
 736 symtable_export (symtable stable, bool yesNo)
 737 {
 738   idTable *st = stable->idTable;
 739   st->exporting = yesNo;
 740   (void) sort_setExporting (yesNo);
 741 }
 742
 743 static void
 744 symHashTable_dump (symHashTable * t, FILE * f, bool lco)
 745 {
 746   /* like symHashTable_dump2 but for output to .lcs file */
 747   int i, size;
 748   bucket *b;
 749   htEntry *entry;
 750   htData *d;
 751   ltoken tok;
 752   sigNodeSet sigs;
 753
 754   for (i = 0; i <= HT_MAXINDEX; i++)
 755     {
 756             b = t->buckets[i];
 757
 758       for (entry = b; entry != NULL; entry = entry->next)
 759         {
 760           d = entry->data;
 761
 762           switch (d->kind)
 763             {
 764             case IK_SORT:
 765               /*@switchbreak@*/ break;
 766             case IK_OP:
 767               {
 768                 char *name = cstring_toCharsSafe (nameNode_unparse (d->content.op->name));
 769                 sigs = d->content.op->signatures;
 770                 size = sigNodeSet_size (sigs);
 771
 772
 773                 sigNodeSet_elements (sigs, x)
 774                   {
 775                     cstring s = sigNode_unparse (x);
 776
 777                     if (lco)
 778                       {
 779                         fprintf (f, "%%LCL");
 780                       }
 781
 782                     fprintf (f, "op %s %s\n", name, cstring_toCharsSafe (s));
 783                     cstring_free (s);
 784                   } end_sigNodeSet_elements;
 785
 786                 sfree (name);
 787                 /*@switchbreak@*/ break;
 788               }
 789             case IK_TAG:
 790               tok = d->content.tag->id;
 791
 792               if (!ltoken_isUndefined (tok))
 793                 {
 794                   cstring s = tagKind_unparse (d->content.tag->kind);
 795
 796                   if (lco)
 797                     {
 798                       fprintf (f, "%%LCL");
 799                     }
 800
 801                   fprintf (f, "tag %s %s\n", ltoken_getTextChars (tok),
 802                            cstring_toCharsSafe (s));
 803                   cstring_free (s);
 804                 }
 805               /*@switchbreak@*/ break;
 806             }
 807         }
 808     }
 809 }
 810
 811 void
 812 symtable_dump (symtable stable, FILE * f, bool lco)
 813 {
 814   symHashTable *ht = stable->hTable;
 815
 816
 817   fprintf (f, "%s\n", BEGINSYMTABLE);
 818
 819   symHashTable_dump (ht, f, lco);
 820
 821   symtable_dumpId (stable, f, lco);
 822
 823   fprintf (f, "%s\n", SYMTABLEEND);
 824   }
 825
 826 lsymbol
 827 lsymbol_translateSort (mapping m, lsymbol s)
 828 {
 829   lsymbol res = mapping_find (m, s);
 830   if (res == lsymbol_undefined)
 831     return s;
 832   return res;
 833 }
 834
 835 static /*@null@*/ lslOp
 836   lslOp_renameSorts (mapping map,/*@returned@*/ /*@null@*/ lslOp op)
 837 {
 838   sigNode sign;
 839
 840   if (op != (lslOp) 0)
 841     {
 842       ltokenList domain;
 843       ltoken range;
 844
 845       sign = op->signature;
 846       range = sign->range;
 847       domain = sign->domain;
 848
 849       ltokenList_elements (domain, dt)
 850         {
 851           ltoken_setText (dt,
 852                           lsymbol_translateSort (map, ltoken_getText (dt)));
 853         } end_ltokenList_elements;
 854
 855       /*@-onlytrans@*/ /* A memory leak... */
 856       op->signature = makesigNode (sign->tok, domain, range);
 857       /*@=onlytrans@*/
 858     }
 859
 860   return op;
 861 }
 862
 863 static /*@null@*/ signNode
 864   signNode_fromsigNode (sigNode s)
 865 {
 866   signNode sign;
 867   sortList slist;
 868
 869   if (s == (sigNode) 0)
 870     {
 871       return (signNode) 0;
 872     }
 873
 874   sign = (signNode) dmalloc (sizeof (*sign));
 875   slist = sortList_new ();
 876   sign->tok = ltoken_copy (s->tok);
 877   sign->key = s->key;
 878   sign->range = sort_makeSort (ltoken_undefined, ltoken_getText (s->range));
 879
 880   ltokenList_elements (s->domain, dt)
 881     {
 882       sortList_addh (slist, sort_makeSort (ltoken_undefined, ltoken_getText (dt)));
 883     } end_ltokenList_elements;
 884
 885   sign->domain = slist;
 886   return sign;
 887 }
 888
 889
 890 /**  2.4.3 ymtan  93.09.23  -- fixed bug in parseGlobals: removed ";" at the
 891  **                            end of pairNode (gstr).
 892  */
 893
 894 static /*@only@*/ pairNodeList
 895 parseGlobals (char *line, inputStream srce)
 896 {
 897   pairNodeList plist = pairNodeList_new ();
 898   pairNode p;
 899   int semi_index;
 900   char *lineptr, sostr[MAXBUFFLEN], gstr[MAXBUFFLEN];
 901
 902   /* line is not all blank */
 903   /* expected format: "sort1 g1; sort2 g2; sort3 g3;" */
 904   lineptr = line;
 905
 906   while (!isBlankLine (lineptr))
 907     {
 908       if (sscanf (lineptr, "%s %s", &(sostr[0]), gstr) != 2)
 909         {
 910           lclplainerror
 911             (message
 912              ("%q: Imported file contains illegal function global declaration.\n"
 913               "Skipping rest of the line: %s (%s)",
 914               fileloc_unparseRaw (inputStream_fileName (srce),
 915                                   inputStream_thisLineNumber (srce)),
 916               cstring_fromChars (line),
 917               cstring_fromChars (lineptr)));
 918           return plist;
 919         }
 920
 921       p = (pairNode) dmalloc (sizeof (*p));
 922
 923       /* Note: remove the ";" separator at the end of gstr */
 924       semi_index = size_toInt (strlen (gstr));
 925       gstr[semi_index - 1] = '\0';
 926
 927       p->tok = ltoken_create (NOTTOKEN, lsymbol_fromChars (gstr));
 928       p->sort = sort_makeSort (ltoken_undefined, lsymbol_fromChars (sostr));
 929
 930       pairNodeList_addh (plist, p);
 931       lineptr = strchr (lineptr, ';');  /* go pass the next; */
 932
 933       llassert (lineptr != NULL);
 934       lineptr = lineptr + 1;
 935     }
 936
 937   return plist;
 938 }
 939
 940 static bool
 941 isBlankLine (char *line)
 942 {
 943   int i;
 944
 945   if (line == NULL) return TRUE;
 946
 947   for (i = 0; line[i] != '\0'; i++)
 948     {
 949       if (line[i] == ' ')
 950         continue;
 951       if (line[i] == '\t')
 952         continue;
 953       if (line[i] == '\n')
 954         return TRUE;
 955       return FALSE;
 956     }
 957   return TRUE;
 958 }
 959
 960 typedef /*@only@*/ fctInfo o_fctInfo;
 961
 962 static void
 963 parseLine (char *line, inputStream srce, mapping map)
 964 {
 965   static /*@owned@*/ o_fctInfo *savedFcn = NULL;
 966   char *lineptr, *lineptr2;
 967   cstring importfile = inputStream_fileName (srce);
 968   char namestr[MAXBUFFLEN], kstr[20], sostr[MAXBUFFLEN];
 969   sort bsort, nullSort = sort_makeNoSort ();
 970   int col = 0;
 971   fileloc imploc = fileloc_undefined;
 972
 973
 974   if (inImport)
 975     {
 976       imploc = fileloc_createImport (importfile, inputStream_thisLineNumber (srce));
 977     }
 978
 979   if (firstWord (line, "op"))
 980     {
 981       lslOp op;
 982
 983       lineptr = strchr (line, 'o');     /* remove any leading blanks */
 984       llassert (lineptr != NULL);
 985       lineptr = strchr (lineptr, ' ');  /* go past "op" */
 986       llassert (lineptr != NULL);
 987
 988       /* add a newline to the end of the line since parseOpLine expects it */
 989       lineptr2 = strchr (lineptr, '\0');
 990
 991       if (lineptr2 != 0)
 992         {
 993           *lineptr2 = '\n';
 994           *(lineptr2 + 1) = '\0';
 995         }
 996
 997       llassert (cstring_isDefined (importfile));
 998       op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
 999
1000       if (op == (lslOp) 0)
1001         {
1002           lclplainerror
1003             (message
1004              ("%q: Imported file contains illegal operator declaration:\n "
1005               "skipping this line: %s",
1006               fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1007               cstring_fromChars (line)));
1008           fileloc_free (imploc);
1009           return;
1010         }
1011
1012             op = lslOp_renameSorts (map, op);
1013
1014       llassert (op != NULL);
1015       llassert (op->name != NULL);
1016
1017       symtable_enterOp (g_symtab, op->name,
1018                         sigNode_copy (op->signature));
1019           /*@-mustfree@*/ } /*@=mustfree@*/
1020   else if (firstWord (line, "type"))
1021     {
1022       typeInfo ti;
1023
1024       if (sscanf (line, "type %s %s %s", namestr, sostr, kstr) != 3)
1025         {
1026           lclplainerror
1027             (message ("%q: illegal type declaration:\n skipping this line: %s",
1028                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1029                       cstring_fromChars (line)));
1030           fileloc_free (imploc);
1031           return;
1032         }
1033
1034       ti = (typeInfo) dmalloc (sizeof (*ti));
1035       ti->id = ltoken_createFull (LLT_TYPEDEF_NAME, lsymbol_fromChars (namestr),
1036                                     importfile, inputStream_thisLineNumber (srce), col);
1037
1038       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1039
1040       if (sort_isNoSort (bsort))
1041         {
1042           lineptr = strchr (line, ' '); /* go past "type" */
1043           llassert (lineptr != NULL);
1044           lineptr = strchr (lineptr + 1, ' ');  /* go past namestr */
1045           llassert (lineptr != NULL);
1046           col = 5 + lineptr - line;     /* 5 for initial "%LCL "*/
1047
1048           lclbug (message ("%q: Imported files contains unknown base sort",
1049                            fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1050
1051           bsort = nullSort;
1052         }
1053       ti->basedOn = bsort;
1054
1055       if (strcmp (kstr, "exposed") == 0)
1056         {
1057           ti->abstract = FALSE;
1058           ti->modifiable = TRUE;
1059         }
1060       else
1061         {
1062           ti->abstract = TRUE;
1063           if (strcmp (kstr, "mutable") == 0)
1064             ti->modifiable = TRUE;
1065           else
1066             ti->modifiable = FALSE;
1067         }
1068       ti->export = TRUE;
1069
1070       /*
1071       ** sort of a hack to get imports to work...
1072       */
1073
1074       if (inImport)
1075         {
1076           cstring cnamestr = cstring_fromChars (namestr);
1077
1078           if (!usymtab_existsGlobEither (cnamestr))
1079             {
1080               (void) usymtab_addEntry
1081                 (uentry_makeDatatype (cnamestr, ctype_unknown,
1082                                       ti->abstract ? ynm_fromBool (ti->modifiable) : MAYBE,
1083                                       ti->abstract ? YES : NO,
1084                                       fileloc_copy (imploc)));
1085             }
1086         }
1087
1088       symtable_enterType (g_symtab, ti);
1089     }
1090   else if (firstWord (line, "var"))
1091     {
1092       varInfo vi;
1093
1094       if (sscanf (line, "var %s %s", namestr, sostr) != 2)
1095         {
1096           lclplainerror
1097             (message ("%q: Imported file contains illegal variable declaration.  "
1098                       "Skipping this line.",
1099                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce))));
1100           fileloc_free (imploc);
1101           return;
1102         }
1103
1104       vi = (varInfo) dmalloc (sizeof (*vi));
1105       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1106       lineptr = strchr (line, ' ');     /* go past "var" */
1107       llassert (lineptr != NULL);
1108       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1109       llassert (lineptr != NULL);
1110       col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1111
1112       if (sort_isNoSort (bsort))
1113         {
1114           lclplainerror (message ("%q: Imported file contains unknown base sort",
1115                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1116           bsort = nullSort;
1117         }
1118
1119       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1120                                   importfile, inputStream_thisLineNumber (srce), col);
1121       vi->sort = bsort;
1122       vi->kind = VRK_VAR;
1123       vi->export = TRUE;
1124       (void) symtable_enterVar (g_symtab, vi);
1125       varInfo_free (vi);
1126
1127       if (inImport)
1128         {
1129           cstring cnamestr = cstring_fromChars (namestr);
1130
1131           if (!usymtab_existsGlobEither (cnamestr))
1132             {
1133
1134               (void) usymtab_supEntrySref
1135                 (uentry_makeVariable (cnamestr, ctype_unknown,
1136                                       fileloc_copy (imploc),
1137                                       FALSE));
1138             }
1139         }
1140     }
1141   else if (firstWord (line, "const"))
1142     {
1143       varInfo vi;
1144
1145       if (sscanf (line, "const %s %s", namestr, sostr) != 2)
1146         {
1147           lclbug (message ("%q: Imported file contains illegal constant declaration: %s",
1148                            fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1149                            cstring_fromChars (line)));
1150           fileloc_free (imploc);
1151           return;
1152         }
1153
1154       vi = (varInfo) dmalloc (sizeof (*vi));
1155       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1156       lineptr = strchr (line, ' ');     /* go past "var" */
1157       llassert (lineptr != NULL);
1158       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1159       llassert (lineptr != NULL);
1160
1161       col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1162
1163       if (sort_isNoSort (bsort))
1164         {
1165           lclplainerror (message ("%q: Imported file contains unknown base sort",
1166                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1167           bsort = nullSort;
1168         }
1169
1170       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1171                                     importfile, inputStream_thisLineNumber (srce), col);
1172       vi->sort = bsort;
1173       vi->kind = VRK_CONST;
1174       vi->export = TRUE;
1175       (void) symtable_enterVar (g_symtab, vi);
1176       varInfo_free (vi);
1177
1178       if (inImport)
1179         {
1180           cstring cnamestr = cstring_fromChars (namestr);
1181
1182           if (!usymtab_existsGlobEither (cnamestr))
1183             {
1184
1185               (void) usymtab_addEntry (uentry_makeConstant (cnamestr,
1186                                                             ctype_unknown,
1187                                                             fileloc_copy (imploc)));
1188             }
1189         }
1190       /* must check for "fcnGlobals" before "fcn" */
1191     }
1192   else if (firstWord (line, "fcnGlobals"))
1193     {
1194       pairNodeList globals;
1195       lineptr = strchr (line, 'f');     /* remove any leading blanks */
1196       llassert (lineptr != NULL);
1197       lineptr = strchr (lineptr, ' ');  /* go past "fcnGlobals" */
1198       llassert (lineptr != NULL);
1199
1200      /* a quick check for empty fcnGlobals */
1201       if (!isBlankLine (lineptr))
1202         {
1203           globals = parseGlobals (lineptr, srce);
1204           /* should ensure that each global in an imported function
1205              corresponds to some existing global.  Since only
1206              "correctly processed" .lcs files are imported, this is
1207              true as an invariant. */
1208         }
1209       else
1210         {
1211           globals = pairNodeList_new ();
1212         }
1213
1214       /* check that they exist, store them on fctInfo */
1215
1216       if (savedFcn != NULL)
1217         {
1218           pairNodeList_free ((*savedFcn)->globals);
1219           (*savedFcn)->globals = globals;  /* evs, moved inside if predicate */
1220
1221           (void) symtable_enterFct (g_symtab, *savedFcn);
1222           savedFcn = NULL;
1223         }
1224       else
1225         {
1226           lclplainerror
1227             (message ("%q: Unexpected function globals.  "
1228                       "Skipping this line: \n%s",
1229                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1230                       cstring_fromChars (line)));
1231           savedFcn = NULL;
1232           pairNodeList_free (globals);
1233         }
1234     }
1235   else if (firstWord (line, "fcn"))
1236     {
1237       lslOp op;
1238       lslOp op2;
1239
1240       if (savedFcn != (fctInfo *) 0)
1241         {
1242           lclplainerror
1243             (message ("%q: illegal function declaration.  Skipping this line:\n%s",
1244                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1245                       cstring_fromChars (line)));
1246           fileloc_free (imploc);
1247           return;
1248         }
1249
1250       savedFcn = (fctInfo *) dmalloc (sizeof (*savedFcn));
1251
1252       lineptr = strchr (line, 'f');     /* remove any leading blanks */
1253       llassert (lineptr != NULL);
1254       lineptr = strchr (lineptr, ' ');  /* go past "fcn" */
1255       llassert (lineptr != NULL);
1256
1257       /* add a newline to the end of the line since parseOpLine expects it */
1258
1259       lineptr2 = strchr (lineptr, '\0');
1260
1261       if (lineptr2 != 0)
1262         {
1263           *lineptr2 = '\n';
1264           *(lineptr2 + 1) = '\0';
1265         }
1266
1267       op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
1268
1269       if (op == (lslOp) 0)
1270         {
1271           lclplainerror
1272             (message ("%q: illegal function declaration: %s",
1273                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1274                       cstring_fromChars (line)));
1275           fileloc_free (imploc);
1276           return;
1277         }
1278
1279       op2 = lslOp_renameSorts (map, op);
1280
1281       llassert (op2 != NULL);
1282
1283       if ((op->name != NULL) && op->name->isOpId)
1284         {
1285           (*savedFcn) = (fctInfo) dmalloc (sizeof (**savedFcn));
1286           (*savedFcn)->id = op->name->content.opid;
1287           (*savedFcn)->signature = signNode_fromsigNode (op2->signature);
1288           (*savedFcn)->globals = pairNodeList_new ();
1289           (*savedFcn)->export = TRUE;
1290
1291           if (inImport)
1292             {
1293               /* 27 Jan 1995 --- added this to be undefined namestr bug */
1294               cstring fname = ltoken_unparse ((*savedFcn)->id);
1295
1296               if (!usymtab_existsGlobEither (fname))
1297                 {
1298                   (void) usymtab_addEntry (uentry_makeFunction
1299                                            (fname, ctype_unknown,
1300                                             typeId_invalid, globSet_new (),
1301                                             sRefSet_undefined,
1302                                             warnClause_undefined,
1303                                             fileloc_copy (imploc)));
1304                 }
1305             }
1306         }
1307       else
1308         {
1309           /* evans 2001-05-27: detected by lclint after fixing external alias bug. */
1310           if (op->name != NULL)
1311             {
1312               ltoken_free (op->name->content.opid);
1313             }
1314
1315           lclplainerror
1316             (message ("%q: unexpected function name: %s",
1317                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1318                       cstring_fromChars (line)));
1319         }
1320     }
1321   else if (firstWord (line, "enumConst"))
1322     {
1323       varInfo vi;
1324
1325       if (sscanf (line, "enumConst %s %s", namestr, sostr) != 2)
1326         {
1327           lclplainerror
1328             (message ("%q: Illegal enum constant declaration.  "
1329                       "Skipping this line:\n%s",
1330                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1331                       cstring_fromChars (line)));
1332           fileloc_free (imploc);
1333           return;
1334         }
1335
1336       vi = (varInfo) dmalloc (sizeof (*vi));
1337       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1338       lineptr = strchr (line, ' ');     /* go past "var" */
1339       llassert (lineptr != NULL);
1340       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1341       llassert (lineptr != NULL);
1342
1343       col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1344       if (sort_isNoSort (bsort))
1345         {
1346           lclplainerror (message ("%q: unknown base sort\n",
1347                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1348           bsort = nullSort;
1349         }
1350
1351       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1352                                     importfile, inputStream_thisLineNumber (srce), col);
1353
1354       vi->sort = bsort;
1355       vi->kind = VRK_ENUM;
1356       vi->export = TRUE;
1357       (void) symtable_enterVar (g_symtab, vi);
1358       varInfo_free (vi);
1359
1360       if (inImport)
1361         {
1362           cstring cnamestr = cstring_fromChars (namestr);
1363           if (!usymtab_existsEither (cnamestr))
1364             {
1365                       (void) usymtab_addEntry (uentry_makeConstant (cnamestr, ctype_unknown,
1366                                                             fileloc_copy (imploc)));
1367             }
1368         }
1369     }
1370   else if (firstWord (line, "tag"))
1371     {
1372      /* do nothing, sort processing already handles this */
1373     }
1374   else
1375     {
1376       lclplainerror
1377         (message ("%q: Unknown symbol declaration.  Skipping this line:\n%s",
1378                   fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1379                   cstring_fromChars (line)));
1380     }
1381
1382     fileloc_free (imploc);
1383 }
1384
1385 void
1386 symtable_import (inputStream imported, ltoken tok, mapping map)
1387 {
1388   char *buf;
1389   cstring importfile;
1390   inputStream lclsource;
1391   int old_lsldebug;
1392   bool old_inImport = inImport;
1393
1394   buf = inputStream_nextLine (imported);
1395   importfile = inputStream_fileName (imported);
1396
1397   llassert (buf != NULL);
1398
1399   if (!firstWord (buf, "%LCLSymbolTable"))
1400     {
1401       lclsource = LCLScanSource ();
1402       lclfatalerror (tok,
1403                      message ("Expecting '%%LCLSymbolTable' line in import file %s:\n%s\n",
1404                               importfile,
1405                               cstring_fromChars (buf)));
1406     }
1407
1408   old_lsldebug = lsldebug;
1409   lsldebug = 0;
1410   allowed_redeclaration = TRUE;
1411   inImport = TRUE;
1412
1413   for (;;)
1414     {
1415       buf = inputStream_nextLine (imported);
1416       llassert (buf != NULL);
1417
1418
1419       if (firstWord (buf, "%LCLSymbolTableEnd"))
1420         {
1421           break;
1422         }
1423       else
1424         {                       /* a good line, remove %LCL from line first */
1425           if (firstWord (buf, "%LCL"))
1426             {
1427               parseLine (buf + 4, imported, map);
1428             }
1429           else
1430             {
1431               lclsource = LCLScanSource ();
1432               lclfatalerror
1433                 (tok,
1434                  message ("Expecting '%%LCL' prefix in import file %s:\n%s\n",
1435                           importfile,
1436                           cstring_fromChars (buf)));
1437             }
1438         }
1439     }
1440
1441   /* restore old value */
1442   inImport = old_inImport;
1443   lsldebug = old_lsldebug;
1444   allowed_redeclaration = FALSE;
1445   }
1446
1447 static void
1448 symtable_dumpId (symtable stable, FILE *f, bool lco)
1449 {
1450   idTable *st = stable->idTable;
1451   unsigned int i;
1452   idTableEntry *se;
1453   fctInfo fi;
1454   typeInfo ti;
1455   varInfo vi;
1456
1457   for (i = 1; i < st->size; i++)
1458     {
1459       /* 2/22/93 I think there is a off-by-1 error, 0 entry is never used */
1460       se = st->entries + i;
1461       llassert (se != NULL);
1462
1463
1464       /*@-loopswitchbreak@*/
1465       switch (se->kind)
1466         {
1467         case SYMK_FCN:
1468           {
1469             cstring tmp;
1470
1471             fi = (se->info).fct;
1472
1473             if (lco)
1474               {
1475                 fprintf (f, "%%LCL");
1476               }
1477
1478             if (!lco && !fi->export)
1479               {
1480                 fprintf (f, "spec ");
1481               }
1482
1483             tmp = signNode_unparse (fi->signature);
1484             fprintf (f, "fcn %s %s \n", ltoken_getTextChars (fi->id),
1485                      cstring_toCharsSafe (tmp));
1486             cstring_free (tmp);
1487
1488             tmp = pairNodeList_unparse (fi->globals);
1489             fprintf (f, "%%LCLfcnGlobals %s\n", cstring_toCharsSafe (tmp));
1490             cstring_free (tmp);
1491             break;
1492           }
1493         case SYMK_SCOPE:
1494           if (lco)
1495             {
1496               break;
1497             }
1498
1499           /*@-switchswitchbreak@*/
1500           switch ((se->info).scope->kind)
1501             {
1502             case SPE_GLOBAL:
1503               fprintf (f, "Global scope\n");
1504               break;
1505             case SPE_ABSTRACT:
1506               fprintf (f, "Abstract type scope\n");
1507               break;
1508             case SPE_FCN:
1509               fprintf (f, "Function scope\n");
1510               break;
1511              /* a let scope can only occur in a function scope, should not push
1512                 a new scope, so symtable_lookupInScope works properly
1513                    case letScope:
1514                      fprintf (f, "Let scope\n");
1515                      break; */
1516             case SPE_QUANT:
1517               fprintf (f, "Quantifier scope\n");
1518               break;
1519             case SPE_CLAIM:
1520               fprintf (f, "Claim scope\n");
1521               break;
1522             case SPE_INVALID:
1523               break;
1524             }
1525           break;
1526         case SYMK_TYPE:
1527           ti = (se->info).type;
1528           if (lco)
1529             fprintf (f, "%%LCL");
1530           if (!lco && !ti->export)
1531             fprintf (f, "spec ");
1532           fprintf (f, "type %s %s",
1533                    ltoken_getTextChars (ti->id), sort_getName (ti->basedOn));
1534           if (ti->abstract)
1535             {
1536               if (ti->modifiable)
1537                 fprintf (f, " mutable\n");
1538               else
1539                 fprintf (f, " immutable\n");
1540             }
1541           else
1542             fprintf (f, " exposed\n");
1543           break;
1544         case SYMK_VAR:
1545
1546           vi = (se->info).var;
1547           if (lco)
1548             {
1549               fprintf (f, "%%LCL");
1550             }
1551
1552           if (!lco && !vi->export)
1553             {
1554               fprintf (f, "spec ");
1555             }
1556           switch (vi->kind)
1557             {
1558             case VRK_CONST:
1559               fprintf (f, "const %s %s\n",
1560                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1561               break;
1562             case VRK_VAR:
1563               fprintf (f, "var %s %s\n",
1564                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1565               break;
1566             case VRK_ENUM:
1567               fprintf (f, "enumConst %s %s\n",
1568                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1569               break;
1570             default:
1571               if (lco)
1572                 {
1573                   switch (vi->kind)
1574                     {
1575                     case VRK_GLOBAL:
1576                       fprintf (f, "global %s %s\n", ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1577                       break;
1578                     case VRK_PRIVATE:   /* for private vars within function */
1579                       fprintf (f, "local %s %s\n",
1580                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1581                       break;
1582                     case VRK_LET:
1583                       fprintf (f, "let %s %s\n",
1584                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1585                       break;
1586                     case VRK_PARAM:
1587                       fprintf (f, "param %s %s\n",
1588                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1589                       break;
1590                     case VRK_QUANT:
1591                       fprintf (f, "quant %s %s\n",
1592                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1593                       break;
1594                     BADDEFAULT;
1595                     }
1596                   /*@=loopswitchbreak@*/
1597                   /*@=switchswitchbreak@*/
1598                 }
1599             }
1600         }
1601     }
1602 }
1603
1604 static /*@exposed@*/ /*@out@*/ idTableEntry *
1605 nextFree (idTable * st)
1606 {
1607   idTableEntry *ret;
1608   unsigned int n = st->size;
1609
1610   if (n >= st->allocated)
1611     {
1612       /*
1613       ** this loses with the garbage collector
1614       ** (and realloc is notoriously dangerous)
1615       **
1616       ** st->entries = (idTableEntry *) LSLMoreMem (st->entries, (n + DELTA)
1617       **                                * sizeof (idTableEntry));
1618       **
1619       ** instead, we copy the symtable...
1620       */
1621
1622       idTableEntry *oldentries = st->entries;
1623       unsigned int i;
1624
1625       st->entries = dmalloc ((n+DELTA) * sizeof (*st->entries));
1626
1627       for (i = 0; i < n; i++)
1628         {
1629           st->entries[i] = oldentries[i];
1630         }
1631
1632       sfree (oldentries);
1633
1634       st->allocated = n + DELTA;
1635     }
1636
1637   ret = &(st->entries[st->size]);
1638   st->size++;
1639   return ret;
1640 }
1641
1642
1643 static /*@dependent@*/ /*@null@*/ idTableEntry *
1644   symtable_lookup (idTable *st, lsymbol id)
1645 {
1646   int n;
1647   idTableEntry *e;
1648
1649   for (n = st->size - 1; n >= 0; n--)
1650     {
1651       e = &(st->entries[n]);
1652
1653       /*@-loopswitchbreak@*/
1654       switch (e->kind)
1655         {
1656         case SYMK_SCOPE:
1657           break;
1658         case SYMK_FCN:
1659           if (ltoken_getText (e->info.fct->id) == id) return e;
1660           break;
1661         case SYMK_TYPE:
1662           if (ltoken_getText (e->info.type->id) == id) return e;
1663           break;
1664         case SYMK_VAR:
1665           if (ltoken_getText (e->info.var->id) == id) return e;
1666           break;
1667         BADDEFAULT;
1668         }
1669       /*@=loopswitchbreak@*/
1670     }
1671
1672   return (idTableEntry *) 0;
1673 }
1674
1675
1676 static /*@dependent@*/ /*@null@*/ idTableEntry *
1677   symtable_lookupInScope (idTable *st, lsymbol id)
1678 {
1679   int n;
1680   idTableEntry *e;
1681   for (n = st->size - 1; n >= 0; n--)
1682     {
1683       e = &(st->entries[n]);
1684       if (e->kind == SYMK_SCOPE)
1685         break;
1686       if (ltoken_getText (e->info.fct->id) == id)
1687         {
1688           return e;
1689         }
1690     }
1691   return (idTableEntry *) 0;
1692 }
1693
1694 /* hash table implementation */
1695
1696 static symbolKey
1697 htData_key (htData * x)
1698 {
1699   /* assume x points to a valid htData struct */
1700   switch (x->kind)
1701     {
1702     case IK_SORT:
1703       return x->content.sort;
1704     case IK_OP:
1705       {                         /* get the textSym of the token */
1706         nameNode n = (x->content.op)->name;
1707
1708         if (n->isOpId)
1709           {
1710             return ltoken_getText (n->content.opid);
1711           }
1712         else
1713           {
1714             llassert (n->content.opform != NULL);
1715             return (n->content.opform)->key;
1716           }
1717       }
1718     case IK_TAG:
1719       return ltoken_getText ((x->content).tag->id);
1720     }
1721   BADEXIT;
1722 }
1723
1724 static void htData_free (/*@null@*/ /*@only@*/ htData *d)
1725 {
1726   if (d != NULL)
1727     {
1728       switch (d->kind)
1729         {
1730         case IK_SORT:
1731           break;
1732         case IK_OP:
1733           /* nameNode_free (d->content.op->name);*/
1734           sigNodeSet_free (d->content.op->signatures);
1735           break;
1736         case IK_TAG:
1737           {
1738             switch (d->content.tag->kind)
1739               {
1740               case TAG_STRUCT:
1741               case TAG_UNION:
1742               case TAG_FWDSTRUCT:
1743               case TAG_FWDUNION:
1744                 /*
1745                  ** no: stDeclNodeList_free (d->content.tag->content.decls);
1746                  **     it is dependent!
1747                  */
1748                 /*@switchbreak@*/ break;
1749               case TAG_ENUM:
1750
1751                 /* no: ltokenList_free (d->content.tag->content.enums);
1752                  **     it is dependent!
1753                  */
1754
1755                 /*@switchbreak@*/ break;
1756               }
1757           }
1758         }
1759
1760       sfree (d);
1761     }
1762 }
1763
1764 static void bucket_free (/*@null@*/ /*@only@*/ bucket *b)
1765 {
1766   if (b != NULL)
1767     {
1768       bucket_free (b->next);
1769       htData_free (b->data);
1770       sfree (b);
1771     }
1772 }
1773
1774 static void symHashTable_free (/*@only@*/ symHashTable *h)
1775 {
1776   unsigned int i;
1777
1778   for (i = 0; i < h->size; i++)
1779     {
1780       bucket_free (h->buckets[i]);
1781     }
1782
1783   sfree (h->buckets);
1784   sfree (h);
1785 }
1786
1787 static /*@only@*/ symHashTable *
1788 symHashTable_create (unsigned int size)
1789 {
1790   unsigned int i;
1791   symHashTable *t = (symHashTable *) dmalloc (sizeof (*t));
1792
1793   t->buckets = (bucket **) dmalloc ((size + 1) * sizeof (*t->buckets));
1794   t->count = 0;
1795   t->size = size;
1796
1797   for (i = 0; i <= size; i++)
1798     {
1799       t->buckets[i] = (bucket *) NULL;
1800     }
1801
1802   return t;
1803 }
1804
1805 static /*@null@*/ /*@exposed@*/ htData *
1806 symHashTable_get (symHashTable *t, symbolKey key, infoKind kind, /*@null@*/ nameNode n)
1807 {
1808   bucket *b;
1809   htEntry *entry;
1810   htData *d;
1811
1812   b = t->buckets[MASH (key, kind)];
1813   if (b == (bucket *) 0)
1814     {
1815       return ((htData *) 0);
1816     }
1817
1818   for (entry = (htEntry *) b; entry != NULL; entry = entry->next)
1819     {
1820       d = entry->data;
1821
1822       if (d->kind == kind && htData_key (d) == key)
1823         if (kind != IK_OP || sameNameNode (n, d->content.op->name))
1824           {
1825             return d;
1826           }
1827     }
1828   return ((htData *) 0);
1829 }
1830
1831 static bool
1832 symHashTable_put (symHashTable *t, /*@only@*/ htData *data)
1833 {
1834   /* if key is already taken, don't insert, return FALSE
1835      else insert it and return TRUE. */
1836   symbolKey key;
1837   htData *oldd;
1838   infoKind kind;
1839   nameNode name;
1840
1841   key = htData_key (data);
1842   kind = data->kind;
1843
1844   if (kind == IK_OP && (!data->content.op->name->isOpId))
1845     {
1846       name = data->content.op->name;
1847     }
1848   else
1849     {
1850       name = (nameNode) 0;
1851     }
1852
1853   oldd = symHashTable_get (t, key, kind, name);
1854
1855   if (oldd == (htData *) 0)
1856     {
1857       /*@-deparrays@*/
1858       bucket *new_entry = (bucket *) dmalloc (sizeof (*new_entry));
1859       bucket *b = (t->buckets[MASH (key, kind)]);
1860       htEntry *entry = (htEntry *) b;
1861       /*@=deparrays@*/
1862
1863       new_entry->data = data;
1864       new_entry->next = entry;
1865       t->buckets[MASH (key, kind)] = new_entry;
1866       t->count++;
1867
1868       return TRUE;
1869     }
1870   else
1871     {
1872       htData_free (data);
1873     }
1874
1875   return FALSE;
1876 }
1877
1878 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
1879   symHashTable_forcePut (symHashTable *t, /*@only@*/ htData *data)
1880 {
1881   /* Put data in, return old value */
1882   symbolKey key;
1883   bucket *b;
1884   htData *oldd;
1885   htEntry *entry, *new_entry;
1886   infoKind kind;
1887   nameNode name;
1888
1889   key = htData_key (data);
1890   kind = data->kind;
1891
1892   if (kind == IK_OP && (!data->content.op->name->isOpId))
1893     {
1894       name = data->content.op->name;
1895     }
1896   else
1897     {
1898       name = (nameNode) 0;
1899     }
1900
1901   oldd = symHashTable_get (t, key, kind, name);
1902
1903   if (oldd == (htData *) 0)
1904     {
1905       new_entry = (htEntry *) dmalloc (sizeof (*new_entry));
1906
1907       /*@-deparrays@*/
1908       b = t->buckets[MASH (key, kind)];
1909       /*@=deparrays@*/
1910
1911       entry = b;
1912       new_entry->data = data;
1913       new_entry->next = entry;
1914       t->buckets[MASH (key, kind)] = new_entry;
1915       t->count++;
1916
1917       return NULL;
1918     }
1919   else
1920     {                           /* modify in place */
1921       *oldd = *data;            /* copy new info over to old info */
1922
1923       /* dangerous: if the data is the same, don't free it */
1924       if (data != oldd)
1925         {
1926           sfree (data);
1927         /*@-branchstate@*/
1928         }
1929       /*@=branchstate@*/
1930
1931       return oldd;
1932     }
1933 }
1934
1935 #if 0
1936 static unsigned int
1937 symHashTable_count (symHashTable * t)
1938 {
1939   return (t->count);
1940 }
1941
1942 #endif
1943
1944 static void
1945 symHashTable_printStats (symHashTable * t)
1946 {
1947   int i, bucketCount, setsize, sortCount, opCount, tagCount;
1948   int sortTotal, opTotal, tagTotal;
1949   bucket *b;
1950   htEntry *entry;
1951   htData *d;
1952
1953   sortTotal = 0;
1954   opTotal = 0;
1955   tagTotal = 0;
1956   sortCount = 0;
1957   opCount = 0;
1958   tagCount = 0;
1959
1960   /* for debugging only */
1961   printf ("\n Printing symHashTable stats ... \n");
1962   for (i = 0; i <= HT_MAXINDEX; i++)
1963     {
1964       b = t->buckets[i];
1965       bucketCount = 0;
1966       for (entry = b; entry != NULL; entry = entry->next)
1967         {
1968           d = entry->data;
1969           bucketCount++;
1970           switch (d->kind)
1971             {
1972             case IK_SORT:
1973               sortCount++;
1974               /*@switchbreak@*/ break;
1975             case IK_OP:
1976               {
1977                 cstring name = nameNode_unparse (d->content.op->name);
1978                 cstring sigs = sigNodeSet_unparse (d->content.op->signatures);
1979                 opCount++;
1980                 /* had a tt? */
1981                 setsize = sigNodeSet_size (d->content.op->signatures);
1982                 printf ("       Op (%d): %s %s\n", setsize,
1983                         cstring_toCharsSafe (name),
1984                         cstring_toCharsSafe (sigs));
1985                 cstring_free (name);
1986                 cstring_free (sigs);
1987                 /*@switchbreak@*/ break;
1988               }
1989             case IK_TAG:
1990               tagCount++;
1991               /*@switchbreak@*/ break;
1992             }
1993         }
1994       if (bucketCount > 0)
1995         {
1996           printf ("   Bucket %d has count = %d; opCount = %d; sortCount = %d; tagCount = %d\n", i, bucketCount, opCount, sortCount, tagCount);
1997           sortTotal += sortCount;
1998           tagTotal += tagCount;
1999           opTotal += opCount;
2000         }
2001     }
2002   printf ("SymHashTable has total count = %d, opTotal = %d, sortTotal = %d, tagTotal = %d :\n", t->count, opTotal, sortTotal, tagTotal);
2003
2004 }
2005
2006 void
2007 symtable_printStats (symtable s)
2008 {
2009   symHashTable_printStats (s->hTable);
2010  /* for debugging only */
2011   printf ("idTable size = %d; allocated = %d\n",
2012           s->idTable->size, s->idTable->allocated);
2013 }
2014
2015 /*@only@*/ cstring
2016 tagKind_unparse (tagKind k)
2017 {
2018   switch (k)
2019     {
2020     case TAG_STRUCT:
2021     case TAG_FWDSTRUCT:
2022       return cstring_makeLiteral ("struct");
2023     case TAG_UNION:
2024     case TAG_FWDUNION:
2025       return cstring_makeLiteral ("union");
2026     case TAG_ENUM:
2027       return cstring_makeLiteral ("enum");
2028     }
2029   BADEXIT;
2030 }
2031
2032 static void tagInfo_free (/*@only@*/ tagInfo tag)
2033 {
2034   ltoken_free (tag->id);
2035   sfree (tag);
2036 }
2037
2038 /*@observer@*/ sigNodeSet
2039   symtable_possibleOps (symtable tab, nameNode n)
2040 {
2041   opInfo oi = symtable_opInfo (tab, n);
2042
2043   if (opInfo_exists (oi))
2044     {
2045       return (oi->signatures);
2046     }
2047
2048   return sigNodeSet_undefined;
2049 }
2050
2051 bool
2052 symtable_opExistsWithArity (symtable tab, nameNode n, int arity)
2053 {
2054   opInfo oi = symtable_opInfo (tab, n);
2055
2056   if (opInfo_exists (oi))
2057     {
2058       sigNodeSet sigs = oi->signatures;
2059       sigNodeSet_elements (sigs, sig)
2060       {
2061         if (ltokenList_size (sig->domain) == arity)
2062           return TRUE;
2063       } end_sigNodeSet_elements;
2064     }
2065   return FALSE;
2066 }
2067
2068 static bool
2069 domainMatches (ltokenList domain, sortSetList argSorts)
2070 {
2071   /* expect their length to match */
2072   /* each domain sort in op must be an element of
2073      the corresponding set in argSorts. */
2074   bool matched = TRUE;
2075   sort s;
2076
2077   sortSetList_reset (argSorts);
2078   ltokenList_elements (domain, dom)
2079     {
2080       s = sort_fromLsymbol (ltoken_getText (dom));
2081       if (!(sortSet_member (sortSetList_current (argSorts), s)))
2082         {
2083           /*      printf ("   mismatched element is: %s in %s\n", ltoken_getTextChars (*dom),
2084                   sortSet_unparse (sortSetList_current (argSorts))); */
2085           matched = FALSE;
2086           break;
2087         }
2088       sortSetList_advance (argSorts);
2089   } end_ltokenList_elements;
2090
2091   return matched;
2092 }
2093
2094 /*@only@*/ lslOpSet
2095   symtable_opsWithLegalDomain (symtable tab, /*@temp@*/ /*@null@*/ nameNode n,
2096                                sortSetList argSorts, sort qual)
2097 {
2098  /* handles nil qual */
2099   lslOpSet ops = lslOpSet_new ();
2100   lslOp op;
2101   sort rangeSort;
2102   opInfo oi;
2103
2104   llassert (n != NULL);
2105   oi = symtable_opInfo (tab, n);
2106
2107   if (opInfo_exists (oi))
2108     {
2109       sigNodeSet sigs = oi->signatures;
2110
2111       sigNodeSet_elements (sigs, sig)
2112         {
2113           if (ltokenList_size (sig->domain) == sortSetList_size (argSorts))
2114             {
2115               rangeSort = sigNode_rangeSort (sig);
2116
2117               if ((qual == 0) || (sort_equal (rangeSort, qual)))
2118                 {
2119                   if (domainMatches (sig->domain, argSorts))
2120                     {
2121                       op = (lslOp) dmalloc (sizeof (*op));
2122
2123                       /* each domain sort in op must be an element of
2124                          the corresponding set in argSorts. */
2125                       op->signature = sig;
2126                       op->name = nameNode_copy (n);
2127                       (void) lslOpSet_insert (ops, op);
2128                     }
2129                 }
2130             }
2131         } end_sigNodeSet_elements;
2132     }
2133   return ops;
2134 }