Readded files.

[splint.git] / src / symtable.c

/*
** 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;
}


/**  2.4.3 ymtan  93.09.23  -- fixed bug in parseGlobals: removed ";" at the
 **                            end of pairNode (gstr).
 */

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;
}