Rules about write-object.
The theorem about write-object turns it into update-object,
similarly to how write-var is turned into update-var.
The condition for the replacement is captured by
For now we only support top-level object designators, but we plan to extend things to other object designators.
Since update-object takes the base address,
the rules
We include the rule for commutativity of object-disjointp, so it does not matter the order of the disjoint objects in the hypotheses of the rules vs. the available hypothesis during the symbolic execution (i.e. commutativity normalizes them, via its loop stopper).
Function:
(defun write-object-okp (objdes val compst) (declare (xargs :guard (and (objdesignp objdes) (valuep val) (compustatep compst)))) (let ((__function__ 'write-object-okp)) (declare (ignorable __function__)) (b* (((unless (objdesign-case objdes :alloc)) nil) (addr (objdesign-alloc->get objdes)) (heap (compustate->heap compst)) (addr+obj (omap::assoc addr heap)) ((unless (consp addr+obj)) nil) (obj (cdr addr+obj)) ((unless (equal (type-of-value val) (type-of-value obj))) nil)) t)))
Theorem:
(defthm booleanp-of-write-object-okp (b* ((yes/no (write-object-okp objdes val compst))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm write-object-okp-of-objdesign-fix-objdes (equal (write-object-okp (objdesign-fix objdes) val compst) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-objdesign-equiv-congruence-on-objdes (implies (objdesign-equiv objdes objdes-equiv) (equal (write-object-okp objdes val compst) (write-object-okp objdes-equiv val compst))) :rule-classes :congruence)
Theorem:
(defthm write-object-okp-of-value-fix-val (equal (write-object-okp objdes (value-fix val) compst) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-value-equiv-congruence-on-val (implies (value-equiv val val-equiv) (equal (write-object-okp objdes val compst) (write-object-okp objdes val-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm write-object-okp-of-compustate-fix-compst (equal (write-object-okp objdes val (compustate-fix compst)) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (write-object-okp objdes val compst) (write-object-okp objdes val compst-equiv))) :rule-classes :congruence)
Theorem:
(defthm write-object-okp-of-add-frame (equal (write-object-okp objdes val (add-frame fun compst)) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-of-enter-scope (equal (write-object-okp objdes val (enter-scope compst)) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-of-add-var (equal (write-object-okp objdes val (add-var var val2 compst)) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-of-update-var (equal (write-object-okp objdes val (update-var var val2 compst)) (write-object-okp objdes val compst)))
Theorem:
(defthm write-object-okp-of-update-object-same (implies (equal (objdesign-kind objdes) :alloc) (equal (write-object-okp objdes val (update-object objdes val2 compst)) (equal (type-of-value val) (type-of-value val2)))))
Theorem:
(defthm write-object-okp-of-update-object-disjoint (implies (object-disjointp objdes objdes2) (equal (write-object-okp objdes val (update-object objdes2 val2 compst)) (write-object-okp objdes val compst))))
Theorem:
(defthm write-object-okp-when-valuep-of-read-object (implies (and (syntaxp (symbolp compst)) (equal (objdesign-kind objdes) :alloc) (equal old-val (read-object objdes compst)) (valuep old-val)) (equal (write-object-okp objdes val compst) (equal (type-of-value val) (type-of-value old-val)))))
Theorem:
(defthm write-object-okp-of-if*-val (implies (and (write-object-okp objdes b compst) (write-object-okp objdes c compst)) (write-object-okp objdes (if* a b c) compst)))
Theorem:
(defthm write-object-okp-when-valuep-of-read-object-no-syntaxp (implies (and (equal (objdesign-kind objdes) :alloc) (equal old-val (read-object objdes compst)) (valuep old-val)) (equal (write-object-okp objdes val compst) (equal (type-of-value val) (type-of-value old-val)))))
Theorem:
(defthm write-object-to-update-object (implies (write-object-okp objdes val compst) (equal (write-object objdes val compst) (update-object objdes val compst))))
Theorem:
(defthm write-object-of-objdesign-static (equal (write-object (objdesign-static var) val compst) (write-static-var var val compst)))