Generate a C return statement from an ACL2 term.
(atc-gen-return-stmt term mvp gin state) → (mv erp 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
If
If instead
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
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
Function:
(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 'binary-+ (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 'binary-+ (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)) (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 expr.result (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 type-thms)))))))) '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 expr.result 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 expr.result 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:
(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)