Rules about update-object.
We have rules to unconditionally push update-object through all the layers except update-object.
When update-object is applied to update-object,
we have rules similar to the ones for update-var.
If the two object designators are the same, we overwrite the object.
When the object designators differ,
we swap the update-vars
if the right pointer is smaller than the left one,
where smaller is a syntactic check:
when the two pointer arguments are symbols
(which happens in the proofs of C functions),
we compare the symbols;
when the two pointer arguments are read-var calls
(which happens in the proofs of C loops),
we compare the identifier terms,
which boils down to comparing the variable names.
Either way, we normalize the nests of update-object calls
by ordering them according to the pointer.
We are talking about pointers here, and not object designators,
because, as mentioned in atc-symbolic-computation-states,
during symbolic execution the object designators in question
have the form
We also include a rule saying that
updating an object with the existing one is a no-op.
This is similar to
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).
Theorem:
(defthm update-object-of-add-frame (equal (update-object objdes obj (add-frame fun compst)) (add-frame fun (update-object objdes obj compst))))
Theorem:
(defthm update-object-of-enter-scope (equal (update-object objdes obj (enter-scope compst)) (enter-scope (update-object objdes obj compst))))
Theorem:
(defthm update-object-of-add-var (equal (update-object objdes obj (add-var var val compst)) (add-var var val (update-object objdes obj compst))))
Theorem:
(defthm update-object-of-update-var (equal (update-object objdes obj (update-var var val compst)) (update-var var val (update-object objdes obj compst))))
Theorem:
(defthm update-object-of-update-static-var (equal (update-object objdes obj (update-static-var var val compst)) (update-static-var var val (update-object objdes obj compst))))
Theorem:
(defthm update-object-of-update-object-same (equal (update-object objdes obj (update-object objdes obj2 compst)) (update-object objdes obj compst)))
Theorem:
(defthm update-object-of-update-object-less-symbol (implies (and (syntaxp (and (ffn-symb-p objdes 'value-pointer->designator) (ffn-symb-p objdes2 'value-pointer->designator) (b* ((ptr (fargn objdes 1)) (ptr2 (fargn objdes2 1))) (and (symbolp ptr) (symbolp ptr2) (symbol< ptr2 ptr))))) (object-disjointp objdes objdes2)) (equal (update-object objdes obj (update-object objdes2 obj2 compst)) (update-object objdes2 obj2 (update-object objdes obj compst)))) :rule-classes ((:rewrite :loop-stopper nil)))
Theorem:
(defthm update-object-of-update-object-less-ident (implies (and (syntaxp (and (ffn-symb-p objdes 'value-pointer->designator) (ffn-symb-p objdes2 'value-pointer->designator) (b* ((ptr (fargn objdes 1)) (ptr2 (fargn objdes2 1))) (and (ffn-symb-p ptr 'read-var) (ffn-symb-p ptr2 'read-var) (<< (fargn ptr2 1) (fargn ptr 1)))))) (object-disjointp objdes objdes2)) (equal (update-object objdes obj (update-object objdes2 obj2 compst)) (update-object objdes2 obj2 (update-object objdes obj compst)))) :rule-classes ((:rewrite :loop-stopper nil)))
Theorem:
(defthm update-object-of-read-object-same (implies (and (syntaxp (symbolp compst)) (compustatep compst1) (equal (objdesign-kind objdes) :alloc) (valuep (read-object objdes compst)) (equal (read-object objdes compst) (read-object objdes compst1))) (equal (update-object objdes (read-object objdes compst) compst1) compst1)))
Theorem:
(defthm update-object-of-if*-val (equal (update-object objdes (if* a b c) compst) (if* a (update-object objdes b compst) (update-object objdes c compst))))