Latest checkins to Contracts Extractor and Injector breaking loops

Oct 11, 2010 at 9:20 PM

Hello, I did an update of the CCI code and found some issues, given this code:

        public void M(int n)
        {
            System.Diagnostics.Contracts.Contract.Requires(n > 0);
            for (int i = 0; i < n; i++)
            {
            }
            for (int j = 0; j < n; j++)
            {
            }
        }

If I do a contract extraction and injection (without doing any modifications), the second loop is somewhat converted into some strange code, this is what it is converted to (decompiled by Reflector):

 

	public void M(int n)
	{
		Contract.Requires(n > 0);
		for (int i = 0; i < n; i++)
		{
		}
		int j = 0;
		goto Label_002E;
		j++;
		if (j >= n)
		{
			return;
			j = 0;
			goto Label_002E;
		}
	Label_002A:
		j++;
	Label_002E:
		if (j < n)
		{
			goto Label_002A;
		}
	} 

 

Although it may be correct, it is really weird, and a lot different with what the previous version did. Also, it seems to confuse the Code Contracts static checker, and some contracts aren't proven (when they previously were).

I have tested this incrementally adding each revision since 52118 and the problem seems to appear in revision 52128. Also, this only happens when there is a contract in the method, so it is definitely related to the contract extraction and injection.

Regards,

Jonathan

Coordinator
Oct 12, 2010 at 4:37 AM

Great catch! Actually I'm pretty sure it was *not* correct (put a Console.WriteLine within the loop and you should see what I mean), but I think I've fixed it now. Please try out change set 52181 and let me know if it works for you. I'd also be curious to find out what it is that you are doing with this code. Why would you feed the results of extraction and re-injection to the static checker? Or was that just for testing it out?

Oct 12, 2010 at 9:57 PM

Hi Mike, thanks for your time. Unfortunately the last rev breaks some stuff (may be it was a previous rev, I'm not sure), first of all I had to change some castings from Microsoft.Cci.MutableCodeModel.SourceMethodBody to Microsoft.Cci.ILToCodeModel.SourceMethodBody for my code to compile with the latest AST rev. After that, all the contracts that I'm injecting are now ignored, but the ones that originally were in the code are kept. Weird, because debugging I can see the ones I'm adding in the ContractProvider. Should I change the way I write the assembly back to the file? Seems like now it is always writing the original assembly instead of the modified one, because some code I insert isn't there neither.

As to what I'm doing: I'm developing a tool that reads some annotations in the code and injects some contracts and some code using a Mutator. All of this is done before the assembly reaches the Code Contracts' static checker (ccchecker), thus I can use my annotations that are transformed to contracts (plus code) and see the result in Visual Studio just like regular contracts. I can be seen as an extension of the native contracts implemented with native contracts. This is for a tool for memory consumption verification that I'm doing with Diego Garbervetsky at the University of Buenos Aires.

Jonathan

Coordinator
Oct 13, 2010 at 1:13 AM

Yes, I can believe you'd have to change to use the ILToCodeModel definition: I think that was one of the changes I made. I don't know why your injected  contracts should be getting ignored. Are you using the HelloContracts project as a starting point? You might also be interested in the CciSharp sample application in the CciSamples codeplex. It has a NotNull mutator that injects preconditions based on whether the associated parameter has a [NotNull] attribute on it.

Good to know that you are working with Diego! Say hello to him for me.

Oct 13, 2010 at 1:52 AM

Yes, I used the HelloContracts sample as a base for my code. In fact, I just tested the "Inject non-null postconditions" option of the HelloContracts console app with a very simple assembly (1 class, 1 method) and it isn't working with the latest rev, it just outputs an assembly equal to the input one, then I updated CCI to the rev 51735, recompiled, tested again and it worked. So, definitely something is broken after that rev, it isn't just my code.

I actually took some code from that EnsuresNotNullMutator class from CciSharp to build my mutator, it was very useful.

Jonathan

Coordinator
Oct 13, 2010 at 3:27 AM

Ooops. Sorry about that. I just checked in a fix. It was relying on the mutable method body being of a certain type, when it should just create a new mutable body and add the statements from any ISourceMethodBody. (I think it really should just decompile the method body if it isn't an ISourceMethodBody, but I haven't done that yet.)  I'm in the process of creating some regression tests for the contract injection so we (okay, I...) can (try to) avoid making problems like this in the future. I hope to check that in tomorrow. I'm glad that code helped!

Oct 14, 2010 at 2:10 AM

Thank you Mike, the last check in seems to fix the problem of the assembly not being written, however my original issue (two loops and the second one is broken in methods with contracts) have reappeared with the last checkin. It is isn't as blocking as the other one, but some of my contracts fail to be proven now. The example that I gave in the first post throws the same result, some crazy gotos.

Coordinator
Oct 21, 2010 at 2:45 AM

I just made a big checkin today. I hadn't tested it out before I did that, so maybe it was broken. But if I take the program below and compile it ("csc /debug /d:CONTRACTS_FULL foo.cs"), then run it through HelloContracts ("HelloContracts foo.exe") and then look at the result in Reflector everything looks fine. Can you try it after you sync up and let me know if you see any problems? Then I will check that in as a regression test to make sure this doesn't happen again!

using System;
public class C{
  public void M(int n){
    System.Diagnostics.Contracts.Contract.Requires(n > 0);
    for (int i = 0; i < n; i++) {
      Console.WriteLine(i);
    }
    for (int j = 0; j < n; j++) {
      Console.WriteLine(j);
    }
  }
  public string N(){
    return "abc";
  }
}
public class M{
  public static void Main(){
    new C().M(3);
  }
}
Oct 21, 2010 at 8:56 PM

Great, with the last version everything works as expected. I had to make a little change in my code to use CodeContractAwareHostEnvironment instead of PeReader.DefaultHost like HelloContracts.

Thank you!

Coordinator
Oct 21, 2010 at 9:05 PM

Yes, you have to use the CodeContractAware host because the extractor now depends on having an implementation of IContractAwareHost instead of just an ordinary IMetadataHost. That is because we are now supporting abbreviators and validators: a way to encapsulate contracts within a method and then use that method instead of explicit contract calls. Since those methods could be defined anywhere, extracting a contract is no longer a local operation that can be done on (the code model of) a method body in isolation. If the extractor sees a call to an abbreviator, e.g., then it needs to be able to access the contract the abbreviator represents. It does this through the functionality of the IContractAwareHost.