		Search-engine friendly clone of the ACL2 documentation.

Following-hids

Vl-follow-hidexpr-dimscheck

Check array indices against the corresponding array bounds.

Signature
(vl-follow-hidexpr-dimscheck name indices dims &key strictp) → err
Arguments: name — Guard (stringp name).; indices — Indices from the HID piece we're following. I.e., if we are resolving foo[3][4][5].bar, this would be (3 4 5) as an expression list.
Guard (vl-exprlist-p indices).; dims — Corresponding dimensions from the declaration, i.e., if foo is declared as a logic [7:0][15:0][3:0], then this would be the list of ([7:0] [15:0] [3:0]).
Guard (vl-packeddimensionlist-p dims).; strictp — Should we require every index to be resolved?.
Guard (booleanp strictp).
Returns: err — Type (maybe-stringp err).

Definitions and Theorems

Function: vl-follow-hidexpr-dimscheck-fn

(defun vl-follow-hidexpr-dimscheck-fn (name indices dims strictp)
  (declare (xargs :guard (and (stringp name)
                              (vl-exprlist-p indices)
                              (vl-packeddimensionlist-p dims)
                              (booleanp strictp))))
  (let ((__function__ 'vl-follow-hidexpr-dimscheck))
    (declare (ignorable __function__))
    (b* (((when (atom dims))
          (if (atom indices)
              nil
            (cat "indexing into non-array " name)))
         ((when (atom indices))
          (cat "no indices given for array " name))
         ((when (same-lengthp indices dims))
          (vl-follow-hidexpr-dimscheck-aux name indices dims
                                           :strictp strictp))
         (found (len indices))
         (need (len dims))
         ((when (< found need))
          (cat "too many indices for array " name)))
      (cat "not enough indices for array " name))))

Theorem: maybe-stringp-of-vl-follow-hidexpr-dimscheck

(defthm maybe-stringp-of-vl-follow-hidexpr-dimscheck
 (b*
  ((err (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))
  (maybe-stringp err))
 :rule-classes :type-prescription)

Theorem: vl-follow-hidexpr-dimscheck-fn-of-str-fix-name

(defthm vl-follow-hidexpr-dimscheck-fn-of-str-fix-name
 (equal (vl-follow-hidexpr-dimscheck-fn (str-fix name)
                                        indices dims strictp)
        (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))

Theorem: vl-follow-hidexpr-dimscheck-fn-streqv-congruence-on-name

(defthm vl-follow-hidexpr-dimscheck-fn-streqv-congruence-on-name
 (implies
   (streqv name name-equiv)
   (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)
          (vl-follow-hidexpr-dimscheck-fn
               name-equiv indices dims strictp)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-dimscheck-fn-of-vl-exprlist-fix-indices

(defthm vl-follow-hidexpr-dimscheck-fn-of-vl-exprlist-fix-indices
 (equal
      (vl-follow-hidexpr-dimscheck-fn name (vl-exprlist-fix indices)
                                      dims strictp)
      (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))

Theorem: vl-follow-hidexpr-dimscheck-fn-vl-exprlist-equiv-congruence-on-indices

(defthm
 vl-follow-hidexpr-dimscheck-fn-vl-exprlist-equiv-congruence-on-indices
 (implies
   (vl-exprlist-equiv indices indices-equiv)
   (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)
          (vl-follow-hidexpr-dimscheck-fn
               name indices-equiv dims strictp)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-dimscheck-fn-of-vl-packeddimensionlist-fix-dims

(defthm
  vl-follow-hidexpr-dimscheck-fn-of-vl-packeddimensionlist-fix-dims
 (equal
   (vl-follow-hidexpr-dimscheck-fn name indices
                                   (vl-packeddimensionlist-fix dims)
                                   strictp)
   (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))

Theorem: vl-follow-hidexpr-dimscheck-fn-vl-packeddimensionlist-equiv-congruence-on-dims

(defthm
 vl-follow-hidexpr-dimscheck-fn-vl-packeddimensionlist-equiv-congruence-on-dims
 (implies
   (vl-packeddimensionlist-equiv dims dims-equiv)
   (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)
          (vl-follow-hidexpr-dimscheck-fn
               name indices dims-equiv strictp)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-dimscheck-fn-of-bool-fix-strictp

(defthm vl-follow-hidexpr-dimscheck-fn-of-bool-fix-strictp
 (equal (vl-follow-hidexpr-dimscheck-fn
             name
             indices dims (acl2::bool-fix strictp))
        (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))

Theorem: vl-follow-hidexpr-dimscheck-fn-iff-congruence-on-strictp

(defthm vl-follow-hidexpr-dimscheck-fn-iff-congruence-on-strictp
 (implies
   (iff strictp strictp-equiv)
   (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)
          (vl-follow-hidexpr-dimscheck-fn
               name indices dims strictp-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-follow-hidexpr-dimscheck-aux: Main loop to check each index/dimension pair.