		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-fundef

Generate a C function definition from a non-recursive ACL2 function, with accompanying theorems.

Signature
(atc-gen-fundef fn prec-fns prec-tags prec-objs proofs prog-const init-fun-env-thm fn-thms print names-to-avoid state) → (mv erp fundef events updated-prec-fns updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; init-fun-env-thm — Guard (symbolp init-fun-env-thm).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; print — Guard (evmac-input-print-p print).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: fundef — Type (fundefp fundef).; events — Type (pseudo-event-form-listp events).; updated-prec-fns — Type (atc-symbol-fninfo-alistp updated-prec-fns), given (atc-symbol-fninfo-alistp prec-fns).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

We ensure that all the formals affected by the function body have pointer or array types, as required in the user documentation.

We return local and exported events for the theorems about the correctness of the C function definition.

We extend the alist prec-fns with information about the function.

We use the type of the value returned by the statement for the body as the result type of the C function.

For the limit, we need 1 to go from exec-fun to exec-stmt, another 1 from there to exec-block-item-list in the :compound case, and then we use the limit for the block.

Definitions and Theorems

Function: atc-gen-fundef

(defun atc-gen-fundef (fn prec-fns prec-tags prec-objs
                          proofs prog-const init-fun-env-thm
                          fn-thms print names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (atc-symbol-fninfo-alistp prec-fns)
                             (atc-string-taginfo-alistp prec-tags)
                             (atc-string-objinfo-alistp prec-objs)
                             (booleanp proofs)
                             (symbolp prog-const)
                             (symbolp init-fun-env-thm)
                             (symbol-symbol-alistp fn-thms)
                             (evmac-input-print-p print)
                             (symbol-listp names-to-avoid))))
 (declare (xargs :guard (not (eq fn 'quote))))
 (let ((__function__ 'atc-gen-fundef))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-fundef) nil nil nil)
    (wrld (w state))
    (name (symbol-name fn))
    ((unless (paident-stringp name))
     (reterr
      (msg
       "The symbol name ~s0 of the function ~x1 ~
               must be a portable ASCII C identifier, but it is not."
       name fn)))
    ((mv fn-guard-event fn-guard names-to-avoid)
     (atc-gen-fn-guard fn names-to-avoid state))
    ((mv fn-def*-events fn-def* names-to-avoid)
     (atc-gen-fn-def* fn names-to-avoid wrld))
    ((erp typed-formals
          formals-events names-to-avoid)
     (atc-typed-formals fn fn-guard prec-tags
                        prec-objs names-to-avoid wrld))
    ((erp params)
     (atc-gen-param-declon-list typed-formals fn prec-objs))
    (formals (strip-cars typed-formals))
    (compst-var (genvar$ 'atc
                         "COMPST" nil formals state))
    (fenv-var (genvar$ 'atc "FENV" nil formals state))
    (limit-var (genvar$ 'atc
                        "LIMIT" nil formals state))
    (context-preamble
         (atc-gen-context-preamble typed-formals
                                   compst-var fenv-var prog-const))
    ((mv fn-fun-env-thm names-to-avoid)
     (atc-gen-cfun-fun-env-thm-name fn names-to-avoid wrld))
    ((mv init-scope-expand-event
         init-scope-expand-thm
         init-scope-scopep-event
         init-scope-scopep-thm omap-update-nest
         init-formals names-to-avoid)
     (atc-gen-init-scope-thms
          fn fn-guard
          typed-formals prec-tags context-preamble
          prog-const fn-fun-env-thm compst-var
          fenv-var names-to-avoid state))
    ((mv push-init-thm-event push-init-thm
         add-var-nest names-to-avoid)
     (atc-gen-push-init-thm fn fn-guard typed-formals prec-tags
                            context-preamble omap-update-nest
                            compst-var names-to-avoid wrld))
    (premises
         (list (make-atc-premise-compustate :var compst-var
                                            :term add-var-nest)))
    (context (make-atc-context :preamble context-preamble
                               :premises premises))
    ((mv inscope
         init-inscope-events names-to-avoid)
     (atc-gen-init-inscope fn fn-guard typed-formals prec-tags
                           compst-var context names-to-avoid wrld))
    (body (ubody+ fn wrld))
    ((erp affect)
     (atc-find-affected fn body typed-formals prec-fns wrld))
    ((unless (atc-formal-affectable-listp affect typed-formals))
     (reterr
      (msg
       "At least one of the formals of ~x0 ~
               that are affected by its body has a non-pointer non-array type, ~
               or does not refer to an external object. ~
               This is currently disallowed: ~
               only pointer or array variables,
               or variables that refer to external objects, ~
               may be affected by a non-recursive target function."
       fn)))
    ((erp (stmt-gout body))
     (atc-gen-stmt body
                   (make-stmt-gin :context context
                                  :var-term-alist nil
                                  :typed-formals typed-formals
                                  :inscope inscope
                                  :loop-flag nil
                                  :affect affect
                                  :fn fn
                                  :fn-guard fn-guard
                                  :compst-var compst-var
                                  :fenv-var fenv-var
                                  :limit-var limit-var
                                  :prec-fns prec-fns
                                  :prec-tags prec-tags
                                  :prec-objs prec-objs
                                  :thm-index 1
                                  :names-to-avoid names-to-avoid
                                  :proofs proofs)
                   state))
    (names-to-avoid body.names-to-avoid)
    ((when (and (type-case body.type :void)
                (not affect)))
     (reterr
      (raise
       "Internal error: ~
                 the function ~x0 returns void and affects no variables."
       fn)))
    ((unless (or (type-nonchar-integerp body.type)
                 (type-case body.type :struct)
                 (type-case body.type :void)))
     (reterr
      (raise
       "Internal error: ~
                 the function ~x0 has return type ~x1."
       fn body.type)))
    ((mv pop-frame-event
         pop-frame-thm names-to-avoid)
     (atc-gen-pop-frame-thm fn fn-guard
                            (untranslate$ body.term nil state)
                            body.type
                            body.thm-name affect typed-formals
                            compst-var prec-objs prec-tags
                            body.context names-to-avoid wrld))
    (id (make-ident :name name))
    ((mv tyspec &)
     (ident+type-to-tyspec+declor id body.type))
    (fundef
         (make-fundef :tyspec tyspec
                      :declor (make-fun-declor-base :name id
                                                    :params params)
                      :body body.items))
    (finfo (fun-info-from-fundef fundef))
    (limit (cons 'binary-+
                 (cons ''2 (cons body.limit 'nil))))
    (fn-fun-env-event
       (atc-gen-cfun-fun-env-thm fn fn-fun-env-thm
                                 prog-const finfo init-fun-env-thm))
    ((mv fn-result-events
         fn-result-thm names-to-avoid)
     (atc-gen-fn-result-thm fn body.type
                            affect typed-formals prec-fns prec-tags
                            prec-objs names-to-avoid state))
    ((mv fn-correct-events
         fn-correct-print-event fn-correct-thm
         fn-correct-lemma-thm names-to-avoid)
     (if body.thm-name
      (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals
                               affect typed-formals context-preamble
                               compst-var fenv-var limit-var fn-thms
                               fn-fun-env-thm init-scope-expand-thm
                               init-scope-scopep-thm push-init-thm
                               pop-frame-thm body.thm-name
                               body.type body.limit prec-tags
                               prec-objs names-to-avoid state)
      (b* (((mv events print-event name)
            (atc-gen-cfun-correct-thm
                 fn typed-formals body.type
                 affect prec-fns prec-tags prec-objs
                 prog-const compst-var fenv-var limit-var
                 fn-thms fn-fun-env-thm limit state)))
        (mv events
            print-event name nil names-to-avoid))))
    (progress-start?
        (and (evmac-input-print->= print :info)
             (cons (cons 'cw-event
                         (cons '"~%Generating the proofs for ~x0..."
                               (cons (cons 'quote (cons fn 'nil))
                                     'nil)))
                   'nil)))
    (progress-end? (and (evmac-input-print->= print :info)
                        '((cw-event " done.~%"))))
    (print-result? (and (evmac-input-print->= print :result)
                        (list fn-correct-print-event)))
    (local-events (append progress-start? (list fn-fun-env-event)
                          (list fn-guard-event)
                          fn-def*-events formals-events
                          (list init-scope-expand-event)
                          (list init-scope-scopep-event)
                          (list push-init-thm-event)
                          init-inscope-events body.events
                          (and body.thm-name (list pop-frame-event))
                          fn-result-events fn-correct-events
                          progress-end? print-result?))
    (info
      (make-atc-fn-info
           :out-type body.type
           :in-types
           (atc-var-info-list->type-list (strip-cdrs typed-formals))
           :loop? nil
           :affect affect
           :extobjs (atc-typed-formals-to-extobjs typed-formals)
           :result-thm fn-result-thm
           :correct-thm fn-correct-thm
           :correct-mod-thm fn-correct-lemma-thm
           :measure-nat-thm nil
           :fun-env-thm fn-fun-env-thm
           :limit limit
           :guard fn-guard)))
   (retok fundef (and proofs local-events)
          (acons fn info prec-fns)
          names-to-avoid))))

Theorem: fundefp-of-atc-gen-fundef.fundef

(defthm fundefp-of-atc-gen-fundef.fundef
  (b* (((mv acl2::?erp
            ?fundef ?events ?updated-prec-fns
            ?updated-names-to-avoid)
        (atc-gen-fundef fn prec-fns prec-tags prec-objs
                        proofs prog-const init-fun-env-thm
                        fn-thms print names-to-avoid state)))
    (fundefp fundef))
  :rule-classes :rewrite)

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

(defthm pseudo-event-form-listp-of-atc-gen-fundef.events
  (b* (((mv acl2::?erp
            ?fundef ?events ?updated-prec-fns
            ?updated-names-to-avoid)
        (atc-gen-fundef fn prec-fns prec-tags prec-objs
                        proofs prog-const init-fun-env-thm
                        fn-thms print names-to-avoid state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: atc-symbol-fninfo-alistp-of-atc-gen-fundef.updated-prec-fns

(defthm atc-symbol-fninfo-alistp-of-atc-gen-fundef.updated-prec-fns
  (implies
       (atc-symbol-fninfo-alistp prec-fns)
       (b* (((mv acl2::?erp
                 ?fundef ?events ?updated-prec-fns
                 ?updated-names-to-avoid)
             (atc-gen-fundef fn prec-fns prec-tags prec-objs
                             proofs prog-const init-fun-env-thm
                             fn-thms print names-to-avoid state)))
         (atc-symbol-fninfo-alistp updated-prec-fns)))
  :rule-classes :rewrite)

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

(defthm symbol-listp-of-atc-gen-fundef.updated-names-to-avoid
  (implies
       (symbol-listp names-to-avoid)
       (b* (((mv acl2::?erp
                 ?fundef ?events ?updated-prec-fns
                 ?updated-names-to-avoid)
             (atc-gen-fundef fn prec-fns prec-tags prec-objs
                             proofs prog-const init-fun-env-thm
                             fn-thms print names-to-avoid state)))
         (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)