		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-return-stmt

Generate a C return statement from an ACL2 term.

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

The term passed here as parameter is the one representing the expression to be returned by the statement. This may come from two possible places (i.e. from two possible calls in atc-gen-stmt): when encountering a term (mv ret v1 ... vn) affecting variables v1, ..., vn, in which case ret is passed to this function and mvp is t; when encountering a term term that must be an expression term used as a statement term, in which case term is passed to this function and mvp is nil. The flag mvp is used to easily distinguish these two cases, which need slightly different treatment. Note that, in (mv ret v1 ... vn), ret may be either a pure expression term or a function call, and the same holds for the second case discussed above; thus, the two situations cannot be readily distinguished just by looking at the term alone.

If mvp is t, we call atc-gen-expr with term (i.e. ret) and we set the affected variables in gin to nil. In (mv ret v1 ... vn), ret must not affect any variables, which is guaranteed by ACL2 checks on multiple values, which cannot be nested: if ret affected variables, it would have to return multiple values, and could not be an argument of mv in ACL2.

If instead mvp is nil, we also call atc-gen-expr with term, but without modifying the affected variables in gin. This is because the term in question is the whole thing returned by the ACL2 function being translated to C at that point, and so it has to affect exactly the variables that the function affects.

We generate three theorems, which build upon each other: one for exec-stmt applied to the return statement, one for exec-block-item applied to the block item that consists of the return statement, and one for exec-block-item-list applied to the singleton list of that block item. It is the latter term that refers to the list of block items returned as the gout result of this ACL2 function. We start with the first of the three theorems, we will add the other two next.

The limit for the exec-stmt theorem is set to 1 more than the limit for the expression theorem, because we need 1 to go from exec-stmt to the :return case and exec-expr. The limit for the exec-block-item theorem is set to 1 more than the limit for the previous theorem, because we need 1 to go from exec-block-item to the :stmt case and exec-stmt. The limit for the exec-block-item-list theorem is set to 1 more than the limit for the previous theorem, because we need 1 to go from exec-block-item-list to exec-block-item. The limit returned from this ACL2 function is the latter, because it refers to exec-block-item-list.

Definitions and Theorems

Function: atc-gen-return-stmt

(defun atc-gen-return-stmt (term mvp gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (booleanp mvp)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-return-stmt))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-stmt-gout))
    ((stmt-gin gin) gin)
    (wrld (w state))
    ((erp expr.expr expr.type
          expr.term expr.result expr.new-compst
          expr.limit expr.events expr.thm-name
          & & expr.thm-index expr.names-to-avoid)
     (atc-gen-expr term
                   (if mvp (change-stmt-gin gin :affect nil)
                     gin)
                   state))
    ((when (type-case expr.type :void))
     (reterr (raise "Internal error: return term ~x0 has type void."
                    term)))
    ((when (type-case expr.type :array))
     (reterr
      (msg
       "When generating a return statement for function ~x0, ~
               the term ~x1 that represents the return expression ~
               has array type ~x2, which is disallowed."
       gin.fn term expr.type)))
    ((when (type-case expr.type :pointer))
     (reterr
      (msg
       "When generating a return statement for function ~x0, ~
               the term ~x1 that represents the return expression ~
               has pointer type ~x2, which is disallowed."
       gin.fn term expr.type)))
    (stmt (make-stmt-return :value expr.expr))
    (term (if mvp (acl2::make-cons-nest (cons expr.term gin.affect))
            expr.term))
    (uterm (untranslate$ term nil state))
    ((when (not expr.thm-name))
     (retok
      (make-stmt-gout
        :items (list (block-item-stmt stmt))
        :type expr.type
        :term term
        :context gin.context
        :inscope gin.inscope
        :limit
        (pseudo-term-fncall '+
                            (list (pseudo-term-quote 3) expr.limit))
        :events expr.events
        :thm-name nil
        :thm-index expr.thm-index
        :names-to-avoid expr.names-to-avoid)))
    (stmt-limit (pseudo-term-fncall '+
                                    (list (pseudo-term-quote 1)
                                          expr.limit)))
    (thm-index expr.thm-index)
    (names-to-avoid expr.names-to-avoid)
    (valuep-when-type-pred
         (atc-type-to-valuep-thm expr.type gin.prec-tags))
    (value-kind-when-type-pred
         (atc-type-to-value-kind-thm expr.type gin.prec-tags))
    (stmt-thm-name (pack gin.fn '-correct- thm-index))
    (thm-index (1+ thm-index))
    ((mv stmt-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          stmt-thm-name nil names-to-avoid wrld))
    (stmt-formula1
     (cons
         'equal
         (cons (cons 'exec-stmt
                     (cons (cons 'quote (cons stmt 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons (cons 'stmt-value-return
                                       (cons expr.result 'nil))
                                 (cons expr.new-compst 'nil)))
                     'nil))))
    (stmt-formula1
         (atc-contextualize stmt-formula1 gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var stmt-limit t wrld))
    ((mv stmt-formula2 type-thms)
     (atc-gen-term-type-formula
          uterm expr.type
          gin.affect gin.inscope gin.prec-tags))
    (stmt-formula2
         (atc-contextualize stmt-formula2 gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (stmt-formula (cons 'and
                        (cons stmt-formula1
                              (cons stmt-formula2 'nil))))
    (stmt-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-stmt-when-return
            (cons
             '(:e stmt-kind)
             (cons
              'not-zp-of-limit-variable
              (cons
               '(:e stmt-return->value)
               (cons
                'mv-nth-of-cons
                (cons
                 '(:e zp)
                 (cons
                  valuep-when-type-pred
                  (cons
                   expr.thm-name
                   (append
                    type-thms
                    (cons
                     'expr-valuep-of-expr-value
                     (cons
                      'expr-value->value-of-expr-value
                      (cons
                       'value-fix-when-valuep
                       (cons
                          'apconvert-expr-value-when-not-value-array
                          (cons value-kind-when-type-pred
                                'nil))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv stmt-event &)
     (evmac-generate-defthm stmt-thm-name
                            :formula stmt-formula
                            :hints stmt-hints
                            :enable nil))
    ((mv item item-limit item-events
         item-thm-name thm-index names-to-avoid)
     (atc-gen-block-item-stmt
          stmt stmt-limit
          (append expr.events (list stmt-event))
          stmt-thm-name uterm expr.type
          (cons 'stmt-value-return
                (cons expr.result 'nil))
          expr.new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid)
          state))
    (gout (atc-gen-block-item-list-one
               term expr.type item
               item-limit item-events item-thm-name
               (cons 'stmt-value-return
                     (cons expr.result 'nil))
               expr.new-compst gin.context nil
               (change-stmt-gin gin
                                :thm-index thm-index
                                :names-to-avoid names-to-avoid
                                :proofs (and item-thm-name t))
               state)))
   (retok gout))))

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

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