		Search-engine friendly clone of the ACL2 documentation.

Preprocessing

Preprocess-file

Preprocess a single file.

Signature
(preprocess-file file &key (out 'nil) (save ':auto) (read 't) (preprocessor '"cpp") (extra-args ''("-P")) (state 'state)) → (mv erp filename filedata state)
Arguments: file — The file path of the C file to preprocess.
Guard (stringp file).; out — This specifies the output file to which the preprocessed file is saved. If nil, a file will be created with a name and directory typical of temporary files (see oslib::tempfile).
Guard (or (not out) (stringp out)).; save — If t, the output file is saved. If nil, the file is removed after reading it in. If :auto, the default value, the file will be saved only if an explicit out value is provided.; read — If t, the output file will be read and returned. If you want the output file to be created but not read, pass nil. The default is t.; preprocessor — The preprocessor executable to use. The default is "cpp". Other reasonable values might be "gcc", "clang", "cc", etc.
Guard (stringp preprocessor).; extra-args — Arguments to pass to the C preprocessor, in addition to "-E". The default value is (list "-P") (the flag "-P" suppresses the generation of linemarkers).
Guard (string-listp extra-args).
Returns: erp — nil if successful, or the error msgp otherwise.; filename — The output filename if it is saved, or "" otherwise.
Type (stringp filename).; filedata — The preprocessed filedata if read, or (filedata nil) otherwise.
Type (filedatap filedata).

This function preprocesses a filepathp using the system's C preprocessor. See preprocess-files for a simlilar utility which handles a set of files.

By default, we pass the "-P" flag to the preprocessor to disable linemarkers. This behavior may be overriden by explicitly providing a :extra-args value.

Definitions and Theorems

Function: preprocess-file-fn

(defun preprocess-file-fn
       (file out
             save read preprocessor extra-args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp file)
                             (or (not out) (stringp out))
                             (stringp preprocessor)
                             (string-listp extra-args))))
 (let ((__function__ 'preprocess-file))
  (declare (ignorable __function__))
  (b*
   (((reterr) "" (filedata nil) state)
    (filename (canonical-pathname file nil state))
    ((unless (stringp filename))
     (reterr (msg "Filepath does not exist: ~x0" file)))
    (- (acl2::tshell-ensure))
    (save (if (eq :auto save) (and out t) save))
    ((erp out state)
     (b* (((reterr) nil state)
          ((when out)
           (retok (mbe :exec out
                       :logic (if (stringp out) out ""))
                  state))
          ((mv temp state)
           (oslib::tempfile filename))
          ((unless temp)
           (reterr (msg "Could not create temporary file for ~x0"
                        filename))))
       (retok temp state)))
    ((erp out-dirname state)
     (oslib::dirname out))
    ((erp state)
     (b* (((reterr) state)
          ((mv success state)
           (oslib::mkdir out-dirname))
          ((unless success)
           (reterr (msg "Could not make directory: ~x0"
                        out-dirname))))
       (retok state)))
    (preprocess-cmd
         (str::join (append (list* preprocessor "-E" extra-args)
                            (list filename ">" out))
                    " "))
    ((mv exit-status lines state)
     (acl2::tshell-call preprocess-cmd
                        :print nil))
    ((unless (int= 0 exit-status))
     (reterr
      (msg
       "Preprocessing command ~x0 failed with nonzero exit status: ~x1~%~x2"
       preprocess-cmd exit-status
       (str::join lines (string #\Newline)))))
    ((erp bytes state)
     (b* (((unless read) (retok nil state)))
       (acl2::read-file-into-byte-list out state)))
    ((when (stringp bytes))
     (reterr (msg "Error reading output file ~x0: ~x1"
                  out bytes)))
    ((erp state)
     (b* (((reterr) state)
          ((when save) (retok state))
          ((mv success state) (oslib::rmtree out))
          ((unless success)
           (reterr (msg "Could not remove output file: ~x0"
                        out))))
       (retok state))))
   (retok (if save out "")
          (filedata (and read bytes))
          state))))

Theorem: stringp-of-preprocess-file.filename

(defthm stringp-of-preprocess-file.filename
  (b* (((mv acl2::?erp
            ?filename ?filedata acl2::?state)
        (preprocess-file-fn file out save
                            read preprocessor extra-args state)))
    (stringp filename))
  :rule-classes :rewrite)

Theorem: filedatap-of-preprocess-file.filedata

(defthm filedatap-of-preprocess-file.filedata
  (b* (((mv acl2::?erp
            ?filename ?filedata acl2::?state)
        (preprocess-file-fn file out save
                            read preprocessor extra-args state)))
    (filedatap filedata))
  :rule-classes :rewrite)

Subtopics

Preprocess-files: Preprocess a set of files.