Generate a C block item statement that consists of an assignment to a variable.
(atc-gen-block-item-var-asg var var-info? val-term gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
We increase the limit by one for the theorem about exec-expr-asg, because that is what it takes, in exec-expr-asg, to go to exec-expr-call-or-pure.
We further increase the limit by one for the theorem about exec-expr-call-or-asg, because that is what it takes, in exec-expr-call-or-asg, to go to exec-expr-asg.
We further increase the limit by one for the theorem about exec-stmt, because that is what it takes, in exec-stmt, to go to exec-expr-call-or-asg.
Function:
(defun atc-gen-block-item-var-asg (var var-info? val-term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (atc-var-info-optionp var-info?) (pseudo-termp val-term) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-var-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 var-info?) (reterr (raise "Internal error: no information for variable ~x0." var))) (var-info var-info?) (prev-type (atc-var-info->type var-info)) ((erp rhs.expr rhs.type rhs.term & & rhs.limit rhs.events rhs.thm-name & & rhs.thm-index rhs.names-to-avoid) (atc-gen-expr val-term (change-stmt-gin gin :affect nil) state)) ((unless (equal prev-type rhs.type)) (reterr (msg "The type ~x0 of the term ~x1 ~ assigned to the LET variable ~x2 ~ of the function ~x3 ~ differs from the type ~x4 ~ of a variable with the same symbol in scope." rhs.type val-term var gin.fn prev-type))) ((when (type-case rhs.type :array)) (reterr (msg "The term ~x0 to which the variable ~x1 is bound ~ must not have a C array type, ~ but it has type ~x2 instead." val-term var rhs.type))) ((when (type-case rhs.type :pointer)) (reterr (msg "The term ~x0 to which the variable ~x1 is bound ~ must not have a C pointer type, ~ but it has type ~x2 instead." val-term var rhs.type))) (asg (make-expr-binary :op (binop-asg) :arg1 (expr-ident (make-ident :name (symbol-name var))) :arg2 rhs.expr)) (stmt (stmt-expr asg)) (item (block-item-stmt stmt)) (asg-limit (cons 'binary-+ (cons ''1 (cons rhs.limit 'nil)))) (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 (not rhs.thm-name)) (retok item rhs.term item-limit rhs.events nil gin.inscope gin.context rhs.thm-index rhs.names-to-avoid)) (new-compst (if (atc-var-info->externalp var-info) (cons 'update-static-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons rhs.term (cons gin.compst-var 'nil)))) (cons 'update-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons rhs.term (cons gin.compst-var 'nil)))))) (new-compst (untranslate$ new-compst nil state)) (asg-thm-name (pack gin.fn '-correct- rhs.thm-index)) ((mv asg-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix asg-thm-name nil rhs.names-to-avoid wrld)) (thm-index (1+ rhs.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)) (valuep-when-type (atc-type-to-valuep-thm rhs.type gin.prec-tags)) (type-of-value-when-type (atc-type-to-type-of-value-thm rhs.type gin.prec-tags)) (asg-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-asg-ident-via-object (cons '(:e expr-kind) (cons '(:e expr-binary->op) (cons '(:e expr-binary->arg1) (cons '(:e expr-binary->arg2) (cons '(:e binop-kind) (cons 'not-zp-of-limit-variable (cons rhs.thm-name (cons 'mv-nth-of-cons (cons '(:e zp) (cons valuep-when-type (cons 'objdesign-of-var-of-const-identifier (cons '(:e identp) (cons '(:e ident->name) (cons '(:e expr-ident->get) (cons (atc-var-info->thm var-info) (cons 'write-object-of-objdesign-of-var-to-write-var (cons 'write-var-to-update-var (cons 'compustate-frames-number-of-add-var-not-zero (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'compustate-frames-number-of-add-frame-not-zero (cons 'compustate-frames-number-of-update-var (cons 'write-var-okp-of-add-var (cons 'write-var-okp-of-enter-scope (cons 'write-var-okp-of-update-var (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons 'equal-of-ident-and-ident (cons '(:e str-fix) (cons type-of-value-when-type '(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))))))))))))))))))))))))))))))) '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 rhs.events (list 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 rhs.term) (make-atc-premise-compustate :var gin.compst-var :term (if (atc-var-info->externalp var-info) (cons 'update-static-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons var (cons gin.compst-var 'nil)))) (cons 'update-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons var (cons gin.compst-var 'nil))))))))) (notflexarrmem-thms (atc-type-to-notflexarrmem-thms rhs.type gin.prec-tags)) (new-inscope-rules (cons rhs.thm-name (cons 'remove-flexible-array-member-when-absent (append notflexarrmem-thms (cons 'value-fix-when-valuep (cons valuep-when-type '(objdesign-of-var-of-update-var-iff read-object-of-objdesign-of-var-of-update-var 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 rhs.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-var-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-var-asg var var-info? val-term gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-var-asg.val-term* (implies (pseudo-termp val-term) (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-var-asg var var-info? val-term gin state))) (pseudo-termp val-term*))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (pseudo-termp limit)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-var-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-var-asg var var-info? val-term gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)