Generate a C expression from an ACL2 term that represents a structure scalar read.
(atc-gen-expr-struct-read-scalar fn arg-term arg-expr arg-type arg-events arg-thm tag member mem-type gin state) → (mv erp gout)
Function:
(defun atc-gen-expr-struct-read-scalar (fn arg-term arg-expr arg-type arg-events arg-thm tag member mem-type gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arg-term) (exprp arg-expr) (typep arg-type) (pseudo-event-form-listp arg-events) (symbolp arg-thm) (identp tag) (identp member) (typep mem-type) (expr-ginp gin)))) (declare (xargs :guard (type-nonchar-integerp mem-type))) (let ((__function__ 'atc-gen-expr-struct-read-scalar)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) (term (cons fn (cons arg-term 'nil))) ((unless (symbolp arg-term)) (reterr (raise "Internal error: ~ structure read ~x0 applied to non-variable ~x1." fn arg-term)))) (cond ((equal arg-type (type-struct tag)) (b* ((expr (make-expr-member :target arg-expr :name member)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type mem-type :term term :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (recognizer (atc-type-to-recognizer arg-type gin.prec-tags)) (exec-member-read-when-struct-tag-p-and-member (pack 'exec-member-read-when- recognizer '-and- (ident->name member))) (info (atc-get-var arg-term gin.inscope)) ((unless info) (reterr (raise "Internal error: variable ~x0 not found." arg-term))) (var-thm (atc-var-info->thm info)) (mem-typep (atc-type-to-recognizer mem-type gin.prec-tags)) (mem-typep-of-fn (packn-pos (list mem-typep '-of- fn) fn)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-member (cons '(:e expr-kind) (cons '(:e expr-member->target) (cons '(:e expr-member->name) (cons arg-thm (cons 'expr-valuep-of-expr-value (cons exec-member-read-when-struct-tag-p-and-member (cons 'exec-member-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons 'objdesign-option-fix-when-objdesign-optionp (cons 'objdesign-optionp-of-objdesign-of-var (cons var-thm (cons mem-typep-of-fn 'nil)))))))))))))) 'nil)) 'nil))) 'nil)) (objdes (cons 'objdesign-member (cons (cons 'objdesign-of-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name arg-term) 'nil)) 'nil)) (cons gin.compst-var 'nil))) (cons (cons 'ident (cons (cons 'quote (cons (ident->name member) 'nil)) '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 mem-type term term objdes gin.compst-var hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (retok (make-expr-gout :expr expr :type mem-type :term term :events (append arg-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))) ((equal arg-type (type-pointer (type-struct tag))) (b* ((expr (make-expr-memberp :target arg-expr :name member)) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type mem-type :term term :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (arg-type (type-pointer->to arg-type)) (recognizer (atc-type-to-recognizer arg-type gin.prec-tags)) (exec-memberp-read-when-struct-point-p-and-x (pack 'exec-memberp-read-when- recognizer '-and- (ident->name member))) (mem-typep (atc-type-to-recognizer mem-type gin.prec-tags)) (mem-typep-of-fn (packn-pos (list mem-typep '-of- fn) fn)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-memberp (cons '(:e expr-kind) (cons '(:e expr-memberp->target) (cons '(:e expr-memberp->name) (cons arg-thm (cons 'expr-valuep-of-expr-value (cons exec-memberp-read-when-struct-point-p-and-x (cons 'exec-memberp-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons 'read-object-of-add-var (cons 'read-object-of-add-frame (cons 'read-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'object-disjointp-commutative (cons mem-typep-of-fn 'nil)))))))))))))))) 'nil)) 'nil))) 'nil)) (objdes (cons 'objdesign-member (cons (add-suffix-to-fn arg-term "-OBJDES") (cons (cons 'ident (cons (cons 'quote (cons (ident->name member) 'nil)) '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 mem-type term term objdes gin.compst-var hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (retok (make-expr-gout :expr expr :type mem-type :term term :events (append arg-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))) (t (reterr (msg "The reading of a ~x0 structure with member ~x1 ~ is applied to ~ an expression term ~x2 returning ~x3, ~ but a 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 arg-term arg-type (type-struct tag) (type-pointer (type-struct tag)))))))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-struct-read-scalar.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-struct-read-scalar fn arg-term arg-expr arg-type arg-events arg-thm tag member mem-type gin state))) (expr-goutp gout)) :rule-classes :rewrite)