Code Contracts warn of "ensures unproven" when locks are involved

Question

I'm trying to work out how .NET Code Contracts interact with the lock keyword, using the following example:

public class TestClass
{
  private object o1 = new object();
  private object o2 = new object();

  private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      this.o1 = new object();
    }
  }
}

When I run the Code Contract static analysis tool, it prints a a warning: Ensures unproven: this.o1 != null

If I do any of:

• change the o2 in the lock to o1,
• change the o1 inside the lock block to o2,
• adding a second line inside the lock block assigning a new object to o2
• change lock (this.o2) to if (this.o2 != null),
• remove the lock statement entirely.

the warning disappears.

However, changing the line inside the lock block to var temp = new object(); (thus removing all references to o1 from the method) still causes the warning:

private void Test()
  {
    Contract.Requires(this.o1 != null);
    Contract.Requires(this.o2 != null);
    Contract.Ensures(this.o1 != null);

    lock (this.o2) {
      var temp = new object();
    }
  }

---

So there are two questions:

1. Why is this warning occurring?
2. What can be done to prevent it (bearing in mind this is a toy example and there's actually stuff happening inside the lock in the real code)?

Answer 1

Here's how the static checker treats locks and invariants:

If you lock something with the form lock(x.foo) { ... }, the static checker considers x.foo as the protecting lock of x. At the end of the lock scope, it assume that other threads might access x and modify it. As a result, the static checker assumes that all fields of x only satisfy the object invariant after the lock scope, nothing more.

Note that this is not considering all thread interleavings, just interleavings at end of lock scopes.

Answer 2

Add the following code to your class:

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(o1 != null);
    }

I couldn't tell you why, but in this case the static verifier does appear to consider private field assignment and an absence of methods that modify it as sufficient evidence that the field will not be modified. It could be a bug in the verifier? Might be worth reporting on the Code Contracts forum.