Generate a C expression from an ACL2 term that represents a structure array read.
(atc-gen-expr-struct-read-array fn index-term index-expr index-type index-events index-thm struct-term struct-expr struct-type struct-events struct-thm tag member elem-type flexiblep gin state) → (mv erp gout)
Function:
(defun atc-gen-expr-struct-read-array (fn index-term index-expr index-type index-events index-thm struct-term struct-expr struct-type struct-events struct-thm tag member elem-type flexiblep gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp index-term) (exprp index-expr) (typep index-type) (pseudo-event-form-listp index-events) (symbolp index-thm) (pseudo-termp struct-term) (exprp struct-expr) (typep struct-type) (pseudo-event-form-listp struct-events) (symbolp struct-thm) (identp tag) (identp member) (typep elem-type) (booleanp flexiblep) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-struct-read-array)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) (wrld (w state)) ((when (eq fn 'quote)) (reterr (raise "Internal error: QUOTE function."))) (term (cons fn (cons index-term (cons struct-term 'nil)))) ((unless (type-integerp index-type)) (reterr (msg "The reading of a ~x0 structure with array member ~x1 ~ is applied to an index expression term ~x2 returning ~x3, ~ but a C integer operand is expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." (type-struct tag) member index-term index-type))) ((unless (symbolp struct-term)) (reterr (raise "Internal error: ~ structure read ~x0 applied to non-variable ~x1." fn struct-term))) (index-uterm (untranslate$ index-term nil state))) (cond ((equal struct-type (type-struct tag)) (b* ((expr (make-expr-arrsub :arr (make-expr-member :target struct-expr :name member) :sub index-expr)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type elem-type :term term :events (append index-events struct-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (struct-tag-p (atc-type-to-recognizer struct-type gin.prec-tags)) ((mv okp-lemma-event okp-lemma-name thm-index names-to-avoid) (b* ((okp-lemma-name (pack gin.fn '-expr- gin.thm-index '-okp-lemma)) ((mv okp-lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix okp-lemma-name nil gin.names-to-avoid wrld)) (struct-tag (defstruct-info->fixtype (atc-tag-info->defstruct (atc-get-tag-info tag gin.prec-tags)))) (struct-tag-member-index-okp (packn-pos (list struct-tag '- (ident->name member) '-index-okp) struct-tag)) (okp-lemma-formula (cons struct-tag-member-index-okp (cons index-uterm 'nil))) (okp-lemma-formula (atc-contextualize okp-lemma-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (okp-lemma-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons gin.fn-guard '(if* test* declar assign)) 'nil)) (cons ':use (cons (cons ':guard-theorem (cons gin.fn 'nil)) 'nil))))) 'nil)) ((mv okp-lemma-event &) (evmac-generate-defthm okp-lemma-name :formula okp-lemma-formula :hints okp-lemma-hints :enable nil))) (mv okp-lemma-event okp-lemma-name (1+ gin.thm-index) names-to-avoid))) (exec-member-read-when-struct-tag-p-and-member-element (pack 'exec-member-read-when- struct-tag-p '-and- (ident->name member) '-element)) (index-typep (atc-type-to-recognizer index-type gin.prec-tags)) (cintegerp-when-index-type (pack 'cintegerp-when- index-typep)) (var-info (atc-get-var struct-term gin.inscope)) ((unless var-info) (reterr (raise "Internal error: variable ~x0 not found." struct-term))) (var-thm (atc-var-info->thm var-info)) (elem-typep (atc-type-to-recognizer elem-type gin.prec-tags)) (elem-typep-of-fn (packn-pos (list elem-typep '-of- fn) fn)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-arrsub-of-member (cons '(:e expr-kind) (cons '(:e expr-arrsub->arr) (cons '(:e expr-arrsub->sub) (cons '(:e expr-member->target) (cons '(:e expr-member->name) (cons index-thm (cons struct-thm (cons 'expr-valuep-of-expr-value (cons 'exec-arrsub-of-member-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons exec-member-read-when-struct-tag-p-and-member-element (cons cintegerp-when-index-type (cons okp-lemma-name (cons 'objdesignp-when-objdesign-optionp (cons 'objdesign-optionp-of-objdesign-of-var (cons var-thm (cons 'value-integer->get-when-cintegerp (cons elem-typep-of-fn 'nil)))))))))))))))))))) 'nil)) 'nil))) 'nil)) (objdes (cons 'objdesign-element (cons (cons 'objdesign-member (cons (cons 'objdesign-of-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name struct-term) 'nil)) 'nil)) (cons gin.compst-var 'nil))) (cons (cons 'ident (cons (cons 'quote (cons (ident->name member) 'nil)) 'nil)) 'nil))) (cons (cons 'integer-from-cinteger (cons index-term 'nil)) 'nil)))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr elem-type term term objdes gin.compst-var hints nil gin.prec-tags thm-index names-to-avoid state))) (retok (make-expr-gout :expr expr :type elem-type :term term :events (append index-events struct-events (list okp-lemma-event thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))) ((equal struct-type (type-pointer (type-struct tag))) (b* ((expr (make-expr-arrsub :arr (make-expr-memberp :target struct-expr :name member) :sub index-expr)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type elem-type :term term :events (append index-events struct-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) ((mv okp-lemma-event okp-lemma-name thm-index names-to-avoid) (b* ((okp-lemma-name (pack gin.fn '-expr- gin.thm-index '-okp-lemma)) ((mv okp-lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix okp-lemma-name nil gin.names-to-avoid wrld)) (struct-tag (defstruct-info->fixtype (atc-tag-info->defstruct (atc-get-tag-info tag gin.prec-tags)))) (struct-tag-member-index-okp (packn-pos (list struct-tag '- (ident->name member) '-index-okp) struct-tag)) (index-uterm (untranslate$ index-term nil state)) (okp-lemma-formula (if flexiblep (cons struct-tag-member-index-okp (cons index-uterm (cons struct-term 'nil))) (cons struct-tag-member-index-okp (cons index-uterm 'nil)))) (okp-lemma-formula (atc-contextualize okp-lemma-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (okp-lemma-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons gin.fn-guard '(if* test* declar assign)) 'nil)) (cons ':use (cons (cons ':guard-theorem (cons gin.fn 'nil)) 'nil))))) 'nil)) ((mv okp-lemma-event &) (evmac-generate-defthm okp-lemma-name :formula okp-lemma-formula :hints okp-lemma-hints :enable nil))) (mv okp-lemma-event okp-lemma-name (1+ gin.thm-index) names-to-avoid))) (struct-tag-p (atc-type-to-recognizer (type-pointer->to struct-type) gin.prec-tags)) (exec-memberp-read-when-struct-tag-p-and-member-element (pack 'exec-memberp-read-when- struct-tag-p '-and- (ident->name member) '-element)) (index-typep (atc-type-to-recognizer index-type gin.prec-tags)) (cintegerp-when-index-type (pack 'cintegerp-when- index-typep)) (elem-typep (atc-type-to-recognizer elem-type gin.prec-tags)) (elem-typep-of-fn (packn-pos (list elem-typep '-of- fn) fn)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-arrsub-of-memberp (cons '(:e expr-kind) (cons '(:e expr-arrsub->arr) (cons '(:e expr-arrsub->sub) (cons '(:e expr-memberp->target) (cons '(:e expr-memberp->name) (cons index-thm (cons struct-thm (cons 'expr-valuep-of-expr-value (cons 'exec-arrsub-of-memberp-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons exec-memberp-read-when-struct-tag-p-and-member-element (cons 'read-object-of-add-var (cons 'read-object-of-add-frame (cons cintegerp-when-index-type (cons okp-lemma-name (cons 'value-integer->get-when-cintegerp (cons elem-typep-of-fn 'nil))))))))))))))))))) 'nil)) 'nil))) 'nil)) (objdes (cons 'objdesign-element (cons (cons 'objdesign-member (cons (add-suffix-to-fn struct-term "-OBJDES") (cons (cons 'ident (cons (cons 'quote (cons (ident->name member) 'nil)) 'nil)) 'nil))) (cons (cons 'integer-from-cinteger (cons index-term 'nil)) 'nil)))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr elem-type term term objdes gin.compst-var hints nil gin.prec-tags thm-index names-to-avoid state))) (retok (make-expr-gout :expr expr :type elem-type :term term :events (append index-events struct-events (list okp-lemma-event thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))) (t (reterr (msg "The reading of ~x0 structure with array member ~x1 ~ is applied to an expression term ~x2 returning ~x3, ~ but an operand of type ~x4 or ~x5 is expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." tag member struct-term struct-type (type-struct tag) (type-pointer (type-struct tag)))))))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-struct-read-array.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-struct-read-array fn index-term index-expr index-type index-events index-thm struct-term struct-expr struct-type struct-events struct-thm tag member elem-type flexiblep gin state))) (expr-goutp gout)) :rule-classes :rewrite)