Fix for #204

[fedotovalex]

This fixes #204.

The culprit turned out to be the IL generated by Roslyn for comparing references to null. In the old compiler, o => o != null results in

    ldarg.0
    ldnull
    ceq
    ldc.i4.0
    ceq
    ret

which literally translates to (o == null) == 0.

In Roslyn, the same code results in

    ldarg.1
    ldnull
    cgt.un
    ret

which literally translates to o > null. While this is a clever trick and produces shorter IL, it doesn't match implicit non-null assumptions generated by the static checker and thus results in unproven assertions.

The fix is to recognize the cases when cgt.un is used to compare to null and make them look like o != null to the static checker.

[sharwell]

❓ What does o => null != o generate?

[fedotovalex]

❓ What does o => null != o generate?

It still produces cgt.un, with or without optimization.

[sharwell]

It still produces cgt.un, with or without optimization.

And the null is still on the right?

[fedotovalex]

And the null is still on the right?

Yes. It is the same exact sequence:

    ldarg.1
    ldnull
    cgt.un
    ret

[sharwell]

💭 Consider rewording this paragraph. I don't feel that the references to "Roslyn" and "old-style equality comparison" help the reader understand why this code is needed. In fact, even if Roslyn didn't use this style of null check, it would still make since to include this. The following comes to mind.

Since there is no cne instruction, ECMA-335 §III.1.5 makes a note that cgt.un may be used instead for the specific case where the right-hand-side is null. For all integer inputs to the cgt.un instruction, if the right side is null or zero, we treat the instruction as a "not equal" instruction for improved results from the static checker.

[sharwell]

Yes. It is the same exact sequence:

I checked the specification and it calls out cgt.un specifically as a cne-equivalent for null checking. Based on this it doesn't look like you need any other special cases in code.

[fedotovalex]

The following comes to mind.

Since there is no cne instruction, ECMA-335 §III.1.5 makes a note that cgt.un may be used instead for the specific case where the right-hand-side is null. For all integer inputs to the cgt.un instruction, if the right side is null or zero, we treat the instruction as a "not equal" instruction for improved results from the static checker.

This is a stronger statement than what's implemented. The code only deals with nulls on the right hand side, but not with integer zero. So, how about this:

Since there is no cne instruction, ECMA-335 §III.1.5 makes a note that cgt.un may be used instead for the specific case where the right-hand-side is null. If the right side is null, we treat the instruction as a "not equal" instruction for improved results from the static checker.

[sharwell]

👍

[yaakov-h]

Oh, that explains some of the more subtle behaviours I saw when trying to compile the bug report. Nice work!

[SergeyTeplyakov]

Awesome job, guys! Merged.