Check the top-level of a binary expression for precedence problems.
(vl-warn-odd-binary-expression-main op1 a x flipped origx ss) → oddinfos
Note that any particular binary expression, say
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
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)