		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-arrsub

Check an array subscripting expression [C17:6.5.2.1].

Signature
(check-arrsub arr-expr arr-etype sub-expr sub-etype) → etype
Arguments: arr-expr — Guard (exprp arr-expr).; arr-etype — Guard (expr-typep arr-etype).; sub-expr — Guard (exprp sub-expr).; sub-etype — Guard (expr-typep sub-etype).
Returns: etype — Type (expr-type-resultp etype).

We check arr-etype and sub-etype; arr-expr and sub-expr are just used for errors.

We do lvalue conversion for both operands, via expr-type->type. According to [C17:6.3.2/2], we should not do this if an operand has an array type; however, according to [C17:6.3.2/3], we should convert the array to a pointer (which we do via apconvert-type), and thus in the end the result is the same: we have a pointer type that does not denote an lvalue, if the operand is an array. If an operand is an integer, apconvert-type has no effect.

The first expression must have a pointer type [C17:6.5.2.1/1]. The second expression must have an integer type [C17:6.5.2.1/1]. The type of the array subscripting expression is the type referenced by the pointer. An array subscripting expression is always an lvalue.

For now we do not allow the roles of the expressions to be swapped, i.e. that the second expression is a pointer and the first one an integer; note the symmetry in [C17:6.5.2.1/2].

Definitions and Theorems

Function: check-arrsub

(defun check-arrsub (arr-expr arr-etype sub-expr sub-etype)
  (declare (xargs :guard (and (exprp arr-expr)
                              (expr-typep arr-etype)
                              (exprp sub-expr)
                              (expr-typep sub-etype))))
  (let ((__function__ 'check-arrsub))
    (declare (ignorable __function__))
    (b* ((arr-type (apconvert-type (expr-type->type arr-etype)))
         (sub-type (apconvert-type (expr-type->type sub-etype)))
         ((unless (type-case arr-type :pointer))
          (reserrf (list :array-mistype (expr-fix arr-expr)
                         :required :pointer
                         :supplied (type-fix arr-type))))
         ((unless (type-integerp sub-type))
          (reserrf (list :subscript-mistype (expr-fix sub-expr)
                         :required :integer
                         :supplied (type-fix sub-type)))))
      (make-expr-type :type (type-pointer->to arr-type)
                      :lvalue t))))

Theorem: expr-type-resultp-of-check-arrsub

(defthm expr-type-resultp-of-check-arrsub
  (b* ((etype (check-arrsub arr-expr arr-etype sub-expr sub-etype)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-arrsub-of-expr-fix-arr-expr

(defthm check-arrsub-of-expr-fix-arr-expr
  (equal (check-arrsub (expr-fix arr-expr)
                       arr-etype sub-expr sub-etype)
         (check-arrsub arr-expr arr-etype sub-expr sub-etype)))

Theorem: check-arrsub-expr-equiv-congruence-on-arr-expr

(defthm check-arrsub-expr-equiv-congruence-on-arr-expr
  (implies
       (expr-equiv arr-expr arr-expr-equiv)
       (equal (check-arrsub arr-expr arr-etype sub-expr sub-etype)
              (check-arrsub arr-expr-equiv
                            arr-etype sub-expr sub-etype)))
  :rule-classes :congruence)

Theorem: check-arrsub-of-expr-type-fix-arr-etype

(defthm check-arrsub-of-expr-type-fix-arr-etype
  (equal (check-arrsub arr-expr (expr-type-fix arr-etype)
                       sub-expr sub-etype)
         (check-arrsub arr-expr arr-etype sub-expr sub-etype)))

Theorem: check-arrsub-expr-type-equiv-congruence-on-arr-etype

(defthm check-arrsub-expr-type-equiv-congruence-on-arr-etype
  (implies
       (expr-type-equiv arr-etype arr-etype-equiv)
       (equal (check-arrsub arr-expr arr-etype sub-expr sub-etype)
              (check-arrsub arr-expr
                            arr-etype-equiv sub-expr sub-etype)))
  :rule-classes :congruence)

Theorem: check-arrsub-of-expr-fix-sub-expr

(defthm check-arrsub-of-expr-fix-sub-expr
  (equal (check-arrsub arr-expr arr-etype (expr-fix sub-expr)
                       sub-etype)
         (check-arrsub arr-expr arr-etype sub-expr sub-etype)))

Theorem: check-arrsub-expr-equiv-congruence-on-sub-expr

(defthm check-arrsub-expr-equiv-congruence-on-sub-expr
  (implies
       (expr-equiv sub-expr sub-expr-equiv)
       (equal (check-arrsub arr-expr arr-etype sub-expr sub-etype)
              (check-arrsub arr-expr
                            arr-etype sub-expr-equiv sub-etype)))
  :rule-classes :congruence)

Theorem: check-arrsub-of-expr-type-fix-sub-etype

(defthm check-arrsub-of-expr-type-fix-sub-etype
  (equal (check-arrsub arr-expr arr-etype
                       sub-expr (expr-type-fix sub-etype))
         (check-arrsub arr-expr arr-etype sub-expr sub-etype)))

Theorem: check-arrsub-expr-type-equiv-congruence-on-sub-etype

(defthm check-arrsub-expr-type-equiv-congruence-on-sub-etype
  (implies
       (expr-type-equiv sub-etype sub-etype-equiv)
       (equal (check-arrsub arr-expr arr-etype sub-expr sub-etype)
              (check-arrsub arr-expr
                            arr-etype sub-expr sub-etype-equiv)))
  :rule-classes :congruence)