SMTChecker: Relax assertions regarding sort compatibility when creating expressions

[blishko]

This finishes the work started by #14180, which relaxed most of the assertions related to checking compatibility of sorts to allow mixing signed and unsigned Int sorts.

This PR has two parts:

1. Introduces a helper method that expresses the intent of the check and replaces if-then-else branches with this method call.
2. Relaxes one more assertion: in creating array store expression, we are checking if the array's domain sort and access index sort are compatible instead of equal.

Fixes #14792.

[matheusaaguiar]

LGTM, but I think maybe we could improve test coverage?

[matheusaaguiar]

What about mixing other types like mapping(bytes14 => int) and mapping(uint => bytes14)?
Also, I was looking at #14840 and noticed that in that in

solidity/test/libsolidity/smtCheckerTests/types/mapping_6.sol

Line 6 in ae9bcab

mapping(bool => int240) internal v1;

v1 is declared and not used. Although this is already merged I was wondering about that.

[matheusaaguiar]

I wanted to suggest a more meaningful name to this test too.
Maybe mapping_integer_signedness_compatibility/deletion ... I just think we should not continue the trend of just numbering these tests which contain mappings :)

[matheusaaguiar]

Still regarding the tests, could we also add tests involving arrays, i.e, int[] x, uint[10] y or does that makes no sense here?

[blishko]

Also, I was looking at #14840 and noticed that in that in

solidity/test/libsolidity/smtCheckerTests/types/mapping_6.sol

Line 6 in ae9bcab

mapping(bool => int240) internal v1;

v1 is declared and not used. Although this is already merged I was wondering about that.

The example in #14791 was crashing with this kind of mapping just being declared, but not used. So I kept it in the test.

[blishko]

I will rename the test, I agree that it should named properly.

What about mixing other types like mapping(bytes14 => int) and mapping(uint => bytes14)?

I can add more of these mappings, did not think of bytes. The problem was in the type of the domain vs the type of the index. I believe the type of the range should not actually matter.

Still regarding the tests, could we also add tests involving arrays, i.e, int[] x, uint[10] y or does that makes no sense here?

You mean declaring such arrays and then trying to access/delete some element?

[matheusaaguiar]

I can add more of these mappings, did not think of bytes. The problem was in the type of the domain vs the type of the index. I believe the type of the range should not actually matter.

Ok.

You mean declaring such arrays and then trying to access/delete some element?

Yes, but I am not sure if that makes sense in the context of the problem here.

[blishko]

@matheusaaguiar , I renamed the test, added a mapping with bytes and an array. Also added a changelog entry.

Do you think we can merge this?

[matheusaaguiar]

Approved.
We could squash commits, but that's more aesthetics than a requirement.