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