		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-stmt

Generate a C statement from an ACL2 term.

Signature
(atc-gen-stmt term gin state) → (mv erp gout)
Arguments: term — Guard (pseudo-termp term).; gin — Guard (stmt-ginp gin).
Returns: gout — Type (stmt-goutp gout).

At the same time, we check that the term is a statement term, as described in the user documentation.

If the term is a conditional, there are two cases. If the test is mbt, we recursively generate code just for the `then' branch, and then we delegate the rest to a separate function; note that we do not extend the context with the test, because the test is redundant, implied by the guard. If the test is not mbt, we generate an if statement (as a singleton block item list), with recursively generated compound statements as branches; the test expression is generated from the test term; we ensure that the two branches have the same type. When we process the branches, we extend the symbol table with a new empty scope for each branch. The calculation of the limit result is a bit more complicated in this case: we need 1 to go from exec-block-item-list to exec-block-item, another 1 to go from that to exec-stmt, and another 1 to go to the :if or :ifelse case there; the test is pure and so it needs no addition to the limit; since either branch may be taken, we return the sum of the limits for the two branches. More precisely, the limit recursively returned for each branch pertains to the block item list in the branch, but those are put into a compound statement; thus, we need to increase the recursively calculated limit by 1 to go from exec-block-item-list to exec-block-item, and another 1 to go from there to exec-stmt. In principle we could return the maximum from the two branches instead of their sum, but we want the limits to be linear combinations of sub-limits, so that ACL2's linear arithmetic can handle the reasoning about limits during the generated proofs.

If the term is a mv-let, there are three cases. If the term involves a declar<n> wrapper, we ensure that a variable with the same symbol name as the first bound variable is not already in scope (i.e. in the symbol table) and that the name is a portable ASCII identifier; we generate a declaration for the variable, initialized with the expression obtained from the term that the variable is bound to, which also determines the type of the variable, and which must affect the bound variables except the first one; the type must not be a pointer or array type (code generation fails if it is); we also ensure that the other variables are assignable. Otherwise, if the term involves an assign<n> wrapper, we ensure that the first bound variable is assignable, which implies that it must be in scope, and we also ensure that it has the same type as the one in scope; we generate an assignment whose right-hand side is obtained from the unwrapped term, which must be an expression term returning a C value that affects the bound variables except the first one; we also ensure that the other variables are assignable. Otherwise, if the term involves no wrapper, we ensure that the bound variables are all assignable, and that the non-wrapped term has the form described in the user documentation; we generate code that affects the variables from that term. In all cases, we recursively generate the block items for the body and we put those just after the preceding code. We use the sum of the two limits as the overall limit: thus, after exec-block-item-list executes the block items for the bound term, it still has enough limit to execute the block items for the body term.

If the term is a let, there are seven cases. If the binding has the form of a write to a pointed integer, we generate an assignment where the left-hand side uses the indirection unary operator. If the binding has the form of an array write, we generate an array assignment. If the binding has the form of a structure scalar member write, we generate an assignment to the member of the structure, by value or by pointer If the binding has the form of a structure array member write, we generate an assignment to the element of the member of the structure, by value or by pointer. The other three cases are similar to the three mv-let cases above. The limit is calculated as follows. For the case of the term representing code that affects variables, we add up the two limits, similarly to the mv-let case. For the other cases, we have one block item followed by block items. First, we need 1 to go from exec-block-item-list to exec-block-item. Then we take the sum of the limit for the first block item and the limit for the remaining block items (in principle we could take the maximum, but see the discussion above for if for why we take the sum instead). The first block item is a declaration, an assignment, or a function call. If it is a declaration, we need 1 to go from exec-block-item to the :declon case and to exec-expr-call-or-pure, for which we get the limit. If it is an assignment, we need 1 to go from exec-block-item to the :stmt case and to exec-stmt, another 1 to go from there to the :expr case and to exec-expr-call-or-asg, another 1 to fo from there to exec-expr-asg, and another 1 to go from there to exec-expr-call-or-pure, for which we recursively get the limit. For the remaining block items, we need to add another 1 to go from exec-block-item-list to its recursive call.

If the term is a single variable and affect is a singleton list with that variable, there are two cases: if the loop flag is t, it is an error; otherwise, we return nothing, because this is the end of a list of block items that affects that variable. We generate 1 as the limit, because we need 1 to go from exec-block-item-list to the empty list case.

If the term is an mv, there are three cases. If the loop flag is t, it is an error. Otherwise, if the arguments of mv are the affect variables, we return nothing, because this is the end of a list of block items that affects that variable; we return 1 as the limit, for the same reason as the case above. Otherwise, if the cdr of the arguments of mv are the affect variables, we treat the car of the arguments of mv as an expression term that must affect no variables, and generate a return statement for it.

If the term is a call of a recursive target function on its formals, different from the current function fn, then the term represents a loop. The loop flag must be nil for this to be allowed. We retrieve the associated loop statement and return it. We also retrieve the associated limit term, which, as explained in atc-fn-info, suffices to execute exec-stmt-while. But here we are executing lists of block items, so we need to add 1 to go from exec-block-item-list to the call to exec-block-item, another 1 to go from there to the call to exec-stmt, and another 1 to go from there to the call to exec-stmt-while.

If the term is a call of the current function fn on its formals, we ensure that the loop flag is t, and we generate no code. This represents the conclusion of a loop body (on some path).

If the term is a call of a non-recursive target function that returns void, the term represents an expression statement consisting of a call to the corresponding C function. The loop flag must be nil for this to be allowed. We ensure that all the pointer and array arguments are equal to the formals, and that the variables affected by the called function are correct. We retrieve the limit term associated to the called function, which, as explained in atc-fn-info, suffices to execute exec-fun. But here we are executing lists of block items, so we need to add 1 to go from exec-block-item-list to the call of exec-block-item, another 1 to go from there to the call of exec-stmt, another 1 to go from there to the call of exec-expr-call-or-asg, another 1 to go from there to the call of exec-expr-call, and another 1 to go from there to the call of exec-fun.

If the term does not have any of the forms above, we treat it as an expression term returning a C value. We ensure that the loop flag is nil. We also ensure that the expression affects the same variables as the statement term. For the limit, we need 1 to go from exec-block-item-list to exec-block-item, another 1 to go from there to the :stmt case and exec-stmt, another 1 to go from there to the :return case and exec-expr-call-or-pure, for which we use the recursively calculated limit.

Definitions and Theorems

Function: atc-gen-stmt

(defun atc-gen-stmt (term gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-stmt))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-stmt-gout))
    (wrld (w state))
    ((stmt-gin gin) gin)
    ((mv okp test-term then-term else-term)
     (fty-check-if-call term))
    ((when okp)
     (b*
      (((mv mbtp test-arg-term)
        (check-mbt-call test-term))
       ((when mbtp)
        (b*
         (((erp (stmt-gout then))
           (atc-gen-stmt then-term gin state))
          (gin (change-stmt-gin gin
                                :thm-index then.thm-index
                                :names-to-avoid then.names-to-avoid
                                :proofs (and then.thm-name t))))
         (atc-gen-mbt-block-items
              test-arg-term
              then.term else-term then.items then.type
              then.limit then.events then.thm-name
              then.context then.inscope gin state)))
       ((erp (expr-gout test))
        (atc-gen-expr-bool
             test-term
             (make-expr-gin :context gin.context
                            :inscope gin.inscope
                            :prec-tags gin.prec-tags
                            :fn gin.fn
                            :fn-guard gin.fn-guard
                            :compst-var gin.compst-var
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid
                            :proofs gin.proofs)
             state))
       ((erp (stmt-gout then)
             then-context-start then-context-end)
        (b*
         (((reterr)
           (irr-stmt-gout)
           (irr-atc-context)
           (irr-atc-context))
          (then-cond (untranslate$ test.term t state))
          (then-premise (atc-premise-test then-cond))
          (then-context-start
               (atc-context-extend gin.context (list then-premise)))
          ((mv then-inscope then-enter-scope-context
               then-enter-scope-events
               thm-index names-to-avoid)
           (if test.thm-name
               (atc-gen-enter-inscope
                    gin.fn gin.fn-guard
                    gin.inscope then-context-start
                    gin.compst-var gin.prec-tags
                    test.thm-index test.names-to-avoid wrld)
             (mv (cons nil gin.inscope)
                 then-context-start nil
                 test.thm-index test.names-to-avoid)))
          ((erp gout)
           (atc-gen-stmt
                then-term
                (change-stmt-gin gin
                                 :context then-enter-scope-context
                                 :inscope then-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and test.thm-name t))
                state))
          (then-context-end (stmt-gout->context gout)))
         (retok (change-stmt-gout
                     gout
                     :events (append then-enter-scope-events
                                     (stmt-gout->events gout)))
                then-context-start then-context-end)))
       ((erp (stmt-gout else)
             else-context-start else-context-end)
        (b*
         (((reterr)
           (irr-stmt-gout)
           (irr-atc-context)
           (irr-atc-context))
          (not-test-term (cons 'not (cons test.term 'nil)))
          (else-cond (untranslate$ not-test-term t state))
          (else-premise (atc-premise-test else-cond))
          (else-context-start
               (atc-context-extend gin.context (list else-premise)))
          ((mv else-inscope else-enter-scope-context
               else-enter-scope-events
               thm-index names-to-avoid)
           (if test.thm-name
               (atc-gen-enter-inscope
                    gin.fn gin.fn-guard
                    gin.inscope else-context-start
                    gin.compst-var gin.prec-tags
                    then.thm-index then.names-to-avoid wrld)
             (mv (cons nil gin.inscope)
                 else-context-start nil
                 then.thm-index then.names-to-avoid)))
          ((erp gout)
           (atc-gen-stmt
                else-term
                (change-stmt-gin gin
                                 :context else-enter-scope-context
                                 :inscope else-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and test.thm-name t))
                state))
          (else-context-end (stmt-gout->context gout)))
         (retok (change-stmt-gout
                     gout
                     :events (append else-enter-scope-events
                                     (stmt-gout->events gout)))
                else-context-start else-context-end))))
      (atc-gen-if/ifelse-stmt
       test.term
       then.term else.term test.expr then.items
       else.items test.type then.type else.type
       then.limit else.limit test.thm-name
       then.thm-name else.thm-name
       then-context-start else-context-start
       then-context-end else-context-end
       then.inscope else.inscope
       test.events then.events else.events
       (change-stmt-gin gin
                        :thm-index else.thm-index
                        :names-to-avoid else.names-to-avoid
                        :proofs (and test.thm-name
                                     then.thm-name else.thm-name t))
       state)))
    ((mv okp var? vars indices
         val-term body-term wrapper? mv-var)
     (atc-check-mv-let term))
    ((when okp)
     (b*
      ((all-vars (if var? (cons var? vars) vars))
       (val-instance (fty-fsublis-var gin.var-term-alist val-term))
       (vals (atc-make-mv-nth-terms indices val-instance))
       (var-term-alist-body (atc-update-var-term-alist
                                 all-vars vals gin.var-term-alist))
       ((when (eq wrapper? 'declar))
        (b*
         ((var var?)
          ((mv info? & errorp)
           (atc-check-var var gin.inscope))
          ((when errorp)
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           a new variable ~x1 has been encountered ~
                           that has the same symbol name as, ~
                           but different package name from, ~
                           a variable already in scope. ~
                           This is disallowed."
             gin.fn var)))
          ((when info?)
           (reterr
            (msg
             "The variable ~x0 in the function ~x1 ~
                           is already in scope and cannot be re-declared."
             var gin.fn)))
          ((unless (paident-stringp (symbol-name var)))
           (reterr
            (msg
             "The symbol name ~s0 of ~
                           the MV-LET variable ~x1 of the function ~x2 ~
                           must be a portable ASCII C identifier, ~
                           but it is not."
             (symbol-name var)
             var gin.fn)))
          ((mv info?-list innermostp-list)
           (atc-get-vars-check-innermost vars gin.inscope))
          ((when (member-eq nil info?-list))
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           an attempt is made to modify the variables ~x1, ~
                           not all of which are in scope."
             gin.fn vars)))
          ((unless
             (atc-vars-assignablep vars innermostp-list gin.affect))
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           an attempt is made to modify the variables ~x1, ~
                           not all of which are assignable."
             gin.fn vars)))
          ((erp init.expr
                init.type & & & init.limit init.events &
                & & init.thm-index init.names-to-avoid)
           (atc-gen-expr val-term
                         (change-stmt-gin gin :affect vars)
                         state))
          ((when (or (type-case init.type :pointer)
                     (type-case init.type :array)))
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           the term ~x1 of type ~x2 ~
                           is being assigned to a new variable ~x3. ~
                           This is currently disallowed, ~
                           because it would create an alias."
             gin.fn val-term init.type var)))
          ((erp)
           (atc-ensure-formals-not-lost
                vars gin.affect
                gin.typed-formals gin.fn wrld))
          ((mv tyspec declor)
           (ident+type-to-tyspec+declor
                (make-ident :name (symbol-name var))
                init.type))
          (declon
               (make-obj-declon :scspec (scspecseq-none)
                                :tyspec tyspec
                                :declor declor
                                :init? (initer-single init.expr)))
          (item (block-item-declon declon))
          (varinfo (make-atc-var-info :type init.type
                                      :thm nil
                                      :externalp nil))
          (inscope-body (atc-add-var var varinfo gin.inscope))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :var-term-alist var-term-alist-body
                                 :inscope inscope-body
                                 :thm-index init.thm-index
                                 :names-to-avoid init.names-to-avoid
                                 :proofs nil)
                state))
          (type body.type)
          (limit
           (pseudo-term-fncall
            'binary-+
            (list
               (pseudo-term-quote 3)
               (pseudo-term-fncall 'binary-+
                                   (list init.limit body.limit))))))
         (retok
            (make-stmt-gout :items (cons item body.items)
                            :type type
                            :term term
                            :context gin.context
                            :inscope gin.inscope
                            :limit limit
                            :events (append init.events body.events)
                            :thm-name nil
                            :thm-index body.thm-index
                            :names-to-avoid body.names-to-avoid))))
       ((when (eq wrapper? 'assign))
        (b*
         ((var var?)
          ((mv info? innermostp &)
           (atc-check-var var gin.inscope))
          ((unless info?)
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           an attempt is being made ~
                           to modify a variable ~x1 not in scope."
             gin.fn var)))
          ((unless (atc-var-assignablep var innermostp gin.affect))
           (reterr
            (msg
             "When generating C code for the function ~x0, ~
                           an attempt is being made ~
                           to modify a non-assignable variable ~x1."
             gin.fn var)))
          (prev-type (atc-var-info->type info?))
          ((erp rhs.expr
                rhs.type & & & rhs.limit rhs.events
                & & & rhs.thm-index rhs.names-to-avoid)
           (atc-gen-expr val-term
                         (change-stmt-gin gin :affect vars)
                         state))
          ((unless (equal prev-type rhs.type))
           (reterr
            (msg
             "The type ~x0 of the term ~x1 ~
                           assigned to the LET variable ~x2 ~
                           of the function ~x3 ~
                           differs from the type ~x4 ~
                           of a variable with the same symbol in scope."
             rhs.type
             val-term var gin.fn prev-type)))
          ((erp)
           (atc-ensure-formals-not-lost
                vars gin.affect
                gin.typed-formals gin.fn wrld))
          ((when (type-case rhs.type :array))
           (reterr
            (msg
             "The term ~x0 to which the variable ~x1 is bound ~
                           must not have a C array type, ~
                           but it has type ~x2 instead."
             val-term var rhs.type)))
          ((when (type-case rhs.type :pointer))
           (reterr
            (msg
             "The term ~x0 to which the variable ~x1 is bound ~
                           must not have a C pointer type, ~
                           but it has type ~x2 instead."
             val-term var rhs.type)))
          (asg
           (make-expr-binary
             :op (binop-asg)
             :arg1 (expr-ident (make-ident :name (symbol-name var)))
             :arg2 rhs.expr))
          (stmt (stmt-expr asg))
          (item (block-item-stmt stmt))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :var-term-alist var-term-alist-body
                                 :thm-index rhs.thm-index
                                 :names-to-avoid rhs.names-to-avoid
                                 :proofs nil)
                state))
          (type body.type)
          (limit
           (pseudo-term-fncall
            'binary-+
            (list
                (pseudo-term-quote 6)
                (pseudo-term-fncall 'binary-+
                                    (list rhs.limit body.limit))))))
         (retok
             (make-stmt-gout :items (cons item body.items)
                             :type type
                             :term term
                             :context gin.context
                             :inscope gin.inscope
                             :limit limit
                             :events (append rhs.events body.events)
                             :thm-name nil
                             :thm-index body.thm-index
                             :names-to-avoid body.names-to-avoid))))
       ((unless (eq wrapper? nil))
        (reterr (raise "Internal error: MV-LET wrapper is ~x0."
                       wrapper?)))
       ((mv info?-list innermostp-list)
        (atc-get-vars-check-innermost vars gin.inscope))
       ((when (member-eq nil info?-list))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     an attempt is made to modify the variables ~x1, ~
                     not all of which are in scope."
          gin.fn vars)))
       ((unless
             (atc-vars-assignablep vars innermostp-list gin.affect))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     an attempt is made to modify the variables ~x1, ~
                     not all of which are assignable."
          gin.fn vars)))
       ((unless
             (atc-affecting-term-for-let-p val-term gin.prec-fns))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     an MV-LET has been encountered ~
                     whose term ~x1 to which the variables are bound ~
                     does not have the required form."
          gin.fn val-term)))
       ((erp)
        (atc-ensure-formals-not-lost vars gin.affect
                                     gin.typed-formals gin.fn wrld))
       ((erp (stmt-gout xform))
        (atc-gen-stmt val-term
                      (change-stmt-gin gin
                                       :affect vars
                                       :loop-flag nil)
                      state))
       ((unless (type-case xform.type :void))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     an MV-LET has been encountered ~
                     whose term ~x1 to which the variables are bound ~
                     has the non-void type ~x2, ~
                     which is disallowed."
          gin.fn val-term xform.type)))
       ((erp (stmt-gout body))
        (atc-gen-stmt
             body-term
             (change-stmt-gin gin
                              :context xform.context
                              :inscope xform.inscope
                              :var-term-alist var-term-alist-body
                              :thm-index xform.thm-index
                              :names-to-avoid xform.names-to-avoid
                              :proofs (and xform.thm-name t))
             state))
       ((unless (equal (len all-vars) (len indices)))
        (reterr
         (raise
          "Internal error: ~
                       variables ~x0 and indices ~x1 ~
                       do not match in number."
          all-vars indices)))
       (term (acl2::close-lambdas
                  (acl2::make-mv-let-call
                       mv-var
                       all-vars indices xform.term body.term)))
       (items (append xform.items body.items))
       (type body.type)
       (limit (pseudo-term-fncall 'binary-+
                                  (list xform.limit body.limit))))
      (retok
           (make-stmt-gout :items items
                           :type type
                           :term term
                           :context gin.context
                           :inscope gin.inscope
                           :limit limit
                           :events (append xform.events body.events)
                           :thm-name nil
                           :thm-index body.thm-index
                           :names-to-avoid body.names-to-avoid))))
    ((mv okp var val-term body-term wrapper?)
     (atc-check-let term))
    ((when okp)
     (b*
      ((val-instance (fty-fsublis-var gin.var-term-alist val-term))
       (var-term-alist-body
            (atc-update-var-term-alist (list var)
                                       (list val-instance)
                                       gin.var-term-alist))
       ((erp okp fn arg-term type)
        (atc-check-integer-write val-term))
       ((when okp)
        (b*
         (((erp asg-item asg-term
                asg-limit asg-events asg-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-integer-asg
                var val-term
                arg-term type fn wrapper? gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and asg-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons asg-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term asg-item
                asg-limit asg-events asg-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((erp okp fn sub-term elem-term elem-type)
        (atc-check-array-write var val-term))
       ((when okp)
        (b*
         (((erp asg-item asg-term
                asg-limit asg-events asg-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-array-asg
                var val-term sub-term elem-term
                elem-type fn wrapper? gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and asg-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons asg-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term asg-item
                asg-limit asg-events asg-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((erp okp fn
             member-term tag member-name member-type)
        (atc-check-struct-write-scalar var val-term gin.prec-tags))
       ((when okp)
        (b*
         (((erp asg-item asg-term
                asg-limit asg-events asg-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-struct-scalar-asg
                var val-term tag member-name member-term
                member-type fn wrapper? gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and asg-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons asg-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term asg-item
                asg-limit asg-events asg-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((erp okp fn index-term elem-term
             tag member-name elem-type flexiblep)
        (atc-check-struct-write-array var val-term gin.prec-tags))
       ((when okp)
        (b*
         (((erp asg-item asg-term
                asg-limit asg-events asg-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-struct-array-asg
                var val-term tag member-name
                index-term elem-term elem-type
                flexiblep fn wrapper? gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and asg-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons asg-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term asg-item
                asg-limit asg-events asg-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((mv info? innermostp errorp)
        (atc-check-var var gin.inscope))
       ((when errorp)
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     a new variable ~x1 has been encountered ~
                     that has the same symbol name as, ~
                     but different package name from, ~
                     a variable already in scope. ~
                     This is disallowed."
          gin.fn var)))
       ((when (eq wrapper? 'declar))
        (b*
         (((erp decl-item decl-term decl-limit
                decl-events decl-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-var-decl
                var info? val-term gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and decl-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons decl-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term decl-item decl-limit
                decl-events decl-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((unless (atc-var-assignablep var innermostp gin.affect))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     an attempt is being made ~
                     to modify a non-assignable variable ~x1."
          gin.fn var)))
       ((when (eq wrapper? 'assign))
        (b*
         (((erp asg-item asg-term
                asg-limit asg-events asg-thm new-inscope
                new-context thm-index names-to-avoid)
           (atc-gen-block-item-var-asg
                var info? val-term gin state))
          ((erp (stmt-gout body))
           (atc-gen-stmt
                body-term
                (change-stmt-gin gin
                                 :context new-context
                                 :var-term-alist var-term-alist-body
                                 :inscope new-inscope
                                 :thm-index thm-index
                                 :names-to-avoid names-to-avoid
                                 :proofs (and asg-thm t))
                state))
          (term (acl2::close-lambdas
                     (cons (cons 'lambda
                                 (cons (cons var 'nil)
                                       (cons body.term 'nil)))
                           (cons asg-term 'nil))))
          (items-gout
           (atc-gen-block-item-list-cons
                term asg-item
                asg-limit asg-events asg-thm body.items
                body.limit body.events body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state)))
         (retok items-gout)))
       ((unless (eq wrapper? nil))
        (reterr (raise "Internal error: LET wrapper is ~x0."
                       wrapper?)))
       ((unless
             (atc-affecting-term-for-let-p val-term gin.prec-fns))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     we encountered a LET binding ~
                     of the variable ~x1 to the term ~x2 ~
                     that does not have any of the allowed forms. ~
                     See the user documentation."
          gin.fn var val-term)))
       ((erp)
        (atc-ensure-formals-not-lost (list var)
                                     gin.affect
                                     gin.typed-formals gin.fn wrld))
       ((erp (stmt-gout xform))
        (atc-gen-stmt val-term
                      (change-stmt-gin gin
                                       :affect (list var)
                                       :loop-flag nil)
                      state))
       ((unless (type-case xform.type :void))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     a LET has been encountered ~
                     whose unwrapped term ~x1 ~
                     to which the variable is bound ~
                     has the non-void type ~x2, ~
                     which is disallowed."
          gin.fn val-term xform.type)))
       ((erp (stmt-gout body))
        (atc-gen-stmt
             body-term
             (change-stmt-gin gin
                              :context xform.context
                              :inscope xform.inscope
                              :var-term-alist var-term-alist-body
                              :thm-index xform.thm-index
                              :names-to-avoid xform.names-to-avoid
                              :proofs (and xform.thm-name t))
             state))
       (term (acl2::close-lambdas
                  (cons (cons 'lambda
                              (cons (cons var 'nil)
                                    (cons body.term 'nil)))
                        (cons xform.term 'nil)))))
      (if
       (consp body.items)
       (retok
           (atc-gen-block-item-list-append
                term xform.items body.items
                xform.limit body.limit xform.events
                body.events xform.thm-name body.thm-name
                body.type body.context body.inscope
                (change-stmt-gin gin
                                 :thm-index body.thm-index
                                 :names-to-avoid body.names-to-avoid
                                 :proofs (and body.thm-name t))
                state))
       (retok (change-stmt-gout xform :term term)))))
    ((when (and (pseudo-term-case term :var)
                (equal gin.affect
                       (list (pseudo-term-var->name term)))))
     (if gin.loop-flag
      (reterr
       (msg
        "A loop body must end with ~
                   a recursive call on every path, ~
                   but in the function ~x0 it ends with ~x1 instead."
        gin.fn term))
      (retok (atc-gen-block-item-list-none term gin state))))
    ((mv okp terms)
     (fty-check-list-call term))
    ((when okp)
     (b*
      (((unless (>= (len terms) 2))
        (reterr (raise "Internal error: MV applied to ~x0."
                       terms)))
       ((when gin.loop-flag)
        (reterr
         (msg
          "A loop body must end with ~
                     a recursive call on every path, ~
                     but in the function ~x0 it ends with ~x1 instead."
          gin.fn term))))
      (cond
       ((equal terms gin.affect)
        (retok
          (atc-gen-block-item-list-none (acl2::make-cons-nest terms)
                                        gin state)))
       ((equal (cdr terms) gin.affect)
        (atc-gen-return-stmt (car terms)
                             t gin state))
       (t
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     a term ~x0 has been encountered, ~
                     which is disallowed."
          gin.fn term))))))
    ((mv okp loop-fn loop-args in-types
         loop-affect loop-stmt loop-limit)
     (atc-check-loop-call term gin.var-term-alist gin.prec-fns))
    ((when okp)
     (b*
      (((when gin.loop-flag)
        (reterr
         (msg
          "A loop body must end with ~
                     a recursive call on every path, ~
                     but in the function ~x0 it ends with ~x1 instead."
          gin.fn term)))
       (formals (formals+ loop-fn wrld))
       ((unless (equal formals loop-args))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     a call of the recursive function ~x1 ~
                     has been encountered ~
                     that is not on its formals, ~
                     but instead on the arguments ~x2.
                     This is disallowed; see the ATC user documentation."
          gin.fn loop-fn loop-args)))
       ((unless (equal gin.affect loop-affect))
        (reterr
         (msg
          "When generating C code for the function ~x0, ~
                     a call of the recursive function ~x1 ~
                     has been encountered
                     that represents a loop affecting ~x2, ~
                     which differs from the variables ~x3 ~
                     being affected here."
          gin.fn loop-fn loop-affect gin.affect)))
       (infos (atc-get-vars formals gin.inscope))
       ((unless (atc-var-info-listp infos))
        (reterr
         (raise
          "Internal error: not all formals ~x0 have information ~x1."
          formals infos)))
       (types (atc-var-info-list->type-list infos))
       ((unless (equal types in-types))
        (reterr
         (msg
          "The loop function ~x0 with input types ~x1 ~
                     is applied to terms ~x2 returning ~x3. ~
                     This is indicative of dead code under the guards, ~
                     given that the code is guard-verified."
          loop-fn in-types formals types)))
       (limit (pseudo-term-fncall 'binary-+
                                  (list (pseudo-term-quote 3)
                                        loop-limit))))
      (retok
           (make-stmt-gout :items (list (block-item-stmt loop-stmt))
                           :type (type-void)
                           :term term
                           :context gin.context
                           :inscope gin.inscope
                           :limit limit
                           :events nil
                           :thm-name nil
                           :thm-index gin.thm-index
                           :names-to-avoid gin.names-to-avoid))))
    ((when (equal term
                  (cons gin.fn (formals+ gin.fn wrld))))
     (if gin.loop-flag
         (retok (make-stmt-gout :items nil
                                :type (type-void)
                                :term term
                                :context gin.context
                                :inscope gin.inscope
                                :limit (pseudo-term-quote 1)
                                :events nil
                                :thm-name nil
                                :thm-index gin.thm-index
                                :names-to-avoid gin.names-to-avoid))
      (reterr
       (msg
        "When generating code for the recursive function ~x0, ~
                 a recursive call to the loop function occurs ~
                 not at the end of the computation on some path."
        gin.fn))))
    ((erp okp
          called-fn arg-terms in-types out-type
          fn-affect extobjs limit called-fn-guard)
     (atc-check-cfun-call term
                          gin.var-term-alist gin.prec-fns wrld))
    ((when (and okp (type-case out-type :void)))
     (atc-gen-cfun-call-stmt called-fn
                             arg-terms in-types fn-affect extobjs
                             limit called-fn-guard gin state))
    ((when gin.loop-flag)
     (reterr
      (msg
       "A loop body must end with ~
               a recursive call on every path, ~
               but in the function ~x0 it ends with ~x1 instead."
       gin.fn term))))
   (atc-gen-return-stmt term nil gin state))))

Theorem: stmt-goutp-of-atc-gen-stmt.gout

(defthm stmt-goutp-of-atc-gen-stmt.gout
  (b* (((mv acl2::?erp ?gout)
        (atc-gen-stmt term gin state)))
    (stmt-goutp gout))
  :rule-classes :rewrite)