		Search-engine friendly clone of the ACL2 documentation.

Syntax-for-tools

Input-files

Read C files from the file system into an ACL2 representation.

Introduction

In the name of this macro, input is best read as a verb: the macro inputs files into ACL2.

This macro takes as input a list of file paths (which must contain C code), reads those files from the file system, and performs a user-specified level of processing on them, yielding a representation in ACL2 of that C code. This representation can be further processed, e.g. to perform code transformations, after which the macro output-files can be used to write the transformed code to the file system.

This macro currently does not perform very thorough input validation, but we plan to improve that.

General Form

(input-files :files              ...  ; no default
             :preprocess         ...  ; default nil
             :process            ...  ; default :disambiguate
             :const              ...  ; no default
             :const-files        ...  ; default nil
             :const-preproc      ...  ; default nil
             :const-parsed       ...  ; default nil
             :const-disamb       ...  ; default nil
             :gcc                ...  ; default nil
             :short-bytes        ...  ; default 2
             :int-bytes          ...  ; default 4
             :long-bytes         ...  ; default 8
             :long-long-bytes    ...  ; default 8
             :plain-char-signed  ... ; default nil
  )

Inputs

:files

List of zero or more file paths that specify the files to be read.
This must be a list of strings that are valid path names in the system. Non-absolute paths are relative to the connected book directory (see cbd).
This input to this macro is not evaluated.

:preprocess — default nil

Specifies the preprocessor to use, if any, on the files specified by the :files input.
This input must be one of the following:
nil (the default), in which case no preprocessing is done. In this case, the files must be already in preprocessed form, unless the :process input (see below) is nil.
A string, which names the preprocessor to use, which must be in the current path.
:auto, which implicitly names the preprocessor "cpp" (a common default), which must be in the current path.
The preprocessing (if this input is not nil), is performed via the preprocess-file tool.

:process — default :validate

Specifies the processing to perform on the files specified by the :files input (if :preprocess is nil) or on the result of preprocessing those files (if :preprocess is not nil).
This input must be one of the following:
:read, to perform no processing, i.e. just reading the files.
:parse, to parse the files into an abstract syntax representation, which may contain ambiguous constructs.
:disambiguate, to parse the files, and then to disambiguate the possibly ambiguous abstract syntax representation obtained from the parser into a non-ambiguous abstract syntax representation.
:validate (the default), to parse and disambiguate the files, and then to validate the disambiguated abstract syntax representation obtained from the disambiguator. Validation depends on the :short-bytes, :int-bytes, :long-bytes, :long-long-bytes, and :plain-char-signed inputs, which determine an implementation environment.
These levels of processing are ordered as
:read < :parse < :disambiguate < :validate
where a larger level includes and extends the processing of smaller levels. These processing levels are orthogonal to the preprocessing specified by :preprocess, since they apply equally to either the original or the preprocessed files.

:const

Name of the generated ACL2 constant whose value is the final result of processing (and preprocessing) the files specified in the :files input.
This must be a valid name for a new constant.
If :process is :read, the value of the constant named by :const is a file set (i.e. a value of type fileset), containing a representation of the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).
If :process is :parse, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code resulting from the parser. Since the parser captures ambiguous constructs without resolving them, this representation may include ambiguous constructs.
If :process is :disambiguate, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code obtained by disambiguating the one resulting from the parser.
If :process is :validate, the value of the constant named by :const is a translation unit ensemble (i.e. a value of type transunit-ensemble), containing the abstract syntax representation of the code obtained by disambiguating the one resulting from the parser, and such that the abstract syntax representation passed validation.
In the rest of this documentation page, let *const* be the name of this constant.

:const-files — default nil

Name of the generated ACL2 constant whose value is the file set (i.e. a value of type fileset) that represents the files specified by the :files input, as read from the file system, without preprocessing.
If this input is nil, this constant is not generated.
This input must be nil if :preprocess is nil and :process is :read, because in this case the constant would contain the same value as the one specified by :const.
In the rest of this documentation page, let *const-files* be the name of this constant, if not nil.

:const-preproc — default nil

Name of the generated ACL2 constant whole value is the file set (i.e. a value of type fileset) that represents the files obtained by preprocessing the files specified by the :files inputs.
If this input is nil, this constant is not generated.
This input must be nil if :preprocess is nil, because in that case there is no preprocessing. If a constant for the files is desired, the :const-files input can be used for that.
In the rest of this documentation page, let *const-preproc* be the name of this constant, if not nil.

:const-parsed — default nil

Name of the generated ACL2 constant whose value is the translation unit ensemble (i.e. a value of type transunit-ensemble) that represents the result of parsing the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).
If this input is nil, this constant is not generated.
This input must be nil if the :process input is :read, because in that case the files are not parsed.
This input must be nil if the :process input is :parse, because in that case this constant would contain the same value as the constant specified by the :const input.
In the rest of this documentation page, let *const-parsed* be the name of this constant, if not nil.

:const-disamb — default nil

Name of the generated ACL2 constant whose value is the translation unit ensemble (i.e. a value of type transunit-ensemble) that represents the result of parsing and disambiguating the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).
If this input is nil, this constant is not generated.
This input must be nil if the :process input is :read or :parse, because in that case the files are not parsed or disambiguated.
This input must be nil if the :process input is :disambiguate, because in that case this constant would contain the same value as the constant specified by the :const input.
In the rest of this documentation page, let *const-disamb* be the name of this constant, if not nil.

:gcc — default nil

Boolean saying whether certain GCC extensions should be accepted or not.

:short-bytes — default 2

Positive integer saying how many bytes are used to represent signed short int and unsigned short int.
This must be at least 2.

:int-bytes — default 4

Positive integer saying how many bytes are used to represent signed int and unsigned int.
This must be at least 4, and not less than :short-bytes.

:long-bytes — default 8

Positive integer saying how many bytes are used to represent signed long int and unsigned long int.
This must be at least 8, and not less than :int-bytes.

:long-long-bytes — default 8

Positive integer saying how many bytes are used to represent signed long long int and unsigned long long int.
This must be at least 8, and not less than :long-bytes.

:plain-char-signed — default nil

Boolean saying whether the plain char type consists of the same value as the signed char or unsigned char type.

Generated Events

*const*

The named constant containing the result of processing, as specified by :process, the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).

*const-files*

Optionally, the named constant containing the file set that represents the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).

*const-preproc*

Optionally, the named constant containing the file set that represents the result of preprocessing the files specified by :files.

*const-parsed*

Optionally, the named constant containing the abstract syntax representation, obtained from the parser without disambiguation, of the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).

*const-disamb*

Optionally, the named constant containing the abstract syntax representation, obtained from the disambiguator, of the files specified by :files (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).

Subtopics

Input-files-implementation: Implementation of input-files.