• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
          • Scopestack
          • Hid-tools
            • Vl-follow-hidexpr
            • Vl-index-expr-typetrace
            • Vl-follow-scopeexpr
            • Vl-follow-hidexpr-dimscheck
            • Vl-datatype-resolve-selects
            • Vl-datatype-remove-dim
            • Vl-operandinfo
            • Vl-follow-hidexpr-dimcheck
              • Vl-follow-data-selects
              • Vl-follow-hidexpr-error
              • Vl-hidstep
              • Vl-scopestack-find-item/ss/path
              • Vl-follow-array-indices
              • Vl-scopecontext
              • Vl-datatype-set-unsigned
              • Vl-selstep
              • Vl-scopestack-find-elabpath
              • Vl-hid-prefix-for-subhid
              • Vl-find-structmember
              • Vl-select
              • Vl-scopeexpr-replace-hid
              • Vl-genblocklist-find-block
              • Vl-partselect-width
              • Vl-seltrace->indices
              • Vl-datatype->structmembers
              • Vl-hidexpr-resolved-p
              • Vl-operandinfo->indices
              • Vl-flatten-hidindex
              • Vl-subhid-p
              • Vl-seltrace-usertypes-ok
              • Vl-flatten-hidexpr
              • Vl-scopeexpr->hid
              • Vl-seltrace-index-count
              • Vl-operandinfo-usertypes-ok
              • Vl-operandinfo-index-count
              • Vl-datatype-dims-count
              • Vl-scopeexpr-index-count
              • Vl-hidexpr-index-count
              • Vl-usertype-lookup
              • Vl-hidindex-resolved-p
              • Vl-scopeexpr-resolved-p
              • Vl-selstep-usertypes-ok
              • Vl-hidtrace
              • Vl-seltrace
              • Vl-scopedef-interface-p
            • Filtering-by-name
            • Vl-interface-mocktype
            • Stripping-functions
            • Genblob
            • Expr-tools
            • Extract-vl-types
            • Hierarchy
            • Range-tools
            • Finding-by-name
            • Stmt-tools
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Hid-tools

    Vl-follow-hidexpr-dimcheck

    Check an array index against the corresponding array bounds.

    Signature
    (vl-follow-hidexpr-dimcheck name index dim &key strictp) → err
    Arguments
    name — Name being the array, for better errors.
        Guard (stringp name).
    index — An index into an array.
        Guard (vl-expr-p index).
    dim — Bounds from the corresponding declaration.
        Guard (vl-dimension-p dim).
    strictp — Require indices to be resolved?.
        Guard (booleanp strictp).
    Returns
    err — Type (iff (vl-msg-p err) err).

    In strict mode, we require that the index and the array dimensions all be resolved and that the index be in range.

    In non-strict mode, we tolerate unresolved indices and declaration bounds. Note that we still do bounds checking if the indices and array bounds happen to be resolved.

    Definitions and Theorems

    Function: vl-follow-hidexpr-dimcheck-fn

    (defun vl-follow-hidexpr-dimcheck-fn (name index dim strictp)
     (declare (xargs :guard (and (stringp name)
                                 (vl-expr-p index)
                                 (vl-dimension-p dim)
                                 (booleanp strictp))))
     (let ((__function__ 'vl-follow-hidexpr-dimcheck))
      (declare (ignorable __function__))
      (b* ((dim (vl-dimension-fix dim)))
       (vl-dimension-case
        dim (:unsized nil)
        (:star nil)
        (:datatype
         (if strictp
          (vmsg
           "unimplemented: check dimension against datatype-based associative
                      dimension ~a0"
           dim)
          nil))
        (:queue
         (if strictp
          (vmsg
            "unimplemented: check dimension against queue dimension ~a0"
            dim)
          nil))
        (:range
          (b*
           (((unless (vl-expr-resolved-p index))
             (if strictp (vmsg "unresolved array index")
               nil))
            ((unless (vl-range-resolved-p dim.range))
             (if strictp (vmsg "unresolved bounds on declaration of ~s0"
                               (string-fix name))
               nil))
            (idxval (vl-resolved->val index))
            (msbval (vl-resolved->val dim.msb))
            (lsbval (vl-resolved->val dim.lsb))
            (minval (min msbval lsbval))
            (maxval (max msbval lsbval))
            ((unless (and (<= minval idxval)
                          (<= idxval maxval)))
             (vmsg "array index ~x0 out of bounds (~x1 to ~x2)"
                   idxval minval maxval)))
           nil))))))

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

    (defthm return-type-of-vl-follow-hidexpr-dimcheck
      (b* ((err (vl-follow-hidexpr-dimcheck-fn name index dim strictp)))
        (iff (vl-msg-p err) err))
      :rule-classes :rewrite)

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

    (defthm vl-follow-hidexpr-dimcheck-fn-of-str-fix-name
      (equal (vl-follow-hidexpr-dimcheck-fn (str-fix name)
                                            index dim strictp)
             (vl-follow-hidexpr-dimcheck-fn name index dim strictp)))

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

    (defthm vl-follow-hidexpr-dimcheck-fn-streqv-congruence-on-name
     (implies
      (streqv name name-equiv)
      (equal
          (vl-follow-hidexpr-dimcheck-fn name index dim strictp)
          (vl-follow-hidexpr-dimcheck-fn name-equiv index dim strictp)))
     :rule-classes :congruence)

    Theorem: vl-follow-hidexpr-dimcheck-fn-of-vl-expr-fix-index

    (defthm vl-follow-hidexpr-dimcheck-fn-of-vl-expr-fix-index
      (equal (vl-follow-hidexpr-dimcheck-fn name (vl-expr-fix index)
                                            dim strictp)
             (vl-follow-hidexpr-dimcheck-fn name index dim strictp)))

    Theorem: vl-follow-hidexpr-dimcheck-fn-vl-expr-equiv-congruence-on-index

    (defthm
        vl-follow-hidexpr-dimcheck-fn-vl-expr-equiv-congruence-on-index
     (implies
      (vl-expr-equiv index index-equiv)
      (equal
          (vl-follow-hidexpr-dimcheck-fn name index dim strictp)
          (vl-follow-hidexpr-dimcheck-fn name index-equiv dim strictp)))
     :rule-classes :congruence)

    Theorem: vl-follow-hidexpr-dimcheck-fn-of-vl-dimension-fix-dim

    (defthm vl-follow-hidexpr-dimcheck-fn-of-vl-dimension-fix-dim
     (equal
        (vl-follow-hidexpr-dimcheck-fn name index (vl-dimension-fix dim)
                                       strictp)
        (vl-follow-hidexpr-dimcheck-fn name index dim strictp)))

    Theorem: vl-follow-hidexpr-dimcheck-fn-vl-dimension-equiv-congruence-on-dim

    (defthm
     vl-follow-hidexpr-dimcheck-fn-vl-dimension-equiv-congruence-on-dim
     (implies
      (vl-dimension-equiv dim dim-equiv)
      (equal
          (vl-follow-hidexpr-dimcheck-fn name index dim strictp)
          (vl-follow-hidexpr-dimcheck-fn name index dim-equiv strictp)))
     :rule-classes :congruence)

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

    (defthm vl-follow-hidexpr-dimcheck-fn-of-bool-fix-strictp
      (equal (vl-follow-hidexpr-dimcheck-fn
                  name index dim (acl2::bool-fix strictp))
             (vl-follow-hidexpr-dimcheck-fn name index dim strictp)))

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

    (defthm vl-follow-hidexpr-dimcheck-fn-iff-congruence-on-strictp
     (implies
      (iff strictp strictp-equiv)
      (equal
          (vl-follow-hidexpr-dimcheck-fn name index dim strictp)
          (vl-follow-hidexpr-dimcheck-fn name index dim strictp-equiv)))
     :rule-classes :congruence)