Valid-type-spec
Validate a type specifier.
- Signature
(valid-type-spec tyspec type? tyspecs table ienv)
→
(mv erp new-tyspec new-type? new-tyspecs return-types new-table)
- Arguments
- tyspec — Guard (type-specp tyspec).
- type? — Guard (type-optionp type?).
- tyspecs — Guard (type-spec-listp tyspecs).
- table — Guard (valid-tablep table).
- ienv — Guard (ienvp ienv).
- Returns
- erp — Type (maybe-msgp erp).
- new-tyspec — Type (type-specp new-tyspec).
- new-type? — Type (type-optionp new-type?).
- new-tyspecs — Type (type-spec-listp new-tyspecs).
- return-types — Type (type-setp return-types).
- new-table — Type (valid-tablep new-table).
Type specifiers are used to specify types, as described in [C17:6.7.2/2].
Certain type specifiers individually specify a type,
and there cannot be other type specifiers;
an example is void.
Other type specifiers may individually specify a type,
but they may be also combined with other type specifiers
to specify a different type;
an example is signed.
The type specifier _Complex does not individually specify any type,
and must be always combined with other type specifiers.
Given these possibilities,
our approach is to validate type specifiers in order,
while going through the declaration specifiers,
or the specifier and qualifier lists,
where they occur.
As we go through them, we thread through two pieces of information:
an optional type,
non-nil when a type has been definitely determined,
and a list of type specifiers encountered so far.
These two cannot be non-nil at the same time, as the guard requires:
if a type has been determined,
there is no need to keep track of the type specifiers so far;
and if we are keeping track of the type specifiers so far,
we must not have determined a type yet.
Initially,
the optional type and the list of type specifiers are both nil,
because we neither have encountered any type specifiers
nor determined a type.
If we encounter a type specifier like void
that individually denotes a type,
we ensure that no other type specifiers were encountered before,
and we determine the type.
Once a type is determined, any type specifier will cause an error.
We may get at the end without a determined type yet,
but we will have the list of all the type specifiers,
which is used, in another validation function,
to determined the type if any.
Our current type system does not model atomic types,
so for an atomic type we validate the type name
and we regard the atomic type as denoting the same type.
For a structure or union or enumeration type specifier,
we recursively validate their sub-structures,
and the type is determined in all cases.
For typedef names,
we look up the type definition in the validation table.
If no such entry exists in the table, validation fails.
Otherwise, we return the type in the table entry
as the one denoted by the typedef name.
The latter is an important point, because it means that
we always fully expand typedef names
to their typedef-name-free types
(recall that type has no case for typedef names).
In a translation unit, no forward references are allowed,
so the first typedef (if any) cannot refer to others;
later typedefs may refer to previous ones,
but since we expand their definientia through this table lookup,
we effectively always recursively expand all typedefs.
This may be exactly what is needed for validation,
but we will revisit this choice if needed.
For now, for simplicity, we regard
all the type specifiers that are GCC extensions
to determine the unknown type;
except for an empty structure type specifier,
which determines the structure type.
The __int128 may be preceded by unsigned,
according to the GCC documentation;
we found, in practical code,
that it can also be preceded by signed and its underscore variants;
so __int128 alone does not determine a type,
and we use valid-type-spec-list-residual
to determine the type, if any, as done in other cases.
Definitions and Theorems
Theorem: type-spec-list-unambp-of-valid-type-spec
(defthm type-spec-list-unambp-of-valid-type-spec
(implies (type-spec-list-unambp tyspecs)
(b* (((mv acl2::?erp ?new-tyspec ?new-type?
?new-tyspecs ?return-types ?new-table)
(valid-type-spec tyspec type? tyspecs table ienv)))
(type-spec-list-unambp new-tyspecs))))
Theorem: not-type-and-type-specs-of-valid-type-spec
(defthm not-type-and-type-specs-of-valid-type-spec
(b* (((mv acl2::?erp ?new-tyspec ?new-type?
?new-tyspecs ?return-types ?new-table)
(valid-type-spec tyspec type? tyspecs table ienv)))
(not (and new-type? new-tyspecs))))
