• 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
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
          • Vl-modulelist-oddexpr-check
          • *vl-odd-binops-table*
          • Vl-warn-odd-binary-expression-main
          • Vl-expr-probable-selfsize
          • Vl-odd-binop-class
          • Vl-module-oddexpr-check
          • Vl-oddexpr-check
          • Vl-exprctxalist-oddexpr-check
          • Vl-design-oddexpr-check
          • Vl-warn-odd-binary-expression
          • Vl-pp-oddexpr-details
          • *fake-modelement*
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Oddexpr-check

Vl-warn-odd-binary-expression-main

Check the top-level of a binary expression for precedence problems.

Signature

(vl-warn-odd-binary-expression-main op1 a x flipped ss) → *

Arguments

op1 — Guard (vl-op-p op1).

a — Guard (vl-expr-p a).

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

flipped — Guard (booleanp flipped).

ss — Guard (vl-scopestack-p ss).

Note that any particular binary expression, say P OP Q, might have sub-structure in either the P argument or in the Q argument. To deal with this, in vl-warn-odd-binary-expression, we call this function twice:

• First with (OP P Q) and FLIPPED=NIL,
• Then with (OP Q P) and FLIPPED=T.

The first argument, A, we regard as the "simple" argument; we don't try to decompose it any more. However, we try to match X against B OP2 C. Then, we see if we think the sequence A op (B op2 C) seems reasonable.

Definitions and Theorems

Function: vl-warn-odd-binary-expression-main

(defun vl-warn-odd-binary-expression-main (op1 a x flipped ss)
  (declare (xargs :guard (and (vl-op-p op1)
                              (vl-expr-p a)
                              (vl-expr-p x)
                              (booleanp flipped)
                              (vl-scopestack-p ss))))
  (declare (ignorable a flipped))
  (let ((__function__ 'vl-warn-odd-binary-expression-main))
    (declare (ignorable __function__))
    (b* (((when (or (vl-fast-atom-p x)
                    (not (eql (vl-op-arity (vl-nonatom->op x))
                              2))))
          nil)
         (op2 (vl-nonatom->op x))
         (op1-class (vl-odd-binop-class op1))
         (op2-class (vl-odd-binop-class op2))
         (key (cons op1-class op2-class))
         (look (assoc-equal key *vl-odd-binops-table*))
         ((unless look) nil))
      (case (cdr look)
            ((:check-precedence)
             (if (assoc-equal "VL_EXPLICIT_PARENS"
                              (vl-nonatom->atts x))
                 nil
               :check-precedence))
            (:check-type (if (assoc-equal "VL_EXPLICIT_PARENS"
                                          (vl-nonatom->atts x))
                             nil
                           :check-type))
            (:check-type-unless-topargs-boolean
                 (b* (((when (assoc-equal "VL_EXPLICIT_PARENS"
                                          (vl-nonatom->atts x)))
                       nil)
                      (asize (vl-expr-probable-selfsize a ss))
                      (xsize (vl-expr-probable-selfsize x ss))
                      ((when (and (or (not asize) (eql asize 1))
                                  (or (not xsize) (eql xsize 1))))
                       nil))
                   :check-type))
            ((:check-precedence-plusminus)
             (if (and flipped
                      (not (assoc-equal "VL_EXPLICIT_PARENS"
                                        (vl-nonatom->atts x))))
                 :check-precedence
               nil))
            (nil nil)
            (otherwise (raise "Unexpected action type ~x0.~%"
                              (cdr look)))))))