Контракты и удаленный код

Как вы, наверное, знаете, библиотека Code Contracts использует переписывание IL кода для реализации контрактного программирования. Это «архитектурное» решение является вполне логичным, с одной стороны, поскольку позволяет использовать эту библиотеку с любыми языками программирования на платформе .NET. Но, с другой стороны, это приводит к массе проблем, поскольку ccrewrite должен «реверс-инжинирить» IL код в высокоуровневые конструкции и переписывать его специальным образом.

Сегодня я хочу рассмотреть одно из последствий работы на IL уровне, которое может приводить к неожиданным результатам и порассуждать о возможных решениях.

Итак, давайте рассмотрим следующий код:

var hashSet = new HashSet<int>();
Debug.Assert(hashSet.Add(42));

В этом примере показана одна из типовых ошибок программирования, когда действие с побочным эффектом выполняется внутри «условно компилируемой функции». В этом случае, мы проверяем некоторое предположение, которое должно быть верным, но поведение приложения будет зависеть от наличия/отсутствия директивы DEBUG. Теперь, предположим, что вместо класса Debug мы используем контракты. Но, поскольку мы люди вумные, то вместо вызова hashSet.Add прямо внутри вызова метода Contract.Assert, мы выделили локальную переменную:

var hashSet = new HashSet<int>();
var b = hashSet.Add(42);
Debug.Assert(b);

Насколько это поведение является корректным? Контракты не используют условную компиляцию для удаления предусловий/постусловий или утверждений. Точнее, условная компиляция присутствует и без символа CONTRACT_FULL все упоминания о контрактах вообще будут удалены. Но более fine grained настройка осуществляется уже во время исполнения. ccrewrite оставляет предусловия/постусловия или утверждения в зависимости от настроек.

К тому же, мы вызываем метод Add за пределами метода Assert, поэтому даже если мы запустим этот код в режиме с отключенными утверждениями, hashSet должен содержать значение 42. Правда? Может быть.

Ответ зависит от того, как будет вести себя компилятор C# и не заинлайнит ли он переменную b. Компилятор может решить, что временная переменная не очень нужна и преобразовать этот код в следующий:

var hashSet = new HashSet<int>();
Debug.Assert(hashSet.Add(42));

В этом случае, если в свойствах Code Contracts будет указано не включать утверждения (например, выбрано, Preconditions или PreAndPost), то в ccrewrite удалит метод Contract.Assert вместе с вызываемым кодом hashSet.Add.

И вот тут мы приходим к очень грустному выводу: изначальная архитектура ccrewrite оказалась очень хрупкой и зависимой от поведения компилятора. Если даже пользователь выделил локальную переменную, но использовал ее только в Assert/Assume, то поведение приложения может меняться, в зависимости от того, была ли она заинлайнена переменная или нет.

VS2015 обладает более агрессивной оптимизацией по сравнению с VS2013. И мы получаем, что предыдущий код, который всегда нормально работал в VS2013, перестанет работать в VS2015! (Вот здесь идет обсуждение этой проблемы).

Интересно, что ccrewrite не всегда удаляет утверждения. Если утверждение (Assert/Assume) содержит более сложное условие (например, && или ||), то ccrewrite удалит лишь вызов метода Contract.Assert/Assume, но оставит на стеке вычисление аргумента (что, ИМХО, является багом).

Например, следующий код будет «корректно» работать даже в VS2015 и вызов метода hashSet.Add останется в результирующем коде:

var hashSet = new HashSet<int>();
Contract.Assert(hashSet.Add(42) || Ignore());
// Выводит 1 даже в VS2015 в Release режиме и с Preconditions Only контрактами
Console.WriteLine(hashSet.Count);

Итак, что же делать?

Самое неприятное в этой ситуации то, что «корректного» поведения в рамках текущей архитектуры ccrewrite добиться сложно, если вообще возможно.

Итак, есть два варианта:

1. ccrewrite удаляет лишь вызов методов Contract.Assert, но оставляет вычисление первого аргумента на стеке.

Pros: поведение будет стабильным и не будет зависеть от оптимизаций компилятора.

Cons:

• без условной компиляции не получиться удалить вызовы дорогостоящих методов, типа Contract.Assert(CheckSomeAssumptionThatHasNoSideEffectsButTakesForever).
• Потенциально страдает эффективность.

2. ccrewrite удаляет вызовы Contract.Assert/Assume со всеми аргументами.

Pros: это текущее поведение и оно согласовывается с поведением Debug.Assert.
Cons:

• поведение программы меняется в зависимости от оптимизации компилятора, которые совершенно не ясны для пользователя.
• Потенциально страдает корректность.

Я склоняюсь к мысли, что текущее поведение нужно менять, ОСОБЕННО при переходе к VS2015. Так что в новой версии Code Contracts все выражения, присутствующие в методах Contract.Assert/Assume будут оставаться в результирующей сборке, даже когда сами вызовы методов будут вырезаны.

З.Ы. Мне очень интересно ваше мнение. Насколько старой поведение логично? Насколько новое поведение лучше/хуже и нет ли более подходящего решения?