		Search-engine friendly clone of the ACL2 documentation.

Valid-expr

Validate an expression.

Signature
(valid-expr expr table ienv) → (mv erp new-expr type return-types new-table)
Arguments: expr — Guard (exprp expr).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-expr — Type (exprp new-expr).; type — Type (typep type).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

If validation is successful, we return the type of the expression, the set of types returned by return statements in the expression, and a possibly updated validation table. The reason for the set of return types is that, as a GCC extension, an expression may consist of a statement, and the validation of statements involves sets of return types: see valid-stmt. In case of successful validation, we also return a possibly enriched expression: the enrichment consists of a type added as information for identifier expression; that is the type of the identifier expression, calculated by the validator.

For now we do not distinguish lvalues [C17:6.3.2.1/1]. To do that, we will introduce a richer notion of expression type that includes a type and also an indication of whether the expression is an lvalue; we will also perform lvalue conversion where needed. This is already done in c::static-semantics, for the subset of C that is formalized.

We use separate functions to validate the various kinds of expressions, to minimize case splits in the mutually recursive clique of functions. But we need to calculate types for sub-expressions recursively here, and pass the types to those separate functions.

Expressions without subexpressions return the empty set of return types. Other expressions return the union of the sets obtained from validating the sub-constructs.

To validate a compound literal, first we validate the type name, obtaining a type if that validation is successful. Then we validate the initializers with optional designations, passing the type because in general their validation depends on that; however, in our currently approximate type system, all the information we need back from the validation of the initializers with optional designations is the possibly updated validation table. The type of the compound literal is the one denoted by the type name. We also need to pass an indication of the storage duration (i.e. lifetime) of the object, which is either static or automatic, based on whether the compound literal occurs outside or inside the body of a function [C17:6.5.2.5/5], which we can see based on whether the number of scopes in the validation table is 1 or not (recall that this number is never 0).

In a conditional expression, the second operand may be absent; this is a GCC extension. However, for validation, we normalize the situation by replicating the type of the first operand for the second operand, when there is no second operand, according to the semantics of the absence of the second operand.

For the comma operator, we validate both sub-expressions, and the resulting type is the one of the second sub-expression [C17:6.5.17/2].

For a statement expression, we validate the block items. If a type is returned, that is the type of the expression. Otherwise, the expression has type void, as described in the GCC documentation of statement expressions.

The GCC extension __builtin_types_compatible_p is validated by validating its argument type names. The result is signed int, according to the GCC manual.

For the GCC extension __builtin_offsetof, for now we just validate its component type names and expressions (if any), but without checking that the member designators are valid; for that, we need a more refined type system. The result has type size_t [C17:7.19], whose definition is implementation-dependent, and thus for now we return the unknown type.