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-dirdeclor
- Validate a direct declarator.
- Valid-expr
- Validate an expression.
- 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-transunit-ensemble
- Validate a translation unit ensemble.
- Valid-cond
- Validate a conditional expression,
given types for its operands.
- Valid-lookup-ord
- Look up an ordinary identifier in a validation table.
- 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-arrsub
- Validate an array subscripting expression,
given the types of the two sub-expressions.
- Valid-add-ord
- Add an ordinary identifier to the validation table.
- 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-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-cast
- Validate a cast expression,
given the type denoted by the type name
and the type of the argument expression.
- Valid-var
- Validate a variable.
- Valid-spec/qual
- Validate a specifier or qualifier.
- Valid-oct-escape
- Validate an octal escape.
- Valid-decl-spec
- Validate a declaration specifier.
- Valid-add-ord-file-scope
- Add an ordinary identifier
to the file scope of a validation table.
- Valid-param-declon
- Validate a parameter declaration.
- Valid-enum-const
- Validate an enumeration constant.
- Valid-structdeclor
- Validate a structure declarator.
- Valid-structdecl
- Validate a structure declaration.
- Valid-s-char
- Validate a character of a string literal.
- Valid-gensel
- Validate a generic selection expression,
given the types for the components.
- Valid-escape
- Validate an escape sequence.
- Valid-designor
- Validate a designator.
- Valid-const
- Validate a constant.
- Valid-cconst
- Validate a character constant.
- Valid-dec/oct/hex-const
- Validate a decimal, octal, or hexadecimal constant.
- Valid-member
- Validate a member expression,
given the type of the sub-expression.
- 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-param-declor
- Validate a parameter declarator.
- 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-spec/qual-list
- Validate a list of specifiers and qualifiers.
- Valid-fconst
- Validate a floating constant.
- Valid-block-item
- Validate a block item.
- Valid-structdeclor-list
- Validate a list structure declarators.
- Valid-align-spec
- Validate an alignment specifier.
- Valid-simple-escape
- Validate a simple escape.
- Valid-enumer
- Validate an enumerator.
- Valid-decl
- Validate a declaration.
- Valid-enumspec
- Validate an enumeration specifier.
- Valid-dirabsdeclor
- Validate a direct abstract declarator.
- Valid-declor-option
- Validate an optional declarator.
- Valid-pop-scope
- Pop a scope from 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-push-scope
- Push a scope onto the validation table.
- Valid-label
- Validate a label.
- Valid-genassoc
- Validate a generic association.
- Valid-tyname
- Validate a type name.
- Valid-struni-spec
- 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-absdeclor-option
- Validate an optional abstract declarator.
- Valid-expr-list
- Validate a list of expressions.
- Valid-desiniter-list
- Validate a list of zero or more
initializers with optional designations.
- Valid-table-num-scopes
- Number of scopes in a validation table.
- 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-member-designor
- Validate a member designator.
- Valid-init-table
- Initial validation table.
- Valid-empty-scope
- Empty validator scope.
- Valid-decl-list
- Validate a list of declarations.
