		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-fileset

Generate a file set from the ATC targets, and accompanying events.

Signature
(atc-gen-fileset targets path-wo-ext proofs prog-const wf-thm fn-thms header print names-to-avoid state) → (mv erp fileset events updated-names-to-avoid)
Arguments: targets — Guard (symbol-listp targets).; path-wo-ext — Guard (stringp path-wo-ext).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; wf-thm — Guard (symbolp wf-thm).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; header — Guard (booleanp header).; print — Guard (evmac-input-print-p print).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: fileset — Type (filesetp fileset).; events — Type (pseudo-event-form-listp events).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

This does not generate actual files in the file system: it generates an abstract syntactic C file set.

In order to speed up the proofs of the generated theorems for the function environment for relatively large C programs, we generate a theorem to ``cache'' the result of calling init-fun-env on the generated translation unit (obtained by preprocessing the generated C file set), to avoid recomputing that for every function environment theorem. We need to generate the name of this (local) theorem before generating the function environment theorems, so that those theorems can use the name of this theorem in the hints; but we can only generate the theorem after generating the translation unit. So first we generate the name, then we generate the translation unit, and then we generate the theorem; however, in the generated events, we put that theorem before the ones for the functions.

Definitions and Theorems

Function: atc-gen-fileset

(defun atc-gen-fileset (targets path-wo-ext
                                proofs prog-const wf-thm fn-thms
                                header print names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp targets)
                             (stringp path-wo-ext)
                             (booleanp proofs)
                             (symbolp prog-const)
                             (symbolp wf-thm)
                             (symbol-symbol-alistp fn-thms)
                             (booleanp header)
                             (evmac-input-print-p print)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-fileset))
   (declare (ignorable __function__))
   (b*
    (((reterr) (irr-fileset) nil nil)
     (wrld (w state))
     ((mv appcond-events
          fn-appconds appcond-thms names-to-avoid)
      (if proofs (b* (((mv appconds fn-appconds)
                       (atc-gen-appconds targets (w state)))
                      ((mv appcond-events
                           appcond-thms & names-to-avoid)
                       (evmac-appcond-theorem-list
                            appconds nil names-to-avoid print 'atc
                            state)))
                   (mv appcond-events fn-appconds
                       appcond-thms names-to-avoid))
        (mv nil nil nil nil)))
     (wf-thm-events (atc-gen-wf-thm proofs prog-const wf-thm print))
     (init-fun-env-thm (add-suffix-to-fn prog-const "-FUN-ENV"))
     ((mv init-fun-env-thm names-to-avoid)
      (fresh-logical-name-with-$s-suffix init-fun-env-thm
                                         nil names-to-avoid wrld))
     ((erp exts-h
           exts-c fn-thm-events names-to-avoid)
      (atc-gen-ext-declon-lists
           targets nil nil
           nil proofs prog-const init-fun-env-thm
           fn-thms fn-appconds appcond-thms
           header print names-to-avoid state))
     (file-h (and header (make-file :declons exts-h)))
     (file-c (make-file :declons exts-c))
     (fileset (make-fileset :path-wo-ext path-wo-ext
                            :dot-h file-h
                            :dot-c file-c))
     (init-fun-env-events
          (atc-gen-init-fun-env-thm init-fun-env-thm
                                    proofs prog-const fileset))
     (const-events
          (and proofs
               (atc-gen-prog-const prog-const fileset print)))
     (events (append appcond-events
                     const-events wf-thm-events
                     init-fun-env-events fn-thm-events)))
    (retok fileset events names-to-avoid))))

Theorem: filesetp-of-atc-gen-fileset.fileset

(defthm filesetp-of-atc-gen-fileset.fileset
  (b* (((mv acl2::?erp ?fileset
            ?events ?updated-names-to-avoid)
        (atc-gen-fileset targets path-wo-ext
                         proofs prog-const wf-thm fn-thms
                         header print names-to-avoid state)))
    (filesetp fileset))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-fileset.events

(defthm pseudo-event-form-listp-of-atc-gen-fileset.events
  (b* (((mv acl2::?erp ?fileset
            ?events ?updated-names-to-avoid)
        (atc-gen-fileset targets path-wo-ext
                         proofs prog-const wf-thm fn-thms
                         header print names-to-avoid state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-fileset.updated-names-to-avoid

(defthm symbol-listp-of-atc-gen-fileset.updated-names-to-avoid
  (implies
       (symbol-listp names-to-avoid)
       (b* (((mv acl2::?erp ?fileset
                 ?events ?updated-names-to-avoid)
             (atc-gen-fileset targets path-wo-ext
                              proofs prog-const wf-thm fn-thms
                              header print names-to-avoid state)))
         (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)