2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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 + ((int) (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
1082 (cnamestr, ctype_unknown,
1083 ti->abstract ? ynm_fromBool (ti->modifiable) : MAYBE,
1084 ti->abstract ? qual_createAbstract () : qual_createConcrete (),
1085 fileloc_copy (imploc)));
1089 symtable_enterType (g_symtab, ti);
1091 else if (firstWord (line, "var"))
1095 if (sscanf (line, "var %s %s", namestr, sostr) != 2)
1098 (message ("%q: Imported file contains illegal variable declaration. "
1099 "Skipping this line.",
1100 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce))));
1101 fileloc_free (imploc);
1105 vi = (varInfo) dmalloc (sizeof (*vi));
1106 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1107 lineptr = strchr (line, ' '); /* go past "var" */
1108 llassert (lineptr != NULL);
1109 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1110 llassert (lineptr != NULL);
1111 col = 5 + ((int) (lineptr - line)); /* 5 for initial "%LCL "*/
1113 if (sort_isNoSort (bsort))
1115 lclplainerror (message ("%q: Imported file contains unknown base sort",
1116 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1120 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1121 importfile, inputStream_thisLineNumber (srce), col);
1125 (void) symtable_enterVar (g_symtab, vi);
1130 cstring cnamestr = cstring_fromChars (namestr);
1132 if (!usymtab_existsGlobEither (cnamestr))
1135 (void) usymtab_supEntrySref
1136 (uentry_makeVariable (cnamestr, ctype_unknown,
1137 fileloc_copy (imploc),
1142 else if (firstWord (line, "const"))
1146 if (sscanf (line, "const %s %s", namestr, sostr) != 2)
1148 lclbug (message ("%q: Imported file contains illegal constant declaration: %s",
1149 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1150 cstring_fromChars (line)));
1151 fileloc_free (imploc);
1155 vi = (varInfo) dmalloc (sizeof (*vi));
1156 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1157 lineptr = strchr (line, ' '); /* go past "var" */
1158 llassert (lineptr != NULL);
1159 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1160 llassert (lineptr != NULL);
1162 col = 5 + ((int) (lineptr - line)); /* 5 for initial "%LCL "*/
1164 if (sort_isNoSort (bsort))
1166 lclplainerror (message ("%q: Imported file contains unknown base sort",
1167 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1171 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1172 importfile, inputStream_thisLineNumber (srce), col);
1174 vi->kind = VRK_CONST;
1176 (void) symtable_enterVar (g_symtab, vi);
1181 cstring cnamestr = cstring_fromChars (namestr);
1183 if (!usymtab_existsGlobEither (cnamestr))
1186 (void) usymtab_addEntry (uentry_makeConstant (cnamestr,
1188 fileloc_copy (imploc)));
1191 /* must check for "fcnGlobals" before "fcn" */
1193 else if (firstWord (line, "fcnGlobals"))
1195 pairNodeList globals;
1196 lineptr = strchr (line, 'f'); /* remove any leading blanks */
1197 llassert (lineptr != NULL);
1198 lineptr = strchr (lineptr, ' '); /* go past "fcnGlobals" */
1199 llassert (lineptr != NULL);
1201 /* a quick check for empty fcnGlobals */
1202 if (!isBlankLine (lineptr))
1204 globals = parseGlobals (lineptr, srce);
1205 /* should ensure that each global in an imported function
1206 corresponds to some existing global. Since only
1207 "correctly processed" .lcs files are imported, this is
1208 true as an invariant. */
1212 globals = pairNodeList_new ();
1215 /* check that they exist, store them on fctInfo */
1217 if (savedFcn != NULL)
1219 pairNodeList_free ((*savedFcn)->globals);
1220 (*savedFcn)->globals = globals; /* evs, moved inside if predicate */
1222 (void) symtable_enterFct (g_symtab, *savedFcn);
1228 (message ("%q: Unexpected function globals. "
1229 "Skipping this line: \n%s",
1230 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1231 cstring_fromChars (line)));
1233 pairNodeList_free (globals);
1236 else if (firstWord (line, "fcn"))
1241 if (savedFcn != (fctInfo *) 0)
1244 (message ("%q: illegal function declaration. Skipping this line:\n%s",
1245 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1246 cstring_fromChars (line)));
1247 fileloc_free (imploc);
1251 savedFcn = (fctInfo *) dmalloc (sizeof (*savedFcn));
1253 lineptr = strchr (line, 'f'); /* remove any leading blanks */
1254 llassert (lineptr != NULL);
1255 lineptr = strchr (lineptr, ' '); /* go past "fcn" */
1256 llassert (lineptr != NULL);
1258 /* add a newline to the end of the line since parseOpLine expects it */
1260 lineptr2 = strchr (lineptr, '\0');
1265 *(lineptr2 + 1) = '\0';
1268 op = parseOpLine (importfile, cstring_fromChars (lineptr + 1));
1270 if (op == (lslOp) 0)
1273 (message ("%q: illegal function declaration: %s",
1274 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1275 cstring_fromChars (line)));
1276 fileloc_free (imploc);
1280 op2 = lslOp_renameSorts (map, op);
1282 llassert (op2 != NULL);
1284 if ((op->name != NULL) && op->name->isOpId)
1286 (*savedFcn) = (fctInfo) dmalloc (sizeof (**savedFcn));
1287 (*savedFcn)->id = op->name->content.opid;
1288 (*savedFcn)->signature = signNode_fromsigNode (op2->signature);
1289 (*savedFcn)->globals = pairNodeList_new ();
1290 (*savedFcn)->export = TRUE;
1294 /* 27 Jan 1995 --- added this to be undefined namestr bug */
1295 cstring fname = ltoken_unparse ((*savedFcn)->id);
1297 if (!usymtab_existsGlobEither (fname))
1299 (void) usymtab_addEntry (uentry_makeFunction
1300 (fname, ctype_unknown,
1301 typeId_invalid, globSet_new (),
1303 warnClause_undefined,
1304 fileloc_copy (imploc)));
1310 /* evans 2001-05-27: detected by splint after fixing external alias bug. */
1311 if (op->name != NULL)
1313 ltoken_free (op->name->content.opid);
1317 (message ("%q: unexpected function name: %s",
1318 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1319 cstring_fromChars (line)));
1322 else if (firstWord (line, "enumConst"))
1326 if (sscanf (line, "enumConst %s %s", namestr, sostr) != 2)
1329 (message ("%q: Illegal enum constant declaration. "
1330 "Skipping this line:\n%s",
1331 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1332 cstring_fromChars (line)));
1333 fileloc_free (imploc);
1337 vi = (varInfo) dmalloc (sizeof (*vi));
1338 bsort = sort_lookupName (lsymbol_translateSort (map, lsymbol_fromChars (sostr)));
1339 lineptr = strchr (line, ' '); /* go past "var" */
1340 llassert (lineptr != NULL);
1341 lineptr = strchr (lineptr + 1, ' '); /* go past namestr */
1342 llassert (lineptr != NULL);
1344 col = 5 + ((int) (lineptr - line)); /* 5 for initial "%LCL "*/
1345 if (sort_isNoSort (bsort))
1347 lclplainerror (message ("%q: unknown base sort\n",
1348 fileloc_unparseRawCol (importfile, inputStream_thisLineNumber (srce), col)));
1352 vi->id = ltoken_createFull (simpleId, lsymbol_fromChars (namestr),
1353 importfile, inputStream_thisLineNumber (srce), col);
1356 vi->kind = VRK_ENUM;
1358 (void) symtable_enterVar (g_symtab, vi);
1363 cstring cnamestr = cstring_fromChars (namestr);
1364 if (!usymtab_existsEither (cnamestr))
1366 (void) usymtab_addEntry (uentry_makeConstant (cnamestr, ctype_unknown,
1367 fileloc_copy (imploc)));
1371 else if (firstWord (line, "tag"))
1373 /* do nothing, sort processing already handles this */
1378 (message ("%q: Unknown symbol declaration. Skipping this line:\n%s",
1379 fileloc_unparseRaw (importfile, inputStream_thisLineNumber (srce)),
1380 cstring_fromChars (line)));
1383 fileloc_free (imploc);
1387 symtable_import (inputStream imported, ltoken tok, mapping map)
1391 inputStream lclsource;
1393 bool old_inImport = inImport;
1395 buf = inputStream_nextLine (imported);
1396 importfile = inputStream_fileName (imported);
1398 llassert (buf != NULL);
1400 if (!firstWord (buf, "%LCLSymbolTable"))
1402 lclsource = LCLScanSource ();
1404 message ("Expecting '%%LCLSymbolTable' line in import file %s:\n%s\n",
1406 cstring_fromChars (buf)));
1409 old_lsldebug = lsldebug;
1411 allowed_redeclaration = TRUE;
1416 buf = inputStream_nextLine (imported);
1417 llassert (buf != NULL);
1420 if (firstWord (buf, "%LCLSymbolTableEnd"))
1425 { /* a good line, remove %LCL from line first */
1426 if (firstWord (buf, "%LCL"))
1428 parseLine (buf + 4, imported, map);
1432 lclsource = LCLScanSource ();
1435 message ("Expecting '%%LCL' prefix in import file %s:\n%s\n",
1437 cstring_fromChars (buf)));
1442 /* restore old value */
1443 inImport = old_inImport;
1444 lsldebug = old_lsldebug;
1445 allowed_redeclaration = FALSE;
1449 symtable_dumpId (symtable stable, FILE *f, bool lco)
1451 idTable *st = stable->idTable;
1458 for (i = 1; i < st->size; i++)
1460 /* 2/22/93 I think there is a off-by-1 error, 0 entry is never used */
1461 se = st->entries + i;
1462 llassert (se != NULL);
1465 /*@-loopswitchbreak@*/
1472 fi = (se->info).fct;
1476 fprintf (f, "%%LCL");
1479 if (!lco && !fi->export)
1481 fprintf (f, "spec ");
1484 tmp = signNode_unparse (fi->signature);
1485 fprintf (f, "fcn %s %s \n", ltoken_getTextChars (fi->id),
1486 cstring_toCharsSafe (tmp));
1489 tmp = pairNodeList_unparse (fi->globals);
1490 fprintf (f, "%%LCLfcnGlobals %s\n", cstring_toCharsSafe (tmp));
1500 /*@-switchswitchbreak@*/
1501 switch ((se->info).scope->kind)
1504 fprintf (f, "Global scope\n");
1507 fprintf (f, "Abstract type scope\n");
1510 fprintf (f, "Function scope\n");
1512 /* a let scope can only occur in a function scope, should not push
1513 a new scope, so symtable_lookupInScope works properly
1515 fprintf (f, "Let scope\n");
1518 fprintf (f, "Quantifier scope\n");
1521 fprintf (f, "Claim scope\n");
1528 ti = (se->info).type;
1530 fprintf (f, "%%LCL");
1531 if (!lco && !ti->export)
1532 fprintf (f, "spec ");
1533 fprintf (f, "type %s %s",
1534 ltoken_getTextChars (ti->id), sort_getName (ti->basedOn));
1538 fprintf (f, " mutable\n");
1540 fprintf (f, " immutable\n");
1543 fprintf (f, " exposed\n");
1547 vi = (se->info).var;
1550 fprintf (f, "%%LCL");
1553 if (!lco && !vi->export)
1555 fprintf (f, "spec ");
1560 fprintf (f, "const %s %s\n",
1561 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1564 fprintf (f, "var %s %s\n",
1565 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1568 fprintf (f, "enumConst %s %s\n",
1569 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1577 fprintf (f, "global %s %s\n", ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1579 case VRK_PRIVATE: /* for private vars within function */
1580 fprintf (f, "local %s %s\n",
1581 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1584 fprintf (f, "let %s %s\n",
1585 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1588 fprintf (f, "param %s %s\n",
1589 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1592 fprintf (f, "quant %s %s\n",
1593 ltoken_getTextChars (vi->id), sort_getName (vi->sort));
1597 /*@=loopswitchbreak@*/
1598 /*@=switchswitchbreak@*/
1605 static /*@exposed@*/ /*@out@*/ idTableEntry *
1606 nextFree (idTable * st)
1609 unsigned int n = st->size;
1611 if (n >= st->allocated)
1614 ** this loses with the garbage collector
1615 ** (and realloc is notoriously dangerous)
1617 ** st->entries = (idTableEntry *) LSLMoreMem (st->entries, (n + DELTA)
1618 ** * sizeof (idTableEntry));
1620 ** instead, we copy the symtable...
1623 idTableEntry *oldentries = st->entries;
1626 st->entries = dmalloc ((n+DELTA) * sizeof (*st->entries));
1628 for (i = 0; i < n; i++)
1630 st->entries[i] = oldentries[i];
1635 st->allocated = n + DELTA;
1638 ret = &(st->entries[st->size]);
1644 static /*@dependent@*/ /*@null@*/ idTableEntry *
1645 symtable_lookup (idTable *st, lsymbol id)
1650 for (n = st->size - 1; n >= 0; n--)
1652 e = &(st->entries[n]);
1654 /*@-loopswitchbreak@*/
1660 if (ltoken_getText (e->info.fct->id) == id) return e;
1663 if (ltoken_getText (e->info.type->id) == id) return e;
1666 if (ltoken_getText (e->info.var->id) == id) return e;
1670 /*@=loopswitchbreak@*/
1673 return (idTableEntry *) 0;
1677 static /*@dependent@*/ /*@null@*/ idTableEntry *
1678 symtable_lookupInScope (idTable *st, lsymbol id)
1682 for (n = st->size - 1; n >= 0; n--)
1684 e = &(st->entries[n]);
1685 if (e->kind == SYMK_SCOPE)
1687 if (ltoken_getText (e->info.fct->id) == id)
1692 return (idTableEntry *) 0;
1695 /* hash table implementation */
1698 htData_key (htData * x)
1700 /* assume x points to a valid htData struct */
1704 return x->content.sort;
1706 { /* get the textSym of the token */
1707 nameNode n = (x->content.op)->name;
1711 return ltoken_getText (n->content.opid);
1715 llassert (n->content.opform != NULL);
1716 return (n->content.opform)->key;
1720 return ltoken_getText ((x->content).tag->id);
1725 static void htData_free (/*@null@*/ /*@only@*/ htData *d)
1734 /* nameNode_free (d->content.op->name);*/
1735 sigNodeSet_free (d->content.op->signatures);
1739 switch (d->content.tag->kind)
1746 ** no: stDeclNodeList_free (d->content.tag->content.decls);
1749 /*@switchbreak@*/ break;
1752 /* no: ltokenList_free (d->content.tag->content.enums);
1756 /*@switchbreak@*/ break;
1765 static void bucket_free (/*@null@*/ /*@only@*/ bucket *b)
1769 bucket_free (b->next);
1770 htData_free (b->data);
1775 static void symHashTable_free (/*@only@*/ symHashTable *h)
1779 for (i = 0; i < h->size; i++)
1781 bucket_free (h->buckets[i]);
1788 static /*@only@*/ symHashTable *
1789 symHashTable_create (unsigned int size)
1792 symHashTable *t = (symHashTable *) dmalloc (sizeof (*t));
1794 t->buckets = (bucket **) dmalloc ((size + 1) * sizeof (*t->buckets));
1798 for (i = 0; i <= size; i++)
1800 t->buckets[i] = (bucket *) NULL;
1806 static /*@null@*/ /*@exposed@*/ htData *
1807 symHashTable_get (symHashTable *t, symbolKey key, infoKind kind, /*@null@*/ nameNode n)
1813 b = t->buckets[MASH (key, kind)];
1814 if (b == (bucket *) 0)
1816 return ((htData *) 0);
1819 for (entry = (htEntry *) b; entry != NULL; entry = entry->next)
1823 if (d->kind == kind && htData_key (d) == key)
1824 if (kind != IK_OP || sameNameNode (n, d->content.op->name))
1829 return ((htData *) 0);
1833 symHashTable_put (symHashTable *t, /*@only@*/ htData *data)
1835 /* if key is already taken, don't insert, return FALSE
1836 else insert it and return TRUE. */
1842 key = htData_key (data);
1845 if (kind == IK_OP && (!data->content.op->name->isOpId))
1847 name = data->content.op->name;
1851 name = (nameNode) 0;
1854 oldd = symHashTable_get (t, key, kind, name);
1856 if (oldd == (htData *) 0)
1859 bucket *new_entry = (bucket *) dmalloc (sizeof (*new_entry));
1860 bucket *b = (t->buckets[MASH (key, kind)]);
1861 htEntry *entry = (htEntry *) b;
1864 new_entry->data = data;
1865 new_entry->next = entry;
1866 t->buckets[MASH (key, kind)] = new_entry;
1879 static /*@only@*/ /*@exposed@*/ /*@null@*/ htData *
1880 symHashTable_forcePut (symHashTable *t, /*@only@*/ htData *data)
1882 /* Put data in, return old value */
1886 htEntry *entry, *new_entry;
1890 key = htData_key (data);
1893 if (kind == IK_OP && (!data->content.op->name->isOpId))
1895 name = data->content.op->name;
1899 name = (nameNode) 0;
1902 oldd = symHashTable_get (t, key, kind, name);
1904 if (oldd == (htData *) 0)
1906 new_entry = (htEntry *) dmalloc (sizeof (*new_entry));
1909 b = t->buckets[MASH (key, kind)];
1913 new_entry->data = data;
1914 new_entry->next = entry;
1915 t->buckets[MASH (key, kind)] = new_entry;
1921 { /* modify in place */
1922 *oldd = *data; /* copy new info over to old info */
1924 /* dangerous: if the data is the same, don't free it */
1938 symHashTable_count (symHashTable * t)
1946 symHashTable_printStats (symHashTable * t)
1948 int i, bucketCount, setsize, sortCount, opCount, tagCount;
1949 int sortTotal, opTotal, tagTotal;
1961 /* for debugging only */
1962 printf ("\n Printing symHashTable stats ... \n");
1963 for (i = 0; i <= HT_MAXINDEX; i++)
1967 for (entry = b; entry != NULL; entry = entry->next)
1975 /*@switchbreak@*/ break;
1978 cstring name = nameNode_unparse (d->content.op->name);
1979 cstring sigs = sigNodeSet_unparse (d->content.op->signatures);
1982 setsize = sigNodeSet_size (d->content.op->signatures);
1983 printf (" Op (%d): %s %s\n", setsize,
1984 cstring_toCharsSafe (name),
1985 cstring_toCharsSafe (sigs));
1986 cstring_free (name);
1987 cstring_free (sigs);
1988 /*@switchbreak@*/ break;
1992 /*@switchbreak@*/ break;
1995 if (bucketCount > 0)
1997 printf (" Bucket %d has count = %d; opCount = %d; sortCount = %d; tagCount = %d\n", i, bucketCount, opCount, sortCount, tagCount);
1998 sortTotal += sortCount;
1999 tagTotal += tagCount;
2003 printf ("SymHashTable has total count = %d, opTotal = %d, sortTotal = %d, tagTotal = %d :\n", t->count, opTotal, sortTotal, tagTotal);
2008 symtable_printStats (symtable s)
2010 symHashTable_printStats (s->hTable);
2011 /* for debugging only */
2012 printf ("idTable size = %d; allocated = %d\n",
2013 s->idTable->size, s->idTable->allocated);
2017 tagKind_unparse (tagKind k)
2023 return cstring_makeLiteral ("struct");
2026 return cstring_makeLiteral ("union");
2028 return cstring_makeLiteral ("enum");
2033 static void tagInfo_free (/*@only@*/ tagInfo tag)
2035 ltoken_free (tag->id);
2039 /*@observer@*/ sigNodeSet
2040 symtable_possibleOps (symtable tab, nameNode n)
2042 opInfo oi = symtable_opInfo (tab, n);
2044 if (opInfo_exists (oi))
2046 return (oi->signatures);
2049 return sigNodeSet_undefined;
2053 symtable_opExistsWithArity (symtable tab, nameNode n, int arity)
2055 opInfo oi = symtable_opInfo (tab, n);
2057 if (opInfo_exists (oi))
2059 sigNodeSet sigs = oi->signatures;
2060 sigNodeSet_elements (sigs, sig)
2062 if (ltokenList_size (sig->domain) == arity)
2064 } end_sigNodeSet_elements;
2070 domainMatches (ltokenList domain, sortSetList argSorts)
2072 /* expect their length to match */
2073 /* each domain sort in op must be an element of
2074 the corresponding set in argSorts. */
2075 bool matched = TRUE;
2078 sortSetList_reset (argSorts);
2079 ltokenList_elements (domain, dom)
2081 s = sort_fromLsymbol (ltoken_getText (dom));
2082 if (!(sortSet_member (sortSetList_current (argSorts), s)))
2084 /* printf (" mismatched element is: %s in %s\n", ltoken_getTextChars (*dom),
2085 sortSet_unparse (sortSetList_current (argSorts))); */
2089 sortSetList_advance (argSorts);
2090 } end_ltokenList_elements;
2096 symtable_opsWithLegalDomain (symtable tab, /*@temp@*/ /*@null@*/ nameNode n,
2097 sortSetList argSorts, sort q)
2099 /* handles nil qual */
2100 lslOpSet ops = lslOpSet_new ();
2105 llassert (n != NULL);
2106 oi = symtable_opInfo (tab, n);
2108 if (opInfo_exists (oi))
2110 sigNodeSet sigs = oi->signatures;
2112 sigNodeSet_elements (sigs, sig)
2114 if (ltokenList_size (sig->domain) == sortSetList_size (argSorts))
2116 rangeSort = sigNode_rangeSort (sig);
2118 if ((q == NULL) || (sort_equal (rangeSort, q)))
2120 if (domainMatches (sig->domain, argSorts))
2122 op = (lslOp) dmalloc (sizeof (*op));
2124 /* each domain sort in op must be an element of
2125 the corresponding set in argSorts. */
2126 op->signature = sig;
2127 op->name = nameNode_copy (n);
2128 (void) lslOpSet_insert (ops, op);
2132 } end_sigNodeSet_elements;