Generate a C expression from an ACL2 term that represents an array read.
(atc-gen-expr-array-read fn arr-term arr-expr arr-type arr-events arr-thm sub-term sub-expr sub-type sub-events sub-thm elem-type gin state) → (mv erp gout)
We generate a theorem to show that the
Function:
(defun atc-gen-expr-array-read (fn arr-term arr-expr arr-type arr-events arr-thm sub-term sub-expr sub-type sub-events sub-thm elem-type gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arr-term) (exprp arr-expr) (typep arr-type) (pseudo-event-form-listp arr-events) (symbolp arr-thm) (pseudo-termp sub-term) (exprp sub-expr) (typep sub-type) (pseudo-event-form-listp sub-events) (symbolp sub-thm) (typep elem-type) (expr-ginp gin)))) (declare (xargs :guard (type-nonchar-integerp elem-type))) (let ((__function__ 'atc-gen-expr-array-read)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) (wrld (w state)) ((expr-gin gin) gin) ((unless (and (type-case arr-type :array) (equal (type-array->of arr-type) elem-type) (type-integerp sub-type))) (reterr (msg "The reading of a ~x0 array is applied to ~ an expression term ~x1 returning ~x2 ~ and to an expression term ~x3 returning ~x4, ~ but a ~x0 array and an integer operand are expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." elem-type arr-term arr-type sub-term sub-type))) (expr (make-expr-arrsub :arr arr-expr :sub sub-expr)) ((when (eq fn 'quote)) (reterr (raise "Internal error: function symbol is QUOTE."))) (term (cons fn (cons arr-term (cons sub-term 'nil)))) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type elem-type :term term :events (append arr-events sub-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) (elem-fixtype (integer-type-to-fixtype elem-type)) (fn-okp (pack elem-fixtype '-array-index-okp)) ((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)) (arr-uterm (untranslate$ arr-term nil state)) (sub-uterm (untranslate$ sub-term nil state)) (okp-lemma-formula (cons fn-okp (cons arr-uterm (cons sub-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-arrsub-when-elemtype-arrayp (pack 'exec-arrsub-when- elem-fixtype '-arrayp)) ((unless (symbolp arr-term)) (reterr (raise "Interal error: non-variable array ~x0." arr-term))) (info (atc-get-var arr-term gin.inscope)) ((unless info) (reterr (raise "Internal error: variable ~x0 not found in scope." arr-term))) (var-thm (atc-var-info->thm info)) (externalp (atc-var-info->externalp info)) ((unless (type-nonchar-integerp sub-type)) (reterr (raise "Internal error: non-integer index ~x0." sub-term))) (sub-fixtype (integer-type-to-fixtype sub-type)) (sub-type-pred (pack sub-fixtype 'p)) (cintegerp-when-type-pred (pack 'cintegerp-when- sub-type-pred)) (elem-type-pred-of-fn (pack elem-fixtype 'p-of- fn)) (apconvert-expr-value-when-elem-arrayp (pack 'apconvert-expr-value-when- elem-fixtype '-arrayp)) (return-type-of-elem-type (pack 'return-type-of-type- elem-fixtype)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-arrsub (cons '(:e expr-kind) (cons '(:e expr-arrsub->arr) (cons '(:e expr-arrsub->sub) (cons arr-thm (cons sub-thm (cons 'expr-valuep-of-expr-value (cons exec-arrsub-when-elemtype-arrayp (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons var-thm (cons cintegerp-when-type-pred (cons okp-lemma-name (cons elem-type-pred-of-fn (if externalp (cons apconvert-expr-value-when-elem-arrayp (cons 'objdesignp-when-objdesign-optionp (cons 'objdesign-optionp-of-objdesign-of-var (cons 'return-type-of-value-pointer (cons 'value-pointer-validp-of-value-pointer (cons 'return-type-of-pointer-valid (cons 'value-pointer->reftype-of-value-pointer (cons 'type-fix-when-typep (cons 'value-pointer->designator-of-value-pointer (cons 'pointer-valid->get-of-pointer-valid (cons 'objdesign-fix-when-objdesignp (cons return-type-of-elem-type 'nil)))))))))))) '(apconvert-expr-value-when-not-value-array)))))))))))))))) 'nil)) 'nil))) 'nil)) (objdes (if externalp (cons 'objdesign-element (cons (cons 'objdesign-of-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name arr-term) 'nil)) 'nil)) (cons gin.compst-var 'nil))) (cons (cons 'integer-from-cinteger (cons sub-term 'nil)) 'nil))) (cons 'objdesign-element (cons (add-suffix-to-fn arr-term "-OBJDES") (cons (cons 'integer-from-cinteger (cons sub-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 arr-events sub-events (list okp-lemma-event thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-array-read.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-array-read fn arr-term arr-expr arr-type arr-events arr-thm sub-term sub-expr sub-type sub-events sub-thm elem-type gin state))) (expr-goutp gout)) :rule-classes :rewrite)