Is Code Contracts failing to spot obvious relationship between Nullable<T>.HasValue and null?

Question

I am experimenting with applying Code Contracts to my code and I've hit a perplexing problem. This code is failing to meet the contract but unless I'm being really thick I would expect it to be able to easily analyse that id must have a value at the point of return

if (id == null)
    throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

return id.Value;

Wardwarde

have you tried !id.HasValue? – Anaphylaxis

What is the definition of the id field? Is it perchance readonly? – Femme

Spot on Sven! - nice bit of psychic debugging :) (see below) – Wardwarde

Answer 1

I've got to the bottom of this behaviour and it is not Code Contract's fault.

I opened the generated assembly in ILSpy and this is the code that is produced:

public Guid Id
{
    get
    {
        Guid? guid = this.id;
        if (!guid.HasValue)
        {
            throw new InvalidOperationException();
        }
        guid = this.id;
        return guid.Value;
    }
}

The instance variable id is being copied to a local variable and this local variable is being reset back to its original value after the condition block. Now it became obvious why Code Contracts is showing a contract violation error but it still left me confused why the code was being rewritten in this form. I did a little more experimentation and took Code Contracts out of the project altogether and it became apparent that this is standard C# compiler behaviour, but why?

The secret appears to be due to a minor detail that I accidentally omitted from my original question. The id instance variable is declared as readonly and this seems to be responsible for causing the compiler to add the temporary guid variable.

I must admit I'm still confused why the compiler feels it needs to do this to ensure the guarantee of immutability for id but I'll keep digging...

Wardwarde

If you read the C# language spec, you'll find something that says that readonly fields of value types are not variables. Like properties, they are considered values, which for a value type means that all operations on them must be done on a copy. So just like when you access a property of a value type, every time you access a readonly field of a value type it produces a copy. The fact that I knew that was what led me to speculate that was your problem based on the decompiled code. – Femme

Thanks for the excellent explanation. That explains the mystery! – Wardwarde

Just looked it up, the relevant bits are in §7.6.4 of the C# language specification. – Femme

Answer 2

You might try copying the field to a local value and writing the statements in terms of that local value. The prover may be conservative about fields, since it's possible that a call could mutate the field value.

Ambassadoratlarge

Based on the discovered issue, I believe this will work. By explicitly creating the copy, it should only create the copy once, rather than twice (as in the implicit readonly case.) – Ambassadoratlarge

Answer 3

Its not seeing your if throw check as part of its contracts. Try this instead:

if (id == null)    
  throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

Contract.EndContractBlock();

http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.endcontractblock.aspx

Hartill

This is what I thought at first, but 'id' is a field here, so it's probably not appropriate to add a requirement (the client of the code may not be able to directly ensure that the requirement could be met.) It might make sense for this to be a class invariant (if 'id' should always be set), but otherwise it's purely a state check that shouldn't have caller requirements. – Ambassadoratlarge

The thing is your if then throw IS in fact a contract, whether or not your client can affect the outcome of the check or not. The only thing adding the EndContractBlock will do is let the CC pick up on the fact that your if then throw is a contract, which it currently doesn't know. – Hartill

that's true. It may be a good hint to encapsulate this state check in a visible property so that the client has a straightforward way of knowing whether it has fulfilled its end of the contract by putting the object in the right state for the call. – Ambassadoratlarge