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-binary
- Validate a binary expression,
given the type of the sub-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-prototype-args
- Validate a function prototype parameter list against a list of
arguments given the argument types.
- Valid-fundef
- Validate a function definition.
- Valid-unary
- Validate a unary expression,
given the type of the sub-expression.
- Valid-init-declor
- Validate an initializer declarator.
- Valid-stringlit-list
- Validate a list of string literals.
- 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-c-char
- Validate a character of a character constant.
- Valid-funcall
- Validate a function call expression,
given the types of the sub-expressions.
- Valid-iconst
- Validate an integer constant.
- Valid-add-ord-objfuns-file-scope
- Add a list of ordinary identifiers
corresponding to objects or functions
to the file scope of a validation table.
- Valid-initer
- Validate an initializer.
- Valid-declor
- Validate a declarator.
- 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-update-ext
- Update the externals map with an identifier.
- Valid-ext-declon-list
- Validate a list of external declarations.
- Valid-ext-declon
- Validate an external declaration.
- Valid-univ-char-name
- Validate a universal character name.
- Valid-memberp
- Validate a member pointer expression,
given the type of the sub-expression.
- Valid-add-ord-file-scope
- Add an ordinary identifier
to the file scope of a validation table.
- Valid-var
- Validate a variable.
- Valid-s-char
- Validate a character of a string literal.
- Valid-decl-spec
- Validate a declaration specifier.
- Valid-cconst
- Validate a character constant.
- Valid-cast
- Validate a cast expression,
given the type denoted by the type name
and the type of the argument expression.
- 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-stringlit
- Validate a string literal.
- Valid-spec/qual
- Validate a specifier or qualifier.
- Valid-oct-escape
- Validate an octal escape.
- Valid-get-fresh-uid
- Get a fresh uid and update the table accordingly.
- Valid-param-declon
- Validate a parameter declaration.
- Valid-struct-declon
- Validate a structure declaration.
- Valid-struct-declor
- Validate a structure declarator.
- Valid-has-internalp
- Check whether an identifier has been declared with internal linkage
in the validation table.
- Valid-escape
- Validate an escape sequence.
- Valid-enum-const
- Validate an enumeration constant.
- Valid-gensel
- Validate a generic selection expression,
given the types for the components.
- Valid-const
- Validate a constant.
- Valid-desiniter-list
- Validate a list of zero or more
initializers with optional designations.
- Valid-designor
- Validate a designator.
- Valid-param-declor
- Validate a parameter declarator.
- Valid-dec/oct/hex-const
- Validate a decimal, octal, or hexadecimal constant.
- Valid-s-char-list
- Validate a list of characters of a string literal.
- Valid-decl-spec-list
- Validate a list of declaration specifiers.
- Valid-c-char-list
- Validate a list of characters of a character constant.
- Valid-member
- Validate a member expression,
given the type of the sub-expression.
- Valid-init-table
- Initial validation table.
- Valid-lookup-ord-file-scope
- Look up an ordinary identifier
in the file scope of a validation table.
- Valid-comp-stmt
- Validate a compound statement.
- Valid-spec/qual-list
- Validate a list of specifiers and qualifiers.
- Valid-lookup-ext
- Look up the validation information of an identifier in the
externals map.
- Valid-designor-list
- Validate a list of zero or more designators.
- Valid-fconst
- Validate a floating constant.
- Valid-block-item
- Validate a block item.
- Valid-struct-declor-list
- Validate a list structure declarators.
- Valid-genassoc-list
- Validate a list of generic associations.
- Valid-align-spec
- Validate an alignment specifier.
- Valid-enumer
- Validate an enumerator.
- Valid-declon
- Validate a declaration.
- Valid-simple-escape
- Validate a simple escape.
- Valid-enum-spec
- 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-expr-list
- Validate a list of expressions.
- Valid-block-item-list
- Validate a list of block items.
- Valid-absdeclor
- Validate an abstract declarator.
- Valid-struct-declon-list
- Validate a list of structure declarators.
- 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-dirabsdeclor-option
- Validate an optional direct abstract declarator.
- Valid-const-expr
- Validate a constant expression.
- Valid-init-declor-list
- Validate a list of initializer declarators.
- Valid-absdeclor-option
- Validate an optional abstract declarator.
- 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-table-num-scopes
- Number of scopes in a validation table.
- 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-declon-list
- Validate a list of declarations.
- Valid-empty-scope
- Empty validator scope.
