		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-follow-hidexpr-dimscheck

Check array indices against the corresponding array bounds.

Signature
(vl-follow-hidexpr-dimscheck name indices dims &key strictp direct-okp) → 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-dimensionlist-p dims).; strictp — Should we require every index to be resolved?.
Guard (booleanp strictp).; direct-okp — Is it OK to directly refer to the whole array?.
Guard (booleanp direct-okp).
Returns: err — Type (iff (vl-msg-p err) err).

Definitions and Theorems

Function: vl-follow-hidexpr-dimscheck-fn

(defun vl-follow-hidexpr-dimscheck-fn
       (name indices dims strictp direct-okp)
  (declare (xargs :guard (and (stringp name)
                              (vl-exprlist-p indices)
                              (vl-dimensionlist-p dims)
                              (booleanp strictp)
                              (booleanp direct-okp))))
  (let ((__function__ 'vl-follow-hidexpr-dimscheck))
    (declare (ignorable __function__))
    (b* ((name (string-fix name))
         ((when (atom dims))
          (if (atom indices)
              nil
            (vmsg "indexing into non-array ~s0" name)))
         ((when (atom indices))
          (if direct-okp nil
            (vmsg "no indices given for array ~s0" 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))
          (vmsg "too many indices for array ~s0" name)))
      (vmsg "not enough indices for array ~s0"
            name))))

Theorem: return-type-of-vl-follow-hidexpr-dimscheck

(defthm return-type-of-vl-follow-hidexpr-dimscheck
  (b* ((err (vl-follow-hidexpr-dimscheck-fn
                 name indices dims strictp direct-okp)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

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 direct-okp)
    (vl-follow-hidexpr-dimscheck-fn
         name indices dims strictp direct-okp)))

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 direct-okp)
                  (vl-follow-hidexpr-dimscheck-fn
                       name-equiv
                       indices dims strictp direct-okp)))
  :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 direct-okp)
      (vl-follow-hidexpr-dimscheck-fn
           name indices dims strictp direct-okp)))

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 direct-okp)
                 (vl-follow-hidexpr-dimscheck-fn
                      name
                      indices-equiv dims strictp direct-okp)))
 :rule-classes :congruence)

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

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

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

(defthm
 vl-follow-hidexpr-dimscheck-fn-vl-dimensionlist-equiv-congruence-on-dims
 (implies (vl-dimensionlist-equiv dims dims-equiv)
          (equal (vl-follow-hidexpr-dimscheck-fn
                      name indices dims strictp direct-okp)
                 (vl-follow-hidexpr-dimscheck-fn
                      name
                      indices dims-equiv strictp direct-okp)))
 :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)
              direct-okp)
         (vl-follow-hidexpr-dimscheck-fn
              name indices dims strictp direct-okp)))

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 direct-okp)
                  (vl-follow-hidexpr-dimscheck-fn
                       name
                       indices dims strictp-equiv direct-okp)))
  :rule-classes :congruence)

Theorem: vl-follow-hidexpr-dimscheck-fn-of-bool-fix-direct-okp

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

Theorem: vl-follow-hidexpr-dimscheck-fn-iff-congruence-on-direct-okp

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

Subtopics

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