Code to generate the rules for executing assignments to array subscripting expressions.
We generate a rule for the large symbolic execution, and also a rule for the modular proofs. The former will be eventually eliminated, once modular proofs cover all the ATC constructs.
Function:
(defun atc-exec-expr-asg-arrsub-rules-gen (atype) (declare (xargs :guard (typep atype))) (declare (xargs :guard (type-nonchar-integerp atype))) (let ((__function__ 'atc-exec-expr-asg-arrsub-rules-gen)) (declare (ignorable __function__)) (b* ((afixtype (integer-type-to-fixtype atype)) (apred (pack afixtype '-arrayp)) (epred (pack afixtype 'p)) (atype-array-index-okp (pack afixtype '-array-index-okp)) (atype-array-write (pack afixtype '-array-write)) (value-array->elemtype-when-apred (pack 'value-array->elemtype-when- apred)) (value-array-read-when-apred (pack 'value-array-read-when- apred)) (value-array-write-when-apred (pack 'value-array-write-when- apred)) (name (pack 'exec-expr-asg-arrsub-when- apred)) (formula (cons 'implies (cons (cons 'and (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :arrsub) (cons '(equal arr (expr-arrsub->arr left)) (cons '(equal sub (expr-arrsub->sub left)) (cons '(equal (expr-kind arr) :ident) (cons '(equal var (expr-ident->get arr)) (cons '(not (zp limit)) (cons '(equal arr-val (read-var var compst)) (cons '(valuep arr-val) (cons '(equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (cons '(expr-valuep eptr) (cons '(equal ptr (expr-value->value eptr)) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (type-to-maker atype) 'nil))) (cons '(equal array (read-object (value-pointer->designator ptr) compst)) (cons (cons apred '(array)) (cons '(equal eindex (exec-expr-pure sub compst)) (cons '(expr-valuep eindex) (cons '(equal eindex1 (apconvert-expr-value eindex)) (cons '(expr-valuep eindex1) (cons '(equal index (expr-value->value eindex1)) (cons '(cintegerp index) (cons (cons atype-array-index-okp '(array index)) (cons '(equal eval (exec-expr-pure right compst)) (cons '(expr-valuep eval) (cons '(equal eval1 (apconvert-expr-value eval)) (cons '(expr-valuep eval1) (cons '(equal val (expr-value->value eval1)) (cons (cons epred '(val)) 'nil)))))))))))))))))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-object (cons '(value-pointer->designator ptr) (cons (cons atype-array-write '(array index val)) '(compst)))) 'nil))) 'nil)))) (event (cons 'defruled (cons name (cons formula (cons ':expand (cons '((exec-expr-pure (expr-binary->arg1 e) compst) (exec-expr-pure (expr-arrsub->arr (expr-binary->arg1 e)) compst)) (cons ':enable (cons (cons 'exec-expr-asg (cons 'exec-ident (cons 'exec-arrsub (cons 'apconvert-expr-value-when-not-value-array-alt (cons 'value-kind-not-array-when-cintegerp (cons 'read-object-of-objdesign-of-var-to-read-var (cons value-array->elemtype-when-apred (cons 'value-integer->get-when-cintegerp (cons atype-array-index-okp (cons 'integer-range-p (cons value-array-read-when-apred (cons value-array-write-when-apred '(write-object))))))))))))) (cons ':disable (cons '(equal-of-error equal-of-expr-value equal-of-objdesign-element) (cons ':prep-lemmas (cons (cons (cons 'defrule (cons 'lemma (cons (cons 'implies (cons (cons 'and (cons '(expr-valuep (apconvert-expr-value eval)) (cons (cons epred '((expr-value->value (apconvert-expr-value eval)))) 'nil))) (cons (cons epred '((expr-value->value eval))) 'nil))) '(:enable apconvert-expr-value)))) 'nil) 'nil)))))))))))) (name-mod-prf (pack name '-for-modular-proofs)) (formula-mod-prf (cons 'implies (cons (cons 'and (cons '(equal (expr-kind e) :binary) (cons '(equal (binop-kind (expr-binary->op e)) :asg) (cons '(equal left (expr-binary->arg1 e)) (cons '(equal right (expr-binary->arg2 e)) (cons '(equal (expr-kind left) :arrsub) (cons '(equal arr (expr-arrsub->arr left)) (cons '(equal sub (expr-arrsub->sub left)) (cons '(equal (expr-kind arr) :ident) (cons '(not (zp limit)) (cons '(equal arr-eval (exec-expr-pure arr compst)) (cons '(expr-valuep arr-eval) (cons '(equal ptr-eval (apconvert-expr-value arr-eval)) (cons '(expr-valuep ptr-eval) (cons '(equal ptr (expr-value->value ptr-eval)) (cons '(value-case ptr :pointer) (cons '(value-pointer-validp ptr) (cons (cons 'equal (cons '(value-pointer->reftype ptr) (cons (type-to-maker atype) 'nil))) (cons '(equal array (read-object (value-pointer->designator ptr) compst)) (cons (cons apred '(array)) (cons '(equal sub-eval (exec-expr-pure sub compst)) (cons '(expr-valuep sub-eval) (cons '(equal index-eval (apconvert-expr-value sub-eval)) (cons '(expr-valuep index-eval) (cons '(equal index (expr-value->value index-eval)) (cons '(cintegerp index) (cons (cons atype-array-index-okp '(array index)) (cons '(equal right-eval (exec-expr-pure right compst)) (cons '(expr-valuep right-eval) (cons '(equal eval (apconvert-expr-value right-eval)) (cons '(expr-valuep eval) (cons '(equal val (expr-value->value eval)) (cons (cons epred '(val)) 'nil))))))))))))))))))))))))))))))))) (cons (cons 'equal (cons '(exec-expr-asg e compst fenv limit) (cons (cons 'write-object (cons '(value-pointer->designator ptr) (cons (cons atype-array-write '(array index val)) '(compst)))) 'nil))) 'nil)))) (event-mod-prf (cons 'defruled (cons name-mod-prf (cons formula-mod-prf (cons ':enable (cons (cons name '(read-var-to-read-object-of-objdesign-of-var valuep-of-read-object-of-objdesign-of-var exec-expr-pure-when-ident-no-syntaxp exec-ident)) 'nil))))))) (mv name (list event event-mod-prf)))))
Theorem:
(defthm symbolp-of-atc-exec-expr-asg-arrsub-rules-gen.name (b* (((mv ?name ?events) (atc-exec-expr-asg-arrsub-rules-gen atype))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-expr-asg-arrsub-rules-gen.events (b* (((mv ?name ?events) (atc-exec-expr-asg-arrsub-rules-gen atype))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-expr-asg-arrsub-rules-gen-loop (atypes) (declare (xargs :guard (type-listp atypes))) (declare (xargs :guard (type-nonchar-integer-listp atypes))) (let ((__function__ 'atc-exec-expr-asg-arrsub-rules-gen-loop)) (declare (ignorable __function__)) (b* (((when (endp atypes)) (mv nil nil)) ((mv name events) (atc-exec-expr-asg-arrsub-rules-gen (car atypes))) ((mv more-names more-events) (atc-exec-expr-asg-arrsub-rules-gen-loop (cdr atypes)))) (mv (cons name more-names) (append events more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-expr-asg-arrsub-rules-gen-loop.names (b* (((mv ?names ?events) (atc-exec-expr-asg-arrsub-rules-gen-loop atypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-expr-asg-arrsub-rules-gen-loop.events (b* (((mv ?names ?events) (atc-exec-expr-asg-arrsub-rules-gen-loop atypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-expr-asg-arrsub-rules-gen-all nil (declare (xargs :guard t)) (let ((__function__ 'atc-exec-expr-asg-arrsub-rules-gen-all)) (declare (ignorable __function__)) (b* (((mv names events) (atc-exec-expr-asg-arrsub-rules-gen-loop *nonchar-integer-types*))) (cons 'progn (cons (cons 'defsection (cons 'atc-exec-expr-asg-arrsub-rules (cons ':short (cons '"Rules for executing assignment expressions to array subscript expressions." (append events (cons (cons 'defval (cons '*atc-exec-expr-asg-arrsub-rules* (cons (cons 'quote (cons (append names '((:e expr-kind) (:e expr-arrsub->arr) (:e expr-arrsub->sub) (:e expr-binary->op) (:e expr-binary->arg1) (:e expr-binary->arg2) (:e expr-ident->get) (:e binop-kind))) 'nil)) 'nil))) 'nil)))))) 'nil)))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-expr-asg-arrsub-rules-gen-all (b* ((event (atc-exec-expr-asg-arrsub-rules-gen-all))) (pseudo-event-formp event)) :rule-classes :rewrite)