		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.

The (non-event) macro input-files-prog provides a programmatic interface to the functionality of input-files.

General Form

(input-files :files             ...  ; required, no default
             :path              ...  ; default "."
             :preprocess        ...  ; default nil
             :preprocess-args   ...  ; default nil
             :process           ...  ; default :validate
             :const             ...  ; required, no default
             :keep-going        ...  ; default nil
             :std               ...  ; default 17
             :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 — required, no default

Term evaluating to a list of one or more file paths that specify the files to be read.
Each file path must be a string.
These paths are relative to the path specified by the :path input.

:path — default "."

Path that the file paths in :files are relative to.
This must be a non-empty string that is a valid path name in the system. It may or may not end with a slash. A non-absolute path is relative to the connected book directory (see cbd). In particular, the "." path (which is the default) specifies the connected book directory.

:preprocess — default nil

Specifies the preprocessor to use, if any, on the files specified by the :files and :path inputs.
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.
A string, which names the preprocessor to use, which must be in the current system path for executables.
:auto, which implicitly names the preprocessor "gcc", which must be in the current system path for executables.
The preprocessing (if this input is not nil), is performed via the preprocess-file tool.

:preprocess-args — default nil

Specifies arguments to pass to the preprocessor.
This must evaluate to a list of strings or to an omap from strings to lists of strings.
If :preprocess is nil, the :preprocess-args input must evaluate to nil.
If :preprocess is not nil, the input files are preprocessed. For each file, we provide the -E flag to the preprocessor, as well as some instantiation of the -std= flag. This latter flag is based on the combination of the :std and :gcc inputs, as indicated by the following table.
:gcc nil :gcc t
:std 17 -std=c17 -std=gnu17
:std 23 -std=c23 -std=gnu23
The :preprocess-args input specifies additional arguments to pass to the preprocessor beyond the two outlined above. If :preprocess-args is a string list, this list of arguments is passed to the preprocessor for each file, following the -E and ('-std=') arguments. If :preprocess-args is an omap, then we provide the list of arguments associated with the file name (again, after the -E and -std= arguments). A file in the :files list corresponds to a list of arguments in the map only when the file name matches the map key exactly (i.e., without prepending the :path). If the file name is not in the key set, only the -E and std= arguments are provided. If :preprocess-args is nil, it is technically both a string list and an omap from strings to string lists; the behavior is the same under either interpretation: only the -E and -std= arguments are provided for each file.

	:gcc nil	:gcc t
:std 17	-std=c17	-std=gnu17
:std 23	-std=c23	-std=gnu23

:process — default :validate

Specifies the processing to perform on the files specified by the :files and :path inputs (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:
: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, which annotated the abstract syntax with validation information.
These levels of processing are ordered as
: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 — required, no default

Name of the generated ACL2 constant whose value is the result of processing (and possibly preprocessing) the files specified in the :files and :path inputs.
If :process is :parse, the value of the constant named by :const is a code ensemble consisting of the translation unit ensemble resulting from the parser, paired with the implementation environment determined by the inputs described below. 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 code ensemble consisting of the translation unit ensemble resulting from the disambiguator, paired with the implementation environment determined by the inputs described below. This representation has no ambiguous constructs.
If :process is :validate, the value of the constant named by :const is a code ensemble consisting of the translation unit ensemble resulting from the validator, paired with the implementation environment determined by the inputs described below. This representation has no ambiguous constructs and is annotated with validation information.
In all cases, the keys of the translation unit ensemble map are the file paths specified in the :files input, without the :path prefix.
In the rest of this documentation page, let *const* be the name of this constant.

:keep-going — default nil

Boolean flag saying whether to keep going after failing to input a file. When t, files which fail parsing, disambiguation, or validation are dropped and the relevant error is printed. Furthermore, at the end of each stage, if any file has failed, then the fraction of successful files is also printed.
This flag is provided primarily for debugging purposes. Successful validation of later files following the first failure may be erroneous due to the inability to perform certain cross-checks against the dropped files.

:std — default 17

Either 17 or 23 saying which C standard should be used, namely C17 or C23.
Currently support for C23 is very limited, but it is being extended.

:gcc — default nil

Boolean flag 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 2, 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 4, 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.

Together, the inputs :std, :gcc, :short-bytes, :int-bytes, :long-bytes, :long-long-bytes, and :plain-char-signed determine an implementation environment. This is part of the code ensemble that is the value of the constant *const*.

Generated Events

*const*

The named constant containing the result of processing, as specified by :process, the files specified by the :files and :path inputs (if :preprocess is nil) or the files resulting from preprocessing those (if :preprocess is not nil).
This constant can be passed to output-files or to some transformation.

Subtopics

Input-files-implementation: Implementation of input-files.
Input-files-prog: Programmatic interface to input-files.