Validator
Validator of the C abstract syntax for tools.
Besides syntactic validity,
C code must satisfy a number of additional constraints
in order to be compiled.
These constraints form the static semantics of C.
C compilers check that the code satisfies these constraints
prior to translating it.
Here we provide a validator of C code,
whose purpose is to check those constraints,
i.e. to check whether the C code is valid and compilable.
If successful, the validator adds information to the abstract syntax,
Thus,
We start with an approximate validator
that should accept all valid C code
but also some invalid C code (due to the approximation).
Even in its approximate form,
this may be useful to perform some validation,
and to calculate information (approximate types)
that may be useful for manipulating the abstract syntax
(e.g. for C-to-C transformations).
In a sense, the validator extends the disambiguator,
which performs an even more approximate validation,
just enough to disambiguate the abstract syntax.
Thus, there are structural similarities between
the validator and the disambiguator.
Similarly to a compiler, the validator makes use of a symbol table,
which tracks information about the symbols (identifiers) in the code.
These symbol tables, called `validation tables', are, in some sense,
an extension of the disambiguation tables used by the disambiguator.
We use error-value tuples to handle errors in the validator.
The ACL2 functions that validate the various parts of the abstract syntax
follow the valid-<fixtype> naming scheme,
where <fixtype> is the name of
the fixtype of the abstract syntax part,
and where valid is best read as an abbreviation of `validate'
rather than as the adjective `valid'.
This validator is work in progress.
Subtopics
- Valid-exprs/decls/stmts
- Validate expressions, declarations, statements,
and related artifacts.
- Type
- Fixtype of C types [C:6.2.5].
- Valid-stmt
- Validate a statement.
- Valid-expr
- Validate an expression.
- Valid-dirdeclor
- Validate a direct declarator.
- Valid-transunit
- Validate a translation unit.
- Valid-stor-spec-list
- Validate a list of storage class specifiers.
- Valid-unary
- Validate a unary expression,
given the type of the sub-expression.
- Valid-initdeclor
- Validate an initializer declarator.
- Valid-fundef
- Validate a function definition.
- Valid-binary
- Validate a binary expression,
given the type of the sub-expression.
- Valid-type-spec
- Validate a type specifier.
- Valid-lookup-ord
- Look up an ordinary identifier in a validation table.
- Valid-type-spec-list-residual
- Validate a residual list of type specifiers.
- Type-uaconvert-signed-unsigned
- Convert a promoted signed integer type
and a promoted unsigned integer type
to their common type,
according to the usual arithmetic conversions [C:6.3.1.8].
- Valid-declor
- Validate a declarator.
- Valid-cond
- Validate a conditional expression,
given types for its operands.
- Type-uaconvert
- Perform the usual arithmetic conversions on two arithmetic types
[C:6.3.1.8].
- Valid-transunit-ensemble
- Validate a translation unit ensemble.
- Valid-c-char
- Validate a character of a character constant.
- Valid-ord-info
- Fixtype of validation information about ordinary identifiers.
- Valid-initer
- Validate an initializer.
- Valid-iconst
- Validate an integer constant.
- Valid-stringlit-list
- Validate a list of string literals.
- Valid-funcall
- Validate a function call expression,
given the types of the sub-expressions.
- Valid-add-ord
- Add an ordinary identifier to the validation table.
- Lifetime
- Fixtype of lifetimes.
- Valid-arrsub
- Validate an array subscripting expression,
given the types of the two sub-expressions.
- Type-promote
- Perform integer promotions on an arithmetic type [C:6.3.1.1/2].
- Valid-univ-char-name
- Validate a universal character name.
- Valid-cast
- Validate a cast expression,
given the type denoted by the type name
and the type of the argument expression.
- Valid-add-ord-file-scope
- Add an ordinary identifier
to the file scope of a validation table.
- Valid-spec/qual
- Validate a specifier or qualifier.
- Valid-sizeof/alignof
- Validate a sizeof operator applied to a type name,
or an alignof operator,
given the type denoted by the argument type name.
- Valid-memberp
- Validate a member pointer expression,
given the type of the sub-expression.
- Valid-extdecl
- Validate an external declaration.
- Valid-decl-spec
- Validate a declaration specifier.
- Valid-paramdecl
- Validate a parameter declaration.
- Valid-oct-escape
- Validate an octal escape.
- Valid-extdecl-list
- Validate a list of external declarations.
- Valid-structdeclor
- Validate a structure declarator.
- Valid-structdecl
- Validate a structure declaration.
- Valid-designor
- Validate a designator.
- Valid-defstatus
- Fixtype of definition statuses for validation.
- Valid-escape
- Validate an escape sequence.
- Valid-enum-const
- Validate an enumeration constant.
- Valid-var
- Validate a variable.
- Valid-table
- Fixtype of validation tables.
- Valid-s-char
- Validate a character of a string literal.
- Valid-ord-info-option
- Fixtype of
optional validation information about ordinary identifiers.
- Valid-dec/oct/hex-const
- Validate a decimal, octal, or hexadecimal constant.
- Valid-cconst
- Validate a character constant.
- Valid-gensel
- Validate a generic selection expression,
given the types for the components.
- Linkage-option
- Fixtype of optional linkages.
- Lifetime-option
- Fixtype of optional lifetimes.
- Valid-decl-spec-list
- Validate a list of declaration specifiers.
- Type-option
- Fixtype of optional types.
- Linkage
- Fixtype of linkages.
- Valid-lookup-ord-file-scope
- Look up an ordinary identifier
in the file scope of a validation table.
- Valid-member
- Validate a member expression,
given the type of the sub-expression.
- Valid-scope
- Fixtype of validation scopes.
- Type-uaconvert-unsigned
- Convert two promoted unsigned integer types to their common type,
according to the usual arithmetic conversions [C:6.3.1.8].
- Valid-const
- Validate a constant.
- Type-uaconvert-signed
- Convert two promoted signed integer types to their common type,
according to the usual arithmetic conversions [C:6.3.1.8].
- Valid-paramdeclor
- Validate a parameter declarator.
- Valid-spec/qual-list
- Validate a list of specifiers and qualifiers.
- Valid-fconst
- Validate a floating constant.
- Valid-stringlit
- Validate a string literal.
- Valid-s-char-list
- Validate a list of characters of a string literal.
- Valid-c-char-list
- Validate a list of characters of a character constant.
- Valid-block-item
- Validate a block item.
- Valid-structdeclor-list
- Validate a list structure declarators.
- Valid-simple-escape
- Validate a simple escape.
- Valid-pop-scope
- Pop a scope from the validation table.
- Valid-align-spec
- Validate an alignment specifier.
- Valid-enumer
- Validate an enumerator.
- Valid-dirabsdeclor
- Validate a direct abstract declarator.
- Valid-decl
- Validate a declaration.
- Valid-enumspec
- Validate an enumeration specifier.
- Valid-declor-option
- Validate an optional declarator.
- Valid-push-scope
- Push a scope onto the validation table.
- Valid-initer-option
- Validate an optional initializer.
- Valid-block-item-list
- Validate a list of block items.
- Valid-absdeclor
- Validate an abstract declarator.
- Type-unsigned-integerp
- Check if a type is an unsigned integer type [C:6.2.5/6].
- Type-fpconvert
- Convert function types to pointer types.
- Valid-label
- Validate a label.
- Valid-genassoc
- Validate a generic association.
- Type-signed-integerp
- Check if a type is a signed integer type [C:6.2.5/4].
- Type-promotedp
- Check if an arithmetic type is a promoted one.
- Type-arithmeticp
- Check if a type is an arithmetic type [C:6.2.5/18].
- Type-apconvert
- Convert array types to pointer types.
- Valid-tyname
- Validate a type name.
- Valid-strunispec
- Validate a structure or union specifier.
- Valid-structdecl-list
- Validate a list of structure declarators.
- Valid-ord-scope
- Fixtype of validation scopes of ordinary identifiers.
- Valid-genassoc-list
- Validate a list of generic associations.
- Valid-dirabsdeclor-option
- Validate an optional direct abstract declarator.
- Valid-designor-list
- Validate a list of zero or more designators.
- Valid-const-expr
- Validate a constant expression.
- Type-standard-unsigned-integerp
- Check if a type is a standard unsigned integer type [C:6.2.5/6].
- Type-standard-signed-integerp
- Check if a type is a standard signed integer type [C:6.2.5/4].
- Type-aggregatep
- Check if a type is an aggregate type [C:6.2.5/21].
- Valid-initdeclor-list
- Validate a list of initializer declarators.
- Valid-desiniter-list
- Validate a list of zero or more
initializers with optional designations.
- Valid-absdeclor-option
- Validate an optional abstract declarator.
- Valid-table-num-scopes
- Number of scopes in a validation table.
- Valid-expr-list
- Validate a list of expressions.
- Type-standard-integerp
- Check if a type is a standard integer type [C:6.2.5/7].
- Type-real-floatingp
- Check if a type is a real floating type [C:6.2.5/10].
- Valid-paramdecl-list
- Validate a list of parameter declarations.
- Valid-desiniter
- Validate an initializer with optional designation.
- Valid-const-expr-option
- Validate an optional constant expression.
- Type-integerp
- Check if a type is an integer type [C:6.2.5/17].
- Type-floatingp
- Check if a type is a floating type [C:6.2.5/11].
- Type-complexp
- Check if a type is a complex type [C:6.2.5/11].
- Type-characterp
- Check if a type is a character type [C:6.2.5/15].
- Type-basicp
- Check if a type is a basic type [C:6.2.5/14].
- Valid-expr-option
- Validate an optional expression.
- Type-scalarp
- Check if a type is a scalar type [C:6.2.5/21].
- Type-realp
- Check if a type is a real type [C:6.2.5/17].
- Valid-statassert
- Validate a static assertion declaration.
- Valid-enumer-list
- Validate a list of enumerators.
- Valid-init-table
- Initial validation table.
- Valid-empty-scope
- Empty validator scope.
- Valid-member-designor
- Validate a member designator.
- Valid-decl-list
- Validate a list of declarations.
- Irr-valid-table
- An irrelevant validation table.
- Valid-scope-list
- Fixtype of lists of validation scopes.
- Type-set
- Fixtype of sets of types.
- Type-option-type-alist
- Fixtype of alists from optional types to types.
- Irr-linkage
- An irrelevant linkage.
- Irr-lifetime
- An irrelevant lifetime.
- Type-list
- Fixtype of lists of types.
- Irr-type
- An irrelevant type.
