src/Headers/usymtab.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** usymtab.h
   7 */
   8
   9 # ifndef USYMTAB_H
  10 # define USYMTAB_H
  11
  12 /*@constant null usymtab GLOBAL_ENV; @*/
  13 # define GLOBAL_ENV usymtab_undefined
  14
  15 typedef enum {
  16   US_GLOBAL,
  17   US_NORMAL,
  18   US_TBRANCH, US_FBRANCH,
  19   US_CBRANCH, US_SWITCH
  20 } uskind;
  21
  22 typedef struct { int level; int index; } *refentry;
  23 typedef /*@only@*/ refentry o_refentry;
  24 typedef o_refentry *refTable;
  25
  26 struct s_usymtab
  27 {
  28   uskind   kind;
  29   int      nentries;
  30   int      nspace;
  31   int      lexlevel;
  32   bool     mustBreak;
  33   exitkind exitCode;
  34   /*@reldef@*/ /*@only@*/ o_uentry  *entries;
  35   /*@null@*/ /*@only@*/ cstringTable htable;   /* for the global environment */
  36   /*@null@*/ /*@only@*/ refTable  reftable; /* for branched environments */
  37              /*@only@*/ guardSet  guards;   /* guarded references (not null) */
  38   aliasTable aliases;
  39   /*@owned@*/ usymtab env;
  40 } ;
  41
  42 /*
  43 ** rep invariant:
  44 **
  45 ** (left as exercise to reader)  ;)
  46 */
  47
  48 extern void usymtab_printTypes (void)
  49   /*@globals internalState@*/
  50   /*@modifies g_warningstream@*/ ;
  51
  52 extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
  53
  54 extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ;
  55 extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ;
  56 extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
  57 extern void usymtab_checkFinalScope (bool p_isReturn)
  58   /*@globals internalState@*/
  59   /*@modifies *g_warningstream@*/ ;
  60
  61 extern void usymtab_allUsed (void)
  62    /*@globals internalState@*/
  63    /*@modifies *g_warningstream@*/ ;
  64
  65 extern void usymtab_allDefined (void)
  66    /*@globals internalState@*/
  67    /*@modifies *g_warningstream@*/ ;
  68
  69 extern void usymtab_prepareDump (void)
  70    /*@modifies internalState@*/ ;
  71
  72 extern void usymtab_dump (FILE *p_fout)
  73    /*@globals internalState@*/
  74    /*@modifies *p_fout@*/ ;
  75
  76
  77 extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
  78
  79 extern /*@exposed@*/ /*@dependent@*/ uentry
  80   usymtab_getRefQuiet (int p_level, usymId p_index)
  81   /*@globals internalState@*/ ;
  82
  83 extern void usymtab_printLocal (void)
  84   /*@globals internalState@*/
  85   /*@modifies stdout@*/ ;
  86
  87 extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno)
  88    /*@globals internalState@*/;
  89 extern void usymtab_free (void) /*@modifies internalState@*/ ;
  90 extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ;
  91
  92 extern /*@exposed@*/  uentry usymtab_lookupExpose (cstring p_k)
  93    /*@globals internalState@*/ ;
  94
  95 extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
  96    /*@globals internalState@*/ ;
  97
  98 # define usymtab_lookup(s) (usymtab_lookupExpose (s))
  99
 100 extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k)
 101    /*@globals internalState@*/ ;
 102 extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k)
 103    /*@globals internalState@*/ ;
 104 extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k)
 105    /*@globals internalState@*/ ;
 106 extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k)
 107    /*@globals internalState@*/ ;
 108 extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
 109    /*@globals internalState@*/ ;
 110
 111 extern ctype usymtab_lookupType (cstring p_k)
 112    /*@globals internalState@*/ ;
 113
 114 extern bool usymtab_isDefinitelyNull (sRef p_s)
 115    /*@globals internalState@*/ ;
 116 extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
 117    /*@globals internalState@*/ ;
 118
 119 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
 120    /*@modifies internalState, p_e@*/ ;
 121
 122 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
 123    /*@modifies internalState, p_e@*/ ;
 124
 125 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
 126    /*@modifies internalState@*/ ;
 127
 128 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
 129    /*@globals internalState@*/ ;
 130
 131 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
 132   /*@globals internalState@*/ ;
 133
 134 extern bool usymtab_exists (cstring p_k)
 135    /*@globals internalState@*/ ;
 136
 137 extern bool usymtab_existsVar (cstring p_k)
 138    /*@globals internalState@*/ ;
 139
 140 extern bool usymtab_existsGlob (cstring p_k)
 141    /*@globals internalState@*/ ;
 142
 143 extern bool usymtab_existsType (cstring p_k)
 144    /*@globals internalState@*/ ;
 145
 146 extern bool usymtab_existsEither (cstring p_k)
 147    /*@globals internalState@*/ ;
 148
 149 extern bool usymtab_existsTypeEither (cstring p_k)
 150    /*@globals internalState@*/ ;
 151
 152 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
 153 extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
 154
 155 extern void usymtab_supEntry (/*@only@*/ uentry p_e)
 156   /*@modifies internalState, p_e@*/ ;
 157
 158 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
 159   /*@modifies internalState, p_s@*/ ;
 160
 161 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
 162   /*@modifies internalState, p_e@*/ ;
 163
 164 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
 165   /*@modifies internalState@*/ ;
 166
 167 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
 168   /*@modifies internalState, p_e@*/ ;
 169
 170 extern /*@exposed@*/ uentry
 171   usymtab_supEntryReturn (/*@only@*/ uentry p_e)
 172   /*@modifies internalState, p_e@*/ ;
 173
 174 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
 175   /*@modifies internalState, p_e@*/ ;
 176
 177 extern ctype usymtab_lookupAbstractType (cstring p_k)
 178      /*@globals internalState@*/ /*@modifies nothing@*/ ;
 179
 180 extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
 181      /*@globals internalState@*/ ;
 182
 183 extern bool usymtab_existsEnumTag (cstring p_k)
 184   /*@globals internalState@*/ ;
 185 extern bool usymtab_existsUnionTag (cstring p_k)
 186   /*@globals internalState@*/ ;
 187 extern bool usymtab_existsStructTag (cstring p_k)
 188   /*@globals internalState@*/ ;
 189
 190 extern usymId usymId_fromInt (int p_i) /*@*/ ;
 191 # define usymId_fromInt(i)   ((usymId)(i))
 192
 193 extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
 194 # define usymId_isInvalid(u) ((u) == USYMIDINVALID)
 195
 196 extern bool usymId_isValid (usymId p_u) /*@*/ ;
 197 # define usymId_isValid(u)   ((u) != USYMIDINVALID)
 198
 199 extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
 200 # define typeId_isInvalid(u) ((u) == typeId_invalid)
 201
 202 extern bool typeId_isValid (typeId p_u) /*@*/ ;
 203 # define typeId_isValid(u)   ((u) != typeId_invalid)
 204
 205 extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
 206 # define typeId_equal(u1,u2) ((u1) == (u2))
 207
 208 extern typeId typeId_fromInt (int p_i);
 209 # define typeId_fromInt(i)   ((typeId)(i))
 210
 211 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
 212 # define usymtab_entries(x, m_i)   \
 213     { int m_ind; \
 214       if (usymtab_isDefined (x)) \
 215         for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
 216            { uentry m_i = (x)->entries[m_ind];
 217
 218 # define end_usymtab_entries }}
 219
 220 extern /*@unused@*/ void usymtab_displayAllUses (void)
 221    /*@globals internalState@*/
 222    /*@modifies *g_warningstream@*/ ;
 223
 224 extern /*@unused@*/ void usymtab_printOut (void)
 225    /*@globals internalState@*/
 226    /*@modifies *g_warningstream@*/ ;
 227
 228 extern /*@unused@*/ void usymtab_printAll (void)
 229    /*@globals internalState@*/
 230    /*@modifies *g_warningstream@*/ ;
 231
 232 extern void usymtab_enterScope (void)
 233   /*@modifies internalState;@*/ ;
 234 extern void usymtab_enterFunctionScope (uentry p_fcn)
 235   /*@modifies internalState;@*/ ;
 236 extern void usymtab_quietExitScope (fileloc p_loc)
 237   /*@modifies internalState;@*/ ;
 238 extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
 239 extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
 240 extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
 241 extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
 242 extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
 243
 244 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
 245   /*@globals internalState@*/ ;
 246
 247 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
 248 extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
 249 extern void usymtab_destroyMod (void) /*@modifies internalState@*/ ;
 250 extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
 251 extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
 252
 253 extern void usymtab_exportHeader (void)
 254    /*@modifies internalState@*/ ;
 255
 256 extern ctype usymtab_structFieldsType (uentryList p_f)
 257    /*@globals internalState@*/ ;
 258
 259 extern ctype usymtab_unionFieldsType (uentryList p_f)
 260    /*@globals internalState@*/ ;
 261
 262 extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
 263    /*@globals internalState@*/ ;
 264
 265 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
 266    /*@globals internalState@*/ ;
 267
 268 extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
 269   /*@modifies internalState@*/ ;
 270 extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
 271   /*@modifies internalState@*/ ;
 272
 273 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
 274   /*@modifies internalState@*/ ;
 275 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
 276   /*@modifies internalState@*/ ;
 277
 278 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
 279   /*@modifies internalState@*/ ;
 280
 281 extern void
 282   usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
 283   /*@modifies internalState@*/ ;
 284
 285 extern void
 286   usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
 287                        bool p_isOpt, clause p_cl)
 288    /*@modifies internalState@*/ ;
 289
 290 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
 291 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
 292 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_warningstream@*/ ;
 293 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
 294 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
 295
 296 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
 297
 298 extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ;
 299 extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid)
 300   /*@globals internalState@*/ ;
 301 extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid)
 302   /*@globals internalState@*/ ;
 303
 304 extern typeId
 305   usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
 306   /*@modifies internalState, p_e@*/ ;
 307 extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
 308   /*@modifies internalState, p_e@*/ ;
 309
 310 extern /*@exposed@*/ uentry
 311   usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
 312   /*@modifies internalState, p_e@*/ ;
 313
 314 extern /*@exposed@*/ uentry
 315   usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
 316   /*@modifies internalState, p_e@*/ ;
 317
 318 extern int uentry_directParamNo (uentry p_ue)
 319   /*@globals internalState@*/ ;
 320
 321 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
 322   /*@modifies internalState@*/ ;
 323
 324 extern void usymtab_switchBranch (exprNode p_s)
 325   /*@modifies internalState@*/ ;
 326
 327 extern /*@only@*/ cstring usymtab_unparseStack (void)
 328   /*@globals internalState@*/ ;
 329 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
 330   /*@modifies internalState@*/ ;
 331
 332 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
 333   /*@globals internalState@*/ ;
 334
 335 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
 336   /*@globals internalState@*/ ;
 337
 338 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
 339   /*@globals internalState@*/ ;
 340
 341 extern void usymtab_clearAlias (sRef p_s)
 342   /*@modifies internalState, p_s@*/ ;
 343
 344 extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
 345   /*@modifies internalState@*/ ;
 346
 347 extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
 348   /*@modifies internalState@*/ ;
 349
 350 extern /*@only@*/ cstring usymtab_unparseAliases (void)
 351   /*@globals internalState@*/ ;
 352
 353 extern /*@exposed@*/ uentry
 354   usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
 355    /*@modifies internalState@*/ ;
 356
 357 extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
 358    /*@globals internalState@*/ ;
 359
 360 extern bool usymtab_existsReal (cstring p_k)
 361    /*@globals internalState@*/ ;
 362
 363 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
 364    /*@globals internalState@*/ ;
 365
 366 extern void usymtab_exportLocal (void)
 367    /*@modifies internalState@*/ ;
 368
 369 extern void usymtab_popCaseBranch (void)
 370      /*@modifies internalState@*/ ;
 371
 372 /* special scopes */
 373
 374 /*@constant int globScope;@*/
 375 # define globScope 0  /* global variables */
 376
 377 /*@constant int fileScope;@*/
 378 # define fileScope   1  /* file-level static variables */
 379
 380 /*@constant int paramsScope;@*/
 381 # define paramsScope 2  /* function parameters */
 382
 383 /*@constant int functionScope;@*/
 384 # define functionScope 3
 385
 386 extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
 387
 388 /*@constant null usymtab usymtab_undefined; @*/
 389 # define usymtab_undefined ((usymtab)NULL)
 390 # define usymtab_isDefined(u) ((u) != usymtab_undefined)
 391
 392 extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
 393   /*@globals internalState@*/
 394   /*@modifies *g_warningstream, p_e@*/ ;
 395
 396 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
 397 extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ;
 398 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
 399
 400 # ifdef DEBUGSPLINT
 401 extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ;
 402 # endif
 403
 404 # else
 405 # error "Multiple include"
 406 # endif
 407
 408
 409