]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
616915dd | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
6 | ** This program is free software; you can redistribute it and/or modify it | |
7 | ** under the terms of the GNU General Public License as published by the | |
8 | ** Free Software Foundation; either version 2 of the License, or (at your | |
9 | ** option) any later version. | |
10 | ** | |
11 | ** This program is distributed in the hope that it will be useful, but | |
12 | ** WITHOUT ANY WARRANTY; without even the implied warranty of | |
13 | ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU | |
14 | ** General Public License for more details. | |
15 | ** | |
16 | ** The GNU General Public License is available from http://www.gnu.org/ or | |
17 | ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, | |
18 | ** MA 02111-1307, USA. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 23 | */ |
24 | /* | |
25 | ** lsymbol.c | |
26 | ** | |
27 | ** String manager | |
28 | ** | |
29 | ** This module implements an abstraction for efficiently managing | |
30 | ** string comparisons. It alloctes and manages a string context, | |
31 | ** which consists of three major data structures: | |
32 | ** - a StringEntry table | |
33 | ** - a character-string table | |
34 | ** - a hash table | |
35 | ** | |
36 | ** A StringEntry table is made of of StringEntries. StringEntries | |
37 | ** are linked in hash-chains to support fast lookup. Every | |
38 | ** allocated StringEntry corresponds to a unique character-string | |
39 | ** in the character-string table. StringEntries can be referenced | |
40 | ** via Symbol values. | |
41 | ** | |
42 | ** A character-string table is composed of character-strings. A | |
43 | ** character-string is a variable length byte array that is always | |
44 | ** null-terminated ('\0'). | |
45 | ** | |
46 | ** A hash table manages the start of each hash-list of StringEntries. | |
47 | ** StringEntries are entered into the hash-list by hashing on its | |
48 | ** character-string representation. | |
49 | ** | |
50 | ** This module provides routines for retrieving a unique Symbol for a | |
51 | ** given character-string, and returning the character-string given its | |
52 | ** corresponding Symbol. An item is allocated in both tables whenever a | |
53 | ** new character-string is encountered, otherwise the Symbol for the | |
54 | ** character-string is found and returned. | |
55 | ** | |
56 | ** AUTHORS: | |
57 | ** | |
58 | ** Shota Aki | |
59 | ** | |
60 | ** MODIFICATION HISTORY: | |
61 | ** | |
62 | ** {0} Aki at Digital -- 89.08.07 -- original | |
63 | ** {1} Aki at Digital -- 89.11.13 -- context switchable | |
64 | ** {2} Aki at Digital -- 89.11.28 -- removed use of TABLES interface | |
65 | ** {3} Aki at Digital -- 89.11.29 -- moved to RC | |
66 | ** {4} Aki at Digital -- 90.04.10 -- support primary-context | |
67 | ** {5} McKeeman at Digital -- 90.05.08 -- C to Larch SL | |
68 | ** {6} Wild at Digital -- 91.06.26 -- Update copyright notice. | |
69 | ** {n} Who at Where -- yy.mm.dd -- what | |
70 | */ | |
71 | ||
1b8ae690 | 72 | # include "splintMacros.nf" |
616915dd | 73 | # include "basic.h" |
74 | ||
75 | /*@+ignorequals@*/ | |
76 | ||
77 | /*@constant int NULLFACTOR; @*/ | |
78 | # define NULLFACTOR 1 | |
79 | ||
80 | typedef Handle CharIndex; | |
81 | ||
82 | typedef struct | |
83 | { | |
84 | lsymbol HashNext; | |
85 | CharIndex i; | |
86 | } StringEntry; | |
87 | ||
88 | static void AllocCharSpace (unsigned p_newSize) /*@modifies internalState@*/ ; | |
89 | static CharIndex AllocChar (/*@unique@*/ char *p_name) /*@modifies internalState@*/ ; | |
90 | static void AllocEntrySpace (unsigned p_newSize) /*@modifies internalState@*/ ; | |
91 | static lsymbol AllocEntry (char *p_name, long unsigned p_hashValue) | |
92 | /*@modifies internalState@*/ ; | |
93 | ||
94 | static /*@only@*/ /*@null@*/ lsymbol *hashArray = NULL; | |
95 | ||
96 | static long unsigned MaxChar; | |
97 | static CharIndex FreeChar; | |
98 | static /*@only@*/ /*@null@*/ char *CharString; | |
99 | ||
100 | static long unsigned MaxEntry; | |
101 | static lsymbol FreeEntry; | |
102 | static /*@only@*/ /*@null@*/ StringEntry *Entry; | |
103 | ||
104 | lsymbol | |
105 | lsymbol_fromString (cstring s) | |
106 | { | |
107 | if (cstring_isUndefined (s)) | |
108 | { | |
109 | return lsymbol_undefined; | |
110 | } | |
111 | else | |
112 | { | |
113 | return (lsymbol_fromChars (cstring_toCharsSafe (s))); | |
114 | } | |
115 | } | |
116 | ||
117 | lsymbol | |
118 | lsymbol_fromChars (/*@temp@*/ char *name) | |
119 | { | |
120 | lsymbol ss; | |
121 | long unsigned hashValue; | |
122 | unsigned h = 0; | |
123 | char *p = name; | |
124 | ||
125 | while (*p != '\0') | |
126 | { | |
127 | h = (h << 1) + (unsigned) (*p++); | |
128 | } | |
129 | ||
130 | hashValue = h & HASHMASK; | |
131 | ||
132 | if (hashArray == NULL) /* evs - was MaxIndex == 0 */ | |
133 | { | |
134 | /* nothing initialized */ | |
135 | ss = AllocEntry (name, hashValue); | |
136 | } | |
137 | else | |
138 | { | |
139 | ss = hashArray[hashValue]; /* start of hash chain */ | |
140 | ||
141 | if (ss == lsymbol_undefined) | |
142 | { | |
143 | /* hash not initialized */ | |
144 | ss = AllocEntry (name, hashValue); | |
145 | } | |
146 | else | |
147 | { | |
148 | /* | |
149 | * Traverse hash-chain. Loop terminates when | |
150 | * a match is found or end of chain is encountered. | |
151 | */ | |
152 | ||
153 | llassert (Entry != NULL); | |
154 | llassert (CharString != NULL); | |
155 | ||
156 | while (strcmp (&CharString[Entry[ss].i], name) != 0) | |
157 | { | |
158 | if (lsymbol_undefined == (ss = Entry[ss].HashNext)) | |
159 | { | |
160 | ss = AllocEntry (name, hashValue); | |
161 | break; | |
162 | } | |
163 | } | |
164 | } | |
165 | } | |
166 | ||
167 | return ss; | |
168 | } | |
169 | ||
170 | cstring lsymbol_toString (lsymbol ss) | |
171 | { | |
172 | return (cstring_fromChars (lsymbol_toChars (ss))); | |
173 | } | |
174 | ||
175 | char * | |
176 | lsymbol_toCharsSafe (lsymbol ss) | |
177 | { | |
178 | char *ret = lsymbol_toChars (ss); | |
179 | ||
180 | if (ret == NULL) | |
181 | { | |
182 | ret = mstring_create (0); | |
183 | } | |
184 | ||
185 | return ret; | |
186 | } | |
187 | ||
188 | char *lsymbol_toChars (lsymbol ss) | |
189 | { | |
190 | if (lsymbol_isDefined (ss)) | |
191 | { | |
192 | if (ss >= FreeEntry) | |
193 | { | |
194 | llcontbug (message ("lsymbol_toChars: invalid lsymbol: %d", ss)); | |
195 | return NULL; | |
196 | } | |
197 | ||
198 | llassert (Entry != NULL); | |
199 | llassert (CharString != NULL); | |
200 | ||
201 | return &CharString[Entry[ss].i]; | |
202 | } | |
203 | else | |
204 | { | |
205 | return NULL; | |
206 | } | |
207 | } | |
208 | ||
209 | static void | |
210 | AllocCharSpace (unsigned newSize) | |
211 | { | |
212 | llassert (newSize > MaxChar); | |
213 | ||
214 | CharString = (char *) drealloc ((void *) CharString, newSize * sizeof (*CharString)); | |
215 | MaxChar = newSize; | |
216 | /*@-compdef@*/ | |
217 | } /*@=compdef@*/ | |
218 | ||
219 | static CharIndex | |
220 | AllocChar (/*@unique@*/ char *name) | |
221 | { | |
222 | int namelength; | |
223 | CharIndex retVal; | |
224 | long unsigned size; | |
225 | CharIndex unused; | |
226 | ||
227 | namelength = size_toInt (strlen (name)); | |
228 | unused = FreeChar; | |
229 | size = MaxChar; | |
230 | ||
231 | if ((unused + namelength + NULLFACTOR) > size) | |
232 | { | |
233 | if (size == 0) | |
234 | size = INITCHARSTRING; | |
235 | else | |
236 | size = (unsigned) (DELTACHARSTRING * size); | |
237 | ||
238 | AllocCharSpace (size); | |
239 | } | |
240 | ||
241 | llassert (CharString != NULL); | |
242 | ||
243 | retVal = unused; | |
244 | strcpy (&CharString[unused], name); | |
245 | unused += namelength; | |
246 | CharString[unused] = '\0'; | |
247 | unused += 1; | |
248 | ||
249 | FreeChar = unused; | |
250 | return retVal; | |
251 | } | |
252 | ||
253 | static void | |
254 | AllocEntrySpace (unsigned newSize) | |
255 | { | |
256 | llassert (newSize > MaxEntry); | |
257 | ||
258 | /* Casts mess up checking here. */ | |
259 | /*@-mustfree@*/ | |
260 | Entry = (StringEntry *) drealloc ((void *) Entry, newSize * sizeof (*Entry)); | |
261 | /*@=mustfree@*/ | |
262 | ||
263 | if (MaxEntry == 0) MaxEntry = 1; | |
264 | ||
265 | FreeEntry = MaxEntry; | |
266 | MaxEntry = newSize; | |
267 | /*@-compdef@*/ | |
268 | } /*@=compdef@*/ | |
269 | ||
270 | static lsymbol AllocEntry (char *name, long unsigned hashValue) | |
271 | { | |
272 | lsymbol retVal; | |
273 | long unsigned size; | |
274 | ||
275 | size = MaxEntry; | |
276 | ||
277 | if ((retVal = FreeEntry) == size) | |
278 | { | |
279 | if (size == 0) | |
280 | { | |
281 | size = INITSTRINGENTRY; | |
282 | } | |
283 | else | |
284 | { | |
285 | size = (unsigned) (DELTASTRINGENTRY * size); | |
286 | } | |
287 | ||
288 | AllocEntrySpace (size); | |
289 | retVal = FreeEntry; | |
290 | } | |
291 | ||
292 | FreeEntry = retVal + 1; | |
293 | ||
294 | llassert (hashArray != NULL); | |
295 | llassert (Entry != NULL); | |
296 | ||
297 | Entry[retVal].HashNext = hashArray[hashValue]; | |
298 | hashArray[hashValue] = retVal; | |
299 | Entry[retVal].i = AllocChar (name); | |
300 | ||
301 | return retVal; | |
302 | } | |
303 | ||
304 | void | |
305 | lsymbol_initMod (void) | |
306 | /*@globals undef CharString, undef Entry; @*/ | |
307 | { | |
308 | int i; | |
309 | ||
310 | if (hashArray != NULL) | |
311 | { | |
312 | sfree (hashArray); | |
313 | } | |
314 | ||
315 | hashArray = (lsymbol *) dmalloc (HASHSIZE * sizeof (*hashArray)); | |
316 | ||
317 | for (i = 0; i < HASHSIZE; i++) | |
318 | { | |
319 | hashArray[i] = lsymbol_undefined; | |
320 | } | |
321 | ||
322 | MaxChar = 0; | |
323 | MaxEntry = 0; | |
324 | ||
325 | FreeChar = 0; | |
326 | FreeEntry = 0; | |
327 | ||
328 | CharString = (char *) 0; | |
329 | Entry = (StringEntry *) 0; | |
330 | /*@-compdef@*/ | |
331 | } | |
332 | /*@=compdef@*/ | |
333 | ||
334 | void | |
335 | lsymbol_destroyMod (void) | |
336 | /*@globals killed Entry, killed CharString, killed hashArray@*/ | |
337 | { | |
338 | sfree (Entry); | |
339 | sfree (CharString); | |
340 | sfree (hashArray); | |
341 | } | |
342 | ||
343 | void | |
344 | lsymbol_printStats (void) | |
345 | { | |
346 | /* only for debugging */ | |
347 | printf ("Number of lsymbols generated = %d\n", (int) FreeEntry); | |
348 | } | |
349 | ||
350 | /* | |
351 | ** note lsymbol_setbool, etc. defined in abstract.c | |
352 | */ | |
353 | ||
354 | ||
355 | ||
356 | ||
357 | ||
358 | ||
359 | ||
360 |