[SMTChecker] Fix comparison of CHCVerificationTarget for proper std::set ordering

[radik878]

What was changed

• Moved comparison logic from SafeTargetsCompare struct to CHCVerificationTarget::operator<
• Removed the SafeTargetsCompare struct completely
• Fixed a bug where == was used instead of < in the comparison operator
• Updated std::set<CHCVerificationTarget, SafeTargetsCompare> to use default std::set<CHCVerificationTarget>

[github-actions]

Thank you for your contribution to the Solidity compiler! A team member will follow up shortly.

If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother.

If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix.

[blishko]

LGMT!

Thanks for finding this out!
I am fine with merging this, but I will look into it further, because CHCVerificationTarget also provides operator<, which, however, works completely differently, which is weird.
I don't think we need both.

[blishko]

It looks like the operator< on CHCVerificationTarget is not really used now.
I think we should just replace the implementation of the operator with the fixed implementation of SafeTargetsCompare and then delete SafeTargetsCompare.

[radik878]

It looks like the operator< on CHCVerificationTarget is not really used now. I think we should just replace the implementation of the operator with the fixed implementation of SafeTargetsCompare and then delete SafeTargetsCompare.

Did i make changes correctly?

[cameel]

Just two general notes:

• The current state of the PR seems to be actually changing the behavior of the operator slightly, but no tests needed to be updated. That's always suspicious. Either we're missing test coverage or the code is not actually running.
• Please remember to update the PR/commit description if you change what the PR is about. Currently it still says it's doing what you originally tried to do, which is very misleading.

[blishko]

Yes, this is what I meant.

I've just noticed that there was an extra space, can you fix that as well?
Also, can you rebase your branch? I believe that should fix the external tests in CI.

[blishko]

• The current state of the PR seems to be actually changing the behavior of the operator slightly, but no tests needed to be updated. That's always suspicious. Either we're missing test coverage or the code is not actually running.

My understanding is that this only affects the order of verification targets proved safe.
If I remember correctly, we usually just count them and report the count to the user.
I'll have to think about a way to design a test for this.

• Please remember to update the PR/commit description if you change what the PR is about. Currently it still says it's doing what you originally tried to do, which is very misleading.

I agree, please update the description.

[blishko]

@cameel, I have checked the codebase and it turns out that the problematic piece of code (one fixed in this PR) is indeed never reached at the moment.

In current codebase the comparison is only used in std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> m_safeTargets, in the value, which is a set of CHCVerificationTarget, where the verification targets are sorted.
However, we only add two targets to the same set if they are associated with the same ASTNode, which is the key in the m_safeTargets map.
So we only have compare two targets if they have the same errorNode, which is exactly the if-condition of the comparison.

Thus currently, the bug was never triggered, but it was indeed a hidden bug in the implementation.

My conclusion is that other than a unit test, we are not able to test the changed place in the code, and we don't have unit tests, right?
So, I would merge this PR, after it is rebased and description updated, as is.

[radik878]

@cameel, I have checked the codebase and it turns out that the problematic piece of code (one fixed in this PR) is indeed never reached at the moment.

In current codebase the comparison is only used in std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> m_safeTargets, in the value, which is a set of CHCVerificationTarget, where the verification targets are sorted. However, we only add two targets to the same set if they are associated with the same ASTNode, which is the key in the m_safeTargets map. So we only have compare two targets if they have the same errorNode, which is exactly the if-condition of the comparison.

Thus currently, the bug was never triggered, but it was indeed a hidden bug in the implementation.

My conclusion is that other than a unit test, we are not able to test the changed place in the code, and we don't have unit tests, right? So, I would merge this PR, after it is rebased and description updated, as is.

updated description

[blishko]

Thanks!

[cameel]

My conclusion is that other than a unit test, we are not able to test the changed place in the code, and we don't have unit tests, right?

Well, we do have boost tests and do sometimes use unit tests for stuff we cannot reach with code snippets, but I agree - this one is not a case where I'd add one. It does not seem worth the effort. I pointed it out as a general precaution to the contributor, but if you checked the code and think it's fine, I trust your judgement here.

BTW, I disabled automerge because it got stuck and also because the commits need squashing first. This is a single change, it does not need 4 commits. Especially there should be no merge commits in there, those make history just unreadable.

[blishko]

I agree. @radik878 can you squash the commits?

[radik878]

I agree. @radik878 can you squash the commits?

Tough to say, 'Unable to squash. Squashing replays all commits up to the last one required for the squash. A merge commit cannot exist among those commits.'
This error and I don't know what to do with this

[cameel]

https://git-scm.com/book/en/v2/Git-Tools-Rewriting-History

[blishko]

You basically need to remove the merge commit, then you will be able to squash your three commits.
Do you need help with that?

[radik878]

You basically need to remove the merge commit, then you will be able to squash your three commits. Do you need help with that?

I tried but i don't know. Github desktop doesn't let me remove merge commit

[blishko]

Let me see if I can do something on my side.

It's a good idea to learn git directly (not relying solely on GitHub), it's a very useful skill!

[radik878]

Let me see if I can do something on my side.

It's a good idea to learn git directly (not relying solely on GitHub), it's a very useful skill!

It's really a good idea, I am convinced of this once again.