• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
          • Following-hids
            • Vl-follow-hidexpr
            • Vl-partselect-type-top-dimension-replacement
            • Vl-hidindex-datatype-resolve-dims
            • Vl-follow-hidexpr-error
            • Vl-follow-hidexpr-dimscheck
            • Vl-index-find-type
            • Vl-follow-hidexpr-dimcheck
            • Vl-partselect-expr-type
            • Vl-ss-find-hidexpr-range!!
            • Vl-hidstep
            • Vl-ss-find-hidexpr-range
            • Vl-genarrayblocklist-find-block
            • Vl-flatten-hidindex
            • Vl-hidexpr-resolved-p
            • Vl-flatten-hidexpr
            • Vl-hidindex-resolved-p
            • Vl-hidtrace
          • Vl-hidexpr-traverse-datatype
          • Abstract-hids
          • Vl-hidexpr-find-type
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Following-hids

Vl-follow-hidexpr-error

Report an error while following a HID.

Signature

(vl-follow-hidexpr-error short ss &key (ctx 'ctx) 
                         (origx 'origx) 
                         (x 'x)) 
 
  → 
warning

Arguments

short — Brief description of the error.
    Guard (stringp short).

ss — Detailed context for the error.
    Guard (vl-scopestack-p ss).

ctx — Original context for this HID.
    Guard (acl2::any-p ctx).

origx — Original, full HID being resolved.
    Guard (vl-expr-p origx).

x — Current place in the HID.
    Guard (vl-expr-p x).

Returns

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

This is smart in a few ways: it distinguishes between ordinary identifiers and hierarchical identifiers in the error type, and avoids providing excessive context if we haven't gotten anywhere down into the HID yet.

Definitions and Theorems

Function: vl-follow-hidexpr-error-fn

(defun vl-follow-hidexpr-error-fn (short ss ctx origx x)
 (declare (xargs :guard (and (stringp short)
                             (vl-scopestack-p ss)
                             (acl2::any-p ctx)
                             (vl-expr-p origx)
                             (vl-expr-p x))))
 (let ((__function__ 'vl-follow-hidexpr-error))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x))
       (origx (vl-expr-fix origx))
       (short (string-fix short))
       (type (if (vl-idexpr-p origx)
                 :vl-bad-identifier
               :vl-bad-hid))
       ((when (equal x origx))
        (make-vl-warning :type type
                         :msg "~a0: error resolving ~a1: ~s2."
                         :args (list ctx origx short)
                         :fn __function__)))
   (make-vl-warning
    :type type
    :msg
    "~a0: error resolving ~a1: ~s2.~%~
                           (Failed to resolve ~a3 in ~s4)."
    :args (list ctx
                origx short x (vl-scopestack->path ss))
    :fn __function__))))

Theorem: vl-warning-p-of-vl-follow-hidexpr-error

(defthm vl-warning-p-of-vl-follow-hidexpr-error
  (b* ((warning (vl-follow-hidexpr-error-fn short ss ctx origx x)))
    (vl-warning-p warning))
  :rule-classes :rewrite)

Theorem: vl-follow-hidexpr-error-fn-of-str-fix-short

(defthm vl-follow-hidexpr-error-fn-of-str-fix-short
  (equal (vl-follow-hidexpr-error-fn (str-fix short)
                                     ss ctx origx x)
         (vl-follow-hidexpr-error-fn short ss ctx origx x)))

Theorem: vl-follow-hidexpr-error-fn-streqv-congruence-on-short

(defthm vl-follow-hidexpr-error-fn-streqv-congruence-on-short
 (implies
    (streqv short short-equiv)
    (equal (vl-follow-hidexpr-error-fn short ss ctx origx x)
           (vl-follow-hidexpr-error-fn short-equiv ss ctx origx x)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-error-fn-of-vl-scopestack-fix-ss

(defthm vl-follow-hidexpr-error-fn-of-vl-scopestack-fix-ss
  (equal (vl-follow-hidexpr-error-fn short (vl-scopestack-fix ss)
                                     ctx origx x)
         (vl-follow-hidexpr-error-fn short ss ctx origx x)))

Theorem: vl-follow-hidexpr-error-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-follow-hidexpr-error-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
    (vl-scopestack-equiv ss ss-equiv)
    (equal (vl-follow-hidexpr-error-fn short ss ctx origx x)
           (vl-follow-hidexpr-error-fn short ss-equiv ctx origx x)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-error-fn-of-identity-ctx

(defthm vl-follow-hidexpr-error-fn-of-identity-ctx
  (equal (vl-follow-hidexpr-error-fn short ss (identity ctx)
                                     origx x)
         (vl-follow-hidexpr-error-fn short ss ctx origx x)))

Theorem: vl-follow-hidexpr-error-fn-equal-congruence-on-ctx

(defthm vl-follow-hidexpr-error-fn-equal-congruence-on-ctx
 (implies
    (equal ctx ctx-equiv)
    (equal (vl-follow-hidexpr-error-fn short ss ctx origx x)
           (vl-follow-hidexpr-error-fn short ss ctx-equiv origx x)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-error-fn-of-vl-expr-fix-origx

(defthm vl-follow-hidexpr-error-fn-of-vl-expr-fix-origx
 (equal (vl-follow-hidexpr-error-fn short ss ctx (vl-expr-fix origx)
                                    x)
        (vl-follow-hidexpr-error-fn short ss ctx origx x)))

Theorem: vl-follow-hidexpr-error-fn-vl-expr-equiv-congruence-on-origx

(defthm vl-follow-hidexpr-error-fn-vl-expr-equiv-congruence-on-origx
 (implies
    (vl-expr-equiv origx origx-equiv)
    (equal (vl-follow-hidexpr-error-fn short ss ctx origx x)
           (vl-follow-hidexpr-error-fn short ss ctx origx-equiv x)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-error-fn-of-vl-expr-fix-x

(defthm vl-follow-hidexpr-error-fn-of-vl-expr-fix-x
 (equal
     (vl-follow-hidexpr-error-fn short ss ctx origx (vl-expr-fix x))
     (vl-follow-hidexpr-error-fn short ss ctx origx x)))

Theorem: vl-follow-hidexpr-error-fn-vl-expr-equiv-congruence-on-x

(defthm vl-follow-hidexpr-error-fn-vl-expr-equiv-congruence-on-x
 (implies
    (vl-expr-equiv x x-equiv)
    (equal (vl-follow-hidexpr-error-fn short ss ctx origx x)
           (vl-follow-hidexpr-error-fn short ss ctx origx x-equiv)))
 :rule-classes :congruence)