Preprocess a single file.
(preprocess-file file &key (out 'nil) (save ':auto) (read 't) (preprocessor '"cpp") (extra-args ''("-P")) (state 'state)) → (mv erp filename filedata state)
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
Function:
(defun preprocess-file-fn (file out save read preprocessor extra-args state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (filepathp 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 (filepath->unwrap file)) ((unless (stringp filename)) (reterr (msg "Filepath is not a string: ~x0" filename))) (canonical-filename (canonical-pathname filename nil state)) ((unless (stringp canonical-filename)) (reterr (msg "Filepath does not exist: ~x0" filename))) (filename canonical-filename) (- (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:
(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:
(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)