Skip to content

Conversation

@byd110
Copy link
Collaborator

@byd110 byd110 commented Sep 16, 2025

In #1099, the optimization (applied in #259) is reverted because it causes test failure in #1097. This PR reapply this optimization and fix the problem that causes the test failure.

Problem Description:

The test failure happens when the TransferResult is regular when visiting a boolean expression. This is because the visit methods of equality and inequality checks assume that the transfer result they get is conditional. They do refinement on both stores and return the same result. However, the refinement on the else store is not recorded to the given regular transfer result, which raised the false positive.

Solution:

This PR fix this problem by adding a check in visit methods of boolean expressions. If result is regular, then turn it into conditional with same ThenStore and ElseStore.

Evaluation:

No test failure with this fix. Also looks into the same test case as in 2e14088. The store number also drops to 484. Additionally, compared the number of stores. It drops from 2227 on master branch to 1676 after this fix, which is around 25% reduction.

Possible Future Work

Currently, we only fix the problem for this specific Nonemtpy checker. However, there could be a way to prevent this from happening. The idea is described in #1401. Also, there is a abandoned PR #1378 that made a little attempt. Maybe worth coming back in the future if the need grows.

… NonEmptyTransfer.java, adapt the test case accordingly, and update CHANGELOG.md
@byd110 byd110 marked this pull request as ready for review September 19, 2025 18:06
@byd110
Copy link
Collaborator Author

byd110 commented Sep 25, 2025

Create a new issue #1407 to mention the handling of boolean variables.

@byd110 byd110 requested a review from wmdietl September 26, 2025 00:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants