1. Home
2. Blog
3. Contracts and Removed Code

As you probably know, the Code Contracts library uses the IL code rewriting to implement contract programming. This "architectural" solution, on the one hand, is quite logical because it allows you to use this library with any programming language of the .NET platform. But, on the other hand, it causes a lot of problems because ccrewrite has to “reverse engineer” the IL code into high-level constructs and rewrite it in a special way.

Today I want to consider one of the consequences of working on the IL level, which can lead to unexpected results, and speculate on possible solutions.

So, let's look at the following code:

This example shows one of the typical programming errors, when an action with a side effect is performed within a "conditionally compiled function". In this case, we test a hypothesis that must be true, but the behavior of the application will depend on the presence/absence of a DEBUG directive. Now, suppose that instead of the Debug class, we use contracts. But, since we are smart, instead of calling hashSet.Add directly from within the Contract.Assert method, we have allocated a local variable:

Is this behavior correct? Contracts do not use conditional compilation for removal of preconditions/postconditions and assertions. More precisely, conditional compilation is present and without the CONTRACT_FULL symbol, all mention of the contracts will be deleted. But a more fine grained configuration is carried out during the execution. Ccrewrite leaves preconditions/postconditions or assertions depending on the settings.

In addition, we call the Add method outside the Assert method, so even if we run this code in a mode with disabled assertions, hashSet must contain the value 42. Shouldn’t it? It may.

The answer depends on how the C# compiler will behave and whether it will inline the variable b. The compiler may decide that a temporary variable is not very necessary and convert this code into the following:

In this case, if in the properties of Code Contracts it will be specified not to include the assertions (for example, Preconditions or PreAndPost are selected), then ccrewrite will remove the Contract.Assert method together with the called hashSet.Add code.

And here we come to a very sad conclusion: the original ccrewrite architecture is very fragile and dependent on the behavior of the compiler. Even if the user has allocated a local variable, but used it only in Assert/Assume, the behavior of the application may vary depending on whether the variable has been inlined or not.

VS2015 has a more aggressive optimization than VS2013. And it occurs that the previous code that used to work fine in VS2013, stops working in VS2015! (Here is a discussion of this issue).

Interestingly, ccrewrite does not always remove assertions. If an assertion (Assert/Assume) contains a more complex condition (for example, && or ||), then ccrewrite will only remove the call of the Contract.Assert/Assume method, but will leave the calculation of the argument on the stack (which, IMHO, is a bug).

For example, the following code will "correctly" work even in VS2015, and the call of hashSet.Add method will remain in the resulting code:

So what can we do?

The worst thing in this situation is that it is difficult, if at all possible, to achieve a "correct" behavior under the current architecture of ccrewrite.

There are two options:

1. ccrewrite removes only the calls of Contract.Assert methods, but keeps the calculation of the first argument on the stack.

Pros: the behavior will be stable and will not depend on compiler optimizations.

Cons:

• Without conditional compilation you will not be able to remove the calls of costly methods, such as Contract.Assert(CheckSomeAssumptionThatHasNoSideEffectsButTakesForever).
• Efficiency will potentially suffer.

2. ccrewrite removes calls of Contract.Assert/Assume with all the arguments.

Pros: This is the current behavior and it is in line with the Debug.Assert behavior.

Cons:

• The behavior of the program varies depending on the compiler optimization which is totally unclear for the user.
• Correctness will potentially suffer.

I tend to think that the current behavior should be changed, ESPECIALLY in the transition to VS2015. So in the new version of Code Contracts all expressions, present in Contract.Assert/Assume methods, will remain in the resulting build, even when the calls themselves will be cut out.

P.S. I am very interested in your opinion. Is the old behavior logical? To what extent is the new behavior better/worse, and is there a more suitable solution?

Sergey Teplyakov
Expert in .Net, С++ and Application Architecture