		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Read-object

Read an object in the computation state.

Signature
(read-object objdes compst) → obj
Arguments: objdes — Guard (objdesignp objdes).; compst — Guard (compustatep compst).
Returns: obj — Type (value-resultp obj).

If the object designator is a static variable, we look it up in static storage. If the object designator is an automatic variable, we index the frame stack, we index the scope stack, and we find the variable by name; note that, as explained in objdesign, the indices start at the bottom, i.e. the end of the lists, so we reverse the lists before indexing them. If the object designator is for allocated storage, we look up the object in the heap by address. Otherwise, first we recursively read the super-object, then we access the sub-object (array element or structure member), ensuring that the super-object is of the appropriate kind for the object designator.

Definitions and Theorems

Function: read-object

(defun read-object (objdes compst)
 (declare (xargs :guard (and (objdesignp objdes)
                             (compustatep compst))))
 (let ((__function__ 'read-object))
  (declare (ignorable __function__))
  (objdesign-case
       objdes :static
       (b* ((var+val (omap::assoc objdes.name
                                  (compustate->static compst)))
            ((when (not var+val))
             (error (list :static-var-not-found objdes.name))))
         (cdr var+val))
       :auto
       (b* ((rev-frames (rev (compustate->frames compst)))
            ((unless (< objdes.frame (len rev-frames)))
             (error (list :frame-index-out-of-range objdes.frame)))
            (frame (nth objdes.frame rev-frames))
            (rev-scopes (rev (frame->scopes frame)))
            ((unless (< objdes.scope (len rev-scopes)))
             (error (list :scope-index-out-of-range objdes.scope)))
            (scope (nth objdes.scope rev-scopes))
            (var+val (omap::assoc objdes.name scope))
            ((unless (consp var+val))
             (error (list :name-not-found objdes.name)))
            (val (cdr var+val)))
         val)
       :alloc
       (b* ((addr objdes.get)
            (heap (compustate->heap compst))
            (addr+obj (omap::assoc addr heap))
            ((unless (consp addr+obj))
             (error (list :address-not-found addr)))
            (obj (cdr addr+obj)))
         obj)
       :element
       (b* ((obj (read-object objdes.super compst))
            ((when (errorp obj)) obj)
            ((unless (value-case obj :array))
             (error (list :objdesign-mismatch (objdesign-fix objdes)
                          :required :array
                          :supplied obj))))
         (value-array-read objdes.index obj))
       :member
       (b* ((obj (read-object objdes.super compst))
            ((when (errorp obj)) obj)
            ((unless (value-case obj :struct))
             (error (list :objdesign-mismatch (objdesign-fix objdes)
                          :required :struct
                          :supplied obj))))
         (value-struct-read objdes.name obj)))))

Theorem: value-resultp-of-read-object

(defthm value-resultp-of-read-object
  (b* ((obj (read-object objdes compst)))
    (value-resultp obj))
  :rule-classes :rewrite)

Theorem: valuep-of-read-object-of-objdesign-of-var

(defthm valuep-of-read-object-of-objdesign-of-var
  (b* ((objdes (objdesign-of-var var compst)))
    (implies objdes
             (valuep (read-object objdes compst)))))

Theorem: read-object-of-objdesign-fix-objdes

(defthm read-object-of-objdesign-fix-objdes
  (equal (read-object (objdesign-fix objdes)
                      compst)
         (read-object objdes compst)))

Theorem: read-object-objdesign-equiv-congruence-on-objdes

(defthm read-object-objdesign-equiv-congruence-on-objdes
  (implies (objdesign-equiv objdes objdes-equiv)
           (equal (read-object objdes compst)
                  (read-object objdes-equiv compst)))
  :rule-classes :congruence)

Theorem: read-object-of-compustate-fix-compst

(defthm read-object-of-compustate-fix-compst
  (equal (read-object objdes (compustate-fix compst))
         (read-object objdes compst)))

Theorem: read-object-compustate-equiv-congruence-on-compst

(defthm read-object-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (read-object objdes compst)
                  (read-object objdes compst-equiv)))
  :rule-classes :congruence)