		Search-engine friendly clone of the ACL2 documentation.

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 origx ss) → oddinfos
Arguments: op1 — Outer operator, joins a and x.
Guard (vl-binaryop-p op1).; a — The simple argument (not to be looked inside).
Guard (vl-expr-p a).; x — The complex argument (contains the inner operator, if any).
Guard (vl-expr-p x).; flipped — Nil means the original expression was a op x, T means it was x op a.
Guard (booleanp flipped).; origx — Guard (vl-expr-p origx).; ss — Guard (vl-scopestack-p ss).
Returns: oddinfos — Type (vl-oddinfolist-p oddinfos).

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 origx ss)
 (declare (xargs :guard (and (vl-binaryop-p op1)
                             (vl-expr-p a)
                             (vl-expr-p x)
                             (booleanp flipped)
                             (vl-expr-p origx)
                             (vl-scopestack-p ss))))
 (declare (ignorable flipped))
 (let ((__function__ 'vl-warn-odd-binary-expression-main))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x))
       (a (vl-expr-fix a))
       (origx (vl-expr-fix origx)))
   (vl-expr-case
    x :vl-binary
    (b* ((op2 x.op)
         (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 (cdr look)) nil)
         (asize (vl-expr-probable-selfsize a ss))
         (xsize (vl-expr-probable-selfsize x ss)))
     (case
         (cdr look)
         ((:check-precedence)
          (if (assoc-equal "VL_EXPLICIT_PARENS" x.atts)
              nil
            (list (make-vl-oddinfo :type :check-precedence
                                   :subexpr origx
                                   :simple a
                                   :swidth asize
                                   :complex x
                                   :cwidth xsize))))
         (:check-type (if (assoc-equal "VL_EXPLICIT_PARENS" x.atts)
                          nil
                        (list (make-vl-oddinfo :type :check-type
                                               :subexpr origx
                                               :simple a
                                               :swidth asize
                                               :complex x
                                               :cwidth xsize))))
         (:check-type-unless-topargs-boolean
              (b* (((when (assoc-equal "VL_EXPLICIT_PARENS" x.atts))
                    nil)
                   (asize (vl-expr-probable-selfsize a ss))
                   (xsize (vl-expr-probable-selfsize x ss))
                   ((when (and (or (eql asize 1) (not asize))
                               (or (eql xsize 1) (not xsize))))
                    nil))
                (list (make-vl-oddinfo :type :check-type
                                       :subexpr origx
                                       :simple a
                                       :swidth asize
                                       :complex x
                                       :cwidth xsize))))
         ((:check-precedence-plusminus) nil)
         (otherwise (raise "Unexpected action type ~x0.~%"
                           (cdr look)))))
    :otherwise nil))))

Theorem: vl-oddinfolist-p-of-vl-warn-odd-binary-expression-main

(defthm vl-oddinfolist-p-of-vl-warn-odd-binary-expression-main
 (b*
  ((oddinfos
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))
  (vl-oddinfolist-p oddinfos))
 :rule-classes :rewrite)

Theorem: vl-warn-odd-binary-expression-main-of-vl-binaryop-fix-op1

(defthm vl-warn-odd-binary-expression-main-of-vl-binaryop-fix-op1
 (equal
     (vl-warn-odd-binary-expression-main (vl-binaryop-fix op1)
                                         a x flipped origx ss)
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-vl-binaryop-equiv-congruence-on-op1

(defthm
 vl-warn-odd-binary-expression-main-vl-binaryop-equiv-congruence-on-op1
 (implies
  (vl-binaryop-equiv op1 op1-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1-equiv a x flipped origx ss)))
 :rule-classes :congruence)

Theorem: vl-warn-odd-binary-expression-main-of-vl-expr-fix-a

(defthm vl-warn-odd-binary-expression-main-of-vl-expr-fix-a
 (equal
     (vl-warn-odd-binary-expression-main op1 (vl-expr-fix a)
                                         x flipped origx ss)
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-a

(defthm
   vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-a
 (implies
  (vl-expr-equiv a a-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1 a-equiv x flipped origx ss)))
 :rule-classes :congruence)

Theorem: vl-warn-odd-binary-expression-main-of-vl-expr-fix-x

(defthm vl-warn-odd-binary-expression-main-of-vl-expr-fix-x
 (equal
     (vl-warn-odd-binary-expression-main op1 a (vl-expr-fix x)
                                         flipped origx ss)
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-x

(defthm
   vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-x
 (implies
  (vl-expr-equiv x x-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1 a x-equiv flipped origx ss)))
 :rule-classes :congruence)

Theorem: vl-warn-odd-binary-expression-main-of-bool-fix-flipped

(defthm vl-warn-odd-binary-expression-main-of-bool-fix-flipped
 (equal
     (vl-warn-odd-binary-expression-main
          op1 a x (acl2::bool-fix flipped)
          origx ss)
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-iff-congruence-on-flipped

(defthm vl-warn-odd-binary-expression-main-iff-congruence-on-flipped
 (implies
  (iff flipped flipped-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1 a x flipped-equiv origx ss)))
 :rule-classes :congruence)

Theorem: vl-warn-odd-binary-expression-main-of-vl-expr-fix-origx

(defthm vl-warn-odd-binary-expression-main-of-vl-expr-fix-origx
 (equal
     (vl-warn-odd-binary-expression-main
          op1 a x flipped (vl-expr-fix origx)
          ss)
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-origx

(defthm
 vl-warn-odd-binary-expression-main-vl-expr-equiv-congruence-on-origx
 (implies
  (vl-expr-equiv origx origx-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1 a x flipped origx-equiv ss)))
 :rule-classes :congruence)

Theorem: vl-warn-odd-binary-expression-main-of-vl-scopestack-fix-ss

(defthm vl-warn-odd-binary-expression-main-of-vl-scopestack-fix-ss
 (equal
     (vl-warn-odd-binary-expression-main
          op1 a
          x flipped origx (vl-scopestack-fix ss))
     (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)))

Theorem: vl-warn-odd-binary-expression-main-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-warn-odd-binary-expression-main-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
       (vl-warn-odd-binary-expression-main op1 a x flipped origx ss)
       (vl-warn-odd-binary-expression-main
            op1 a x flipped origx ss-equiv)))
 :rule-classes :congruence)