Generate a C block item statement that consists of an assignment to an array element.
(atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
This is somewhat analogous to atc-gen-block-item-var-asg.
Function:
(defun atc-gen-block-item-array-asg (var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (pseudo-termp val-term) (pseudo-termp sub-term) (pseudo-termp elem-term) (typep elem-type) (symbolp array-write-fn) (symbolp wrapper?) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-array-asg)) (declare (ignorable __function__)) (b* (((reterr) (irr-block-item) nil nil nil nil nil (irr-atc-context) 1 nil) ((stmt-gin gin) gin) (wrld (w state)) ((unless (eq wrapper? nil)) (reterr (msg "The array write term ~x0 to which ~x1 is bound ~ has the ~x2 wrapper, which is disallowed." val-term var wrapper?))) ((unless (member-eq var gin.affect)) (reterr (msg "The array ~x0 is being written to, ~ but it is not among the variables ~x1 ~ currently affected." var gin.affect))) ((erp (expr-gout arr)) (atc-gen-expr-pure var (make-expr-gin :context gin.context :inscope gin.inscope :prec-tags gin.prec-tags :fn gin.fn :fn-guard gin.fn-guard :compst-var gin.compst-var :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid :proofs gin.proofs) state)) ((erp (expr-gout sub)) (atc-gen-expr-pure sub-term (make-expr-gin :context gin.context :inscope gin.inscope :prec-tags gin.prec-tags :fn gin.fn :fn-guard gin.fn-guard :compst-var gin.compst-var :thm-index arr.thm-index :names-to-avoid arr.names-to-avoid :proofs (and arr.thm-name t)) state)) ((erp (expr-gout elem)) (atc-gen-expr-pure elem-term (make-expr-gin :context gin.context :inscope gin.inscope :prec-tags gin.prec-tags :fn gin.fn :fn-guard gin.fn-guard :compst-var gin.compst-var :thm-index sub.thm-index :names-to-avoid sub.names-to-avoid :proofs (and sub.thm-name t)) state)) ((unless (and (type-case arr.type :array) (equal (type-array->of arr.type) elem-type))) (reterr (msg "The array ~x0 of type ~x1 ~ does not have the expected array type of ~x2. ~ This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var arr.type elem-type))) ((unless (type-integerp sub.type)) (reterr (msg "The array ~x0 of type ~x1 ~ is being indexed with ~ a subscript ~x2 of non-integer type ~x3, ~ instead of integer type as expected. This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var arr.type sub-term sub.type))) ((unless (equal elem.type elem-type)) (reterr (msg "The array ~x0 of type ~x1 ~ is being written to with ~ an element ~x2 of type x3, ~ instead of type ~x4 as expected. This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var arr.type elem-term elem.type elem-type))) (asg (make-expr-binary :op (binop-asg) :arg1 (make-expr-arrsub :arr arr.expr :sub sub.expr) :arg2 elem.expr)) (stmt (stmt-expr asg)) (item (block-item-stmt stmt)) (asg-limit ''1) (expr-limit (cons 'binary-+ (cons ''1 (cons asg-limit 'nil)))) (stmt-limit (cons 'binary-+ (cons ''1 (cons expr-limit 'nil)))) (item-limit (cons 'binary-+ (cons ''1 (cons stmt-limit 'nil)))) (varinfo (atc-get-var var gin.inscope)) ((unless varinfo) (reterr (raise "Internal error: no information for variable ~x0." var))) ((when (eq array-write-fn 'quote)) (reterr (raise "Internal error: array writer is QUOTE."))) (array-write-term (cons array-write-fn (cons var (cons sub.term (cons elem.term 'nil))))) ((when (not elem.thm-name)) (retok item array-write-term item-limit (append arr.events sub.events elem.events) nil gin.inscope gin.context elem.thm-index elem.names-to-avoid)) (okp-lemma-name (pack gin.fn '-asg- elem.thm-index '-okp-lemma)) ((mv okp-lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix okp-lemma-name nil elem.names-to-avoid wrld)) (thm-index (1+ elem.thm-index)) (elem-fixtype (pack (type-kind elem-type))) (index-okp (pack elem-fixtype '-array-index-okp)) (okp-lemma-formula (cons index-okp (cons var (cons sub.term '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)) (new-compst (if (atc-var-info->externalp varinfo) (cons 'update-static-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons array-write-term (cons gin.compst-var 'nil)))) (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons array-write-term (cons gin.compst-var 'nil)))))) (new-compst (untranslate$ new-compst nil state)) (asg-thm-name (pack gin.fn '-correct- thm-index)) ((mv asg-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix asg-thm-name nil names-to-avoid wrld)) (thm-index (1+ thm-index)) (asg-formula (cons 'equal (cons (cons 'exec-expr-asg (cons (cons 'quote (cons asg 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons new-compst 'nil)))) (asg-formula (atc-contextualize asg-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var asg-limit t wrld)) (exec-expr-asg-arrsub-when-elem-fixtype-arrayp-for-modular-proofs (pack 'exec-expr-asg-arrsub-when- elem-fixtype '-arrayp-for-modular-proofs)) (value-kind-when-sub-type-pred (atc-type-to-value-kind-thm sub.type gin.prec-tags)) (value-kind-when-elem-type-pred (atc-type-to-value-kind-thm elem-type gin.prec-tags)) (valuep-when-sub-type-pred (atc-type-to-valuep-thm sub.type gin.prec-tags)) (valuep-when-elem-type-pred (atc-type-to-valuep-thm elem-type gin.prec-tags)) (valuep-when-arr-type-pred (atc-type-to-valuep-thm arr.type gin.prec-tags)) (sub-type-pred (atc-type-to-recognizer sub.type gin.prec-tags)) (cintegerp-when-sub-type-pred (pack 'cintegerp-when- sub-type-pred)) (elem-fixtype-arrayp-of-elem-fixtype-array-write (pack elem-fixtype '-arrayp-of- elem-fixtype '-array-write)) (elem-fixtype-array-length-of-elem-fixtype-array-write (pack elem-fixtype '-array-length-of- elem-fixtype '-array-write)) (type-of-value-when-elem-fixtype-arrayp (atc-type-to-type-of-value-thm arr.type gin.prec-tags)) (value-array->length-when-elem-fixtype-arrayp (pack 'value-array->length-when- elem-fixtype '-arrayp)) (apconvert-expr-value-when-elem-fixtype-arrayp (pack 'apconvert-expr-value-when- elem-fixtype '-arrayp)) (return-type-of-type-elem-fixtype (pack 'return-type-of-type- elem-fixtype)) (asg-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons exec-expr-asg-arrsub-when-elem-fixtype-arrayp-for-modular-proofs (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e expr-binary->arg1) (cons '(:e expr-binary->arg2) (cons '(:e expr-arrsub->arr) (cons '(:e expr-arrsub->sub) (cons '(:e expr-ident->get) (cons '(:e binop-kind) (cons 'not-zp-of-limit-variable (cons arr.thm-name (cons 'expr-valuep-of-expr-value (cons 'apconvert-expr-value-when-not-value-array (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons (atc-var-info->thm varinfo) (cons sub.thm-name (cons value-kind-when-sub-type-pred (cons valuep-when-sub-type-pred (cons cintegerp-when-sub-type-pred (cons okp-lemma-name (cons elem.thm-name (cons value-kind-when-elem-type-pred (cons valuep-when-elem-type-pred (cons 'write-object-to-update-object (cons 'write-object-okp-when-valuep-of-read-object-no-syntaxp (cons valuep-when-arr-type-pred (cons elem-fixtype-arrayp-of-elem-fixtype-array-write (cons type-of-value-when-elem-fixtype-arrayp (cons value-array->length-when-elem-fixtype-arrayp (cons elem-fixtype-array-length-of-elem-fixtype-array-write (cons apconvert-expr-value-when-elem-fixtype-arrayp (cons 'objdesign-optionp-of-objdesign-of-var (cons 'objdesignp-when-objdesign-optionp (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 return-type-of-type-elem-fixtype '(value-pointer->designator-of-value-pointer pointer-valid->get-of-pointer-valid objdesign-fix-when-objdesignp write-object-of-objdesign-of-var-to-write-var write-var-to-write-static-var var-autop-of-add-frame var-autop-of-enter-scope var-autop-of-add-var var-autop-of-update-var var-autop-of-update-static-var var-autop-of-update-object write-static-var-to-update-static-var write-static-var-okp-of-add-var write-static-var-okp-of-enter-scope write-static-var-okp-of-add-frame write-static-var-okp-when-valuep-of-read-static-var read-object-of-objdesign-static ident-fix-when-identp identp-of-ident equal-of-ident-and-ident (:e str-fix)))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))) 'nil)) ((mv asg-event &) (evmac-generate-defthm asg-thm-name :formula asg-formula :hints asg-hints :enable nil)) ((mv item item-limit item-events item-thm-name thm-index names-to-avoid) (atc-gen-block-item-asg asg asg-limit (append arr.events sub.events elem.events (list okp-lemma-event asg-event)) asg-thm-name new-compst (change-stmt-gin gin :thm-index thm-index :names-to-avoid names-to-avoid :proofs (and asg-thm-name t)) state)) (new-context (atc-context-extend gin.context (list (make-atc-premise-cvalue :var var :term array-write-term) (make-atc-premise-compustate :var gin.compst-var :term (if (atc-var-info->externalp varinfo) (cons 'update-static-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons var (cons gin.compst-var 'nil)))) (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons var (cons gin.compst-var 'nil))))))))) (new-inscope-rules (cons 'objdesign-of-var-of-update-object (cons 'objdesign-of-var-of-enter-scope-iff (cons 'objdesign-of-var-of-add-var-iff (cons 'read-object-auto/static-of-update-object-alloc (cons 'read-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'read-object-of-objdesign-of-var-of-add-var (cons 'read-object-of-objdesign-of-var-of-enter-scope (cons 'objdesign-kind-of-objdesign-of-var (cons 'compustate-frames-number-of-add-var-not-zero (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'object-disjointp-commutative (cons 'value-fix-when-valuep (cons 'remove-flexible-array-member-when-absent (cons 'not-flexible-array-member-p-when-ucharp (cons 'not-flexible-array-member-p-when-scharp (cons 'not-flexible-array-member-p-when-ushortp (cons 'not-flexible-array-member-p-when-sshortp (cons 'not-flexible-array-member-p-when-uintp (cons 'not-flexible-array-member-p-when-sintp (cons 'not-flexible-array-member-p-when-ulongp (cons 'not-flexible-array-member-p-when-slongp (cons 'not-flexible-array-member-p-when-ullongp (cons 'not-flexible-array-member-p-when-sllongp (cons 'not-flexible-array-member-p-when-uchar-arrayp (cons 'not-flexible-array-member-p-when-schar-arrayp (cons 'not-flexible-array-member-p-when-ushort-arrayp (cons 'not-flexible-array-member-p-when-sshort-arrayp (cons 'not-flexible-array-member-p-when-uint-arrayp (cons 'not-flexible-array-member-p-when-sint-arrayp (cons 'not-flexible-array-member-p-when-ulong-arrayp (cons 'not-flexible-array-member-p-when-slong-arrayp (cons 'not-flexible-array-member-p-when-ullong-arrayp (cons 'not-flexible-array-member-p-when-sllong-arrayp (cons 'not-flexible-array-member-p-when-value-pointer (cons 'valuep-when-ucharp (cons 'valuep-when-scharp (cons 'valuep-when-ushortp (cons 'valuep-when-sshortp (cons 'valuep-when-uintp (cons 'valuep-when-sintp (cons 'valuep-when-ulongp (cons 'valuep-when-slongp (cons 'valuep-when-ullongp (cons 'valuep-when-sllongp (cons valuep-when-arr-type-pred (cons elem-fixtype-arrayp-of-elem-fixtype-array-write '(ident-fix-when-identp identp-of-ident equal-of-ident-and-ident (:e str-fix) objdesign-of-var-of-update-static-var-iff read-object-of-objdesign-of-var-of-update-static-var-different read-object-of-objdesign-of-var-of-update-static-var-same var-autop-of-add-frame var-autop-of-enter-scope var-autop-of-add-var var-autop-of-update-var var-autop-of-update-static-var var-autop-of-update-object))))))))))))))))))))))))))))))))))))))))))))))))) ((mv new-inscope new-inscope-events names-to-avoid) (atc-gen-new-inscope gin.fn gin.fn-guard gin.inscope new-context gin.compst-var new-inscope-rules gin.prec-tags thm-index names-to-avoid wrld)) (thm-index (1+ thm-index)) (events (append item-events new-inscope-events))) (retok item array-write-term item-limit events item-thm-name new-inscope new-context thm-index names-to-avoid))))
Theorem:
(defthm block-itemp-of-atc-gen-block-item-array-asg.item (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-array-asg.val-term* (implies (symbolp array-write-fn) (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (pseudo-termp val-term*))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-array-asg.limit (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (pseudo-termp limit)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-array-asg.events (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-array-asg.thm-name (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-array-asg.new-inscope (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-array-asg.new-context (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-array-asg.thm-index (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-array-asg.names-to-avoid (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)