Contract.Require(x != null) gets translated in "!(x <= null)" in the documentation rewritten by CC

[ndepend]

We have a lot of require not null contracts and I noticed that the contract formatting in the XML doc that used to be csharp="XYZ != null" is now csharp="!(XYZ <= null)". If I look in the xml generated I get:

// XML Generated Now     csharp="!(initialSeq <= null)"
<requires description="initialSeq must not be null" csharp="!(initialSeq &lt;= null)" vb="!(initialSeq &lt;= Nothing)">!(initialSeq &lt;= null)</requires>

// XML Generated Before  csharp="initialSeq != null"
<requires description="initialSeq must not be null" csharp="initialSeq != null" vb="initialSeq &lt;&gt; Nothing">initialSeq != null</requires>

Here is the contract declaration in the C# code:

// Contract declaration in the C# code
Contract.Requires(initialSeq != null, "initialSeq must not be null");

Here is the IL emitted from VS2015 (Update 1 RC) after being rewritten with 1.9.1:

IL_0000: ldarg.0
IL_0001: ldnull
IL_0002: cgt.un
IL_0004: ldstr "initialSeq must not be null"
IL_0009: ldstr "initialSeq != null"
IL_000e: call void System.Diagnostics.Contracts.__ContractsRuntime::Requires(bool, string, string)
IL_0013: nop
IL_0014: nop
IL_0015: br IL_001a

Here is the IL when compiled with VS2013 + Code Contract 1.7 if it can help:

L_0000: ldarg.0 
L_0001: ldnull 
L_0002: ceq 
L_0004: ldc.i4.0 
L_0005: ceq 
L_0007: ldstr "initialSeq must not be null"
L_000c: ldstr "initialSeq != null"
L_0011: call void System.Diagnostics.Contracts.__ContractsRuntime::Requires(bool, string, string)
L_0016: nop 
L_0017: ldarg.1 
L_0018: ldnull 
L_0019: ceq 
L_001b: ldc.i4.0 
L_001c: ceq

This is likely cause by Roslyn - Roslyn compiler emits x != null as x > null, whereas the old <= VS2013 compiler emitted it as (x == null) == 0 as you can see from the VS2013 IL above.

ccdocgen likely needs to be updated to understand that x > null also means x != null.

[sharwell]

I find the VS2013 IL very interesting. The explicit allowing of cgt.un for null checking has been in ECMA-335 for many years, and the benefit for this extremely common case is clear. The IL does make it obvious why you are seeing what you're seeing though! 😄

[ndykman]

I created a pull request with a fix for this specific issue. It's not a more general fix, just for CCDoc. There is an existing class that tries to simplify Boolean expressions for documentation generation. I just added an additional overriding method that looks at greater than expressions, and if it sees something like x > null, it rewrites it as x != null for the documentation.

[SergeyTeplyakov]

@ndykman Is it possible to add test case to cover this change?

[ndykman]

Would need some guidance on where to set that up. The current regression tests for CCDoc (Microsoft.Research/RegressionTest/CCDoc) would have caught the error if the test DLL was built with VS2015 (the XML wouldn't match the expected XML doc).

[ndepend]

@ndykman when you havea fix with bits compiled, I'll be glad to test. So far this issue still force us to keep some projects under VS2013 (those with CC, CC 1.7) and the other ones are under VS2015. Juggling with 2 IDEs is not convenient. Thanks

[SergeyTeplyakov]

@ndykman I can't remember right from my head is it possible to use the same approach that is used in Foxtrot tests: there are different cases for diferent C# compilers. If that would not be possible, I think it would be OK at least to test private bits with @psmacchia codebase to check whether the fix is good or not before accepting PR.

[ndepend]

If you have an url like https://ci.appveyor.com/project/hubuk/codecontracts/build/1.9.11201.50/artifacts with new bits including the fix, please let me know

[ndykman]

I will look into posting the build as requested.

[ndykman]

Still haven't a hard time not having AppVeyor not time out (only have the free plan). So, for now, use this link (http://1drv.ms/1lJBDpL) to get the MSI I built locally. Or, visit (http://1drv.ms/1lJBUcq) for a zipped version of the ccdocgen.exe executable only.

[ndepend]

Good news, the issue seems fixed with this last version!! I now get again XML like

<requires description="project must not be null" csharp="project != null" vb="project &lt;&gt; Nothing">

[ghost]

@ndykman I have a problem with your MSI version:
in a fresh installed VS2015 (Community) Update 1 I get the following error from the static checker:

CodeContracts: BitmapHeaderLibrary: Diagnostic: Failed to connect to any cache.
(1,1): warning : CodeContracts: System.Diagnostics.Contracts.ContractDeclarativeAssemblyAttribute.#ctor()[0x6]: Cannot connect to the cache. The CodeContracts static check will not run

[ndykman]

Oh, the build was intended to test the ccdocgen executable. It is possible that maybe something in my fork that is causing an issue, I will look into it.

ETA: I updated the MSI after rebasing my branch (minus the changes to BooleanExpressionHelper.cs)

[SergeyTeplyakov]

Merged and should be fixed.