|
|
|---|
|
|
|
|---|
Generate a C block item statement that consists of an assignment to an element of an array member of a structure.
(atc-gen-block-item-struct-array-asg
var val-term tag member-name
index-term elem-term elem-type flexiblep
struct-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.
The limit is set to 3 more than the sum of the limits for the left and right expression (the maximum would also work): 1 to go from exec-block-item to exec-stmt, 1 to go from there to exec-expr on the assignment, 1 to go from there to exec-expr on the left and right sides. The left side is an array subscript expression, so we need 1 to go to exec-expr on the sub-expressions; the array sub-expression is a struct member expression so it needs 1 more; the struct sub-expression is always a variable so it needs 1 more; then we add the limit needed for the index sub-expression.
Function:
(defun atc-gen-block-item-struct-array-asg (var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (pseudo-termp val-term) (identp tag) (identp member-name) (pseudo-termp index-term) (pseudo-termp elem-term) (typep elem-type) (booleanp flexiblep) (symbolp struct-write-fn) (symbolp wrapper?) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-struct-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 structure write term ~x0 ~ to which ~x1 is bound ~ has the ~x2 wrapper, which is disallowed." val-term var wrapper?))) ((erp (expr-gout struct)) (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 (member-equal struct.type (list (type-struct tag) (type-pointer (type-struct tag))))) (reterr (msg "The structure ~x0 of type ~x1 ~ does not have the expected type ~x2 or ~x3. ~ This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var struct.type (type-struct tag) (type-pointer (type-struct tag))))) (pointerp (type-case struct.type :pointer)) ((when (and pointerp (not (member-eq var gin.affect)))) (reterr (msg "The structure ~x0 ~ is being written to by pointer, ~ but it is not among the variables ~x1 ~ currently affected." var gin.affect))) ((erp (expr-gout index)) (atc-gen-expr-pure index-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 struct.thm-index :names-to-avoid struct.names-to-avoid :proofs (and struct.thm-name t)) state)) ((unless (type-integerp index.type)) (reterr (msg "The structure ~x0 of type ~x1 ~ is being written to with ~ an index ~x2 of type ~x3, ~ instead of a C integer type as expected. ~ This is indicative of ~ unreachable code under the guards, ~ given that the code is guard-verified." var struct.type index-term index.type))) ((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 index.thm-index :names-to-avoid index.names-to-avoid :proofs (and index.thm-name t)) state)) ((unless (equal elem.type elem-type)) (reterr (msg "The structure ~x0 of type ~x1 ~ is being written to with ~ a member array 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 struct.type elem-term elem.type elem-type))) (asg-mem (if pointerp (make-expr-memberp :target struct.expr :name member-name) (make-expr-member :target struct.expr :name member-name))) (asg (make-expr-binary :op (binop-asg) :arg1 (make-expr-arrsub :arr asg-mem :sub index.expr) :arg2 elem.expr)) (stmt (stmt-expr asg)) (item (block-item-stmt stmt)) ((unless (expr-purep index.expr)) (reterr (raise "Internal error: non-pure expression ~x0." index.expr))) ((unless (expr-purep elem.expr)) (reterr (raise "Internal error: non-pure expression ~x0." elem.expr))) (index-limit (cons 'quote (cons (expr-pure-limit index.expr) 'nil))) (left-limit (cons '+ (cons ''3 (cons index-limit 'nil)))) (right-limit (cons 'quote (cons (expr-pure-limit elem.expr) 'nil))) (expr-limit (cons '+ (cons ''1 (cons (cons '+ (cons left-limit (cons right-limit 'nil))) 'nil)))) (stmt-limit (cons '+ (cons ''1 (cons expr-limit 'nil)))) (item-limit (cons '+ (cons ''1 (cons stmt-limit 'nil)))) ((when (eq struct-write-fn 'quote)) (reterr (raise "Internal error: structure writer is QUOTE."))) (struct-write-term (cons struct-write-fn (cons index.term (cons elem.term (cons var 'nil))))) (varinfo (atc-get-var var gin.inscope)) ((unless varinfo) (reterr (raise "Internal error: no information for variable ~x0." var))) ((when (not elem.thm-name)) (retok item struct-write-term item-limit (append struct.events index.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)) (info (atc-get-tag-info tag gin.prec-tags)) (struct-tag (defstruct-info->fixtype (atc-tag-info->defstruct info))) (index-okp (packn-pos (list struct-tag '- (ident->name member-name) '-index-okp) struct-write-fn)) (okp-lemma-formula (if flexiblep (cons index-okp (cons index-term (cons var 'nil))) (cons index-okp (cons index-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 pointerp (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons struct-write-term (cons gin.compst-var 'nil)))) (cons 'update-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons struct-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)) (uterm (untranslate$ elem.term nil state)) (exec-formula (cons 'equal (cons (cons 'exec-expr (cons (cons 'quote (cons asg 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons (cons 'expr-value (cons uterm '(nil))) (cons new-compst 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var expr-limit t wrld)) (pred (atc-type-to-recognizer elem.type gin.prec-tags)) (type-formula (cons pred (cons uterm 'nil))) (type-formula (atc-contextualize type-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (asg-formula (cons 'and (cons exec-formula (cons type-formula 'nil)))) (exec-expr-when-asg-thms (atc-string-taginfo-alist-to-member-write-thms gin.prec-tags)) (valuep-when-elem-type-pred (atc-type-to-valuep-thm elem.type gin.prec-tags)) (valuep-when-index-type-pred (atc-type-to-valuep-thm index.type gin.prec-tags)) (value-kind-when-elem-type-pred (atc-type-to-value-kind-thm elem.type gin.prec-tags)) (value-kind-when-index-type-pred (atc-type-to-value-kind-thm index.type gin.prec-tags)) (index-type-pred (atc-type-to-recognizer index.type gin.prec-tags)) (cintegerp-when-index-type-pred (pack 'cintegerp-when- index-type-pred)) (valuep-thms (atc-string-taginfo-alist-to-valuep-thms gin.prec-tags)) (type-of-value-thms (atc-string-taginfo-alist-to-type-of-value-thms gin.prec-tags)) (writer-return-thms (atc-string-taginfo-alist-to-writer-return-thms gin.prec-tags)) (asg-hints (if pointerp (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (append exec-expr-when-asg-thms (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-memberp->target) (cons '(:e expr-memberp->name) (cons '(:e expr-ident->get) (cons '(:e binop-kind) (cons 'equal-of-const-and-ident (cons '(:e identp) (cons '(:e ident->name) (cons '(:e str-fix) (cons 'not-zp-of-limit-variable (cons 'not-zp-of-limit-minus-const (cons 'read-var-to-read-object-of-objdesign-of-var (cons (atc-var-info->thm varinfo) (cons 'objdesign-of-var-of-const-identifier (cons index.thm-name (cons elem.thm-name (cons 'expr-valuep-of-expr-value (cons 'apconvert-expr-value-when-not-value-array (cons valuep-when-elem-type-pred (cons valuep-when-index-type-pred (cons value-kind-when-elem-type-pred (cons value-kind-when-index-type-pred (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons cintegerp-when-index-type-pred (cons okp-lemma-name (cons 'write-object-to-update-object (cons 'write-object-okp-of-enter-scope (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 (append valuep-thms (append type-of-value-thms (append writer-return-thms '(compustatep-of-add-var compustatep-of-update-object expr-valuep-of-expr-value expr-value->value-of-expr-value value-fix-when-valuep (:e expr-pure-limit) (:e expr-purep) max))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))) 'nil) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (append exec-expr-when-asg-thms (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-member->target) (cons '(:e expr-member->name) (cons '(:e expr-ident->get) (cons '(:e binop-kind) (cons 'equal-of-const-and-ident (cons '(:e identp) (cons '(:e ident->name) (cons '(:e str-fix) (cons 'not-zp-of-limit-variable (cons 'not-zp-of-limit-minus-const (cons 'read-var-to-read-object-of-objdesign-of-var (cons (atc-var-info->thm varinfo) (cons 'objdesign-of-var-of-const-identifier (cons elem.thm-name (cons 'expr-valuep-of-expr-value (cons 'apconvert-expr-value-when-not-value-array (cons 'value-kind-when-sintp (cons 'expr-value->value-of-expr-value (cons 'value-fix-when-valuep (cons valuep-when-elem-type-pred (cons valuep-when-index-type-pred (cons cintegerp-when-index-type-pred (cons okp-lemma-name (cons index.thm-name (cons 'write-var-of-const-identifier (cons 'write-var-to-update-var (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'compustate-frames-number-of-add-var-not-zero (cons 'write-var-okp-of-enter-scope (cons 'write-var-okp-of-add-var (append type-of-value-thms (append writer-return-thms '(ident-fix-when-identp identp-of-ident equal-of-ident-and-ident compustate-frames-number-of-update-var write-var-okp-of-update-var compustatep-of-add-var compustatep-of-update-var expr-valuep-of-expr-value expr-value->value-of-expr-value value-fix-when-valuep (:e expr-pure-limit) (:e expr-purep) max)))))))))))))))))))))))))))))))))))))))) '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 expr-limit (append struct.events index.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 t) state)) (new-context (atc-context-extend gin.context (list (make-atc-premise-cvalue :var var :term struct-write-term) (make-atc-premise-compustate :var gin.compst-var :term (if pointerp (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (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 (type-struct tag) gin.prec-tags)) (value-kind-thms (atc-string-taginfo-alist-to-value-kind-thms gin.prec-tags)) (new-inscope-rules (if pointerp (cons 'objdesign-of-var-of-update-object-iff (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'read-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'read-var-of-update-object (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'read-var-of-enter-scope (cons 'compustate-frames-number-of-add-var-not-zero (cons 'compustate-frames-number-of-update-object (cons 'read-var-of-add-var (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 'read-object-of-update-object-same (cons 'remove-flexible-array-member-when-absent (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 (append valuep-thms (append writer-return-thms '(equal-of-ident-and-ident (:e str-fix) ident-fix-when-identp identp-of-ident expr-valuep-of-expr-value expr-value->value-of-expr-value value-fix-when-valuep))))))))))))))))))))))))))))))))))))) (cons 'objdesign-of-var-of-update-var-iff (cons 'read-object-of-objdesign-of-var-of-update-var (cons 'remove-flexible-array-member-when-absent (append notflexarrmem-thms (append value-kind-thms (cons 'value-fix-when-valuep (append valuep-thms (append writer-return-thms '(equal-of-ident-and-ident (:e str-fix) ident-fix-when-identp identp-of-ident expr-valuep-of-expr-value expr-value->value-of-expr-value value-fix-when-valuep))))))))))) ((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 struct-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-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-struct-array-asg.val-term* (implies (and (symbolp struct-write-fn) (pseudo-termp index-term) (pseudo-termp elem-term) (symbolp var)) (b* (((mv acl2::?erp ?item ?val-term* ?limit ?events ?thm-name ?new-inscope ?new-context ?thm-index ?names-to-avoid) (atc-gen-block-item-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (pseudo-termp val-term*))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (pseudo-termp limit)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (atc-symbol-varinfo-alist-listp new-inscope)) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (atc-contextp new-context)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (posp thm-index)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-block-item-struct-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-struct-array-asg var val-term tag member-name index-term elem-term elem-type flexiblep struct-write-fn wrapper? gin state))) (symbol-listp names-to-avoid)) :rule-classes :rewrite)