Eliminate pure-null if statements and merge simply nested ifs.
(vl-ifstmt-combine-rewrite condition truebranch falsebranch atts) → stmt
There are probably other things we could do here. For now, we just carry out two simple rewrites:
// Rewrite 1: if (test) --> null [null] else [null] // Rewrite 2: if (test1) if (test1 && test2) if (test2) --> body body
Function:
(defun vl-ifstmt-combine-rewrite (condition truebranch falsebranch atts) (declare (xargs :guard (and (vl-expr-p condition) (vl-stmt-p truebranch) (vl-stmt-p falsebranch) (vl-atts-p atts)))) (let ((__function__ 'vl-ifstmt-combine-rewrite)) (declare (ignorable __function__)) (b* ((fail-to-apply (make-vl-ifstmt :condition condition :truebranch truebranch :falsebranch falsebranch :atts atts)) ((when (and (vl-nullstmt-p truebranch) (vl-nullstmt-p falsebranch))) (make-vl-nullstmt)) ((unless (vl-ifstmt-p truebranch)) fail-to-apply) ((unless (vl-nullstmt-p falsebranch)) fail-to-apply) ((vl-ifstmt inner) truebranch) ((unless (vl-nullstmt-p inner.falsebranch)) fail-to-apply) (new-condition (make-vl-nonatom :op :vl-binary-logand :args (list condition inner.condition)))) (make-vl-ifstmt :condition new-condition :truebranch inner.truebranch :falsebranch falsebranch :atts (acons "VL_COMBINED_IF" nil atts)))))
Theorem:
(defthm vl-stmt-p-of-vl-ifstmt-combine-rewrite (implies (and (force (vl-expr-p condition)) (force (vl-stmt-p truebranch)) (force (vl-stmt-p falsebranch)) (force (vl-atts-p atts))) (b* ((stmt (vl-ifstmt-combine-rewrite condition truebranch falsebranch atts))) (vl-stmt-p stmt))) :rule-classes :rewrite)