Проверяем Microsoft Code Contracts



    Мы успешно создали и продолжаем развивать анализатор PVS-Studio для языка C/C++. Со временем стало понятно, что многие из реализованных диагностик никак не связаны с конкретным языком программирования, и тогда мы решили попробовать применить свой опыт к другому языку программирования, к C#. В данной статье будет рассказано о проверке проекта Code Contracts от Microsoft с помощью нового C# анализатора.

    О проекте MS Code Contracts


    Code Contracts предоставляют метод, с помощью которого выражаются предположения о коде программы в .NET приложениях. Контракты принимают форму предусловий, постусловий и инвариантов объекта, и выступают в роли проверенной документации ваших внешних и внутренних API. Контракты используются для того, чтобы улучшить процесс тестирования с помощью проверки во время выполнения программы, позволяя проводить статическую верификацию контрактов и генерацию документации.

    Это проект среднего размера (около ~4000 исходных файлов), который активно развивается: содержит много недописанного и некорректно написанного кода. Именно на этом этапе необходимо внедрять статический анализ в процесс разработки.

    О новом анализаторе C# кода


    Проект Code Contracts проверен с помощью экспериментальной версии PVS-Studio, которая доступна по этой ссылке: http://files.viva64.com/beta/PVS-Studio_setup.exe.

    Анализатор в скором времени перестанет быть экспериментальным. Мы планируем выпустить первую релизную версию PVS-Studio с поддержкой С# уже 22.12.2015. При этом анализатор меняет старший номер версии на 6.0.

    Ценовая политика не претерпит никаких изменений. Раньше PVS-Studio позволял проверять программы на языках C, C++, C++/CLI, C++/CX. Теперь к этому списку просто добавляется C#.

    Результаты проверки


    Подготавливая статью о проверке открытого проекта, мы приводим в ней информацию далеко не о всех предупреждениях, которые выдаёт статический анализатор. Поэтому мы рекомендуем авторам проекта самостоятельно выполнить анализ проекта и изучить все выдаваемые анализатором сообщения.

    Наиболее опасные найденные места


    V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 3. Present: 2. VSServiceProvider.cs 515
    void AskToReportError(Exception exn) {
      ....
      var emailBody = new StringBuilder();
      emailBody.AppendLine("Hi Code Contracts user,");
      emailBody.AppendLine();
      ....
      emailBody.AppendLine(
        String.Format(".... {0} {1} Visual Studio {2} Bug Report",
          typeof(VSServiceProvider).Assembly.GetName().Version,
    #if DEBUG
                                                     "Debug"
    #else
                                                     "Release"
    #endif
                                               ));
      ....
    }

    Функция String.Format() ожидает 3 аргумента, а передано всего 2 аргумента. В этом случае возникает FormatException.

    V3014 It is likely that a wrong variable is being incremented inside the 'for' operator. Consider reviewing 'i'. SparseArray.cs 1956
    override public string ToString()
    {
      StringBuilder str = new StringBuilder();
    
      for (int i = 0; i < data.Length; i++)
      {
        if (data[i] != null)
        {
          for (int j = 0; j < lastElement[i]; i++)  //<==
          {
            str.AppendFormat("({0},{1})", data[i][j].Index,
                                          data[i][j].Value);
          }
        }
      }
    
      return str.ToString();
    }

    Во вложенном цикле не изменяется переменная-счётчик 'j', т.к. вместо 'j++' выполняется изменение счётчика внешнего цикла 'i++'.

    Ещё несколько подобных мест:
    • V3014 It is likely that a wrong variable is being incremented inside the 'for' operator. Consider reviewing 'k'. Writer.cs 3984
    • V3014 It is likely that a wrong variable is being incremented inside the 'for' operator. Consider reviewing 'count_d'. Octagons.cs 509

    V3003 The use of 'if (A) {...} else if (A) {...}' pattern was detected. There is a probability of logical error presence. Check lines: 203, 207. WeakestPreconditionProver.csToSMT2.cs 203
    private BoxedExpression DeclareVariable(....)
    {
      var tmp = original.ToString().Replace(' ', '_');
      this.Info.AddDeclaration(string.Format("....", tmp, type));
      this.ResultValue = tmp;
    
      if (type == FLOAT32)       //<==
      {
        types[original] = FloatType.Float32;
      }
      else if (type == FLOAT64)  //<==
      {
        types[original] = FloatType.Float64;
      }
    
      return original;
    }

    Анализатор обнаружил два одинаковых условных выражения, из-за чего операторы во втором условии никогда не получат управления. Хотя, на первый взгляд, это не так, мы перейдём к определению констант FLOAT32 и FLOAT64, и увидим следующий код:
    private const string FLOAT32 = "(_ FP 11 53)"; // To change!!!
    private const string FLOAT64 = "(_ FP 11 53)";

    Константы действительно равны! Хотя здесь и есть комментарий, что необходимо произвести замену значения константы FLOAT32, это место легко пропустить в будущем. В развивающихся проектах важно помечать такие места как TODO и регулярно просматривать результаты статического анализа кода.

    V3003 The use of 'if (A) {...} else if (A) {...}' pattern was detected. There is a probability of logical error presence. Check lines: 1200, 1210. OutputPrettyCS.cs 1200
    public enum TypeConstraint
    {
      NONE,
      CLASS,     //<==
      STRUCT,    //<==
      BASECLASS,
    }
    
    public void Output(OutputHelper oh)
    {
      Contract.Requires(oh != null);
    
      oh.Output("where ", false);
      mParent.OutputName(oh);
      oh.Output(" : ", false);
      //** base class
      bool comma = false;
      if (mTypeConstraint == TypeConstraint.CLASS)       //<==???
      {
        oh.Output("class", false);
        comma = true;
      }
      else if (mTypeConstraint == TypeConstraint.STRUCT)
      {
        oh.Output("struct", false);
        comma = true;
      }
      else if (mTypeConstraint == TypeConstraint.CLASS)  //<==???
      {
        oh.Output(mClassConstraint, false);
        comma = true;
      }
    }

    В этом фрагменте кода одинаковые условия более очевидны. Скорее всего, в одном из условий переменную 'mTypeConstraint' хотели сравнить с константой TypeConstraint.BASECLASS, вместо TypeConstraint.CLASS.

    V3022 Expression 'c > '\xFFFF'' is always false. Output.cs 685
    private static string Encode(string s)
    {
      ....
      foreach( char c in s ) {
        if (c == splitC || c == '\n' || c == '\\') {
          specialCount++;
        }
        else if (c > '\x7F') {
          if (c > '\xFFFF') specialCount += 9;
          else specialCount += 5;
        }
      }
      ....
    }

    Выражение «c > '\xFFFF'» никогда не будет истинным и оператор «specialCount += 9» никогда не выполнится. Переменная 'c' имеет тип Char, максимальное значение которого и есть "\xFFFF'. Не очень понятно, как должен работать этот код и как его надо исправить. Возможно мы имеем дело с опечаткой или фрагментом кода, позаимствованным из приложения на другом языке. Например, в языке Си/Си++ иногда используются символы разрядностью 32-бита. И там как раз «играют» со значением 0xFFFF. Пример подобного кода:
    /* putUTF8 -- write a character to stdout in UTF8 encoding */
    static void putUTF8(long c)
    {
      if (c <= 0x7F) {         /* Leave ASCII encoded */
        printf("&#%ld;", c);
      } else if (c <= 0x07FF) {     /* 110xxxxx 10xxxxxx */
        putchar(0xC0 | (c >> 6));
        putchar(0x80 | (c & 0x3F));
      } else if (c <= 0xFFFF) {     /* 1110xxxx + 2 */
        putchar(0xE0 | (c >> 12));
        putchar(0x80 | ((c >> 6) & 0x3F));
        putchar(0x80 | (c & 0x3F));
      } else if (c <= 0x1FFFFF) {    /* 11110xxx + 3 */
        putchar(0xF0 | (c >> 18));
        putchar(0x80 | ((c >> 12) & 0x3F));
        putchar(0x80 | ((c >> 6) & 0x3F));
        putchar(0x80 | (c & 0x3F));
      } else if (c <= 0x3FFFFFF) {    /* 111110xx + 4 */
        putchar(0xF8 | (c >> 24));
        putchar(0x80 | ((c >> 18) & 0x3F));
        putchar(0x80 | ((c >> 12) & 0x3F));
        putchar(0x80 | ((c >> 6) & 0x3F));
        putchar(0x80 | (c & 0x3F));
      } else if (c <= 0x7FFFFFFF) {    /* 1111110x + 5 */
        putchar(0xFC | (c >> 30));
        putchar(0x80 | ((c >> 24) & 0x3F));
        putchar(0x80 | ((c >> 18) & 0x3F));
        putchar(0x80 | ((c >> 12) & 0x3F));
        putchar(0x80 | ((c >> 6) & 0x3F));
        putchar(0x80 | (c & 0x3F));
      } else {          /* Not a valid character... */
        printf("&#%ld;", c);
      } 
    }

    V3008 The 'this.InsideMonitor' variable is assigned values twice successively. Perhaps this is a mistake. Check lines: 751, 749. AssertionCrawlerAnalysis.cs 751
    private Data(Data state, Variable v)
    {
      this.IsReached = state.IsReached;
      this.InsideMonitor = state.InsideMonitor;  //<==
      this.symbols = new List<Variable>(state.symbols) { v };
      this.InsideMonitor = false;                //<==???
    }

    Очень подозрительно, что некая функция изменяет состояние объекта с помощью значений, переданных через параметры функции и в последним момент перезаписывает значение поля «this.InsideMonitor» константой 'false'. Ранее уже было выполнено присваивание «this.InsideMonitor = state.InsideMonitor».

    V3009 It's odd that this method always returns one and the same value of 'true'. LinearEqualities.cs 5262
    public bool TryGetFirstAvailableDimension(out int dim)
    {
      for (var i = 0; i < map.Length; i++)
      {
        if (!map[i])
        {
          dim = i;
          return true;
        }
      }
    
      map.Length++;
    
      dim = map.Length;
    
      return true;
    }

    Анализатор обнаружил функцию, которая всегда возвращает одно значение «true». Можно предположить, что при выполнении условия "!map[i]" функция должна вернуть одно значение, а если условие ни разу не было истинным, то вернуть другое значение. Возможно, здесь ошибка.

    Остальные предупреждения


    V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 1. Present: 2. Output.cs 68
    public override void WriteLine(string value)
    {
      output.WriteLine(string.Format("{1}", DateTime.Now,
        value.Replace("{", "{{").Replace("}","}}")));
      //output.WriteLine(string.Format("[{0}] {1}",
        //DateTime.Now., value));
    }

    Раньше функция String.Format() принимала и печатала 2 значения: дату и некоторое значение. Потом этот код закомментировали и написали другой вариант, в котором аргумент с индексом 0 не используется, т.е. дата теперь не печатается.

    Другие примеры вызова функций форматирования с неиспользованными аргументами:
    • V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 6. Present: 7. CacheModelExtensions.cs 46
    • V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 1. Present: 2. CodeFixesInference.cs 1608
    • V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 2. Present: 3. ExpressionManipulation.cs 442

    V3004 The 'then' statement is equivalent to the 'else' statement. Metadata.cs 2602
    private void SerializeFieldRvaTable(....)
    {
      ....
      switch (row.TargetSection){
        case PESection.SData:
        case PESection.TLS:
          Fixup fixup = new Fixup();
          fixup.fixupLocation = writer.BaseStream.Position;
          fixup.addressOfNextInstruction = row.RVA;
          if (row.TargetSection == PESection.SData){
            sdataFixup.nextFixUp = fixup;   //<==
            sdataFixup = fixup;             //<==
          }else{
            sdataFixup.nextFixUp = fixup;   //<==
            sdataFixup = fixup;             //<==
          }
          writer.Write((int)0);
          break;
      ....
    }

    Анализатор обнаружил идентичные блоки кода в условном операторе. Это может быть лишним кодом или один блок кода забыли изменить после копирования. Copy-Paste не щадит и C# программистов.

    Весь список подобных мест:
    • V3004 The 'then' statement is equivalent to the 'else' statement. Nodes.cs 6698
    • V3004 The 'then' statement is equivalent to the 'else' statement. Nodes.cs 6713
    • V3004 The 'then' statement is equivalent to the 'else' statement. WarningSuggestionLinkOutput.cs 108
    • V3004 The 'then' statement is equivalent to the 'else' statement. NonNullAnalyzer.cs 1753

    V3001 There are identical sub-expressions 'semanticType.Name == null' to the left and to the right of the '||' operator. ContractsProvider.cs 694
    public bool TryGetTypeReference(....)
    {
      ....
      if (semanticType.Name == null || semanticType.Name == null)
        goto ReturnFalse;
      cciType = new Microsoft.Cci.MutableCodeModel.NamespaceTypeR....
      {
        ContainingUnitNamespace = cciNamespace,
        GenericParameterCount = (ushort) (....),
        InternFactory = Host.InternFactory,
        IsValueType = semanticType.IsValueType,
        IsEnum = semanticType.TypeKind == TypeKind.Enum,
        Name = Host.NameTable.GetNameFor(semanticType.Name),
        TypeCode=CSharpToCCIHelper.GetPrimitiveTypeCode(semanticType)
      };
      goto ReturnTrue;'
      ....
    }

    Условие «semanticType.Name == null» проверяют 2 раза. Либо проверка избыточна и её можно упростить, либо забыли проверить другое поле у объекта.

    Ещё одно предупреждение на эту тему:
    • V3001 There are identical sub-expressions 'semanticType.Name == null' to the left and to the right of the '||' operator. ContractsProvider.cs 714

    V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'other', 'right'. CallerInvariant.cs 189
    public override Predicate JoinWith(Predicate other)
    {
      var right = other as PredicateNullness;
      if (other != null)
      {
        if (this.value == right.value)
        {
          return this;
        }
      }
    
      return PredicateTop.Value;
    }

    Анализатор обнаружил потенциальную ошибку, которая может привести к доступу по нулевой ссылке. Необходимо сравнивать с 'null' результат выполнения оператора 'as'.

    Если возникнет ситуация, когда объект 'other' не будет нулевым, но его не удастся привести к типу 'PredicateNullness', то возникнет доступ по нулевой ссылке при обращении к «right.value».

    Таких сравнений в проекте найдено много, вот весь список:
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'facts', 'moreRefinedFacts'. SimplePostconditionDispatcher.cs 319
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'objProvenance', 'provenance'. AssertionCrawlerAnalysis.cs 816
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'prev', 'other'. NonRelationalValueAbstraction.cs 1063
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'prev', 'castedPrev'. GenericDomains.cs 1657
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'right'. LinearEqualitiesForSubpolyhedra.cs 859
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'other'. NonRelationalValueAbstraction.cs 1047
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'other'. NonRelationalValueAbstraction.cs 1055
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'right'. LinearEqualities.cs 849
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'right'. LinearEqualities.cs 973
    • V3019 Possibly an incorrect variable is compared to null after type conversion using 'as' keyword. Check variables 'a', 'right'. LinearEqualities.cs 1119

    V3030 Recurring check. The 'this.lineOffsets == null' condition was already verified in line 612. Nodes.cs 613
    public virtual void InsertOrDeleteLines(....)
    {
      ....
      if (this.lineOffsets == null)
        if (this.lineOffsets == null) this.ComputeLineOffsets();
      if (lineCount < 0)
        this.DeleteLines(offset, -lineCount);
      else
        this.InsertLines(offset, lineCount);
      ....
    }

    Идущие подряд две одинаковые проверки «this.lineOffsets == null». Такой код не имеет смысла. Возможно, хотели проверить что-то ещё.

    V3002 The switch statement does not cover all values of the 'UnaryOperator' enum: Conv_dec. WeakestPreconditionProver.csToSMT2.cs 453
    private string Combine(UnaryOperator unaryOperator, string arg)
    {
      Contract.Requires(arg != null);
    
      var format = "({0} {1})";
      string op = null;
    
      switch (unaryOperator)
      {
        case UnaryOperator.Neg:
        case UnaryOperator.Not:
        case UnaryOperator.Not:
          {
            op = "not";
          }
          break;
    
        case UnaryOperator.WritableBytes:
        case UnaryOperator.Conv_i:
        case UnaryOperator.Conv_i1:
        case UnaryOperator.Conv_i2:
        case UnaryOperator.Conv_i4:
        case UnaryOperator.Conv_i8:
        case UnaryOperator.Conv_r_un:
        case UnaryOperator.Conv_r4:
        case UnaryOperator.Conv_r8:
        case UnaryOperator.Conv_u:
        case UnaryOperator.Conv_u1:
        case UnaryOperator.Conv_u2:
        case UnaryOperator.Conv_u4:
        case UnaryOperator.Conv_u8:
          {
            return null;
         }
      }
    
      return string.Format(format, op, arg);
    }

    Анализатор обнаружил оператор 'switch', в котором выбор варианта осуществляется по переменной enum-типа. При этом в операторе 'switch' пропущен 1 элемент «UnaryOperator. Conv_dec». Это очень подозрительно.

    Ниже приведено определение перечисления «UnaryOperator»:
    public enum UnaryOperator
    {
      ....
      Conv_u8,
      Conv_r_un,
      Neg,
      Not,
      WritableBytes,
      Conv_dec,      //<==
    }

    Возможная ошибка заключается в том, что данная функция реализована таким образом, чтобы для значения «UnaryOperator.Not» возвращать форматированную строку, а в остальных случаях значение 'null'. Но так как элемент «UnaryOperator. Conv_dec» пропущен, то для него значение переменной 'op' останется равно 'null' и оно попадёт в форматированную строку, которую вернёт функция.

    Заключение


    Надеемся вам понравилась эта статья. Обещаем и дальше радовать наших читателей проверками интересных открытых проектов.

    Как уже упоминалось выше, первый релиз намечен на 22.12.2015. Как правило в конце года принимаются решения о будущих закупках. Поэтому, всем заинтересовавшимся, предлагаем, не откладывая уже сейчас связаться с нами по вопросам приобретения PVS-Studio. И мы будем рады видеть вашу компанию среди наших довольных клиентов.

    Спасибо за внимание. И безбажного вам кода!


    Если хотите поделиться этой статьей с англоязычной аудиторией, то прошу использовать ссылку на перевод: Svyatoslav Razmyslov. Analysis of Microsoft Code Contracts.

    Прочитали статью и есть вопрос?
    Часто к нашим статьям задают одни и те же вопросы. Ответы на них мы собрали здесь: Ответы на вопросы читателей статей про PVS-Studio, версия 2015. Пожалуйста, ознакомьтесь со списком.
    PVS-Studio
    Статический анализ кода для C, C++, C# и Java

    Комментарии 11

      +5
      Призываю SergeyT!
        +10
        Ну, как вам сказать:), что можно ожидать от кода, entry point которого называется MikesArchitecture? Комьюнити в последнее время пытается причесать этого монстра, но поддается он с трудом.

        Так что у меня есть фичареквест для любого анализатора: если он встречает метод с именем _Some_Authors_Name_Architecture, то прекращает анализ с сообщением, что он сдается и дальше не готов анализировать код дабы не повредить свою психику:)
        0
        Ошибка с InsideMonitor может быть и не ошибкой, если InsideMonitor — свойство, на сеттер которого может быть повешена хитрая логика, влияющая на инициализацию symbols (хотя с виду symbols обычное поле).
          +2
          public struct Data
          {
            public readonly bool IsReached;
            private readonly List<Variable> symbols;
            public bool InsideMonitor /* = false*/;
          ....
          

          Пока исходники под рукой, нашёл полный код, это просто поля, даже есть коммент, но код всё равно подозрительный.

          Если каким-то диагностикам приходится работать со свойствами, то мы пытаемся определить их сложность и не выдавать предупреждения.
          +1
          Реквестирую проверку CoreCrl.
          0
          Edit: фигню сморозил.
            0
            С типом char в Java много раз встречал проверки вроде if(char > 0xFFFF) или что-то вроде if(char < 0x1FFFF). Люди иногда забывают, что char — это UTF-16 code unit, а вовсе не code point, и чтобы нормально анализировать UTF-16 строку, надо учитывать суррогатные пары.
              +1
              Всем, кому интересна эта тема. Мы выпустили релизную версию PVS-Studio 6.00 с поддержкой C#. Приглашаю скачать и попробовать: www.viva64.com/ru/pvs-studio-download

              Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

              Самое читаемое