• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • 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
          • 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
            • Vl-syscall->returninfo
            • Vl-*ary-syscall-p
            • Vl-unary-syscall-p
              • Vl-0ary-syscall-p
              • Vl-sysfun-should-size-args-p
              • Vl-$random-expr-p
              • Vl-sysfunexpr->name
              • Vl-sysfunexpr-p
              • Vl-unary-syscall->arg
            • 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
    • Syscalls

    Vl-unary-syscall-p

    Recognize calls of a particular unary system function call.

    Signature
    (vl-unary-syscall-p name x) → *
    Arguments
    name — Name of the particular system call, e.g., $bits.
        Guard (stringp name).
    x — Expression to test.
        Guard (vl-expr-p x).

    For instance, to see if x is a call of $bits, you could write:

    (vl-unary-syscall-p "$bits" x)

    Definitions and Theorems

    Function: vl-unary-syscall-p

    (defun vl-unary-syscall-p (name x)
      (declare (xargs :guard (and (stringp name) (vl-expr-p x))))
      (let ((__function__ 'vl-unary-syscall-p))
        (declare (ignorable __function__))
        (b* (((when (vl-fast-atom-p x)) nil)
             ((vl-nonatom x))
             ((unless (and (eq x.op :vl-syscall)
                           (consp x.args)
                           (consp (cdr x.args))
                           (atom (cddr x.args))))
              nil)
             (fn (first x.args))
             ((unless (vl-sysfunexpr-p fn)) nil))
          (equal (vl-sysfunexpr->name fn)
                 (string-fix name)))))

    Theorem: arity-stuff-about-vl-unary-syscall-p

    (defthm arity-stuff-about-vl-unary-syscall-p
      (implies (vl-unary-syscall-p name x)
               (and (not (equal (vl-expr-kind x) :atom))
                    (equal (vl-nonatom->op x) :vl-syscall)
                    (consp (vl-nonatom->args x))
                    (consp (cdr (vl-nonatom->args x)))
                    (vl-expr-p (cadr (vl-nonatom->args x)))))
      :rule-classes :forward-chaining)

    Theorem: vl-unary-syscall-p-of-str-fix-name

    (defthm vl-unary-syscall-p-of-str-fix-name
      (equal (vl-unary-syscall-p (str-fix name) x)
             (vl-unary-syscall-p name x)))

    Theorem: vl-unary-syscall-p-streqv-congruence-on-name

    (defthm vl-unary-syscall-p-streqv-congruence-on-name
      (implies (streqv name name-equiv)
               (equal (vl-unary-syscall-p name x)
                      (vl-unary-syscall-p name-equiv x)))
      :rule-classes :congruence)

    Theorem: vl-unary-syscall-p-of-vl-expr-fix-x

    (defthm vl-unary-syscall-p-of-vl-expr-fix-x
      (equal (vl-unary-syscall-p name (vl-expr-fix x))
             (vl-unary-syscall-p name x)))

    Theorem: vl-unary-syscall-p-vl-expr-equiv-congruence-on-x

    (defthm vl-unary-syscall-p-vl-expr-equiv-congruence-on-x
      (implies (vl-expr-equiv x x-equiv)
               (equal (vl-unary-syscall-p name x)
                      (vl-unary-syscall-p name x-equiv)))
      :rule-classes :congruence)