		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-arrsub

Validate an array subscripting expression, given the types of the two sub-expressions.

Signature
(valid-arrsub expr type-arg1 type-arg2) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type-arg1 — Guard (typep type-arg1).; type-arg2 — Guard (typep type-arg2).
Returns: type — Type (typep type).

After converting array types to pointer types, one sub-expression must have pointer type, and the other sub-expression must have integer type [C:6.5.2.1/1]. The expression should have the type referenced by the pointer type, but since for now we model just one pointer type, the type of the expression is unknown.

There is no need to perform function-to-pointer conversion, because that would result in a pointer to function, which is disallowed, as it has to be a pointer to a complete object type [C:6.5.2.1/1]. So by leaving function types as such, we automatically disallow them.

Definitions and Theorems

Function: valid-arrsub

(defun valid-arrsub (expr type-arg1 type-arg2)
 (declare (xargs :guard (and (exprp expr)
                             (typep type-arg1)
                             (typep type-arg2))))
 (declare (xargs :guard (expr-case expr :arrsub)))
 (let ((__function__ 'valid-arrsub))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((when (or (type-case type-arg1 :unknown)
               (type-case type-arg2 :unknown)))
     (retok (type-unknown)))
    (type1 (type-apconvert type-arg1))
    (type2 (type-apconvert type-arg2))
    ((unless (or (and (type-case type1 :pointer)
                      (type-integerp type2))
                 (and (type-integerp type1)
                      (type-case type2 :pointer))))
     (reterr
      (msg
       "In the array subscripting expression ~x0, ~
                      the first sub-expression has type ~x1, ~
                      and the second sub-expression has type ~x2."
       (expr-fix expr)
       (type-fix type-arg1)
       (type-fix type-arg2)))))
   (retok (type-unknown)))))

Theorem: typep-of-valid-arrsub.type

(defthm typep-of-valid-arrsub.type
  (b* (((mv acl2::?erp ?type)
        (valid-arrsub expr type-arg1 type-arg2)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-arrsub-of-expr-fix-expr

(defthm valid-arrsub-of-expr-fix-expr
  (equal (valid-arrsub (expr-fix expr)
                       type-arg1 type-arg2)
         (valid-arrsub expr type-arg1 type-arg2)))

Theorem: valid-arrsub-expr-equiv-congruence-on-expr

(defthm valid-arrsub-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-arrsub expr type-arg1 type-arg2)
                  (valid-arrsub expr-equiv type-arg1 type-arg2)))
  :rule-classes :congruence)

Theorem: valid-arrsub-of-type-fix-type-arg1

(defthm valid-arrsub-of-type-fix-type-arg1
  (equal (valid-arrsub expr (type-fix type-arg1)
                       type-arg2)
         (valid-arrsub expr type-arg1 type-arg2)))

Theorem: valid-arrsub-type-equiv-congruence-on-type-arg1

(defthm valid-arrsub-type-equiv-congruence-on-type-arg1
  (implies (type-equiv type-arg1 type-arg1-equiv)
           (equal (valid-arrsub expr type-arg1 type-arg2)
                  (valid-arrsub expr type-arg1-equiv type-arg2)))
  :rule-classes :congruence)

Theorem: valid-arrsub-of-type-fix-type-arg2

(defthm valid-arrsub-of-type-fix-type-arg2
  (equal (valid-arrsub expr type-arg1 (type-fix type-arg2))
         (valid-arrsub expr type-arg1 type-arg2)))

Theorem: valid-arrsub-type-equiv-congruence-on-type-arg2

(defthm valid-arrsub-type-equiv-congruence-on-type-arg2
  (implies (type-equiv type-arg2 type-arg2-equiv)
           (equal (valid-arrsub expr type-arg1 type-arg2)
                  (valid-arrsub expr type-arg1 type-arg2-equiv)))
  :rule-classes :congruence)