Contracts extraction and injection in constructors

Oct 9, 2010 at 11:55 PM
Edited Oct 10, 2010 at 12:10 AM

Hello, based on the sample HelloContracts I'm doing a tool that injects some contracts into an assembly. I've found a weird situation that I need some help on.

Consider this simple class with a contract in the constructor:

 

    class C
    {
        public int a { get; set; }

        public C()
        {
            System.Diagnostics.Contracts.Contract.Ensures(a == 42);
            a = 42;
        }
    }

 

The static checker of Code Contracts verifies the ensures with no problems, but if I read the assembly, extract the contracts with Microsoft.Cci.MutableContracts.ContractHelper.ExtractContracts and inject them again with Microsoft.Cci.MutableContracts.ContractHelper.InjectContractCalls without modifying them the Ensures is not validated anymore by the static checker. In fact, the static checker completely ignores the Ensures.

I did some debugging at the IL level to see how the assemblies differ and this is what I found:

IL of the constructor without extraction and injection (with some comments inserted):

.method public hidebysig specialname rtspecialname instance void .ctor() cil managed
{
    .maxstack 8
	
    //base()
    L_0000: ldarg.0 
    L_0001: call instance void [mscorlib]System.Object::.ctor()
    
    //ensures a == 42
    L_0006: ldarg.0 
    L_0007: call instance int32 N.C::get_a()
    L_000c: ldc.i4.s 0x2a
    L_000e: ceq 
    L_0010: call void [mscorlib]System.Diagnostics.Contracts.Contract::Ensures(bool)
	
    //a = 42
    L_0015: ldarg.0 
    L_0016: ldc.i4.s 0x2a
    L_0018: call instance void N.C::set_a(int32)
    
    //return
    L_001d: ret 
}

 

IL of the constructor doing extraction and injection (with some comments inserted):

.method public hidebysig specialname rtspecialname instance void .ctor() cil managed
{
    .maxstack 8
	
    //ensures a == 42
    L_0000: ldarg.0 
    L_0001: call instance int32 N.C::get_a()
    L_0006: ldc.i4.s 0x2a
    L_0008: ceq 
    L_000a: call void [mscorlib]System.Diagnostics.Contracts.Contract::Ensures(bool)
	
    //base()
    L_000f: ldarg.0 
    L_0010: call instance void [mscorlib]System.Object::.ctor()
	
    //a = 42
    L_0015: ldarg.0 
    L_0016: ldc.i4.s 0x2a
    L_0018: call instance void N.C::set_a(int32)
    
    //return
    L_001d: ret 
}

 

So, I concluded that problem is that Microsoft.Cci.MutableContracts.ContractHelper.InjectContractCalls always injects the contracts at the beginning of the method, and the Code Contracts' static checker doesn't seem to like that. The base() call for a constructor must be before the contracts for the static checker to work. My questions would be:

  • Is this a bug in the static checker of Code Contracts? Should I report that?
  • Is this a problem with the way the contracts injection is done? Should it inject the contracts after the base() call in constructors?
  • Is there some workaround?

Of course, modifying Microsoft.Cci.MutableContracts.ContractHelper.InjectContractCalls should be a possible solution, but I want to leave that as a last resource and I don't think that injecting the contracts at the beginning of a method is completely wrong.

I also tested this with virtual methods and overriding, where the call to the base method is explicit, and this problem doesn't exist, it seems to affect only constructors. 

Regards,

Jonathan

Oct 10, 2010 at 12:51 AM

Hello again, I did some digging in the AST code and found that the needed change was really simple, I submitted a patch with that change (ID 7027).

I'm not sure if it is correct for every case, but it works in all of my tests. It could fail when there isn't a call to a base constructor, or when that call has more than one statement.

Jonathan

Coordinator
Oct 11, 2010 at 2:49 AM

Thanks! Great catch! I've checked in the fix.