• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • 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-data-selects

Given a HID expression denoting a variable of the input type, create a trace showing the type of each field select/indexing operation.

Signature

(vl-follow-data-selects x type trace) → (mv err seltrace)

Arguments

x — Guard (vl-hidexpr-p x).

type — Guard (vl-datatype-p type).

trace — Accumulator.
    Guard (vl-seltrace-p trace).

Returns

err — Type (iff (vl-msg-p err) err).

seltrace — Type (vl-seltrace-p seltrace).

Implementation notes: This function only

Definitions and Theorems

Function: vl-follow-data-selects

(defun vl-follow-data-selects (x type trace)
 (declare (xargs :guard (and (vl-hidexpr-p x)
                             (vl-datatype-p type)
                             (vl-seltrace-p trace))))
 (declare (xargs :guard (vl-datatype-resolved-p type)))
 (let ((__function__ 'vl-follow-data-selects))
  (declare (ignorable __function__))
  (b*
   ((type (vl-datatype-fix type))
    (trace (vl-seltrace-fix trace))
    ((when (vl-hidexpr-case x :end))
     (mv nil trace))
    ((vl-hidexpr-dot x))
    ((mv err rev-idxtrace)
     (vl-follow-array-indices (vl-hidindex->indices x.first)
                              type))
    ((when err) (mv err nil))
    (trace (revappend rev-idxtrace trace))
    (type (if (consp rev-idxtrace)
              (vl-selstep->type (car trace))
            type))
    (type (vl-maybe-usertype-resolve type))
    ((mv ok members)
     (vl-datatype->structmembers type))
    (nextname
         (vl-hidexpr-case x.rest
                          :end x.rest.name
                          :dot (vl-hidindex->name x.rest.first)))
    ((unless (and ok (atom (vl-datatype->udims type))
                  (atom (vl-datatype->pdims type))))
     (mv
      (vmsg
       "Dot-indexing (field ~s0) into a non-struct/union datatype: ~a1"
       nextname type)
      nil))
    ((when (eq nextname :vl-$root))
     (mv (vmsg "Can't use $root to index into a data structure: ~a0"
               (vl-hidexpr-fix x))
         nil))
    (member (vl-find-structmember nextname members))
    ((unless member)
     (mv
      (vmsg
       "Dot-indexing failed: struct/union member ~
                                   ~s0 not found in type ~a1"
       nextname (vl-datatype-fix type))
      nil))
    (membtype (vl-structmember->type member))
    (next-frame
      (make-vl-selstep :select (make-vl-select-field :name nextname)
                       :type membtype))
    (trace (cons next-frame trace)))
   (vl-follow-data-selects x.rest membtype trace))))

Theorem: return-type-of-vl-follow-data-selects.err

(defthm return-type-of-vl-follow-data-selects.err
  (b* (((mv ?err ?seltrace)
        (vl-follow-data-selects x type trace)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-seltrace-p-of-vl-follow-data-selects.seltrace

(defthm vl-seltrace-p-of-vl-follow-data-selects.seltrace
  (b* (((mv ?err ?seltrace)
        (vl-follow-data-selects x type trace)))
    (vl-seltrace-p seltrace))
  :rule-classes :rewrite)

Theorem: vl-seltrace-usertypes-ok-of-vl-follow-data-selects

(defthm vl-seltrace-usertypes-ok-of-vl-follow-data-selects
  (b* (((mv ?err ?seltrace)
        (vl-follow-data-selects x type trace)))
    (implies (and (vl-datatype-resolved-p type)
                  (vl-seltrace-usertypes-ok trace))
             (vl-seltrace-usertypes-ok seltrace))))

Theorem: vl-seltrace-indices-of-vl-follow-data-selects

(defthm vl-seltrace-indices-of-vl-follow-data-selects
  (b* (((mv ?err ?seltrace)
        (vl-follow-data-selects x type trace)))
    (implies (not err)
             (equal (vl-seltrace->indices seltrace)
                    (revappend (vl-hidexpr->subexprs x)
                               (vl-seltrace->indices trace))))))

Theorem: vl-follow-data-selects-of-vl-hidexpr-fix-x

(defthm vl-follow-data-selects-of-vl-hidexpr-fix-x
  (equal (vl-follow-data-selects (vl-hidexpr-fix x)
                                 type trace)
         (vl-follow-data-selects x type trace)))

Theorem: vl-follow-data-selects-vl-hidexpr-equiv-congruence-on-x

(defthm vl-follow-data-selects-vl-hidexpr-equiv-congruence-on-x
  (implies (vl-hidexpr-equiv x x-equiv)
           (equal (vl-follow-data-selects x type trace)
                  (vl-follow-data-selects x-equiv type trace)))
  :rule-classes :congruence)

Theorem: vl-follow-data-selects-of-vl-datatype-fix-type

(defthm vl-follow-data-selects-of-vl-datatype-fix-type
  (equal (vl-follow-data-selects x (vl-datatype-fix type)
                                 trace)
         (vl-follow-data-selects x type trace)))

Theorem: vl-follow-data-selects-vl-datatype-equiv-congruence-on-type

(defthm vl-follow-data-selects-vl-datatype-equiv-congruence-on-type
  (implies (vl-datatype-equiv type type-equiv)
           (equal (vl-follow-data-selects x type trace)
                  (vl-follow-data-selects x type-equiv trace)))
  :rule-classes :congruence)

Theorem: vl-follow-data-selects-of-vl-seltrace-fix-trace

(defthm vl-follow-data-selects-of-vl-seltrace-fix-trace
  (equal (vl-follow-data-selects x type (vl-seltrace-fix trace))
         (vl-follow-data-selects x type trace)))

Theorem: vl-follow-data-selects-vl-seltrace-equiv-congruence-on-trace

(defthm vl-follow-data-selects-vl-seltrace-equiv-congruence-on-trace
  (implies (vl-seltrace-equiv trace trace-equiv)
           (equal (vl-follow-data-selects x type trace)
                  (vl-follow-data-selects x type trace-equiv)))
  :rule-classes :congruence)