src/symtable.c

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