		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-arrsub

Execute the array subscripting operation on expression values.

Signature
(exec-arrsub arr sub compst) → eval
Arguments: arr — Guard (expr-valuep arr).; sub — Guard (expr-valuep sub).; compst — Guard (compustatep compst).
Returns: eval — Type (expr-value-resultp eval).

We perform array-to-pointer conversion [C:5.3.2.1/3] on both operands.

The first operand must be a valid pointer to an array; the pointer must have the element type of the array. The second operand must be an integer value (of any integer type). The resulting index must be in range for the array, and the indexed element is returned as result, as an expression value whose object designator is for the array element.

This semantics is an approximation of the real one in C, but it is adequate to our C subset. In full C, an array subscripting expression a[i] is equivalent to *(a+i), so a should be really a pointer to the first element of the array, to which the index i is added to obtain a pointer to the element. In our C subset, we have limited support for pointers, in particular there is no explicit pointer arithmetic, other than implicitly as array subscripting. So we have our own treatment of array subscipting here, in which the pointer is assumed to be to the array (not the first element), and the index is just used to obtain the element. This treatment is equivalent to the real one for our current purposes.

Note that, in full C, pointers are almost never to arrays, but rather they are to elements of arrays. The only way to get a pointer to an array as such is via &a when a is an array object name; except for this case, and for the case of an argument to sizeof, as well as for string literals (currently not in our C subset), an array is always converted to a pointer to its first element [C:6.3.2.1/3].

In any case, we plan to make our formal semantics more consistent with full C in the treatment of arrays.

Definitions and Theorems

Function: exec-arrsub

(defun exec-arrsub (arr sub compst)
  (declare (xargs :guard (and (expr-valuep arr)
                              (expr-valuep sub)
                              (compustatep compst))))
  (let ((__function__ 'exec-arrsub))
    (declare (ignorable __function__))
    (b* ((arr (apconvert-expr-value arr))
         ((when (errorp arr)) arr)
         (arr (expr-value->value arr))
         ((unless (value-case arr :pointer))
          (error (list :mistype-arrsub
                       :required :pointer
                       :supplied (type-of-value arr))))
         ((unless (value-pointer-validp arr))
          (error (list :invalid-pointer arr)))
         (objdes (value-pointer->designator arr))
         (reftype (value-pointer->reftype arr))
         (array (read-object objdes compst))
         ((when (errorp array))
          (error (list :array-not-found
                       arr (compustate-fix compst))))
         ((unless (value-case array :array))
          (error (list :not-array
                       arr (compustate-fix compst))))
         ((unless (equal reftype (value-array->elemtype array)))
          (error (list :mistype-array-read
                       :pointer reftype
                       :array (value-array->elemtype array))))
         (sub (apconvert-expr-value sub))
         ((when (errorp sub)) sub)
         (sub (expr-value->value sub))
         ((unless (value-integerp sub))
          (error (list :mistype-array :index
                       :required :integer
                       :supplied (type-of-value sub))))
         (index (value-integer->get sub))
         ((when (< index 0))
          (error (list :negative-array-index
                       :array array
                       :index sub)))
         (val (value-array-read index array))
         ((when (errorp val)) val)
         (elem-objdes (make-objdesign-element :super objdes
                                              :index index)))
      (make-expr-value :value val
                       :object elem-objdes))))

Theorem: expr-value-resultp-of-exec-arrsub

(defthm expr-value-resultp-of-exec-arrsub
  (b* ((eval (exec-arrsub arr sub compst)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-arrsub-of-expr-value-fix-arr

(defthm exec-arrsub-of-expr-value-fix-arr
  (equal (exec-arrsub (expr-value-fix arr)
                      sub compst)
         (exec-arrsub arr sub compst)))

Theorem: exec-arrsub-expr-value-equiv-congruence-on-arr

(defthm exec-arrsub-expr-value-equiv-congruence-on-arr
  (implies (expr-value-equiv arr arr-equiv)
           (equal (exec-arrsub arr sub compst)
                  (exec-arrsub arr-equiv sub compst)))
  :rule-classes :congruence)

Theorem: exec-arrsub-of-expr-value-fix-sub

(defthm exec-arrsub-of-expr-value-fix-sub
  (equal (exec-arrsub arr (expr-value-fix sub)
                      compst)
         (exec-arrsub arr sub compst)))

Theorem: exec-arrsub-expr-value-equiv-congruence-on-sub

(defthm exec-arrsub-expr-value-equiv-congruence-on-sub
  (implies (expr-value-equiv sub sub-equiv)
           (equal (exec-arrsub arr sub compst)
                  (exec-arrsub arr sub-equiv compst)))
  :rule-classes :congruence)

Theorem: exec-arrsub-of-compustate-fix-compst

(defthm exec-arrsub-of-compustate-fix-compst
  (equal (exec-arrsub arr sub (compustate-fix compst))
         (exec-arrsub arr sub compst)))

Theorem: exec-arrsub-compustate-equiv-congruence-on-compst

(defthm exec-arrsub-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-arrsub arr sub compst)
                  (exec-arrsub arr sub compst-equiv)))
  :rule-classes :congruence)