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,
which downstream tools (e.g. C-to-C transformations) can make use of.
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 is useful to perform some validation,
and to calculate information (approximate types)
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.
See valid-table.
We use error-value tuples to handle errors in the validator.
The ACL2 functions that validate
the various constructs of the abstract syntax
follow the valid-<fixtype> naming scheme,
where <fixtype> is the name of
the fixtype of the abstract syntax construct,
and where valid is best read as an abbreviation of `validate'
rather than as the adjective `valid'.
Subtopics
- Valid-exprs/decls/stmts
- Validate expressions, declarations, statements,
and related artifacts.
- Valid-stmt
- Validate a statement.
- Valid-expr
- Validate an expression.
- Valid-dirdeclor
- Validate a direct declarator.
- Valid-type-spec
- Validate a type specifier.
- Valid-transunit
- Validate a translation unit.
- Valid-stor-spec-list
- Validate a list of storage class specifiers.
- Valid-binary
- Validate a binary expression,
given the type of the sub-expression.
- 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-type-spec-list-residual
- Validate a residual list of type specifiers.
- Valid-cond
- Validate a conditional expression,
given types for its operands.
- Valid-lookup-ord
- Look up an ordinary identifier in a validation table.
- Valid-transunit-ensemble
- Validate a translation unit ensemble.
- Valid-declor
- Validate a declarator.
- Valid-iconst
- Validate an integer constant.
- Valid-initer
- Validate an initializer.
- Valid-c-char
- Validate a character of a character 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.
- Valid-arrsub
- Validate an array subscripting expression,
given the types of the two sub-expressions.
- Valid-univ-char-name
- Validate a universal character name.
- Valid-extdecl
- Validate an external declaration.
- Valid-extdecl-list
- Validate a list of external declarations.
- 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-decl-spec
- Validate a declaration specifier.
- Valid-var
- Validate a variable.
- Valid-param-declon
- Validate a parameter declaration.
- Valid-oct-escape
- Validate an octal escape.
- Valid-structdeclor
- Validate a structure declarator.
- Valid-structdecl
- Validate a structure declaration.
- Valid-designor
- Validate a designator.
- Valid-escape
- Validate an escape sequence.
- Valid-enum-const
- Validate an enumeration constant.
- Valid-cconst
- Validate a character constant.
- Valid-s-char
- Validate a character of a string literal.
- Valid-dec/oct/hex-const
- Validate a decimal, octal, or hexadecimal constant.
- Valid-const
- Validate a constant.
- Valid-gensel
- Validate a generic selection expression,
given the types for the components.
- Valid-decl-spec-list
- Validate a list of declaration specifiers.
- 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-param-declor
- 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-align-spec
- Validate an alignment specifier.
- Valid-enumer
- Validate an enumerator.
- Valid-dirabsdeclor
- Validate a direct abstract declarator.
- Valid-decl
- Validate a declaration.
- Valid-pop-scope
- Pop a scope from the validation table.
- 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.
- Valid-label
- Validate a label.
- Valid-genassoc
- Validate a generic association.
- Valid-tyname
- Validate a type name.
- Valid-strunispec
- Validate a structure or union specifier.
- Valid-structdecl-list
- Validate a list of structure declarators.
- 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.
- 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.
- Valid-param-declon-list
- Validate a list of parameter declarations.
- Valid-desiniter
- Validate an initializer with optional designation.
- Valid-const-expr-option
- Validate an optional constant expression.
- Valid-expr-option
- Validate an optional expression.
- 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.
