		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-hidexpr-traverse-datatype

Given a dotted expression that indexes into a datatype, find the type of the expression.

Signature
(vl-hidexpr-traverse-datatype x type) → (mv warning restype)
Arguments: x — Guard (vl-expr-p x).; type — Guard (vl-datatype-p type).
Returns: warning — Type (iff (vl-warning-p warning) warning).; restype — Type (iff (vl-datatype-p restype) (not warning)).

A helpful invariant to remember when thinking about this function: The type and unpacked dimensions of a given call of this function belong to the base (leftmost) variable in the HID.

Also note: the datatype should be fully usertype-resolved, as by vl-datatype-usertype-elim.

BOZO Rewrite this documentation under the new assumption that the datatypes are pre-resolved.

Example: Suppose we have the following type declarations

typedef struct packed { logic [3:0] foo; } [4:0] foostruct;
typedef union { foostruct [5:0] bar; logic [2:0] baz; } bunion [0:6];
typedef struct { bunion fa [0:8], logic [1:0] ba; } bstruct;
bstruct myvar [8:0];

For this example, we'll write a type with both packed an unpacked dimensions with an underscore between the packed and unpacked dims.

A bunion is a type consisting of an unpacked array of 7 elements each of which may either be a packed array of 6 foostructs (a packed structure containing one 4-bit logic field) or a 3-bit logic; a bstruct is a struct containing an unpacked array of 9 bunions and an additional 2-bit logic field; and myvar is an unpacked array of 9 bstructs.

Suppose our expression is myvar[1].fa[8][4].bar[3][4].foo.

First, before calling this function we look up the type of myvar. We get a vardecl, which has a type bstruct _ [8:0]. Then we're ready to run.
Outermost call: We resolve the type bstruct to its struct definition. We cancel our index with the single array dimension, leaving just the struct. We find the element fa inside the struct, and recur on the remainder of our expression, fa[8][4].bar[3][4].foo, with the structmember's type, bunion _ [0:8].
We resolve the bunion type to the union, and append the unpacked dimensions of the type and the element to get [0:8][0:6]. We then check the indices from the expression against this type and unpacked dimensions, which results in just the bare union type (the definition of bunion, but without its unpacked dimension [0:6]). We find the element bar inside the union and recur: bar[3][4].foo, type foostruct[5:0].
We resolve the type foostruct to its struct type, and append the packed dimensions to get [5:0][4:0]. We then check the indices from the expression, which results in cancelling out the dimension to obtain just the bare struct. We find the element foo of the struct and recur on that.
Finally, we have just the atom foo as our expression, so we return the type logic[3:0].

Definitions and Theorems

Function: vl-hidexpr-traverse-datatype

(defun vl-hidexpr-traverse-datatype (x type)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-datatype-p type))))
 (declare (xargs :guard (vl-hidexpr-p x)))
 (let ((__function__ 'vl-hidexpr-traverse-datatype))
  (declare (ignorable __function__))
  (b*
   ((type (vl-datatype-fix type))
    ((when (vl-hidexpr->endp x))
     (mv nil type))
    (idx1 (vl-hidexpr->first x))
    ((mv warning baretype)
     (vl-hidindex-datatype-resolve-dims idx1 type))
    ((when warning) (mv warning nil))
    ((when (or (consp (vl-datatype->udims baretype))
               (consp (vl-datatype->pdims baretype))))
     (mv
      (make-vl-warning
       :type :vl-hid-datatype-fail
       :msg
       "Not enough indices in dotted selector ~a0: ~
                                   extra ~s1 dimensions."
       :args (list (vl-expr-fix x)
                   (if (consp (vl-datatype->udims baretype))
                       "unpacked"
                     "packed"))
       :fn __function__)
      nil))
    ((mv ok members)
     (vl-datatype->structmembers baretype))
    ((unless ok)
     (mv
      (make-vl-warning
       :type :vl-hid-datatype-fail
       :msg
       "Dot-indexing into a datatype that isn't a ~
                                   struct or union: ~a0"
       :args (list (vl-datatype-fix baretype))
       :fn __function__)
      nil))
    (next-hid (vl-hidexpr->rest x))
    (nextname (vl-hidindex->name (vl-hidexpr->first next-hid)))
    (member (vl-find-structmember nextname members))
    ((unless member)
     (mv
      (make-vl-warning
       :type :vl-structindex-fail
       :msg
       "Dot-indexing failed: struct/union member ~
                                   ~s0 not found in type ~a1"
       :args (list nextname (vl-datatype-fix baretype))
       :fn __function__)
      nil))
    (membtype (vl-structmember->type member)))
   (vl-hidexpr-traverse-datatype next-hid membtype))))

Theorem: return-type-of-vl-hidexpr-traverse-datatype.warning

(defthm return-type-of-vl-hidexpr-traverse-datatype.warning
  (b* (((mv common-lisp::?warning ?restype)
        (vl-hidexpr-traverse-datatype x type)))
    (iff (vl-warning-p warning) warning))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-hidexpr-traverse-datatype.restype

(defthm return-type-of-vl-hidexpr-traverse-datatype.restype
  (b* (((mv common-lisp::?warning ?restype)
        (vl-hidexpr-traverse-datatype x type)))
    (iff (vl-datatype-p restype)
         (not warning)))
  :rule-classes :rewrite)

Theorem: vl-hidexpr-traverse-datatype-of-vl-expr-fix-x

(defthm vl-hidexpr-traverse-datatype-of-vl-expr-fix-x
  (equal (vl-hidexpr-traverse-datatype (vl-expr-fix x)
                                       type)
         (vl-hidexpr-traverse-datatype x type)))

Theorem: vl-hidexpr-traverse-datatype-vl-expr-equiv-congruence-on-x

(defthm vl-hidexpr-traverse-datatype-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-hidexpr-traverse-datatype x type)
                  (vl-hidexpr-traverse-datatype x-equiv type)))
  :rule-classes :congruence)

Theorem: vl-hidexpr-traverse-datatype-of-vl-datatype-fix-type

(defthm vl-hidexpr-traverse-datatype-of-vl-datatype-fix-type
  (equal (vl-hidexpr-traverse-datatype x (vl-datatype-fix type))
         (vl-hidexpr-traverse-datatype x type)))

Theorem: vl-hidexpr-traverse-datatype-vl-datatype-equiv-congruence-on-type

(defthm
  vl-hidexpr-traverse-datatype-vl-datatype-equiv-congruence-on-type
  (implies (vl-datatype-equiv type type-equiv)
           (equal (vl-hidexpr-traverse-datatype x type)
                  (vl-hidexpr-traverse-datatype x type-equiv)))
  :rule-classes :congruence)