Check if a Java block has an ending
(atj-check-foldable-return block) → (mv yes/no pre-block test-expr then-block then-expr else-block else-expr)
We check whether the block has the structure described here. If it does, we return its components, i.e. the block that precedes the declaration of the result variable, the `then' block without the final assignment to the result variable, the expression assigned to the result variable in the `then' block, the `else' block without the final assignment to the result variable, and the expression assigned to the result variable in the `else' block.
If the first result of this function is
We prove that, if the first result is
Function:
(defun atj-check-foldable-return (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'atj-check-foldable-return)) (declare (ignorable __function__)) (b* (((fun (fail)) (mv nil nil (jexpr-name "") nil (jexpr-name "") nil (jexpr-name ""))) ((unless (>= (len block) 3)) (fail)) (pre-block (butlast block 3)) (rest-block (nthcdr (len pre-block) block)) (3rd-to-last-statem (car rest-block)) (2nd-to-last-statem (cadr rest-block)) (last-statem (caddr rest-block)) ((unless (jstatem-case last-statem :return)) (fail)) (return-expr? (jstatem-return->expr? last-statem)) ((when (null return-expr?)) (fail)) (return-expr return-expr?) ((unless (jexpr-case return-expr :name)) (fail)) (result-var (jexpr-name->get return-expr)) ((unless (jstatem-case 2nd-to-last-statem :ifelse)) (fail)) (test-expr (jstatem-ifelse->test 2nd-to-last-statem)) (then+asg-block (jstatem-ifelse->then 2nd-to-last-statem)) (else+asg-block (jstatem-ifelse->else 2nd-to-last-statem)) ((unless (and (consp then+asg-block) (consp else+asg-block))) (fail)) (then-block (butlast then+asg-block 1)) (else-block (butlast else+asg-block 1)) (then-asg (car (last then+asg-block))) (else-asg (car (last else+asg-block))) ((unless (and (jstatem-case then-asg :expr) (jstatem-case else-asg :expr))) (fail)) (then-asg (jstatem-expr->get then-asg)) (else-asg (jstatem-expr->get else-asg)) ((unless (and (jexpr-case then-asg :binary) (jexpr-case else-asg :binary) (jbinop-case (jexpr-binary->op then-asg) :asg) (jbinop-case (jexpr-binary->op else-asg) :asg) (equal (jexpr-binary->left then-asg) (jexpr-name result-var)) (equal (jexpr-binary->left else-asg) (jexpr-name result-var)))) (fail)) (then-expr (jexpr-binary->right then-asg)) (else-expr (jexpr-binary->right else-asg)) ((unless (jstatem-case 3rd-to-last-statem :locvar)) (fail)) (locvar (jstatem-locvar->get 3rd-to-last-statem)) ((unless (and (equal (jlocvar->name locvar) result-var) (equal (jlocvar->init? locvar) nil))) (fail))) (mv t pre-block test-expr then-block then-expr else-block else-expr))))
Theorem:
(defthm booleanp-of-atj-check-foldable-return.yes/no (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-check-foldable-return.pre-block (implies (and (jblockp block)) (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jblockp pre-block))) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-check-foldable-return.test-expr (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jexprp test-expr)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-check-foldable-return.then-block (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jblockp then-block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-check-foldable-return.then-expr (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jexprp then-expr)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-check-foldable-return.else-block (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jblockp else-block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-check-foldable-return.else-expr (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (jexprp else-expr)) :rule-classes :rewrite)
Theorem:
(defthm atj-check-foldable-return-then-decreases (implies (mv-nth 0 (atj-check-foldable-return block)) (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (< (jblock-count-ifs then-block) (jblock-count-ifs block)))) :rule-classes :linear)
Theorem:
(defthm atj-check-foldable-return-else-decreases (implies (mv-nth 0 (atj-check-foldable-return block)) (b* (((mv ?yes/no ?pre-block ?test-expr ?then-block ?then-expr ?else-block ?else-expr) (atj-check-foldable-return block))) (< (jblock-count-ifs else-block) (jblock-count-ifs block)))) :rule-classes :linear)