		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: erp — Type (maybe-msgp erp).; 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 [C17:6.5.2.1/1]. The expression has the type referenced by the pointer type.

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 [C17: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)))
 (b* (((reterr) (irr-type))
      (type1 (type-apconvert type-arg1))
      (type2 (type-apconvert type-arg2))
      ((when (and (type-case type1 :pointer)
                  (or (type-integerp type2)
                      (type-case type2 :unknown))))
       (retok (type-pointer->to type1)))
      ((when (and (type-case type2 :pointer)
                  (or (type-integerp type1)
                      (type-case type1 :unknown))))
       (retok (type-pointer->to type2)))
      ((when (or (type-case type-arg1 :unknown)
                 (type-case type-arg2 :unknown)))
       (retok (type-unknown))))
  (retmsg$
   "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))))

Theorem: maybe-msgp-of-valid-arrsub.erp

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

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)