]>
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 | ** abstract.c | |
26 | ** | |
27 | ** Module for building abstract syntax trees for LCL. | |
28 | ** | |
29 | ** This module is too close to the surface syntax of LCL. | |
30 | ** Suffices for now. | |
31 | ** | |
32 | ** AUTHOR: | |
33 | ** Yang Meng Tan, | |
34 | ** Massachusetts Institute of Technology | |
35 | */ | |
36 | ||
1b8ae690 | 37 | # include "splintMacros.nf" |
b73d1009 | 38 | # include "basic.h" |
616915dd | 39 | # include "lslparse.h" |
40 | # include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */ | |
41 | # include "lclscan.h" | |
42 | # include "lh.h" | |
43 | # include "imports.h" | |
44 | ||
45 | static lsymbol lsymbol_Bool; | |
46 | static lsymbol lsymbol_bool; | |
47 | static lsymbol lsymbol_TRUE; | |
48 | static lsymbol lsymbol_FALSE; | |
49 | ||
50 | static void lclPredicateNode_free (/*@only@*/ /*@null@*/ lclPredicateNode p_x) ; | |
51 | static void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode p_x) ; | |
52 | static void CTypesNode_free (/*@null@*/ /*@only@*/ CTypesNode p_x); | |
53 | static /*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode p_x) /*@*/ ; | |
54 | static void | |
55 | constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode p_x); | |
56 | static void claimNode_free (/*@only@*/ /*@null@*/ claimNode p_x); | |
57 | static void iterNode_free (/*@only@*/ /*@null@*/ iterNode p_x); | |
58 | static void abstBodyNode_free (/*@only@*/ /*@null@*/ abstBodyNode p_n); | |
59 | static void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode p_x); | |
60 | static void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode p_x); | |
61 | static void typeNode_free (/*@only@*/ /*@null@*/ typeNode p_t); | |
62 | static /*@null@*/ strOrUnionNode | |
63 | strOrUnionNode_copy (/*@null@*/ strOrUnionNode p_n) /*@*/ ; | |
64 | static void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode p_n) | |
65 | /*@modifies *p_n @*/ ; | |
66 | ||
67 | static void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode p_x); | |
68 | static /*@only@*/ /*@null@*/ enumSpecNode | |
69 | enumSpecNode_copy (/*@null@*/ enumSpecNode p_x) /*@*/ ; | |
70 | static /*@only@*/ lclTypeSpecNode | |
71 | lclTypeSpecNode_copySafe (lclTypeSpecNode p_n) /*@*/ ; | |
72 | static void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode p_n); | |
73 | static void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack p_x); | |
74 | static void opFormNode_free (/*@only@*/ /*@null@*/ opFormNode p_op); | |
75 | static quantifiedTermNode quantifiedTermNode_copy (quantifiedTermNode p_q) /*@*/ ; | |
76 | static void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode p_x); | |
77 | static void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode p_x); | |
78 | static void exportNode_free (/*@null@*/ /*@only@*/ exportNode p_x); | |
79 | static void privateNode_free (/*@only@*/ /*@null@*/ privateNode p_x); | |
80 | static /*@null@*/ termNode termNode_copy (/*@null@*/ termNode p_t) /*@*/ ; | |
81 | static void | |
82 | stmtNode_free (/*@only@*/ /*@null@*/ stmtNode p_x) /*@modifies *p_x@*/ ; | |
83 | static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr p_x) /*@*/ ; | |
84 | ||
85 | static lsymbol ConditionalSymbol; | |
86 | static lsymbol equalSymbol; | |
87 | static lsymbol eqSymbol; | |
88 | static lclTypeSpecNode exposedType; | |
89 | ||
90 | static /*@only@*/ cstring abstDeclaratorNode_unparse (abstDeclaratorNode p_x); | |
91 | static pairNodeList extractParams (/*@null@*/ typeExpr p_te); | |
92 | static sort extractReturnSort (lclTypeSpecNode p_t, declaratorNode p_d); | |
93 | static void checkAssociativity (termNode p_x, ltoken p_op); | |
94 | static void LCLBootstrap (void); | |
95 | static cstring printMiddle (int p_j); | |
96 | static void paramNode_checkQualifiers (lclTypeSpecNode p_t, typeExpr p_d); | |
97 | ||
98 | void | |
99 | resetImports (cstring current) | |
100 | { | |
101 | lsymbolSet_free (g_currentImports); | |
102 | ||
103 | g_currentImports = lsymbolSet_new (); /* equal_symbol; */ | |
104 | (void) lsymbolSet_insert (g_currentImports, | |
28bf4b0b | 105 | lsymbol_fromString (current)); |
616915dd | 106 | } |
107 | ||
108 | void | |
109 | abstract_init () | |
110 | { | |
111 | typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); | |
112 | nameNode nn; | |
113 | ltoken dom, range; | |
114 | sigNode sign; | |
115 | opFormNode opform; | |
116 | ltokenList domain = ltokenList_new (); | |
117 | ltokenList domain2; | |
118 | ||
119 | equalSymbol = lsymbol_fromChars ("="); | |
120 | eqSymbol = lsymbol_fromChars ("\\eq"); | |
121 | ||
122 | /* | |
123 | ** not: cstring_toCharsSafe (context_getBoolName ()) | |
124 | ** we use the hard wired "bool" name. | |
125 | */ | |
126 | ||
127 | lsymbol_bool = lsymbol_fromChars ("bool"); | |
128 | lsymbol_Bool = lsymbol_fromChars ("Bool"); | |
129 | ||
130 | lsymbol_TRUE = lsymbol_fromChars ("TRUE"); | |
131 | lsymbol_FALSE = lsymbol_fromChars ("FALSE"); | |
132 | ||
133 | ConditionalSymbol = lsymbol_fromChars ("if__then__else__"); | |
134 | ||
135 | /* generate operators for | |
136 | ** __ \not, __ \implies __ , __ \and __, __ \or __ | |
137 | */ | |
138 | ||
139 | range = ltoken_create (simpleId, lsymbol_bool); | |
140 | dom = ltoken_create (simpleId, lsymbol_bool); | |
141 | ||
142 | ltokenList_addh (domain, ltoken_copy (dom)); | |
143 | ||
144 | domain2 = ltokenList_copy (domain); /* moved this here (before release) */ | |
145 | ||
146 | sign = makesigNode (ltoken_undefined, domain, ltoken_copy (range)); | |
147 | ||
148 | opform = makeOpFormNode (ltoken_undefined, OPF_ANYOPM, | |
149 | opFormUnion_createAnyOp (ltoken_not), | |
150 | ltoken_undefined); | |
151 | nn = makeNameNodeForm (opform); | |
152 | symtable_enterOp (g_symtab, nn, sign); | |
153 | ||
154 | ltokenList_addh (domain2, dom); | |
155 | ||
156 | sign = makesigNode (ltoken_undefined, domain2, range); | |
157 | ||
158 | opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, | |
159 | opFormUnion_createAnyOp (ltoken_and), | |
160 | ltoken_undefined); | |
161 | ||
162 | nn = makeNameNodeForm (opform); | |
163 | symtable_enterOp (g_symtab, nn, sigNode_copy (sign)); | |
164 | ||
165 | opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, | |
166 | opFormUnion_createAnyOp (ltoken_or), | |
167 | ltoken_undefined); | |
168 | ||
169 | nn = makeNameNodeForm (opform); | |
170 | symtable_enterOp (g_symtab, nn, sigNode_copy (sign)); | |
171 | ||
172 | opform = makeOpFormNode (ltoken_undefined, OPF_MANYOPM, | |
173 | opFormUnion_createAnyOp (ltoken_implies), | |
174 | ltoken_undefined); | |
175 | nn = makeNameNodeForm (opform); | |
176 | symtable_enterOp (g_symtab, nn, sign); | |
177 | ||
178 | /* from lclscanline.c's init procedure */ | |
179 | /* comment out so we can add in lclinit.lci: synonym double float */ | |
180 | /* ReserveToken (FLOAT, "float"); */ | |
181 | /* But we need to make the scanner parse "float" not as a simpleId, but | |
182 | as a TYPEDEF_NAME. This is done later in abstract_init */ | |
183 | ||
184 | ti->id = ltoken_createType (LLT_TYPEDEF_NAME, SID_TYPE, lsymbol_fromChars ("float")); | |
185 | ||
186 | ti->modifiable = FALSE; | |
187 | ti->abstract = FALSE; | |
188 | ti->export = FALSE; /* this is implicit, not exported */ | |
2a6e9c30 | 189 | ti->basedOn = g_sortFloat; |
616915dd | 190 | symtable_enterType (g_symtab, ti); |
191 | } | |
192 | ||
193 | void | |
194 | declareForwardType (declaratorNode declare) | |
195 | { | |
196 | typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); | |
197 | sort tsort, handle; | |
198 | lsymbol typedefname; | |
199 | ||
200 | typedefname = ltoken_getText (declare->id); | |
201 | ti->id = ltoken_copy (declare->id); | |
202 | ||
203 | ltoken_setCode (ti->id, LLT_TYPEDEF_NAME); | |
204 | ltoken_setIdType (ti->id, SID_TYPE); | |
205 | ||
206 | ti->modifiable = FALSE; | |
207 | ti->abstract = FALSE; | |
208 | tsort = lclTypeSpecNode2sort (exposedType); | |
209 | handle = typeExpr2ptrSort (tsort, declare->type); | |
210 | ti->basedOn = sort_makeSyn (declare->id, handle, typedefname); | |
211 | ti->export = FALSE; | |
212 | ||
213 | symtable_enterType (g_symtab, ti); | |
214 | } | |
215 | ||
216 | void LCLBuiltins (void) | |
217 | { | |
218 | typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); | |
219 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
220 | ||
221 | /* immutable type bool; | |
222 | uses CTrait; | |
223 | constant bool FALSE = false; | |
224 | constant bool TRUE = true; */ | |
225 | ||
226 | /* the following defines the builtin LSL sorts and operators */ | |
227 | LCLBootstrap (); | |
228 | ||
229 | /* now LCL builtin proper */ | |
230 | /* do "immutable type bool;" */ | |
231 | ||
232 | ti->id = ltoken_copy (ltoken_bool); | |
233 | ||
234 | ltoken_setCode (ti->id, LLT_TYPEDEF_NAME); | |
235 | ltoken_setIdType (ti->id, SID_TYPE); | |
236 | ||
237 | ti->modifiable = FALSE; | |
238 | ti->abstract = TRUE; | |
2a6e9c30 | 239 | ti->basedOn = g_sortBool; |
1b8ae690 | 240 | ti->export = FALSE; /* this wasn't set (detected by Splint) */ |
616915dd | 241 | symtable_enterType (g_symtab, ti); |
242 | ||
243 | /* do "constant bool FALSE = false;" */ | |
244 | vi->id = ltoken_createType (simpleId, SID_VAR, lsymbol_fromChars ("FALSE")); | |
245 | ||
246 | vi->kind = VRK_CONST; | |
2a6e9c30 | 247 | vi->sort = g_sortBool; |
616915dd | 248 | vi->export = TRUE; |
249 | ||
250 | (void) symtable_enterVar (g_symtab, vi); | |
251 | ||
252 | /* do "constant bool TRUE = true;" */ | |
253 | /* vi->id = ltoken_copy (vi->id); */ | |
254 | ltoken_setText (vi->id, lsymbol_fromChars ("TRUE")); | |
255 | (void) symtable_enterVar (g_symtab, vi); | |
256 | ||
257 | varInfo_free (vi); | |
258 | ||
259 | importCTrait (); | |
260 | } | |
261 | ||
262 | static void | |
263 | LCLBootstrap (void) | |
264 | { | |
265 | nameNode nn1, nn2; | |
266 | ltoken range; | |
267 | sigNode sign; | |
268 | sort s; | |
269 | ||
270 | /* | |
271 | ** Minimal we need to bootstrap is to provide the sort | |
272 | ** "bool" and 2 bool constants "true" and "false". | |
273 | ** sort_init should already have been called, and hence | |
274 | ** the bool and Bool sorts defined. | |
275 | */ | |
276 | ||
277 | s = sort_makeImmutable (ltoken_undefined, lsymbol_bool); | |
278 | range = ltoken_create (simpleId, lsymbol_bool); | |
dfd82dce | 279 | sign = makesigNode (ltoken_undefined, ltokenList_new (), range); |
616915dd | 280 | |
281 | nn1 = (nameNode) dmalloc (sizeof (*nn1)); | |
282 | nn1->isOpId = TRUE; | |
283 | ||
284 | nn1->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("true")); | |
285 | ||
286 | symtable_enterOp (g_symtab, nn1, sign); | |
287 | ||
288 | nn2 = (nameNode) dmalloc (sizeof (*nn2)); | |
289 | nn2->isOpId = TRUE; | |
290 | nn2->content.opid = ltoken_create (simpleId, lsymbol_fromChars ("false")); | |
291 | ||
292 | symtable_enterOp (g_symtab, nn2, sigNode_copy (sign)); | |
293 | } | |
294 | ||
295 | interfaceNodeList | |
296 | consInterfaceNode (/*@only@*/ interfaceNode n, /*@returned@*/ interfaceNodeList ns) | |
297 | { | |
298 | /* n is never empty, but ns may be empty */ | |
299 | interfaceNodeList_addl (ns, n); | |
300 | return (ns); | |
301 | } | |
302 | ||
303 | /*@only@*/ interfaceNode | |
304 | makeInterfaceNodeImports (/*@only@*/ importNodeList x) | |
305 | { | |
306 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
307 | lsymbol importSymbol; | |
308 | ||
309 | i->kind = INF_IMPORTS; | |
310 | i->content.imports = x; /* an importNodeList */ | |
311 | ||
312 | importNodeList_elements (x, imp) | |
313 | { | |
314 | importSymbol = ltoken_getRawText (imp->val); | |
315 | ||
316 | if (lsymbolSet_member (g_currentImports, importSymbol)) | |
317 | { | |
318 | lclerror (imp->val, | |
319 | message ("Circular imports: %s", | |
320 | cstring_fromChars (lsymbol_toChars (importSymbol)))); | |
321 | } | |
322 | else | |
323 | { | |
324 | processImport (importSymbol, imp->val, imp->kind); | |
325 | } | |
326 | } end_importNodeList_elements; | |
327 | ||
328 | lhOutLine (cstring_undefined); | |
329 | return (i); | |
330 | } | |
331 | ||
332 | /*@only@*/ interfaceNode | |
333 | makeInterfaceNodeUses (/*@only@*/ traitRefNodeList x) | |
334 | { | |
335 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
336 | ||
337 | i->kind = INF_USES; | |
338 | i->content.uses = x; | |
339 | /* read in LSL traits */ | |
340 | ||
341 | return (i); | |
342 | } | |
343 | ||
344 | /*@only@*/ interfaceNode | |
345 | interfaceNode_makeConst (/*@only@*/ constDeclarationNode x) | |
346 | { | |
347 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
348 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
349 | ||
350 | e->kind = XPK_CONST; | |
351 | e->content.constdeclaration = x; | |
352 | i->kind = INF_EXPORT; | |
353 | i->content.export = e; | |
354 | ||
355 | return (i); | |
356 | } | |
357 | ||
358 | /*@only@*/ interfaceNode | |
359 | interfaceNode_makeVar (/*@only@*/ varDeclarationNode x) | |
360 | { | |
361 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
362 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
363 | ||
364 | e->kind = XPK_VAR; | |
365 | e->content.vardeclaration = x; | |
366 | i->kind = INF_EXPORT; | |
367 | i->content.export = e; | |
368 | ||
369 | if (context_msgLh ()) | |
370 | { | |
371 | lhOutLine (lhVarDecl (x->type, x->decls, x->qualifier)); | |
372 | } | |
373 | ||
374 | return (i); | |
375 | } | |
376 | ||
377 | /*@only@*/ interfaceNode | |
378 | interfaceNode_makeType (/*@only@*/ typeNode x) | |
379 | { | |
380 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
381 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
382 | e->kind = XPK_TYPE; | |
383 | e->content.type = x; | |
384 | i->kind = INF_EXPORT; | |
385 | i->content.export = e; | |
386 | ||
387 | if (context_msgLh ()) | |
388 | { | |
389 | ||
390 | lhOutLine (lhType (x)); | |
391 | } | |
392 | ||
393 | return (i); | |
394 | } | |
395 | ||
396 | /*@only@*/ interfaceNode | |
397 | interfaceNode_makeFcn (/*@only@*/ fcnNode x) | |
398 | { | |
399 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
400 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
401 | ||
402 | e->kind = XPK_FCN; | |
403 | e->content.fcn = x; | |
404 | i->kind = INF_EXPORT; | |
405 | i->content.export = e; | |
406 | ||
407 | if (context_msgLh ()) | |
408 | { | |
409 | llassert (x->typespec != NULL); | |
410 | llassert (x->declarator != NULL); | |
411 | ||
412 | lhOutLine (lhFunction (x->typespec, x->declarator)); | |
413 | } | |
414 | ||
415 | return (i); | |
416 | } | |
417 | ||
418 | /*@only@*/ interfaceNode | |
419 | interfaceNode_makeClaim (/*@only@*/ claimNode x) | |
420 | { | |
421 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
422 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
423 | ||
424 | e->kind = XPK_CLAIM; | |
425 | e->content.claim = x; | |
426 | i->kind = INF_EXPORT; | |
427 | i->content.export = e; | |
428 | return (i); | |
429 | } | |
430 | ||
431 | /*@only@*/ interfaceNode | |
432 | interfaceNode_makeIter (/*@only@*/ iterNode x) | |
433 | { | |
434 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
435 | exportNode e = (exportNode) dmalloc (sizeof (*e)); | |
436 | ||
437 | e->kind = XPK_ITER; | |
438 | e->content.iter = x; | |
439 | i->kind = INF_EXPORT; | |
440 | i->content.export = e; | |
441 | return (i); | |
442 | } | |
443 | ||
444 | /*@only@*/ interfaceNode | |
445 | interfaceNode_makePrivConst (/*@only@*/ constDeclarationNode x) | |
446 | { | |
447 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
448 | privateNode e = (privateNode) dmalloc (sizeof (*e)); | |
449 | ||
450 | e->kind = PRIV_CONST; | |
451 | e->content.constdeclaration = x; | |
452 | i->kind = INF_PRIVATE; | |
453 | i->content.private = e; | |
454 | return (i); | |
455 | } | |
456 | ||
457 | /*@only@*/ interfaceNode | |
458 | interfaceNode_makePrivVar (/*@only@*/ varDeclarationNode x) | |
459 | { | |
460 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
461 | privateNode e = (privateNode) dmalloc (sizeof (*e)); | |
462 | ||
463 | e->kind = PRIV_VAR; | |
464 | e->content.vardeclaration = x; | |
465 | i->kind = INF_PRIVATE; | |
466 | i->content.private = e; | |
467 | return (i); | |
468 | } | |
469 | ||
470 | /*@only@*/ interfaceNode | |
471 | interfaceNode_makePrivType (/*@only@*/ typeNode x) | |
472 | { | |
473 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
474 | privateNode e = (privateNode) dmalloc (sizeof (*e)); | |
475 | ||
476 | e->kind = PRIV_TYPE; | |
477 | e->content.type = x; | |
478 | i->kind = INF_PRIVATE; | |
479 | i->content.private = e; | |
480 | return (i); | |
481 | } | |
482 | ||
483 | /*@only@*/ interfaceNode | |
484 | interfaceNode_makePrivFcn (/*@only@*/ fcnNode x) | |
485 | { | |
486 | interfaceNode i = (interfaceNode) dmalloc (sizeof (*i)); | |
487 | privateNode e = (privateNode) dmalloc (sizeof (*e)); | |
488 | ||
489 | /* | |
1b8ae690 | 490 | ** bug detected by enum checking |
616915dd | 491 | ** e->kind = XPK_FCN; |
492 | */ | |
493 | ||
494 | e->kind = PRIV_FUNCTION; | |
495 | e->content.fcn = x; | |
496 | i->kind = INF_PRIVATE; | |
497 | i->content.private = e; | |
498 | return (i); | |
499 | } | |
500 | ||
501 | /*@only@*/ cstring | |
502 | exportNode_unparse (exportNode n) | |
503 | { | |
504 | if (n != (exportNode) 0) | |
505 | { | |
506 | switch (n->kind) | |
507 | { | |
508 | case XPK_CONST: | |
509 | return (message | |
510 | ("%q\n", | |
511 | constDeclarationNode_unparse (n->content.constdeclaration))); | |
512 | case XPK_VAR: | |
513 | return (message | |
514 | ("%q\n", | |
515 | varDeclarationNode_unparse (n->content.vardeclaration))); | |
516 | case XPK_TYPE: | |
517 | return (message ("%q\n", typeNode_unparse (n->content.type))); | |
518 | case XPK_FCN: | |
519 | return (fcnNode_unparse (n->content.fcn)); | |
520 | case XPK_CLAIM: | |
521 | return (claimNode_unparse (n->content.claim)); | |
522 | case XPK_ITER: | |
523 | return (iterNode_unparse (n->content.iter)); | |
524 | default: | |
525 | llfatalbug (message ("exportNode_unparse: unknown kind: %d", (int) n->kind)); | |
526 | } | |
527 | } | |
528 | return cstring_undefined; | |
529 | } | |
530 | ||
531 | /*@only@*/ cstring | |
532 | privateNode_unparse (privateNode n) | |
533 | { | |
534 | if (n != (privateNode) 0) | |
535 | { | |
536 | switch (n->kind) | |
537 | { | |
538 | case PRIV_CONST: | |
539 | return (constDeclarationNode_unparse (n->content.constdeclaration)); | |
540 | case PRIV_VAR: | |
541 | return (varDeclarationNode_unparse (n->content.vardeclaration)); | |
542 | case PRIV_TYPE: | |
543 | return (typeNode_unparse (n->content.type)); | |
544 | case PRIV_FUNCTION: | |
545 | return (fcnNode_unparse (n->content.fcn)); | |
546 | default: | |
547 | llfatalbug (message ("privateNode_unparse: unknown kind: %d", | |
548 | (int) n->kind)); | |
549 | } | |
550 | } | |
551 | return cstring_undefined; | |
552 | } | |
553 | ||
554 | void lclPredicateNode_free (/*@null@*/ /*@only@*/ lclPredicateNode x) | |
555 | { | |
556 | if (x != NULL) | |
557 | { | |
558 | termNode_free (x->predicate); | |
559 | ltoken_free (x->tok); | |
560 | sfree (x); | |
561 | } | |
562 | } | |
563 | ||
564 | static /*@only@*/ cstring | |
565 | lclPredicateNode_unparse (/*@null@*/ lclPredicateNode p) /*@*/ | |
566 | { | |
567 | if (p != (lclPredicateNode) 0) | |
568 | { | |
569 | cstring st = cstring_undefined; | |
570 | ||
571 | switch (p->kind) | |
572 | { | |
573 | case LPD_REQUIRES: | |
574 | st = cstring_makeLiteral (" requires "); | |
575 | break; | |
576 | case LPD_CHECKS: | |
577 | st = cstring_makeLiteral (" checks "); | |
578 | break; | |
579 | case LPD_ENSURES: | |
580 | st = cstring_makeLiteral (" ensures "); | |
581 | break; | |
582 | case LPD_INTRACLAIM: | |
583 | st = cstring_makeLiteral (" claims "); | |
584 | break; | |
585 | case LPD_CONSTRAINT: | |
586 | st = cstring_makeLiteral ("constraint "); | |
587 | break; | |
588 | case LPD_INITIALLY: | |
589 | st = cstring_makeLiteral ("initially "); | |
590 | break; | |
591 | case LPD_PLAIN: | |
592 | break; | |
593 | default: | |
594 | llfatalbug (message ("lclPredicateNode_unparse: unknown kind: %d", | |
595 | (int) p->kind)); | |
596 | } | |
597 | return (message ("%q%q;\n", st, termNode_unparse (p->predicate))); | |
598 | } | |
599 | return cstring_undefined; | |
600 | } | |
601 | ||
602 | bool | |
603 | ltoken_similar (ltoken t1, ltoken t2) | |
604 | { | |
605 | lsymbol sym1 = ltoken_getText (t1); | |
606 | lsymbol sym2 = ltoken_getText (t2); | |
607 | ||
608 | if (sym1 == sym2) | |
609 | { | |
610 | return TRUE; | |
611 | } | |
612 | ||
613 | if ((sym1 == eqSymbol && sym2 == equalSymbol) || | |
614 | (sym2 == eqSymbol && sym1 == equalSymbol)) | |
615 | { | |
616 | return TRUE; | |
617 | } | |
618 | ||
619 | if ((sym1 == lsymbol_bool && sym2 == lsymbol_Bool) || | |
620 | (sym2 == lsymbol_bool && sym1 == lsymbol_Bool)) | |
621 | { | |
622 | return TRUE; | |
623 | } | |
624 | ||
625 | return FALSE; | |
626 | } | |
627 | ||
628 | /*@only@*/ cstring | |
629 | iterNode_unparse (/*@null@*/ iterNode i) | |
630 | { | |
631 | if (i != (iterNode) 0) | |
632 | { | |
633 | return (message ("iter %s %q", ltoken_unparse (i->name), | |
634 | paramNodeList_unparse (i->params))); | |
635 | } | |
636 | return cstring_undefined; | |
637 | } | |
638 | ||
639 | ||
640 | /*@only@*/ cstring | |
641 | fcnNode_unparse (/*@null@*/ fcnNode f) | |
642 | { | |
643 | if (f != (fcnNode) 0) | |
644 | { | |
645 | return (message ("%q %q%q{\n%q%q%q%q%q%q}\n", | |
646 | lclTypeSpecNode_unparse (f->typespec), | |
647 | declaratorNode_unparse (f->declarator), | |
648 | varDeclarationNodeList_unparse (f->globals), | |
649 | varDeclarationNodeList_unparse (f->inits), | |
650 | letDeclNodeList_unparse (f->lets), | |
651 | lclPredicateNode_unparse (f->require), | |
652 | modifyNode_unparse (f->modify), | |
653 | lclPredicateNode_unparse (f->ensures), | |
654 | lclPredicateNode_unparse (f->claim))); | |
655 | } | |
656 | return cstring_undefined; | |
657 | } | |
658 | ||
659 | /*@only@*/ cstring | |
660 | varDeclarationNode_unparse (/*@null@*/ varDeclarationNode x) | |
661 | { | |
662 | if (x != (varDeclarationNode) 0) | |
663 | { | |
664 | cstring st; | |
665 | ||
666 | if (x->isSpecial) | |
667 | { | |
668 | return (sRef_unparse (x->sref)); | |
669 | } | |
670 | else | |
671 | { | |
672 | switch (x->qualifier) | |
673 | { | |
674 | case QLF_NONE: | |
675 | st = cstring_undefined; | |
676 | break; | |
677 | case QLF_CONST: | |
678 | st = cstring_makeLiteral ("const "); | |
679 | break; | |
680 | case QLF_VOLATILE: | |
681 | st = cstring_makeLiteral ("volatile "); | |
682 | break; | |
683 | BADDEFAULT; | |
684 | } | |
685 | ||
686 | st = message ("%q%q %q", st, lclTypeSpecNode_unparse (x->type), | |
687 | initDeclNodeList_unparse (x->decls)); | |
688 | return (st); | |
689 | } | |
690 | } | |
691 | ||
692 | return cstring_undefined; | |
693 | } | |
694 | ||
695 | /*@only@*/ cstring | |
696 | typeNode_unparse (/*@null@*/ typeNode t) | |
697 | { | |
698 | if (t != (typeNode) 0) | |
699 | { | |
700 | switch (t->kind) | |
701 | { | |
702 | case TK_ABSTRACT: | |
703 | return (abstractNode_unparse (t->content.abstract)); | |
704 | case TK_EXPOSED: | |
705 | return (exposedNode_unparse (t->content.exposed)); | |
706 | case TK_UNION: | |
707 | return (taggedUnionNode_unparse (t->content.taggedunion)); | |
708 | default: | |
709 | llfatalbug (message ("typeNode_unparse: unknown kind: %d", (int)t->kind)); | |
710 | } | |
711 | } | |
712 | return cstring_undefined; | |
713 | } | |
714 | ||
715 | /*@only@*/ cstring | |
716 | constDeclarationNode_unparse (/*@null@*/ constDeclarationNode x) | |
717 | { | |
718 | if (x != (constDeclarationNode) 0) | |
719 | { | |
720 | return (message ("constant %q %q", lclTypeSpecNode_unparse (x->type), | |
721 | initDeclNodeList_unparse (x->decls))); | |
722 | } | |
723 | ||
724 | return cstring_undefined; | |
725 | } | |
726 | ||
727 | /*@only@*/ storeRefNode | |
728 | makeStoreRefNodeTerm (/*@only@*/ termNode t) | |
729 | { | |
730 | storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); | |
731 | ||
732 | x->kind = SRN_TERM; | |
733 | x->content.term = t; | |
734 | return (x); | |
735 | } | |
736 | ||
737 | /*@only@*/ storeRefNode | |
738 | makeStoreRefNodeType (/*@only@*/ lclTypeSpecNode t, bool isObj) | |
739 | { | |
740 | storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); | |
741 | ||
742 | x->kind = isObj ? SRN_OBJ : SRN_TYPE; | |
743 | x->content.type = t; | |
744 | return (x); | |
745 | } | |
746 | ||
747 | storeRefNode | |
748 | makeStoreRefNodeInternal (void) | |
749 | { | |
750 | storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); | |
751 | ||
752 | x->kind = SRN_SPECIAL; | |
753 | x->content.ref = sRef_makeInternalState (); | |
754 | return (x); | |
755 | } | |
756 | ||
757 | storeRefNode | |
758 | makeStoreRefNodeSystem (void) | |
759 | { | |
760 | storeRefNode x = (storeRefNode) dmalloc (sizeof (*x)); | |
761 | ||
762 | x->kind = SRN_SPECIAL; | |
763 | x->content.ref = sRef_makeSystemState (); | |
764 | return (x); | |
765 | } | |
766 | ||
767 | /*@only@*/ modifyNode | |
768 | makeModifyNodeSpecial (/*@only@*/ ltoken t, bool modifiesNothing) | |
769 | { | |
770 | modifyNode x = (modifyNode) dmalloc (sizeof (*x)); | |
771 | ||
772 | x->tok = t; | |
773 | x->modifiesNothing = modifiesNothing; | |
774 | x->hasStoreRefList = FALSE; | |
775 | return (x); | |
776 | } | |
777 | ||
778 | /*@only@*/ modifyNode | |
779 | makeModifyNodeRef (/*@only@*/ ltoken t, /*@only@*/ storeRefNodeList y) | |
780 | { | |
781 | modifyNode x = (modifyNode) dmalloc (sizeof (*x)); | |
782 | sort sort; | |
783 | ||
784 | x->tok = t; | |
785 | x->hasStoreRefList = TRUE; | |
786 | x->modifiesNothing = FALSE; | |
787 | x->list = y; | |
788 | /* check that all storeRef's are modifiable */ | |
789 | ||
790 | storeRefNodeList_elements (y, sr) | |
791 | { | |
792 | if (storeRefNode_isTerm (sr)) | |
793 | { | |
794 | sort = sr->content.term->sort; | |
795 | ||
796 | if (!sort_mutable (sort) && sort_isValidSort (sort)) | |
797 | { | |
798 | ltoken errtok = termNode_errorToken (sr->content.term); | |
799 | lclerror (errtok, | |
800 | message ("Term denoting immutable object used in modifies list: %q", | |
801 | termNode_unparse (sr->content.term))); | |
802 | } | |
803 | } | |
804 | else | |
805 | { | |
806 | if (!storeRefNode_isSpecial (sr)) | |
807 | { | |
808 | sort = lclTypeSpecNode2sort (sr->content.type); | |
809 | ||
810 | if (storeRefNode_isObj (sr)) | |
811 | { | |
812 | sort = sort_makeObj (sort); | |
813 | } | |
814 | ||
815 | if (!sort_mutable (sort)) | |
816 | { | |
817 | ltoken errtok = lclTypeSpecNode_errorToken (sr->content.type); | |
818 | lclerror (errtok, | |
819 | message ("Immutable type used in modifies list: %q", | |
820 | sort_unparse (sort))); | |
821 | } | |
822 | } | |
823 | } | |
824 | } end_storeRefNodeList_elements; | |
825 | return (x); | |
826 | } | |
827 | ||
828 | /*@observer@*/ ltoken | |
829 | termNode_errorToken (/*@null@*/ termNode n) | |
830 | { | |
831 | if (n != (termNode) 0) | |
832 | { | |
833 | switch (n->kind) | |
834 | { | |
835 | case TRM_LITERAL: | |
836 | case TRM_UNCHANGEDALL: | |
837 | case TRM_UNCHANGEDOTHERS: | |
838 | case TRM_SIZEOF: | |
839 | case TRM_CONST: | |
840 | case TRM_VAR: | |
841 | case TRM_ZEROARY: /* also the default kind, when no in symbol table */ | |
842 | return n->literal; | |
843 | case TRM_QUANTIFIER: | |
844 | return n->quantified->open; | |
845 | case TRM_APPLICATION: | |
846 | if (n->name != NULL) | |
847 | { | |
848 | if (n->name->isOpId) | |
849 | { | |
850 | return n->name->content.opid; | |
851 | } | |
852 | else | |
853 | { | |
854 | llassert (n->name->content.opform != NULL); | |
855 | return n->name->content.opform->tok; | |
856 | } | |
857 | } | |
858 | else | |
859 | { | |
860 | return ltoken_undefined; | |
861 | } | |
862 | } | |
863 | } | |
864 | return ltoken_undefined; | |
865 | } | |
866 | ||
867 | /*@observer@*/ ltoken | |
868 | nameNode_errorToken (/*@null@*/ nameNode nn) | |
869 | { | |
870 | if (nn != (nameNode) 0) | |
871 | { | |
872 | if (nn->isOpId) | |
873 | { | |
874 | return nn->content.opid; | |
875 | } | |
876 | else | |
877 | { | |
878 | if (nn->content.opform != NULL) | |
879 | { | |
880 | return nn->content.opform->tok; | |
881 | } | |
882 | } | |
883 | } | |
884 | ||
885 | return ltoken_undefined; | |
886 | } | |
887 | ||
888 | /*@observer@*/ ltoken | |
889 | lclTypeSpecNode_errorToken (/*@null@*/ lclTypeSpecNode t) | |
890 | { | |
891 | if (t != (lclTypeSpecNode) 0) | |
892 | { | |
893 | switch (t->kind) | |
894 | { | |
895 | case LTS_TYPE: | |
896 | { | |
897 | llassert (t->content.type != NULL); | |
898 | ||
899 | if (ltokenList_empty (t->content.type->ctypes)) | |
900 | break; | |
901 | else | |
902 | return (ltokenList_head (t->content.type->ctypes)); | |
903 | } | |
904 | case LTS_STRUCTUNION: | |
905 | llassert (t->content.structorunion != NULL); | |
906 | return t->content.structorunion->tok; | |
907 | case LTS_ENUM: | |
908 | llassert (t->content.enumspec != NULL); | |
909 | return t->content.enumspec->tok; | |
910 | case LTS_CONJ: | |
911 | return (lclTypeSpecNode_errorToken (t->content.conj->a)); | |
912 | } | |
913 | } | |
914 | ||
915 | return ltoken_undefined; | |
916 | } | |
917 | ||
918 | static bool | |
919 | sort_member_modulo_cstring (sort s, /*@null@*/ termNode t) | |
920 | { | |
921 | ||
922 | if (t != (termNode) 0) | |
923 | { | |
924 | if (t->kind == TRM_LITERAL) | |
925 | { /* allow multiple types */ | |
926 | sortNode sn; | |
927 | ||
928 | sortSet_elements (t->possibleSorts, el) | |
929 | { | |
930 | if (sort_compatible_modulo_cstring (s, el)) | |
931 | { | |
932 | return TRUE; | |
933 | } | |
934 | } end_sortSet_elements; | |
935 | ||
936 | sn = sort_lookup (s); | |
937 | ||
28bf4b0b | 938 | if (sn->kind == SRT_PTR) |
616915dd | 939 | { |
940 | char *lit = lsymbol_toChars (ltoken_getText (t->literal)); | |
941 | ||
942 | if (lit != NULL) | |
943 | { | |
944 | long val = 0; | |
945 | ||
946 | if (sscanf (lit, "%ld", &val) == 1) | |
947 | { | |
948 | if (val == 0) return TRUE; | |
949 | } | |
950 | } | |
951 | } | |
952 | ||
953 | return FALSE; | |
954 | } | |
955 | else | |
956 | { | |
957 | return sort_compatible_modulo_cstring (s, t->sort); | |
958 | } | |
959 | } | |
960 | return FALSE; | |
961 | } | |
962 | ||
963 | /*@only@*/ letDeclNode | |
964 | makeLetDeclNode (ltoken varid, /*@only@*/ /*@null@*/ lclTypeSpecNode t, | |
965 | /*@only@*/ termNode term) | |
966 | { | |
967 | letDeclNode x = (letDeclNode) dmalloc (sizeof (*x)); | |
968 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
969 | ltoken errtok; | |
970 | sort s, termsort; | |
971 | ||
972 | if (t != (lclTypeSpecNode) 0) | |
973 | { | |
974 | /* check varid has the same sort as term */ | |
975 | s = lclTypeSpecNode2sort (t); | |
976 | termsort = term->sort; | |
977 | /* should keep the arguments in order */ | |
978 | if (!sort_member_modulo_cstring (s, term) && | |
979 | !term->error_reported) | |
980 | { | |
981 | errtok = termNode_errorToken (term); | |
982 | ||
28bf4b0b | 983 | /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */ |
616915dd | 984 | /* sprintf (ERRMSG, "expect `%s' type but given term has `%s' type", |
985 | sort_unparse (s), sort_unparse (termsort)); */ | |
986 | ||
987 | lclerror (errtok, | |
988 | message ("Let declaration expects type %q", sort_unparse (s))); | |
989 | /* evs --- don't know how to generated this message or what it means? */ | |
990 | } | |
991 | } | |
992 | else | |
993 | { | |
994 | s = term->sort; | |
995 | } | |
996 | /* assign variable its type and sort, store in symbol table */ | |
997 | vi->id = ltoken_copy (varid); | |
998 | vi->kind = VRK_LET; | |
999 | vi->sort = s; | |
1000 | vi->export = TRUE; | |
1001 | ||
1002 | (void) symtable_enterVar (g_symtab, vi); | |
1003 | varInfo_free (vi); | |
1004 | ||
1005 | x->varid = varid; | |
1006 | x->sortspec = t; | |
1007 | x->term = term; | |
1008 | x->sort = sort_makeNoSort (); | |
1009 | ||
1010 | return (x); | |
1011 | } | |
1012 | ||
1013 | /*@only@*/ programNode | |
1014 | makeProgramNodeAction (/*@only@*/ programNodeList x, actionKind k) | |
1015 | { | |
1016 | programNode n = (programNode) dmalloc (sizeof (*n)); | |
1017 | n->wrapped = 0; | |
1018 | n->kind = k; | |
1019 | n->content.args = x; | |
1020 | return (n); | |
1021 | } | |
1022 | ||
1023 | /*@only@*/ programNode | |
1024 | makeProgramNode (/*@only@*/ stmtNode x) | |
1025 | { | |
1026 | programNode n = (programNode) dmalloc (sizeof (*n)); | |
1027 | ||
1028 | n->wrapped = 0; | |
1029 | n->kind = ACT_SELF; | |
1030 | n->content.self = x; | |
1031 | return (n); | |
1032 | } | |
1033 | ||
1034 | /*@only@*/ typeNode | |
1035 | makeAbstractTypeNode (/*@only@*/ abstractNode x) | |
1036 | { | |
1037 | typeNode n = (typeNode) dmalloc (sizeof (*n)); | |
1038 | ||
1039 | n->kind = TK_ABSTRACT; | |
1040 | n->content.abstract = x; | |
1041 | ||
1042 | return (n); | |
1043 | } | |
1044 | ||
1045 | /*@only@*/ typeNode | |
1046 | makeExposedTypeNode (/*@only@*/ exposedNode x) | |
1047 | { | |
1048 | typeNode n = (typeNode) dmalloc (sizeof (*n)); | |
1049 | ||
1050 | n->kind = TK_EXPOSED; | |
1051 | n->content.exposed = x; | |
1052 | return (n); | |
1053 | } | |
1054 | ||
1055 | /* | |
1056 | ** evs added 8 Sept 1993 | |
1057 | */ | |
1058 | ||
1059 | /*@only@*/ importNode | |
1060 | importNode_makePlain (/*@only@*/ ltoken t) | |
1061 | { | |
1062 | importNode imp = (importNode) dmalloc (sizeof (*imp)); | |
1063 | ||
1064 | imp->kind = IMPPLAIN; | |
1065 | imp->val = t; | |
1066 | return (imp); | |
1067 | } | |
1068 | ||
1069 | /*@only@*/ importNode | |
1070 | importNode_makeBracketed (/*@only@*/ ltoken t) | |
1071 | { | |
1072 | importNode imp = (importNode) dmalloc (sizeof (*imp)); | |
1073 | ||
1074 | imp->kind = IMPBRACKET; | |
1075 | imp->val = t; | |
1076 | return (imp); | |
1077 | } | |
1078 | ||
1079 | static cstring extractQuote (/*@only@*/ cstring s) | |
1080 | { | |
abd7f895 | 1081 | size_t len = cstring_length (s); |
616915dd | 1082 | char *sc = cstring_toCharsSafe (s); |
1083 | cstring t; | |
1084 | ||
1085 | llassert (len > 1); | |
1086 | *(sc + len - 1) = '\0'; | |
1087 | t = cstring_fromChars (mstring_copy (sc + 1)); | |
1088 | cstring_free (s); | |
1089 | return (t); | |
1090 | } | |
1091 | ||
1092 | /*@only@*/ importNode | |
1093 | importNode_makeQuoted (/*@only@*/ ltoken t) | |
1094 | { | |
1095 | importNode imp = (importNode) dmalloc (sizeof (*imp)); | |
1096 | cstring q = extractQuote (cstring_copy (ltoken_getRawString (t))); | |
1097 | ||
1098 | imp->kind = IMPQUOTE; | |
1099 | ||
28bf4b0b | 1100 | ltoken_setRawText (t, lsymbol_fromString (q)); |
616915dd | 1101 | |
1102 | imp->val = t; | |
1103 | ||
1104 | cstring_free (q); | |
1105 | return (imp); | |
1106 | } | |
1107 | ||
1108 | /* | |
1109 | ** check that is it '<' and '>' | |
1110 | ** should probably be in a different file? | |
1111 | */ | |
1112 | ||
1113 | static void cylerror (/*@only@*/ char *s) | |
1114 | { | |
1115 | ylerror(s); | |
1116 | sfree (s); | |
1117 | } | |
1118 | ||
1119 | void | |
1120 | checkBrackets (ltoken lb, ltoken rb) | |
1121 | { | |
1122 | /* no attempt at error recovery...not really necessary */ | |
1123 | cstring tname; | |
1124 | ||
1125 | tname = ltoken_getRawString (lb); | |
1126 | ||
1127 | if (!cstring_equalLit (tname, "<")) | |
1128 | { | |
1129 | cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname))); | |
1130 | } | |
1131 | ||
1132 | tname = ltoken_getRawString (rb); | |
1133 | ||
1134 | if (!cstring_equalLit (tname, ">")) | |
1135 | { | |
1136 | cylerror (cstring_toCharsSafeO (message ("Invalid import token: %s", tname))); | |
1137 | } | |
1138 | } | |
1139 | ||
1140 | /*@only@*/ traitRefNode | |
1141 | makeTraitRefNode (/*@only@*/ ltokenList fl, /*@only@*/ renamingNode r) | |
1142 | { | |
1143 | traitRefNode n = (traitRefNode) dmalloc (sizeof (*n)); | |
1144 | ||
1145 | n->traitid = fl; | |
1146 | n->rename = r; | |
1147 | return (n); | |
1148 | } | |
1149 | ||
1150 | /* | |
1151 | ** printLeaves: no commas | |
1152 | */ | |
1153 | ||
1154 | static /*@only@*/ cstring | |
1155 | printLeaves (ltokenList f) | |
1156 | { | |
1157 | bool firstone = TRUE; | |
1158 | cstring s = cstring_undefined; | |
1159 | ||
1160 | ltokenList_elements (f, i) | |
1161 | { | |
1162 | if (firstone) | |
1163 | { | |
1164 | s = cstring_copy (ltoken_unparse (i)); | |
1165 | firstone = FALSE; | |
1166 | } | |
1167 | else | |
1168 | { | |
1169 | s = message ("%q %s", s, ltoken_unparse (i)); | |
1170 | } | |
1171 | } end_ltokenList_elements; | |
1172 | ||
1173 | return s; | |
1174 | } | |
1175 | ||
1176 | ||
1177 | /*@only@*/ cstring | |
1178 | printLeaves2 (ltokenList f) | |
1179 | { | |
1180 | return (ltokenList_unparse (f)); | |
1181 | } | |
1182 | ||
1183 | /*@only@*/ cstring | |
1184 | printRawLeaves2 (ltokenList f) | |
1185 | { | |
1186 | bool first = TRUE; | |
1187 | cstring s = cstring_undefined; | |
1188 | ||
1189 | ltokenList_elements (f, i) | |
1190 | { | |
1191 | if (first) | |
1192 | { | |
1193 | s = message ("%s", ltoken_getRawString (i)); | |
1194 | first = FALSE; | |
1195 | } | |
1196 | else | |
1197 | s = message ("%q, %s", s, ltoken_getRawString (i)); | |
1198 | } end_ltokenList_elements; | |
1199 | ||
1200 | return s; | |
1201 | } | |
1202 | ||
1203 | /*@only@*/ renamingNode | |
1204 | makeRenamingNode (/*@only@*/ typeNameNodeList n, /*@only@*/ replaceNodeList r) | |
1205 | { | |
1206 | renamingNode ren = (renamingNode) dmalloc (sizeof (*ren)); | |
1207 | ||
1208 | if (typeNameNodeList_empty (n)) | |
1209 | { | |
1210 | ren->is_replace = TRUE; | |
1211 | ren->content.replace = r; | |
1212 | typeNameNodeList_free (n); | |
1213 | } | |
1214 | else | |
1215 | { | |
1216 | nameAndReplaceNode nr = (nameAndReplaceNode) dmalloc (sizeof (*nr)); | |
1217 | nr->replacelist = r; | |
1218 | nr->namelist = n; | |
1219 | ren->is_replace = FALSE; | |
1220 | ren->content.name = nr; | |
1221 | } | |
1222 | ||
1223 | return (ren); | |
1224 | } | |
1225 | ||
1226 | /*@only@*/ cstring | |
1227 | renamingNode_unparse (/*@null@*/ renamingNode x) | |
1228 | { | |
1229 | if (x != (renamingNode) 0) | |
1230 | { | |
1231 | if (x->is_replace) | |
1232 | { | |
1233 | return (replaceNodeList_unparse (x->content.replace)); | |
1234 | } | |
1235 | else | |
1236 | { | |
1237 | return (message ("%q%q", typeNameNodeList_unparse (x->content.name->namelist), | |
1238 | replaceNodeList_unparse (x->content.name->replacelist))); | |
1239 | } | |
1240 | } | |
1241 | return cstring_undefined; | |
1242 | } | |
1243 | ||
1244 | /*@only@*/ replaceNode | |
1245 | makeReplaceNameNode (ltoken t, typeNameNode tn, nameNode nn) | |
1246 | { | |
1247 | replaceNode r = (replaceNode) dmalloc (sizeof (*r)); | |
1248 | ||
1249 | r->tok = t; | |
1250 | r->isCType = FALSE; | |
1251 | r->typename = tn; | |
1252 | r->content.renamesortname.name = nn; | |
28bf4b0b | 1253 | r->content.renamesortname.signature = (sigNode) NULL; |
616915dd | 1254 | |
1255 | return (r); | |
1256 | } | |
1257 | ||
1258 | /*@only@*/ replaceNode | |
1259 | makeReplaceNode (ltoken t, typeNameNode tn, | |
1260 | bool is_ctype, ltoken ct, | |
1261 | nameNode nn, sigNode sn) | |
1262 | { | |
1263 | replaceNode r = (replaceNode) dmalloc (sizeof (*r)); | |
1264 | ||
1265 | r->tok = t; | |
1266 | r->isCType = is_ctype; | |
1267 | r->typename = tn; | |
1268 | ||
1269 | if (is_ctype) | |
1270 | { | |
1271 | r->content.ctype = ct; | |
1272 | sigNode_free (sn); | |
1273 | nameNode_free (nn); | |
1274 | } | |
1275 | else | |
1276 | { | |
1277 | r->content.renamesortname.name = nn; | |
1278 | r->content.renamesortname.signature = sn; | |
1279 | ltoken_free (ct); | |
1280 | } | |
1281 | ||
1282 | return (r); | |
1283 | } | |
1284 | ||
1285 | /*@only@*/ cstring | |
1286 | replaceNode_unparse (/*@null@*/ replaceNode x) | |
1287 | { | |
1288 | if (x != (replaceNode) 0) | |
1289 | { | |
1290 | cstring st; | |
1291 | ||
1292 | st = message ("%q for ", typeNameNode_unparse (x->typename)); | |
1293 | ||
1294 | if (x->isCType) | |
1295 | { | |
1296 | st = message ("%q%s", st, ltoken_getRawString (x->content.ctype)); | |
1297 | } | |
1298 | else | |
1299 | { | |
1300 | st = message ("%q%q%q", st, nameNode_unparse (x->content.renamesortname.name), | |
1301 | sigNode_unparse (x->content.renamesortname.signature)); | |
1302 | } | |
1303 | return st; | |
1304 | } | |
1305 | return cstring_undefined; | |
1306 | } | |
1307 | ||
1308 | /*@only@*/ nameNode | |
1309 | makeNameNodeForm (/*@only@*/ /*@null@*/ opFormNode opform) | |
1310 | { | |
1311 | nameNode nn = (nameNode) dmalloc (sizeof (*nn)); | |
1312 | ||
1313 | nn->isOpId = FALSE; | |
1314 | nn->content.opform = opform; | |
1315 | ||
1316 | return (nn); | |
1317 | } | |
1318 | ||
1319 | /*@only@*/ nameNode | |
1320 | makeNameNodeId (/*@only@*/ ltoken opid) | |
1321 | { | |
1322 | nameNode nn = (nameNode) dmalloc (sizeof (*nn)); | |
1323 | ||
1324 | /* | |
1325 | ** current LSL -syms output bug produces "if_then_else_" rather | |
1326 | ** than 6 separate tokens | |
1327 | */ | |
1328 | ||
1329 | if (ltoken_getText (opid) == ConditionalSymbol) | |
1330 | { | |
1331 | opFormNode opform = makeOpFormNode (ltoken_undefined, OPF_IF, | |
1332 | opFormUnion_createMiddle (0), | |
1333 | ltoken_undefined); | |
1334 | nn->isOpId = FALSE; | |
1335 | nn->content.opform = opform; | |
1336 | ltoken_free (opid); | |
1337 | } | |
1338 | else | |
1339 | { | |
1340 | nn->isOpId = TRUE; | |
1341 | nn->content.opid = opid; | |
1342 | } | |
1343 | ||
1344 | return (nn); | |
1345 | } | |
1346 | ||
1347 | /*@only@*/ cstring | |
1348 | nameNode_unparse (/*@null@*/ nameNode n) | |
1349 | { | |
1350 | if (n != (nameNode) 0) | |
1351 | { | |
1352 | if (n->isOpId) | |
1353 | { | |
1354 | return (cstring_copy (ltoken_getRawString (n->content.opid))); /*!!!*/ | |
1355 | } | |
1356 | else | |
1357 | { | |
1358 | return (opFormNode_unparse (n->content.opform)); | |
1359 | } | |
1360 | } | |
1361 | return cstring_undefined; | |
1362 | } | |
1363 | ||
1364 | /*@only@*/ sigNode | |
1365 | makesigNode (ltoken t, /*@only@*/ ltokenList domain, ltoken range) | |
1366 | { | |
1367 | sigNode s = (sigNode) dmalloc (sizeof (*s)); | |
e5081f8c | 1368 | unsigned long int key; |
616915dd | 1369 | |
1370 | /* | |
1371 | ** Assign a hash key here to speed up lookup of operators. | |
1372 | */ | |
1373 | ||
1374 | s->tok = t; | |
1375 | s->domain = domain; | |
1376 | s->range = range; | |
1377 | key = MASH (0, ltoken_getText (range)); | |
1378 | ||
1379 | ltokenList_elements (domain, id) | |
1380 | { | |
1381 | lsymbol sym = ltoken_getText (id); | |
1382 | key = MASH (key, sym); | |
1383 | } end_ltokenList_elements; | |
1384 | ||
1385 | s->key = key; | |
e5081f8c | 1386 | return (s); |
616915dd | 1387 | } |
1388 | ||
1389 | cstring sigNode_unparse (/*@null@*/ sigNode n) | |
1390 | { | |
1391 | if (n != (sigNode) 0) | |
1392 | { | |
1393 | return (message (":%q -> %s", printLeaves2 (n->domain), | |
1394 | ltoken_unparse (n->range))); | |
1395 | } | |
1396 | ||
1397 | return cstring_undefined; | |
1398 | } | |
1399 | ||
1400 | void sigNode_markOwned (sigNode n) | |
1401 | { | |
1402 | sfreeEventually (n); | |
1403 | } | |
1404 | ||
1405 | /*@only@*/ cstring | |
1406 | sigNode_unparseText (/*@null@*/ sigNode n) | |
1407 | { | |
1408 | if (n != (sigNode) 0) | |
1409 | { | |
1410 | return (message ("%q -> %s", printLeaves2 (n->domain), | |
1411 | ltoken_unparse (n->range))); | |
1412 | } | |
1413 | return cstring_undefined; | |
1414 | } | |
1415 | ||
e5081f8c | 1416 | static unsigned long opFormNode2key (opFormNode op, opFormKind k) |
616915dd | 1417 | { |
e5081f8c | 1418 | unsigned long int key; |
616915dd | 1419 | |
1420 | switch (k) | |
1421 | { | |
1422 | case OPF_IF: | |
1423 | /* OPF_IF is the first enum, so it's 0 */ | |
1424 | ||
1425 | /*@-type@*/ | |
1426 | key = MASH (k, k + 1); | |
1427 | /*@=type@*/ | |
1428 | ||
1429 | break; | |
1430 | case OPF_ANYOP: | |
1431 | case OPF_MANYOP: | |
1432 | case OPF_ANYOPM: | |
1433 | case OPF_MANYOPM: | |
1434 | { /* treat eq and = the same */ | |
1435 | lsymbol sym = ltoken_getText (op->content.anyop); | |
1436 | ||
1437 | if (sym == equalSymbol) | |
1438 | { | |
1439 | key = MASH (k, eqSymbol); | |
1440 | } | |
1441 | else | |
1442 | { | |
1443 | key = MASH (k, ltoken_getText (op->content.anyop)); | |
1444 | } | |
1445 | break; | |
1446 | } | |
1447 | case OPF_MIDDLE: | |
1448 | case OPF_MMIDDLE: | |
1449 | case OPF_MIDDLEM: | |
1450 | case OPF_MMIDDLEM: | |
1451 | case OPF_BMIDDLE: | |
1452 | case OPF_BMMIDDLE: | |
1453 | case OPF_BMIDDLEM: | |
1454 | case OPF_BMMIDDLEM: | |
1455 | key = MASH (k, op->content.middle); | |
1456 | key = MASH (key, ltoken_getRawText (op->tok)); | |
1457 | break; | |
1458 | case OPF_SELECT: | |
1459 | case OPF_MAP: | |
1460 | case OPF_MSELECT: | |
1461 | case OPF_MMAP: | |
1462 | key = MASH (k, ltoken_getRawText (op->content.id)); | |
1463 | break; | |
1464 | default: | |
1465 | key = 0; | |
1466 | } | |
1467 | ||
1468 | return key; | |
1469 | } | |
1470 | ||
1471 | /*@only@*/ opFormNode | |
1472 | makeOpFormNode (ltoken t, opFormKind k, opFormUnion u, | |
1473 | ltoken close) | |
1474 | { | |
1475 | opFormNode n = (opFormNode) dmalloc (sizeof (*n)); | |
e5081f8c | 1476 | unsigned long int key = 0; |
616915dd | 1477 | |
1478 | /* | |
1479 | ** Assign a hash key here to speed up lookup of operators. | |
1480 | */ | |
1481 | ||
1482 | n->tok = t; | |
1483 | n->close = close; | |
1484 | n->kind = k; | |
616915dd | 1485 | |
1486 | switch (k) | |
1487 | { | |
1488 | case OPF_IF: | |
1489 | n->content.middle = 0; | |
1490 | /* OPF_IF is the first enum, so it's 0 */ | |
1491 | key = MASH /*@+enumint@*/ (k, k + 1) /*@=enumint@*/; | |
1492 | break; | |
1493 | case OPF_ANYOP: | |
1494 | case OPF_MANYOP: | |
1495 | case OPF_ANYOPM: | |
1496 | case OPF_MANYOPM: | |
1497 | { /* treat eq and = the same */ | |
1498 | lsymbol sym = ltoken_getText (u.anyop); | |
1499 | ||
1500 | if (sym == equalSymbol) | |
1501 | { | |
1502 | key = MASH (k, eqSymbol); | |
1503 | } | |
1504 | else | |
1505 | { | |
1506 | key = MASH (k, ltoken_getText (u.anyop)); | |
1507 | } | |
1508 | ||
1509 | n->content = u; | |
1510 | break; | |
1511 | } | |
1512 | case OPF_MIDDLE: | |
1513 | case OPF_MMIDDLE: | |
1514 | case OPF_MIDDLEM: | |
1515 | case OPF_MMIDDLEM: | |
1516 | case OPF_BMIDDLE: | |
1517 | case OPF_BMMIDDLE: | |
1518 | case OPF_BMIDDLEM: | |
1519 | case OPF_BMMIDDLEM: | |
1520 | n->content = u; | |
1521 | key = MASH (k, u.middle); | |
1522 | key = MASH (key, ltoken_getRawText (t)); | |
1523 | break; | |
1524 | case OPF_SELECT: | |
1525 | case OPF_MAP: | |
1526 | case OPF_MSELECT: | |
1527 | case OPF_MMAP: | |
1528 | key = MASH (k, ltoken_getRawText (u.id)); | |
1529 | n->content = u; | |
1530 | break; | |
1531 | default: | |
1532 | { | |
1533 | llbug (message ("makeOpFormNode: unknown opFormKind: %d", (int) k)); | |
1534 | } | |
1535 | } | |
1536 | n->key = key; | |
e5081f8c | 1537 | return (n); |
616915dd | 1538 | } |
1539 | ||
1540 | static cstring printMiddle (int j) | |
1541 | { | |
1542 | int i; | |
1543 | char *s = mstring_createEmpty (); | |
1544 | ||
1545 | for (i = j; i >= 1; i--) | |
1546 | { | |
1547 | s = mstring_concatFree1 (s, "__"); | |
1548 | ||
1549 | if (i != 1) | |
1550 | { | |
1551 | s = mstring_concatFree1 (s, ", "); | |
1552 | } | |
1553 | } | |
1554 | ||
1555 | return cstring_fromCharsO (s); | |
1556 | } | |
1557 | ||
1558 | /*@only@*/ cstring | |
1559 | opFormNode_unparse (/*@null@*/ opFormNode n) | |
1560 | { | |
1561 | if (n != (opFormNode) 0) | |
1562 | { | |
1563 | switch (n->kind) | |
1564 | { | |
1565 | case OPF_IF: | |
1566 | return (cstring_makeLiteral ("if __ then __ else __ ")); | |
1567 | case OPF_ANYOP: | |
1568 | return (cstring_copy (ltoken_getRawString (n->content.anyop))); | |
1569 | case OPF_MANYOP: | |
1570 | return (message ("__ %s", ltoken_getRawString (n->content.anyop))); | |
1571 | case OPF_ANYOPM: | |
1572 | return (message ("%s __ ", ltoken_getRawString (n->content.anyop))); | |
1573 | case OPF_MANYOPM: | |
1574 | return (message ("__ %s __ ", ltoken_getRawString (n->content.anyop))); | |
1575 | case OPF_MIDDLE: | |
1576 | return (message ("%s %q %s", | |
1577 | ltoken_getRawString (n->tok), | |
1578 | printMiddle (n->content.middle), | |
1579 | ltoken_getRawString (n->close))); | |
1580 | case OPF_MMIDDLE: | |
1581 | return (message ("__ %s %q %s", | |
1582 | ltoken_getRawString (n->tok), | |
1583 | printMiddle (n->content.middle), | |
1584 | ltoken_getRawString (n->close))); | |
1585 | case OPF_MIDDLEM: | |
1586 | return (message ("%s %q %s __", | |
1587 | ltoken_getRawString (n->tok), | |
1588 | printMiddle (n->content.middle), | |
1589 | ltoken_getRawString (n->close))); | |
1590 | case OPF_MMIDDLEM: | |
1591 | return (message ("__ %s%q %s __", | |
1592 | ltoken_getRawString (n->tok), | |
1593 | printMiddle (n->content.middle), | |
1594 | ltoken_getRawString (n->close))); | |
1595 | case OPF_BMIDDLE: | |
1596 | return (message ("[%q]", printMiddle (n->content.middle))); | |
1597 | case OPF_BMMIDDLE: | |
1598 | return (message ("__ [%q]", printMiddle (n->content.middle))); | |
1599 | case OPF_BMIDDLEM: | |
1600 | return (message ("[%q] __", printMiddle (n->content.middle))); | |
1601 | case OPF_BMMIDDLEM: | |
1602 | return (message ("__ [%q] __", printMiddle (n->content.middle))); | |
1603 | case OPF_SELECT: | |
1604 | return (message (" \\select %s", ltoken_getRawString (n->content.id))); | |
1605 | case OPF_MAP: | |
1606 | return (message (" \\field_arrow%s", ltoken_getRawString (n->content.id))); | |
1607 | case OPF_MSELECT: | |
1608 | return (message ("__ \\select %s", ltoken_getRawString (n->content.id))); | |
1609 | case OPF_MMAP: | |
1610 | return (message ("__ \\field_arrow %s", ltoken_getRawString (n->content.id))); | |
1611 | default: | |
1612 | llfatalbug (message ("opFormNodeUnparse: unknown kind: %d", | |
1613 | (int) n->kind)); | |
1614 | } | |
1615 | } | |
1616 | return cstring_undefined; | |
1617 | } | |
1618 | ||
1619 | /*@only@*/ typeNameNode | |
1620 | makeTypeNameNode (bool isObj, lclTypeSpecNode t, abstDeclaratorNode n) | |
1621 | { | |
1622 | typeNameNode tn = (typeNameNode) dmalloc (sizeof (*tn)); | |
1623 | typeNamePack p = (typeNamePack) dmalloc (sizeof (*p)); | |
1624 | ||
1625 | tn->isTypeName = TRUE; | |
1626 | p->isObj = isObj; | |
1627 | p->type = t; | |
1628 | p->abst = n; | |
1629 | tn->opform = (opFormNode) 0; | |
1630 | tn->typename = p; | |
1631 | return (tn); | |
1632 | } | |
1633 | ||
1634 | /*@only@*/ typeNameNode | |
1635 | makeTypeNameNodeOp (opFormNode n) | |
1636 | { | |
1637 | typeNameNode t = (typeNameNode) dmalloc (sizeof (*t)); | |
1638 | t->typename = (typeNamePack) 0; | |
1639 | t->opform = n; | |
1640 | t->isTypeName = FALSE; | |
1641 | return (t); | |
1642 | } | |
1643 | ||
1644 | /*@only@*/ cstring | |
1645 | typeNameNode_unparse (/*@null@*/ typeNameNode n) | |
1646 | { | |
1647 | if (n != (typeNameNode) 0) | |
1648 | { | |
1649 | if (n->isTypeName) | |
1650 | { | |
1651 | cstring st = cstring_undefined; | |
1652 | typeNamePack p = n->typename; | |
1653 | ||
1654 | llassert (p != NULL); | |
1655 | ||
1656 | if (p->isObj) | |
1657 | st = cstring_makeLiteral ("obj "); | |
1658 | ||
1659 | return (message ("%q%q%q", st, lclTypeSpecNode_unparse (p->type), | |
1660 | abstDeclaratorNode_unparse (p->abst))); | |
1661 | ||
1662 | } | |
1663 | else | |
1664 | return (opFormNode_unparse (n->opform)); | |
1665 | } | |
1666 | return cstring_undefined; | |
1667 | } | |
1668 | ||
1669 | /*@only@*/ lclTypeSpecNode | |
1670 | makeLclTypeSpecNodeConj (/*@null@*/ lclTypeSpecNode a, /*@null@*/ lclTypeSpecNode b) | |
1671 | { | |
1672 | lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); | |
1673 | ||
1674 | n->kind = LTS_CONJ; | |
f9264521 | 1675 | n->pointers = pointers_undefined; |
616915dd | 1676 | n->quals = qualList_new (); |
1677 | n->content.conj = (lclconj) dmalloc (sizeof (*n->content.conj)); | |
1678 | n->content.conj->a = a; | |
1679 | n->content.conj->b = b; | |
1680 | ||
1681 | return (n); | |
1682 | } | |
1683 | ||
1684 | /*@only@*/ lclTypeSpecNode | |
1685 | makeLclTypeSpecNodeType (/*@null@*/ CTypesNode x) | |
1686 | { | |
1687 | lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); | |
1688 | ||
1689 | n->kind = LTS_TYPE; | |
f9264521 | 1690 | n->pointers = pointers_undefined; |
616915dd | 1691 | n->content.type = x; |
1692 | n->quals = qualList_new (); | |
1693 | return (n); | |
1694 | } | |
1695 | ||
1696 | /*@only@*/ lclTypeSpecNode | |
1697 | makeLclTypeSpecNodeSU (/*@null@*/ strOrUnionNode x) | |
1698 | { | |
1699 | lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); | |
1700 | ||
1701 | n->kind = LTS_STRUCTUNION; | |
f9264521 | 1702 | n->pointers = pointers_undefined; |
616915dd | 1703 | n->content.structorunion = x; |
1704 | n->quals = qualList_new (); | |
1705 | return (n); | |
1706 | } | |
1707 | ||
1708 | /*@only@*/ lclTypeSpecNode | |
1709 | makeLclTypeSpecNodeEnum (/*@null@*/ enumSpecNode x) | |
1710 | { | |
1711 | lclTypeSpecNode n = (lclTypeSpecNode) dmalloc (sizeof (*n)); | |
1712 | ||
1713 | n->quals = qualList_new (); | |
1714 | n->kind = LTS_ENUM; | |
f9264521 | 1715 | n->pointers = pointers_undefined; |
616915dd | 1716 | n->content.enumspec = x; |
1717 | return (n); | |
1718 | } | |
1719 | ||
1720 | lclTypeSpecNode | |
1721 | lclTypeSpecNode_addQual (lclTypeSpecNode n, qual q) | |
1722 | { | |
1723 | llassert (lclTypeSpecNode_isDefined (n)); | |
1724 | n->quals = qualList_add (n->quals, q); | |
1725 | return n; | |
1726 | } | |
1727 | ||
1728 | /*@only@*/ cstring | |
1729 | lclTypeSpecNode_unparse (/*@null@*/ lclTypeSpecNode n) | |
1730 | { | |
1731 | if (n != (lclTypeSpecNode) 0) | |
1732 | { | |
1733 | switch (n->kind) | |
1734 | { | |
1735 | case LTS_TYPE: | |
1736 | llassert (n->content.type != NULL); | |
1737 | return (printLeaves (n->content.type->ctypes)); | |
1738 | case LTS_STRUCTUNION: | |
1739 | return (strOrUnionNode_unparse (n->content.structorunion)); | |
1740 | case LTS_ENUM: | |
1741 | return (enumSpecNode_unparse (n->content.enumspec)); | |
1742 | case LTS_CONJ: | |
1743 | return (lclTypeSpecNode_unparse (n->content.conj->a)); | |
1744 | default: | |
1745 | llfatalbug (message ("lclTypeSpecNode_unparse: unknown lclTypeSpec kind: %d", | |
1746 | (int) n->kind)); | |
1747 | } | |
1748 | } | |
1749 | return cstring_undefined; | |
1750 | } | |
1751 | ||
1752 | /*@only@*/ enumSpecNode | |
1753 | makeEnumSpecNode (ltoken t, ltoken optTagId, | |
1754 | /*@owned@*/ ltokenList enums) | |
1755 | { | |
1756 | enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n)); | |
1757 | tagInfo ti; | |
1758 | smemberInfo *top = smemberInfo_undefined; | |
1759 | ||
1760 | n->tok = t; | |
1761 | n->opttagid = ltoken_copy (optTagId); | |
1762 | n->enums = enums; | |
1763 | ||
1764 | /* generate sort for this LCL type */ | |
1765 | n->sort = sort_makeEnum (optTagId); | |
1766 | ||
1767 | if (!ltoken_isUndefined (optTagId)) | |
1768 | { | |
1769 | /* First, check to see if tag is already defined */ | |
1770 | ti = symtable_tagInfo (g_symtab, ltoken_getText (optTagId)); | |
1771 | ||
1772 | if (tagInfo_exists (ti)) | |
1773 | { | |
1774 | if (ti->kind == TAG_ENUM) | |
1775 | { | |
1776 | /* 23 Sep 1995 --- had been noting here...is this right? */ | |
1777 | ||
1778 | ti->content.enums = enums; | |
1779 | ti->sort = n->sort; | |
1780 | ti->imported = context_inImport (); | |
1781 | } | |
1782 | else | |
1783 | { | |
1784 | lclerror (optTagId, | |
1785 | message ("Tag %s previously defined as %q, redefined as enum", | |
1786 | ltoken_getRawString (optTagId), | |
1787 | tagKind_unparse (ti->kind))); | |
1788 | ||
1789 | /* evs --- shouldn't they be in different name spaces? */ | |
1790 | } | |
1791 | ||
1792 | ltoken_free (optTagId); | |
1793 | } | |
1794 | else | |
1795 | { | |
1796 | ti = (tagInfo) dmalloc (sizeof (*ti)); | |
1797 | ||
1798 | ti->kind = TAG_ENUM; | |
1799 | ti->id = optTagId; | |
1800 | ti->content.enums = enums; | |
1801 | ti->sort = n->sort; | |
1802 | ti->imported = context_inImport (); | |
1803 | /* First, store tag info in symbol table */ | |
1804 | (void) symtable_enterTag (g_symtab, ti); | |
1805 | } | |
1806 | } | |
1807 | ||
1808 | /* check that enumeration constants are unique */ | |
1809 | ||
1810 | ltokenList_reset (enums); | |
1811 | ||
1812 | while (!ltokenList_isFinished (enums)) | |
1813 | { | |
1814 | ltoken c = ltokenList_current (enums); | |
1815 | smemberInfo *ei = (smemberInfo *) dmalloc (sizeof (*ei)); | |
1816 | ||
1817 | ei->name = ltoken_getText (c); | |
1818 | ei->next = top; | |
1819 | ei->sort = n->sort; | |
1820 | top = ei; | |
1821 | ||
1822 | if (!varInfo_exists (symtable_varInfo (g_symtab, ltoken_getText (c)))) | |
1823 | { /* put info into symbol table */ | |
1824 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
1825 | ||
1826 | vi->id = ltoken_copy (c); | |
1827 | vi->kind = VRK_ENUM; | |
1828 | vi->sort = n->sort; | |
1829 | vi->export = TRUE; | |
1830 | ||
1831 | (void) symtable_enterVar (g_symtab, vi); | |
1832 | varInfo_free (vi); | |
1833 | } | |
1834 | else | |
1835 | { | |
1836 | lclerror (c, message ("Enumerated value redeclared: %s", | |
1837 | ltoken_getRawString (c))); | |
1838 | ltokenList_removeCurrent (enums); | |
1839 | } | |
1840 | ltokenList_advance (enums); | |
1841 | /*@-branchstate@*/ | |
1842 | } | |
1843 | /*@=branchstate@*/ | |
1844 | ||
1845 | (void) sort_updateEnum (n->sort, top); | |
1846 | return (n); | |
1847 | } | |
1848 | ||
1849 | /*@only@*/ enumSpecNode | |
1850 | makeEnumSpecNode2 (ltoken t, ltoken tagid) | |
1851 | { | |
1852 | /* a reference, not a definition */ | |
1853 | enumSpecNode n = (enumSpecNode) dmalloc (sizeof (*n)); | |
1854 | tagInfo ti = symtable_tagInfo (g_symtab, ltoken_getText (tagid)); | |
1855 | ||
1856 | n->tok = t; | |
1857 | n->opttagid = tagid; | |
1858 | n->enums = ltokenList_new (); | |
1859 | ||
1860 | if (tagInfo_exists (ti)) | |
1861 | { | |
1862 | if (ti->kind == TAG_ENUM) | |
1863 | { | |
1864 | n->sort = ti->sort; | |
1865 | } | |
1866 | else | |
1867 | { | |
1868 | n->sort = sort_makeNoSort (); | |
1869 | lclerror (tagid, message ("Tag %s defined as %q, used as enum", | |
1870 | ltoken_getRawString (tagid), | |
1871 | tagKind_unparse (ti->kind))); | |
1872 | } | |
1873 | } | |
1874 | else | |
1875 | { | |
1876 | n->sort = sort_makeNoSort (); | |
1877 | lclerror (t, message ("Undefined type: enum %s", | |
1878 | ltoken_getRawString (tagid))); | |
1879 | } | |
1880 | ||
1881 | return (n); | |
1882 | } | |
1883 | ||
1884 | /*@only@*/ cstring | |
1885 | enumSpecNode_unparse (/*@null@*/ enumSpecNode n) | |
1886 | { | |
1887 | if (n != (enumSpecNode) 0) | |
1888 | { | |
1889 | cstring s = cstring_makeLiteral ("enum "); | |
1890 | ||
1891 | if (!ltoken_isUndefined (n->opttagid)) | |
1892 | { | |
1893 | s = message ("%q%s ", s, ltoken_getRawString (n->opttagid)); | |
1894 | } | |
1895 | ||
1896 | s = message ("%q{%q}", s, printLeaves2 (n->enums)); | |
1897 | return s; | |
1898 | } | |
1899 | return cstring_undefined; | |
1900 | } | |
1901 | ||
1902 | /*@only@*/ strOrUnionNode | |
1903 | makestrOrUnionNode (ltoken str, suKind k, ltoken opttagid, | |
1904 | /*@only@*/ stDeclNodeList x) | |
1905 | { | |
1906 | strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n)); | |
1907 | lsymbolSet set = lsymbolSet_new (); | |
1908 | declaratorNodeList declarators; | |
1909 | sort fieldsort, tsort1, tsort2; | |
1910 | smemberInfo *mi, *top = smemberInfo_undefined; | |
1911 | bool doTag = FALSE; | |
1912 | bool isStruct = (k == SU_STRUCT); | |
1913 | tagInfo t; | |
1914 | ||
1915 | ||
1916 | n->kind = k; | |
1917 | n->tok = str; | |
1918 | n->opttagid = ltoken_copy (opttagid); | |
1919 | n->structdecls = x; | |
1920 | n->sort = isStruct ? sort_makeStr (opttagid) : sort_makeUnion (opttagid); | |
1921 | ||
1922 | if (!ltoken_isUndefined (opttagid)) | |
1923 | { | |
1924 | /* First, check to see if tag is already defined */ | |
1925 | t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid)); | |
1926 | ||
1927 | if (tagInfo_exists (t)) | |
1928 | { | |
1929 | if ((t->kind == TAG_FWDUNION && k == SU_UNION) || | |
1930 | (t->kind == TAG_FWDSTRUCT && k == SU_STRUCT)) | |
1931 | { | |
1932 | /* to allow self-recursive types and forward tag declarations */ | |
1933 | t->content.decls = stDeclNodeList_copy (x); /* update tag info */ | |
1934 | t->sort = n->sort; | |
1935 | } | |
1936 | else | |
1937 | { | |
1938 | lclerror (opttagid, | |
1939 | message ("Tag %s previously defined as %q, used as %q", | |
1940 | ltoken_getRawString (opttagid), | |
1941 | tagKind_unparse (t->kind), | |
1942 | cstring_makeLiteral (isStruct ? "struct" : "union"))); | |
1943 | } | |
1944 | } | |
1945 | else | |
1946 | { | |
1947 | doTag = TRUE; | |
1948 | } | |
1949 | } | |
1950 | else | |
1951 | { | |
1952 | doTag = TRUE; | |
1953 | } | |
1954 | ||
1955 | if (doTag && !ltoken_isUndefined (opttagid)) | |
1956 | { | |
1957 | t = (tagInfo) dmalloc (sizeof (*t)); | |
1958 | ||
1959 | /* can either override prev defn or use prev defn */ | |
1960 | /* override it so as to detect more errors */ | |
1961 | ||
1962 | t->kind = (k == SU_STRUCT) ? TAG_STRUCT : TAG_UNION; | |
1963 | t->id = opttagid; | |
1964 | t->content.decls = stDeclNodeList_copy (x); | |
1965 | t->sort = n->sort; | |
1966 | t->imported = FALSE; | |
1967 | ||
1968 | /* Next, update tag info in symbol table */ | |
1969 | (void) symtable_enterTagForce (g_symtab, t); | |
1970 | } | |
1971 | ||
1972 | /* check no duplicate field names */ | |
1973 | ||
1974 | stDeclNodeList_elements (x, i) | |
1975 | { | |
1976 | fieldsort = lclTypeSpecNode2sort (i->lcltypespec); | |
1977 | ||
1978 | /* need the locations, not values */ | |
1979 | /* fieldsort = sort_makeObj (fieldsort); */ | |
1980 | /* 2/19/93, was | |
1981 | fieldsort = sort_makeGlobal (fieldsort); */ | |
1982 | ||
1983 | declarators = i->declarators; | |
1984 | ||
1985 | declaratorNodeList_elements (declarators, decl) | |
1986 | { | |
1987 | lsymbol fieldname; | |
1988 | mi = (smemberInfo *) dmalloc (sizeof (*mi)); | |
1989 | /* need to make dynamic copies */ | |
1990 | fieldname = ltoken_getText (decl->id); | |
1991 | ||
1992 | /* 2/19/93, added */ | |
1993 | tsort1 = typeExpr2ptrSort (fieldsort, decl->type); | |
1994 | tsort2 = sort_makeGlobal (tsort1); | |
1995 | ||
1996 | mi->name = fieldname; | |
1997 | mi->sort = tsort2; /* fieldsort; */ | |
1998 | mi->next = top; | |
1999 | top = mi; | |
2000 | ||
2001 | if (lsymbolSet_member (set, fieldname)) | |
2002 | { | |
2003 | lclerror (decl->id, | |
2004 | message ("Field name reused: %s", | |
2005 | ltoken_getRawString (decl->id))); | |
2006 | } | |
2007 | else | |
2008 | { | |
2009 | (void) lsymbolSet_insert (set, fieldname); | |
2010 | } | |
2011 | /*@-branchstate@*/ | |
2012 | } end_declaratorNodeList_elements; | |
2013 | /*@=branchstate@*/ | |
2014 | } end_stDeclNodeList_elements; | |
2015 | ||
2016 | if (k == SU_STRUCT) | |
2017 | { | |
2018 | (void) sort_updateStr (n->sort, top); | |
2019 | } | |
2020 | else | |
2021 | { | |
2022 | (void) sort_updateUnion (n->sort, top); | |
2023 | } | |
2024 | ||
2025 | /* We shall keep the info with both tags and types if any | |
2026 | of them are present. */ | |
2027 | ||
2028 | lsymbolSet_free (set); | |
2029 | ||
2030 | return (n); | |
2031 | } | |
2032 | ||
2033 | /*@only@*/ strOrUnionNode | |
2034 | makeForwardstrOrUnionNode (ltoken str, suKind k, | |
2035 | ltoken tagid) | |
2036 | { | |
2037 | strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n)); | |
2038 | sort sort = sort_makeNoSort (); | |
2039 | tagInfo t; | |
2040 | ||
2041 | /* a reference, not a definition */ | |
2042 | ||
2043 | n->kind = k; | |
2044 | n->tok = str; | |
2045 | n->opttagid = tagid; | |
2046 | n->structdecls = stDeclNodeList_new (); | |
2047 | ||
2048 | /* get sort for this LCL type */ | |
2049 | t = symtable_tagInfo (g_symtab, ltoken_getText (tagid)); | |
2050 | ||
2051 | if (tagInfo_exists (t)) | |
2052 | { | |
2053 | sort = t->sort; | |
2054 | ||
2055 | if (!(((t->kind == TAG_STRUCT || t->kind == TAG_FWDSTRUCT) && k == SU_STRUCT) | |
2056 | || ((t->kind == TAG_UNION || t->kind == TAG_FWDUNION) && k == SU_UNION))) | |
2057 | { | |
2058 | lclerror (tagid, | |
2059 | message ("Tag %s previously defined as %q, used as %q", | |
2060 | ltoken_getRawString (tagid), | |
2061 | tagKind_unparse (t->kind), | |
2062 | cstring_makeLiteral ((k == SU_STRUCT) ? "struct" : "union"))); | |
2063 | } | |
2064 | } | |
2065 | else | |
2066 | { | |
2067 | /* | |
2068 | ** changed from error: 31 Mar 1994 | |
2069 | ** | |
2070 | ** lclerror (str, message ("Undefined type: %s %s", s, ltoken_getRawString (tagid)); | |
2071 | ** | |
2072 | */ | |
2073 | ||
2074 | /* forward struct's and union's are ok... */ | |
2075 | ||
2076 | if (k == SU_STRUCT) | |
2077 | { | |
2078 | (void) checkAndEnterTag (TAG_FWDSTRUCT, ltoken_copy (tagid)); | |
2079 | lhForwardStruct (tagid); | |
2080 | sort = sort_makeStr (tagid); | |
2081 | } | |
2082 | else | |
2083 | { | |
2084 | (void) checkAndEnterTag (TAG_FWDUNION, ltoken_copy (tagid)); | |
2085 | lhForwardUnion (tagid); | |
2086 | sort = sort_makeUnion (tagid); | |
2087 | } | |
2088 | } | |
2089 | ||
2090 | n->sort = sort; | |
2091 | return (n); | |
2092 | } | |
2093 | ||
2094 | /*@only@*/ cstring | |
2095 | strOrUnionNode_unparse (/*@null@*/ strOrUnionNode n) | |
2096 | { | |
2097 | if (n != (strOrUnionNode) 0) | |
2098 | { | |
2099 | cstring s; | |
2100 | switch (n->kind) | |
2101 | { | |
2102 | case SU_STRUCT: | |
2103 | s = cstring_makeLiteral ("struct "); | |
2104 | break; | |
2105 | case SU_UNION: | |
2106 | s = cstring_makeLiteral ("union "); | |
2107 | break; | |
2108 | BADDEFAULT | |
2109 | } | |
2110 | ||
2111 | if (!ltoken_isUndefined (n->opttagid)) | |
2112 | { | |
2113 | s = message ("%q%s ", s, ltoken_getRawString (n->opttagid)); | |
2114 | } | |
2115 | s = message ("%q{%q}", s, stDeclNodeList_unparse (n->structdecls)); | |
2116 | return s; | |
2117 | } | |
2118 | return cstring_undefined; | |
2119 | } | |
2120 | ||
2121 | /*@only@*/ stDeclNode | |
2122 | makestDeclNode (lclTypeSpecNode s, | |
2123 | declaratorNodeList x) | |
2124 | { | |
2125 | stDeclNode n = (stDeclNode) dmalloc (sizeof (*n)); | |
2126 | ||
2127 | n->lcltypespec = s; | |
2128 | n->declarators = x; | |
2129 | return n; | |
2130 | } | |
2131 | ||
2132 | /*@only@*/ typeExpr | |
2133 | makeFunctionNode (typeExpr x, paramNodeList p) | |
2134 | { | |
2135 | typeExpr y = (typeExpr) dmalloc (sizeof (*y)); | |
2136 | ||
2137 | y->wrapped = 0; | |
2138 | y->kind = TEXPR_FCN; | |
2139 | y->content.function.returntype = x; | |
2140 | y->content.function.args = p; | |
2141 | y->sort = sort_makeNoSort (); | |
2142 | ||
2143 | return (y); | |
2144 | } | |
2145 | ||
2146 | static /*@observer@*/ ltoken | |
2147 | extractDeclarator (/*@null@*/ typeExpr t) | |
2148 | { | |
2149 | if (t != (typeExpr) 0) | |
2150 | { | |
2151 | switch (t->kind) | |
2152 | { | |
2153 | case TEXPR_BASE: | |
2154 | return t->content.base; | |
2155 | case TEXPR_PTR: | |
2156 | return (extractDeclarator (t->content.pointer)); | |
2157 | case TEXPR_ARRAY: | |
2158 | return (extractDeclarator (t->content.array.elementtype)); | |
2159 | case TEXPR_FCN: | |
2160 | return (extractDeclarator (t->content.function.returntype)); | |
2161 | } | |
2162 | } | |
2163 | ||
2164 | return ltoken_undefined; | |
2165 | } | |
2166 | ||
2167 | /*@only@*/ typeExpr | |
2168 | makeTypeExpr (ltoken t) | |
2169 | { | |
2170 | typeExpr x = (typeExpr) dmalloc (sizeof (*x)); | |
2171 | ||
2172 | ||
2173 | x->wrapped = 0; | |
2174 | x->kind = TEXPR_BASE; | |
2175 | x->content.base = t; | |
2176 | x->sort = sort_makeNoSort (); | |
2177 | ||
2178 | return (x); | |
2179 | } | |
2180 | ||
2181 | ||
2182 | /*@only@*/ declaratorNode | |
2183 | makeDeclaratorNode (typeExpr t) | |
2184 | { | |
2185 | declaratorNode x = (declaratorNode) dmalloc (sizeof (*x)); | |
2186 | ||
2187 | x->id = ltoken_copy (extractDeclarator (t)); | |
2188 | x->type = t; | |
2189 | x->isRedecl = FALSE; | |
2190 | ||
2191 | return (x); | |
2192 | } | |
2193 | ||
2194 | static /*@only@*/ declaratorNode | |
2195 | makeUnknownDeclaratorNode (/*@only@*/ ltoken t) | |
2196 | { | |
2197 | declaratorNode x = (declaratorNode) dmalloc (sizeof (*x)); | |
2198 | ||
2199 | x->id = t; | |
2200 | x->type = (typeExpr) 0; | |
2201 | x->isRedecl = FALSE; | |
2202 | ||
2203 | return (x); | |
2204 | } | |
2205 | ||
2206 | static /*@only@*/ cstring | |
2207 | printTypeExpr2 (/*@null@*/ typeExpr x) | |
2208 | { | |
2209 | paramNodeList params; | |
2210 | ||
2211 | if (x != (typeExpr) 0) | |
2212 | { | |
2213 | cstring s; /* print out types in reverse order */ | |
2214 | ||
2215 | switch (x->kind) | |
2216 | { | |
2217 | case TEXPR_BASE: | |
2218 | return (message ("%s ", ltoken_getRawString (x->content.base))); | |
2219 | case TEXPR_PTR: | |
2220 | return (message ("%qptr to ", printTypeExpr2 (x->content.pointer))); | |
2221 | case TEXPR_ARRAY: | |
2222 | return (message ("array[%q] of %q", | |
2223 | termNode_unparse (x->content.array.size), | |
2224 | printTypeExpr2 (x->content.array.elementtype))); | |
2225 | case TEXPR_FCN: | |
2226 | s = printTypeExpr2 (x->content.function.returntype); | |
2227 | params = x->content.function.args; | |
2228 | if (!paramNodeList_empty (params)) | |
2229 | { | |
2230 | s = message ("%qfcn with args: (%q)", s, | |
2231 | paramNodeList_unparse (x->content.function.args)); | |
2232 | } | |
2233 | else | |
2234 | s = message ("%qfcn with no args", s); | |
2235 | return s; | |
2236 | default: | |
2237 | llfatalbug (message ("printTypeExpr2: unknown typeExprKind: %d", (int) x->kind)); | |
2238 | } | |
2239 | } | |
2240 | return cstring_undefined; | |
2241 | } | |
2242 | ||
2243 | /*@only@*/ cstring | |
2244 | declaratorNode_unparse (declaratorNode x) | |
2245 | { | |
2246 | return (typeExpr_unparse (x->type)); | |
2247 | } | |
2248 | ||
2249 | /*@only@*/ declaratorNode | |
2250 | declaratorNode_copy (declaratorNode x) | |
2251 | { | |
2252 | declaratorNode ret = (declaratorNode) dmalloc (sizeof (*ret)); | |
2253 | ||
2254 | ret->type = typeExpr_copy (x->type); | |
2255 | ret->id = ltoken_copy (x->id); | |
2256 | ret->isRedecl = x->isRedecl; | |
2257 | ||
2258 | return (ret); | |
2259 | } | |
2260 | ||
2261 | static /*@null@*/ typeExpr typeExpr_copy (/*@null@*/ typeExpr x) | |
2262 | { | |
2263 | if (x == NULL) | |
2264 | { | |
2265 | return NULL; | |
2266 | } | |
2267 | else | |
2268 | { | |
2269 | typeExpr ret = (typeExpr) dmalloc (sizeof (*ret)); | |
2270 | ||
2271 | ret->wrapped = x->wrapped; | |
2272 | ret->kind = x->kind; | |
2273 | ||
2274 | switch (ret->kind) | |
2275 | { | |
2276 | case TEXPR_BASE: | |
2277 | ret->content.base = ltoken_copy (x->content.base); | |
2278 | break; | |
2279 | case TEXPR_PTR: | |
2280 | ret->content.pointer = typeExpr_copy (x->content.pointer); | |
2281 | break; | |
2282 | case TEXPR_ARRAY: | |
2283 | ret->content.array.elementtype = typeExpr_copy (x->content.array.elementtype); | |
2284 | ret->content.array.size = termNode_copy (x->content.array.size); | |
2285 | break; | |
2286 | case TEXPR_FCN: | |
2287 | ret->content.function.returntype = typeExpr_copy (x->content.function.returntype); | |
2288 | ret->content.function.args = paramNodeList_copy (x->content.function.args); | |
2289 | break; | |
2290 | } | |
2291 | ||
2292 | ret->sort = x->sort; | |
2293 | return ret; | |
2294 | } | |
2295 | } | |
2296 | ||
2297 | static /*@only@*/ cstring | |
2298 | typeExpr_unparseCode (/*@null@*/ typeExpr x) | |
2299 | { | |
2300 | /* print out types in order of appearance in source */ | |
2301 | cstring s = cstring_undefined; | |
2302 | ||
2303 | if (x != (typeExpr) 0) | |
2304 | { | |
2305 | switch (x->kind) | |
2306 | { | |
2307 | case TEXPR_BASE: | |
2308 | return (cstring_copy (ltoken_getRawString (x->content.base))); | |
2309 | case TEXPR_PTR: | |
2310 | return (typeExpr_unparseCode (x->content.pointer)); | |
2311 | case TEXPR_ARRAY: | |
2312 | return (typeExpr_unparseCode (x->content.array.elementtype)); | |
2313 | case TEXPR_FCN: | |
2314 | return (typeExpr_unparseCode (x->content.function.returntype)); | |
2315 | } | |
2316 | } | |
2317 | return s; | |
2318 | } | |
2319 | ||
2320 | void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x) | |
2321 | { | |
2322 | if (x != (typeExpr) 0) | |
2323 | { | |
2324 | switch (x->kind) | |
2325 | { | |
2326 | case TEXPR_BASE: | |
2327 | break; | |
2328 | case TEXPR_PTR: | |
2329 | typeExpr_free (x->content.pointer); | |
2330 | break; | |
2331 | case TEXPR_ARRAY: | |
2332 | typeExpr_free (x->content.array.elementtype); | |
2333 | termNode_free (x->content.array.size); | |
2334 | break; | |
2335 | case TEXPR_FCN: | |
2336 | typeExpr_free (x->content.function.returntype); | |
2337 | paramNodeList_free (x->content.function.args); | |
2338 | break; | |
2339 | /*@-branchstate@*/ | |
2340 | } | |
2341 | /*@=branchstate@*/ | |
2342 | ||
2343 | sfree (x); | |
2344 | } | |
2345 | } | |
2346 | ||
2347 | ||
2348 | /*@only@*/ cstring | |
2349 | declaratorNode_unparseCode (declaratorNode x) | |
2350 | { | |
2351 | return (typeExpr_unparseCode (x->type)); | |
2352 | } | |
2353 | ||
2354 | /*@only@*/ cstring | |
2355 | typeExpr_unparse (/*@null@*/ typeExpr x) | |
2356 | { | |
2357 | cstring s = cstring_undefined; /* print out types in order of appearance in source */ | |
2358 | paramNodeList params; | |
2359 | int i; | |
2360 | ||
2361 | if (x != (typeExpr) 0) | |
2362 | { | |
2363 | cstring front = cstring_undefined; | |
2364 | cstring back = cstring_undefined; | |
2365 | ||
2366 | llassert (x->wrapped < 100); | |
2367 | ||
2368 | for (i = x->wrapped; i >= 1; i--) | |
2369 | { | |
2370 | front = cstring_appendChar (front, '('); | |
2371 | back = cstring_appendChar (back, ')'); | |
2372 | } | |
2373 | ||
2374 | switch (x->kind) | |
2375 | { | |
2376 | case TEXPR_BASE: | |
2377 | s = message ("%q%s", s, ltoken_getRawString (x->content.base)); | |
2378 | break; | |
2379 | case TEXPR_PTR: | |
2380 | s = message ("%q*%q", s, typeExpr_unparse (x->content.pointer)); | |
2381 | break; | |
2382 | case TEXPR_ARRAY: | |
2383 | s = message ("%q%q[%q]", s, | |
2384 | typeExpr_unparse (x->content.array.elementtype), | |
2385 | termNode_unparse (x->content.array.size)); | |
2386 | break; | |
2387 | case TEXPR_FCN: | |
2388 | s = message ("%q%q (", s, | |
2389 | typeExpr_unparse (x->content.function.returntype)); | |
2390 | params = x->content.function.args; | |
2391 | ||
2392 | if (!paramNodeList_empty (params)) | |
2393 | { | |
2394 | s = message ("%q%q", s, | |
2395 | paramNodeList_unparse (x->content.function.args)); | |
2396 | } | |
2397 | ||
2398 | s = message ("%q)", s); | |
2399 | break; | |
2400 | } | |
2401 | s = message ("%q%q%q", front, s, back); | |
2402 | } | |
2403 | else | |
2404 | { | |
2405 | s = cstring_makeLiteral ("?"); | |
2406 | } | |
2407 | ||
2408 | return s; | |
2409 | } | |
2410 | ||
2411 | /*@only@*/ cstring | |
2412 | typeExpr_unparseNoBase (/*@null@*/ typeExpr x) | |
2413 | { | |
2414 | cstring s = cstring_undefined; /* print out types in order of appearance in source */ | |
2415 | paramNodeList params; | |
2416 | int i; | |
2417 | ||
2418 | if (x != (typeExpr) 0) | |
2419 | { | |
2420 | cstring front = cstring_undefined; | |
2421 | cstring back = cstring_undefined; | |
2422 | ||
2423 | llassert (x->wrapped < 100); | |
2424 | ||
2425 | for (i = x->wrapped; i >= 1; i--) | |
2426 | { | |
2427 | front = cstring_appendChar (front, '('); | |
2428 | back = cstring_appendChar (back, ')'); | |
2429 | } | |
2430 | ||
2431 | switch (x->kind) | |
2432 | { | |
2433 | case TEXPR_BASE: | |
2434 | s = message ("%q /* %s */", s, ltoken_getRawString (x->content.base)); | |
2435 | break; | |
2436 | case TEXPR_PTR: | |
2437 | s = message ("%q*%q", s, typeExpr_unparseNoBase (x->content.pointer)); | |
2438 | break; | |
2439 | case TEXPR_ARRAY: | |
2440 | s = message ("%q%q[%q]", s, | |
2441 | typeExpr_unparseNoBase (x->content.array.elementtype), | |
2442 | termNode_unparse (x->content.array.size)); | |
2443 | break; | |
2444 | case TEXPR_FCN: | |
2445 | s = message ("%q%q (", s, | |
2446 | typeExpr_unparseNoBase (x->content.function.returntype)); | |
2447 | params = x->content.function.args; | |
2448 | ||
2449 | if (!paramNodeList_empty (params)) | |
2450 | { | |
2451 | s = message ("%q%q", s, | |
2452 | paramNodeList_unparse (x->content.function.args)); | |
2453 | } | |
2454 | ||
2455 | s = message ("%q)", s); | |
2456 | break; | |
2457 | } | |
2458 | s = message ("%q%q%q", front, s, back); | |
2459 | } | |
2460 | else | |
2461 | { | |
2462 | s = cstring_makeLiteral ("?"); | |
2463 | } | |
2464 | ||
2465 | return s; | |
2466 | } | |
2467 | ||
2468 | cstring | |
2469 | typeExpr_name (/*@null@*/ typeExpr x) | |
2470 | { | |
2471 | if (x != (typeExpr) 0) | |
2472 | { | |
2473 | switch (x->kind) | |
2474 | { | |
2475 | case TEXPR_BASE: | |
2476 | return (cstring_copy (ltoken_getRawString (x->content.base))); | |
2477 | case TEXPR_PTR: | |
2478 | return (typeExpr_name (x->content.pointer)); | |
2479 | case TEXPR_ARRAY: | |
2480 | return (typeExpr_name (x->content.array.elementtype)); | |
2481 | case TEXPR_FCN: | |
2482 | return (typeExpr_name (x->content.function.returntype)); | |
2483 | } | |
2484 | } | |
2485 | ||
2486 | /* evs --- 14 Mar 1995 | |
2487 | ** not a bug: its okay to have empty parameter names | |
2488 | ** llbug ("typeExpr_name: null"); | |
2489 | */ | |
2490 | ||
2491 | return cstring_undefined; | |
2492 | } | |
2493 | ||
2494 | /*@only@*/ typeExpr | |
2495 | makePointerNode (ltoken star, /*@only@*/ /*@returned@*/ typeExpr x) | |
2496 | { | |
2497 | if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0))) | |
2498 | { | |
2499 | x->content.function.returntype = makePointerNode (star, x->content.function.returntype); | |
2500 | return x; | |
2501 | } | |
2502 | else | |
2503 | { | |
2504 | typeExpr y = (typeExpr) dmalloc (sizeof (*y)); | |
2505 | ||
2506 | y->wrapped = 0; | |
2507 | y->kind = TEXPR_PTR; | |
2508 | y->content.pointer = x; | |
2509 | y->sort = sort_makeNoSort (); | |
2510 | ltoken_free (star); | |
2511 | ||
2512 | return y; | |
2513 | } | |
2514 | } | |
2515 | ||
2516 | typeExpr makeArrayNode (/*@returned@*/ typeExpr x, | |
2517 | /*@only@*/ arrayQualNode a) | |
2518 | { | |
2519 | if (x != (typeExpr)0 && (x->kind == TEXPR_FCN && (x->wrapped == 0))) | |
2520 | { | |
2521 | /* | |
2522 | ** Spurious errors reported here, because of referencing | |
2523 | ** in makeArrayNode. | |
2524 | */ | |
2525 | ||
b73d1009 | 2526 | /*@-usereleased@*/ |
2527 | x->content.function.returntype = makeArrayNode (x, a); | |
2528 | /*@=usereleased@*/ | |
2529 | /*@-kepttrans@*/ | |
2530 | return x; | |
2531 | /*@=kepttrans@*/ | |
616915dd | 2532 | } |
2533 | else | |
2534 | { | |
2535 | typeExpr y = (typeExpr) dmalloc (sizeof (*y)); | |
2536 | y->wrapped = 0; | |
2537 | y->kind = TEXPR_ARRAY; | |
2538 | ||
2539 | if (a == (arrayQualNode) 0) | |
2540 | { | |
2541 | y->content.array.size = (termNode) 0; | |
2542 | } | |
2543 | else | |
2544 | { | |
2545 | y->content.array.size = a->term; | |
2546 | ltoken_free (a->tok); | |
2547 | sfree (a); | |
2548 | } | |
2549 | ||
2550 | y->content.array.elementtype = x; | |
2551 | y->sort = sort_makeNoSort (); | |
2552 | ||
2553 | return (y); | |
2554 | } | |
2555 | } | |
2556 | ||
2557 | /*@only@*/ constDeclarationNode | |
2558 | makeConstDeclarationNode (lclTypeSpecNode t, initDeclNodeList decls) | |
2559 | { | |
2560 | constDeclarationNode n = (constDeclarationNode) dmalloc (sizeof (*n)); | |
2561 | sort s, s2, initValueSort; | |
2562 | ltoken varid, errtok; | |
2563 | termNode initValue; | |
2564 | ||
2565 | s = lclTypeSpecNode2sort (t); | |
2566 | ||
2567 | initDeclNodeList_elements (decls, init) | |
2568 | { | |
2569 | declaratorNode vdnode = init->declarator; | |
2570 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
2571 | ||
2572 | varid = ltoken_copy (vdnode->id); | |
2573 | s2 = typeExpr2ptrSort (s, vdnode->type); | |
2574 | initValue = init->value; | |
2575 | ||
2576 | if (termNode_isDefined (initValue) && !initValue->error_reported) | |
2577 | { | |
2578 | initValueSort = initValue->sort; | |
2579 | ||
2580 | /* should keep the arguments in order */ | |
2581 | if (!sort_member_modulo_cstring (s2, initValue) | |
2582 | && !initValue->error_reported) | |
2583 | { | |
2584 | errtok = termNode_errorToken (initValue); | |
2585 | ||
2586 | lclerror | |
2587 | (errtok, | |
2588 | message ("Constant %s declared type %q, initialized to %q: %q", | |
2589 | ltoken_unparse (varid), | |
2590 | sort_unparse (s2), | |
2591 | sort_unparse (initValueSort), | |
2592 | termNode_unparse (initValue))); | |
2593 | } | |
2594 | } | |
2595 | ||
2596 | vi->id = varid; | |
2597 | vi->kind = VRK_CONST; | |
2598 | vi->sort = s2; | |
2599 | vi->export = TRUE; | |
2600 | ||
2601 | (void) symtable_enterVar (g_symtab, vi); | |
2602 | varInfo_free (vi); | |
2603 | ||
2604 | } end_initDeclNodeList_elements; | |
2605 | ||
2606 | n->type = t; | |
2607 | n->decls = decls; | |
2608 | ||
2609 | return n; | |
2610 | } | |
2611 | ||
2612 | varDeclarationNode makeInternalStateNode (void) | |
2613 | { | |
2614 | varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); | |
2615 | ||
2616 | n->isSpecial = TRUE; | |
2617 | n->sref = sRef_makeInternalState (); | |
2618 | ||
2619 | /*@-compdef@*/ return n; /*@=compdef@*/ | |
2620 | } | |
2621 | ||
2622 | varDeclarationNode makeFileSystemNode (void) | |
2623 | { | |
2624 | varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); | |
2625 | ||
2626 | n->isSpecial = TRUE; | |
2627 | n->sref = sRef_makeSystemState (); | |
2628 | ||
2629 | /*@-compdef@*/ return n; /*@=compdef@*/ | |
2630 | } | |
2631 | ||
2632 | /*@only@*/ varDeclarationNode | |
2633 | makeVarDeclarationNode (lclTypeSpecNode t, initDeclNodeList x, | |
2634 | bool isGlobal, bool isPrivate) | |
2635 | { | |
2636 | varDeclarationNode n = (varDeclarationNode) dmalloc (sizeof (*n)); | |
2637 | sort s, s2, initValueSort; | |
2638 | ltoken varid, errtok; | |
2639 | termNode initValue; | |
2640 | declaratorNode vdnode; | |
2641 | ||
2642 | n->isSpecial = FALSE; | |
2643 | n->qualifier = QLF_NONE; | |
2644 | n->isGlobal = isGlobal; | |
2645 | n->isPrivate = isPrivate; | |
2646 | n->decls = x; | |
2647 | ||
2648 | s = lclTypeSpecNode2sort (t); | |
2649 | ||
2650 | /* t is an lclTypeSpec, its sort may not be assigned yet */ | |
2651 | ||
2652 | initDeclNodeList_elements (x, init) | |
2653 | { | |
2654 | vdnode = init->declarator; | |
2655 | varid = vdnode->id; | |
2656 | s2 = typeExpr2ptrSort (s, vdnode->type); | |
2657 | initValue = init->value; | |
2658 | ||
2659 | if (termNode_isDefined (initValue) && !initValue->error_reported) | |
2660 | { | |
2661 | initValueSort = initValue->sort; | |
2662 | /* should keep the arguments in order */ | |
2663 | if (!sort_member_modulo_cstring (s2, initValue) | |
2664 | && !initValue->error_reported) | |
2665 | { | |
2666 | errtok = termNode_errorToken (initValue); | |
2667 | ||
2668 | lclerror (errtok, | |
2669 | message ("Variable %s declared type %q, initialized to %q", | |
2670 | ltoken_unparse (varid), | |
2671 | sort_unparse (s2), | |
2672 | sort_unparse (initValueSort))); | |
2673 | } | |
2674 | } | |
2675 | ||
2676 | /* | |
2677 | ** If global, check that it has been declared already, don't push | |
2678 | ** onto symbol table yet (wrong scope, done in enteringFcnScope | |
2679 | */ | |
2680 | ||
2681 | if (isGlobal) | |
2682 | { | |
2683 | varInfo vi = symtable_varInfo (g_symtab, ltoken_getText (varid)); | |
2684 | ||
2685 | if (!varInfo_exists (vi)) | |
2686 | { | |
2687 | lclerror (varid, | |
2688 | message ("Undeclared global variable: %s", | |
2689 | ltoken_getRawString (varid))); | |
2690 | } | |
2691 | else | |
2692 | { | |
2693 | if (vi->kind == VRK_CONST) | |
2694 | { | |
2695 | lclerror (varid, | |
2696 | message ("Constant used in global list: %s", | |
2697 | ltoken_getRawString (varid))); | |
2698 | } | |
2699 | } | |
2700 | } | |
2701 | else | |
2702 | { | |
2703 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
2704 | ||
2705 | vi->id = ltoken_copy (varid); | |
2706 | if (isPrivate) | |
2707 | { | |
2708 | vi->kind = VRK_PRIVATE; | |
2709 | /* check that initValue is not empty */ | |
2710 | if (initValue == (termNode) 0) | |
2711 | { | |
2712 | lclerror (varid, | |
2713 | message ("Private variable must have initialization: %s", | |
2714 | ltoken_getRawString (varid))); | |
2715 | } | |
2716 | } | |
2717 | else | |
2718 | { | |
2719 | vi->kind = VRK_VAR; | |
2720 | } | |
2721 | ||
2722 | vi->sort = sort_makeGlobal (s2); | |
2723 | vi->export = TRUE; | |
2724 | ||
2725 | vdnode->isRedecl = symtable_enterVar (g_symtab, vi); | |
2726 | varInfo_free (vi); | |
2727 | } | |
2728 | } end_initDeclNodeList_elements; | |
2729 | ||
2730 | n->type = t; | |
2731 | ||
2732 | return n; | |
2733 | } | |
2734 | ||
2735 | /*@only@*/ initDeclNode | |
2736 | makeInitDeclNode (declaratorNode d, termNode x) | |
2737 | { | |
2738 | initDeclNode n = (initDeclNode) dmalloc (sizeof (*n)); | |
2739 | ||
2740 | n->declarator = d; | |
2741 | n->value = x; | |
2742 | return n; | |
2743 | } | |
2744 | ||
2745 | /*@only@*/ abstractNode | |
2746 | makeAbstractNode (ltoken t, ltoken name, | |
2747 | bool isMutable, bool isRefCounted, abstBodyNode a) | |
2748 | { | |
2749 | abstractNode n = (abstractNode) dmalloc (sizeof (*n)); | |
2750 | sort handle; | |
2751 | typeInfo ti = (typeInfo) dmalloc (sizeof (*ti)); | |
2752 | ||
2753 | n->tok = t; | |
2754 | n->isMutable = isMutable; | |
2755 | n->name = name; | |
2756 | n->body = a; | |
2757 | n->isRefCounted = isRefCounted; | |
2758 | ||
2759 | if (isMutable) | |
2760 | handle = sort_makeMutable (name, ltoken_getText (name)); | |
2761 | else | |
2762 | handle = sort_makeImmutable (name, ltoken_getText (name)); | |
2763 | n->sort = handle; | |
2764 | ||
2765 | ti->id = ltoken_createType (ltoken_getCode (ltoken_typename), SID_TYPE, | |
2766 | ltoken_getText (name)); | |
2767 | ti->modifiable = isMutable; | |
2768 | ti->abstract = TRUE; | |
2769 | ti->basedOn = handle; | |
2770 | ti->export = TRUE; | |
2771 | ||
2772 | symtable_enterType (g_symtab, ti); | |
2773 | ||
2774 | ||
2775 | return n; | |
2776 | } | |
2777 | ||
2778 | /*@only@*/ cstring | |
2779 | abstractNode_unparse (abstractNode n) | |
2780 | { | |
2781 | if (n != (abstractNode) 0) | |
2782 | { | |
2783 | cstring s; | |
2784 | ||
2785 | if (n->isMutable) | |
2786 | s = cstring_makeLiteral ("mutable"); | |
2787 | else | |
2788 | s = cstring_makeLiteral ("immutable"); | |
2789 | ||
2790 | return (message ("%q type %s%q;", s, ltoken_getRawString (n->name), | |
2791 | abstBodyNode_unparse (n->body))); | |
2792 | } | |
2793 | return cstring_undefined; | |
2794 | } | |
2795 | ||
2796 | void | |
2797 | setExposedType (lclTypeSpecNode s) | |
2798 | { | |
2799 | exposedType = s; | |
2800 | } | |
2801 | ||
2802 | /*@only@*/ exposedNode | |
2803 | makeExposedNode (ltoken t, lclTypeSpecNode s, | |
2804 | declaratorInvNodeList d) | |
2805 | { | |
2806 | exposedNode n = (exposedNode) dmalloc (sizeof (*n)); | |
2807 | ||
2808 | n->tok = t; | |
2809 | n->type = s; | |
2810 | n->decls = d; | |
2811 | ||
2812 | return n; | |
2813 | } | |
2814 | ||
2815 | /*@only@*/ cstring | |
2816 | exposedNode_unparse (exposedNode n) | |
2817 | { | |
2818 | if (n != (exposedNode) 0) | |
2819 | { | |
2820 | return (message ("typedef %q %q;", | |
2821 | lclTypeSpecNode_unparse (n->type), | |
2822 | declaratorInvNodeList_unparse (n->decls))); | |
2823 | } | |
2824 | return cstring_undefined; | |
2825 | } | |
2826 | ||
2827 | /*@only@*/ declaratorInvNode | |
2828 | makeDeclaratorInvNode (declaratorNode d, abstBodyNode b) | |
2829 | { | |
2830 | declaratorInvNode n = (declaratorInvNode) dmalloc (sizeof (*n)); | |
2831 | n->declarator = d; | |
2832 | n->body = b; | |
2833 | ||
2834 | return (n); | |
2835 | } | |
2836 | ||
2837 | /*@only@*/ cstring | |
2838 | declaratorInvNode_unparse (declaratorInvNode d) | |
2839 | { | |
2840 | return (message ("%q%q", declaratorNode_unparse (d->declarator), | |
2841 | abstBodyNode_unparseExposed (d->body))); | |
2842 | } | |
2843 | ||
2844 | /*@only@*/ cstring | |
2845 | abstBodyNode_unparse (abstBodyNode n) | |
2846 | { | |
2847 | if (n != (abstBodyNode) 0) | |
2848 | { | |
2849 | return (lclPredicateNode_unparse (n->typeinv)); | |
2850 | } | |
2851 | return cstring_undefined; | |
2852 | } | |
2853 | ||
2854 | /*@only@*/ cstring | |
2855 | abstBodyNode_unparseExposed (abstBodyNode n) | |
2856 | { | |
2857 | if (n != (abstBodyNode) 0) | |
2858 | { | |
2859 | return (message ("%q", lclPredicateNode_unparse (n->typeinv))); | |
2860 | } | |
2861 | return cstring_undefined; | |
2862 | } | |
2863 | ||
2864 | /*@only@*/ cstring | |
2865 | taggedUnionNode_unparse (taggedUnionNode n) | |
2866 | { | |
2867 | if (n != (taggedUnionNode) 0) | |
2868 | { | |
2869 | return (message ("tagged union {%q}%q;\n", | |
2870 | stDeclNodeList_unparse (n->structdecls), | |
2871 | declaratorNode_unparse (n->declarator))); | |
2872 | } | |
2873 | return cstring_undefined; | |
2874 | } | |
2875 | ||
2876 | static /*@observer@*/ paramNodeList | |
2877 | typeExpr_toParamNodeList (/*@null@*/ typeExpr te) | |
2878 | { | |
2879 | if (te != (typeExpr) 0) | |
2880 | { | |
2881 | switch (te->kind) | |
2882 | { | |
2883 | case TEXPR_FCN: | |
2884 | return te->content.function.args; | |
2885 | case TEXPR_PTR: | |
2886 | return typeExpr_toParamNodeList (te->content.pointer); | |
2887 | case TEXPR_ARRAY: | |
2888 | /* return typeExpr_toParamNodeList (te->content.array.elementtype); */ | |
2889 | case TEXPR_BASE: | |
2890 | return paramNodeList_undefined; | |
2891 | } | |
2892 | } | |
2893 | return paramNodeList_undefined; | |
2894 | } | |
2895 | ||
2896 | /*@only@*/ fcnNode | |
2897 | fcnNode_fromDeclarator (/*@only@*/ /*@null@*/ lclTypeSpecNode t, | |
2898 | /*@only@*/ declaratorNode d) | |
2899 | { | |
dfd82dce | 2900 | return (makeFcnNode (qual_createUnknown (), t, d, |
2901 | varDeclarationNodeList_new (), | |
2902 | varDeclarationNodeList_new (), | |
2903 | letDeclNodeList_new (), | |
616915dd | 2904 | (lclPredicateNode) 0, |
2905 | (lclPredicateNode) 0, | |
2906 | (modifyNode) 0, | |
2907 | (lclPredicateNode) 0, | |
2908 | (lclPredicateNode) 0)); | |
2909 | } | |
2910 | ||
2911 | /*@only@*/ iterNode | |
2912 | makeIterNode (ltoken id, paramNodeList p) | |
2913 | { | |
2914 | iterNode x = (iterNode) dmalloc (sizeof (*x)); | |
2915 | bool hasYield = FALSE; | |
2916 | ||
2917 | x->name = id; | |
2918 | x->params = p; | |
2919 | ||
2920 | /* check there is at least one yield param */ | |
2921 | ||
2922 | paramNodeList_elements (p, pe) | |
2923 | { | |
2924 | if (paramNode_isYield (pe)) | |
2925 | { | |
2926 | hasYield = TRUE; | |
2927 | break; | |
2928 | } | |
2929 | } end_paramNodeList_elements | |
2930 | ||
2931 | if (!hasYield) | |
2932 | { | |
2933 | lclerror (id, message ("Iterator has no yield parameters: %s", | |
2934 | ltoken_getRawString (id))); | |
2935 | } | |
2936 | ||
2937 | return (x); | |
2938 | } | |
2939 | ||
2940 | /*@only@*/ fcnNode | |
2941 | makeFcnNode (qual specQual, | |
2942 | /*@null@*/ lclTypeSpecNode t, | |
2943 | declaratorNode d, | |
2944 | /*@null@*/ globalList g, | |
2945 | /*@null@*/ varDeclarationNodeList privateinits, | |
2946 | /*@null@*/ letDeclNodeList lets, | |
2947 | /*@null@*/ lclPredicateNode checks, | |
2948 | /*@null@*/ lclPredicateNode requires, | |
2949 | /*@null@*/ modifyNode m, | |
2950 | /*@null@*/ lclPredicateNode ensures, | |
2951 | /*@null@*/ lclPredicateNode claims) | |
2952 | { | |
2953 | fcnNode x = (fcnNode) dmalloc (sizeof (*x)); | |
28bf4b0b | 2954 | |
616915dd | 2955 | if (d->type != (typeExpr)0 && (d->type)->kind != TEXPR_FCN) |
2956 | { | |
2957 | lclerror (d->id, cstring_makeLiteral | |
2958 | ("Attempt to specify function without parameter list")); | |
2959 | d->type = makeFunctionNode (d->type, paramNodeList_new ()); | |
2960 | } | |
28bf4b0b | 2961 | |
616915dd | 2962 | x->special = specQual; |
2963 | x->typespec = t; | |
2964 | x->declarator = d; | |
2965 | x->globals = g; | |
2966 | x->inits = privateinits; | |
2967 | x->lets = lets; | |
2968 | x->checks = checks; | |
2969 | x->require = requires; | |
2970 | x->modify = m; | |
2971 | x->ensures = ensures; | |
2972 | x->claim = claims; | |
2973 | ||
2974 | /* extract info to fill in x->name =; x->signature =; */ | |
2975 | x->name = ltoken_copy (d->id); | |
2976 | ||
2977 | return (x); | |
2978 | } | |
2979 | ||
2980 | /*@only@*/ claimNode | |
2981 | makeClaimNode (ltoken id, paramNodeList p, | |
2982 | globalList g, letDeclNodeList lets, lclPredicateNode requires, | |
2983 | programNode b, lclPredicateNode ensures) | |
2984 | { | |
2985 | claimNode x = (claimNode) dmalloc (sizeof (*x)); | |
2986 | ||
2987 | ||
2988 | x->name = id; | |
2989 | x->params = p; | |
2990 | x->globals = g; | |
2991 | x->lets = lets; | |
2992 | x->require = requires; | |
2993 | x->body = b; | |
2994 | x->ensures = ensures; | |
2995 | return (x); | |
2996 | } | |
2997 | ||
2998 | /*@only@*/ lclPredicateNode | |
2999 | makeIntraClaimNode (ltoken t, lclPredicateNode n) | |
3000 | { | |
3001 | ltoken_free (n->tok); | |
3002 | n->tok = t; | |
3003 | n->kind = LPD_INTRACLAIM; | |
3004 | return (n); | |
3005 | } | |
3006 | ||
3007 | /*@only@*/ lclPredicateNode | |
3008 | makeRequiresNode (ltoken t, lclPredicateNode n) | |
3009 | { | |
3010 | ltoken_free (n->tok); | |
3011 | n->tok = t; | |
3012 | n->kind = LPD_REQUIRES; | |
3013 | return (n); | |
3014 | } | |
3015 | ||
3016 | /*@only@*/ lclPredicateNode | |
3017 | makeChecksNode (ltoken t, lclPredicateNode n) | |
3018 | { | |
3019 | ltoken_free (n->tok); | |
3020 | n->tok = t; | |
3021 | n->kind = LPD_CHECKS; | |
3022 | return (n); | |
3023 | } | |
3024 | ||
3025 | /*@only@*/ lclPredicateNode | |
3026 | makeEnsuresNode (ltoken t, lclPredicateNode n) | |
3027 | { | |
3028 | ltoken_free (n->tok); | |
3029 | n->tok = t; | |
3030 | n->kind = LPD_ENSURES; | |
3031 | return (n); | |
3032 | } | |
3033 | ||
3034 | /*@only@*/ lclPredicateNode | |
3035 | makeLclPredicateNode (ltoken t, termNode n, | |
3036 | lclPredicateKind k) | |
3037 | { | |
3038 | lclPredicateNode x = (lclPredicateNode) dmalloc (sizeof (*x)); | |
3039 | ||
3040 | x->tok = t; | |
3041 | x->predicate = n; | |
3042 | x->kind = k; | |
3043 | return (x); | |
3044 | } | |
3045 | ||
3046 | /*@only@*/ quantifierNode | |
3047 | makeQuantifierNode (varNodeList v, ltoken quant) | |
3048 | { | |
3049 | quantifierNode x = (quantifierNode) dmalloc (sizeof (*x)); | |
3050 | ||
3051 | x->quant = quant; | |
3052 | x->vars = v; | |
3053 | x->isForall = cstring_equalLit (ltoken_unparse (quant), "\forall"); | |
3054 | ||
3055 | return (x); | |
3056 | } | |
3057 | ||
3058 | /*@only@*/ arrayQualNode | |
3059 | makeArrayQualNode (ltoken t, termNode term) | |
3060 | { | |
3061 | arrayQualNode x = (arrayQualNode) dmalloc (sizeof (*x)); | |
3062 | ||
3063 | x->tok = t; | |
3064 | x->term = term; | |
3065 | return (x); | |
3066 | } | |
3067 | ||
3068 | /*@only@*/ varNode | |
3069 | makeVarNode (/*@only@*/ ltoken varid, bool isObj, lclTypeSpecNode t) | |
3070 | { | |
3071 | varNode x = (varNode) dmalloc (sizeof (*x)); | |
3072 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
3073 | sort sort; | |
3074 | ||
3075 | vi->id = ltoken_copy (varid); | |
3076 | sort = lclTypeSpecNode2sort (t); | |
3077 | ||
3078 | /* 9/3/93, The following is needed because we want value sorts to be | |
3079 | the default, object sort is generated only if there is "obj" qualifier. | |
3080 | There are 2 cases: (1) for immutable types (including C primitive types), | |
3081 | we need to generate the object sort if qualifier is present; (2) for | |
3082 | array, struct and union types, they are already in their object sorts. | |
3083 | */ | |
3084 | ||
3085 | sort = sort_makeVal (sort); /* both cases are now value sorts */ | |
3086 | ||
3087 | if (isObj) | |
3088 | { | |
3089 | sort = sort_makeObj (sort); | |
3090 | } | |
3091 | ||
3092 | ||
3093 | vi->sort = sort; | |
3094 | vi->kind = VRK_QUANT; | |
3095 | vi->export = TRUE; | |
3096 | ||
3097 | (void) symtable_enterVar (g_symtab, vi); | |
3098 | varInfo_free (vi); | |
3099 | ||
3100 | x->varid = varid; | |
3101 | x->isObj = isObj; | |
3102 | x->type = t; | |
3103 | x->sort = sort_makeNoSort (); | |
3104 | ||
3105 | return (x); | |
3106 | } | |
3107 | ||
3108 | /*@only@*/ abstBodyNode | |
3109 | makeAbstBodyNode (ltoken t, fcnNodeList f) | |
3110 | { | |
3111 | abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); | |
3112 | ||
3113 | x->tok = t; | |
3114 | x->typeinv = (lclPredicateNode)0; | |
3115 | x->fcns = f; | |
3116 | return (x); | |
3117 | } | |
3118 | ||
3119 | /*@only@*/ abstBodyNode | |
3120 | makeExposedBodyNode (ltoken t, lclPredicateNode inv) | |
3121 | { | |
3122 | abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); | |
3123 | ||
3124 | x->tok = t; | |
3125 | x->typeinv = inv; | |
3126 | x->fcns = fcnNodeList_undefined; | |
3127 | return (x); | |
3128 | } | |
3129 | ||
3130 | /*@only@*/ abstBodyNode | |
3131 | makeAbstBodyNode2 (ltoken t, ltokenList ops) | |
3132 | { | |
3133 | abstBodyNode x = (abstBodyNode) dmalloc (sizeof (*x)); | |
3134 | ||
3135 | x->tok = t; | |
3136 | x->typeinv = (lclPredicateNode) 0; | |
3137 | ||
3138 | x->fcns = fcnNodeList_new (); | |
3139 | ||
3140 | ltokenList_elements (ops, op) | |
3141 | { | |
3142 | x->fcns = fcnNodeList_add | |
3143 | (x->fcns, | |
3144 | fcnNode_fromDeclarator (lclTypeSpecNode_undefined, | |
3145 | makeUnknownDeclaratorNode (ltoken_copy (op)))); | |
3146 | } end_ltokenList_elements; | |
3147 | ||
3148 | ltokenList_free (ops); | |
3149 | ||
3150 | return (x); | |
3151 | } | |
3152 | ||
3153 | /*@only@*/ stmtNode | |
3154 | makeStmtNode (ltoken varId, ltoken fcnId, /*@only@*/ termNodeList v) | |
3155 | { | |
3156 | stmtNode n = (stmtNode) dmalloc (sizeof (*n)); | |
3157 | ||
3158 | n->lhs = varId; | |
3159 | n->operator = fcnId; | |
3160 | n->args = v; | |
3161 | return (n); | |
3162 | } | |
3163 | ||
3164 | /* printDeclarators -> declaratorNodeList_unparse */ | |
3165 | ||
3166 | static cstring abstDeclaratorNode_unparse (abstDeclaratorNode x) | |
3167 | { | |
3168 | return (typeExpr_unparse ((typeExpr) x)); | |
3169 | } | |
3170 | ||
3171 | /*@only@*/ paramNode | |
3172 | makeParamNode (lclTypeSpecNode t, typeExpr d) | |
3173 | { | |
3174 | paramNode x = (paramNode) dmalloc (sizeof (*x)); | |
3175 | ||
3176 | paramNode_checkQualifiers (t, d); | |
3177 | ||
3178 | x->type = t; | |
3179 | x->paramdecl = d; | |
3180 | x->kind = PNORMAL; /*< forgot this! >*/ | |
3181 | ||
3182 | return (x); | |
3183 | } | |
3184 | ||
3185 | /*@only@*/ paramNode | |
3186 | paramNode_elipsis (void) | |
3187 | { | |
3188 | paramNode x = (paramNode) dmalloc (sizeof (*x)); | |
3189 | ||
3190 | x->type = (lclTypeSpecNode) 0; | |
3191 | x->paramdecl = (typeExpr) 0; | |
3192 | x->kind = PELIPSIS; | |
3193 | ||
3194 | return (x); | |
3195 | } | |
3196 | ||
3197 | static /*@observer@*/ ltoken typeExpr_getTok (typeExpr d) | |
3198 | { | |
3199 | while (d != (typeExpr)0) | |
3200 | { | |
3201 | if (d->kind == TEXPR_BASE) | |
3202 | { | |
3203 | return (d->content.base); | |
3204 | } | |
3205 | else | |
3206 | { | |
3207 | if (d->kind == TEXPR_PTR) | |
3208 | { | |
3209 | d = d->content.pointer; | |
3210 | } | |
3211 | else if (d->kind == TEXPR_ARRAY) | |
3212 | { | |
3213 | d = d->content.array.elementtype; | |
3214 | } | |
3215 | else if (d->kind == TEXPR_FCN) | |
3216 | { | |
3217 | d = d->content.function.returntype; | |
3218 | } | |
3219 | else | |
3220 | { | |
3221 | BADBRANCH; | |
3222 | } | |
3223 | } | |
3224 | } | |
3225 | ||
3226 | llfatalerror (cstring_makeLiteral ("typeExpr_getTok: unreachable code")); | |
3227 | BADEXIT; | |
3228 | } | |
3229 | ||
3230 | void | |
3231 | paramNode_checkQualifiers (lclTypeSpecNode t, typeExpr d) | |
3232 | { | |
3233 | bool isPointer = FALSE; | |
3234 | bool isUser = FALSE; | |
3235 | bool hasAlloc = FALSE; | |
3236 | bool hasAlias = FALSE; | |
3237 | ||
3238 | llassert (lclTypeSpecNode_isDefined (t)); | |
3239 | ||
f9264521 | 3240 | if (pointers_isUndefined (t->pointers) |
616915dd | 3241 | && (d != (typeExpr)0 && d->kind != TEXPR_PTR) && d->kind != TEXPR_ARRAY) |
3242 | { | |
3243 | if (t->kind == LTS_TYPE) | |
3244 | { | |
3245 | sortNode sn; | |
3246 | ||
3247 | llassert (t->content.type != NULL); | |
3248 | ||
3249 | sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort)); | |
3250 | ||
28bf4b0b | 3251 | if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY |
3252 | || sn->kind == SRT_HOF || sn->kind == SRT_NONE) | |
616915dd | 3253 | { |
3254 | isPointer = TRUE; | |
3255 | } | |
3256 | } | |
3257 | } | |
3258 | else | |
3259 | { | |
3260 | isPointer = TRUE; | |
3261 | } | |
3262 | ||
3263 | if (d != (typeExpr)0 && d->kind != TEXPR_BASE) | |
3264 | { | |
3265 | if (t->kind == LTS_TYPE) | |
3266 | { | |
3267 | sortNode sn; | |
3268 | ||
3269 | llassert (t->content.type != NULL); | |
3270 | sn = sort_quietLookup (sort_getUnderlying ((t->content.type)->sort)); | |
3271 | ||
28bf4b0b | 3272 | if (sn->kind == SRT_PTR || sn->kind == SRT_ARRAY |
3273 | || sn->kind == SRT_HOF || sn->kind == SRT_NONE) | |
616915dd | 3274 | { |
3275 | isUser = TRUE; | |
3276 | } | |
3277 | } | |
3278 | } | |
3279 | else | |
3280 | { | |
3281 | isPointer = TRUE; | |
3282 | } | |
3283 | ||
3284 | if (d != (typeExpr)NULL) | |
3285 | { | |
3286 | qualList_elements (t->quals, q) | |
3287 | { | |
3288 | if (qual_isAllocQual (q)) | |
3289 | { | |
3290 | if (hasAlloc) | |
3291 | { | |
3292 | ltoken tok = typeExpr_getTok (d); | |
3293 | lclerror (tok, message ("Parameter declared with multiple allocation " | |
3294 | "qualifiers: %q", typeExpr_unparse (d))); | |
3295 | } | |
3296 | hasAlloc = TRUE; | |
3297 | ||
3298 | if (!isPointer) | |
3299 | { | |
3300 | ltoken tok = typeExpr_getTok (d); | |
3301 | lclerror (tok, message ("Non-pointer declared as %s parameter: %q", | |
3302 | qual_unparse (q), | |
3303 | typeExpr_unparse (d))); | |
3304 | } | |
3305 | } | |
3306 | if (qual_isAliasQual (q)) | |
3307 | { | |
3308 | if (hasAlias) | |
3309 | { | |
3310 | ltoken tok = typeExpr_getTok (d); | |
3311 | lclerror (tok, message ("Parameter declared with multiple alias qualifiers: %q", | |
3312 | typeExpr_unparse (d))); | |
3313 | } | |
3314 | hasAlias = TRUE; | |
3315 | ||
3316 | if (!(isPointer || isUser)) | |
3317 | { | |
3318 | ltoken tok = typeExpr_getTok (d); | |
3319 | lclerror (tok, message ("Unsharable type declared as %s parameter: %q", | |
3320 | qual_unparse (q), | |
3321 | typeExpr_unparse (d))); | |
3322 | } | |
3323 | } | |
3324 | } end_qualList_elements; | |
3325 | } | |
3326 | } | |
3327 | ||
3328 | /*@only@*/ cstring | |
3329 | paramNode_unparse (paramNode x) | |
3330 | { | |
3331 | if (x != (paramNode) 0) | |
3332 | { | |
3333 | if (x->kind == PELIPSIS) | |
3334 | { | |
3335 | return (cstring_makeLiteral ("...")); | |
3336 | } | |
3337 | ||
3338 | if (x->paramdecl != (typeExpr) 0) | |
3339 | { /* handle (void) */ | |
3340 | return (message ("%q %q", lclTypeSpecNode_unparse (x->type), | |
3341 | typeExpr_unparse (x->paramdecl))); | |
3342 | } | |
3343 | else | |
3344 | { | |
3345 | return (lclTypeSpecNode_unparse (x->type)); | |
3346 | } | |
3347 | } | |
3348 | return cstring_undefined; | |
3349 | } | |
3350 | ||
3351 | static cstring | |
3352 | lclTypeSpecNode_unparseAltComments (/*@null@*/ lclTypeSpecNode typespec) /*@*/ | |
3353 | { | |
3354 | if (typespec != (lclTypeSpecNode) 0) | |
3355 | { | |
3356 | cstring s = qualList_toCComments (typespec->quals); | |
3357 | ||
3358 | switch (typespec->kind) | |
3359 | { | |
3360 | case LTS_TYPE: | |
3361 | { | |
3362 | llassert (typespec->content.type != NULL); | |
3363 | ||
3364 | return (cstring_concatFree | |
3365 | (s, printLeaves (typespec->content.type->ctypes))); | |
3366 | } | |
3367 | case LTS_ENUM: | |
3368 | { | |
3369 | bool first = TRUE; | |
3370 | enumSpecNode n = typespec->content.enumspec; | |
3371 | ||
3372 | s = cstring_concatFree (s, cstring_makeLiteral ("enum")); | |
3373 | llassert (n != NULL); | |
3374 | ||
3375 | if (!ltoken_isUndefined (n->opttagid)) | |
3376 | { | |
3377 | s = message ("%q %s", s, ltoken_unparse (n->opttagid)); | |
3378 | } | |
3379 | s = message ("%q {", s); | |
3380 | ||
3381 | ltokenList_elements (n->enums, e) | |
3382 | { | |
3383 | if (first) | |
3384 | { | |
3385 | first = FALSE; | |
3386 | s = message ("%q%s", s, ltoken_getRawString (e)); | |
3387 | } | |
3388 | else | |
3389 | s = message ("%q, %s", s, ltoken_getRawString (e)); | |
3390 | } end_ltokenList_elements; | |
3391 | ||
3392 | return (message ("%q}", s)); | |
3393 | } | |
3394 | case LTS_STRUCTUNION: | |
3395 | { | |
3396 | strOrUnionNode n = typespec->content.structorunion; | |
3397 | stDeclNodeList decls; | |
3398 | ||
3399 | llassert (n != NULL); | |
3400 | ||
3401 | switch (n->kind) | |
3402 | { | |
3403 | case SU_STRUCT: | |
3404 | s = cstring_concatFree (s, cstring_makeLiteral ("struct ")); | |
3405 | /*@switchbreak@*/ break; | |
3406 | case SU_UNION: | |
3407 | s = cstring_concatFree (s, cstring_makeLiteral ("union ")); | |
3408 | /*@switchbreak@*/ break; | |
3409 | } | |
3410 | ||
3411 | if (!ltoken_isUndefined (n->opttagid)) | |
3412 | { | |
3413 | if (stDeclNodeList_size (n->structdecls) == 0) | |
3414 | { | |
3415 | return (message ("%q%s", s, ltoken_unparse (n->opttagid))); | |
3416 | } | |
3417 | ||
d5047b91 | 3418 | s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid)); |
616915dd | 3419 | } |
3420 | else | |
3421 | { | |
d5047b91 | 3422 | s = message ("%q{\n\t", s); |
616915dd | 3423 | } |
3424 | ||
3425 | decls = n->structdecls; | |
3426 | ||
3427 | stDeclNodeList_elements (decls, f) | |
3428 | { | |
d5047b91 | 3429 | s = message ("%q%q %q;\n\t", s, |
616915dd | 3430 | lclTypeSpecNode_unparseAltComments (f->lcltypespec), |
3431 | declaratorNodeList_unparse (f->declarators)); | |
3432 | } end_stDeclNodeList_elements; | |
3433 | ||
d5047b91 | 3434 | return (message ("%q }", s)); |
616915dd | 3435 | } |
3436 | case LTS_CONJ: | |
3437 | { | |
3438 | cstring_free (s); | |
3439 | ||
3440 | return | |
3441 | (message | |
3442 | ("%q, %q", | |
3443 | lclTypeSpecNode_unparseAltComments (typespec->content.conj->a), | |
3444 | lclTypeSpecNode_unparseAltComments (typespec->content.conj->b))); | |
3445 | } | |
3446 | BADDEFAULT; | |
3447 | } | |
3448 | } | |
3449 | else | |
3450 | { | |
3451 | llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec"); | |
3452 | ||
3453 | return cstring_undefined; | |
3454 | } | |
3455 | ||
3456 | BADEXIT; | |
3457 | } | |
3458 | ||
3459 | cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec) | |
3460 | { | |
3461 | if (typespec != (lclTypeSpecNode) 0) | |
3462 | { | |
3463 | cstring s = qualList_toCComments (typespec->quals); | |
3464 | ||
3465 | switch (typespec->kind) | |
3466 | { | |
3467 | case LTS_TYPE: | |
3468 | { | |
3469 | llassert (typespec->content.type != NULL); | |
3470 | ||
3471 | return (cstring_concatFree | |
3472 | (s, printLeaves (typespec->content.type->ctypes))); | |
3473 | } | |
3474 | case LTS_ENUM: | |
3475 | { | |
3476 | bool first = TRUE; | |
3477 | enumSpecNode n = typespec->content.enumspec; | |
3478 | ||
3479 | s = cstring_concatFree (s, cstring_makeLiteral ("enum")); | |
3480 | llassert (n != NULL); | |
3481 | ||
3482 | if (!ltoken_isUndefined (n->opttagid)) | |
3483 | { | |
3484 | s = message ("%q %s", s, ltoken_unparse (n->opttagid)); | |
3485 | } | |
3486 | s = message ("%q {", s); | |
3487 | ||
3488 | ltokenList_elements (n->enums, e) | |
3489 | { | |
3490 | if (first) | |
3491 | { | |
3492 | first = FALSE; | |
3493 | s = message ("%q%s", s, ltoken_getRawString (e)); | |
3494 | } | |
3495 | else | |
3496 | s = message ("%q, %s", s, ltoken_getRawString (e)); | |
3497 | } end_ltokenList_elements; | |
3498 | ||
3499 | return (message ("%q}", s)); | |
3500 | } | |
3501 | case LTS_STRUCTUNION: | |
3502 | { | |
3503 | strOrUnionNode n = typespec->content.structorunion; | |
3504 | stDeclNodeList decls; | |
3505 | ||
3506 | llassert (n != NULL); | |
3507 | ||
3508 | switch (n->kind) | |
3509 | { | |
3510 | case SU_STRUCT: | |
3511 | s = cstring_concatFree (s, cstring_makeLiteral ("struct ")); | |
3512 | /*@switchbreak@*/ break; | |
3513 | case SU_UNION: | |
3514 | s = cstring_concatFree (s, cstring_makeLiteral ("union ")); | |
3515 | /*@switchbreak@*/ break; | |
3516 | } | |
3517 | ||
3518 | if (!ltoken_isUndefined (n->opttagid)) | |
3519 | { | |
3520 | if (stDeclNodeList_size (n->structdecls) == 0) | |
3521 | { | |
3522 | return (message ("%q%s", s, ltoken_unparse (n->opttagid))); | |
3523 | } | |
3524 | ||
d5047b91 | 3525 | s = message ("%q%s {\n\t", s, ltoken_unparse (n->opttagid)); |
616915dd | 3526 | } |
3527 | else | |
3528 | { | |
d5047b91 | 3529 | s = message ("%q{\n\t", s); |
616915dd | 3530 | } |
3531 | ||
3532 | decls = n->structdecls; | |
3533 | ||
3534 | stDeclNodeList_elements (decls, f) | |
3535 | { | |
d5047b91 | 3536 | s = message ("%q%q %q;\n\t", s, |
616915dd | 3537 | lclTypeSpecNode_unparseComments (f->lcltypespec), |
3538 | declaratorNodeList_unparse (f->declarators)); | |
3539 | } end_stDeclNodeList_elements; | |
3540 | ||
d5047b91 | 3541 | return (message ("%q }", s)); |
616915dd | 3542 | } |
3543 | case LTS_CONJ: | |
3544 | { | |
3545 | cstring_free (s); | |
3546 | ||
3547 | return | |
3548 | (message | |
3549 | ("%q /*@alt %q@*/", | |
3550 | lclTypeSpecNode_unparseComments (typespec->content.conj->a), | |
3551 | lclTypeSpecNode_unparseAltComments (typespec->content.conj->b))); | |
3552 | } | |
3553 | BADDEFAULT; | |
3554 | } | |
3555 | } | |
3556 | else | |
3557 | { | |
3558 | llcontbuglit ("lclTypeSpecNode_unparseComments: null typespec"); | |
3559 | ||
3560 | return cstring_undefined; | |
3561 | } | |
3562 | ||
3563 | BADEXIT; | |
3564 | } | |
3565 | ||
3566 | /*@only@*/ cstring | |
3567 | paramNode_unparseComments (paramNode x) | |
3568 | { | |
3569 | if (x != (paramNode) 0) | |
3570 | { | |
3571 | if (x->kind == PELIPSIS) | |
3572 | { | |
3573 | return (cstring_makeLiteral ("...")); | |
3574 | } | |
3575 | ||
3576 | if (x->paramdecl != (typeExpr) 0) | |
3577 | { /* handle (void) */ | |
3578 | return (message ("%q %q", | |
3579 | lclTypeSpecNode_unparseComments (x->type), | |
3580 | typeExpr_unparseNoBase (x->paramdecl))); | |
3581 | } | |
3582 | else | |
3583 | { | |
3584 | return (lclTypeSpecNode_unparseComments (x->type)); | |
3585 | } | |
3586 | } | |
3587 | return cstring_undefined; | |
3588 | } | |
3589 | ||
3590 | /*@only@*/ termNode | |
3591 | makeIfTermNode (ltoken ift, termNode ifn, ltoken thent, | |
3592 | termNode thenn, ltoken elset, | |
3593 | termNode elsen) | |
3594 | { | |
3595 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3596 | opFormNode opform = makeOpFormNode (ift, OPF_IF, opFormUnion_createMiddle (0), | |
3597 | ltoken_undefined); | |
3598 | nameNode nn = makeNameNodeForm (opform); | |
3599 | termNodeList args = termNodeList_new (); | |
3600 | ||
3601 | t->error_reported = FALSE; | |
3602 | t->wrapped = 0; | |
3603 | termNodeList_addh (args, ifn); | |
3604 | termNodeList_addh (args, thenn); | |
3605 | termNodeList_addh (args, elsen); | |
3606 | t->name = nn; | |
3607 | t->args = args; | |
3608 | t->kind = TRM_APPLICATION; | |
3609 | t->sort = sort_makeNoSort (); | |
3610 | t->given = t->sort; | |
3611 | t->possibleSorts = sortSet_new (); | |
3612 | t->possibleOps = lslOpSet_new (); | |
3613 | ||
3614 | ltoken_free (thent); | |
3615 | ltoken_free (elset); | |
3616 | ||
3617 | return (t); | |
3618 | } | |
3619 | ||
3620 | static /*@observer@*/ ltoken | |
3621 | nameNode2anyOp (nameNode n) | |
3622 | { | |
3623 | if (n != (nameNode) 0) | |
3624 | { | |
3625 | opFormNode opnode = n->content.opform; | |
3626 | opFormKind kind; | |
3627 | ||
3628 | llassert (opnode != NULL); | |
3629 | ||
3630 | kind = opnode->kind; | |
3631 | ||
3632 | if (kind == OPF_MANYOPM || kind == OPF_ANYOP || | |
3633 | kind == OPF_MANYOP || kind == OPF_ANYOPM) | |
3634 | { | |
3635 | opFormUnion u; | |
3636 | ||
3637 | u = opnode->content; | |
3638 | return u.anyop; | |
3639 | } | |
3640 | } | |
3641 | return ltoken_undefined; | |
3642 | } | |
3643 | ||
3644 | /*@only@*/ termNode | |
3645 | makeInfixTermNode (termNode x, ltoken op, termNode y) | |
3646 | { | |
3647 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3648 | opFormNode opform; | |
3649 | nameNode nn; | |
3650 | termNodeList args = termNodeList_new (); | |
3651 | ||
3652 | checkAssociativity (x, op); | |
3653 | ||
3654 | opform = makeOpFormNode (op, OPF_MANYOPM, | |
3655 | opFormUnion_createAnyOp (op), | |
3656 | ltoken_undefined); | |
3657 | ||
3658 | nn = makeNameNodeForm (opform); | |
3659 | ||
3660 | t->error_reported = FALSE; | |
3661 | t->wrapped = 0; | |
3662 | termNodeList_addh (args, x); | |
3663 | termNodeList_addh (args, y); | |
3664 | t->name = nn; | |
3665 | t->args = args; | |
3666 | t->kind = TRM_APPLICATION; | |
3667 | t->sort = sort_makeNoSort (); | |
3668 | t->given = t->sort; | |
28bf4b0b | 3669 | t->possibleSorts = sortSet_new (); /* sort_equal */ |
616915dd | 3670 | t->possibleOps = lslOpSet_new (); |
3671 | return (t); | |
3672 | } | |
3673 | ||
3674 | /*@only@*/ quantifiedTermNode | |
3675 | quantifiedTermNode_copy (quantifiedTermNode q) | |
3676 | { | |
3677 | quantifiedTermNode ret = (quantifiedTermNode) dmalloc (sizeof (*ret)); | |
3678 | ||
3679 | ret->quantifiers = quantifierNodeList_copy (q->quantifiers); | |
3680 | ret->open = ltoken_copy (q->open); | |
3681 | ret->close = ltoken_copy (q->close); | |
3682 | ret->body = termNode_copySafe (q->body); | |
3683 | ||
3684 | return (ret); | |
3685 | } | |
3686 | ||
3687 | /*@only@*/ termNode | |
3688 | makeQuantifiedTermNode (quantifierNodeList qn, ltoken open, | |
3689 | termNode t, ltoken close) | |
3690 | { | |
3691 | sort sort; | |
3692 | termNode n = (termNode) dmalloc (sizeof (*n)); | |
3693 | quantifiedTermNode q = (quantifiedTermNode) dmalloc (sizeof (*q)); | |
3694 | ||
1b8ae690 | 3695 | n->name = NULL; /*> missing this --- detected by splint <*/ |
616915dd | 3696 | n->error_reported = FALSE; |
3697 | n->wrapped = 0; | |
3698 | n->error_reported = FALSE; | |
3699 | n->kind = TRM_QUANTIFIER; | |
3700 | n->possibleSorts = sortSet_new (); | |
3701 | n->possibleOps = lslOpSet_new (); | |
3702 | n->kind = TRM_UNCHANGEDALL; | |
3703 | n->args = termNodeList_new (); /*< forgot this >*/ | |
3704 | ||
3705 | termNodeList_free (t->args); | |
3706 | t->args = termNodeList_new (); | |
3707 | ||
2a6e9c30 | 3708 | sort = g_sortBool; |
616915dd | 3709 | n->sort = sort; |
3710 | (void) sortSet_insert (n->possibleSorts, sort); | |
3711 | ||
3712 | q->quantifiers = qn; | |
3713 | q->open = open; | |
3714 | q->close = close; | |
3715 | q->body = t; | |
3716 | ||
3717 | n->quantified = q; | |
3718 | return (n); | |
3719 | } | |
3720 | ||
3721 | /*@only@*/ termNode | |
3722 | makePostfixTermNode (/*@returned@*/ /*@only@*/ termNode secondary, ltokenList postfixops) | |
3723 | { | |
3724 | termNode top = secondary; | |
3725 | ||
3726 | ltokenList_elements (postfixops, op) | |
3727 | { | |
3728 | top = makePostfixTermNode2 (top, ltoken_copy (op)); | |
3729 | /*@i@*/ } end_ltokenList_elements; | |
3730 | ||
3731 | ltokenList_free (postfixops); | |
3732 | ||
3733 | return (top); /* dep as only? */ | |
3734 | } | |
3735 | ||
3736 | /* | |
3737 | ** secondary is returned in the args list | |
3738 | */ | |
3739 | ||
3740 | /*@only@*/ termNode | |
3741 | makePostfixTermNode2 (/*@returned@*/ /*@only@*/ termNode secondary, | |
3742 | /*@only@*/ ltoken postfixop) | |
3743 | { | |
3744 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3745 | ||
3746 | opFormNode opform = makeOpFormNode (postfixop, | |
3747 | OPF_MANYOP, opFormUnion_createAnyOp (postfixop), | |
3748 | ltoken_undefined); | |
3749 | nameNode nn = makeNameNodeForm (opform); | |
3750 | termNodeList args = termNodeList_new (); | |
3751 | ||
3752 | t->error_reported = FALSE; | |
3753 | t->wrapped = 0; | |
3754 | termNodeList_addh (args, secondary); | |
3755 | t->name = nn; | |
3756 | t->args = args; | |
3757 | t->kind = TRM_APPLICATION; | |
3758 | t->sort = sort_makeNoSort (); | |
3759 | t->given = t->sort; | |
3760 | t->possibleSorts = sortSet_new (); | |
3761 | t->possibleOps = lslOpSet_new (); | |
3762 | return t; | |
3763 | } | |
3764 | ||
3765 | /*@only@*/ termNode | |
3766 | makePrefixTermNode (ltoken op, termNode arg) | |
3767 | { | |
3768 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3769 | termNodeList args = termNodeList_new (); | |
3770 | opFormNode opform = makeOpFormNode (op, OPF_ANYOPM, opFormUnion_createAnyOp (op), | |
3771 | ltoken_undefined); | |
3772 | nameNode nn = makeNameNodeForm (opform); | |
3773 | ||
3774 | t->error_reported = FALSE; | |
3775 | t->wrapped = 0; | |
3776 | t->name = nn; | |
3777 | termNodeList_addh (args, arg); | |
3778 | t->args = args; | |
3779 | t->kind = TRM_APPLICATION; | |
3780 | t->sort = sort_makeNoSort (); | |
3781 | t->given = t->sort; | |
3782 | t->possibleSorts = sortSet_new (); | |
3783 | t->possibleOps = lslOpSet_new (); | |
3784 | return t; | |
3785 | } | |
3786 | ||
3787 | /*@only@*/ termNode | |
3788 | makeOpCallTermNode (ltoken op, ltoken open, | |
3789 | termNodeList args, ltoken close) | |
3790 | { | |
3791 | /* like prefixTerm, but with opId LPAR termNodeList RPAR */ | |
3792 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3793 | nameNode nn = makeNameNodeId (op); | |
3794 | ||
3795 | t->error_reported = FALSE; | |
3796 | t->wrapped = 0; | |
3797 | t->name = nn; | |
3798 | t->args = args; | |
3799 | t->kind = TRM_APPLICATION; | |
3800 | t->sort = sort_makeNoSort (); | |
3801 | t->given = t->sort; | |
3802 | t->possibleSorts = sortSet_new (); | |
3803 | t->possibleOps = lslOpSet_new (); | |
3804 | ||
3805 | ltoken_free (open); | |
3806 | ltoken_free (close); | |
3807 | ||
3808 | return t; | |
3809 | } | |
3810 | ||
3811 | /*@exposed@*/ termNode | |
3812 | CollapseInfixTermNode (/*@returned@*/ termNode secondary, termNodeList infix) | |
3813 | { | |
3814 | termNode left = secondary; | |
3815 | ||
3816 | termNodeList_elements (infix, node) | |
3817 | { | |
3818 | termNodeList_addl (node->args, termNode_copySafe (left)); | |
3819 | left = node; | |
3820 | /* computePossibleSorts (left); */ | |
3821 | } end_termNodeList_elements; | |
3822 | ||
3823 | return (left); | |
3824 | } | |
3825 | ||
3826 | static void | |
3827 | checkAssociativity (termNode x, ltoken op) | |
3828 | { | |
3829 | ltoken lastOpToken; | |
3830 | ||
3831 | if (x->wrapped == 0 && /* no parentheses */ | |
3832 | x->kind == TRM_APPLICATION && x->name != (nameNode) 0 && | |
3833 | (!x->name->isOpId)) | |
3834 | { | |
3835 | lastOpToken = nameNode2anyOp (x->name); | |
3836 | ||
3837 | if ((ltoken_getCode (lastOpToken) == logicalOp && | |
3838 | ltoken_getCode (op) == logicalOp) || | |
3839 | ((ltoken_getCode (lastOpToken) == simpleOp || | |
3840 | ltoken_getCode (lastOpToken) == LLT_MULOP) && | |
3841 | (ltoken_getCode (op) == simpleOp || | |
3842 | ltoken_getCode (op) == LLT_MULOP))) | |
3843 | if (ltoken_getText (lastOpToken) != ltoken_getText (op)) | |
3844 | { | |
3845 | lclerror (op, | |
3846 | message | |
3847 | ("Parentheses needed to specify associativity of %s and %s", | |
3848 | cstring_fromChars (lsymbol_toChars (ltoken_getText (lastOpToken))), | |
3849 | cstring_fromChars (lsymbol_toChars (ltoken_getText (op))))); | |
3850 | } | |
3851 | } | |
3852 | } | |
3853 | ||
3854 | termNodeList | |
3855 | pushInfixOpPartNode (/*@returned@*/ termNodeList x, ltoken op, | |
3856 | /*@only@*/ termNode secondary) | |
3857 | { | |
3858 | termNode lastLeftTerm; | |
3859 | termNodeList args = termNodeList_new (); | |
3860 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3861 | opFormNode opform; | |
3862 | nameNode nn; | |
3863 | ||
3864 | termNodeList_addh (args, secondary); | |
3865 | ||
3866 | if (!termNodeList_empty (x)) | |
3867 | { | |
3868 | termNodeList_reset (x); | |
3869 | lastLeftTerm = termNodeList_current (x); | |
3870 | checkAssociativity (lastLeftTerm, op); | |
3871 | } | |
3872 | ||
3873 | opform = makeOpFormNode (op, OPF_MANYOPM, | |
3874 | opFormUnion_createAnyOp (op), ltoken_undefined); | |
3875 | ||
3876 | nn = makeNameNodeForm (opform); | |
3877 | ||
3878 | t->error_reported = FALSE; | |
3879 | t->wrapped = 0; | |
3880 | t->name = nn; | |
3881 | t->kind = TRM_APPLICATION; | |
3882 | t->args = args; | |
3883 | t->sort = sort_makeNoSort (); | |
3884 | t->given = t->sort; | |
3885 | t->possibleSorts = sortSet_new (); | |
3886 | t->possibleOps = lslOpSet_new (); | |
3887 | termNodeList_addh (x, t); | |
3888 | /* don't compute sort yet, do it in CollapseInfixTermNode */ | |
3889 | return (x); | |
3890 | } | |
3891 | ||
3892 | termNode | |
3893 | updateMatchedNode (/*@only@*/ termNode left, /*@returned@*/ termNode t, | |
3894 | /*@only@*/ termNode right) | |
3895 | { | |
3896 | opFormNode op; | |
3897 | ||
3898 | if ((t == (termNode) 0) || (t->name == NULL) || t->name->isOpId) | |
3899 | { | |
3900 | llbugexitlit ("updateMatchedNode: expect opForm in nameNode"); | |
3901 | } | |
3902 | ||
3903 | op = t->name->content.opform; | |
3904 | llassert (op != NULL); | |
3905 | ||
3906 | if (left == (termNode) 0) | |
3907 | { | |
3908 | if (right == (termNode) 0) | |
3909 | { | |
3910 | /* op->kind is not changed */ | |
3911 | termNode_free (right); | |
3912 | } | |
3913 | else | |
3914 | { | |
3915 | op->kind = OPF_MIDDLEM; | |
3916 | op->key = opFormNode2key (op, OPF_MIDDLEM); | |
3917 | termNodeList_addh (t->args, right); | |
3918 | } | |
3919 | } | |
3920 | else | |
3921 | { | |
3922 | termNodeList_addl (t->args, left); | |
3923 | if (right == (termNode) 0) | |
3924 | { | |
3925 | op->kind = OPF_MMIDDLE; | |
3926 | op->key = opFormNode2key (op, OPF_MMIDDLE); | |
3927 | } | |
3928 | else | |
3929 | { | |
3930 | op->kind = OPF_MMIDDLEM; | |
3931 | op->key = opFormNode2key (op, OPF_MMIDDLEM); | |
3932 | termNodeList_addh (t->args, right); | |
3933 | } | |
3934 | } | |
3935 | return t; | |
3936 | } | |
3937 | ||
3938 | /*@only@*/ termNode | |
3939 | updateSqBracketedNode (/*@only@*/ termNode left, | |
3940 | /*@only@*/ /*@returned@*/ termNode t, | |
3941 | /*@only@*/ termNode right) | |
3942 | { | |
3943 | opFormNode op; | |
3944 | ||
3945 | if ((t == (termNode) 0) || (t->name == NULL) || (t->name->isOpId)) | |
3946 | { | |
3947 | llbugexitlit ("updateSqBracketededNode: expect opForm in nameNode"); | |
3948 | } | |
3949 | ||
3950 | op = t->name->content.opform; | |
3951 | llassert (op != NULL); | |
3952 | ||
3953 | if (left == (termNode) 0) | |
3954 | { | |
3955 | if (right == (termNode) 0) | |
3956 | { | |
3957 | /* op->kind is not changed */ | |
3958 | } | |
3959 | else | |
3960 | { | |
3961 | op->kind = OPF_BMIDDLEM; | |
3962 | op->key = opFormNode2key (op, OPF_BMIDDLEM); | |
3963 | termNodeList_addh (t->args, right); | |
3964 | } | |
3965 | } | |
3966 | else | |
3967 | { | |
3968 | termNodeList_addl (t->args, left); | |
3969 | ||
3970 | if (right == (termNode) 0) | |
3971 | { | |
3972 | op->kind = OPF_BMMIDDLE; | |
3973 | op->key = opFormNode2key (op, OPF_BMMIDDLE); | |
3974 | } | |
3975 | else | |
3976 | { | |
3977 | op->kind = OPF_BMMIDDLEM; | |
3978 | op->key = opFormNode2key (op, OPF_BMMIDDLEM); | |
3979 | termNodeList_addh (t->args, right); | |
3980 | } | |
3981 | } | |
3982 | return t; | |
3983 | } | |
3984 | ||
3985 | /*@only@*/ termNode | |
3986 | makeSqBracketedNode (ltoken lbracket, | |
3987 | termNodeList args, ltoken rbracket) | |
3988 | { | |
3989 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
3990 | int size; | |
3991 | opFormNode opform; | |
3992 | nameNode nn; | |
3993 | ||
3994 | t->error_reported = FALSE; | |
3995 | t->wrapped = 0; | |
3996 | ||
3997 | size = termNodeList_size (args); | |
3998 | opform = makeOpFormNode (lbracket, OPF_BMIDDLE, opFormUnion_createMiddle (size), | |
3999 | rbracket); | |
4000 | nn = makeNameNodeForm (opform); | |
4001 | t->name = nn; | |
4002 | t->kind = TRM_APPLICATION; | |
4003 | t->args = args; | |
4004 | t->sort = sort_makeNoSort (); | |
4005 | t->given = t->sort; | |
4006 | t->possibleSorts = sortSet_new (); | |
4007 | t->possibleOps = lslOpSet_new (); | |
4008 | /* do sort checking later, not here, incomplete parse */ | |
4009 | return (t); | |
4010 | } | |
4011 | ||
4012 | /*@only@*/ termNode | |
4013 | makeMatchedNode (ltoken open, termNodeList args, ltoken close) | |
4014 | { | |
4015 | /* matched : open args close */ | |
4016 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4017 | int size; | |
4018 | opFormNode opform; | |
4019 | nameNode nn; | |
4020 | ||
4021 | t->error_reported = FALSE; | |
4022 | t->wrapped = 0; | |
4023 | ||
4024 | size = termNodeList_size (args); | |
4025 | opform = makeOpFormNode (open, OPF_MIDDLE, opFormUnion_createMiddle (size), close); | |
4026 | nn = makeNameNodeForm (opform); | |
4027 | t->name = nn; | |
4028 | t->kind = TRM_APPLICATION; | |
4029 | t->args = args; | |
4030 | t->sort = sort_makeNoSort (); | |
4031 | t->given = t->sort; | |
4032 | t->possibleSorts = sortSet_new (); | |
4033 | t->possibleOps = lslOpSet_new (); | |
4034 | /* do sort checking later, not here, incomplete parse */ | |
4035 | return (t); | |
4036 | } | |
4037 | ||
4038 | /*@only@*/ termNode | |
4039 | makeSimpleTermNode (ltoken varid) | |
4040 | { | |
4041 | sort theSort = sort_makeNoSort (); | |
4042 | lsymbol sym; | |
4043 | opInfo oi; | |
4044 | varInfo vi; | |
4045 | termNode n = (termNode) dmalloc (sizeof (*n)); | |
4046 | ||
4047 | n->error_reported = FALSE; | |
4048 | n->wrapped = 0; | |
4049 | n->name = (nameNode) 0; | |
4050 | n->given = theSort; | |
4051 | n->args = termNodeList_new (); | |
4052 | n->possibleSorts = sortSet_new (); | |
4053 | n->possibleOps = lslOpSet_new (); | |
4054 | ||
4055 | sym = ltoken_getText (varid); | |
4056 | ||
4057 | /* lookup current scope */ | |
4058 | vi = symtable_varInfoInScope (g_symtab, sym); | |
4059 | ||
4060 | if (varInfo_exists (vi)) | |
4061 | { | |
4062 | theSort = vi->sort; | |
4063 | n->kind = TRM_VAR; | |
4064 | n->sort = theSort; | |
4065 | n->literal = varid; | |
4066 | (void) sortSet_insert (n->possibleSorts, theSort); | |
4067 | } | |
4068 | else | |
4069 | { /* need to handle LCL constants */ | |
4070 | vi = symtable_varInfo (g_symtab, sym); | |
4071 | ||
4072 | if (varInfo_exists (vi) && vi->kind == VRK_CONST) | |
4073 | { | |
4074 | theSort = vi->sort; | |
4075 | n->kind = TRM_CONST; | |
4076 | n->sort = theSort; | |
4077 | n->literal = varid; | |
4078 | (void) sortSet_insert (n->possibleSorts, theSort); | |
4079 | } | |
4080 | else | |
4081 | { /* and LSL operators (true, false, new, nil, etc) */ | |
4082 | nameNode nn = makeNameNodeId (ltoken_copy (varid)); | |
4083 | oi = symtable_opInfo (g_symtab, nn); | |
4084 | ||
4085 | if (opInfo_exists (oi) && (oi->name->isOpId) && | |
4086 | !sigNodeSet_isEmpty (oi->signatures)) | |
4087 | { | |
4088 | sigNodeSet_elements (oi->signatures, x) | |
4089 | { | |
4090 | if (ltokenList_empty (x->domain)) | |
4091 | /* yes, it really is empty, not not empty */ | |
4092 | { | |
4093 | lslOp op = (lslOp) dmalloc (sizeof (*op)); | |
4094 | ||
4095 | op->name = nameNode_copy (nn); | |
4096 | op->signature = x; | |
4097 | (void) sortSet_insert (n->possibleSorts, sigNode_rangeSort (x)); | |
4098 | (void) lslOpSet_insert (n->possibleOps, op); | |
4099 | } | |
4100 | } end_sigNodeSet_elements; | |
4101 | } | |
4102 | ||
4103 | nameNode_free (nn); | |
4104 | ||
4105 | if (sortSet_size (n->possibleSorts) == 0) | |
4106 | { | |
4107 | lclerror | |
4108 | (varid, | |
4109 | message ("Unrecognized identifier (constant, variable or operator): %s", | |
4110 | ltoken_getRawString (varid))); | |
4111 | ||
4112 | } | |
4113 | ||
4114 | n->sort = sort_makeNoSort (); | |
4115 | n->literal = varid; | |
4116 | n->kind = TRM_ZEROARY; | |
4117 | } | |
4118 | } | |
4119 | ||
4120 | return (n); | |
4121 | } | |
4122 | ||
4123 | /*@only@*/ termNode | |
4124 | makeSelectTermNode (termNode pri, ltoken select, /*@dependent@*/ ltoken id) | |
4125 | { | |
4126 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4127 | opFormNode opform = makeOpFormNode (select, | |
4128 | OPF_MSELECT, opFormUnion_createAnyOp (id), | |
4129 | ltoken_undefined); | |
4130 | nameNode nn = makeNameNodeForm (opform); | |
4131 | termNodeList args = termNodeList_new (); | |
4132 | ||
4133 | t->error_reported = FALSE; | |
4134 | t->wrapped = 0; | |
4135 | t->name = nn; | |
4136 | t->kind = TRM_APPLICATION; | |
4137 | termNodeList_addh (args, pri); | |
4138 | t->args = args; | |
4139 | t->kind = TRM_APPLICATION; | |
4140 | t->sort = sort_makeNoSort (); | |
4141 | t->given = t->sort; | |
4142 | t->possibleSorts = sortSet_new (); | |
4143 | t->possibleOps = lslOpSet_new (); | |
4144 | ||
4145 | return t; | |
4146 | } | |
4147 | ||
4148 | /*@only@*/ termNode | |
4149 | makeMapTermNode (termNode pri, ltoken map, /*@dependent@*/ ltoken id) | |
4150 | { | |
4151 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4152 | opFormNode opform = makeOpFormNode (map, OPF_MMAP, opFormUnion_createAnyOp (id), | |
4153 | ltoken_undefined); | |
4154 | nameNode nn = makeNameNodeForm (opform); | |
4155 | termNodeList args = termNodeList_new (); | |
4156 | ||
4157 | t->error_reported = FALSE; | |
4158 | t->wrapped = 0; | |
4159 | t->kind = TRM_APPLICATION; | |
4160 | t->name = nn; | |
4161 | termNodeList_addh (args, pri); | |
4162 | t->args = args; | |
4163 | t->kind = TRM_APPLICATION; | |
4164 | t->sort = sort_makeNoSort (); | |
4165 | t->given = t->sort; | |
4166 | t->possibleSorts = sortSet_new (); | |
4167 | t->possibleOps = lslOpSet_new (); | |
4168 | return t; | |
4169 | } | |
4170 | ||
4171 | /*@only@*/ termNode | |
4172 | makeLiteralTermNode (ltoken tok, sort s) | |
4173 | { | |
4174 | nameNode nn = makeNameNodeId (ltoken_copy (tok)); | |
4175 | opInfo oi = symtable_opInfo (g_symtab, nn); | |
4176 | lslOp op = (lslOp) dmalloc (sizeof (*op)); | |
4177 | termNode n = (termNode) dmalloc (sizeof (*n)); | |
4178 | sigNode sign; | |
4179 | ltoken range; | |
4180 | ||
4181 | n->name = nn; | |
4182 | n->error_reported = FALSE; | |
4183 | n->wrapped = 0; | |
4184 | n->kind = TRM_LITERAL; | |
4185 | n->literal = tok; | |
4186 | n->given = sort_makeNoSort (); | |
4187 | n->sort = n->given; | |
4188 | n->args = termNodeList_new (); | |
4189 | n->possibleSorts = sortSet_new (); | |
4190 | n->possibleOps = lslOpSet_new (); | |
4191 | ||
4192 | /* look up signatures for this operator too */ | |
4193 | ||
4194 | range = ltoken_create (simpleId, sort_getLsymbol (s)); | |
dfd82dce | 4195 | sign = makesigNode (ltoken_undefined, ltokenList_new (), |
616915dd | 4196 | ltoken_copy (range)); |
4197 | ||
4198 | if (opInfo_exists (oi) && (oi->name->isOpId) | |
4199 | && (sigNodeSet_size (oi->signatures) > 0)) | |
4200 | { | |
4201 | sigNodeSet_elements (oi->signatures, x) | |
4202 | { | |
4203 | if (ltokenList_empty (x->domain)) | |
4204 | { | |
4205 | lslOp opn = (lslOp) dmalloc (sizeof (*opn)); | |
4206 | sort sort; | |
4207 | ||
4208 | opn->name = nameNode_copy (nn); | |
4209 | opn->signature = x; | |
4210 | sort = sigNode_rangeSort (x); | |
4211 | (void) sortSet_insert (n->possibleSorts, sort); | |
4212 | (void) lslOpSet_insert (n->possibleOps, opn); | |
4213 | } | |
4214 | } end_sigNodeSet_elements; | |
4215 | } | |
4216 | ||
4217 | /* insert into literal term */ | |
4218 | (void) sortSet_insert (n->possibleSorts, s); | |
4219 | ||
4220 | op->name = nameNode_copy (nn); | |
4221 | op->signature = sign; | |
4222 | (void) lslOpSet_insert (n->possibleOps, op); | |
4223 | ||
4224 | /* enter the literal as an operator into the operator table */ | |
4225 | /* 8/9/93. C's char constant 'c' syntax conflicts | |
4226 | with LSL's lslinit.lsi table. Throw out, because it's not | |
4227 | needed anyway. */ | |
4228 | /* symtable_enterOp (g_symtab, nn, sign); */ | |
4229 | ||
2a6e9c30 | 4230 | if (s == g_sortInt) |
616915dd | 4231 | { |
4232 | sigNode osign; | |
4233 | lslOp opn = (lslOp) dmalloc (sizeof (*opn)); | |
4234 | ||
4235 | /* if it is a C int, we should overload it as double too because | |
4236 | C allows you to say "x > 2". */ | |
4237 | ||
2a6e9c30 | 4238 | (void) sortSet_insert (n->possibleSorts, g_sortDouble); |
616915dd | 4239 | |
4240 | ltoken_setText (range, lsymbol_fromChars ("double")); | |
4241 | osign = makesigNode (ltoken_undefined, ltokenList_new (), range); | |
4242 | opn->name = nameNode_copy (nn); | |
4243 | opn->signature = osign; | |
4244 | (void) lslOpSet_insert (n->possibleOps, opn); | |
4245 | ||
4246 | symtable_enterOp (g_symtab, nameNode_copySafe (nn), sigNode_copy (osign)); | |
4247 | } | |
4248 | else | |
4249 | { | |
4250 | ltoken_free (range); | |
4251 | } | |
4252 | ||
4253 | /* future: could overload cstrings to be both char_Vec as well as | |
4254 | char_ObjPtr */ | |
4255 | ||
4256 | /*@-mustfree@*/ | |
4257 | return n; | |
4258 | } /*@=mustfree@*/ | |
4259 | ||
4260 | /*@only@*/ termNode | |
4261 | makeUnchangedTermNode1 (ltoken op, /*@unused@*/ ltoken all) | |
4262 | { | |
4263 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4264 | ||
4265 | t->error_reported = FALSE; | |
4266 | t->wrapped = 0; | |
4267 | t->kind = TRM_UNCHANGEDALL; | |
2a6e9c30 | 4268 | t->sort = g_sortBool; |
616915dd | 4269 | t->literal = op; |
4270 | t->given = sort_makeNoSort (); | |
4271 | t->name = NULL; /*< missing this >*/ | |
4272 | t->args = termNodeList_new (); | |
4273 | t->possibleSorts = sortSet_new (); | |
4274 | t->possibleOps = lslOpSet_new (); | |
4275 | (void) sortSet_insert (t->possibleSorts, t->sort); | |
4276 | ||
4277 | ltoken_free (all); | |
4278 | ||
4279 | return t; | |
4280 | } | |
4281 | ||
4282 | /*@only@*/ termNode | |
4283 | makeUnchangedTermNode2 (ltoken op, storeRefNodeList x) | |
4284 | { | |
4285 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4286 | ltoken errtok; | |
4287 | sort sort; | |
4288 | ||
4289 | t->name = NULL; /*< missing this >*/ | |
4290 | t->error_reported = FALSE; | |
4291 | t->wrapped = 0; | |
4292 | t->kind = TRM_UNCHANGEDOTHERS; | |
2a6e9c30 | 4293 | t->sort = g_sortBool; |
616915dd | 4294 | t->literal = op; |
4295 | t->unchanged = x; | |
4296 | t->given = sort_makeNoSort (); | |
4297 | t->possibleSorts = sortSet_new (); | |
4298 | t->possibleOps = lslOpSet_new (); | |
4299 | t->args = termNodeList_new (); | |
4300 | ||
4301 | (void) sortSet_insert (t->possibleSorts, t->sort); | |
4302 | /* check storeRefNode's are mutable, uses sort of term */ | |
4303 | ||
4304 | storeRefNodeList_elements (x, sto) | |
4305 | { | |
4306 | if (storeRefNode_isTerm (sto)) | |
4307 | { | |
4308 | sort = sto->content.term->sort; | |
4309 | if (!sort_mutable (sort)) | |
4310 | { | |
4311 | errtok = termNode_errorToken (sto->content.term); | |
4312 | lclerror (errtok, | |
4313 | message ("Term denoting immutable object used in unchanged list: %q", | |
4314 | termNode_unparse (sto->content.term))); | |
4315 | } | |
4316 | } | |
4317 | else | |
4318 | { | |
4319 | if (storeRefNode_isType (sto)) | |
4320 | { | |
4321 | lclTypeSpecNode type = sto->content.type; | |
4322 | sort = lclTypeSpecNode2sort (type); | |
4323 | if (!sort_mutable (sort)) | |
4324 | { | |
4325 | errtok = lclTypeSpecNode_errorToken (type); | |
4326 | lclerror (errtok, message ("Immutable type used in unchanged list: %q", | |
4327 | sort_unparse (sort))); | |
4328 | } | |
4329 | } | |
4330 | } | |
4331 | } end_storeRefNodeList_elements; | |
4332 | ||
4333 | return t; | |
4334 | } | |
4335 | ||
4336 | /*@only@*/ termNode | |
4337 | makeSizeofTermNode (ltoken op, lclTypeSpecNode type) | |
4338 | { | |
4339 | termNode t = (termNode) dmalloc (sizeof (*t)); | |
4340 | ||
4341 | t->name = NULL; /*< missing this >*/ | |
4342 | t->error_reported = FALSE; | |
4343 | t->wrapped = 0; | |
4344 | t->kind = TRM_SIZEOF; | |
2a6e9c30 | 4345 | t->sort = g_sortInt; |
616915dd | 4346 | t->literal = op; |
4347 | t->sizeofField = type; | |
4348 | t->given = sort_makeNoSort (); | |
4349 | t->possibleSorts = sortSet_new (); | |
4350 | t->possibleOps = lslOpSet_new (); | |
4351 | t->args = termNodeList_new (); | |
4352 | ||
4353 | (void) sortSet_insert (t->possibleSorts, t->sort); | |
4354 | /* nothing to check */ | |
4355 | return (t); | |
4356 | } | |
4357 | ||
4358 | /*@only@*/ cstring | |
4359 | claimNode_unparse (claimNode c) | |
4360 | { | |
4361 | if (c != (claimNode) 0) | |
4362 | { | |
4363 | cstring s = message ("claims (%q)%q{\n%q", | |
4364 | paramNodeList_unparse (c->params), | |
4365 | varDeclarationNodeList_unparse (c->globals), | |
4366 | lclPredicateNode_unparse (c->require)); | |
4367 | ||
4368 | if (c->body != NULL) | |
4369 | { | |
4370 | s = message ("%qbody {%q}\n", s, programNode_unparse (c->body)); | |
4371 | } | |
4372 | s = message ("%q%q}\n", s, lclPredicateNode_unparse (c->ensures)); | |
4373 | return s; | |
4374 | } | |
4375 | return cstring_undefined; | |
4376 | } | |
4377 | ||
4378 | static void | |
4379 | WrongArity (ltoken tok, int expect, int size) | |
4380 | { | |
4381 | lclerror (tok, message ("Expecting %d arguments but given %d", expect, size)); | |
4382 | } | |
4383 | ||
4384 | static cstring | |
4385 | printTermNode2 (/*@null@*/ opFormNode op, termNodeList args, sort sort) | |
4386 | { | |
4387 | if (op != (opFormNode) 0) | |
4388 | { | |
4389 | cstring s = cstring_undefined; | |
4390 | cstring sortText; | |
4391 | cstring sortSpace; | |
4392 | ||
4393 | if (sort != sort_makeNoSort ()) | |
4394 | { | |
4395 | sortText = message (": %s", cstring_fromChars (lsymbol_toChars (sort_getLsymbol (sort)))); | |
4396 | sortSpace = cstring_makeLiteral (" "); | |
4397 | } | |
4398 | else | |
4399 | { | |
4400 | sortText = cstring_undefined; | |
4401 | sortSpace = cstring_undefined; | |
4402 | } | |
4403 | ||
4404 | switch (op->kind) | |
4405 | { | |
4406 | case OPF_IF: | |
4407 | { | |
4408 | int size = termNodeList_size (args); | |
4409 | ||
4410 | if (size == 3) | |
4411 | { | |
4412 | s = message ("if %q then %q else %q\n", | |
4413 | termNode_unparse (termNodeList_getN (args, 0)), | |
4414 | termNode_unparse (termNodeList_getN (args, 1)), | |
4415 | termNode_unparse (termNodeList_getN (args, 2))); | |
4416 | } | |
4417 | else | |
4418 | { | |
4419 | WrongArity (op->tok, 3, size); | |
4420 | s = cstring_makeLiteral ("if __ then __ else __"); | |
4421 | } | |
4422 | s = message ("%q%s", s, sortText); | |
4423 | break; | |
4424 | } | |
4425 | case OPF_ANYOP: | |
4426 | { /* ymtan ? */ | |
4427 | s = message ("%s %s", | |
4428 | ltoken_getRawString (op->content.anyop), | |
4429 | sortText); | |
4430 | break; | |
4431 | } | |
4432 | case OPF_MANYOP: | |
4433 | { | |
4434 | int size = termNodeList_size (args); | |
4435 | ||
4436 | if (size == 1) | |
4437 | { | |
4438 | s = message ("%q ", termNode_unparse (termNodeList_head (args))); | |
4439 | } | |
4440 | else | |
4441 | { | |
4442 | WrongArity (op->content.anyop, 1, size); | |
4443 | s = cstring_makeLiteral ("__ "); | |
4444 | } | |
4445 | s = message ("%q%s%s", s, ltoken_getRawString (op->content.anyop), | |
4446 | sortText); | |
4447 | break; | |
4448 | } | |
4449 | case OPF_ANYOPM: | |
4450 | { | |
4451 | int size = termNodeList_size (args); | |
4452 | ||
4453 | s = message ("%s ", ltoken_getRawString (op->content.anyop)); | |
4454 | ||
4455 | if (size == 1) | |
4456 | { | |
4457 | s = message ("%q%q", s, termNode_unparse (termNodeList_head (args))); | |
4458 | } | |
4459 | else | |
4460 | { | |
4461 | WrongArity (op->content.anyop, 1, size); | |
4462 | s = message ("%q__", s); | |
4463 | } | |
4464 | s = message ("%q%s", s, sortText); | |
4465 | break; | |
4466 | } | |
4467 | case OPF_MANYOPM: | |
4468 | { | |
4469 | int size = termNodeList_size (args); | |
4470 | ||
4471 | if (size == 2) | |
4472 | { | |
4473 | s = message ("%q %s %q", | |
4474 | termNode_unparse (termNodeList_getN (args, 0)), | |
4475 | ltoken_getRawString (op->content.anyop), | |
4476 | termNode_unparse (termNodeList_getN (args, 1))); | |
4477 | } | |
4478 | else | |
4479 | { | |
4480 | WrongArity (op->content.anyop, 2, size); | |
4481 | s = message ("__ %s __", ltoken_getRawString (op->content.anyop)); | |
4482 | } | |
4483 | s = message ("%q%s", s, sortText); | |
4484 | break; | |
4485 | } | |
4486 | case OPF_MIDDLE: | |
4487 | { | |
4488 | int size = termNodeList_size (args); | |
4489 | int expect = op->content.middle; | |
4490 | ||
4491 | /* ymtan ? use { or openSym token ? */ | |
4492 | ||
4493 | if (size == expect) | |
4494 | { | |
4495 | s = message ("{%q}", termNodeList_unparse (args)); | |
4496 | } | |
4497 | else | |
4498 | { | |
4499 | WrongArity (op->tok, expect, size); | |
4500 | s = cstring_makeLiteral ("{ * }"); | |
4501 | } | |
4502 | ||
4503 | s = message ("%q%s", s, sortText); | |
11db3170 | 4504 | break; |
616915dd | 4505 | } |
4506 | case OPF_MMIDDLE: | |
4507 | { | |
4508 | int size = termNodeList_size (args); | |
4509 | int expect = op->content.middle + 1; | |
4510 | ||
4511 | if (size == expect) | |
4512 | { | |
4513 | s = message ("%q{%q}", | |
4514 | termNode_unparse (termNodeList_head (args)), | |
4515 | termNodeList_unparseTail (args)); | |
4516 | } | |
4517 | else | |
4518 | { | |
4519 | WrongArity (op->tok, expect, size); | |
4520 | s = cstring_makeLiteral ("__ { * }"); | |
4521 | } | |
4522 | ||
4523 | s = message ("%q%s", s, sortText); | |
4524 | break; | |
4525 | } | |
4526 | case OPF_MIDDLEM: | |
4527 | { | |
4528 | int size = termNodeList_size (args); | |
4529 | int expect = op->content.middle + 1; | |
4530 | ||
4531 | if (size == expect) | |
4532 | { | |
4533 | termNodeList_finish (args); | |
4534 | ||
4535 | s = message ("{%q}%s%s%q", | |
4536 | termNodeList_unparseToCurrent (args), | |
4537 | sortText, sortSpace, | |
4538 | termNode_unparse (termNodeList_current (args))); | |
4539 | } | |
4540 | else | |
4541 | { | |
4542 | WrongArity (op->tok, expect, size); | |
4543 | ||
4544 | s = message ("{ * }%s __", sortText); | |
4545 | ||
4546 | /* used to put in extra space! evs 94-01-05 */ | |
4547 | } | |
4548 | break; | |
4549 | } | |
4550 | case OPF_MMIDDLEM: | |
4551 | { | |
4552 | int size = termNodeList_size (args); | |
4553 | int expect = op->content.middle + 2; | |
4554 | ||
4555 | if (size == expect) | |
4556 | { | |
4557 | termNodeList_finish (args); | |
4558 | ||
4559 | s = message ("%q {%q} %s%s%q", | |
4560 | termNode_unparse (termNodeList_head (args)), | |
4561 | termNodeList_unparseSecondToCurrent (args), | |
4562 | sortText, sortSpace, | |
4563 | termNode_unparse (termNodeList_current (args))); | |
4564 | } | |
4565 | else | |
4566 | { | |
4567 | WrongArity (op->tok, expect, size); | |
4568 | s = message ("__ { * } %s __", sortText); | |
4569 | ||
4570 | /* also had extra space? */ | |
4571 | } | |
4572 | break; | |
4573 | } | |
4574 | case OPF_BMIDDLE: | |
4575 | { | |
4576 | int size = termNodeList_size (args); | |
4577 | int expect = op->content.middle; | |
4578 | ||
4579 | if (size == expect) | |
4580 | { | |
4581 | s = message ("[%q]", termNodeList_unparse (args)); | |
4582 | } | |
4583 | else | |
4584 | { | |
4585 | WrongArity (op->tok, expect, size); | |
4586 | s = cstring_makeLiteral ("[ * ]"); | |
4587 | } | |
4588 | s = message ("%q%s", s, sortText); | |
4589 | break; | |
4590 | } | |
4591 | case OPF_BMMIDDLE: | |
4592 | { | |
4593 | int size = termNodeList_size (args); | |
4594 | int expect = op->content.middle + 1; | |
4595 | ||
4596 | if (size == expect) | |
4597 | { | |
4598 | s = message ("%q[%q]", | |
4599 | termNode_unparse (termNodeList_head (args)), | |
4600 | termNodeList_unparseTail (args)); | |
4601 | } | |
4602 | else | |
4603 | { | |
4604 | WrongArity (op->tok, expect, size); | |
4605 | s = cstring_makeLiteral ("__ [ * ]"); | |
4606 | } | |
4607 | ||
4608 | s = message ("%q%s", s, sortText); | |
4609 | break; | |
4610 | } | |
4611 | case OPF_BMMIDDLEM: | |
4612 | { | |
4613 | int size = termNodeList_size (args); | |
4614 | int expect = op->content.middle + 1; | |
4615 | ||
4616 | if (size == expect) | |
4617 | { | |
4618 | s = message ("%q[%q] __", | |
4619 | termNode_unparse (termNodeList_head (args)), | |
4620 | termNodeList_unparseTail (args)); | |
4621 | } | |
4622 | else | |
4623 | { | |
4624 | WrongArity (op->tok, expect, size); | |
4625 | s = cstring_makeLiteral ("__ [ * ] __"); | |
4626 | } | |
4627 | s = message ("%q%s", s, sortText); | |
4628 | break; | |
4629 | } | |
4630 | case OPF_BMIDDLEM: | |
4631 | { | |
4632 | int size = termNodeList_size (args); | |
4633 | int expect = op->content.middle + 1; | |
4634 | ||
4635 | if (size == expect) | |
4636 | { | |
4637 | termNodeList_finish (args); | |
4638 | ||
4639 | s = message ("[%q]%s%s%q", | |
4640 | termNodeList_unparseToCurrent (args), | |
4641 | sortText, sortSpace, | |
4642 | termNode_unparse (termNodeList_current (args))); | |
4643 | } | |
4644 | else | |
4645 | { | |
4646 | WrongArity (op->tok, expect, size); | |
4647 | s = cstring_makeLiteral ("[ * ] __"); | |
4648 | } | |
4649 | ||
4650 | break; | |
4651 | } | |
4652 | case OPF_SELECT: | |
4653 | { /* ymtan constant, check args ? */ | |
4654 | s = cstring_prependChar ('.', ltoken_getRawString (op->content.id)); | |
4655 | break; | |
4656 | } | |
4657 | case OPF_MAP: | |
4658 | s = cstring_concat (cstring_makeLiteralTemp ("->"), | |
4659 | ltoken_getRawString (op->content.id)); | |
4660 | break; | |
4661 | case OPF_MSELECT: | |
4662 | { | |
4663 | int size = termNodeList_size (args); | |
4664 | ||
4665 | if (size == 1) | |
4666 | { | |
4667 | s = message ("%q.%s", termNode_unparse (termNodeList_head (args)), | |
4668 | ltoken_getRawString (op->content.id)); | |
4669 | } | |
4670 | else | |
4671 | { | |
4672 | WrongArity (op->content.id, 1, size); | |
4673 | s = cstring_concat (cstring_makeLiteralTemp ("__."), | |
4674 | ltoken_getRawString (op->content.id)); | |
4675 | } | |
4676 | break; | |
4677 | } | |
4678 | case OPF_MMAP: | |
4679 | { | |
4680 | int size = termNodeList_size (args); | |
4681 | ||
4682 | if (size == 1) | |
4683 | { | |
4684 | s = message ("%q->%s", termNode_unparse (termNodeList_head (args)), | |
4685 | ltoken_getRawString (op->content.id)); | |
4686 | } | |
4687 | else | |
4688 | { | |
4689 | WrongArity (op->content.id, 1, size); | |
4690 | s = cstring_concat (cstring_makeLiteralTemp ("__->"), | |
4691 | ltoken_getRawString (op->content.id)); | |
4692 | } | |
4693 | break; | |
4694 | } | |
4695 | } | |
4696 | ||
4697 | cstring_free (sortSpace); | |
4698 | cstring_free (sortText); | |
4699 | return s; | |
4700 | } | |
4701 | return cstring_undefined; | |
4702 | } | |
4703 | ||
4704 | /*@only@*/ cstring | |
4705 | termNode_unparse (/*@null@*/ termNode n) | |
4706 | { | |
4707 | cstring s = cstring_undefined; | |
4708 | cstring back = cstring_undefined; | |
4709 | cstring front = cstring_undefined; | |
4710 | int count; | |
4711 | ||
4712 | if (n != (termNode) 0) | |
4713 | { | |
4714 | for (count = n->wrapped; count > 0; count--) | |
4715 | { | |
4716 | front = cstring_appendChar (front, '('); | |
4717 | back = cstring_appendChar (back, ')'); | |
4718 | } | |
4719 | ||
4720 | switch (n->kind) | |
4721 | { | |
4722 | case TRM_LITERAL: | |
4723 | case TRM_CONST: | |
4724 | case TRM_VAR: | |
4725 | case TRM_ZEROARY: | |
4726 | s = cstring_copy (ltoken_getRawString (n->literal)); | |
4727 | break; | |
4728 | case TRM_APPLICATION: | |
4729 | { | |
4730 | nameNode nn = n->name; | |
4731 | if (nn != (nameNode) 0) | |
4732 | { | |
4733 | if (nn->isOpId) | |
4734 | { | |
4735 | s = message ("%s (%q) ", | |
4736 | ltoken_getRawString (nn->content.opid), | |
4737 | termNodeList_unparse (n->args)); | |
4738 | /* must we handle n->given ? skip for now */ | |
4739 | } | |
4740 | else | |
4741 | { | |
4742 | s = message ("%q ", printTermNode2 (nn->content.opform, n->args, n->given)); | |
4743 | } | |
4744 | } | |
4745 | else | |
4746 | { | |
4747 | llfatalbug | |
4748 | (message ("termNode_unparse: expect non-empty nameNode: TRM_APPLICATION: %q", | |
4749 | nameNode_unparse (nn))); | |
4750 | } | |
4751 | break; | |
4752 | } | |
4753 | case TRM_UNCHANGEDALL: | |
4754 | s = cstring_makeLiteral ("unchanged (all)"); | |
4755 | break; | |
4756 | case TRM_UNCHANGEDOTHERS: | |
4757 | s = message ("unchanged (%q)", storeRefNodeList_unparse (n->unchanged)); | |
4758 | break; | |
4759 | case TRM_SIZEOF: | |
4760 | s = message ("sizeof (%q)", lclTypeSpecNode_unparse (n->sizeofField)); | |
4761 | break; | |
4762 | case TRM_QUANTIFIER: | |
4763 | { | |
4764 | quantifiedTermNode x = n->quantified; | |
4765 | s = message ("%q%s%q%s", | |
4766 | quantifierNodeList_unparse (x->quantifiers), | |
4767 | ltoken_getRawString (x->open), | |
4768 | termNode_unparse (x->body), | |
4769 | ltoken_getRawString (x->close)); | |
4770 | break; | |
4771 | } | |
4772 | } | |
4773 | } | |
4774 | return (message ("%q%q%q", front, s, back)); | |
4775 | } | |
4776 | ||
4777 | static void modifyNode_free (/*@null@*/ /*@only@*/ modifyNode m) | |
4778 | { | |
4779 | if (m != (modifyNode) 0) | |
4780 | { | |
4781 | ||
4782 | if (m->hasStoreRefList) | |
4783 | { | |
4784 | storeRefNodeList_free (m->list); | |
4785 | /*@-branchstate@*/ | |
4786 | } | |
4787 | /*@=branchstate@*/ | |
4788 | ||
4789 | ltoken_free (m->tok); | |
4790 | sfree (m); | |
4791 | } | |
4792 | } | |
4793 | ||
4794 | /*@only@*/ cstring | |
4795 | modifyNode_unparse (/*@null@*/ modifyNode m) | |
4796 | { | |
4797 | if (m != (modifyNode) 0) | |
4798 | { | |
4799 | if (m->hasStoreRefList) | |
4800 | { | |
4801 | return (message (" modifies %q; \n", storeRefNodeList_unparse (m->list))); | |
4802 | } | |
4803 | else | |
4804 | { | |
4805 | if (m->modifiesNothing) | |
4806 | { | |
4807 | return (cstring_makeLiteral ("modifies nothing; \n")); | |
4808 | } | |
4809 | else | |
4810 | { | |
4811 | return (cstring_makeLiteral ("modifies anything; \n")); | |
4812 | } | |
4813 | } | |
4814 | } | |
4815 | return cstring_undefined; | |
4816 | } | |
4817 | ||
4818 | /*@only@*/ cstring | |
4819 | programNode_unparse (programNode p) | |
4820 | { | |
4821 | if (p != (programNode) 0) | |
4822 | { | |
4823 | cstring s = cstring_undefined; | |
4824 | int count; | |
4825 | ||
4826 | switch (p->kind) | |
4827 | { | |
4828 | case ACT_SELF: | |
4829 | { | |
4830 | cstring back = cstring_undefined; | |
4831 | ||
4832 | for (count = p->wrapped; count > 0; count--) | |
4833 | { | |
4834 | s = cstring_appendChar (s, '('); | |
4835 | back = cstring_appendChar (back, ')'); | |
4836 | } | |
4837 | s = message ("%q%q%q", s, stmtNode_unparse (p->content.self), back); | |
4838 | break; | |
4839 | } | |
4840 | case ACT_ITER: | |
4841 | s = message ("*(%q)", programNodeList_unparse (p->content.args)); | |
4842 | break; | |
4843 | case ACT_ALTERNATE: | |
4844 | s = message ("|(%q)", programNodeList_unparse (p->content.args)); | |
4845 | break; | |
4846 | case ACT_SEQUENCE: | |
4847 | s = programNodeList_unparse (p->content.args); | |
4848 | break; | |
4849 | } | |
4850 | ||
4851 | return s; | |
4852 | } | |
4853 | return cstring_undefined; | |
4854 | } | |
4855 | ||
4856 | /*@only@*/ cstring | |
4857 | stmtNode_unparse (stmtNode x) | |
4858 | { | |
4859 | cstring s = cstring_undefined; | |
4860 | ||
4861 | if (x != (stmtNode) 0) | |
4862 | { | |
4863 | if (ltoken_isValid (x->lhs)) | |
4864 | { | |
4865 | s = cstring_concat (ltoken_getRawString (x->lhs), | |
4866 | cstring_makeLiteralTemp (" = ")); | |
4867 | } | |
4868 | ||
4869 | s = message ("%q%s (%q)", s, | |
4870 | ltoken_getRawString (x->operator), | |
4871 | termNodeList_unparse (x->args)); | |
4872 | } | |
4873 | ||
4874 | return s; | |
4875 | } | |
4876 | ||
4877 | /*@only@*/ lslOp | |
4878 | makelslOpNode (/*@only@*/ /*@null@*/ nameNode name, | |
4879 | /*@dependent@*/ sigNode s) | |
4880 | { | |
4881 | lslOp x = (lslOp) dmalloc (sizeof (*x)); | |
4882 | ||
4883 | x->name = name; | |
4884 | x->signature = s; | |
4885 | ||
4886 | /* enter operator info into symtab */ | |
4887 | /* if not, they may need to be renamed in LCL imports */ | |
4888 | ||
4889 | if (g_lslParsingTraits) | |
4890 | { | |
4891 | if (name != NULL) | |
4892 | { | |
4893 | symtable_enterOp (g_symtab, nameNode_copySafe (name), sigNode_copy (s)); | |
4894 | } | |
4895 | } | |
4896 | else | |
4897 | { | |
4898 | /* nameNode_free (name); */ /* YIKES! */ | |
4899 | } | |
4900 | ||
4901 | return x; | |
4902 | } | |
4903 | ||
4904 | /*@only@*/ cstring | |
4905 | lslOp_unparse (lslOp x) | |
4906 | { | |
4907 | char *s = mstring_createEmpty (); | |
4908 | ||
4909 | if (x != (lslOp) 0) | |
4910 | { | |
4911 | s = mstring_concatFree (s, cstring_toCharsSafe (nameNode_unparse (x->name))); | |
4912 | ||
4913 | if (x->signature != (sigNode) 0) | |
4914 | { | |
4915 | s = mstring_concatFree (s, cstring_toCharsSafe (sigNode_unparse (x->signature))); | |
4916 | } | |
4917 | } | |
4918 | ||
4919 | return cstring_fromCharsO (s); | |
4920 | } | |
4921 | ||
4922 | static bool | |
4923 | sameOpFormNode (/*@null@*/ opFormNode n1, /*@null@*/ opFormNode n2) | |
4924 | { | |
4925 | if (n1 == n2) | |
4926 | return TRUE; | |
4927 | ||
4928 | if (n1 == 0) | |
4929 | return FALSE; | |
4930 | ||
4931 | if (n2 == 0) | |
4932 | return FALSE; | |
4933 | ||
4934 | if (n1->kind == n2->kind) | |
4935 | { | |
4936 | switch (n1->kind) | |
4937 | { | |
4938 | case OPF_IF: | |
4939 | return TRUE; | |
4940 | case OPF_ANYOP: | |
4941 | case OPF_MANYOP: | |
4942 | case OPF_ANYOPM: | |
4943 | return (ltoken_similar (n1->content.anyop, n2->content.anyop)); | |
4944 | case OPF_MANYOPM: | |
4945 | { | |
4946 | /* want to treat eq and = the same */ | |
4947 | return ltoken_similar (n1->content.anyop, n2->content.anyop); | |
4948 | } | |
4949 | case OPF_MIDDLE: | |
4950 | case OPF_MMIDDLE: | |
4951 | case OPF_MIDDLEM: | |
4952 | case OPF_MMIDDLEM: | |
4953 | /* need to check the rawText of openSym and closeSym */ | |
4954 | if ((int) n1->content.middle == (int) n2->content.middle) | |
4955 | { | |
4956 | if (lsymbol_equal (ltoken_getRawText (n1->tok), | |
4957 | ltoken_getRawText (n2->tok)) && | |
4958 | lsymbol_equal (ltoken_getRawText (n1->close), | |
4959 | ltoken_getRawText (n2->close))) | |
4960 | return TRUE; | |
4961 | } | |
4962 | return FALSE; | |
4963 | case OPF_BMIDDLE: | |
4964 | case OPF_BMMIDDLE: | |
4965 | case OPF_BMIDDLEM: | |
4966 | case OPF_BMMIDDLEM: | |
4967 | return ((int) n1->content.middle == (int) n2->content.middle); | |
4968 | case OPF_SELECT: | |
4969 | case OPF_MAP: | |
4970 | case OPF_MSELECT: | |
4971 | case OPF_MMAP: | |
4972 | return (ltoken_similar (n1->content.id, n2->content.id)); | |
4973 | } | |
4974 | } | |
4975 | return FALSE; | |
4976 | } | |
4977 | ||
4978 | bool | |
4979 | sameNameNode (/*@null@*/ nameNode n1, /*@null@*/ nameNode n2) | |
4980 | { | |
4981 | if (n1 == n2) | |
4982 | return TRUE; | |
4983 | if (n1 != (nameNode) 0 && n2 != (nameNode) 0) | |
4984 | { | |
4985 | if (bool_equal (n1->isOpId, n2->isOpId)) | |
4986 | { | |
4987 | if (n1->isOpId) | |
4988 | return (ltoken_similar (n1->content.opid, n2->content.opid)); | |
4989 | else | |
4990 | return sameOpFormNode (n1->content.opform, | |
4991 | n2->content.opform); | |
4992 | } | |
4993 | } | |
4994 | return FALSE; | |
4995 | } | |
4996 | ||
4997 | void CTypesNode_free (/*@only@*/ /*@null@*/ CTypesNode x) | |
4998 | { | |
4999 | if (x != NULL) | |
5000 | { | |
5001 | ltokenList_free (x->ctypes); | |
5002 | sfree (x); | |
5003 | } | |
5004 | } | |
5005 | ||
5006 | /*@null@*/ CTypesNode CTypesNode_copy (/*@null@*/ CTypesNode x) | |
5007 | { | |
5008 | if (x != NULL) | |
5009 | { | |
5010 | CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode)); | |
5011 | newnode->intfield = x->intfield; | |
5012 | newnode->ctypes = ltokenList_copy (x->ctypes); | |
5013 | newnode->sort = x->sort; | |
5014 | ||
5015 | return newnode; | |
5016 | } | |
5017 | else | |
5018 | { | |
5019 | return NULL; | |
5020 | } | |
5021 | } | |
5022 | ||
5023 | /*@only@*/ CTypesNode | |
5024 | makeCTypesNode (/*@only@*/ CTypesNode ctypes, ltoken ct) | |
5025 | { | |
5026 | /*@only@*/ CTypesNode newnode; | |
5027 | lsymbol sortname; | |
5028 | bits sortbits; | |
5029 | ||
5030 | if (ctypes == (CTypesNode) NULL) | |
5031 | { | |
5032 | newnode = (CTypesNode) dmalloc (sizeof (*newnode)); | |
5033 | newnode->intfield = 0; | |
5034 | newnode->ctypes = ltokenList_new (); | |
5035 | newnode->sort = sort_makeNoSort (); | |
5036 | } | |
5037 | else | |
5038 | { | |
5039 | newnode = ctypes; | |
5040 | } | |
5041 | ||
5042 | if ((ltoken_getIntField (ct) & newnode->intfield) != 0) | |
5043 | { | |
5044 | lclerror (ct, | |
5045 | message | |
5046 | ("Duplicate type specifier ignored: %s", | |
5047 | cstring_fromChars | |
5048 | (lsymbol_toChars | |
5049 | (lclctype_toSortDebug (ltoken_getIntField (ct)))))); | |
5050 | ||
5051 | /* evs --- don't know how to generator this error */ | |
5052 | ||
5053 | /* Use previous value, to keep things consistent */ | |
5054 | ltoken_free (ct); | |
5055 | return newnode; | |
5056 | } | |
5057 | ||
5058 | sortbits = newnode->intfield | ltoken_getIntField (ct); | |
5059 | sortname = lclctype_toSort (sortbits); | |
5060 | ||
5061 | if (sortname == lsymbol_fromChars ("error")) | |
5062 | { | |
5063 | lclerror (ct, cstring_makeLiteral ("Invalid combination of type specifiers")); | |
5064 | } | |
5065 | else | |
5066 | { | |
5067 | newnode->intfield = sortbits; | |
5068 | } | |
5069 | ||
5070 | ltokenList_addh (newnode->ctypes, ct); | |
5071 | ||
5072 | /* | |
5073 | ** Sorts are assigned after CTypesNode is created during parsing, | |
5074 | ** see bison grammar. | |
5075 | */ | |
5076 | ||
5077 | return newnode; | |
5078 | } | |
5079 | ||
5080 | /*@only@*/ CTypesNode | |
5081 | makeTypeSpecifier (ltoken typedefname) | |
5082 | { | |
5083 | CTypesNode newnode = (CTypesNode) dmalloc (sizeof (*newnode)); | |
5084 | typeInfo ti = symtable_typeInfo (g_symtab, ltoken_getText (typedefname)); | |
5085 | ||
5086 | newnode->intfield = 0; | |
5087 | newnode->ctypes = ltokenList_singleton (ltoken_copy (typedefname)); | |
5088 | ||
5089 | /* if we see "bool" include bool.h header file */ | |
5090 | ||
5091 | if (ltoken_getText (typedefname) == lsymbol_bool) | |
5092 | { | |
5093 | lhIncludeBool (); | |
5094 | } | |
5095 | ||
5096 | if (typeInfo_exists (ti)) | |
5097 | { | |
28bf4b0b | 5098 | /* must we be concern about whether this type is exported by module? |
5099 | No. Because all typedef's are exported. No hiding supported. */ | |
5100 | /* Later, may want to keep types around too */ | |
5101 | /* 3/2/93, use underlying sort */ | |
616915dd | 5102 | newnode->sort = sort_getUnderlying (ti->basedOn); |
5103 | } | |
5104 | else | |
5105 | { | |
5106 | lclerror (typedefname, message ("Unrecognized type: %s", | |
5107 | ltoken_getRawString (typedefname))); | |
5108 | /* evs --- Don't know how to get this message */ | |
28bf4b0b | 5109 | |
616915dd | 5110 | newnode->sort = sort_makeNoSort (); |
5111 | } | |
5112 | ||
5113 | ltoken_free (typedefname); | |
5114 | return newnode; | |
5115 | } | |
5116 | ||
5117 | bool sigNode_equal (sigNode n1, sigNode n2) | |
5118 | { | |
5119 | /* n1 and n2 are never 0 */ | |
5120 | ||
5121 | return ((n1 == n2) || | |
5122 | (n1->key == n2->key && | |
5123 | ltoken_similar (n1->range, n2->range) && | |
5124 | ltokenList_equal (n1->domain, n2->domain))); | |
5125 | } | |
5126 | ||
5127 | sort | |
5128 | typeExpr2ptrSort (sort base, /*@null@*/ typeExpr t) | |
5129 | { | |
5130 | if (t != (typeExpr) 0) | |
5131 | { | |
5132 | switch (t->kind) | |
5133 | { | |
5134 | case TEXPR_BASE: | |
5135 | return base; | |
5136 | case TEXPR_PTR: | |
5137 | return typeExpr2ptrSort (sort_makePtr (ltoken_undefined, base), | |
5138 | t->content.pointer); | |
5139 | case TEXPR_ARRAY: | |
5140 | return typeExpr2ptrSort (sort_makeArr (ltoken_undefined, base), | |
5141 | t->content.array.elementtype); | |
5142 | case TEXPR_FCN: | |
5143 | /* map all hof types to some sort of SRT_HOF */ | |
5144 | return sort_makeHOFSort (base); | |
5145 | } | |
5146 | } | |
5147 | return base; | |
5148 | } | |
5149 | ||
5150 | static sort | |
5151 | typeExpr2returnSort (sort base, /*@null@*/ typeExpr t) | |
5152 | { | |
5153 | if (t != (typeExpr) 0) | |
5154 | { | |
5155 | switch (t->kind) | |
5156 | { | |
5157 | case TEXPR_BASE: | |
5158 | return base; | |
5159 | case TEXPR_PTR: | |
5160 | return typeExpr2returnSort (sort_makePtr (ltoken_undefined, base), | |
5161 | t->content.pointer); | |
5162 | case TEXPR_ARRAY: | |
5163 | return typeExpr2returnSort (sort_makeArr (ltoken_undefined, base), | |
5164 | t->content.array.elementtype); | |
5165 | case TEXPR_FCN: | |
5166 | return typeExpr2returnSort (base, t->content.function.returntype); | |
5167 | } | |
5168 | } | |
5169 | return base; | |
5170 | } | |
5171 | ||
5172 | sort | |
5173 | lclTypeSpecNode2sort (lclTypeSpecNode type) | |
5174 | { | |
5175 | if (type != (lclTypeSpecNode) 0) | |
5176 | { | |
5177 | switch (type->kind) | |
5178 | { | |
5179 | case LTS_TYPE: | |
5180 | llassert (type->content.type != NULL); | |
5181 | return sort_makePtrN (type->content.type->sort, type->pointers); | |
5182 | case LTS_STRUCTUNION: | |
5183 | llassert (type->content.structorunion != NULL); | |
f9264521 | 5184 | return sort_makePtrN (type->content.structorunion->sort, type->pointers); |
616915dd | 5185 | case LTS_ENUM: |
5186 | llassert (type->content.enumspec != NULL); | |
f9264521 | 5187 | return sort_makePtrN (type->content.enumspec->sort, type->pointers); |
616915dd | 5188 | case LTS_CONJ: |
5189 | return (lclTypeSpecNode2sort (type->content.conj->a)); | |
5190 | } | |
5191 | } | |
5192 | return (sort_makeNoSort ()); | |
5193 | } | |
5194 | ||
5195 | lsymbol | |
5196 | checkAndEnterTag (tagKind k, ltoken opttagid) | |
5197 | { | |
5198 | /* should be tagKind, instead of int */ | |
5199 | tagInfo t; | |
5200 | sort sort = sort_makeNoSort (); | |
5201 | ||
5202 | if (!ltoken_isUndefined (opttagid)) | |
5203 | { | |
5204 | switch (k) | |
5205 | { | |
5206 | case TAG_FWDSTRUCT: | |
5207 | case TAG_STRUCT: | |
5208 | sort = sort_makeStr (opttagid); | |
5209 | break; | |
5210 | case TAG_FWDUNION: | |
5211 | case TAG_UNION: | |
5212 | sort = sort_makeUnion (opttagid); | |
5213 | break; | |
5214 | case TAG_ENUM: | |
5215 | sort = sort_makeEnum (opttagid); | |
5216 | break; | |
5217 | } | |
5218 | ||
5219 | /* see if it is already in symbol table */ | |
5220 | t = symtable_tagInfo (g_symtab, ltoken_getText (opttagid)); | |
5221 | ||
5222 | if (tagInfo_exists (t)) | |
5223 | { | |
5224 | if (t->kind == TAG_FWDUNION || t->kind == TAG_FWDSTRUCT) | |
5225 | { | |
5226 | /* this is fine, for mutually recursive types */ | |
5227 | } | |
5228 | else | |
5229 | { /* this is not good, complain later */ | |
5230 | cstring s; | |
5231 | ||
5232 | switch (k) | |
5233 | { | |
5234 | case TAG_ENUM: | |
5235 | s = cstring_makeLiteral ("Enum"); | |
5236 | break; | |
5237 | case TAG_STRUCT: | |
5238 | case TAG_FWDSTRUCT: | |
5239 | s = cstring_makeLiteral ("Struct"); | |
5240 | break; | |
5241 | case TAG_UNION: | |
5242 | case TAG_FWDUNION: | |
5243 | s = cstring_makeLiteral ("Union"); | |
5244 | break; | |
5245 | } | |
5246 | ||
5247 | t->sort = sort; | |
5248 | t->kind = k; | |
5249 | lclerror (opttagid, | |
5250 | message ("Tag redefined: %q %s", s, | |
5251 | ltoken_getRawString (opttagid))); | |
5252 | ||
5253 | } | |
5254 | ||
5255 | ltoken_free (opttagid); | |
5256 | } | |
5257 | else | |
5258 | { | |
5259 | tagInfo newnode = (tagInfo) dmalloc (sizeof (*newnode)); | |
5260 | ||
5261 | newnode->sort = sort; | |
5262 | newnode->kind = k; | |
5263 | newnode->id = opttagid; | |
5264 | newnode->imported = FALSE; | |
5265 | newnode->content.decls = stDeclNodeList_new (); | |
5266 | ||
5267 | (void) symtable_enterTag (g_symtab, newnode); | |
5268 | } | |
5269 | } | |
5270 | ||
5271 | return sort_getLsymbol (sort); | |
5272 | } | |
5273 | ||
5274 | static sort | |
5275 | extractReturnSort (lclTypeSpecNode t, declaratorNode d) | |
5276 | { | |
5277 | sort sort; | |
5278 | sort = lclTypeSpecNode2sort (t); | |
5279 | sort = typeExpr2returnSort (sort, d->type); | |
5280 | return sort; | |
5281 | } | |
5282 | ||
5283 | void | |
5284 | signNode_free (/*@only@*/ signNode sn) | |
5285 | { | |
5286 | sortList_free (sn->domain); | |
5287 | ltoken_free (sn->tok); | |
5288 | sfree (sn); | |
5289 | } | |
5290 | ||
5291 | /*@only@*/ cstring | |
5292 | signNode_unparse (signNode sn) | |
5293 | { | |
5294 | cstring s = cstring_undefined; | |
5295 | ||
5296 | if (sn != (signNode) 0) | |
5297 | { | |
5298 | s = message (": %q -> %s", sortList_unparse (sn->domain), | |
5299 | sort_unparseName (sn->range)); | |
5300 | } | |
5301 | return s; | |
5302 | } | |
5303 | ||
5304 | static /*@only@*/ pairNodeList | |
5305 | globalList_toPairNodeList (globalList g) | |
5306 | { | |
5307 | /* expect list to be globals, drop private ones */ | |
5308 | pairNodeList result = pairNodeList_new (); | |
5309 | pairNode p; | |
5310 | declaratorNode vdnode; | |
5311 | lclTypeSpecNode type; | |
5312 | sort sort; | |
5313 | lsymbol sym; | |
5314 | initDeclNodeList decls; | |
5315 | ||
5316 | varDeclarationNodeList_elements (g, x) | |
5317 | { | |
5318 | if (x->isSpecial) | |
5319 | { | |
5320 | ; | |
5321 | } | |
5322 | else | |
5323 | { | |
5324 | if (x->isGlobal && !x->isPrivate) | |
5325 | { | |
5326 | type = x->type; | |
5327 | decls = x->decls; | |
5328 | ||
5329 | initDeclNodeList_elements (decls, init) | |
5330 | { | |
5331 | p = (pairNode) dmalloc (sizeof (*p)); | |
5332 | ||
5333 | vdnode = init->declarator; | |
5334 | sym = ltoken_getText (vdnode->id); | |
5335 | /* 2/21/93, not sure if it should be extractReturnSort, | |
5336 | or some call to typeExpr2ptrSort */ | |
5337 | sort = extractReturnSort (type, vdnode); | |
5338 | p->sort = sort_makeGlobal (sort); | |
5339 | /* if (!sort_isArrayKind (sort)) p->sort = sort_makeObj (sort); | |
5340 | else p->sort = sort; */ | |
5341 | /* p->name = sym; */ | |
5342 | p->tok = ltoken_copy (vdnode->id); | |
5343 | pairNodeList_addh (result, p); | |
5344 | } end_initDeclNodeList_elements; | |
5345 | } | |
5346 | } | |
5347 | } end_varDeclarationNodeList_elements; | |
5348 | return result; | |
5349 | } | |
5350 | ||
5351 | void | |
5352 | enteringFcnScope (lclTypeSpecNode t, declaratorNode d, globalList g) | |
5353 | { | |
5354 | scopeInfo si = (scopeInfo) dmalloc (sizeof (*si)); | |
5355 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
5356 | sort returnSort; | |
5357 | ltoken result = ltoken_copy (ltoken_id); | |
5358 | pairNodeList paramPairs, globals; | |
5359 | fctInfo fi = (fctInfo) dmalloc (sizeof (*fi)); | |
5360 | signNode sign = (signNode) dmalloc (sizeof (*sign)); | |
5361 | sortList domain = sortList_new (); | |
e5081f8c | 5362 | unsigned long int key; |
616915dd | 5363 | |
5364 | paramPairs = extractParams (d->type); | |
5365 | returnSort = extractReturnSort (t, d); | |
5366 | globals = globalList_toPairNodeList (g); | |
5367 | ||
5368 | sign->tok = ltoken_undefined; | |
5369 | sign->range = returnSort; | |
5370 | ||
5371 | key = MASH (0, sort_getLsymbol (returnSort)); | |
5372 | ||
5373 | pairNodeList_elements (paramPairs, p) | |
5374 | { | |
5375 | sortList_addh (domain, p->sort); | |
5376 | key = MASH (key, sort_getLsymbol (p->sort)); | |
5377 | } end_pairNodeList_elements; | |
5378 | ||
5379 | sign->domain = domain; | |
5380 | sign->key = key; | |
5381 | ||
5382 | /* push fcn onto symbol table stack first */ | |
5383 | fi->id = ltoken_copy (d->id); | |
5384 | fi->export = TRUE; | |
5385 | fi->signature = sign; | |
5386 | fi->globals = globals; | |
5387 | ||
5388 | (void) symtable_enterFct (g_symtab, fi); | |
5389 | ||
5390 | /* push new fcn scope */ | |
5391 | si->kind = SPE_FCN; | |
5392 | symtable_enterScope (g_symtab, si); | |
5393 | ||
5394 | /* add "result" with return type to current scope */ | |
5395 | ltoken_setText (result, lsymbol_fromChars ("result")); | |
5396 | ||
5397 | vi->id = result; | |
5398 | vi->sort = sort_makeFormal (returnSort); /* make appropriate values */ | |
5399 | vi->kind = VRK_PARAM; | |
5400 | vi->export = TRUE; | |
5401 | ||
5402 | (void) symtable_enterVar (g_symtab, vi); | |
5403 | ||
5404 | /* | |
5405 | ** evs - 4 Mar 1995 | |
5406 | ** pust globals first (they are in outer scope) | |
5407 | */ | |
5408 | ||
5409 | /* push onto symbol table the global variables declared in this function, | |
5410 | together with their respective sorts */ | |
5411 | ||
5412 | pairNodeList_elements (globals, gl) | |
5413 | { | |
5414 | ltoken_free (vi->id); | |
5415 | vi->id = ltoken_copy (gl->tok); | |
5416 | vi->kind = VRK_GLOBAL; | |
5417 | vi->sort = gl->sort; | |
5418 | (void) symtable_enterVar (g_symtab, vi); | |
5419 | } end_pairNodeList_elements; | |
5420 | ||
5421 | /* | |
5422 | ** could enter a new scope; instead, warn when variable shadows global | |
5423 | ** that is used | |
5424 | */ | |
5425 | ||
5426 | /* | |
5427 | ** push onto symbol table the formal parameters of this function, | |
5428 | ** together with their respective sorts | |
5429 | */ | |
5430 | ||
5431 | pairNodeList_elements (paramPairs, pair) | |
5432 | { | |
5433 | ltoken_free (vi->id); | |
5434 | vi->id = ltoken_copy (pair->tok); | |
5435 | vi->sort = pair->sort; | |
5436 | vi->kind = VRK_PARAM; | |
5437 | (void) symtable_enterVar (g_symtab, vi); | |
5438 | } end_pairNodeList_elements; | |
5439 | ||
5440 | pairNodeList_free (paramPairs); | |
5441 | varInfo_free (vi); | |
5442 | } | |
5443 | ||
5444 | void | |
5445 | enteringClaimScope (paramNodeList params, globalList g) | |
5446 | { | |
5447 | scopeInfo si = (scopeInfo) dmalloc (sizeof (*si)); | |
5448 | pairNodeList globals; | |
5449 | lclTypeSpecNode paramtype; | |
5450 | typeExpr paramdecl; | |
5451 | sort sort; | |
5452 | ||
5453 | globals = globalList_toPairNodeList (g); | |
5454 | /* push new claim scope */ | |
5455 | si->kind = SPE_CLAIM; | |
5456 | ||
5457 | symtable_enterScope (g_symtab, si); | |
5458 | ||
5459 | /* push onto symbol table the formal parameters of this function, | |
5460 | together with their respective sorts */ | |
5461 | ||
5462 | paramNodeList_elements (params, param) | |
5463 | { | |
5464 | paramdecl = param->paramdecl; | |
5465 | paramtype = param->type; | |
5466 | if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0) | |
5467 | { | |
5468 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
5469 | ||
5470 | sort = lclTypeSpecNode2sort (paramtype); | |
5471 | sort = sort_makeFormal (sort); | |
5472 | vi->sort = typeExpr2ptrSort (sort, paramdecl); | |
5473 | vi->id = ltoken_copy (extractDeclarator (paramdecl)); | |
5474 | vi->kind = VRK_PARAM; | |
5475 | vi->export = TRUE; | |
5476 | ||
5477 | (void) symtable_enterVar (g_symtab, vi); | |
5478 | varInfo_free (vi); | |
5479 | } | |
5480 | } end_paramNodeList_elements; | |
5481 | ||
5482 | /* push onto symbol table the global variables declared in this function, | |
5483 | together with their respective sorts */ | |
5484 | ||
5485 | pairNodeList_elements (globals, g2) | |
5486 | { | |
5487 | varInfo vi = (varInfo) dmalloc (sizeof (*vi)); | |
5488 | ||
5489 | vi->id = ltoken_copy (g2->tok); | |
5490 | vi->kind = VRK_GLOBAL; | |
5491 | vi->sort = g2->sort; | |
5492 | vi->export = TRUE; | |
5493 | ||
5494 | /* should catch duplicates in formals */ | |
5495 | (void) symtable_enterVar (g_symtab, vi); | |
5496 | varInfo_free (vi); | |
5497 | } end_pairNodeList_elements; | |
5498 | ||
5499 | pairNodeList_free (globals); | |
5500 | /* should not free it here! ltoken_free (claimId); @*/ | |
5501 | } | |
5502 | ||
5503 | static /*@only@*/ pairNodeList | |
5504 | extractParams (/*@null@*/ typeExpr te) | |
5505 | { | |
5506 | /* extract the parameters from a function header declarator's typeExpr */ | |
5507 | sort sort; | |
5508 | typeExpr paramdecl; | |
5509 | paramNodeList params; | |
5510 | lclTypeSpecNode paramtype; | |
5511 | pairNodeList head = pairNodeList_new (); | |
5512 | pairNode pair; | |
5513 | ||
5514 | if (te != (typeExpr) 0) | |
5515 | { | |
5516 | params = typeExpr_toParamNodeList (te); | |
5517 | if (paramNodeList_isDefined (params)) | |
5518 | { | |
5519 | paramNodeList_elements (params, param) | |
5520 | { | |
5521 | paramdecl = param->paramdecl; | |
5522 | paramtype = param->type; | |
5523 | if (paramdecl != (typeExpr) 0 && paramtype != (lclTypeSpecNode) 0) | |
5524 | { | |
5525 | pair = (pairNode) dmalloc (sizeof (*pair)); | |
5526 | sort = lclTypeSpecNode2sort (paramtype); | |
5527 | /* 2/17/93, was sort_makeVal (sort) */ | |
5528 | sort = sort_makeFormal (sort); | |
5529 | pair->sort = typeExpr2ptrSort (sort, paramdecl); | |
5530 | /* pair->name = ltoken_getText (extractDeclarator (paramdecl)); */ | |
5531 | pair->tok = ltoken_copy (extractDeclarator (paramdecl)); | |
5532 | pairNodeList_addh (head, pair); | |
5533 | } | |
5534 | } end_paramNodeList_elements; | |
5535 | } | |
5536 | } | |
5537 | return head; | |
5538 | } | |
5539 | ||
5540 | sort | |
5541 | sigNode_rangeSort (sigNode sig) | |
5542 | { | |
5543 | if (sig == (sigNode) 0) | |
5544 | { | |
5545 | return sort_makeNoSort (); | |
5546 | } | |
5547 | else | |
5548 | { | |
5549 | return sort_fromLsymbol (ltoken_getText (sig->range)); | |
5550 | } | |
5551 | } | |
5552 | ||
5553 | /*@only@*/ sortList | |
5554 | sigNode_domain (sigNode sig) | |
5555 | { | |
5556 | sortList domain = sortList_new (); | |
5557 | ||
5558 | if (sig == (sigNode) 0) | |
5559 | { | |
5560 | ; | |
5561 | } | |
5562 | else | |
5563 | { | |
5564 | ltokenList dom = sig->domain; | |
5565 | ||
5566 | ltokenList_elements (dom, tok) | |
5567 | { | |
5568 | sortList_addh (domain, sort_fromLsymbol (ltoken_getText (tok))); | |
5569 | } end_ltokenList_elements; | |
5570 | } | |
5571 | ||
5572 | return domain; | |
5573 | } | |
5574 | ||
5575 | opFormUnion | |
5576 | opFormUnion_createAnyOp (/*@temp@*/ ltoken t) | |
5577 | { | |
5578 | opFormUnion u; | |
5579 | ||
5580 | /* do not distinguish between .anyop and .id */ | |
5581 | u.anyop = t; | |
5582 | return u; | |
5583 | } | |
5584 | ||
5585 | opFormUnion | |
5586 | opFormUnion_createMiddle (int middle) | |
5587 | { | |
5588 | opFormUnion u; | |
5589 | ||
5590 | u.middle = middle; | |
5591 | return u; | |
5592 | } | |
5593 | ||
5594 | paramNode | |
5595 | markYieldParamNode (paramNode p) | |
5596 | { | |
5597 | p->kind = PYIELD; | |
5598 | ||
5599 | llassert (p->type != NULL); | |
5600 | p->type->quals = qualList_add (p->type->quals, qual_createYield ()); | |
5601 | ||
5602 | return (p); | |
5603 | } | |
5604 | ||
5605 | /*@only@*/ lclTypeSpecNode | |
5606 | lclTypeSpecNode_copySafe (lclTypeSpecNode n) | |
5607 | { | |
5608 | lclTypeSpecNode ret = lclTypeSpecNode_copy (n); | |
5609 | ||
5610 | llassert (ret != NULL); | |
5611 | return ret; | |
5612 | } | |
5613 | ||
5614 | /*@null@*/ /*@only@*/ lclTypeSpecNode | |
5615 | lclTypeSpecNode_copy (/*@null@*/ lclTypeSpecNode n) | |
5616 | { | |
5617 | if (n != NULL) | |
5618 | { | |
5619 | switch (n->kind) | |
5620 | { | |
5621 | case LTS_CONJ: | |
5622 | return (makeLclTypeSpecNodeConj (lclTypeSpecNode_copy (n->content.conj->a), | |
5623 | lclTypeSpecNode_copy (n->content.conj->b))); | |
5624 | case LTS_TYPE: | |
5625 | return (makeLclTypeSpecNodeType (CTypesNode_copy (n->content.type))); | |
5626 | case LTS_STRUCTUNION: | |
5627 | return (makeLclTypeSpecNodeSU (strOrUnionNode_copy (n->content.structorunion))); | |
5628 | case LTS_ENUM: | |
5629 | return (makeLclTypeSpecNodeEnum (enumSpecNode_copy (n->content.enumspec))); | |
5630 | } | |
5631 | } | |
5632 | ||
5633 | return NULL; | |
5634 | } | |
5635 | ||
5636 | void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode n) | |
5637 | { | |
5638 | if (n != NULL) | |
5639 | { | |
5640 | switch (n->kind) | |
5641 | { | |
5642 | case LTS_CONJ: | |
5643 | lclTypeSpecNode_free (n->content.conj->a); | |
5644 | lclTypeSpecNode_free (n->content.conj->b); | |
5645 | break; | |
5646 | case LTS_TYPE: | |
5647 | CTypesNode_free (n->content.type); | |
5648 | break; | |
5649 | case LTS_STRUCTUNION: | |
5650 | strOrUnionNode_free (n->content.structorunion); | |
5651 | break; | |
5652 | case LTS_ENUM: | |
5653 | enumSpecNode_free (n->content.enumspec); | |
5654 | break; | |
5655 | } | |
5656 | ||
5657 | qualList_free (n->quals); | |
5658 | sfree (n); | |
5659 | } | |
5660 | } | |
5661 | ||
5662 | static /*@null@*/ opFormNode opFormNode_copy (/*@null@*/ opFormNode op) | |
5663 | { | |
5664 | if (op != NULL) | |
5665 | { | |
5666 | opFormNode ret = (opFormNode) dmalloc (sizeof (*ret)); | |
5667 | ||
5668 | ret->tok = ltoken_copy (op->tok); | |
5669 | ret->kind = op->kind; | |
5670 | ret->content = op->content; | |
5671 | ret->key = op->key; | |
5672 | ret->close = ltoken_copy (op->close); | |
5673 | ||
5674 | return ret; | |
5675 | } | |
5676 | else | |
5677 | { | |
5678 | return NULL; | |
5679 | } | |
5680 | } | |
5681 | ||
5682 | void opFormNode_free (/*@null@*/ opFormNode op) | |
5683 | { | |
28bf4b0b | 5684 | if (op != NULL) |
5685 | { | |
5686 | ltoken_free (op->tok); | |
5687 | ltoken_free (op->close); | |
5688 | sfree (op); | |
5689 | } | |
616915dd | 5690 | } |
5691 | ||
5692 | void nameNode_free (nameNode n) | |
5693 | { | |
5694 | ||
5695 | if (n != NULL) | |
5696 | { | |
5697 | if (!n->isOpId) | |
5698 | { | |
5699 | opFormNode_free (n->content.opform); | |
5700 | } | |
5701 | ||
5702 | sfree (n); | |
5703 | } | |
5704 | } | |
5705 | ||
5706 | bool | |
5707 | lslOp_equal (lslOp x, lslOp y) | |
5708 | { | |
5709 | return ((x == y) || | |
5710 | ((x != 0) && (y != 0) && | |
5711 | sameNameNode (x->name, y->name) && | |
5712 | sigNode_equal (x->signature, y->signature))); | |
5713 | } | |
5714 | ||
5715 | void lslOp_free (lslOp x) | |
5716 | { | |
5717 | nameNode_free (x->name); | |
5718 | sfree (x); | |
5719 | } | |
5720 | ||
5721 | void sigNode_free (sigNode x) | |
5722 | { | |
5723 | if (x != NULL) | |
5724 | { | |
5725 | ltokenList_free (x->domain); | |
5726 | ltoken_free (x->tok); | |
5727 | ltoken_free (x->range); | |
5728 | sfree (x); | |
5729 | } | |
5730 | } | |
5731 | ||
5732 | void declaratorNode_free (/*@null@*/ /*@only@*/ declaratorNode x) | |
5733 | { | |
5734 | if (x != NULL) | |
5735 | { | |
5736 | typeExpr_free (x->type); | |
5737 | ltoken_free (x->id); | |
5738 | sfree (x); | |
5739 | } | |
5740 | } | |
5741 | ||
5742 | void abstBodyNode_free (/*@null@*/ /*@only@*/ abstBodyNode n) | |
5743 | { | |
5744 | if (n != NULL) | |
5745 | { | |
5746 | lclPredicateNode_free (n->typeinv); | |
5747 | fcnNodeList_free (n->fcns); | |
5748 | ltoken_free (n->tok); | |
5749 | sfree (n); | |
5750 | } | |
5751 | } | |
5752 | ||
5753 | void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode f) | |
5754 | { | |
5755 | if (f != NULL) | |
5756 | { | |
5757 | lclTypeSpecNode_free (f->typespec); | |
5758 | declaratorNode_free (f->declarator); | |
5759 | globalList_free (f->globals); | |
5760 | varDeclarationNodeList_free (f->inits); | |
5761 | letDeclNodeList_free (f->lets); | |
5762 | lclPredicateNode_free (f->checks); | |
5763 | lclPredicateNode_free (f->require); | |
5764 | lclPredicateNode_free (f->claim); | |
5765 | lclPredicateNode_free (f->ensures); | |
5766 | modifyNode_free (f->modify); | |
5767 | ltoken_free (f->name); | |
5768 | sfree (f); | |
5769 | } | |
5770 | } | |
5771 | ||
5772 | void declaratorInvNode_free (/*@null@*/ /*@only@*/ declaratorInvNode x) | |
5773 | { | |
5774 | if (x != NULL) | |
5775 | { | |
5776 | declaratorNode_free (x->declarator); | |
5777 | abstBodyNode_free (x->body); | |
5778 | sfree (x); | |
5779 | } | |
5780 | } | |
5781 | ||
5782 | /*@only@*/ lslOp lslOp_copy (lslOp x) | |
5783 | { | |
5784 | return (makelslOpNode (nameNode_copy (x->name), x->signature)); | |
5785 | } | |
5786 | ||
5787 | sigNode sigNode_copy (sigNode s) | |
5788 | { | |
5789 | llassert (s != NULL); | |
5790 | return (makesigNode (ltoken_copy (s->tok), | |
5791 | ltokenList_copy (s->domain), | |
5792 | ltoken_copy (s->range))); | |
5793 | } | |
5794 | ||
5795 | /*@null@*/ nameNode nameNode_copy (/*@null@*/ nameNode n) | |
5796 | { | |
5797 | if (n == NULL) return NULL; | |
5798 | return nameNode_copySafe (n); | |
5799 | } | |
5800 | ||
5801 | nameNode nameNode_copySafe (nameNode n) | |
5802 | { | |
5803 | if (n->isOpId) | |
5804 | { | |
5805 | return (makeNameNodeId (ltoken_copy (n->content.opid))); | |
5806 | } | |
5807 | else | |
5808 | { | |
1b8ae690 | 5809 | /* error should be detected by splint: forgot to copy opform! */ |
616915dd | 5810 | return (makeNameNodeForm (opFormNode_copy (n->content.opform))); |
5811 | } | |
5812 | } | |
5813 | ||
5814 | bool initDeclNode_isRedeclaration (initDeclNode d) | |
5815 | { | |
5816 | return (d->declarator->isRedecl); | |
5817 | } | |
5818 | ||
5819 | void termNode_free (/*@only@*/ /*@null@*/ termNode t) | |
5820 | { | |
28bf4b0b | 5821 | if (t != NULL) |
5822 | { | |
5823 | sortSet_free (t->possibleSorts); | |
5824 | lslOpSet_free (t->possibleOps); | |
5825 | nameNode_free (t->name); | |
5826 | termNodeList_free (t->args); | |
5827 | sfree (t); | |
5828 | } | |
616915dd | 5829 | } |
5830 | ||
5831 | /*@only@*/ termNode termNode_copySafe (termNode t) | |
5832 | { | |
5833 | termNode ret = termNode_copy (t); | |
5834 | ||
5835 | llassert (ret != NULL); | |
5836 | return ret; | |
5837 | } | |
5838 | ||
5839 | /*@null@*/ /*@only@*/ termNode termNode_copy (/*@null@*/ termNode t) | |
5840 | { | |
5841 | if (t != NULL) | |
5842 | { | |
5843 | termNode ret = (termNode) dmalloc (sizeof (*ret)); | |
5844 | ||
5845 | ret->wrapped = t->wrapped; | |
5846 | ret->kind = t->kind; | |
5847 | ret->sort = t->sort; | |
5848 | ret->given = t->given; | |
5849 | ret->possibleSorts = sortSet_copy (t->possibleSorts); | |
5850 | ret->error_reported = t->error_reported; | |
5851 | ret->possibleOps = lslOpSet_copy (t->possibleOps); | |
5852 | ret->name = nameNode_copy (t->name); | |
5853 | ret->args = termNodeList_copy (t->args); | |
5854 | ||
5855 | if (t->kind == TRM_LITERAL | |
5856 | || t->kind == TRM_SIZEOF | |
5857 | || t->kind == TRM_VAR | |
5858 | || t->kind == TRM_CONST | |
5859 | || t->kind == TRM_ZEROARY) | |
5860 | { | |
5861 | ret->literal = ltoken_copy (t->literal); | |
5862 | } | |
5863 | ||
5864 | if (t->kind == TRM_UNCHANGEDOTHERS) | |
5865 | { | |
5866 | ret->unchanged = storeRefNodeList_copy (t->unchanged); | |
5867 | } | |
5868 | ||
5869 | if (t->kind == TRM_QUANTIFIER) | |
5870 | { | |
5871 | ret->quantified = quantifiedTermNode_copy (t->quantified); | |
5872 | } | |
5873 | ||
5874 | if (t->kind == TRM_SIZEOF) | |
5875 | { | |
5876 | ret->sizeofField = lclTypeSpecNode_copySafe (t->sizeofField); | |
5877 | } | |
5878 | ||
5879 | return ret; | |
5880 | } | |
5881 | else | |
5882 | { | |
5883 | ||
5884 | return NULL; | |
5885 | } | |
5886 | } | |
5887 | ||
5888 | void importNode_free (/*@only@*/ /*@null@*/ importNode x) | |
5889 | { | |
28bf4b0b | 5890 | if (x != NULL) |
5891 | { | |
5892 | ltoken_free (x->val); | |
5893 | sfree (x); | |
5894 | } | |
616915dd | 5895 | } |
5896 | ||
5897 | void initDeclNode_free (/*@only@*/ /*@null@*/ initDeclNode x) | |
5898 | { | |
5899 | if (x != NULL) | |
5900 | { | |
5901 | declaratorNode_free (x->declarator); | |
5902 | termNode_free (x->value); | |
5903 | sfree (x); | |
5904 | } | |
5905 | } | |
5906 | ||
5907 | void letDeclNode_free (/*@only@*/ /*@null@*/ letDeclNode x) | |
5908 | { | |
5909 | if (x != NULL) | |
5910 | { | |
5911 | lclTypeSpecNode_free (x->sortspec); | |
5912 | termNode_free (x->term); | |
5913 | ltoken_free (x->varid); | |
5914 | sfree (x); | |
5915 | } | |
5916 | } | |
5917 | ||
5918 | void pairNode_free (/*@only@*/ /*@null@*/ pairNode x) | |
5919 | { | |
28bf4b0b | 5920 | if (x != NULL) |
5921 | { | |
5922 | ltoken_free (x->tok); | |
5923 | sfree (x); | |
5924 | } | |
616915dd | 5925 | } |
5926 | ||
5927 | /*@null@*/ paramNode paramNode_copy (/*@null@*/ paramNode p) | |
5928 | { | |
5929 | if (p != NULL) | |
5930 | { | |
5931 | paramNode ret = (paramNode) dmalloc (sizeof (*ret)); | |
5932 | ||
5933 | ret->type = lclTypeSpecNode_copy (p->type); | |
5934 | ret->paramdecl = typeExpr_copy (p->paramdecl); | |
5935 | ret->kind = p->kind; | |
5936 | return ret; | |
5937 | } | |
5938 | ||
5939 | return NULL; | |
5940 | } | |
5941 | ||
5942 | void paramNode_free (/*@only@*/ /*@null@*/ paramNode x) | |
5943 | { | |
5944 | if (x != NULL) | |
5945 | { | |
5946 | lclTypeSpecNode_free (x->type); | |
5947 | typeExpr_free (x->paramdecl); | |
5948 | sfree (x); | |
5949 | } | |
5950 | } | |
5951 | ||
5952 | void programNode_free (/*@only@*/ /*@null@*/ programNode x) | |
5953 | { | |
5954 | if (x != NULL) | |
5955 | { | |
5956 | switch (x->kind) | |
5957 | { | |
5958 | case ACT_SELF: stmtNode_free (x->content.self); break; | |
5959 | case ACT_ITER: | |
5960 | case ACT_ALTERNATE: | |
5961 | case ACT_SEQUENCE: programNodeList_free (x->content.args); break; | |
5962 | BADDEFAULT; | |
5963 | } | |
5964 | sfree (x); | |
5965 | } | |
5966 | } | |
5967 | ||
5968 | quantifierNode quantifierNode_copy (quantifierNode x) | |
5969 | { | |
5970 | quantifierNode ret = (quantifierNode) dmalloc (sizeof (*ret)); | |
5971 | ||
5972 | ret->quant = ltoken_copy (x->quant); | |
5973 | ret->vars = varNodeList_copy (x->vars); | |
5974 | ret->isForall = x->isForall; | |
5975 | ||
5976 | return ret; | |
5977 | } | |
5978 | ||
5979 | void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x) | |
5980 | { | |
5981 | if (x != NULL) | |
5982 | { | |
5983 | varNodeList_free (x->vars); | |
5984 | ltoken_free (x->quant); | |
5985 | sfree (x); | |
5986 | } | |
5987 | } | |
5988 | ||
5989 | void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode x) | |
5990 | { | |
5991 | if (x != NULL) | |
5992 | { | |
5993 | if (x->isCType) | |
5994 | { | |
5995 | ; | |
5996 | } | |
5997 | else | |
5998 | { | |
5999 | nameNode_free (x->content.renamesortname.name); | |
6000 | sigNode_free (x->content.renamesortname.signature); | |
6001 | } | |
6002 | ||
6003 | typeNameNode_free (x->typename); | |
6004 | ltoken_free (x->tok); | |
6005 | sfree (x); | |
6006 | } | |
6007 | } | |
6008 | ||
6009 | storeRefNode storeRefNode_copy (storeRefNode x) | |
6010 | { | |
6011 | storeRefNode ret = (storeRefNode) dmalloc (sizeof (*ret)); | |
6012 | ||
6013 | ret->kind = x->kind; | |
6014 | ||
6015 | switch (x->kind) | |
6016 | { | |
6017 | case SRN_TERM: | |
6018 | ret->content.term = termNode_copySafe (x->content.term); | |
6019 | break; | |
6020 | case SRN_OBJ: case SRN_TYPE: | |
6021 | ret->content.type = lclTypeSpecNode_copy (x->content.type); | |
6022 | break; | |
6023 | case SRN_SPECIAL: | |
6024 | ret->content.ref = sRef_copy (x->content.ref); | |
6025 | break; | |
6026 | } | |
6027 | ||
6028 | return ret; | |
6029 | } | |
6030 | ||
6031 | void storeRefNode_free (/*@only@*/ /*@null@*/ storeRefNode x) | |
6032 | { | |
6033 | if (x != NULL) | |
6034 | { | |
6035 | if (storeRefNode_isTerm (x)) | |
6036 | { | |
6037 | termNode_free (x->content.term); | |
6038 | } | |
6039 | else if (storeRefNode_isType (x) || storeRefNode_isObj (x)) | |
6040 | { | |
6041 | lclTypeSpecNode_free (x->content.type); | |
6042 | } | |
6043 | else | |
6044 | { | |
6045 | /* nothing to free */ | |
6046 | } | |
6047 | ||
6048 | sfree (x); | |
6049 | } | |
6050 | } | |
6051 | ||
6052 | stDeclNode stDeclNode_copy (stDeclNode x) | |
6053 | { | |
6054 | stDeclNode ret = (stDeclNode) dmalloc (sizeof (*ret)); | |
6055 | ||
6056 | ret->lcltypespec = lclTypeSpecNode_copySafe (x->lcltypespec); | |
6057 | ret->declarators = declaratorNodeList_copy (x->declarators); | |
6058 | ||
6059 | return ret; | |
6060 | } | |
6061 | ||
6062 | void stDeclNode_free (/*@only@*/ /*@null@*/ stDeclNode x) | |
6063 | { | |
6064 | if (x != NULL) | |
6065 | { | |
6066 | lclTypeSpecNode_free (x->lcltypespec); | |
6067 | declaratorNodeList_free (x->declarators); | |
6068 | sfree (x); | |
6069 | } | |
6070 | } | |
6071 | ||
6072 | void traitRefNode_free (/*@only@*/ /*@null@*/ traitRefNode x) | |
6073 | { | |
6074 | if (x != NULL) | |
6075 | { | |
6076 | ltokenList_free (x->traitid); | |
6077 | renamingNode_free (x->rename); | |
6078 | sfree (x); | |
6079 | } | |
6080 | } | |
6081 | ||
6082 | void typeNameNode_free (/*@only@*/ /*@null@*/ typeNameNode n) | |
6083 | { | |
6084 | if (n != NULL) | |
6085 | { | |
6086 | typeNamePack_free (n->typename); | |
6087 | opFormNode_free (n->opform); | |
6088 | sfree (n); | |
6089 | } | |
6090 | } | |
6091 | ||
6092 | void varDeclarationNode_free (/*@only@*/ /*@null@*/ varDeclarationNode x) | |
6093 | { | |
6094 | if (x != NULL) | |
6095 | { | |
6096 | if (x->isSpecial) | |
6097 | { | |
6098 | ; | |
6099 | } | |
6100 | else | |
6101 | { | |
6102 | lclTypeSpecNode_free (x->type); | |
6103 | initDeclNodeList_free (x->decls); | |
6104 | sfree (x); | |
6105 | } | |
6106 | } | |
6107 | } | |
6108 | ||
6109 | varNode varNode_copy (varNode x) | |
6110 | { | |
6111 | varNode ret = (varNode) dmalloc (sizeof (*ret)); | |
6112 | ||
6113 | ret->varid = ltoken_copy (x->varid); | |
6114 | ret->isObj = x->isObj; | |
6115 | ret->type = lclTypeSpecNode_copySafe (x->type); | |
6116 | ret->sort = x->sort; | |
6117 | ||
6118 | return ret; | |
6119 | } | |
6120 | ||
6121 | void varNode_free (/*@only@*/ /*@null@*/ varNode x) | |
6122 | { | |
6123 | if (x != NULL) | |
6124 | { | |
6125 | lclTypeSpecNode_free (x->type); | |
6126 | ltoken_free (x->varid); | |
6127 | sfree (x); | |
6128 | } | |
6129 | } | |
6130 | ||
6131 | void stmtNode_free (/*@only@*/ /*@null@*/ stmtNode x) | |
6132 | { | |
6133 | if (x != NULL) | |
6134 | { | |
6135 | ltoken_free (x->lhs); | |
6136 | termNodeList_free (x->args); | |
6137 | ltoken_free (x->operator); | |
6138 | sfree (x); | |
6139 | } | |
6140 | } | |
6141 | ||
6142 | void renamingNode_free (/*@only@*/ /*@null@*/ renamingNode x) | |
6143 | { | |
6144 | if (x != NULL) | |
6145 | { | |
6146 | if (x->is_replace) | |
6147 | { | |
6148 | replaceNodeList_free (x->content.replace); | |
6149 | } | |
6150 | else | |
6151 | { | |
6152 | nameAndReplaceNode_free (x->content.name); | |
6153 | } | |
6154 | ||
6155 | sfree (x); | |
6156 | } | |
6157 | } | |
6158 | ||
6159 | void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode x) | |
6160 | { | |
6161 | if (x != NULL) | |
6162 | { | |
6163 | typeNameNodeList_free (x->namelist); | |
6164 | replaceNodeList_free (x->replacelist); | |
6165 | sfree (x); | |
6166 | } | |
6167 | } | |
6168 | ||
6169 | void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack x) | |
6170 | { | |
6171 | if (x != NULL) | |
6172 | { | |
6173 | lclTypeSpecNode_free (x->type); | |
6174 | abstDeclaratorNode_free (x->abst); | |
6175 | sfree (x); | |
6176 | } | |
6177 | } | |
6178 | ||
6179 | cstring interfaceNode_unparse (interfaceNode x) | |
6180 | { | |
6181 | if (x != NULL) | |
6182 | { | |
6183 | switch (x->kind) | |
6184 | { | |
6185 | case INF_IMPORTS: | |
6186 | return (message ("[imports] %q", importNodeList_unparse (x->content.imports))); | |
6187 | case INF_USES: | |
6188 | return (message ("[uses] %q", traitRefNodeList_unparse (x->content.uses))); | |
6189 | case INF_EXPORT: | |
6190 | return (message ("[export] %q", exportNode_unparse (x->content.export))); | |
6191 | case INF_PRIVATE: | |
6192 | return (message ("[private] %q", privateNode_unparse (x->content.private))); | |
6193 | } | |
6194 | ||
6195 | BADBRANCH; | |
6196 | } | |
6197 | else | |
6198 | { | |
6199 | return (cstring_makeLiteral ("<interface node undefined>")); | |
6200 | } | |
8250fa4a | 6201 | |
6202 | BADBRANCHRET (cstring_undefined); | |
616915dd | 6203 | } |
6204 | ||
6205 | void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode x) | |
6206 | { | |
6207 | if (x != NULL) | |
6208 | { | |
6209 | ||
6210 | switch (x->kind) | |
6211 | { | |
6212 | case INF_IMPORTS: importNodeList_free (x->content.imports); break; | |
6213 | case INF_USES: traitRefNodeList_free (x->content.uses); break; | |
6214 | case INF_EXPORT: exportNode_free (x->content.export); break; | |
6215 | case INF_PRIVATE: privateNode_free (x->content.private); break; | |
6216 | } | |
6217 | sfree (x); | |
6218 | } | |
6219 | } | |
6220 | ||
6221 | void exportNode_free (/*@null@*/ /*@only@*/ exportNode x) | |
6222 | { | |
6223 | if (x != NULL) | |
6224 | { | |
6225 | switch (x->kind) | |
6226 | { | |
6227 | case XPK_CONST: constDeclarationNode_free (x->content.constdeclaration); break; | |
6228 | case XPK_VAR: varDeclarationNode_free (x->content.vardeclaration); break; | |
6229 | case XPK_TYPE: typeNode_free (x->content.type); break; | |
6230 | case XPK_FCN: fcnNode_free (x->content.fcn); break; | |
6231 | case XPK_CLAIM: claimNode_free (x->content.claim); break; | |
6232 | case XPK_ITER: iterNode_free (x->content.iter); break; | |
6233 | } | |
6234 | ||
6235 | sfree (x); | |
6236 | } | |
6237 | } | |
6238 | ||
6239 | void privateNode_free (/*@null@*/ /*@only@*/ privateNode x) | |
6240 | { | |
6241 | if (x != NULL) | |
6242 | { | |
6243 | switch (x->kind) | |
6244 | { | |
6245 | case PRIV_CONST: | |
6246 | constDeclarationNode_free (x->content.constdeclaration); break; | |
6247 | case PRIV_VAR: | |
6248 | varDeclarationNode_free (x->content.vardeclaration); break; | |
6249 | case PRIV_TYPE: | |
6250 | typeNode_free (x->content.type); break; | |
6251 | case PRIV_FUNCTION: | |
6252 | fcnNode_free (x->content.fcn); break; | |
6253 | } | |
6254 | ||
6255 | sfree (x); | |
6256 | } | |
6257 | } | |
6258 | ||
6259 | void constDeclarationNode_free (/*@only@*/ /*@null@*/ constDeclarationNode x) | |
6260 | { | |
6261 | if (x != NULL) | |
6262 | { | |
6263 | lclTypeSpecNode_free (x->type); | |
6264 | initDeclNodeList_free (x->decls); | |
6265 | sfree (x); | |
6266 | } | |
6267 | } | |
6268 | ||
6269 | void typeNode_free (/*@only@*/ /*@null@*/ typeNode t) | |
6270 | { | |
6271 | if (t != NULL) | |
6272 | { | |
6273 | switch (t->kind) | |
6274 | { | |
6275 | case TK_ABSTRACT: abstractNode_free (t->content.abstract); break; | |
6276 | case TK_EXPOSED: exposedNode_free (t->content.exposed); break; | |
6277 | case TK_UNION: taggedUnionNode_free (t->content.taggedunion); break; | |
6278 | } | |
6279 | ||
6280 | sfree (t); | |
6281 | } | |
6282 | } | |
6283 | ||
6284 | void claimNode_free (/*@only@*/ /*@null@*/ claimNode x) | |
6285 | { | |
6286 | if (x != NULL) | |
6287 | { | |
6288 | paramNodeList_free (x->params); | |
6289 | globalList_free (x->globals); | |
6290 | letDeclNodeList_free (x->lets); | |
6291 | lclPredicateNode_free (x->require); | |
6292 | programNode_free (x->body); | |
6293 | lclPredicateNode_free (x->ensures); | |
6294 | ltoken_free (x->name); | |
6295 | sfree (x); | |
6296 | } | |
6297 | } | |
6298 | ||
6299 | void iterNode_free (/*@only@*/ /*@null@*/ iterNode x) | |
6300 | { | |
6301 | if (x != NULL) | |
6302 | { | |
6303 | paramNodeList_free (x->params); | |
6304 | ltoken_free (x->name); | |
6305 | sfree (x); | |
6306 | } | |
6307 | } | |
6308 | ||
6309 | void abstractNode_free (/*@only@*/ /*@null@*/ abstractNode x) | |
6310 | { | |
6311 | if (x != NULL) | |
6312 | { | |
6313 | abstBodyNode_free (x->body); | |
6314 | ltoken_free (x->tok); | |
6315 | ltoken_free (x->name); | |
6316 | sfree (x); | |
6317 | } | |
6318 | } | |
6319 | ||
6320 | void exposedNode_free (/*@only@*/ /*@null@*/ exposedNode x) | |
6321 | { | |
6322 | if (x != NULL) | |
6323 | { | |
6324 | lclTypeSpecNode_free (x->type); | |
6325 | declaratorInvNodeList_free (x->decls); | |
6326 | ltoken_free (x->tok); | |
6327 | sfree (x); | |
6328 | } | |
6329 | } | |
6330 | ||
6331 | void taggedUnionNode_free (/*@only@*/ /*@null@*/ taggedUnionNode x) | |
6332 | { | |
6333 | if (x != NULL) | |
6334 | { | |
6335 | stDeclNodeList_free (x->structdecls); | |
6336 | declaratorNode_free (x->declarator); | |
6337 | sfree (x); | |
6338 | } | |
6339 | } | |
6340 | ||
6341 | /*@only@*/ /*@null@*/ strOrUnionNode | |
6342 | strOrUnionNode_copy (/*@null@*/ strOrUnionNode n) | |
6343 | { | |
6344 | if (n != NULL) | |
6345 | { | |
6346 | strOrUnionNode ret = (strOrUnionNode) dmalloc (sizeof (*ret)); | |
6347 | ||
6348 | ret->kind = n->kind; | |
6349 | ret->tok = ltoken_copy (n->tok); | |
6350 | ret->opttagid = ltoken_copy (n->opttagid); | |
6351 | ret->sort = n->sort; | |
6352 | ret->structdecls = stDeclNodeList_copy (n->structdecls); | |
6353 | ||
6354 | return ret; | |
6355 | } | |
6356 | else | |
6357 | { | |
6358 | return NULL; | |
6359 | } | |
6360 | } | |
6361 | ||
6362 | void strOrUnionNode_free (/*@null@*/ /*@only@*/ strOrUnionNode n) | |
6363 | { | |
6364 | if (n != NULL) | |
6365 | { | |
6366 | stDeclNodeList_free (n->structdecls); | |
6367 | ltoken_free (n->tok); | |
6368 | ltoken_free (n->opttagid); | |
6369 | sfree (n); | |
6370 | } | |
6371 | } | |
6372 | ||
6373 | void enumSpecNode_free (/*@null@*/ /*@only@*/ enumSpecNode x) | |
6374 | { | |
6375 | if (x != NULL) | |
6376 | { | |
6377 | ltokenList_free (x->enums); | |
6378 | ltoken_free (x->tok); | |
6379 | ltoken_free (x->opttagid); | |
6380 | sfree (x); | |
6381 | } | |
6382 | } | |
6383 | ||
6384 | /*@only@*/ /*@null@*/ enumSpecNode enumSpecNode_copy (/*@null@*/ enumSpecNode x) | |
6385 | { | |
6386 | if (x != NULL) | |
6387 | { | |
6388 | enumSpecNode ret = (enumSpecNode) dmalloc (sizeof (*ret)); | |
6389 | ||
6390 | ret->tok = ltoken_copy (x->tok); | |
6391 | ret->opttagid = ltoken_copy (x->opttagid); | |
6392 | ret->enums = ltokenList_copy (x->enums); | |
6393 | ret->sort = x->sort; | |
6394 | ||
6395 | return ret; | |
6396 | } | |
6397 | else | |
6398 | { | |
6399 | return NULL; | |
6400 | } | |
6401 | } | |
6402 | ||
6403 | void lsymbol_setbool (lsymbol s) | |
6404 | { | |
6405 | lsymbol_bool = s; | |
6406 | } | |
6407 | ||
6408 | lsymbol lsymbol_getbool () | |
6409 | { | |
6410 | return lsymbol_bool; | |
6411 | } | |
6412 | ||
6413 | lsymbol lsymbol_getBool () | |
6414 | { | |
6415 | return lsymbol_Bool; | |
6416 | } | |
6417 | ||
6418 | lsymbol lsymbol_getFALSE () | |
6419 | { | |
6420 | return lsymbol_FALSE; | |
6421 | } | |
6422 | ||
6423 | lsymbol lsymbol_getTRUE () | |
6424 | { | |
6425 | return lsymbol_TRUE; | |
6426 | } | |
6427 | ||
6428 |