Generate a C block item statement that consists of an assignment to a pointed integer.
(atc-gen-block-item-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
Function:
(defun atc-gen-block-item-integer-asg (var val-term arg-term type integer-write-fn wrapper? gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (pseudo-termp val-term) (pseudo-termp arg-term) (typep type) (symbolp integer-write-fn) (symbolp wrapper?) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-integer-asg)) (declare (ignorable __function__)) (b* (((reterr) (irr-block-item) nil nil nil nil nil (irr-atc-context) 1 nil) (wrld (w state)) ((stmt-gin gin) gin) ((unless (eq wrapper? nil)) (reterr (msg "The pointed integer 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 pointed integer ~x0 is being written to, ~ but it is not among the variables ~x1 ~ currently affected." var gin.affect))) ((erp (expr-gout ptr)) (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)) ((unless (equal ptr.type (type-pointer type))) (reterr (msg "The variable ~x0 of type ~x1 does not have ~ the expected type ~x2. ~ This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var ptr.type (type-pointer type)))) ((erp (expr-gout int)) (atc-gen-expr-pure arg-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 ptr.thm-index :names-to-avoid ptr.names-to-avoid :proofs (and ptr.thm-name t)) state)) ((unless (equal int.type type)) (reterr (msg "The term ~x0 of type ~x1 does not have ~ the expected type ~x2. ~ This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." arg-term int.type type))) (asg (make-expr-binary :op (binop-asg) :arg1 (make-expr-unary :op (unop-indir) :arg ptr.expr) :arg2 int.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)))) ((when (eq integer-write-fn 'quote)) (reterr (raise "Internal error: integer writer is QUOTE."))) (integer-write-term (cons integer-write-fn (cons int.term 'nil))) (varinfo (atc-get-var var gin.inscope)) ((unless varinfo) (reterr (raise "Internal error: no information for variable ~x0." var))) ((when (not int.thm-name)) (retok item integer-write-term item-limit (append ptr.events int.events) nil gin.inscope gin.context int.thm-index int.names-to-avoid)) (new-compst (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons integer-write-term (cons gin.compst-var 'nil))))) (new-compst (untranslate$ new-compst nil state)) (asg-thm-name (pack gin.fn '-correct- int.thm-index)) ((mv asg-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix asg-thm-name nil int.names-to-avoid wrld)) (thm-index (1+ int.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)) (type-pred (atc-type-to-recognizer type gin.prec-tags)) (exec-expr-asg-thm (pack 'exec-expr-asg-indir-when- type-pred '-for-modular-proofs)) (value-kind-thm (atc-type-to-value-kind-thm type gin.prec-tags)) (valuep-when-type-pred (atc-type-to-valuep-thm type gin.prec-tags)) (type-of-value-thm (atc-type-to-type-of-value-thm type gin.prec-tags)) (type-pred-of-integer-write-fn (pack type-pred '-of- integer-write-fn)) (asg-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons exec-expr-asg-thm (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e expr-binary->arg1) (cons '(:e expr-binary->arg2) (cons '(:e binop-kind) (cons '(:e expr-unary->op) (cons '(:e expr-unary->arg) (cons '(:e unop-kind) (cons 'not-zp-of-limit-variable (cons '(:e expr-ident->get) (cons 'read-var-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons 'read-var-to-read-object-of-objdesign-of-var (cons (atc-var-info->thm varinfo) (cons ptr.thm-name (cons int.thm-name (cons 'expr-valuep-of-expr-value (cons 'apconvert-expr-value-when-not-value-array (cons value-kind-thm (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons 'write-object-to-update-object (cons 'write-object-okp-of-add-var (cons 'write-object-okp-of-add-frame (cons 'write-object-okp-when-valuep-of-read-object-no-syntaxp (cons type-of-value-thm (cons type-pred-of-integer-write-fn 'nil)))))))))))))))))))))))))))))) '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 ptr.events int.events (list asg-event)) asg-thm-name new-compst (change-stmt-gin gin :thm-index thm-index :names-to-avoid names-to-avoid :proofs t) state)) (new-context (atc-context-extend gin.context (list (make-atc-premise-cvalue :var var :term integer-write-term) (make-atc-premise-compustate :var gin.compst-var :term (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons var (cons gin.compst-var 'nil)))))))) (type-pred-of-type-write (pack type-pred '-of- (type-kind type) '-write)) (not-flexible-array-member-p-when-type-pred (pack 'not-flexible-array-member-p-when- type-pred)) (new-inscope-rules (cons 'objdesign-of-var-of-update-object-iff (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'read-var-of-update-object (cons 'compustate-frames-number-of-add-var-not-zero (cons 'read-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'object-disjointp-commutative (cons 'read-var-of-add-var (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-value-pointer (cons 'value-fix-when-valuep (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 type-pred-of-type-write (cons not-flexible-array-member-p-when-type-pred '(ident-fix-when-identp identp-of-ident equal-of-ident-and-ident (:e str-fix) read-var-of-update-object compustate-frames-number-of-enter-scope-not-zero read-var-of-enter-scope read-var-of-update-object compustate-frames-number-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 integer-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-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-integer-asg.val-term* (implies (symbolp integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (pseudo-termp val-term*))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (pseudo-termp limit)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-integer-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-integer-asg var val-term arg-term type integer-write-fn wrapper? gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)