---

symtable.c

Go to the documentation of this file.

/*
** LCLint - annotation-assisted static program checker
** Copyright (C) 1994-2000 University of Virginia,
**         Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
** 
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
** General Public License for more details.
** 
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
** For more information: http://lclint.cs.virginia.edu
*/
/*
** symtable.c
**
** Symbol table abstraction
**
**  AUTHORS:
**
**      Gary Feldman, Technical Languages and Environments, DECspec project
**      Steve Garland,
**         Massachusetts Institute of Technology
**      Joe Wild, Technical Languages and Environments, DECspec project
**      Yang Meng Tan,
**         Massachusetts Institute of Technology
**
**  CREATION DATE:
**
**      20 January 1991
*/

# include "lclintMacros.nf"
# include "llbasic.h"
# include "gram.h"
# include "lclscan.h"
# include "lclsyntable.h"
# include "lslparse.h"

/*@+ignorequals@*/

static bool isBlankLine (char *p_line);
static bool inImport = FALSE;

/*@constant static int MAXBUFFLEN;@*/
# define MAXBUFFLEN 512
/*@constant static int DELTA;@*/
# define DELTA 100

static void symHashTable_dump (symHashTable * p_t, FILE * p_f, bool p_lco);

static void tagInfo_free (/*@only@*/ tagInfo p_tag);
static /*@observer@*/ scopeInfo symtable_scopeInfo (symtable p_stable);

static void symtable_dumpId (symtable p_stable, FILE *p_f, bool p_lco);
static lsymbol nameNode2key (nameNode p_n);

typedef enum
{
  SYMK_FCN, SYMK_SCOPE, SYMK_TYPE, SYMK_VAR
} symKind;

typedef struct
{
  symKind kind;
  union
  {
    /*@only@*/ fctInfo fct;
    /*@only@*/ scopeInfo scope;
    /*@only@*/ typeInfo type;
    /*@only@*/ varInfo var;
  } info;
} idTableEntry;

typedef struct _idTable
{
  unsigned int size;
  unsigned int allocated;
  /*@relnull@*/ idTableEntry *entries;
  bool exporting;
} idTable;

struct _symtableStruct
{
  idTable *idTable;             /* data is idTableEntry */
  symHashTable *hTable;         /* data is htData */
  mapping *type2sort;           /* maps LCL type symbol to LSL sort */
} ;

static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *p_x);
static /*@out@*/ /*@exposed@*/ idTableEntry *nextFree (idTable * p_st);
static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookup (idTable * p_st, lsymbol p_id);
static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookupInScope (idTable * p_st, lsymbol p_id);

static /*@only@*/ idTable *symtable_newIdTable (void);
static void idTableEntry_free (idTableEntry p_x);

/* Local implementatio of hash table */

static bool allowed_redeclaration = FALSE;
static symbolKey htData_key (htData *p_x);

static void symHashTable_free (/*@only@*/ symHashTable *p_h);
static /*@only@*/ symHashTable *symHashTable_create (unsigned int p_size);
static /*@null@*/ /*@exposed@*/ htData *
  symHashTable_get (symHashTable * p_t, symbolKey p_key, infoKind p_kind, 
                 /*@null@*/ nameNode p_n);
static bool symHashTable_put (symHashTable *p_t, /*@only@*/ htData *p_data);
static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
  symHashTable_forcePut (symHashTable * p_t, /*@only@*/ htData *p_data);
/* static unsigned int symHashTable_count (symHashTable * t); */

static void idTable_free (/*@only@*/ idTable *p_st);

void varInfo_free (/*@only@*/ varInfo v)
{
  sfree (v);
}

static /*@only@*/ varInfo varInfo_copy (varInfo v)
{
  varInfo ret = (varInfo) dmalloc (sizeof (*ret));

  ret->id = ltoken_copy (v->id);
  ret->sort = v->sort;
  ret->kind = v->kind;
  ret->export = v->export;

  return ret;
}

void symtable_free (symtable stable)
{
  /* symtable_printStats (stable); */

  idTable_free (stable->idTable);
  symHashTable_free (stable->hTable);
  mapping_free (stable->type2sort);
  sfree (stable);
}

static void idTable_free (idTable *st)
{
  unsigned int i;

  for (i = 0; i < st->size; i++)
    {
      idTableEntry_free (st->entries[i]);
    }

  sfree (st->entries);
  sfree (st);
}

static void fctInfo_free (/*@only@*/ fctInfo f)
{
  signNode_free (f->signature);
  pairNodeList_free (f->globals);
  ltoken_free (f->id);
  sfree (f);
}

static void typeInfo_free (/*@only@*/ typeInfo t)
{
  sfree (t);
}

static void scopeInfo_free (/*@only@*/ scopeInfo s)
{
  sfree (s);
}

static void idTableEntry_free (idTableEntry x)
{
  switch (x.kind)
    {
    case SYMK_FCN:
      fctInfo_free (x.info.fct);
      break;
    case SYMK_SCOPE:
      scopeInfo_free (x.info.scope);
      break;
    case SYMK_TYPE:
      typeInfo_free (x.info.type);
      break;
    case SYMK_VAR:
      varInfo_free (x.info.var);
      break;
    }
}

static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *x)
{
  switch (x->kind)
    {
    case SYMK_FCN:
      return (x->info.fct->id);
    case SYMK_SCOPE:
      return ltoken_undefined;
    case SYMK_TYPE:
      return (x->info.type->id);
    case SYMK_VAR:
      return (x->info.var->id);
    }

  BADBRANCH;
}

/*@only@*/ symtable
symtable_new (void)
{
  symtable stable = (symtable) dmalloc (sizeof (*stable));
  idTableEntry *e;
  
  stable->idTable = symtable_newIdTable ();
  stable->hTable = symHashTable_create (HT_MAXINDEX);
  stable->type2sort = mapping_create ();
  
  /* add builtin synonym:  Bool -> bool */
  
  mapping_bind (stable->type2sort, lsymbol_getBool (), lsymbol_getbool ());

  /*
  ** done by symtable_newIdTable
  ** st->allocated = 0;
  ** st->entries = (idTableEntry *) 0;
  ** st->exporting = TRUE;
  */

  /* this is global scope */
  e = nextFree (stable->idTable);
  e->kind = SYMK_SCOPE;
  (e->info).scope = (scopeInfo) dmalloc (sizeof (*((e->info).scope)));
  (e->info).scope->kind = SPE_GLOBAL;
  
  return stable;
}

static /*@only@*/ idTable *symtable_newIdTable (void)
{
  idTable *st = (idTable *) dmalloc (sizeof (*st));

  st->size = 0;
  st->allocated = 0;
  st->entries = (idTableEntry *) 0;
  st->exporting = TRUE;
  
  /* this was being done twice!
     e = nextFree (st);
     e->kind = SYMK_SCOPE;
     (e->info).scope.kind = globScope;
     */

  return st;
}

static lsymbol
nameNode2key (nameNode n)
{
  unsigned int ret;

  if (n->isOpId)
    {
      ret =  ltoken_getText (n->content.opid);
    }
  else
    {
      /* use opForm's key as its Identifier */
      llassert (n->content.opform != NULL);
      ret = (n->content.opform)->key;
    }

  return ret;
}

/*
** requires: nameNode n is already in st.
*/

static bool
htData_insertSignature (htData *d, /*@owned@*/ sigNode oi)
{
  sigNodeSet set = d->content.op->signatures;

  
  if (oi != (sigNode) 0)
    {
      return (sigNodeSet_insert (set, oi));
    }
  return FALSE;
}

void
symtable_enterOp (symtable st, /*@only@*/ /*@notnull@*/ nameNode n, 
                  /*@owned@*/ sigNode oi)
{
  /*
  ** Operators are overloaded, we allow entering opInfo more than once,
  ** even if it's the same signature. 
  **
  ** Assumes all sorts are already entered into the symbol table 
  */

  symHashTable *ht = st->hTable;
  htData *d;
  lsymbol id;

  
  
  id = nameNode2key (n);

  d = symHashTable_get (ht, id, IK_OP, n);
  
  if (d == (htData *) 0)
    {                           /* first signature of this operator */
      opInfo op = (opInfo) dmalloc (sizeof (*op));
      htData *nd = (htData *) dmalloc (sizeof (*nd));

      op->name = n;

      if (oi != (sigNode) 0)
        {
          op->signatures = sigNodeSet_singleton (oi);
          ht->count++;
        }
      else
        {
          op->signatures = sigNodeSet_new ();
          sigNode_markOwned (oi);
        }

      nd->kind = IK_OP;
      nd->content.op = op;
      (void) symHashTable_put (ht, nd);
    }
  else
    {
      
      nameNode_free (n);  /*<<<??? */

      if (htData_insertSignature (d, oi))
        {
          ht->count++;
        }
    }
}

bool
  symtable_enterTag (symtable st, tagInfo ti)
{
  /* put ti only if it is not already in symtable */
  symHashTable *ht = st->hTable;
  htData *d;
  symbolKey key = ltoken_getText (ti->id);

  d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);
  if (d == (htData *) 0)
    {
      d = (htData *) dmalloc (sizeof (*d));
      d->kind = IK_TAG;
      d->content.tag = ti;
      d->content.tag->imported = context_inImport ();
      (void) symHashTable_put (ht, d);
      return TRUE;
    }
  else
    {
      if (d->content.tag->imported)
        {
          d->content.tag = ti;
          d->content.tag->imported = context_inImport ();
          return TRUE;
        }
      else
        {
          tagInfo_free (ti);
          return FALSE;
        }
    }
}

bool
symtable_enterTagForce (symtable st, tagInfo ti)
{
 /* put ti, force-put if necessary */
  symHashTable *ht = st->hTable;
  htData *d;
  symbolKey key = ltoken_getText (ti->id);

  d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);

  if (d == (htData *) 0)
    {
      d = (htData *) dmalloc (sizeof (*d));
      
      d->kind = IK_TAG;
      d->content.tag = ti;
      d->content.tag->imported = context_inImport ();
      (void) symHashTable_put (ht, d);
      return TRUE;
    }
  else
    {
            
      d->kind = IK_TAG;
      d->content.tag = ti;
      d->content.tag->imported = context_inImport ();
      /* interpret return data later, htData * */
      /*@i@*/ (void) symHashTable_forcePut (ht, d);
      return FALSE;
    }
}

/*@null@*/ opInfo
symtable_opInfo (symtable st, /*@notnull@*/ nameNode n)
{
  symHashTable *ht = st->hTable;
  lsymbol i = nameNode2key (n);

  htData *d;
  d = symHashTable_get (ht, i, IK_OP, n);
  if (d == (htData *) 0)
    {
      return (opInfo)NULL;
    }

  return (d->content.op);
}

/*@null@*/ tagInfo
symtable_tagInfo (symtable st, lsymbol i)
{
  symHashTable *ht = st->hTable;
  htData *d;
  d = symHashTable_get (ht, i, IK_TAG, 0);

  if (d == (htData *) 0)
    {
      return (tagInfo) NULL;
    }

  return (d->content.tag);
}

void
  symtable_enterScope (symtable stable, scopeInfo si)
{
  idTable *st = stable->idTable;
  idTableEntry *e = nextFree (st);
  if (si->kind == SPE_GLOBAL)
    llbuglit ("symtable_enterScope: SPE_GLOBAL");
  e->kind = SYMK_SCOPE;
  (e->info).scope = si;
}

void
symtable_exitScope (symtable stable)
{
  idTable *st = stable->idTable;
  int n;

  if (st->entries != NULL)
    {
      for (n = st->size - 1; (st->entries[n]).kind != SYMK_SCOPE; n--)
        {
          ;
        }
    }
  else
    {
      llcontbuglit ("symtable_exitScope: no scope to exit");
      n = 0;
    }

  st->size = n;
}

bool
symtable_enterFct (symtable stable, fctInfo fi)
{
  idTable *st = stable->idTable;
  idTableEntry *e;
  bool redecl = FALSE;

  if (!allowed_redeclaration &&
      symtable_lookup (st, ltoken_getText (fi->id)) != (idTableEntry *) 0)
    {
      lclRedeclarationError (fi->id);
      redecl = TRUE;
    }
  
  e = nextFree (st);
  e->kind = SYMK_FCN;
  fi->export = st->exporting;   /* && !fi->private; */
  (e->info).fct = fi;

  return redecl;
}

void
symtable_enterType (symtable stable, /*@only@*/ typeInfo ti)
{
  idTable *st = stable->idTable;
  idTableEntry *e;
  bool insertp = TRUE;
  scopeKind k = (symtable_scopeInfo (stable))->kind;

  /* symtable_disp (stable); */

  if (k != SPE_GLOBAL && k != SPE_INVALID)      /* fixed for LCLint */
    {
      llbug (message ("%q: symtable_enterType: expect global scope. (type: %s)",
                      ltoken_unparseLoc (ti->id),
                      ltoken_getRawString (ti->id)));
    }

  if (!allowed_redeclaration &&
      symtable_lookup (st, ltoken_getText (ti->id)) != (idTableEntry *) 0)
    {
     /* ignore if Bool is re-entered */
      if (ltoken_getText (ti->id) == lsymbol_getBool () ||
          ltoken_getText (ti->id) == lsymbol_getbool ())
        {
          insertp = FALSE;
        }
      else
        {
          lclRedeclarationError (ti->id);
        }
    }
  if (insertp)
    {
      /* make sure it is a type TYPEDEF_NAME; */
      
      if (ltoken_getCode (ti->id) != LLT_TYPEDEF_NAME)
        {
          lclbug (message ("symtable_enterType: gets a simpleId, expect a type: %s",
                           ltoken_getRawString (ti->id)));
        }
      
      e = nextFree (st);
      e->kind = SYMK_TYPE;
      ti->export = st->exporting;/* && !ti->private; */
      (e->info).type = ti;
      mapping_bind (stable->type2sort, ltoken_getText (ti->id),
                    sort_getLsymbol (sort_makeVal (sort_getUnderlying (ti->basedOn))));
    }
  else
    {
      typeInfo_free (ti);
    }
}

lsymbol
lsymbol_sortFromType (symtable s, lsymbol typename)
{
  lsymbol inter;
  lsymbol out;
  ltoken tok;
 /* check the synonym table first */
  if (LCLIsSyn (typename))
    {
      tok = LCLGetTokenForSyn (typename);
      inter = ltoken_getText (tok);
     /*    printf ("In lsymbol_sortFromType: %s -> %s\n",
                lsymbol_toChars (typename), lsymbol_toChars (inter)); */
    }
  else
    {
      inter = typename;
    }

  /* now map LCL type to sort */
  out = mapping_find (s->type2sort, inter);
  
  if (out == lsymbol_undefined)
    {
      return inter;
    }

  return out;
}

/* really temp! */

/*
** returns true is vi is a redeclaration
*/

bool
symtable_enterVar (symtable stable, /*@temp@*/ varInfo vi)
{
  idTable *st = stable->idTable;
  bool insertp = TRUE;
  bool redecl = FALSE;

  
  /* symtable_disp (symtab); */
  
  if (!allowed_redeclaration &&
      (symtable_lookupInScope (st, ltoken_getText (vi->id)) != (idTableEntry *) 0))
    {
      if (ltoken_getText (vi->id) == lsymbol_getTRUE () ||
          ltoken_getText (vi->id) == lsymbol_getFALSE ())
        {
          insertp = FALSE;
        }
      else
        {
          if (usymtab_existsEither (ltoken_getRawString (vi->id)))
            {
                      lclRedeclarationError (vi->id);
              redecl = TRUE;
            }
          else
            {
              llbuglit ("redeclared somethingerother?!");
            }
        }
    }

  if (insertp)
    {
      idTableEntry *e = nextFree (st);

      e->kind = SYMK_VAR;
      vi->export = st->exporting &&     /* !vi.private && */
        (vi->kind == VRK_VAR || vi->kind == VRK_CONST || vi->kind == VRK_ENUM);
      (e->info).var = varInfo_copy (vi);
    }
  
    return (redecl);
}

bool
symtable_exists (symtable stable, lsymbol i)
{
  idTable *st = stable->idTable;
  return symtable_lookup (st, i) != (idTableEntry *) 0;
}

/*@null@*/ typeInfo
symtable_typeInfo (symtable stable, lsymbol i)
{
  idTable *st;
  idTableEntry *e;

  st = stable->idTable;
  e = symtable_lookup (st, i);

  if (e == (idTableEntry *) 0 || e->kind != SYMK_TYPE)
    {
      return (typeInfo) NULL;
    }

  return (e->info).type;
}

/*@null@*/ varInfo
symtable_varInfo (symtable stable, lsymbol i)
{
  idTable *st = stable->idTable;
  idTableEntry *e;

  e = symtable_lookup (st, i);

  if (e == (idTableEntry *) 0 || e->kind != SYMK_VAR)
    {
      return (varInfo) NULL;
    }

  return (e->info).var;
}

/*@null@*/ varInfo
symtable_varInfoInScope (symtable stable, lsymbol id)
{
  /* if current scope is a SPE_QUANT, can go beyond current scope */
  idTable *st = stable->idTable;
  idTableEntry *e2 = (idTableEntry *) 0;
  int n;
  
  for (n = st->size - 1; n >= 0; n--)
    {
      ltoken tok;

      e2 = &(st->entries[n]);
      
      if (e2->kind == SYMK_SCOPE && e2->info.scope->kind != SPE_QUANT)
        {
          return (varInfo) NULL;
        }

      tok = idTableEntry_getId (e2);

      if (e2->kind == SYMK_VAR && ltoken_getText (tok) == id)
        {
          return (e2->info).var;
        }
    }

  return (varInfo) NULL;
}

scopeInfo
symtable_scopeInfo (symtable stable)
{
  idTable *st = stable->idTable;
  int n;
  idTableEntry *e;

  for (n = st->size - 1; n >= 0; n--)
    {
      e = &(st->entries[n]);
      if (e->kind == SYMK_SCOPE)
        return (e->info).scope;
    }

  lclfatalbug ("symtable_scopeInfo: not found");
  BADEXIT;
}

void
symtable_export (symtable stable, bool yesNo)
{
  idTable *st = stable->idTable;
  st->exporting = yesNo;
  (void) sort_setExporting (yesNo);
}

static void
symHashTable_dump (symHashTable * t, FILE * f, bool lco)
{
  /* like symHashTable_dump2 but for output to .lcs file */
  int i, size;
  bucket *b;
  htEntry *entry;
  htData *d;
  ltoken tok;
  sigNodeSet sigs;
  
  for (i = 0; i <= HT_MAXINDEX; i++)
    {
            b = t->buckets[i];

      for (entry = b; entry != NULL; entry = entry->next)
        {
          d = entry->data;

          switch (d->kind)
            {
            case IK_SORT:
              /*@switchbreak@*/ break;
            case IK_OP:
              {
                char *name = cstring_toCharsSafe (nameNode_unparse (d->content.op->name));
                sigs = d->content.op->signatures;
                size = sigNodeSet_size (sigs);

                
                sigNodeSet_elements (sigs, x)
                  {
                    cstring s = sigNode_unparse (x);

                    if (lco)
                      {
                        fprintf (f, "%%LCL");
                      }

                    fprintf (f, "op %s %s\n", name, cstring_toCharsSafe (s));
                    cstring_free (s);
                  } end_sigNodeSet_elements;

                sfree (name);
                /*@switchbreak@*/ break;
              }
            case IK_TAG:
              tok = d->content.tag->id;
              
              if (!ltoken_isUndefined (tok))
                {
                  cstring s = tagKind_unparse (d->content.tag->kind);

                  if (lco)
                    {
                      fprintf (f, "%%LCL");
                    }

                  fprintf (f, "tag %s %s\n", ltoken_getTextChars (tok), 
                           cstring_toCharsSafe (s));
                  cstring_free (s);
                }
              /*@switchbreak@*/ break;
            }
        }
    }
}

void
symtable_dump (symtable stable, FILE * f, bool lco)
{
  symHashTable *ht = stable->hTable;


  fprintf (f, "%s\n", BEGINSYMTABLE);
   
  symHashTable_dump (ht, f, lco);
   
  symtable_dumpId (stable, f, lco);
  
  fprintf (f, "%s\n", SYMTABLEEND);
  }

lsymbol
lsymbol_translateSort (mapping * m, lsymbol s)
{
  lsymbol res = mapping_find (m, s);
  if (res == lsymbol_undefined)
    return s;
  return res;
}

static /*@null@*/ lslOp
  lslOp_renameSorts (mapping *map,/*@returned@*/ /*@null@*/ lslOp op)
{
  sigNode sign;

  if (op != (lslOp) 0)
    {
      ltokenList domain;
      ltoken range;

      sign = op->signature;
      range = sign->range;
      domain = sign->domain;

      ltokenList_elements (domain, dt)
        {
          ltoken_setText (dt, 
                          lsymbol_translateSort (map, ltoken_getText (dt)));
        } end_ltokenList_elements;

      /*@-onlytrans@*/ /* A memory leak... */
      op->signature = makesigNode (sign->tok, domain, range);
      /*@=onlytrans@*/
    }

  return op;
}

static /*@null@*/ signNode
  signNode_fromsigNode (sigNode s)
{
  signNode sign;
  sortList slist;
  
  if (s == (sigNode) 0)
    {
      return (signNode) 0;
    }
  
  sign = (signNode) dmalloc (sizeof (*sign));
  slist = sortList_new ();
  sign->tok = ltoken_copy (s->tok);
  sign->key = s->key;
  sign->range = sort_makeSort (ltoken_undefined, ltoken_getText (s->range));

  ltokenList_elements (s->domain, dt)
    {
      sortList_addh (slist, sort_makeSort (ltoken_undefined, ltoken_getText (dt)));
    } end_ltokenList_elements;

  sign->domain = slist;
  return sign;
}


static /*@only@*/ pairNodeList
parseGlobals (char *line, tsource *srce)
{
  pairNodeList plist = pairNodeList_new ();
  pairNode p;
  int semi_index;
  char *lineptr, sostr[MAXBUFFLEN], gstr[MAXBUFFLEN];

  /* line is not all blank */
  /* expected format: "sort1 g1; sort2 g2; sort3 g3;" */
  lineptr = line;
  
  while (!isBlankLine (lineptr))
    {
      if (sscanf (lineptr, "%s %s", &(sostr[0]), gstr) != 2)
        {
          lclplainerror 
            (message 
             ("%q: Imported file contains illegal function global declaration.\n"
              "Skipping rest of the line: %s (%s)",
              fileloc_unparseRaw (cstring_fromChars (tsource_fileName (srce)), 
                                  tsource_thisLineNumber (srce)), 
              cstring_fromChars (line), 
              cstring_fromChars (lineptr)));
          return plist;
        }
      
      p = (pairNode) dmalloc (sizeof (*p));
      
      /* Note: remove the ";" separator at the end of gstr */
      semi_index = size_toInt (strlen (gstr));
      gstr[semi_index - 1] = '\0';

      p->tok = ltoken_create (NOTTOKEN, lsymbol_fromChars (gstr));
      p->sort = sort_makeSort (ltoken_undefined, lsymbol_fromChars (sostr));

      pairNodeList_addh (plist, p);
      lineptr = strchr (lineptr, ';');  /* go pass the next; */

      llassert (lineptr != NULL);
      lineptr = lineptr + 1;
    }

  return plist;
}

static bool
isBlankLine (char *line)
{
  int i;

  if (line == NULL) return TRUE;

  for (i = 0; line[i] != '\0'; i++)
    {
      if (line[i] == ' ')
        continue;
      if (line[i] == '\t')
        continue;
      if (line[i] == '\n')
        return TRUE;
      return FALSE;
    }
  return TRUE;
}

typedef /*@only@*/ fctInfo o_fctInfo;

static void
parseLine (char *line, tsource *srce, mapping * map)
{
  static /*@owned@*/ o_fctInfo *savedFcn = NULL;
  char *lineptr, *lineptr2, *cimportfile = tsource_fileName (srce);
  cstring importfile = cstring_fromChars (cimportfile);
  char namestr[MAXBUFFLEN], kstr[20], sostr[MAXBUFFLEN];
  sort bsort, nullSort = sort_makeNoSort ();
  int col = 0;
  fileloc imploc = fileloc_undefined;

  
  if (inImport)
    {
      imploc = fileloc_createImport (importfile, tsource_thisLineNumber (srce));
    }
  
  if (firstWord (line, "op"))
    {
      lslOp op;

      lineptr = strchr (line, 'o');     /* remove any leading blanks */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr, ' ');  /* go past "op" */
      llassert (lineptr != NULL);

      /* add a newline to the end of the line since parseOpLine expects it */
      lineptr2 = strchr (lineptr, '\0');

      if (lineptr2 != 0)
        {
          *lineptr2 = '\n';
          *(lineptr2 + 1) = '\0';
        }

      llassert (cimportfile != NULL);
      op = parseOpLine (cimportfile, lineptr + 1);
      
      if (op == (lslOp) 0)
        {
          lclplainerror
            (message
             ("%q: Imported file contains illegal operator declaration:\n "
              "skipping this line: %s",
              fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
              cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }

            op = lslOp_renameSorts (map, op);

      llassert (op != NULL);
      llassert (op->name != NULL);

      symtable_enterOp (g_symtab, op->name, 
                        sigNode_copy (op->signature));
          /*@-mustfree@*/ } /*@=mustfree@*/
  else if (firstWord (line, "type"))
    {
      typeInfo ti;

      if (sscanf (line, "type %s %s %s", namestr, sostr, kstr) != 3)
        {
          lclplainerror 
            (message ("%q: illegal type declaration:\n skipping this line: %s",
                      fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                      cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }
      
      ti = (typeInfo) dmalloc (sizeof (*ti));
      ti->id = ltoken_createFull (LLT_TYPEDEF_NAME, lsymbol_fromChars (namestr),
                                    importfile, tsource_thisLineNumber (srce), col);

      bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));

      if (sort_isNoSort (bsort))
        {
          lineptr = strchr (line, ' '); /* go past "type" */
          llassert (lineptr != NULL);
          lineptr = strchr (lineptr + 1, ' ');  /* go past namestr */
          llassert (lineptr != NULL);
          col = 5 + lineptr - line;     /* 5 for initial "%LCL "*/

          lclbug (message ("%q: Imported files contains unknown base sort",
                           fileloc_unparseRawCol (importfile, tsource_thisLineNumber (srce), col)));

          bsort = nullSort;
        }
      ti->basedOn = bsort;

      if (strcmp (kstr, "exposed") == 0)
        {
          ti->abstract = FALSE;
          ti->modifiable = TRUE;
        }
      else
        {
          ti->abstract = TRUE;
          if (strcmp (kstr, "mutable") == 0)
            ti->modifiable = TRUE;
          else
            ti->modifiable = FALSE;
        }
      ti->export = TRUE;
      
      /* 
      ** sort of a hack to get imports to work...
      */
      
      if (inImport)
        {
          cstring cnamestr = cstring_fromChars (namestr);

          if (!usymtab_existsGlobEither (cnamestr))
            {
              (void) usymtab_addEntry 
                (uentry_makeDatatype (cnamestr, ctype_unknown,
                                      ti->abstract ? ynm_fromBool (ti->modifiable) : MAYBE,
                                      ti->abstract ? YES : NO,
                                      fileloc_copy (imploc)));
            }
        }

      symtable_enterType (g_symtab, ti);
    }
  else if (firstWord (line, "var"))
    {
      varInfo vi;

      if (sscanf (line, "var %s %s", namestr, sostr) != 2)
        {
          lclplainerror
            (message ("%q: Imported file contains illegal variable declaration.  "
                      "Skipping this line.", 
                      fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce))));
          fileloc_free (imploc);
          return;
        }

      vi = (varInfo) dmalloc (sizeof (*vi));
      bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
      lineptr = strchr (line, ' ');     /* go past "var" */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
      llassert (lineptr != NULL);
      col = 5 + lineptr - line; /* 5 for initial "%LCL "*/

      if (sort_isNoSort (bsort))
        {
          lclplainerror (message ("%q: Imported file contains unknown base sort",
                                  fileloc_unparseRawCol (importfile, tsource_thisLineNumber (srce), col)));
          bsort = nullSort;
        }

      vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
                                  importfile, tsource_thisLineNumber (srce), col);
      vi->sort = bsort;
      vi->kind = VRK_VAR;
      vi->export = TRUE;
      (void) symtable_enterVar (g_symtab, vi);
      varInfo_free (vi);

      if (inImport)
        {
          cstring cnamestr = cstring_fromChars (namestr);

          if (!usymtab_existsGlobEither (cnamestr))
            {
              
              (void) usymtab_supEntrySref 
                (uentry_makeVariable (cnamestr, ctype_unknown, 
                                      fileloc_copy (imploc), 
                                      FALSE));
            }
        }
    }
  else if (firstWord (line, "const"))
    {
      varInfo vi;

      if (sscanf (line, "const %s %s", namestr, sostr) != 2)
        {
          lclbug (message ("%q: Imported file contains illegal constant declaration: %s",
                           fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                           cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }

      vi = (varInfo) dmalloc (sizeof (*vi));
      bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
      lineptr = strchr (line, ' ');     /* go past "var" */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
      llassert (lineptr != NULL);
      
      col = 5 + lineptr - line; /* 5 for initial "%LCL "*/

      if (sort_isNoSort (bsort))
        {
          lclplainerror (message ("%q: Imported file contains unknown base sort",
                                  fileloc_unparseRawCol (importfile, tsource_thisLineNumber (srce), col)));
          bsort = nullSort;
        }

      vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
                                    importfile, tsource_thisLineNumber (srce), col);
      vi->sort = bsort;
      vi->kind = VRK_CONST;
      vi->export = TRUE;
      (void) symtable_enterVar (g_symtab, vi);
      varInfo_free (vi);
      
      if (inImport)
        {
          cstring cnamestr = cstring_fromChars (namestr);
          
          if (!usymtab_existsGlobEither (cnamestr))
            {
                      
              (void) usymtab_addEntry (uentry_makeConstant (cnamestr,
                                                            ctype_unknown,
                                                            fileloc_copy (imploc)));
            }
        }
      /* must check for "fcnGlobals" before "fcn" */
    }
  else if (firstWord (line, "fcnGlobals"))
    {
      pairNodeList globals;
      lineptr = strchr (line, 'f');     /* remove any leading blanks */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr, ' ');  /* go past "fcnGlobals" */
      llassert (lineptr != NULL);

     /* a quick check for empty fcnGlobals */
      if (!isBlankLine (lineptr))
        {
          globals = parseGlobals (lineptr, srce);
          /* should ensure that each global in an imported function
             corresponds to some existing global.  Since only
             "correctly processed" .lcs files are imported, this is
             true as an invariant. */
        }
      else
        {
          globals = pairNodeList_new ();
        }
      
      /* check that they exist, store them on fctInfo */

      if (savedFcn != NULL)
        {
          pairNodeList_free ((*savedFcn)->globals);
          (*savedFcn)->globals = globals;  /* evs, moved inside if predicate */

          (void) symtable_enterFct (g_symtab, *savedFcn);
          savedFcn = NULL;
        }
      else
        {
          lclplainerror 
            (message ("%q: Unexpected function globals.  "
                      "Skipping this line: \n%s",
                      fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                      cstring_fromChars (line)));
          savedFcn = NULL;
          pairNodeList_free (globals);
        }
    }
  else if (firstWord (line, "fcn"))
    {
      lslOp op;
      lslOp op2; 

      if (savedFcn != (fctInfo *) 0)
        {
          lclplainerror 
            (message ("%q: illegal function declaration.  Skipping this line:\n%s",
                      fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                      cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }

      savedFcn = (fctInfo *) dmalloc (sizeof (*savedFcn));

      lineptr = strchr (line, 'f');     /* remove any leading blanks */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr, ' ');  /* go past "fcn" */
      llassert (lineptr != NULL);

      /* add a newline to the end of the line since parseOpLine expects it */

      lineptr2 = strchr (lineptr, '\0');

      if (lineptr2 != 0)
        {
          *lineptr2 = '\n';
          *(lineptr2 + 1) = '\0';
        }

      op = parseOpLine (cimportfile, lineptr + 1);

      if (op == (lslOp) 0)
        {
          lclplainerror (message ("%q: illegal function declaration: %s",
                                  fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                                  cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }
        
      op2 = lslOp_renameSorts (map, op);

      llassert (op2 != NULL);

      if ((op->name != NULL) && op->name->isOpId)
        {
          (*savedFcn) = (fctInfo) dmalloc (sizeof (**savedFcn));
          (*savedFcn)->id = op->name->content.opid;
          (*savedFcn)->signature = signNode_fromsigNode (op2->signature);
          (*savedFcn)->globals = pairNodeList_new ();
          (*savedFcn)->export = TRUE;
          
          if (inImport)
            {
              /* 27 Jan 1995 --- added this to be undefined namestr bug */
              cstring fname = ltoken_unparse ((*savedFcn)->id);
              
              if (!usymtab_existsGlobEither (fname))
                {
                                  (void) usymtab_addEntry (uentry_makeFunction
                                           (fname, ctype_unknown, 
                                            typeId_invalid, globSet_new (),
                                            sRefSet_undefined, 
                                            fileloc_copy (imploc)));
                }
            }
        }
      else
        {
          lclplainerror (message ("%q: unexpected function name: %s",
                                  fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                                  cstring_fromChars (line)));
        }
    }
  else if (firstWord (line, "enumConst"))
    {
      varInfo vi;

      if (sscanf (line, "enumConst %s %s", namestr, sostr) != 2)
        {
          lclplainerror 
            (message ("%q: Illegal enum constant declaration.  "
                      "Skipping this line:\n%s",
                      fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                      cstring_fromChars (line)));
          fileloc_free (imploc);
          return;
        }
      
      vi = (varInfo) dmalloc (sizeof (*vi));
      bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
      lineptr = strchr (line, ' ');     /* go past "var" */
      llassert (lineptr != NULL);
      lineptr = strchr (lineptr + 1, ' ');      /* go past namestr */
      llassert (lineptr != NULL);

      col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
      if (sort_isNoSort (bsort))
        {
          lclplainerror (message ("%q: unknown base sort\n",
                                  fileloc_unparseRawCol (importfile, tsource_thisLineNumber (srce), col)));
          bsort = nullSort;
        }

      vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
                                    importfile, tsource_thisLineNumber (srce), col);
                        
      vi->sort = bsort;
      vi->kind = VRK_ENUM;
      vi->export = TRUE;
      (void) symtable_enterVar (g_symtab, vi);
      varInfo_free (vi);

      if (inImport)
        {
          cstring cnamestr = cstring_fromChars (namestr);
          if (!usymtab_existsEither (cnamestr))
            {
                      (void) usymtab_addEntry (uentry_makeConstant (cnamestr, ctype_unknown,
                                                            fileloc_copy (imploc)));
            }
        }
    }
  else if (firstWord (line, "tag"))
    {
     /* do nothing, sort processing already handles this */
    }
  else
    {
      lclplainerror 
        (message ("%q: Unknown symbol declaration.  Skipping this line:\n%s",
                  fileloc_unparseRaw (importfile, tsource_thisLineNumber (srce)), 
                  cstring_fromChars (line)));
    }

    fileloc_free (imploc);
}

void
symtable_import (tsource *imported, ltoken tok, mapping * map)
{
  char *buf, *importfile;
  tsource *lclsource;
  int old_lsldebug;
  bool old_inImport = inImport;

  buf = tsource_nextLine (imported);
  importfile = tsource_fileName (imported);

  llassert (buf != NULL);

  if (!firstWord (buf, "%LCLSymbolTable"))
    {
      lclsource = LCLScanSource ();
      lclfatalerror (tok, 
                     message ("Expecting '%%LCLSymbolTable' line in import file %s:\n%s\n",
                              cstring_fromChars (importfile), 
                              cstring_fromChars (buf)));
    }

  old_lsldebug = lsldebug;
  lsldebug = 0;
  allowed_redeclaration = TRUE;
  inImport = TRUE;

  for (;;)
    {
      buf = tsource_nextLine (imported);
      llassert (buf != NULL);

      
      if (firstWord (buf, "%LCLSymbolTableEnd"))
        {
          break;
        }
      else
        {                       /* a good line, remove %LCL from line first */
          if (firstWord (buf, "%LCL"))
            {
              parseLine (buf + 4, imported, map);
            }
          else
            {
              lclsource = LCLScanSource ();
              lclfatalerror 
                (tok,
                 message ("Expecting '%%LCL' prefix in import file %s:\n%s\n",
                          cstring_fromChars (importfile), 
                          cstring_fromChars (buf)));
            }
        }
    }

  /* restore old value */
  inImport = old_inImport;
  lsldebug = old_lsldebug;
  allowed_redeclaration = FALSE;
  }

static void
symtable_dumpId (symtable stable, FILE *f, bool lco)
{
  idTable *st = stable->idTable;
  unsigned int i;
  idTableEntry *se;
  fctInfo fi;
  typeInfo ti;
  varInfo vi;

  for (i = 1; i < st->size; i++)
    {
      /* 2/22/93 I think there is a off-by-1 error, 0 entry is never used */
      se = st->entries + i;
      llassert (se != NULL);
      
      
      /*@-loopswitchbreak@*/
      switch (se->kind)
        {
        case SYMK_FCN:
          {
            cstring tmp;
            
            fi = (se->info).fct;
            
            if (lco)
              {
                fprintf (f, "%%LCL");
              }

            if (!lco && !fi->export)
              {
                fprintf (f, "spec ");
              }
            
            tmp = signNode_unparse (fi->signature);
            fprintf (f, "fcn %s %s \n", ltoken_getTextChars (fi->id), 
                     cstring_toCharsSafe (tmp));
            cstring_free (tmp);
            
            tmp = pairNodeList_unparse (fi->globals);
            fprintf (f, "%%LCLfcnGlobals %s\n", cstring_toCharsSafe (tmp));
            cstring_free (tmp);
            break;
          }
        case SYMK_SCOPE:
          if (lco)
            {
              break;
            }

          /*@-switchswitchbreak@*/
          switch ((se->info).scope->kind)
            {
            case SPE_GLOBAL:
              fprintf (f, "Global scope\n");
              break;
            case SPE_ABSTRACT:
              fprintf (f, "Abstract type scope\n");
              break;
            case SPE_FCN:
              fprintf (f, "Function scope\n");
              break;
             /* a let scope can only occur in a function scope, should not push
                a new scope, so symtable_lookupInScope works properly
                   case letScope:
                     fprintf (f, "Let scope\n");
                     break; */
            case SPE_QUANT:
              fprintf (f, "Quantifier scope\n");
              break;
            case SPE_CLAIM:
              fprintf (f, "Claim scope\n");
              break;
            case SPE_INVALID:
              break;
            }
          break;
        case SYMK_TYPE:
          ti = (se->info).type;
          if (lco)
            fprintf (f, "%%LCL");
          if (!lco && !ti->export)
            fprintf (f, "spec ");
          fprintf (f, "type %s %s",
                   ltoken_getTextChars (ti->id), sort_getName (ti->basedOn));
          if (ti->abstract)
            {
              if (ti->modifiable)
                fprintf (f, " mutable\n");
              else
                fprintf (f, " immutable\n");
            }
          else
            fprintf (f, " exposed\n");
          break;
        case SYMK_VAR:

          vi = (se->info).var;
          if (lco)
            {
              fprintf (f, "%%LCL");
            }

          if (!lco && !vi->export)
            {
              fprintf (f, "spec ");
            }
          switch (vi->kind)
            {
            case VRK_CONST:
              fprintf (f, "const %s %s\n",
                       ltoken_getTextChars (vi->id), sort_getName (vi->sort));
              break;
            case VRK_VAR:
              fprintf (f, "var %s %s\n",
                       ltoken_getTextChars (vi->id), sort_getName (vi->sort));
              break;
            case VRK_ENUM:
              fprintf (f, "enumConst %s %s\n",
                       ltoken_getTextChars (vi->id), sort_getName (vi->sort));
              break;
            default:
              if (lco)
                {
                  switch (vi->kind)
                    {
                    case VRK_GLOBAL:
                      fprintf (f, "global %s %s\n", ltoken_getTextChars (vi->id), sort_getName (vi->sort));
                      break;
                    case VRK_PRIVATE:   /* for private vars within function */
                      fprintf (f, "local %s %s\n",
                               ltoken_getTextChars (vi->id), sort_getName (vi->sort));
                      break;
                    case VRK_LET:
                      fprintf (f, "let %s %s\n",
                               ltoken_getTextChars (vi->id), sort_getName (vi->sort));
                      break;
                    case VRK_PARAM:
                      fprintf (f, "param %s %s\n",
                               ltoken_getTextChars (vi->id), sort_getName (vi->sort));
                      break;
                    case VRK_QUANT:
                      fprintf (f, "quant %s %s\n",
                               ltoken_getTextChars (vi->id), sort_getName (vi->sort));
                      break;
                    BADDEFAULT;
                    }
                  /*@=loopswitchbreak@*/
                  /*@=switchswitchbreak@*/
                }
            }
        }
    }
}

static /*@exposed@*/ /*@out@*/ idTableEntry *
nextFree (idTable * st)
{
  idTableEntry *ret;
  unsigned int n = st->size;

  if (n >= st->allocated)
    {
      /*
      ** this loses with the garbage collector
      ** (and realloc is notoriously dangerous)
      **
      ** st->entries = (idTableEntry *) LSLMoreMem (st->entries, (n + DELTA) 
      **                                * sizeof (idTableEntry));
      **
      ** instead, we copy the symtable...
      */
      
      idTableEntry *oldentries = st->entries;
      unsigned int i;
      
      st->entries = dmalloc ((n+DELTA) * sizeof (*st->entries));
      
      for (i = 0; i < n; i++)
        {
          st->entries[i] = oldentries[i];
        }
      
      sfree (oldentries);
      
      st->allocated = n + DELTA;
    }
  
  ret = &(st->entries[st->size]);
  st->size++;
  return ret;
}


static /*@dependent@*/ /*@null@*/ idTableEntry *
  symtable_lookup (idTable *st, lsymbol id)
{
  int n;
  idTableEntry *e;

  for (n = st->size - 1; n >= 0; n--)
    {
      e = &(st->entries[n]);

      /*@-loopswitchbreak@*/
      switch (e->kind)
        {
        case SYMK_SCOPE: 
          break;
        case SYMK_FCN:
          if (ltoken_getText (e->info.fct->id) == id) return e;
          break;
        case SYMK_TYPE:
          if (ltoken_getText (e->info.type->id) == id) return e;
          break;
        case SYMK_VAR:
          if (ltoken_getText (e->info.var->id) == id) return e;
          break;
        BADDEFAULT;
        }
      /*@=loopswitchbreak@*/
    }

  return (idTableEntry *) 0;
}


static /*@dependent@*/ /*@null@*/ idTableEntry *
  symtable_lookupInScope (idTable *st, lsymbol id)
{
  int n;
  idTableEntry *e;
  for (n = st->size - 1; n >= 0; n--)
    {
      e = &(st->entries[n]);
      if (e->kind == SYMK_SCOPE)
        break;
      if (ltoken_getText (e->info.fct->id) == id)
        {
          return e;
        }
    }
  return (idTableEntry *) 0;
}

/* hash table implementation */

static symbolKey
htData_key (htData * x)
{
  /* assume x points to a valid htData struct */
  switch (x->kind)
    {
    case IK_SORT:
      return x->content.sort;
    case IK_OP:
      {                         /* get the textSym of the token */
        nameNode n = (x->content.op)->name;

        if (n->isOpId)
          {
            return ltoken_getText (n->content.opid);
          }
        else
          {
            llassert (n->content.opform != NULL);
            return (n->content.opform)->key;
          }
      }
    case IK_TAG:
      return ltoken_getText ((x->content).tag->id);
    }
  BADEXIT;
}

static void htData_free (/*@null@*/ /*@only@*/ htData *d)
{
  if (d != NULL)
    {
      switch (d->kind)
        {
        case IK_SORT:
          break;
        case IK_OP:
          /* nameNode_free (d->content.op->name);*/
          sigNodeSet_free (d->content.op->signatures);
          break;
        case IK_TAG:
          {
            switch (d->content.tag->kind)
              {
              case TAG_STRUCT:
              case TAG_UNION:
              case TAG_FWDSTRUCT:
              case TAG_FWDUNION:
                /*
                 ** no: stDeclNodeList_free (d->content.tag->content.decls);
                 **     it is dependent!
                 */
                /*@switchbreak@*/ break;
              case TAG_ENUM:
                
                /* no: ltokenList_free (d->content.tag->content.enums);
                 **     it is dependent!
                 */
                
                /*@switchbreak@*/ break;
              }
          }
        }
      
      sfree (d);
    }
}

static void bucket_free (/*@null@*/ /*@only@*/ bucket *b)
{
  if (b != NULL)
    {
      bucket_free (b->next);
      htData_free (b->data);
      sfree (b);
    }
}

static void symHashTable_free (/*@only@*/ symHashTable *h)
{
  unsigned int i;

  for (i = 0; i < h->size; i++)
    {
      bucket_free (h->buckets[i]);
    }

  sfree (h->buckets);
  sfree (h);
}      
      
static /*@only@*/ symHashTable *
symHashTable_create (unsigned int size)
{
  unsigned int i;
  symHashTable *t = (symHashTable *) dmalloc (sizeof (*t));
  
  t->buckets = (bucket **) dmalloc ((size + 1) * sizeof (*t->buckets));
  t->count = 0;
  t->size = size;

  for (i = 0; i <= size; i++)
    {
      t->buckets[i] = (bucket *) NULL;
    }

  return t;
}

static /*@null@*/ /*@exposed@*/ htData *
symHashTable_get (symHashTable *t, symbolKey key, infoKind kind, /*@null@*/ nameNode n)
{
  bucket *b;
  htEntry *entry;
  htData *d;

  b = t->buckets[MASH (key, kind)];
  if (b == (bucket *) 0)
    {
      return ((htData *) 0);
    }
  
  for (entry = (htEntry *) b; entry != NULL; entry = entry->next)
    {
      d = entry->data;

      if (d->kind == kind && htData_key (d) == key)
        if (kind != IK_OP || sameNameNode (n, d->content.op->name))
          {
            return d;
          }
    }
  return ((htData *) 0);
}

static bool
symHashTable_put (symHashTable *t, /*@only@*/ htData *data)
{
  /* if key is already taken, don't insert, return FALSE
     else insert it and return TRUE. */
  symbolKey key;
  htData *oldd;
  infoKind kind;
  nameNode name;

  key = htData_key (data);
  kind = data->kind;

  if (kind == IK_OP && (!data->content.op->name->isOpId))
    {
      name = data->content.op->name;
    }
  else
    {
      name = (nameNode) 0;
    }
  
  oldd = symHashTable_get (t, key, kind, name);

  if (oldd == (htData *) 0)
    {
      /*@-deparrays@*/
      bucket *new_entry = (bucket *) dmalloc (sizeof (*new_entry));
      bucket *b = (t->buckets[MASH (key, kind)]);
      htEntry *entry = (htEntry *) b;
      /*@=deparrays@*/

      new_entry->data = data;
      new_entry->next = entry;
      t->buckets[MASH (key, kind)] = new_entry;
      t->count++;

      return TRUE;
    }
  else
    {
      htData_free (data);
    }

  return FALSE;
}

static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
  symHashTable_forcePut (symHashTable *t, /*@only@*/ htData *data)
{
  /* Put data in, return old value */
  symbolKey key;
  bucket *b;
  htData *oldd;
  htEntry *entry, *new_entry;
  infoKind kind;
  nameNode name;

  key = htData_key (data);
  kind = data->kind;

  if (kind == IK_OP && (!data->content.op->name->isOpId))
    {
      name = data->content.op->name;
    }
  else
    {
      name = (nameNode) 0;
    }

  oldd = symHashTable_get (t, key, kind, name);

  if (oldd == (htData *) 0)
    {
      new_entry = (htEntry *) dmalloc (sizeof (*new_entry));

      /*@-deparrays@*/
      b = t->buckets[MASH (key, kind)];
      /*@=deparrays@*/

      entry = b;
      new_entry->data = data;
      new_entry->next = entry;
      t->buckets[MASH (key, kind)] = new_entry;
      t->count++;

      return NULL;
    }
  else
    {                           /* modify in place */
      *oldd = *data;            /* copy new info over to old info */

      /* dangerous: if the data is the same, don't free it */
      if (data != oldd)   
        {
          sfree (data); 
        /*@-branchstate@*/ 
        } 
      /*@=branchstate@*/

      return oldd;
    }
}

#if 0
static unsigned int
symHashTable_count (symHashTable * t)
{
  return (t->count);
}

#endif

static void
symHashTable_printStats (symHashTable * t)
{
  int i, bucketCount, setsize, sortCount, opCount, tagCount;
  int sortTotal, opTotal, tagTotal;
  bucket *b;
  htEntry *entry;
  htData *d;

  sortTotal = 0;
  opTotal = 0;
  tagTotal = 0;
  sortCount = 0;
  opCount = 0;
  tagCount = 0;

  /* for debugging only */
  printf ("\n Printing symHashTable stats ... \n");
  for (i = 0; i <= HT_MAXINDEX; i++)
    {
      b = t->buckets[i];
      bucketCount = 0;
      for (entry = b; entry != NULL; entry = entry->next)
        {
          d = entry->data;
          bucketCount++;
          switch (d->kind)
            {
            case IK_SORT:
              sortCount++;
              /*@switchbreak@*/ break;
            case IK_OP:
              {
                cstring name = nameNode_unparse (d->content.op->name);
                cstring sigs = sigNodeSet_unparse (d->content.op->signatures);
                opCount++;
                /* had a tt? */
                setsize = sigNodeSet_size (d->content.op->signatures);
                printf ("       Op (%d): %s %s\n", setsize, 
                        cstring_toCharsSafe (name), 
                        cstring_toCharsSafe (sigs));
                cstring_free (name);
                cstring_free (sigs);
                /*@switchbreak@*/ break;
              }
            case IK_TAG:
              tagCount++;
              /*@switchbreak@*/ break;
            }
        }
      if (bucketCount > 0)
        {
          printf ("   Bucket %d has count = %d; opCount = %d; sortCount = %d; tagCount = %d\n", i, bucketCount, opCount, sortCount, tagCount);
          sortTotal += sortCount;
          tagTotal += tagCount;
          opTotal += opCount;
        }
    }
  printf ("SymHashTable has total count = %d, opTotal = %d, sortTotal = %d, tagTotal = %d :\n", t->count, opTotal, sortTotal, tagTotal);

}

void
symtable_printStats (symtable s)
{
  symHashTable_printStats (s->hTable);
 /* for debugging only */
  printf ("idTable size = %d; allocated = %d\n",
          s->idTable->size, s->idTable->allocated);
}

/*@only@*/ cstring
tagKind_unparse (tagKind k)
{
  switch (k)
    {
    case TAG_STRUCT:
    case TAG_FWDSTRUCT:
      return cstring_makeLiteral ("struct");
    case TAG_UNION:
    case TAG_FWDUNION:
      return cstring_makeLiteral ("union");
    case TAG_ENUM:
      return cstring_makeLiteral ("enum");
    }
  BADEXIT;
}

static void tagInfo_free (/*@only@*/ tagInfo tag)
{
  sfree (tag);
}

/*@observer@*/ sigNodeSet 
  symtable_possibleOps (symtable tab, nameNode n)
{
  opInfo oi = symtable_opInfo (tab, n);
  
  if (opInfo_exists (oi))
    {
      return (oi->signatures);
    }

  return sigNodeSet_undefined;
}

bool
symtable_opExistsWithArity (symtable tab, nameNode n, int arity)
{
  opInfo oi = symtable_opInfo (tab, n);

  if (opInfo_exists (oi))
    {
      sigNodeSet sigs = oi->signatures;
      sigNodeSet_elements (sigs, sig)
      {
        if (ltokenList_size (sig->domain) == arity)
          return TRUE;
      } end_sigNodeSet_elements;
    }
  return FALSE;
}

static bool
domainMatches (ltokenList domain, sortSetList argSorts)
{
  /* expect their length to match */
  /* each domain sort in op must be an element of
     the corresponding set in argSorts. */
  bool matched = TRUE;
  sort s;

  sortSetList_reset (argSorts);
  ltokenList_elements (domain, dom)
    {
      s = sort_fromLsymbol (ltoken_getText (dom));
      if (!(sortSet_member (sortSetList_current (argSorts), s)))
        {
          /*      printf ("   mismatched element is: %s in %s\n", ltoken_getTextChars (*dom),
                  sortSet_unparse (sortSetList_current (argSorts))); */
          matched = FALSE;
          break;
        }
      sortSetList_advance (argSorts);
  } end_ltokenList_elements;

  return matched;
}

/*@only@*/ lslOpSet
  symtable_opsWithLegalDomain (symtable tab, /*@temp@*/ /*@null@*/ nameNode n,
                               sortSetList argSorts, sort qual)
{
 /* handles nil qual */
  lslOpSet ops = lslOpSet_new ();
  lslOp op;
  sort rangeSort;
  opInfo oi;

  llassert (n != NULL);
  oi = symtable_opInfo (tab, n);

  if (opInfo_exists (oi))
    {
      sigNodeSet sigs = oi->signatures;

      sigNodeSet_elements (sigs, sig)
        {
          if (ltokenList_size (sig->domain) == sortSetList_size (argSorts))
            {
              rangeSort = sigNode_rangeSort (sig);
              
              if ((qual == 0) || (sort_equal (&rangeSort, &qual)))
                {
                  if (domainMatches (sig->domain, argSorts))
                    {
                      op = (lslOp) dmalloc (sizeof (*op));
                      
                      /* each domain sort in op must be an element of
                         the corresponding set in argSorts. */
                      op->signature = sig;
                      op->name = nameNode_copy (n);
                      (void) lslOpSet_insert (ops, op);
                    }
                }
            }
        } end_sigNodeSet_elements;
    }
  return ops;
}

---