SMTChecker: Loop conditions should be analyzed as in loop context in BMC

[blishko]

Value of loop condition can change between iterations of the loop.
Therefore, BMC should be in the "inside loop" state when analyzing loop conditions.

Previously, when visiting loop condition of a top-level loop, BMC engine did not consider itself being "inside loop", and therefore was checking if the condition is constant (always true or always false).
When the condition is always true in the first iteration and always false in the second iteration, BMC would try to report these two contradicting statements for the same source code expression, leading to an assertion violation in the UniqueErrorReporter.
Because the value of the condition can change between iteration, BMC should not try to check for constant condition in these cases.

As part of this PR the handling of the ConstantCondition verification target has been refactored (first commit).

Fixes #15847.

[cameel]

Following the change from #15880, I guess we don't want this check to be bypassed simply because it's in an unselected contract, right?

Suggested change

	(m_currentContract && !shouldAnalyze(*m_currentContract))
	(m_currentContract && !m_currentContract->canBeDeployed())

[blishko]

Correct! The code has been updated.

[cameel]

It looks to me like this will not exclude constants (bool constant C = true;), just literals (true), right?

Suggested change

	// Do not check for const-ness if this is a constant.
	if (dynamic_cast<Literal const*>(&_condition))
	// Do not check for const-ness if this is a literal.
	if (dynamic_cast<Literal const*>(&_condition))

[blishko]

I am still confused about constants in Solidity. But I believe you are right and I've updated to comment accordingly.

[cameel]

I think this test would be better off named top_level_for_loop_trivial_non_constant_condition.sol. It would better explain why we're checking this, not just what we're testing.

[blishko]

Actually, I don't think that captures the purpose of the test. I tried a different name.

[cameel]

Looks like the ICE isn't the only thing this PR fixes. 0.8.28 reports k == 0 as always false in this example:

contract Test {
    function loop() public pure {
        uint k = 0;
        while (k == 0 ? true : false) {
            ++k;
        }
    }
}

Warning: BMC: Condition is always false.
 --> test.sol:4:16:
  |
4 |         while (k == 0 ? true : false) {
  |                ^^^^^^
Note: Callstack:

The version from your branch does not.

I'm comparing with 0.8.28 binary though so there's also a chance it's the result of another, already merged fix.

[blishko]

You are right, this is the result of the current changes. I've updated the changelog entry, let me know what you think.

[cameel]

checkBooleanNotConstant()'s docstring needs to be updated. It still mentions that the function checks this.

[blishko]

I update the docstring. Actually, coming back to this function, I refactored it further to only perform the satisfiability checks and moved reporting of the result to the only caller.

[cameel]

You're adding/moving these in 3 different places, but you're only adding one new test case and not updating any existing ones. I suspect that we don't have coverage for all 3.

The example I posted under the changelog would probably cover one of them. What's the other one?

[blishko]

I've added you example with while loop, which covers the change in visit(WhileStatement).
The one test with for loop that I added originally actually exercises both changes in visit(ForStatement), so no additional test is needed.

[blishko]

To clarify, there are two places in visit(ForStatement) where the loop condition is visited:
Before each unrolling, and a final check when the loop no longer enters another iteration.
We needed to patch both places.