src/symtable.c

   1 /*
   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 ** 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 "splintMacros.nf"
  44 # include "basic.h"
  45 # include "lslparse.h"
  46 # include "lclscan.h"
  47 # include "lclsyntable.h"
  48 # include "llgrammar.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 + ((int) (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
1082                  (cnamestr, ctype_unknown,
1083                   ti->abstract ? ynm_fromBool (ti->modifiable) : MAYBE,
1084                   ti->abstract ? qual_createAbstract () : qual_createConcrete (),
1085                   fileloc_copy (imploc)));
1086             }
1087         }
1088
1089       symtable_enterType (g_symtab, ti);
1090     }
1091   else if (firstWord (line, "var"))
1092     {
1093       varInfo vi;
1094
1095       if (sscanf (line, "var %s %s", namestr, sostr) != 2)
1096         {
1097           lclplainerror
1098             (message ("%q: Imported file contains illegal variable declaration.  "
1099                       "Skipping this line.",
1100                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce))));
1101           fileloc_free (imploc);
1102           return;
1103         }
1104
1105       vi = (varInfo) dmalloc (sizeof (*vi));
1106       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1107       lineptr = strchr (line, ' ');     /* go past "var" */
1108       llassert (lineptr != NULL);
1109       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1110       llassert (lineptr != NULL);
1111       col = 5 + ((int) (lineptr - line));       /* 5 for initial "%LCL "*/
1112
1113       if (sort_isNoSort (bsort))
1114         {
1115           lclplainerror (message ("%q: Imported file contains unknown base sort",
1116                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1117           bsort = nullSort;
1118         }
1119
1120       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1121                                   importfile, inputStream_thisLineNumber (srce), col);
1122       vi->sort = bsort;
1123       vi->kind = VRK_VAR;
1124       vi->export = TRUE;
1125       (void) symtable_enterVar (g_symtab, vi);
1126       varInfo_free (vi);
1127
1128       if (inImport)
1129         {
1130           cstring cnamestr = cstring_fromChars (namestr);
1131
1132           if (!usymtab_existsGlobEither (cnamestr))
1133             {
1134
1135               (void) usymtab_supEntrySref
1136                 (uentry_makeVariable (cnamestr, ctype_unknown,
1137                                       fileloc_copy (imploc),
1138                                       FALSE));
1139             }
1140         }
1141     }
1142   else if (firstWord (line, "const"))
1143     {
1144       varInfo vi;
1145
1146       if (sscanf (line, "const %s %s", namestr, sostr) != 2)
1147         {
1148           lclbug (message ("%q: Imported file contains illegal constant declaration: %s",
1149                            fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1150                            cstring_fromChars (line)));
1151           fileloc_free (imploc);
1152           return;
1153         }
1154
1155       vi = (varInfo) dmalloc (sizeof (*vi));
1156       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1157       lineptr = strchr (line, ' ');     /* go past "var" */
1158       llassert (lineptr != NULL);
1159       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1160       llassert (lineptr != NULL);
1161
1162       col = 5 + ((int) (lineptr - line));       /* 5 for initial "%LCL "*/
1163
1164       if (sort_isNoSort (bsort))
1165         {
1166           lclplainerror (message ("%q: Imported file contains unknown base sort",
1167                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1168           bsort = nullSort;
1169         }
1170
1171       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1172                                     importfile, inputStream_thisLineNumber (srce), col);
1173       vi->sort = bsort;
1174       vi->kind = VRK_CONST;
1175       vi->export = TRUE;
1176       (void) symtable_enterVar (g_symtab, vi);
1177       varInfo_free (vi);
1178
1179       if (inImport)
1180         {
1181           cstring cnamestr = cstring_fromChars (namestr);
1182
1183           if (!usymtab_existsGlobEither (cnamestr))
1184             {
1185
1186               (void) usymtab_addEntry (uentry_makeConstant (cnamestr,
1187                                                             ctype_unknown,
1188                                                             fileloc_copy (imploc)));
1189             }
1190         }
1191       /* must check for "fcnGlobals" before "fcn" */
1192     }
1193   else if (firstWord (line, "fcnGlobals"))
1194     {
1195       pairNodeList globals;
1196       lineptr = strchr (line, 'f');     /* remove any leading blanks */
1197       llassert (lineptr != NULL);
1198       lineptr = strchr (lineptr, ' ');  /* go past "fcnGlobals" */
1199       llassert (lineptr != NULL);
1200
1201      /* a quick check for empty fcnGlobals */
1202       if (!isBlankLine (lineptr))
1203         {
1204           globals = parseGlobals (lineptr, srce);
1205           /* should ensure that each global in an imported function
1206              corresponds to some existing global.  Since only
1207              "correctly processed" .lcs files are imported, this is
1208              true as an invariant. */
1209         }
1210       else
1211         {
1212           globals = pairNodeList_new ();
1213         }
1214
1215       /* check that they exist, store them on fctInfo */
1216
1217       if (savedFcn != NULL)
1218         {
1219           pairNodeList_free ((*savedFcn)->globals);
1220           (*savedFcn)->globals = globals;  /* evs, moved inside if predicate */
1221
1222           (void) symtable_enterFct (g_symtab, *savedFcn);
1223           savedFcn = NULL;
1224         }
1225       else
1226         {
1227           lclplainerror
1228             (message ("%q: Unexpected function globals.  "
1229                       "Skipping this line: \n%s",
1230                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1231                       cstring_fromChars (line)));
1232           savedFcn = NULL;
1233           pairNodeList_free (globals);
1234         }
1235     }
1236   else if (firstWord (line, "fcn"))
1237     {
1238       lslOp op;
1239       lslOp op2;
1240
1241       if (savedFcn != (fctInfo *) 0)
1242         {
1243           lclplainerror
1244             (message ("%q: illegal function declaration.  Skipping this line:\n%s",
1245                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1246                       cstring_fromChars (line)));
1247           fileloc_free (imploc);
1248           return;
1249         }
1250
1251       savedFcn = (fctInfo *) dmalloc (sizeof (*savedFcn));
1252
1253       lineptr = strchr (line, 'f');     /* remove any leading blanks */
1254       llassert (lineptr != NULL);
1255       lineptr = strchr (lineptr, ' ');  /* go past "fcn" */
1256       llassert (lineptr != NULL);
1257
1258       /* add a newline to the end of the line since parseOpLine expects it */
1259
1260       lineptr2 = strchr (lineptr, '\0');
1261
1262       if (lineptr2 != 0)
1263         {
1264           *lineptr2 = '\n';
1265           *(lineptr2 + 1) = '\0';
1266         }
1267
1268       op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
1269
1270       if (op == (lslOp) 0)
1271         {
1272           lclplainerror
1273             (message ("%q: illegal function declaration: %s",
1274                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1275                       cstring_fromChars (line)));
1276           fileloc_free (imploc);
1277           return;
1278         }
1279
1280       op2 = lslOp_renameSorts (map, op);
1281
1282       llassert (op2 != NULL);
1283
1284       if ((op->name != NULL) && op->name->isOpId)
1285         {
1286           (*savedFcn) = (fctInfo) dmalloc (sizeof (**savedFcn));
1287           (*savedFcn)->id = op->name->content.opid;
1288           (*savedFcn)->signature = signNode_fromsigNode (op2->signature);
1289           (*savedFcn)->globals = pairNodeList_new ();
1290           (*savedFcn)->export = TRUE;
1291
1292           if (inImport)
1293             {
1294               /* 27 Jan 1995 --- added this to be undefined namestr bug */
1295               cstring fname = ltoken_unparse ((*savedFcn)->id);
1296
1297               if (!usymtab_existsGlobEither (fname))
1298                 {
1299                   (void) usymtab_addEntry (uentry_makeFunction
1300                                            (fname, ctype_unknown,
1301                                             typeId_invalid, globSet_new (),
1302                                             sRefSet_undefined,
1303                                             warnClause_undefined,
1304                                             fileloc_copy (imploc)));
1305                 }
1306             }
1307         }
1308       else
1309         {
1310           /* evans 2001-05-27: detected by splint after fixing external alias bug. */
1311           if (op->name != NULL)
1312             {
1313               ltoken_free (op->name->content.opid);
1314             }
1315
1316           lclplainerror
1317             (message ("%q: unexpected function name: %s",
1318                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1319                       cstring_fromChars (line)));
1320         }
1321     }
1322   else if (firstWord (line, "enumConst"))
1323     {
1324       varInfo vi;
1325
1326       if (sscanf (line, "enumConst %s %s", namestr, sostr) != 2)
1327         {
1328           lclplainerror
1329             (message ("%q: Illegal enum constant declaration.  "
1330                       "Skipping this line:\n%s",
1331                       fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1332                       cstring_fromChars (line)));
1333           fileloc_free (imploc);
1334           return;
1335         }
1336
1337       vi = (varInfo) dmalloc (sizeof (*vi));
1338       bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1339       lineptr = strchr (line, ' ');     /* go past "var" */
1340       llassert (lineptr != NULL);
1341       lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
1342       llassert (lineptr != NULL);
1343
1344       col = 5 + ((int) (lineptr - line));       /* 5 for initial "%LCL "*/
1345       if (sort_isNoSort (bsort))
1346         {
1347           lclplainerror (message ("%q: unknown base sort\n",
1348                                   fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1349           bsort = nullSort;
1350         }
1351
1352       vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1353                                     importfile, inputStream_thisLineNumber (srce), col);
1354
1355       vi->sort = bsort;
1356       vi->kind = VRK_ENUM;
1357       vi->export = TRUE;
1358       (void) symtable_enterVar (g_symtab, vi);
1359       varInfo_free (vi);
1360
1361       if (inImport)
1362         {
1363           cstring cnamestr = cstring_fromChars (namestr);
1364           if (!usymtab_existsEither (cnamestr))
1365             {
1366                       (void) usymtab_addEntry (uentry_makeConstant (cnamestr, ctype_unknown,
1367                                                             fileloc_copy (imploc)));
1368             }
1369         }
1370     }
1371   else if (firstWord (line, "tag"))
1372     {
1373      /* do nothing, sort processing already handles this */
1374     }
1375   else
1376     {
1377       lclplainerror
1378         (message ("%q: Unknown symbol declaration.  Skipping this line:\n%s",
1379                   fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1380                   cstring_fromChars (line)));
1381     }
1382
1383     fileloc_free (imploc);
1384 }
1385
1386 void
1387 symtable_import (inputStream imported, ltoken tok, mapping map)
1388 {
1389   char *buf;
1390   cstring importfile;
1391   inputStream lclsource;
1392   int old_lsldebug;
1393   bool old_inImport = inImport;
1394
1395   buf = inputStream_nextLine (imported);
1396   importfile = inputStream_fileName (imported);
1397
1398   llassert (buf != NULL);
1399
1400   if (!firstWord (buf, "%LCLSymbolTable"))
1401     {
1402       lclsource = LCLScanSource ();
1403       lclfatalerror (tok,
1404                      message ("Expecting '%%LCLSymbolTable' line in import file %s:\n%s\n",
1405                               importfile,
1406                               cstring_fromChars (buf)));
1407     }
1408
1409   old_lsldebug = lsldebug;
1410   lsldebug = 0;
1411   allowed_redeclaration = TRUE;
1412   inImport = TRUE;
1413
1414   for (;;)
1415     {
1416       buf = inputStream_nextLine (imported);
1417       llassert (buf != NULL);
1418
1419
1420       if (firstWord (buf, "%LCLSymbolTableEnd"))
1421         {
1422           break;
1423         }
1424       else
1425         {                       /* a good line, remove %LCL from line first */
1426           if (firstWord (buf, "%LCL"))
1427             {
1428               parseLine (buf + 4, imported, map);
1429             }
1430           else
1431             {
1432               lclsource = LCLScanSource ();
1433               lclfatalerror
1434                 (tok,
1435                  message ("Expecting '%%LCL' prefix in import file %s:\n%s\n",
1436                           importfile,
1437                           cstring_fromChars (buf)));
1438             }
1439         }
1440     }
1441
1442   /* restore old value */
1443   inImport = old_inImport;
1444   lsldebug = old_lsldebug;
1445   allowed_redeclaration = FALSE;
1446   }
1447
1448 static void
1449 symtable_dumpId (symtable stable, FILE *f, bool lco)
1450 {
1451   idTable *st = stable->idTable;
1452   unsigned int i;
1453   idTableEntry *se;
1454   fctInfo fi;
1455   typeInfo ti;
1456   varInfo vi;
1457
1458   for (i = 1; i < st->size; i++)
1459     {
1460       /* 2/22/93 I think there is a off-by-1 error, 0 entry is never used */
1461       se = st->entries + i;
1462       llassert (se != NULL);
1463
1464
1465       /*@-loopswitchbreak@*/
1466       switch (se->kind)
1467         {
1468         case SYMK_FCN:
1469           {
1470             cstring tmp;
1471
1472             fi = (se->info).fct;
1473
1474             if (lco)
1475               {
1476                 fprintf (f, "%%LCL");
1477               }
1478
1479             if (!lco && !fi->export)
1480               {
1481                 fprintf (f, "spec ");
1482               }
1483
1484             tmp = signNode_unparse (fi->signature);
1485             fprintf (f, "fcn %s %s \n", ltoken_getTextChars (fi->id),
1486                      cstring_toCharsSafe (tmp));
1487             cstring_free (tmp);
1488
1489             tmp = pairNodeList_unparse (fi->globals);
1490             fprintf (f, "%%LCLfcnGlobals %s\n", cstring_toCharsSafe (tmp));
1491             cstring_free (tmp);
1492             break;
1493           }
1494         case SYMK_SCOPE:
1495           if (lco)
1496             {
1497               break;
1498             }
1499
1500           /*@-switchswitchbreak@*/
1501           switch ((se->info).scope->kind)
1502             {
1503             case SPE_GLOBAL:
1504               fprintf (f, "Global scope\n");
1505               break;
1506             case SPE_ABSTRACT:
1507               fprintf (f, "Abstract type scope\n");
1508               break;
1509             case SPE_FCN:
1510               fprintf (f, "Function scope\n");
1511               break;
1512              /* a let scope can only occur in a function scope, should not push
1513                 a new scope, so symtable_lookupInScope works properly
1514                    case letScope:
1515                      fprintf (f, "Let scope\n");
1516                      break; */
1517             case SPE_QUANT:
1518               fprintf (f, "Quantifier scope\n");
1519               break;
1520             case SPE_CLAIM:
1521               fprintf (f, "Claim scope\n");
1522               break;
1523             case SPE_INVALID:
1524               break;
1525             }
1526           break;
1527         case SYMK_TYPE:
1528           ti = (se->info).type;
1529           if (lco)
1530             fprintf (f, "%%LCL");
1531           if (!lco && !ti->export)
1532             fprintf (f, "spec ");
1533           fprintf (f, "type %s %s",
1534                    ltoken_getTextChars (ti->id), sort_getName (ti->basedOn));
1535           if (ti->abstract)
1536             {
1537               if (ti->modifiable)
1538                 fprintf (f, " mutable\n");
1539               else
1540                 fprintf (f, " immutable\n");
1541             }
1542           else
1543             fprintf (f, " exposed\n");
1544           break;
1545         case SYMK_VAR:
1546
1547           vi = (se->info).var;
1548           if (lco)
1549             {
1550               fprintf (f, "%%LCL");
1551             }
1552
1553           if (!lco && !vi->export)
1554             {
1555               fprintf (f, "spec ");
1556             }
1557           switch (vi->kind)
1558             {
1559             case VRK_CONST:
1560               fprintf (f, "const %s %s\n",
1561                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1562               break;
1563             case VRK_VAR:
1564               fprintf (f, "var %s %s\n",
1565                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1566               break;
1567             case VRK_ENUM:
1568               fprintf (f, "enumConst %s %s\n",
1569                        ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1570               break;
1571             default:
1572               if (lco)
1573                 {
1574                   switch (vi->kind)
1575                     {
1576                     case VRK_GLOBAL:
1577                       fprintf (f, "global %s %s\n", ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1578                       break;
1579                     case VRK_PRIVATE:   /* for private vars within function */
1580                       fprintf (f, "local %s %s\n",
1581                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1582                       break;
1583                     case VRK_LET:
1584                       fprintf (f, "let %s %s\n",
1585                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1586                       break;
1587                     case VRK_PARAM:
1588                       fprintf (f, "param %s %s\n",
1589                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1590                       break;
1591                     case VRK_QUANT:
1592                       fprintf (f, "quant %s %s\n",
1593                                ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1594                       break;
1595                     BADDEFAULT;
1596                     }
1597                   /*@=loopswitchbreak@*/
1598                   /*@=switchswitchbreak@*/
1599                 }
1600             }
1601         }
1602     }
1603 }
1604
1605 static /*@exposed@*/ /*@out@*/ idTableEntry *
1606 nextFree (idTable * st)
1607 {
1608   idTableEntry *ret;
1609   unsigned int n = st->size;
1610
1611   if (n >= st->allocated)
1612     {
1613       /*
1614       ** this loses with the garbage collector
1615       ** (and realloc is notoriously dangerous)
1616       **
1617       ** st->entries = (idTableEntry *) LSLMoreMem (st->entries, (n + DELTA)
1618       **                                * sizeof (idTableEntry));
1619       **
1620       ** instead, we copy the symtable...
1621       */
1622
1623       idTableEntry *oldentries = st->entries;
1624       unsigned int i;
1625
1626       st->entries = dmalloc ((n+DELTA) * sizeof (*st->entries));
1627
1628       for (i = 0; i < n; i++)
1629         {
1630           st->entries[i] = oldentries[i];
1631         }
1632
1633       sfree (oldentries);
1634
1635       st->allocated = n + DELTA;
1636     }
1637
1638   ret = &(st->entries[st->size]);
1639   st->size++;
1640   return ret;
1641 }
1642
1643
1644 static /*@dependent@*/ /*@null@*/ idTableEntry *
1645   symtable_lookup (idTable *st, lsymbol id)
1646 {
1647   int n;
1648   idTableEntry *e;
1649
1650   for (n = st->size - 1; n >= 0; n--)
1651     {
1652       e = &(st->entries[n]);
1653
1654       /*@-loopswitchbreak@*/
1655       switch (e->kind)
1656         {
1657         case SYMK_SCOPE:
1658           break;
1659         case SYMK_FCN:
1660           if (ltoken_getText (e->info.fct->id) == id) return e;
1661           break;
1662         case SYMK_TYPE:
1663           if (ltoken_getText (e->info.type->id) == id) return e;
1664           break;
1665         case SYMK_VAR:
1666           if (ltoken_getText (e->info.var->id) == id) return e;
1667           break;
1668         BADDEFAULT;
1669         }
1670       /*@=loopswitchbreak@*/
1671     }
1672
1673   return (idTableEntry *) 0;
1674 }
1675
1676
1677 static /*@dependent@*/ /*@null@*/ idTableEntry *
1678   symtable_lookupInScope (idTable *st, lsymbol id)
1679 {
1680   int n;
1681   idTableEntry *e;
1682   for (n = st->size - 1; n >= 0; n--)
1683     {
1684       e = &(st->entries[n]);
1685       if (e->kind == SYMK_SCOPE)
1686         break;
1687       if (ltoken_getText (e->info.fct->id) == id)
1688         {
1689           return e;
1690         }
1691     }
1692   return (idTableEntry *) 0;
1693 }
1694
1695 /* hash table implementation */
1696
1697 static symbolKey
1698 htData_key (htData * x)
1699 {
1700   /* assume x points to a valid htData struct */
1701   switch (x->kind)
1702     {
1703     case IK_SORT:
1704       return x->content.sort;
1705     case IK_OP:
1706       {                         /* get the textSym of the token */
1707         nameNode n = (x->content.op)->name;
1708
1709         if (n->isOpId)
1710           {
1711             return ltoken_getText (n->content.opid);
1712           }
1713         else
1714           {
1715             llassert (n->content.opform != NULL);
1716             return (n->content.opform)->key;
1717           }
1718       }
1719     case IK_TAG:
1720       return ltoken_getText ((x->content).tag->id);
1721     }
1722   BADEXIT;
1723 }
1724
1725 static void htData_free (/*@null@*/ /*@only@*/ htData *d)
1726 {
1727   if (d != NULL)
1728     {
1729       switch (d->kind)
1730         {
1731         case IK_SORT:
1732           break;
1733         case IK_OP:
1734           /* nameNode_free (d->content.op->name);*/
1735           sigNodeSet_free (d->content.op->signatures);
1736           break;
1737         case IK_TAG:
1738           {
1739             switch (d->content.tag->kind)
1740               {
1741               case TAG_STRUCT:
1742               case TAG_UNION:
1743               case TAG_FWDSTRUCT:
1744               case TAG_FWDUNION:
1745                 /*
1746                  ** no: stDeclNodeList_free (d->content.tag->content.decls);
1747                  **     it is dependent!
1748                  */
1749                 /*@switchbreak@*/ break;
1750               case TAG_ENUM:
1751
1752                 /* no: ltokenList_free (d->content.tag->content.enums);
1753                  **     it is dependent!
1754                  */
1755
1756                 /*@switchbreak@*/ break;
1757               }
1758           }
1759         }
1760
1761       sfree (d);
1762     }
1763 }
1764
1765 static void bucket_free (/*@null@*/ /*@only@*/ bucket *b)
1766 {
1767   if (b != NULL)
1768     {
1769       bucket_free (b->next);
1770       htData_free (b->data);
1771       sfree (b);
1772     }
1773 }
1774
1775 static void symHashTable_free (/*@only@*/ symHashTable *h)
1776 {
1777   unsigned int i;
1778
1779   for (i = 0; i < h->size; i++)
1780     {
1781       bucket_free (h->buckets[i]);
1782     }
1783
1784   sfree (h->buckets);
1785   sfree (h);
1786 }
1787
1788 static /*@only@*/ symHashTable *
1789 symHashTable_create (unsigned int size)
1790 {
1791   unsigned int i;
1792   symHashTable *t = (symHashTable *) dmalloc (sizeof (*t));
1793
1794   t->buckets = (bucket **) dmalloc ((size + 1) * sizeof (*t->buckets));
1795   t->count = 0;
1796   t->size = size;
1797
1798   for (i = 0; i <= size; i++)
1799     {
1800       t->buckets[i] = (bucket *) NULL;
1801     }
1802
1803   return t;
1804 }
1805
1806 static /*@null@*/ /*@exposed@*/ htData *
1807 symHashTable_get (symHashTable *t, symbolKey key, infoKind kind, /*@null@*/ nameNode n)
1808 {
1809   bucket *b;
1810   htEntry *entry;
1811   htData *d;
1812
1813   b = t->buckets[MASH (key, kind)];
1814   if (b == (bucket *) 0)
1815     {
1816       return ((htData *) 0);
1817     }
1818
1819   for (entry = (htEntry *) b; entry != NULL; entry = entry->next)
1820     {
1821       d = entry->data;
1822
1823       if (d->kind == kind && htData_key (d) == key)
1824         if (kind != IK_OP || sameNameNode (n, d->content.op->name))
1825           {
1826             return d;
1827           }
1828     }
1829   return ((htData *) 0);
1830 }
1831
1832 static bool
1833 symHashTable_put (symHashTable *t, /*@only@*/ htData *data)
1834 {
1835   /* if key is already taken, don't insert, return FALSE
1836      else insert it and return TRUE. */
1837   symbolKey key;
1838   htData *oldd;
1839   infoKind kind;
1840   nameNode name;
1841
1842   key = htData_key (data);
1843   kind = data->kind;
1844
1845   if (kind == IK_OP && (!data->content.op->name->isOpId))
1846     {
1847       name = data->content.op->name;
1848     }
1849   else
1850     {
1851       name = (nameNode) 0;
1852     }
1853
1854   oldd = symHashTable_get (t, key, kind, name);
1855
1856   if (oldd == (htData *) 0)
1857     {
1858       /*@-deparrays@*/
1859       bucket *new_entry = (bucket *) dmalloc (sizeof (*new_entry));
1860       bucket *b = (t->buckets[MASH (key, kind)]);
1861       htEntry *entry = (htEntry *) b;
1862       /*@=deparrays@*/
1863
1864       new_entry->data = data;
1865       new_entry->next = entry;
1866       t->buckets[MASH (key, kind)] = new_entry;
1867       t->count++;
1868
1869       return TRUE;
1870     }
1871   else
1872     {
1873       htData_free (data);
1874     }
1875
1876   return FALSE;
1877 }
1878
1879 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
1880   symHashTable_forcePut (symHashTable *t, /*@only@*/ htData *data)
1881 {
1882   /* Put data in, return old value */
1883   symbolKey key;
1884   bucket *b;
1885   htData *oldd;
1886   htEntry *entry, *new_entry;
1887   infoKind kind;
1888   nameNode name;
1889
1890   key = htData_key (data);
1891   kind = data->kind;
1892
1893   if (kind == IK_OP && (!data->content.op->name->isOpId))
1894     {
1895       name = data->content.op->name;
1896     }
1897   else
1898     {
1899       name = (nameNode) 0;
1900     }
1901
1902   oldd = symHashTable_get (t, key, kind, name);
1903
1904   if (oldd == (htData *) 0)
1905     {
1906       new_entry = (htEntry *) dmalloc (sizeof (*new_entry));
1907
1908       /*@-deparrays@*/
1909       b = t->buckets[MASH (key, kind)];
1910       /*@=deparrays@*/
1911
1912       entry = b;
1913       new_entry->data = data;
1914       new_entry->next = entry;
1915       t->buckets[MASH (key, kind)] = new_entry;
1916       t->count++;
1917
1918       return NULL;
1919     }
1920   else
1921     {                           /* modify in place */
1922       *oldd = *data;            /* copy new info over to old info */
1923
1924       /* dangerous: if the data is the same, don't free it */
1925       if (data != oldd)
1926         {
1927           sfree (data);
1928         /*@-branchstate@*/
1929         }
1930       /*@=branchstate@*/
1931
1932       return oldd;
1933     }
1934 }
1935
1936 #if 0
1937 static unsigned int
1938 symHashTable_count (symHashTable * t)
1939 {
1940   return (t->count);
1941 }
1942
1943 #endif
1944
1945 static void
1946 symHashTable_printStats (symHashTable * t)
1947 {
1948   int i, bucketCount, setsize, sortCount, opCount, tagCount;
1949   int sortTotal, opTotal, tagTotal;
1950   bucket *b;
1951   htEntry *entry;
1952   htData *d;
1953
1954   sortTotal = 0;
1955   opTotal = 0;
1956   tagTotal = 0;
1957   sortCount = 0;
1958   opCount = 0;
1959   tagCount = 0;
1960
1961   /* for debugging only */
1962   printf ("\n Printing symHashTable stats ... \n");
1963   for (i = 0; i <= HT_MAXINDEX; i++)
1964     {
1965       b = t->buckets[i];
1966       bucketCount = 0;
1967       for (entry = b; entry != NULL; entry = entry->next)
1968         {
1969           d = entry->data;
1970           bucketCount++;
1971           switch (d->kind)
1972             {
1973             case IK_SORT:
1974               sortCount++;
1975               /*@switchbreak@*/ break;
1976             case IK_OP:
1977               {
1978                 cstring name = nameNode_unparse (d->content.op->name);
1979                 cstring sigs = sigNodeSet_unparse (d->content.op->signatures);
1980                 opCount++;
1981                 /* had a tt? */
1982                 setsize = sigNodeSet_size (d->content.op->signatures);
1983                 printf ("       Op (%d): %s %s\n", setsize,
1984                         cstring_toCharsSafe (name),
1985                         cstring_toCharsSafe (sigs));
1986                 cstring_free (name);
1987                 cstring_free (sigs);
1988                 /*@switchbreak@*/ break;
1989               }
1990             case IK_TAG:
1991               tagCount++;
1992               /*@switchbreak@*/ break;
1993             }
1994         }
1995       if (bucketCount > 0)
1996         {
1997           printf ("   Bucket %d has count = %d; opCount = %d; sortCount = %d; tagCount = %d\n", i, bucketCount, opCount, sortCount, tagCount);
1998           sortTotal += sortCount;
1999           tagTotal += tagCount;
2000           opTotal += opCount;
2001         }
2002     }
2003   printf ("SymHashTable has total count = %d, opTotal = %d, sortTotal = %d, tagTotal = %d :\n", t->count, opTotal, sortTotal, tagTotal);
2004
2005 }
2006
2007 void
2008 symtable_printStats (symtable s)
2009 {
2010   symHashTable_printStats (s->hTable);
2011  /* for debugging only */
2012   printf ("idTable size = %d; allocated = %d\n",
2013           s->idTable->size, s->idTable->allocated);
2014 }
2015
2016 /*@only@*/ cstring
2017 tagKind_unparse (tagKind k)
2018 {
2019   switch (k)
2020     {
2021     case TAG_STRUCT:
2022     case TAG_FWDSTRUCT:
2023       return cstring_makeLiteral ("struct");
2024     case TAG_UNION:
2025     case TAG_FWDUNION:
2026       return cstring_makeLiteral ("union");
2027     case TAG_ENUM:
2028       return cstring_makeLiteral ("enum");
2029     }
2030   BADEXIT;
2031 }
2032
2033 static void tagInfo_free (/*@only@*/ tagInfo tag)
2034 {
2035   ltoken_free (tag->id);
2036   sfree (tag);
2037 }
2038
2039 /*@observer@*/ sigNodeSet
2040   symtable_possibleOps (symtable tab, nameNode n)
2041 {
2042   opInfo oi = symtable_opInfo (tab, n);
2043
2044   if (opInfo_exists (oi))
2045     {
2046       return (oi->signatures);
2047     }
2048
2049   return sigNodeSet_undefined;
2050 }
2051
2052 bool
2053 symtable_opExistsWithArity (symtable tab, nameNode n, int arity)
2054 {
2055   opInfo oi = symtable_opInfo (tab, n);
2056
2057   if (opInfo_exists (oi))
2058     {
2059       sigNodeSet sigs = oi->signatures;
2060       sigNodeSet_elements (sigs, sig)
2061       {
2062         if (ltokenList_size (sig->domain) == arity)
2063           return TRUE;
2064       } end_sigNodeSet_elements;
2065     }
2066   return FALSE;
2067 }
2068
2069 static bool
2070 domainMatches (ltokenList domain, sortSetList argSorts)
2071 {
2072   /* expect their length to match */
2073   /* each domain sort in op must be an element of
2074      the corresponding set in argSorts. */
2075   bool matched = TRUE;
2076   sort s;
2077
2078   sortSetList_reset (argSorts);
2079   ltokenList_elements (domain, dom)
2080     {
2081       s = sort_fromLsymbol (ltoken_getText (dom));
2082       if (!(sortSet_member (sortSetList_current (argSorts), s)))
2083         {
2084           /*      printf ("   mismatched element is: %s in %s\n", ltoken_getTextChars (*dom),
2085                   sortSet_unparse (sortSetList_current (argSorts))); */
2086           matched = FALSE;
2087           break;
2088         }
2089       sortSetList_advance (argSorts);
2090   } end_ltokenList_elements;
2091
2092   return matched;
2093 }
2094
2095 /*@only@*/ lslOpSet
2096   symtable_opsWithLegalDomain (symtable tab, /*@temp@*/ /*@null@*/ nameNode n,
2097                                sortSetList argSorts, sort q)
2098 {
2099  /* handles nil qual */
2100   lslOpSet ops = lslOpSet_new ();
2101   lslOp op;
2102   sort rangeSort;
2103   opInfo oi;
2104
2105   llassert (n != NULL);
2106   oi = symtable_opInfo (tab, n);
2107
2108   if (opInfo_exists (oi))
2109     {
2110       sigNodeSet sigs = oi->signatures;
2111
2112       sigNodeSet_elements (sigs, sig)
2113         {
2114           if (ltokenList_size (sig->domain) == sortSetList_size (argSorts))
2115             {
2116               rangeSort = sigNode_rangeSort (sig);
2117
2118               if ((q == NULL) || (sort_equal (rangeSort, q)))
2119                 {
2120                   if (domainMatches (sig->domain, argSorts))
2121                     {
2122                       op = (lslOp) dmalloc (sizeof (*op));
2123
2124                       /* each domain sort in op must be an element of
2125                          the corresponding set in argSorts. */
2126                       op->signature = sig;
2127                       op->name = nameNode_copy (n);
2128                       (void) lslOpSet_insert (ops, op);
2129                     }
2130                 }
2131             }
2132         } end_sigNodeSet_elements;
2133     }
2134   return ops;
2135 }