src/Headers/symtable.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   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
  27 typedef struct {
  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
  34 typedef struct {
  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 */
  55 } varKind;
  56
  57 typedef struct {
  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
  69 typedef struct {
  70   /*@only@*/ nameNode name;
  71   /*@only@*/ sigNodeSet signatures;
  72 } *opInfo;
  73
  74 typedef struct {
  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
 103 typedef struct {
 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
 116 typedef struct s_htEntry {
 117   /*@only@*/ htData *data;
 118   /*@only@*/ struct s_htEntry *next;
 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
 134 typedef struct s_symtableStruct *symtable;
 135
 136 extern /*@falsewhennull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti);
 137 # define typeInfo_exists(ti)  ((ti) != NULL)
 138
 139 extern /*@falsewhennull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi);
 140 # define varInfo_exists(vi)   ((vi) != NULL)
 141
 142 extern /*@falsewhennull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi);
 143 # define tagInfo_exists(ti)   ((ti) != NULL)
 144
 145 extern /*@falsewhennull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi);
 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
 175 extern void symtable_import(inputStream p_imported, ltoken p_tok, mapping p_map);
 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);
 181 extern lsymbol lsymbol_translateSort (mapping p_m, lsymbol p_s);
 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,
 186                                sortSetList p_argSorts, sort p_qual);
 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