• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
          • Expression-sizing-minutia
          • Expression-sizing-intro
          • Vl-keyvalue-pattern-collect-array-replacements
          • Vl-assignpattern-positional-replacement
          • Vl-plainarg-exprsize
          • Vl-assignpattern-keyvalue-replacement
          • Vl-keyvalue-pattern-collect-struct-replacements
          • Vl-modulelist-exprsize
          • Vl-expr-assignpattern-extend/truncate
          • Vl-structmemberlist->types
          • Vl-expr-size
          • Vl-expr-selfdetermine-type
          • Vl-assignpattern-multi-replacement
          • Vl-parse-keyval-pattern-struct
          • Vl-plainarglist-exprsize
          • Vl-parse-keyval-pattern-array
          • Vl-warn-about-implicit-extension
          • Vl-assigncontext-size
          • Vl-arguments-exprsize
          • Vl-assignpattern-replacement
          • Vl-packeddimensionlist-exprsize
          • Vl-namedparamvaluelist-exprsize
          • Vl-maybe-delayoreventcontrol-exprsize
          • Vl-repeateventcontrol-exprsize
          • Vl-paramvaluelist-exprsize
          • Vl-maybe-packeddimension-exprsize
          • Vl-delayoreventcontrol-exprsize
          • Vl-namedparamvalue-exprsize
          • Vl-namedarglist-exprsize
          • Vl-enumitemlist-exprsize
          • Vl-packeddimension-exprsize
          • Vl-maybe-paramvalue-exprsize
          • Vl-evatomlist-exprsize
          • Vl-atom-selfdetermine-type
          • Vl-rangelist-exprsize
          • Vl-maybe-gatedelay-exprsize
          • Vl-maybe-datatype-exprsize
          • Vl-gatedelay-exprsize
          • Vl-paramargs-exprsize
          • Vl-namedarg-exprsize
          • Vl-eventcontrol-exprsize
          • Vl-enumbasetype-exprsize
          • Vl-delaycontrol-exprsize
          • Vl-paramvalue-exprsize
          • Vl-maybe-range-exprsize
          • Vl-enumitem-exprsize
          • Vl-range-exprsize
          • Vl-paramdecl-exprsize
          • Vl-paramdecllist-exprsize
          • Vl-maybe-expr-size
          • Vl-evatom-exprsize
          • Vl-vardecllist-exprsize
          • Vl-portdecllist-exprsize
          • Vl-modinstlist-exprsize
          • Vl-initiallist-exprsize
          • Vl-gateinstlist-exprsize
          • Vl-fundecllist-exprsize
          • Vl-assign-exprsize
          • Vl-interfaceport-exprsize
          • Vl-assignlist-exprsize
          • Vl-alwayslist-exprsize
          • Vl-portlist-exprsize
          • Vl-modinst-exprsize
          • Vl-gateinst-exprsize
          • Vl-fundecl-exprsize
          • Vl-vardecl-exprsize
          • Vl-regularport-exprsize
          • Vl-portdecl-exprsize
          • Vl-initial-exprsize
          • Vl-always-exprsize
          • Vl-port-exprsize
          • Vl-lvalue-type
          • Vl-classify-extension-warning-hook
          • Welltyped
          • Vl-castexpr->datatype
          • Vl-expr-size-assigncontext
          • Vl-type-expr-pairs-sum-datatype-sizes
          • Vl-basictype->datatype
          • Vl-expr-replace-assignpatterns
          • Vl-design-exprsize
          • Vl-op-simple-vector-p
          • Vl-expr-val-alist-max-count
          • Vl-expr-has-patterns
          • Vl-exprlist-max-count
          • Vl-unsigned-when-size-zero-lst
          • Vl-type-expr-pairs
          • Append-n
          • Vl-expr-val-alist
          • Vl-datatypelist
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expression-sizing

Vl-parse-keyval-pattern-array

Signature

(vl-parse-keyval-pattern-array fields range orig-x ctx warnings) 
  → 
(mv successp alist new-warnings)

Arguments

fields — Guard (vl-exprlist-p fields).

range — Guard (and (vl-range-p range) (vl-range-resolved-p range)).

orig-x — Guard (vl-expr-p orig-x).

ctx — Guard (vl-context-p ctx).

warnings — Guard (vl-warninglist-p warnings).

Returns

successp — Type (booleanp successp).

alist — Type (vl-expr-val-alist-p alist).

new-warnings — Type (vl-warninglist-p new-warnings).

Definitions and Theorems

Function: vl-parse-keyval-pattern-array

(defun vl-parse-keyval-pattern-array
       (fields range orig-x ctx warnings)
 (declare (xargs :guard (and (vl-exprlist-p fields)
                             (and (vl-range-p range)
                                  (vl-range-resolved-p range))
                             (vl-expr-p orig-x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-parse-keyval-pattern-array))
  (declare (ignorable __function__))
  (b*
   ((warnings (vl-warninglist-fix warnings))
    (ctx (vl-context-fix ctx))
    (orig-x (vl-expr-fix orig-x))
    ((when (atom fields))
     (mv t nil warnings))
    (pair (vl-expr-fix (car fields)))
    ((unless (and (not (vl-atom-p pair))
                  (eq (vl-nonatom->op pair)
                      :vl-keyvalue)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Expected key-value pairs in assignment ~
                                  pattern ~a1 (bad: ~a2)"
       :args (list ctx orig-x pair))))
    (pair.args (vl-nonatom->args pair))
    (idx (first pair.args))
    (defaultp (and (vl-atom-p idx)
                   (equal (vl-atom->guts idx)
                          (vl-keyguts :vl-default))))
    ((unless (or defaultp (vl-expr-resolved-p idx)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Expected keys in array keyval pattern ~
                                  to be integers (except for default): ~a1 ~
                                  (bad: ~a2)"
       :args (list ctx orig-x pair))))
    (key (if defaultp :default
           (vl-resolved->val idx)))
    ((unless
          (or defaultp
              (and (<= key
                       (vl-resolved->val (vl-range->msb range)))
                   (<= (vl-resolved->val (vl-range->lsb range))
                       key))
              (and (<= (vl-resolved->val (vl-range->msb range))
                       key)
                   (<= key
                       (vl-resolved->val (vl-range->lsb range))))))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Assign pattern key out of range for ~
                                  array type: ~a1 (bad: ~a2)"
       :args (list ctx orig-x pair))))
    ((mv rest-ok rest warnings)
     (vl-parse-keyval-pattern-array (cdr fields)
                                    range orig-x ctx warnings)))
   (mv rest-ok
       (cons (cons key (second pair.args))
             rest)
       warnings))))

Theorem: booleanp-of-vl-parse-keyval-pattern-array.successp

(defthm booleanp-of-vl-parse-keyval-pattern-array.successp
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-array
             fields range orig-x ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-expr-val-alist-p-of-vl-parse-keyval-pattern-array.alist

(defthm vl-expr-val-alist-p-of-vl-parse-keyval-pattern-array.alist
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-array
             fields range orig-x ctx warnings)))
    (vl-expr-val-alist-p alist))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-parse-keyval-pattern-array.new-warnings

(defthm
     vl-warninglist-p-of-vl-parse-keyval-pattern-array.new-warnings
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-array
             fields range orig-x ctx warnings)))
    (vl-warninglist-p new-warnings))
  :rule-classes :rewrite)

Theorem: vl-exprlist-max-count-of-vl-parse-keyval-pattern-array

(defthm vl-exprlist-max-count-of-vl-parse-keyval-pattern-array
 (<
  (vl-exprlist-max-count
       (alist-vals (mv-nth 1
                           (vl-parse-keyval-pattern-array
                                fields range orig-x ctx warnings))))
  (vl-exprlist-count fields))
 :rule-classes :linear)

Theorem: vl-parse-keyval-pattern-array-of-vl-exprlist-fix-fields

(defthm vl-parse-keyval-pattern-array-of-vl-exprlist-fix-fields
 (equal
  (vl-parse-keyval-pattern-array (vl-exprlist-fix fields)
                                 range orig-x ctx warnings)
  (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-array-vl-exprlist-equiv-congruence-on-fields

(defthm
 vl-parse-keyval-pattern-array-vl-exprlist-equiv-congruence-on-fields
 (implies
  (vl-exprlist-equiv fields fields-equiv)
  (equal
    (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)
    (vl-parse-keyval-pattern-array fields-equiv
                                   range orig-x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-array-of-vl-expr-fix-orig-x

(defthm vl-parse-keyval-pattern-array-of-vl-expr-fix-orig-x
 (equal
  (vl-parse-keyval-pattern-array fields range (vl-expr-fix orig-x)
                                 ctx warnings)
  (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-array-vl-expr-equiv-congruence-on-orig-x

(defthm
   vl-parse-keyval-pattern-array-vl-expr-equiv-congruence-on-orig-x
 (implies
  (vl-expr-equiv orig-x orig-x-equiv)
  (equal
   (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)
   (vl-parse-keyval-pattern-array fields
                                  range orig-x-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-array-of-vl-context-fix-ctx

(defthm vl-parse-keyval-pattern-array-of-vl-context-fix-ctx
 (equal
  (vl-parse-keyval-pattern-array
       fields range orig-x (vl-context-fix ctx)
       warnings)
  (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-array-vl-context-equiv-congruence-on-ctx

(defthm
   vl-parse-keyval-pattern-array-vl-context-equiv-congruence-on-ctx
 (implies
  (vl-context-equiv ctx ctx-equiv)
  (equal
   (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)
   (vl-parse-keyval-pattern-array fields
                                  range orig-x ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-array-of-vl-warninglist-fix-warnings

(defthm vl-parse-keyval-pattern-array-of-vl-warninglist-fix-warnings
 (equal
  (vl-parse-keyval-pattern-array fields range orig-x
                                 ctx (vl-warninglist-fix warnings))
  (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-array-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-parse-keyval-pattern-array-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
   (vl-parse-keyval-pattern-array fields range orig-x ctx warnings)
   (vl-parse-keyval-pattern-array fields
                                  range orig-x ctx warnings-equiv)))
 :rule-classes :congruence)