		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-wf-thm

Generate the theorem asserting the static well-formedness of the generated C code (referenced as the named constant).

Signature
(atc-gen-wf-thm proofs prog-const wf-thm print) → events
Arguments: proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; wf-thm — Guard (symbolp wf-thm).; print — Guard (evmac-input-print-p print).
Returns: events — Type (pseudo-event-form-listp events).

The theorem asserts that running the static semantics (i.e. check-fileset) on the C code succeeds. We also include an assertion that the C code is a fileset (i.e. that it satisfies filesetp); this does not directly follow from check-fileset, which fixes its argument to be a file set.

Since this is a ground theorem, we expect that it should be easily provable using just the executable counterparts of check-fileset and filesetp, which are executable functions.

Definitions and Theorems

Function: atc-gen-wf-thm

(defun atc-gen-wf-thm (proofs prog-const wf-thm print)
 (declare (xargs :guard (and (booleanp proofs)
                             (symbolp prog-const)
                             (symbolp wf-thm)
                             (evmac-input-print-p print))))
 (let ((__function__ 'atc-gen-wf-thm))
  (declare (ignorable __function__))
  (b*
   (((unless proofs) nil)
    ((mv local-event exported-event)
     (evmac-generate-defthm
         wf-thm
         :formula
         (cons 'and
               (cons (cons 'filesetp (cons prog-const 'nil))
                     (cons (cons 'equal
                                 (cons (cons 'check-fileset
                                             (cons prog-const 'nil))
                                       '(:wellformed)))
                           'nil)))
         :hints
         '(("Goal" :in-theory '((:e check-fileset) (:e filesetp))))
         :enable nil))
    (progress-start?
     (and
       (evmac-input-print->= print :info)
       '((cw-event "~%Generating the well-formedness theorem..."))))
    (progress-end? (and (evmac-input-print->= print :info)
                        '((cw-event " done.~%"))))
    (print-result?
     (and
      (evmac-input-print->= print :result)
      (cons
          (cons 'cw-event
                (cons '"~%~x0~|"
                      (cons (cons 'quote (cons exported-event 'nil))
                            'nil)))
          'nil))))
   (append progress-start?
           (list local-event exported-event)
           progress-end? print-result?))))

Theorem: pseudo-event-form-listp-of-atc-gen-wf-thm

(defthm pseudo-event-form-listp-of-atc-gen-wf-thm
  (b* ((events (atc-gen-wf-thm proofs prog-const wf-thm print)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)