]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
c0de361f | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. |
885824d3 | 3 | ** See ../LICENSE for license information. |
4 | */ | |
5 | /* | |
6 | ** symtable.h | |
7 | */ | |
8 | ||
9 | # ifndef SYMTABLE_H | |
10 | # define SYMTABLE_H | |
11 | ||
12 | /* There are 3 separate namespaces being maintained in this symbol | |
13 | table: (N1) for C objects, functions, typedef names and enumeration | |
14 | constants. (N2) for C tags. (N3) for LSL operators. I re-use the | |
15 | old linked list to represent N1 since it is here and it is convenient | |
16 | for representing scopes. Two more new hashtables are added to store | |
17 | N2 and N3, each keyed on the lsymbol of the identifier. */ | |
18 | ||
19 | /*@constant observer char *BEGINSYMTABLE;@*/ | |
20 | # define BEGINSYMTABLE "%LCLSymbolTable" | |
21 | ||
22 | /*@constant observer char *SYMTABLEEND;@*/ | |
23 | # define SYMTABLEEND "%LCLSymbolTableEnd" | |
24 | ||
25 | typedef long unsigned symbolKey; | |
26 | ||
28bf4b0b | 27 | typedef struct { |
885824d3 | 28 | ltoken id; |
29 | bool export; /* all HOF maps to one sort kind: SRT_HOF */ | |
30 | /*@only@*/ signNode signature; /* in terms of sorts, no HOF */ | |
31 | /*@only@*/ pairNodeList globals; /* list of (sort globalnameSym) */ | |
32 | } *fctInfo; | |
33 | ||
28bf4b0b | 34 | typedef struct { |
885824d3 | 35 | ltoken id; |
36 | sort basedOn; | |
37 | bool abstract; /* TRUE means LCL abstract type */ | |
38 | bool modifiable; /* TRUE indicates the abstract type is mutable */ | |
39 | bool export; /* if TRUE, export it from this module */ | |
40 | } *typeInfo; | |
41 | ||
42 | typedef enum | |
43 | { | |
44 | VRK_CONST, /* an LCL constant */ | |
45 | VRK_ENUM, /* an enumeration constant, | |
46 | a special kind of LCL constant */ | |
47 | VRK_VAR, /* an LCL variable */ | |
48 | VRK_PRIVATE,/* a variable private to current function/module */ | |
49 | /* function private overrides module private, usual scoping | |
50 | rules */ | |
51 | VRK_GLOBAL, /* in globals of a function */ | |
52 | VRK_LET, /* local let variable in a function decl */ | |
53 | VRK_PARAM, /* formal parameters of a function/claim */ | |
54 | VRK_QUANT /* bound by a quantifier */ | |
28bf4b0b | 55 | } varKind; |
885824d3 | 56 | |
28bf4b0b | 57 | typedef struct { |
885824d3 | 58 | ltoken id; |
59 | sort sort; | |
60 | varKind kind; | |
61 | bool export; /* if TRUE, export it from this module */ | |
62 | } *varInfo; | |
63 | ||
64 | /* The same lsymbol can originate from different files: | |
65 | an LCL file or an LSL file. Each occurrence in an LCL file appears | |
66 | as one of {opId, anyOp, logicalOp, simpleOp, eqOp, MULOP} ltoken. | |
67 | Each occurrence in an LSL file appears as an lslOp AST. */ | |
68 | ||
28bf4b0b | 69 | typedef struct { |
885824d3 | 70 | /*@only@*/ nameNode name; |
71 | /*@only@*/ sigNodeSet signatures; | |
72 | } *opInfo; | |
73 | ||
28bf4b0b | 74 | typedef struct { |
885824d3 | 75 | ltoken id; |
76 | tagKind kind; | |
77 | bool imported; | |
78 | sort sort; | |
79 | /*@reldef@*/ union | |
80 | { | |
81 | /*@null@*/ /*@dependent@*/ ltokenList enums; | |
82 | /*@null@*/ stDeclNodeList decls; | |
83 | } content; | |
84 | } *tagInfo; | |
85 | ||
86 | typedef enum { | |
87 | IK_SORT, IK_OP, IK_TAG | |
88 | } infoKind; | |
89 | ||
90 | typedef struct { | |
91 | infoKind kind; | |
92 | union { | |
93 | tagInfo tag; | |
94 | sort sort; | |
95 | opInfo op;} content; | |
96 | } htData; | |
97 | ||
98 | typedef enum { | |
99 | SPE_GLOBAL, SPE_FCN, SPE_QUANT, SPE_CLAIM, | |
100 | SPE_ABSTRACT, SPE_INVALID | |
101 | } scopeKind; | |
102 | ||
28bf4b0b | 103 | typedef struct { |
885824d3 | 104 | scopeKind kind; |
105 | } *scopeInfo; | |
106 | ||
107 | /* | |
108 | ** A simple hash table implementation: Given a key K and a | |
109 | ** pointer P to a piece of data, associate K with P. | |
110 | ** | |
111 | ** Assumes that K is unsigned int, and data supports | |
112 | ** 3 operations: | |
113 | ** data_key: htData * -> unsigned int | |
114 | */ | |
115 | ||
28bf4b0b | 116 | typedef struct s_htEntry { |
885824d3 | 117 | /*@only@*/ htData *data; |
28bf4b0b | 118 | /*@only@*/ struct s_htEntry *next; |
885824d3 | 119 | } htEntry; |
120 | ||
121 | /* Each bucket is a linked list of entries */ | |
122 | ||
123 | typedef htEntry bucket; | |
124 | typedef /*@relnull@*/ /*@only@*/ bucket *o_bucket; | |
125 | ||
126 | typedef struct { | |
127 | unsigned int count; | |
128 | unsigned int size; | |
129 | /*@relnull@*/ /*@only@*/ o_bucket *buckets; | |
130 | } symHashTable; | |
131 | ||
132 | /* Local to implementation */ | |
133 | ||
28bf4b0b | 134 | typedef struct s_symtableStruct *symtable; |
885824d3 | 135 | |
0e41eb0e | 136 | extern /*@falsewhennull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti); |
885824d3 | 137 | # define typeInfo_exists(ti) ((ti) != NULL) |
138 | ||
0e41eb0e | 139 | extern /*@falsewhennull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi); |
885824d3 | 140 | # define varInfo_exists(vi) ((vi) != NULL) |
141 | ||
0e41eb0e | 142 | extern /*@falsewhennull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi); |
885824d3 | 143 | # define tagInfo_exists(ti) ((ti) != NULL) |
144 | ||
0e41eb0e | 145 | extern /*@falsewhennull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi); |
885824d3 | 146 | # define opInfo_exists(oi) ((oi) != NULL) |
147 | ||
148 | extern /*@only@*/ symtable symtable_new (void) /*@*/ ; | |
149 | extern void symtable_enterScope (symtable p_stable, /*@keep@*/ scopeInfo p_si); | |
150 | extern void symtable_exitScope(symtable p_stable); | |
151 | ||
152 | extern bool symtable_enterFct (symtable p_stable, /*@only@*/ fctInfo p_fi); | |
153 | extern void symtable_enterType (symtable p_stable, /*@only@*/ typeInfo p_ti); | |
154 | ||
155 | /* not only --- it is copied! */ | |
156 | extern bool symtable_enterVar (symtable p_stable, /*@temp@*/ varInfo p_vi); | |
157 | extern void symtable_enterOp (symtable p_st, | |
158 | /*@only@*/ /*@notnull@*/ nameNode p_n, | |
159 | /*@owned@*/ sigNode p_oi); | |
160 | extern bool symtable_enterTag (symtable p_st, /*@only@*/ tagInfo p_ti); | |
161 | extern bool symtable_enterTagForce(symtable p_st, /*@only@*/ tagInfo p_ti); | |
162 | ||
163 | extern bool symtable_exists(symtable p_stable, lsymbol p_i); | |
164 | ||
165 | extern /*@observer@*/ /*@null@*/ typeInfo symtable_typeInfo(symtable p_stable, lsymbol p_i); | |
166 | extern /*@observer@*/ /*@null@*/ varInfo symtable_varInfo(symtable p_stable, lsymbol p_i); | |
167 | extern /*@observer@*/ /*@null@*/ varInfo symtable_varInfoInScope(symtable p_stable, lsymbol p_id); | |
168 | extern /*@observer@*/ /*@null@*/ opInfo symtable_opInfo(symtable p_st, | |
169 | /*@notnull@*/ nameNode p_n); | |
170 | extern /*@observer@*/ /*@null@*/ tagInfo symtable_tagInfo(symtable p_st, lsymbol p_i); | |
171 | ||
172 | extern void symtable_export(symtable p_stable, bool p_yesNo); | |
173 | extern void symtable_dump(symtable p_stable, FILE *p_f, bool p_lco); | |
174 | ||
28bf4b0b | 175 | extern void symtable_import(inputStream p_imported, ltoken p_tok, mapping p_map); |
885824d3 | 176 | |
177 | extern /*@unused@*/ void symtable_printStats (symtable p_s); | |
178 | ||
179 | extern lsymbol lsymbol_sortFromType (symtable, lsymbol); | |
180 | extern cstring tagKind_unparse (tagKind p_k); | |
28bf4b0b | 181 | extern lsymbol lsymbol_translateSort (mapping p_m, lsymbol p_s); |
885824d3 | 182 | extern void varInfo_free (/*@only@*/ varInfo p_v); |
183 | ||
184 | extern /*@only@*/ lslOpSet | |
185 | symtable_opsWithLegalDomain (symtable p_tab, /*@temp@*/ /*@null@*/ nameNode p_n, | |
53306cab | 186 | sortSetList p_argSorts, sort p_q); |
885824d3 | 187 | extern /*@observer@*/ sigNodeSet |
188 | symtable_possibleOps (symtable p_tab, nameNode p_n); | |
189 | extern bool symtable_opExistsWithArity(symtable p_tab, nameNode p_n, int p_arity); | |
190 | ||
191 | extern void symtable_free (/*@only@*/ symtable p_stable); | |
192 | ||
193 | # else | |
194 | # error "Multiple include" | |
195 | # endif | |
196 |