1 /* 2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. 3 ** See ../LICENSE for license information. 4 ** 5 */ 6 /* 7 ** exprNode.h 8 */ 9 10 # ifndef EXPRNODE_H 11 # define EXPRNODE_H 12 13 /* 14 ** expression Nodes: 15 ** 16 ** ctype typ --- type of expression 17 ** 18 ** union _val 19 ** { long ival; 20 ** char cval; 21 ** double fval; 22 ** cstring sval; 23 ** } *val --- value, if known. if unknown, val = (_val *)0 24 ** 25 ** storeRef sref --- storage referred to by expression, of storeRef_null 26 ** 27 ** cstring etext --- to get nice error messages, punt for now! 28 */ 29 30 /* in exprNode_type: typedef struct _exprNode *exprNode; */ 31 32 typedef enum 33 { 34 XPR_PARENS, XPR_ASSIGN, XPR_CALL, XPR_EMPTY, XPR_VAR, 35 XPR_OP, XPR_POSTOP, XPR_PREOP, XPR_SIZEOFT, XPR_SIZEOF, XPR_ALIGNOFT, XPR_ALIGNOF, 36 XPR_OFFSETOF, XPR_CAST, XPR_FETCH, XPR_VAARG, XPR_ITER, 37 XPR_FOR, XPR_FORPRED, XPR_GOTO, XPR_CONTINUE, XPR_BREAK, 38 XPR_RETURN, XPR_NULLRETURN, XPR_COMMA, XPR_COND, XPR_IF, XPR_IFELSE, 39 XPR_DOWHILE, XPR_WHILE, XPR_STMT, XPR_STMTLIST, XPR_SWITCH, 40 XPR_INIT, XPR_FACCESS, XPR_ARROW, XPR_CONST, XPR_STRINGLITERAL, 41 XPR_NUMLIT, XPR_BODY, XPR_NODE, XPR_ITERCALL, XPR_TOK, 42 XPR_WHILEPRED, XPR_CASE, XPR_FTCASE, XPR_DEFAULT, XPR_FTDEFAULT, 43 XPR_BLOCK, XPR_INITBLOCK, 44 XPR_LABEL 45 } exprKind; 46 47 typedef struct 48 { 49 /*@only@*/ qtype q; 50 /*@only@*/ cstringList field; 51 } *exprOffsetof; 52 53 typedef struct 54 { 55 /*@only@*/ exprNode a; 56 /*@only@*/ exprNode b; 57 } *exprPair; 58 59 typedef struct 60 { 61 /*@only@*/ exprNode pred; 62 /*@only@*/ exprNode tbranch; 63 /*@only@*/ exprNode fbranch; 64 } *exprTriple; 65 66 typedef struct 67 { 68 /*@dependent@*/ /*@observer@*/ uentry sname; 69 /*@only@*/ exprNodeList args; 70 /*@only@*/ exprNode body; 71 /*@dependent@*/ /*@observer@*/ uentry ename; 72 } *exprIter; 73 74 typedef struct 75 { 76 /*@only@*/ exprNode fcn; 77 /*@only@*/ exprNodeList args; 78 } *exprCall; 79 80 typedef struct 81 { 82 /*@dependent@*/ /*@exposed@*/ uentry iter; 83 /*@only@*/ exprNodeList args; 84 } *exprIterCall; 85 86 typedef struct 87 { 88 /*@only@*/ exprNode a; 89 /*@only@*/ exprNode b; 90 lltok op; 91 } *exprOp; 92 93 typedef struct 94 { 95 /*@only@*/ exprNode rec; 96 /*@only@*/ cstring field; 97 } *exprField; 98 99 typedef struct 100 { 101 /*@only@*/ exprNode a; 102 lltok op; 103 } *exprUop; 104 105 typedef struct 106 { 107 /*@only@*/ exprNode exp; 108 lltok tok; 109 qtype q; 110 } *exprCast; 111 112 typedef struct 113 { 114 /*@only@*/ exprNode exp; 115 idDecl id; 116 } *exprInit; 117 118 typedef /*@null@*/ union 119 { 120 cstring literal; 121 cstring id; 122 lltok tok; 123 qtype qt; /* sizeof(type) */ 124 /* use for any 2-operator (comma, arrayFetch, case, stmt) */ 125 exprPair pair; 126 exprOp op; /* pair + operator */ 127 exprUop uop; 128 exprInit init; 129 exprIter iter; 130 exprCall call; 131 exprIterCall itercall; 132 exprCast cast; 133 exprNode single; 134 exprField field; 135 exprTriple triple; /* ifelse, ternary op, for pred */ 136 exprOffsetof offset; 137 } *exprData; 138 139 /*@constant null exprData exprData_undefined; @*/ 140 # define exprData_undefined ((exprData) NULL) 141 142 struct s_exprNode 143 { 144 bool isJumpPoint BOOLBITS; /* expr can be reached non-sequentially */ 145 bool canBreak BOOLBITS; /* expr can break (has break, continue) */ 146 bool mustBreak BOOLBITS; 147 148 ctype typ; 149 exitkind exitCode; 150 151 multiVal val; 152 /*@exposed@*/ sRef sref; 153 sRefSet uses; /* sRef's used by this expression */ 154 sRefSet sets; /* sRef's set by this expression */ 155 sRefSet msets; /* sRef's possibly set (implicit out params, etc.) */ 156 157 guardSet guards; 158 exprKind kind; 159 160 fileloc loc; 161 /*@relnull@*/ exprData edata; 162 cstring etext; 163 /*@notnull@*/ constraintList requiresConstraints; 164 /*@notnull@*/ constraintList ensuresConstraints; 165 166 /* 167 ** These two are used only for boolean expressions, 168 ** they store the ensures constraints for the true and false cases 169 */ 170 171 /*@notnull@*/ constraintList trueEnsuresConstraints; 172 /*@notnull@*/ constraintList falseEnsuresConstraints; 173 } ; 174 175 /*@constant null exprNode exprNode_undefined; @*/ 176 # define exprNode_undefined ((exprNode)NULL) 177 178 extern /*@falsewhennull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ; 179 extern /*@unused@*/ /*@nullwhentrue@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ; 180 extern /*@nullwhentrue@*/ bool exprNode_isError (exprNode p_e) /*@*/ ; 181 182 # define exprNode_isDefined(e) ((e) != exprNode_undefined) 183 # define exprNode_isUndefined(e) ((e) == exprNode_undefined) 184 # define exprNode_isError(e) ((e) == exprNode_undefined) 185 186 extern /*@dependent@*/ /*@exposed@*/ guardSet 187 exprNode_getGuards (/*@sef@*/ exprNode p_e) /*@*/ ; 188 # define exprNode_getGuards(e) \ 189 (exprNode_isDefined(e) ? (e)->guards : guardSet_undefined) 190 191 extern ctype exprNode_getType (/*@sef@*/ exprNode p_e) /*@*/ ; 192 # define exprNode_getType(e) \ 193 (exprNode_isDefined(e) ? (e)->typ : ctype_unknown) 194 195 extern /*@unused@*/ /*@falsewhennull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ; 196 # define exprNode_isInParens(e) \ 197 (exprNode_isDefined(e) && (e)->kind == XPR_PARENS) 198 199 extern bool exprNode_isStringLiteral (/*@sef@*/ exprNode p_e) /*@*/ ; 200 # define exprNode_isStringLiteral(e) \ 201 (exprNode_isDefined(e) && (e)->kind == XPR_STRINGLITERAL) 202 203 extern /*@unused@*/ bool exprNode_knownIntValue (/*@sef@*/ exprNode p_e) /*@*/ ; 204 # define exprNode_knownIntValue(e) \ 205 (exprNode_isDefined(e) && multiVal_isInt (exprNode_getValue (e))) 206 207 extern /*@unused@*/ bool exprNode_knownStringValue (/*@sef@*/ exprNode p_e) /*@*/ ; 208 # define exprNode_knownStringValue(e) \ 209 (exprNode_isDefined(e) && multiVal_isString (exprNode_getValue (e))) 210 211 extern bool exprNode_hasValue (/*@sef@*/ exprNode p_e) /*@*/ ; 212 # define exprNode_hasValue(e) \ 213 (exprNode_isDefined(e) && multiVal_isDefined (exprNode_getValue (e))) 214 215 extern /*@exposed@*/ multiVal exprNode_getValue (exprNode p_e) /*@*/ ; 216 extern long exprNode_getLongValue (exprNode p_e) /*@*/ ; 217 218 extern /*@observer@*/ cstring exprNode_unparseFirst (exprNode p_e) /*@*/ ; 219 extern void exprNode_revealState (exprNode p_e) /*@modifies g_messagestream@*/ ; 220 221 extern /*@observer@*/ guardSet exprNode_getForGuards (exprNode p_pred) /*@*/ ; 222 extern bool exprNode_loopMustExec (exprNode p_forPred) /*@*/ ; 223 224 extern bool exprNode_isNullValue (exprNode p_e) /*@*/ ; 225 extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ; 226 extern /*@exposed@*/ uentry exprNode_getUentry (exprNode p_e) 227 /*@globals internalState@*/ ; 228 extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ; 229 230 extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ; 231 extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ; 232 # define exprNode_getLoc exprNode_loc 233 234 extern exprNode 235 exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ; 236 extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ; 237 extern exprNode 238 exprNode_cond (/*@keep@*/ exprNode p_pred, /*@keep@*/ exprNode p_ifclause, 239 /*@keep@*/ exprNode p_elseclause) /*@*/ ; 240 241 extern exprNode 242 exprNode_condIfOmit (/*@keep@*/ exprNode p_pred, 243 /*@keep@*/ exprNode p_elseclause) /*@*/ ; 244 245 extern exprNode exprNode_makeError(void) /*@*/ ; 246 247 extern exprNode exprNode_makeInitBlock (lltok p_brace, /*@only@*/ exprNodeList p_inits) /*@*/ ; 248 249 extern exprNode exprNode_functionCall (/*@only@*/ exprNode p_f, 250 /*@only@*/ exprNodeList p_args) /*@*/ ; 251 extern /*@notnull@*/ exprNode 252 exprNode_fromIdentifier (/*@observer@*/ uentry p_c) /*@globals internalState@*/ ; 253 extern exprNode exprNode_fromUIO (cstring p_c) /*@globals internalState@*/ ; 254 extern exprNode exprNode_fieldAccess (/*@only@*/ exprNode p_s, 255 /*@only@*/ lltok p_dot, 256 /*@only@*/ cstring p_f) /*@*/ ; 257 258 extern exprNode exprNode_arrowAccess (/*@only@*/ exprNode p_s, 259 /*@only@*/ lltok p_arrow, 260 /*@only@*/ cstring p_f) /*@*/ ; 261 262 extern exprNode exprNode_postOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) 263 /*@modifies p_e@*/ ; 264 extern exprNode exprNode_preOp (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_op) /*@*/ ; 265 extern exprNode exprNode_addParens (/*@only@*/ lltok p_lpar, /*@only@*/ exprNode p_e) /*@*/ ; 266 extern exprNode exprNode_offsetof (/*@only@*/ qtype p_qt, /*@only@*/ cstringList p_s) /*@*/ ; 267 extern exprNode exprNode_sizeofType (/*@only@*/ qtype p_qt) /*@*/ ; 268 extern exprNode exprNode_sizeofExpr (/*@only@*/ exprNode p_e) /*@*/ ; 269 extern exprNode exprNode_alignofType (/*@only@*/ qtype p_qt) /*@*/ ; 270 extern exprNode exprNode_alignofExpr (/*@only@*/ exprNode p_e) /*@*/ ; 271 extern exprNode 272 exprNode_op (/*@only@*/ exprNode p_e1, /*@keep@*/ exprNode p_e2, /*@only@*/ lltok p_op) /*@*/ ; 273 extern exprNode 274 exprNode_assign (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2, /*@only@*/ lltok p_op) ; 275 extern exprNode 276 exprNode_arrayFetch (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) 277 /*@modifies p_e1, p_e2@*/ ; 278 279 extern void exprNode_free (/*@only@*/ exprNode p_e) ; 280 extern exprNode 281 exprNode_vaArg (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_arg, /*@only@*/ qtype p_qt) 282 /*@globals internalState@*/ ; 283 284 extern bool exprNode_isMultiStatement (exprNode p_e) /*@*/ ; 285 286 /* 287 ** Has surrounding quotes. 288 */ 289 290 extern /*@only@*/ /*@notnull@*/ exprNode 291 exprNode_stringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ; 292 293 extern /*@only@*/ /*@notnull@*/ exprNode 294 exprNode_wideStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ; 295 296 /* 297 ** No surrounding quotes. 298 */ 299 300 extern /*@notnull@*/ exprNode 301 exprNode_rawStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ; 302 303 extern exprNode exprNode_comma (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) /*@*/ ; 304 extern exprNode exprNode_labelMarker (/*@only@*/ cstring p_label); 305 extern exprNode 306 exprNode_notReached (/*@returned@*/ exprNode p_stmt); 307 308 extern 309 exprNode exprNode_caseMarker (/*@only@*/ exprNode p_test, bool p_fallThrough) /*@*/ ; 310 311 extern exprNode exprNode_concat (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2); 312 extern /*@notnull@*/ exprNode exprNode_createTok (/*@only@*/ lltok p_t) /*@*/ ; 313 extern exprNode exprNode_statement (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t); 314 extern exprNode exprNode_makeBlock (/*@only@*/ exprNode p_e); 315 extern exprNode exprNode_compoundStatementExpression (/*@only@*/ lltok p_tlparen, /*@only@*/ exprNode p_e) ; 316 317 extern void exprNode_checkIfPred (exprNode p_pred) /*@modifies g_warningstream@*/ ; 318 319 extern exprNode exprNode_if (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause); 320 extern exprNode 321 exprNode_ifelse (/*@only@*/ exprNode p_pred, /*@only@*/ exprNode p_tclause, 322 /*@only@*/ exprNode p_eclause); 323 extern exprNode exprNode_switch (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_s); 324 extern exprNode exprNode_while (/*@keep@*/ exprNode p_t, /*@keep@*/ exprNode p_b); 325 extern exprNode exprNode_doWhile (/*@only@*/ exprNode p_b, /*@only@*/ exprNode p_t); 326 extern /*@notnull@*/ /*@only@*/ exprNode exprNode_goto (/*@only@*/ cstring p_label); 327 extern exprNode exprNode_continue (/*@only@*/ lltok p_l, int p_qcontinue); 328 extern exprNode exprNode_break (/*@only@*/ lltok p_l, int p_bqual); 329 extern exprNode exprNode_nullReturn (/*@only@*/ lltok p_t); 330 extern exprNode exprNode_return (/*@only@*/ exprNode p_e); 331 extern /*@dependent@*/ /*@observer@*/ cstring 332 exprNode_unparse (/*@temp@*/ exprNode p_e) /*@*/ ; 333 334 extern /*@falsewhennull@*/ bool exprNode_isBlock (exprNode p_e) /*@*/ ; 335 extern /*@falsewhennull@*/ bool exprNode_isCharLiteral (exprNode p_e) /*@*/ ; 336 extern /*@falsewhennull@*/ bool exprNode_isNumLiteral (exprNode p_e) /*@*/ ; 337 338 extern exprNode 339 exprNode_makeInitialization (/*@only@*/ idDecl p_t, /*@only@*/ exprNode p_e); 340 341 exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl p_t) ; 342 343 extern bool exprNode_isInitializer (exprNode p_e) /*@*/ ; 344 345 extern bool exprNode_matchType (ctype p_expected, exprNode p_e); 346 347 extern /*@notnull@*/ /*@only@*/ exprNode 348 exprNode_defaultMarker (/*@only@*/ lltok p_def, bool p_fallThrough); 349 350 extern exprNode 351 exprNode_iter (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist, 352 /*@only@*/ exprNode p_body, /*@observer@*/ uentry p_end); 353 extern exprNode exprNode_iterId (/*@observer@*/ uentry p_c); 354 extern exprNode exprNode_iterExpr (/*@returned@*/ exprNode p_e); 355 extern exprNode exprNode_iterNewId (/*@only@*/ cstring p_s); 356 extern exprNode 357 exprNode_iterStart (/*@observer@*/ uentry p_name, /*@only@*/ exprNodeList p_alist); 358 extern exprNode exprNode_numLiteral (ctype p_c, /*@temp@*/ cstring p_t, 359 /*@only@*/ fileloc p_loc, long p_val) /*@*/ ; 360 extern void exprNode_initMod (void) /*@modifies internalState@*/ ; 361 extern exprNode exprNode_for (/*@keep@*/ exprNode p_inc, /*@keep@*/ exprNode p_body); 362 extern exprNode 363 exprNode_forPred (/*@only@*/ exprNode p_init, 364 /*@only@*/ exprNode p_test, /*@only@*/ exprNode p_inc); 365 extern exprNode exprNode_floatLiteral (double p_d, ctype p_ct, 366 cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ; 367 extern /*@notnull@*/ exprNode exprNode_createId (/*@observer@*/ uentry p_c); 368 extern /*@notnull@*/ exprNode exprNode_makeConstantString (/*@temp@*/ cstring p_c, /*@only@*/ fileloc p_loc) /*@*/ ; 369 extern exprNode exprNode_cast (/*@only@*/ lltok p_tok, /*@only@*/ exprNode p_e, /*@only@*/ qtype p_q); 370 extern bool exprNode_matchLiteral (ctype p_expected, exprNode p_e); 371 extern void exprNode_checkUseParam (exprNode p_current); 372 extern void exprNode_checkSet (exprNode p_e, /*@exposed@*/ sRef p_s); 373 extern void exprNode_checkMSet (exprNode p_e, /*@exposed@*/ sRef p_s); 374 extern exprNode exprNode_checkExpr (/*@returned@*/ exprNode p_e); 375 extern bool exprNode_mustEscape (exprNode p_e); 376 extern bool exprNode_errorEscape (exprNode p_e); 377 extern bool exprNode_mayEscape (exprNode p_e); 378 extern exprNode exprNode_whilePred (/*@only@*/ exprNode p_test); 379 extern exprNode 380 exprNode_updateLocation (/*@returned@*/ exprNode p_e, /*@temp@*/ fileloc p_loc); 381 extern void exprNode_freeShallow (/*@only@*/ exprNode p_e); 382 extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ; 383 extern /*@falsewhennull@*/ bool exprNode_isAssign (exprNode p_e) /*@*/ ; 384 385 /*@-exportlocal@*/ 386 extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ; 387 extern bool exprNode_isCaseMarker (exprNode p_e) /*@*/ ; 388 extern bool exprNode_isLabelMarker (exprNode p_e) /*@*/ ; 389 /*@=exportlocal@*/ 390 391 extern /*@only@*/ exprNode exprNode_combineLiterals (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_rest) ; 392 393 extern /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode p_e) ; 394 395 /*drl 01-20-2001*/ 396 exprNode exprNode_createNew(ctype p_c); 397 398 /* drl 07-25-01 */ 399 bool exprNode_isInitBlock (exprNode p_e); 400 401 # else 402 # error "Multiple include" 403 # endif 404