понедельник, 9 ноября 2015 г.

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

Как вы, наверное, знаете, библиотека 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 будут оставаться в результирующей сборке, даже когда сами вызовы методов будут вырезаны.

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

21 комментарий:

  1. работу Debug.Assert очень просто объяснить "новому" разработчику...
    А за assert'ы с побочными эффектами разве на костре не сжигают?

    ОтветитьУдалить
    Ответы
    1. Как пояснил Сергей, assert с побочным эффектом может возникнуть как результат оптимизации компилятора. В том и проблема. Компилятор сжигать на костре не хочется.

      Удалить
    2. Выстрелить в ногу можно на любом языке; при корректном разделении на Command/Query в ассертах никогда не должно быть вызовов, меняющих состояние.

      Удалить
    3. @Анатолий: да, сжигают:)) Но как теперь объяснить семантику Contract.Assert-а? Если код удаляется, то хорошо. Но он может удалить не то, что нужно и тогда вполне валидная программа станет работать неверно. И что делать - хз:(

      @Disparity: кажется в этом случае CQS не поможет. Или я не вижу, как он может помочь.

      Удалить
  2. Первый вариант конечно лучше, есть куча других способов удалить вызовы дорогостоящих методов.
    Also. Вот сколько я имел дело с code contracts, ни разу у меня не было чего нить типа

    Contract.Assert(CheckSomeAssumptionThatHasNoSideEffectsButTakesForever)

    не могу аргументировано подтвердить, но мой скромный опыт подсказывает, что при нормальном дизайне в пред/постусловиях нет дорогостоящх вызовов

    ОтветитьУдалить
    Ответы
    1. В моем проекте есть пара мест с таким поведением, но их реально пара. Так что я склоняюсь к первому варианту, поскольку, как ты правильно заметил, есть кучас способов удалить дорогостоящий метод, но понять, что твой код перестал рабоать из-за удаления нужного - очень сложно.

      Удалить
  3. А нельзя выдавать ворнинг если ccrewrite удаляет потенциально важный вызов (например, не-pure метод)? В качестве компромиссного фикса в ответ на такой ворнинг можно было бы предусмотреть какую-то дополнительную конструкцию (или параметр метода, такого как Assert), указывающую, что следующий кусок надо оставить. Самая близкая аналогия, которая приходит на ум - GC.KeepAlive - метод, который ничего не делает, но заставляет думать JIT, что ссылка нужна до указанного момента.

    ОтветитьУдалить
    Ответы
    1. Андрей, очень дельный совет, спасибо.

      Я только не уверен, что в природе существует разумный способ понять, какой метод Pure, а какой - нет. Но, в любом случае, даже с текущими знаниями о pure/impure это будет полезно.

      Я бы сказал, что можно даже усилить это прваило и выдавать предупреждение каждый раз, когда в контракте используется non-pure метод, не зависимо от того, удаляется этот вызов или нет (ведь раз этот вызов есть, то он МОЖЕТ быть удален).

      Удалить
  4. Нет ли возможности определить, есть ли в выражении побочные эффекты?

    Напр. отсутствие аттрибута [Pure] в методе HastSet.Add, должно подсказывать, что побочные эффекты все же могут быть.

    ОтветитьУдалить
    Ответы
    1. Да, этот вопрос очень похож на тот, что поднял Андрей в предыдущем комментарии. Нужно будет попробовать что-то такое сделать.

      Удалить
  5. Есть вариант оставить обе стратегии и выбирать из них. При этом ОГРОМНЫМИ буквами писать, что второй вариант - на свой риск и страх. Может кто-то хочет выгадать что-то по производительности? Но вообще - первый вариант - 99%. И еще, надо чтобы выбрать второй вариант - было как-то ОЧЕНЬ сложно :). Чтобы случайно не получилось...

    ОтветитьУдалить
    Ответы
    1. Этот вариант кажется вполне разумным. тут нужно определиться с дефолтом. Я склоняюсь к тому, что новый вариант должен быть дефолтом, а старый в опциях можно будет вернуть.

      Удалить
  6. Переписывание IL-кода может и выглядеть вполне логичным решением, но позволить некой софтине внутри которой есть метод MikesArchitecture переписывать IL - ну, скажем так, наш тимлид первым делом спросил переписывает ли оно IL, и, узнав, что переписывает навсегда зарубил контракты в такой реализации. И это можно понять, потому что просто страшно.

    ОтветитьУдалить
    Ответы
    1. А мне даже возразить нечего:) Ни по поводу MikesArchitecture, ни по поводу переписывания... :((

      Ну, с хорошим дизайном и модульностью эту адскую сложность можно было бы еще держать под контролем, но в текущем варианте это сделать довольно сложно...

      Удалить
  7. Благодоря этому "класссному" архетиктурному решению - офигенная библиотека превратилась в шлак, который никто не использует.
    Большенству непонятно как её настраивать, у кого-то проблемы с подписанными сборками, всех бесит что это НЕ встроенно в студию а надо доставлять, допиливать, донастраивать.
    А такая классная тема была!

    ОтветитьУдалить
    Ответы
    1. Ну, там история у проекта довольно интересная.
      Поскольку он начинался как ресерч проект, то других вариантов просто не было. Обычно после того, как было доказано, что идея стоящая, все текущее творение выбрасывается и тула переписывается с нуля. Но, к сожалению, второго (переписывания) так и не произошло((

      Удалить
  8. А есть хотя бы обсуждение, что CC надо бы переписать с нуля? С использованием Roslyn теперь уже. Я так понимаю, что обсуждение встраивания контрактов в язык, есть, но на очень базовом уровне. https://github.com/dotnet/roslyn/issues/119
    Я бы предпочел использовать тулу, которая перестраивает C# код, а не IL.

    ОтветитьУдалить
    Ответы
    1. Игорь, с переписыванием на базе Розлина есть несколько открытых проблем/вопросов.

      1. Розлин не предоставляет точку расширения перед эмиттингом IL-а. Т.е. придется городить огород - переписывать C# в C#, а потом что-то хитрое делать, чтобы сгенерированный C# не мешал отладке. Как это сделать нормально - не ясно.

      2. Даже если решить первый вопрос, остается несколько вопросов. Например, поведение контрактов для конструкторов наследников - проверка должна выполняться до вызова конструкторов базового класса. Или, в случае с async методами и блоками итераторов. Там простого синтаксического преобразования будет недостаточно, поскольку важно выбрасывать нарушение контракта как можно раньше. Сейчас ccrewrite делает разные трюки по вытаскиванию контрактов из сгенерированного конечного автомата в исходный метод.

      Ну и последнее, пока никто не хочет вкладывать в это дело существенных средств, которые, явно для этого потребуются...

      Удалить
    2. Насколько я знаю, сейчас Roslyn вообще расширения компилятора не поддерживает, т.е. даже C# в C# переписать не выйдет. Если нет - поправьте меня, буду очень рад увидеть обратное.
      ИМХО, единственый шанс для code contracts, это даже не включение в язык контактов, а создание расширения языка и компилятора, после чего уже можно будет все детали продумывать, типа ситуации с async, про которую вы говорили.

      Удалить
  9. Сергей, тут http://habrahabr.ru/company/pvs-studio/blog/273111 обсуждают CodeContracts. Прокомментируешь?

    ОтветитьУдалить
    Ответы
    1. Ага. Прокомментировал. К сожажалению, вот эта фраза очень четко определяет качество кода Code Contracts:

      It is a medium-sized project (~ 4000 source files), which is actively developing: it contains quite a number of code fragments that are not finished and sometimes incorrectly written. This stage is perfect for implementing a static code analyzer.

      Удалить