2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
27 ** Symbol table abstraction
31 ** Gary Feldman, Technical Languages and Environments, DECspec project
33 ** Massachusetts Institute of Technology
34 ** Joe Wild, Technical Languages and Environments, DECspec project
36 ** Massachusetts Institute of Technology
43 # include "splintMacros.nf"
47 # include "lclsyntable.h"
48 # include "lslparse.h"
52 static bool isBlankLine (char *p_line);
53 static bool inImport = FALSE;
55 /*@constant static int MAXBUFFLEN;@*/
56 # define MAXBUFFLEN 512
57 /*@constant static int DELTA;@*/
60 static void symHashTable_dump (symHashTable * p_t, FILE * p_f, bool p_lco);
62 static void tagInfo_free (/*@only@*/ tagInfo p_tag);
63 static /*@observer@*/ scopeInfo symtable_scopeInfo (symtable p_stable);
65 static void symtable_dumpId (symtable p_stable, FILE *p_f, bool p_lco);
66 static lsymbol nameNode2key (nameNode p_n);
70 SYMK_FCN, SYMK_SCOPE, SYMK_TYPE, SYMK_VAR
78 /*@only@*/ fctInfo fct;
79 /*@only@*/ scopeInfo scope;
80 /*@only@*/ typeInfo type;
81 /*@only@*/ varInfo var;
88 unsigned int allocated;
89 /*@relnull@*/ idTableEntry *entries;
93 struct s_symtableStruct
95 idTable *idTable; /* data is idTableEntry */
96 symHashTable *hTable; /* data is htData */
97 mapping type2sort; /* maps LCL type symbol to LSL sort */
100 static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *p_x);
101 static /*@out@*/ /*@exposed@*/ idTableEntry *nextFree (idTable * p_st);
102 static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookup (idTable * p_st, lsymbol p_id);
103 static /*@dependent@*/ /*@null@*/ idTableEntry *symtable_lookupInScope (idTable * p_st, lsymbol p_id);
105 static /*@only@*/ idTable *symtable_newIdTable (void);
106 static void idTableEntry_free (idTableEntry p_x);
108 /* Local implementatio of hash table */
110 static bool allowed_redeclaration = FALSE;
111 static symbolKey htData_key (htData *p_x);
113 static void symHashTable_free (/*@only@*/ symHashTable *p_h);
114 static /*@only@*/ symHashTable *symHashTable_create (unsigned int p_size);
115 static /*@null@*/ /*@exposed@*/ htData *
116 symHashTable_get (symHashTable * p_t, symbolKey p_key, infoKind p_kind,
117 /*@null@*/ nameNode p_n);
118 static bool symHashTable_put (symHashTable *p_t, /*@only@*/ htData *p_data);
119 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
120 symHashTable_forcePut (symHashTable * p_t, /*@only@*/ htData *p_data);
121 /* static unsigned int symHashTable_count (symHashTable * t); */
123 static void idTable_free (/*@only@*/ idTable *p_st);
125 void varInfo_free (/*@only@*/ varInfo v)
131 static /*@only@*/ varInfo varInfo_copy (varInfo v)
133 varInfo ret = (varInfo) dmalloc (sizeof (*ret));
135 ret->id = ltoken_copy (v->id);
138 ret->export = v->export;
143 void symtable_free (symtable stable)
145 /* symtable_printStats (stable); */
147 idTable_free (stable->idTable);
148 symHashTable_free (stable->hTable);
149 mapping_free (stable->type2sort);
153 static void idTable_free (idTable *st)
157 for (i = 0; i < st->size; i++)
159 idTableEntry_free (st->entries[i]);
166 static void fctInfo_free (/*@only@*/ fctInfo f)
168 signNode_free (f->signature);
169 pairNodeList_free (f->globals);
174 static void typeInfo_free (/*@only@*/ typeInfo t)
180 static void scopeInfo_free (/*@only@*/ scopeInfo s)
185 static void idTableEntry_free (idTableEntry x)
190 fctInfo_free (x.info.fct);
193 scopeInfo_free (x.info.scope);
196 typeInfo_free (x.info.type);
199 varInfo_free (x.info.var);
204 static /*@observer@*/ ltoken idTableEntry_getId (idTableEntry *x)
209 return (x->info.fct->id);
211 return ltoken_undefined;
213 return (x->info.type->id);
215 return (x->info.var->id);
218 BADBRANCHRET (ltoken_undefined);
224 symtable stable = (symtable) dmalloc (sizeof (*stable));
227 stable->idTable = symtable_newIdTable ();
228 stable->hTable = symHashTable_create (HT_MAXINDEX);
229 stable->type2sort = mapping_create ();
231 /* add builtin synonym: Bool -> bool */
233 mapping_bind (stable->type2sort, lsymbol_getBool (), lsymbol_getbool ());
236 ** done by symtable_newIdTable
237 ** st->allocated = 0;
238 ** st->entries = (idTableEntry *) 0;
239 ** st->exporting = TRUE;
242 /* this is global scope */
243 e = nextFree (stable->idTable);
244 e->kind = SYMK_SCOPE;
245 (e->info).scope = (scopeInfo) dmalloc (sizeof (*((e->info).scope)));
246 (e->info).scope->kind = SPE_GLOBAL;
251 static /*@only@*/ idTable *symtable_newIdTable (void)
253 idTable *st = (idTable *) dmalloc (sizeof (*st));
257 st->entries = (idTableEntry *) 0;
258 st->exporting = TRUE;
260 /* this was being done twice!
262 e->kind = SYMK_SCOPE;
263 (e->info).scope.kind = globScope;
270 nameNode2key (nameNode n)
276 ret = ltoken_getText (n->content.opid);
280 /* use opForm's key as its Identifier */
281 llassert (n->content.opform != NULL);
282 ret = (n->content.opform)->key;
289 ** requires: nameNode n is already in st.
293 htData_insertSignature (htData *d, /*@owned@*/ sigNode oi)
295 sigNodeSet set = d->content.op->signatures;
298 if (oi != (sigNode) 0)
300 return (sigNodeSet_insert (set, oi));
306 symtable_enterOp (symtable st, /*@only@*/ /*@notnull@*/ nameNode n,
307 /*@owned@*/ sigNode oi)
310 ** Operators are overloaded, we allow entering opInfo more than once,
311 ** even if it's the same signature.
313 ** Assumes all sorts are already entered into the symbol table
316 symHashTable *ht = st->hTable;
322 id = nameNode2key (n);
324 d = symHashTable_get (ht, id, IK_OP, n);
326 if (d == (htData *) 0)
327 { /* first signature of this operator */
328 opInfo op = (opInfo) dmalloc (sizeof (*op));
329 htData *nd = (htData *) dmalloc (sizeof (*nd));
333 if (oi != (sigNode) 0)
335 op->signatures = sigNodeSet_singleton (oi);
340 op->signatures = sigNodeSet_new ();
341 sigNode_markOwned (oi);
346 (void) symHashTable_put (ht, nd);
351 nameNode_free (n); /*<<<??? */
353 if (htData_insertSignature (d, oi))
361 symtable_enterTag (symtable st, tagInfo ti)
363 /* put ti only if it is not already in symtable */
364 symHashTable *ht = st->hTable;
366 symbolKey key = ltoken_getText (ti->id);
368 d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);
369 if (d == (htData *) 0)
371 d = (htData *) dmalloc (sizeof (*d));
374 d->content.tag->imported = context_inImport ();
375 (void) symHashTable_put (ht, d);
380 if (d->content.tag->imported)
383 d->content.tag->imported = context_inImport ();
395 symtable_enterTagForce (symtable st, tagInfo ti)
397 /* put ti, force-put if necessary */
398 symHashTable *ht = st->hTable;
400 symbolKey key = ltoken_getText (ti->id);
402 d = symHashTable_get (ht, key, IK_TAG, (nameNode) 0);
404 if (d == (htData *) 0)
406 d = (htData *) dmalloc (sizeof (*d));
410 d->content.tag->imported = context_inImport ();
411 (void) symHashTable_put (ht, d);
419 d->content.tag->imported = context_inImport ();
420 /* interpret return data later, htData * */
421 /*@i@*/ (void) symHashTable_forcePut (ht, d);
427 symtable_opInfo (symtable st, /*@notnull@*/ nameNode n)
429 symHashTable *ht = st->hTable;
430 lsymbol i = nameNode2key (n);
433 d = symHashTable_get (ht, i, IK_OP, n);
434 if (d == (htData *) 0)
439 return (d->content.op);
443 symtable_tagInfo (symtable st, lsymbol i)
445 symHashTable *ht = st->hTable;
447 d = symHashTable_get (ht, i, IK_TAG, 0);
449 if (d == (htData *) 0)
451 return (tagInfo) NULL;
454 return (d->content.tag);
458 symtable_enterScope (symtable stable, scopeInfo si)
460 idTable *st = stable->idTable;
461 idTableEntry *e = nextFree (st);
462 if (si->kind == SPE_GLOBAL)
463 llbuglit ("symtable_enterScope: SPE_GLOBAL");
464 e->kind = SYMK_SCOPE;
465 (e->info).scope = si;
469 symtable_exitScope (symtable stable)
471 idTable *st = stable->idTable;
474 if (st->entries != NULL)
476 for (n = st->size - 1; (st->entries[n]).kind != SYMK_SCOPE; n--)
483 llcontbuglit ("symtable_exitScope: no scope to exit");
491 symtable_enterFct (symtable stable, fctInfo fi)
493 idTable *st = stable->idTable;
497 if (!allowed_redeclaration &&
498 symtable_lookup (st, ltoken_getText (fi->id)) != (idTableEntry *) 0)
500 lclRedeclarationError (fi->id);
506 fi->export = st->exporting; /* && !fi->private; */
513 symtable_enterType (symtable stable, /*@only@*/ typeInfo ti)
515 idTable *st = stable->idTable;
518 scopeKind k = (symtable_scopeInfo (stable))->kind;
520 /* symtable_disp (stable); */
522 if (k != SPE_GLOBAL && k != SPE_INVALID) /* fixed for Splint */
524 llbug (message ("%q: symtable_enterType: expect global scope. (type: %s)",
525 ltoken_unparseLoc (ti->id),
526 ltoken_getRawString (ti->id)));
529 if (!allowed_redeclaration &&
530 symtable_lookup (st, ltoken_getText (ti->id)) != (idTableEntry *) 0)
532 /* ignore if Bool is re-entered */
533 if (ltoken_getText (ti->id) == lsymbol_getBool () ||
534 ltoken_getText (ti->id) == lsymbol_getbool ())
540 lclRedeclarationError (ti->id);
545 /* make sure it is a type TYPEDEF_NAME; */
547 if (ltoken_getCode (ti->id) != LLT_TYPEDEF_NAME)
549 lclbug (message ("symtable_enterType: gets a simpleId, expect a type: %s",
550 ltoken_getRawString (ti->id)));
555 ti->export = st->exporting;/* && !ti->private; */
557 mapping_bind (stable->type2sort, ltoken_getText (ti->id),
558 sort_getLsymbol (sort_makeVal (sort_getUnderlying (ti->basedOn))));
567 lsymbol_sortFromType (symtable s, lsymbol typename)
572 /* check the synonym table first */
573 if (LCLIsSyn (typename))
575 tok = LCLGetTokenForSyn (typename);
576 inter = ltoken_getText (tok);
577 /* printf ("In lsymbol_sortFromType: %s -> %s\n",
578 lsymbol_toChars (typename), lsymbol_toChars (inter)); */
585 /* now map LCL type to sort */
586 out = mapping_find (s->type2sort, inter);
588 if (out == lsymbol_undefined)
599 ** returns true is vi is a redeclaration
603 symtable_enterVar (symtable stable, /*@temp@*/ varInfo vi)
605 idTable *st = stable->idTable;
610 /* symtable_disp (symtab); */
612 if (!allowed_redeclaration &&
613 (symtable_lookupInScope (st, ltoken_getText (vi->id)) != (idTableEntry *) 0))
615 if (ltoken_getText (vi->id) == lsymbol_getTRUE () ||
616 ltoken_getText (vi->id) == lsymbol_getFALSE ())
622 if (usymtab_existsEither (ltoken_getRawString (vi->id)))
624 lclRedeclarationError (vi->id);
629 llbuglit ("redeclared somethingerother?!");
636 idTableEntry *e = nextFree (st);
639 vi->export = st->exporting && /* !vi.private && */
640 (vi->kind == VRK_VAR || vi->kind == VRK_CONST || vi->kind == VRK_ENUM);
641 (e->info).var = varInfo_copy (vi);
648 symtable_exists (symtable stable, lsymbol i)
650 idTable *st = stable->idTable;
651 return symtable_lookup (st, i) != (idTableEntry *) 0;
655 symtable_typeInfo (symtable stable, lsymbol i)
660 st = stable->idTable;
661 e = symtable_lookup (st, i);
663 if (e == (idTableEntry *) 0 || e->kind != SYMK_TYPE)
665 return (typeInfo) NULL;
668 return (e->info).type;
672 symtable_varInfo (symtable stable, lsymbol i)
674 idTable *st = stable->idTable;
677 e = symtable_lookup (st, i);
679 if (e == (idTableEntry *) 0 || e->kind != SYMK_VAR)
681 return (varInfo) NULL;
684 return (e->info).var;
688 symtable_varInfoInScope (symtable stable, lsymbol id)
690 /* if current scope is a SPE_QUANT, can go beyond current scope */
691 idTable *st = stable->idTable;
692 idTableEntry *e2 = (idTableEntry *) 0;
695 for (n = st->size - 1; n >= 0; n--)
699 e2 = &(st->entries[n]);
701 if (e2->kind == SYMK_SCOPE && e2->info.scope->kind != SPE_QUANT)
703 return (varInfo) NULL;
706 tok = idTableEntry_getId (e2);
708 if (e2->kind == SYMK_VAR && ltoken_getText (tok) == id)
710 return (e2->info).var;
714 return (varInfo) NULL;
718 symtable_scopeInfo (symtable stable)
720 idTable *st = stable->idTable;
724 for (n = st->size - 1; n >= 0; n--)
726 e = &(st->entries[n]);
727 if (e->kind == SYMK_SCOPE)
728 return (e->info).scope;
731 lclfatalbug ("symtable_scopeInfo: not found");
736 symtable_export (symtable stable, bool yesNo)
738 idTable *st = stable->idTable;
739 st->exporting = yesNo;
740 (void) sort_setExporting (yesNo);
744 symHashTable_dump (symHashTable * t, FILE * f, bool lco)
746 /* like symHashTable_dump2 but for output to .lcs file */
754 for (i = 0; i <= HT_MAXINDEX; i++)
758 for (entry = b; entry != NULL; entry = entry->next)
765 /*@switchbreak@*/ break;
768 char *name = cstring_toCharsSafe (nameNode_unparse (d->content.op->name));
769 sigs = d->content.op->signatures;
770 size = sigNodeSet_size (sigs);
773 sigNodeSet_elements (sigs, x)
775 cstring s = sigNode_unparse (x);
779 fprintf (f, "%%LCL");
782 fprintf (f, "op %s %s\n", name, cstring_toCharsSafe (s));
784 } end_sigNodeSet_elements;
787 /*@switchbreak@*/ break;
790 tok = d->content.tag->id;
792 if (!ltoken_isUndefined (tok))
794 cstring s = tagKind_unparse (d->content.tag->kind);
798 fprintf (f, "%%LCL");
801 fprintf (f, "tag %s %s\n", ltoken_getTextChars (tok),
802 cstring_toCharsSafe (s));
805 /*@switchbreak@*/ break;
812 symtable_dump (symtable stable, FILE * f, bool lco)
814 symHashTable *ht = stable->hTable;
817 fprintf (f, "%s\n", BEGINSYMTABLE);
819 symHashTable_dump (ht, f, lco);
821 symtable_dumpId (stable, f, lco);
823 fprintf (f, "%s\n", SYMTABLEEND);
827 lsymbol_translateSort (mapping m, lsymbol s)
829 lsymbol res = mapping_find (m, s);
830 if (res == lsymbol_undefined)
835 static /*@null@*/ lslOp
836 lslOp_renameSorts (mapping map,/*@returned@*/ /*@null@*/ lslOp op)
845 sign = op->signature;
847 domain = sign->domain;
849 ltokenList_elements (domain, dt)
852 lsymbol_translateSort (map, ltoken_getText (dt)));
853 } end_ltokenList_elements;
855 /*@-onlytrans@*/ /* A memory leak... */
856 op->signature = makesigNode (sign->tok, domain, range);
863 static /*@null@*/ signNode
864 signNode_fromsigNode (sigNode s)
869 if (s == (sigNode) 0)
874 sign = (signNode) dmalloc (sizeof (*sign));
875 slist = sortList_new ();
876 sign->tok = ltoken_copy (s->tok);
878 sign->range = sort_makeSort (ltoken_undefined, ltoken_getText (s->range));
880 ltokenList_elements (s->domain, dt)
882 sortList_addh (slist, sort_makeSort (ltoken_undefined, ltoken_getText (dt)));
883 } end_ltokenList_elements;
885 sign->domain = slist;
890 /** 2.4.3 ymtan 93.09.23 -- fixed bug in parseGlobals: removed ";" at the
891 ** end of pairNode (gstr).
894 static /*@only@*/ pairNodeList
895 parseGlobals (char *line, inputStream srce)
897 pairNodeList plist = pairNodeList_new ();
900 char *lineptr, sostr[MAXBUFFLEN], gstr[MAXBUFFLEN];
902 /* line is not all blank */
903 /* expected format: "sort1 g1; sort2 g2; sort3 g3;" */
906 while (!isBlankLine (lineptr))
908 if (sscanf (lineptr, "%s %s", &(sostr[0]), gstr) != 2)
912 ("%q: Imported file contains illegal function global declaration.\n"
913 "Skipping rest of the line: %s (%s)",
914 fileloc_unparseRaw (inputStream_fileName (srce),
915 inputStream_thisLineNumber (srce)),
916 cstring_fromChars (line),
917 cstring_fromChars (lineptr)));
921 p = (pairNode) dmalloc (sizeof (*p));
923 /* Note: remove the ";" separator at the end of gstr */
924 semi_index = size_toInt (strlen (gstr));
925 gstr[semi_index - 1] = '\0';
927 p->tok = ltoken_create (NOTTOKEN, lsymbol_fromChars (gstr));
928 p->sort = sort_makeSort (ltoken_undefined, lsymbol_fromChars (sostr));
930 pairNodeList_addh (plist, p);
931 lineptr = strchr (lineptr, ';'); /* go pass the next; */
933 llassert (lineptr != NULL);
934 lineptr = lineptr + 1;
941 isBlankLine (char *line)
945 if (line == NULL) return TRUE;
947 for (i = 0; line[i] != '\0'; i++)
960 typedef /*@only@*/ fctInfo o_fctInfo;
963 parseLine (char *line, inputStream srce, mapping map)
965 static /*@owned@*/ o_fctInfo *savedFcn = NULL;
966 char *lineptr, *lineptr2;
967 cstring importfile = inputStream_fileName (srce);
968 char namestr[MAXBUFFLEN], kstr[20], sostr[MAXBUFFLEN];
969 sort bsort, nullSort = sort_makeNoSort ();
971 fileloc imploc = fileloc_undefined;
976 imploc = fileloc_createImport (importfile, inputStream_thisLineNumber (srce));
979 if (firstWord (line, "op"))
983 lineptr = strchr (line, 'o'); /* remove any leading blanks */
984 llassert (lineptr != NULL);
985 lineptr = strchr (lineptr, ' '); /* go past "op" */
986 llassert (lineptr != NULL);
988 /* add a newline to the end of the line since parseOpLine expects it */
989 lineptr2 = strchr (lineptr, '\0');
994 *(lineptr2 + 1) = '\0';
997 llassert (cstring_isDefined (importfile));
998 op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
1000 if (op == (lslOp) 0)
1004 ("%q: Imported file contains illegal operator declaration:\n "
1005 "skipping this line: %s",
1006 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1007 cstring_fromChars (line)));
1008 fileloc_free (imploc);
1012 op = lslOp_renameSorts (map, op);
1014 llassert (op != NULL);
1015 llassert (op->name != NULL);
1017 symtable_enterOp (g_symtab, op->name,
1018 sigNode_copy (op->signature));
1019 /*@-mustfree@*/ } /*@=mustfree@*/
1020 else if (firstWord (line, "type"))
1024 if (sscanf (line, "type %s %s %s", namestr, sostr, kstr) != 3)
1027 (message ("%q: illegal type declaration:\n skipping this line: %s",
1028 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1029 cstring_fromChars (line)));
1030 fileloc_free (imploc);
1034 ti = (typeInfo) dmalloc (sizeof (*ti));
1035 ti->id = ltoken_createFull (LLT_TYPEDEF_NAME, lsymbol_fromChars (namestr),
1036 importfile, inputStream_thisLineNumber (srce), col);
1038 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1040 if (sort_isNoSort (bsort))
1042 lineptr = strchr (line, ' '); /* go past "type" */
1043 llassert (lineptr != NULL);
1044 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1045 llassert (lineptr != NULL);
1046 col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1048 lclbug (message ("%q: Imported files contains unknown base sort",
1049 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1053 ti->basedOn = bsort;
1055 if (strcmp (kstr, "exposed") == 0)
1057 ti->abstract = FALSE;
1058 ti->modifiable = TRUE;
1062 ti->abstract = TRUE;
1063 if (strcmp (kstr, "mutable") == 0)
1064 ti->modifiable = TRUE;
1066 ti->modifiable = FALSE;
1071 ** sort of a hack to get imports to work...
1076 cstring cnamestr = cstring_fromChars (namestr);
1078 if (!usymtab_existsGlobEither (cnamestr))
1080 (void) usymtab_addEntry
1081 (uentry_makeDatatype (cnamestr, ctype_unknown,
1082 ti->abstract ? ynm_fromBool (ti->modifiable) : MAYBE,
1083 ti->abstract ? YES : NO,
1084 fileloc_copy (imploc)));
1088 symtable_enterType (g_symtab, ti);
1090 else if (firstWord (line, "var"))
1094 if (sscanf (line, "var %s %s", namestr, sostr) != 2)
1097 (message ("%q: Imported file contains illegal variable declaration. "
1098 "Skipping this line.",
1099 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce))));
1100 fileloc_free (imploc);
1104 vi = (varInfo) dmalloc (sizeof (*vi));
1105 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1106 lineptr = strchr (line, ' '); /* go past "var" */
1107 llassert (lineptr != NULL);
1108 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1109 llassert (lineptr != NULL);
1110 col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1112 if (sort_isNoSort (bsort))
1114 lclplainerror (message ("%q: Imported file contains unknown base sort",
1115 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1119 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1120 importfile, inputStream_thisLineNumber (srce), col);
1124 (void) symtable_enterVar (g_symtab, vi);
1129 cstring cnamestr = cstring_fromChars (namestr);
1131 if (!usymtab_existsGlobEither (cnamestr))
1134 (void) usymtab_supEntrySref
1135 (uentry_makeVariable (cnamestr, ctype_unknown,
1136 fileloc_copy (imploc),
1141 else if (firstWord (line, "const"))
1145 if (sscanf (line, "const %s %s", namestr, sostr) != 2)
1147 lclbug (message ("%q: Imported file contains illegal constant declaration: %s",
1148 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1149 cstring_fromChars (line)));
1150 fileloc_free (imploc);
1154 vi = (varInfo) dmalloc (sizeof (*vi));
1155 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1156 lineptr = strchr (line, ' '); /* go past "var" */
1157 llassert (lineptr != NULL);
1158 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1159 llassert (lineptr != NULL);
1161 col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1163 if (sort_isNoSort (bsort))
1165 lclplainerror (message ("%q: Imported file contains unknown base sort",
1166 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1170 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1171 importfile, inputStream_thisLineNumber (srce), col);
1173 vi->kind = VRK_CONST;
1175 (void) symtable_enterVar (g_symtab, vi);
1180 cstring cnamestr = cstring_fromChars (namestr);
1182 if (!usymtab_existsGlobEither (cnamestr))
1185 (void) usymtab_addEntry (uentry_makeConstant (cnamestr,
1187 fileloc_copy (imploc)));
1190 /* must check for "fcnGlobals" before "fcn" */
1192 else if (firstWord (line, "fcnGlobals"))
1194 pairNodeList globals;
1195 lineptr = strchr (line, 'f'); /* remove any leading blanks */
1196 llassert (lineptr != NULL);
1197 lineptr = strchr (lineptr, ' '); /* go past "fcnGlobals" */
1198 llassert (lineptr != NULL);
1200 /* a quick check for empty fcnGlobals */
1201 if (!isBlankLine (lineptr))
1203 globals = parseGlobals (lineptr, srce);
1204 /* should ensure that each global in an imported function
1205 corresponds to some existing global. Since only
1206 "correctly processed" .lcs files are imported, this is
1207 true as an invariant. */
1211 globals = pairNodeList_new ();
1214 /* check that they exist, store them on fctInfo */
1216 if (savedFcn != NULL)
1218 pairNodeList_free ((*savedFcn)->globals);
1219 (*savedFcn)->globals = globals; /* evs, moved inside if predicate */
1221 (void) symtable_enterFct (g_symtab, *savedFcn);
1227 (message ("%q: Unexpected function globals. "
1228 "Skipping this line: \n%s",
1229 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1230 cstring_fromChars (line)));
1232 pairNodeList_free (globals);
1235 else if (firstWord (line, "fcn"))
1240 if (savedFcn != (fctInfo *) 0)
1243 (message ("%q: illegal function declaration. Skipping this line:\n%s",
1244 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1245 cstring_fromChars (line)));
1246 fileloc_free (imploc);
1250 savedFcn = (fctInfo *) dmalloc (sizeof (*savedFcn));
1252 lineptr = strchr (line, 'f'); /* remove any leading blanks */
1253 llassert (lineptr != NULL);
1254 lineptr = strchr (lineptr, ' '); /* go past "fcn" */
1255 llassert (lineptr != NULL);
1257 /* add a newline to the end of the line since parseOpLine expects it */
1259 lineptr2 = strchr (lineptr, '\0');
1264 *(lineptr2 + 1) = '\0';
1267 op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
1269 if (op == (lslOp) 0)
1272 (message ("%q: illegal function declaration: %s",
1273 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1274 cstring_fromChars (line)));
1275 fileloc_free (imploc);
1279 op2 = lslOp_renameSorts (map, op);
1281 llassert (op2 != NULL);
1283 if ((op->name != NULL) && op->name->isOpId)
1285 (*savedFcn) = (fctInfo) dmalloc (sizeof (**savedFcn));
1286 (*savedFcn)->id = op->name->content.opid;
1287 (*savedFcn)->signature = signNode_fromsigNode (op2->signature);
1288 (*savedFcn)->globals = pairNodeList_new ();
1289 (*savedFcn)->export = TRUE;
1293 /* 27 Jan 1995 --- added this to be undefined namestr bug */
1294 cstring fname = ltoken_unparse ((*savedFcn)->id);
1296 if (!usymtab_existsGlobEither (fname))
1298 (void) usymtab_addEntry (uentry_makeFunction
1299 (fname, ctype_unknown,
1300 typeId_invalid, globSet_new (),
1302 warnClause_undefined,
1303 fileloc_copy (imploc)));
1309 /* evans 2001-05-27: detected by splint after fixing external alias bug. */
1310 if (op->name != NULL)
1312 ltoken_free (op->name->content.opid);
1316 (message ("%q: unexpected function name: %s",
1317 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1318 cstring_fromChars (line)));
1321 else if (firstWord (line, "enumConst"))
1325 if (sscanf (line, "enumConst %s %s", namestr, sostr) != 2)
1328 (message ("%q: Illegal enum constant declaration. "
1329 "Skipping this line:\n%s",
1330 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1331 cstring_fromChars (line)));
1332 fileloc_free (imploc);
1336 vi = (varInfo) dmalloc (sizeof (*vi));
1337 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1338 lineptr = strchr (line, ' '); /* go past "var" */
1339 llassert (lineptr != NULL);
1340 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1341 llassert (lineptr != NULL);
1343 col = 5 + lineptr - line; /* 5 for initial "%LCL "*/
1344 if (sort_isNoSort (bsort))
1346 lclplainerror (message ("%q: unknown base sort\n",
1347 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1351 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1352 importfile, inputStream_thisLineNumber (srce), col);
1355 vi->kind = VRK_ENUM;
1357 (void) symtable_enterVar (g_symtab, vi);
1362 cstring cnamestr = cstring_fromChars (namestr);
1363 if (!usymtab_existsEither (cnamestr))
1365 (void) usymtab_addEntry (uentry_makeConstant (cnamestr, ctype_unknown,
1366 fileloc_copy (imploc)));
1370 else if (firstWord (line, "tag"))
1372 /* do nothing, sort processing already handles this */
1377 (message ("%q: Unknown symbol declaration. Skipping this line:\n%s",
1378 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1379 cstring_fromChars (line)));
1382 fileloc_free (imploc);
1386 symtable_import (inputStream imported, ltoken tok, mapping map)
1390 inputStream lclsource;
1392 bool old_inImport = inImport;
1394 buf = inputStream_nextLine (imported);
1395 importfile = inputStream_fileName (imported);
1397 llassert (buf != NULL);
1399 if (!firstWord (buf, "%LCLSymbolTable"))
1401 lclsource = LCLScanSource ();
1403 message ("Expecting '%%LCLSymbolTable' line in import file %s:\n%s\n",
1405 cstring_fromChars (buf)));
1408 old_lsldebug = lsldebug;
1410 allowed_redeclaration = TRUE;
1415 buf = inputStream_nextLine (imported);
1416 llassert (buf != NULL);
1419 if (firstWord (buf, "%LCLSymbolTableEnd"))
1424 { /* a good line, remove %LCL from line first */
1425 if (firstWord (buf, "%LCL"))
1427 parseLine (buf + 4, imported, map);
1431 lclsource = LCLScanSource ();
1434 message ("Expecting '%%LCL' prefix in import file %s:\n%s\n",
1436 cstring_fromChars (buf)));
1441 /* restore old value */
1442 inImport = old_inImport;
1443 lsldebug = old_lsldebug;
1444 allowed_redeclaration = FALSE;
1448 symtable_dumpId (symtable stable, FILE *f, bool lco)
1450 idTable *st = stable->idTable;
1457 for (i = 1; i < st->size; i++)
1459 /* 2/22/93 I think there is a off-by-1 error, 0 entry is never used */
1460 se = st->entries + i;
1461 llassert (se != NULL);
1464 /*@-loopswitchbreak@*/
1471 fi = (se->info).fct;
1475 fprintf (f, "%%LCL");
1478 if (!lco && !fi->export)
1480 fprintf (f, "spec ");
1483 tmp = signNode_unparse (fi->signature);
1484 fprintf (f, "fcn %s %s \n", ltoken_getTextChars (fi->id),
1485 cstring_toCharsSafe (tmp));
1488 tmp = pairNodeList_unparse (fi->globals);
1489 fprintf (f, "%%LCLfcnGlobals %s\n", cstring_toCharsSafe (tmp));
1499 /*@-switchswitchbreak@*/
1500 switch ((se->info).scope->kind)
1503 fprintf (f, "Global scope\n");
1506 fprintf (f, "Abstract type scope\n");
1509 fprintf (f, "Function scope\n");
1511 /* a let scope can only occur in a function scope, should not push
1512 a new scope, so symtable_lookupInScope works properly
1514 fprintf (f, "Let scope\n");
1517 fprintf (f, "Quantifier scope\n");
1520 fprintf (f, "Claim scope\n");
1527 ti = (se->info).type;
1529 fprintf (f, "%%LCL");
1530 if (!lco && !ti->export)
1531 fprintf (f, "spec ");
1532 fprintf (f, "type %s %s",
1533 ltoken_getTextChars (ti->id), sort_getName (ti->basedOn));
1537 fprintf (f, " mutable\n");
1539 fprintf (f, " immutable\n");
1542 fprintf (f, " exposed\n");
1546 vi = (se->info).var;
1549 fprintf (f, "%%LCL");
1552 if (!lco && !vi->export)
1554 fprintf (f, "spec ");
1559 fprintf (f, "const %s %s\n",
1560 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1563 fprintf (f, "var %s %s\n",
1564 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1567 fprintf (f, "enumConst %s %s\n",
1568 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1576 fprintf (f, "global %s %s\n", ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1578 case VRK_PRIVATE: /* for private vars within function */
1579 fprintf (f, "local %s %s\n",
1580 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1583 fprintf (f, "let %s %s\n",
1584 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1587 fprintf (f, "param %s %s\n",
1588 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1591 fprintf (f, "quant %s %s\n",
1592 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1596 /*@=loopswitchbreak@*/
1597 /*@=switchswitchbreak@*/
1604 static /*@exposed@*/ /*@out@*/ idTableEntry *
1605 nextFree (idTable * st)
1608 unsigned int n = st->size;
1610 if (n >= st->allocated)
1613 ** this loses with the garbage collector
1614 ** (and realloc is notoriously dangerous)
1616 ** st->entries = (idTableEntry *) LSLMoreMem (st->entries, (n + DELTA)
1617 ** * sizeof (idTableEntry));
1619 ** instead, we copy the symtable...
1622 idTableEntry *oldentries = st->entries;
1625 st->entries = dmalloc ((n+DELTA) * sizeof (*st->entries));
1627 for (i = 0; i < n; i++)
1629 st->entries[i] = oldentries[i];
1634 st->allocated = n + DELTA;
1637 ret = &(st->entries[st->size]);
1643 static /*@dependent@*/ /*@null@*/ idTableEntry *
1644 symtable_lookup (idTable *st, lsymbol id)
1649 for (n = st->size - 1; n >= 0; n--)
1651 e = &(st->entries[n]);
1653 /*@-loopswitchbreak@*/
1659 if (ltoken_getText (e->info.fct->id) == id) return e;
1662 if (ltoken_getText (e->info.type->id) == id) return e;
1665 if (ltoken_getText (e->info.var->id) == id) return e;
1669 /*@=loopswitchbreak@*/
1672 return (idTableEntry *) 0;
1676 static /*@dependent@*/ /*@null@*/ idTableEntry *
1677 symtable_lookupInScope (idTable *st, lsymbol id)
1681 for (n = st->size - 1; n >= 0; n--)
1683 e = &(st->entries[n]);
1684 if (e->kind == SYMK_SCOPE)
1686 if (ltoken_getText (e->info.fct->id) == id)
1691 return (idTableEntry *) 0;
1694 /* hash table implementation */
1697 htData_key (htData * x)
1699 /* assume x points to a valid htData struct */
1703 return x->content.sort;
1705 { /* get the textSym of the token */
1706 nameNode n = (x->content.op)->name;
1710 return ltoken_getText (n->content.opid);
1714 llassert (n->content.opform != NULL);
1715 return (n->content.opform)->key;
1719 return ltoken_getText ((x->content).tag->id);
1724 static void htData_free (/*@null@*/ /*@only@*/ htData *d)
1733 /* nameNode_free (d->content.op->name);*/
1734 sigNodeSet_free (d->content.op->signatures);
1738 switch (d->content.tag->kind)
1745 ** no: stDeclNodeList_free (d->content.tag->content.decls);
1748 /*@switchbreak@*/ break;
1751 /* no: ltokenList_free (d->content.tag->content.enums);
1755 /*@switchbreak@*/ break;
1764 static void bucket_free (/*@null@*/ /*@only@*/ bucket *b)
1768 bucket_free (b->next);
1769 htData_free (b->data);
1774 static void symHashTable_free (/*@only@*/ symHashTable *h)
1778 for (i = 0; i < h->size; i++)
1780 bucket_free (h->buckets[i]);
1787 static /*@only@*/ symHashTable *
1788 symHashTable_create (unsigned int size)
1791 symHashTable *t = (symHashTable *) dmalloc (sizeof (*t));
1793 t->buckets = (bucket **) dmalloc ((size + 1) * sizeof (*t->buckets));
1797 for (i = 0; i <= size; i++)
1799 t->buckets[i] = (bucket *) NULL;
1805 static /*@null@*/ /*@exposed@*/ htData *
1806 symHashTable_get (symHashTable *t, symbolKey key, infoKind kind, /*@null@*/ nameNode n)
1812 b = t->buckets[MASH (key, kind)];
1813 if (b == (bucket *) 0)
1815 return ((htData *) 0);
1818 for (entry = (htEntry *) b; entry != NULL; entry = entry->next)
1822 if (d->kind == kind && htData_key (d) == key)
1823 if (kind != IK_OP || sameNameNode (n, d->content.op->name))
1828 return ((htData *) 0);
1832 symHashTable_put (symHashTable *t, /*@only@*/ htData *data)
1834 /* if key is already taken, don't insert, return FALSE
1835 else insert it and return TRUE. */
1841 key = htData_key (data);
1844 if (kind == IK_OP && (!data->content.op->name->isOpId))
1846 name = data->content.op->name;
1850 name = (nameNode) 0;
1853 oldd = symHashTable_get (t, key, kind, name);
1855 if (oldd == (htData *) 0)
1858 bucket *new_entry = (bucket *) dmalloc (sizeof (*new_entry));
1859 bucket *b = (t->buckets[MASH (key, kind)]);
1860 htEntry *entry = (htEntry *) b;
1863 new_entry->data = data;
1864 new_entry->next = entry;
1865 t->buckets[MASH (key, kind)] = new_entry;
1878 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
1879 symHashTable_forcePut (symHashTable *t, /*@only@*/ htData *data)
1881 /* Put data in, return old value */
1885 htEntry *entry, *new_entry;
1889 key = htData_key (data);
1892 if (kind == IK_OP && (!data->content.op->name->isOpId))
1894 name = data->content.op->name;
1898 name = (nameNode) 0;
1901 oldd = symHashTable_get (t, key, kind, name);
1903 if (oldd == (htData *) 0)
1905 new_entry = (htEntry *) dmalloc (sizeof (*new_entry));
1908 b = t->buckets[MASH (key, kind)];
1912 new_entry->data = data;
1913 new_entry->next = entry;
1914 t->buckets[MASH (key, kind)] = new_entry;
1920 { /* modify in place */
1921 *oldd = *data; /* copy new info over to old info */
1923 /* dangerous: if the data is the same, don't free it */
1937 symHashTable_count (symHashTable * t)
1945 symHashTable_printStats (symHashTable * t)
1947 int i, bucketCount, setsize, sortCount, opCount, tagCount;
1948 int sortTotal, opTotal, tagTotal;
1960 /* for debugging only */
1961 printf ("\n Printing symHashTable stats ... \n");
1962 for (i = 0; i <= HT_MAXINDEX; i++)
1966 for (entry = b; entry != NULL; entry = entry->next)
1974 /*@switchbreak@*/ break;
1977 cstring name = nameNode_unparse (d->content.op->name);
1978 cstring sigs = sigNodeSet_unparse (d->content.op->signatures);
1981 setsize = sigNodeSet_size (d->content.op->signatures);
1982 printf (" Op (%d): %s %s\n", setsize,
1983 cstring_toCharsSafe (name),
1984 cstring_toCharsSafe (sigs));
1985 cstring_free (name);
1986 cstring_free (sigs);
1987 /*@switchbreak@*/ break;
1991 /*@switchbreak@*/ break;
1994 if (bucketCount > 0)
1996 printf (" Bucket %d has count = %d; opCount = %d; sortCount = %d; tagCount = %d\n", i, bucketCount, opCount, sortCount, tagCount);
1997 sortTotal += sortCount;
1998 tagTotal += tagCount;
2002 printf ("SymHashTable has total count = %d, opTotal = %d, sortTotal = %d, tagTotal = %d :\n", t->count, opTotal, sortTotal, tagTotal);
2007 symtable_printStats (symtable s)
2009 symHashTable_printStats (s->hTable);
2010 /* for debugging only */
2011 printf ("idTable size = %d; allocated = %d\n",
2012 s->idTable->size, s->idTable->allocated);
2016 tagKind_unparse (tagKind k)
2022 return cstring_makeLiteral ("struct");
2025 return cstring_makeLiteral ("union");
2027 return cstring_makeLiteral ("enum");
2032 static void tagInfo_free (/*@only@*/ tagInfo tag)
2034 ltoken_free (tag->id);
2038 /*@observer@*/ sigNodeSet
2039 symtable_possibleOps (symtable tab, nameNode n)
2041 opInfo oi = symtable_opInfo (tab, n);
2043 if (opInfo_exists (oi))
2045 return (oi->signatures);
2048 return sigNodeSet_undefined;
2052 symtable_opExistsWithArity (symtable tab, nameNode n, int arity)
2054 opInfo oi = symtable_opInfo (tab, n);
2056 if (opInfo_exists (oi))
2058 sigNodeSet sigs = oi->signatures;
2059 sigNodeSet_elements (sigs, sig)
2061 if (ltokenList_size (sig->domain) == arity)
2063 } end_sigNodeSet_elements;
2069 domainMatches (ltokenList domain, sortSetList argSorts)
2071 /* expect their length to match */
2072 /* each domain sort in op must be an element of
2073 the corresponding set in argSorts. */
2074 bool matched = TRUE;
2077 sortSetList_reset (argSorts);
2078 ltokenList_elements (domain, dom)
2080 s = sort_fromLsymbol (ltoken_getText (dom));
2081 if (!(sortSet_member (sortSetList_current (argSorts), s)))
2083 /* printf (" mismatched element is: %s in %s\n", ltoken_getTextChars (*dom),
2084 sortSet_unparse (sortSetList_current (argSorts))); */
2088 sortSetList_advance (argSorts);
2089 } end_ltokenList_elements;
2095 symtable_opsWithLegalDomain (symtable tab, /*@temp@*/ /*@null@*/ nameNode n,
2096 sortSetList argSorts, sort qual)
2098 /* handles nil qual */
2099 lslOpSet ops = lslOpSet_new ();
2104 llassert (n != NULL);
2105 oi = symtable_opInfo (tab, n);
2107 if (opInfo_exists (oi))
2109 sigNodeSet sigs = oi->signatures;
2111 sigNodeSet_elements (sigs, sig)
2113 if (ltokenList_size (sig->domain) == sortSetList_size (argSorts))
2115 rangeSort = sigNode_rangeSort (sig);
2117 if ((qual == 0) || (sort_equal (rangeSort, qual)))
2119 if (domainMatches (sig->domain, argSorts))
2121 op = (lslOp) dmalloc (sizeof (*op));
2123 /* each domain sort in op must be an element of
2124 the corresponding set in argSorts. */
2125 op->signature = sig;
2126 op->name = nameNode_copy (n);
2127 (void) lslOpSet_insert (ops, op);
2131 } end_sigNodeSet_elements;