Примечание переводчика. На Хабре практически полностью отсутствуют публикации, связанные с языком Ада. А ведь это — живой язык, на котором пишут программы, для которого разрабатываются инструменты статического анализа. Чтобы хоть немного заполнить этот информационный вакуум на Хабре, я решил перевести небольшую заметку, связанную с данным языком. Почему её? В ней упоминается PVS-Studio, и мне это приятно :). Плюс, возможно, российские разработчики на языке Ada узнают о новом для себя инструментарии и увидят, что они совсем не одиноки, и жизнь продолжает кипеть в мире Ада.

В предыдущей заметке мы рассказывали о наших экспериментах по созданию компактных и легких диагностик для исходного кода на языке Ada на основе новой технологии Libadalang. Две описанные там диагностики нашли 12 ошибок в кодовой базе инструментов, разрабатываемых нашей командой в AdaCore. В этой заметке мы расскажем о еще 6 небольших проверках, с помощью которых были обнаружены 114 дефектов. Из этих 6 диагностик 4 нашли ошибки и некачественные фрагменты кода (check_deref_null, check_test_not_null, check_same_test, check_bad_unequal), остальные 2 – возможности для рефакторинга (check_same_then_else, check_useless_assign). Благодаря тому, что прогон каждой диагностики на нашем коде занимает считанные секунды, мы без проблем смогли отладить их до тех пор, пока они не перестали выдавать ложные срабатывания. На данный момент ни одна из этих диагностик не задействует механизм семантического анализа, появившийся недавно в Libadalang, однако, в будущем он позволит улучшить точность анализа. При разработке каждой из проверок мы вдохновлялись похожими компактными диагностиками в других инструментах, в частности, правилами PVS-Studio и его базой ошибок из реальных приложений.

Диагностики разыменований указателей до проверки

Первая реализованная нами диагностика – одна из самых популярных во многих инструментах. Она ищет указатели, которые разыменовываются, а затем проверяются на ноль. Такая ситуация подозрительна, поскольку логично ожидать обратного порядка действий, и указывает либо на ошибку (указатель не должен разыменовываться без предварительной проверки на ноль), либо на проблему некачественного кода (проверка на ноль является лишней). В кодовой базе наших инструментов нашлись обе проблемы. Вот пример ошибки, найденной в компиляторе GNAT в файле g-spipat.adb, где в процедуре Dump разыменовывается указатель P.P в строке 2088:

procedure Dump (P : Pattern) is

  subtype Count is Ada.Text_IO.Count;
  Scol : Count;
  --  Used to keep track of column in dump output

  Refs : Ref_Array (1 .. P.P.Index);
  --  We build a reference array whose N'th element points to the
  --  pattern element whose Index value is N.

а затем, гораздо позже – в строке 2156, проверяется на ноль:

--  If uninitialized pattern, dump line and we are done
if P.P = null then
  Put_Line ("Uninitialized pattern value");
  return;
end if;

Решение проблемы состоит в том, что массив Refs теперь объявляется после того, как точно установлено неравенство указателя P.P нулю. А вот пример некачественного кода, найденный также в компиляторе GNAT в строке 2797 файла g-comlin.adb. Параметр Line сначала объявляется, а затем проверяется на ноль:

  Sections_List : Argument_List_Access :=
                    new Argument_List'(1 .. 1 => null);
  Found         : Boolean;
  Old_Line      : constant Argument_List := Line.all;
  Old_Sections  : constant Argument_List := Sections.all;
  Old_Params    : constant Argument_List := Params.all;
  Index         : Natural;

begin
  if Line = null then
     return;
  end if;

Этот код мы исправили, объявив Line в качестве параметра ненулевого типа доступа. Иногда разыменовывание и проверка происходят в одном и том же выражении, как, например, в следующем фрагменте кода нашего инструмента GNATstack – строка 97 файла dispatching_calls.adb:

if
  Static_Class.Derived.Contains (Explored_Method.Vtable_Entry.Class)
    and then
  Explored_Method /= null
    and then

Код был исправлен таким образом, что проверка на ноль указателя Explored_Method выполняется до его разыменовывания. Всего на данную диагностику пришлось 11 ошибок и 9 фрагментов некачественного кода.

Вторая диагностика в этой категории находит код, в котором за проверкой указателя на ноль следует его же разыменовывание. Как правило, это признак логической ошибки, особенно в сложных булевых выражениях, что показано в примерах из базы ошибок, найденных PVS-Studio. Ошибок этого типа в нашем коде не обнаружено, что может свидетельствовать о высоком качестве тестирования с нашей стороны. Собственно говоря, выполнение подобного кода в языке Ada сразу привело бы к возникновению исключения.

Диагностика проверяемых выражений

Первая диагностика из этой серии ищет проверки идентичных подвыражений в цепочке операторов if-elsif. Такие проверки указывают либо на ошибки, либо на некачественный код. Ниже показан пример ошибки, найденной в компиляторе GNAT в строке 7380 файла sem_ch4.adb:

if Nkind (Right_Opnd (N)) = N_Integer_Literal then
  Remove_Address_Interpretations (Second_Op);

elsif Nkind (Right_Opnd (N)) = N_Integer_Literal then
  Remove_Address_Interpretations (First_Op);
end if;

Правка заключалась в замене Right_Opnd(N) на Left_Opnd(N) во второй проверке. Всего эта диагностика обнаружила 3 ошибки и 7 фрагментов некачественного кода.

Вторая диагностика ищет выражения вида «A /= B or A /= C», где литералы B и C разные. Такие условия всегда верны. Как правило, в них вместо оператора «or» должен использоваться «and». С помощью данной диагностики была найдена одна ошибка в нашем генераторе кода QGen в строке 675 файла himoco-blockdiagramcmg.adb:

if Code_Gen_Mode /= "Function"
  or else Code_Gen_Mode /= "Reusable function"
then
  To_Flatten.Append (Obj);
end if;

Диагностики дублированного кода

Первая диагностика дублированного кода ищет идентичные блоки кода в разных ветвях операторов if и case. Ситуации такого рода указывают на опечатки или логические ошибки, но в нашем случае они выявили только фрагменты, подлежащие рефакторингу. Тем не менее, некоторые из них содержат свыше 20 дублированных строк кода, как в следующем примере – строка 1023 файла be-checks.adb в инструменте CodePeer:

elsif VN_Kind (VN) = Binexpr_VN
  and then Operator (VN) = Logical_And_Op
  and then Int_Sets.Is_In (Big_True, To_Int_Set_Part (Expect))
then
  --  Recurse to propagate check down to operands of "and"
  Do_Check_Sequence
    (Check_Kind,
    Split_Logical_Node (First_Operand (VN)),
    Srcpos,
    File_Name,
    First_Operand (VN),
    Expect,
    Check_Level,
    Callee,
    Callee_VN,
    Callee_Expect,
    Callee_Precondition_Index);
  Do_Check_Sequence
    (Check_Kind,
    Split_Logical_Node (Second_Operand (VN)),
    Srcpos,
    File_Name,
    Second_Operand (VN),
    Expect,
    Check_Level,
    Callee,
    Callee_VN,
    Callee_Expect,
    Callee_Precondition_Index);
...
elsif VN_Kind (VN) = Binexpr_VN
  and then Operator (VN) = Logical_Or_Op
  and then Int_Sets.Is_In (Big_False, To_Int_Set_Part (Expect))
then
  --  Recurse to propagate check down to operands of "and"
  Do_Check_Sequence
    (Check_Kind,
    Split_Logical_Node (First_Operand (VN)),
    Srcpos,
    File_Name,
    First_Operand (VN),
    Expect,
    Check_Level,
    Callee,
    Callee_VN,
    Callee_Expect,
    Callee_Precondition_Index);
  Do_Check_Sequence
    (Check_Kind,
    Split_Logical_Node (Second_Operand (VN)),
    Srcpos,
    File_Name,
    Second_Operand (VN),
    Expect,
    Check_Level,
    Callee,
    Callee_VN,
    Callee_Expect,
    Callee_Precondition_Index);

или в строке 545 файла soap-generator-skel.adb в инструменте GPRbuild:

when WSDL.Types.K_Derived =>
  if Output.Next = null then
    Text_IO.Put
      (Skel_Adb,
      WSDL.Parameters.To_SOAP
        (N.all,
        Object    => "Result",
        Name      => To_String (N.Name),
        Type_Name => T_Name));
  else
    Text_IO.Put
      (Skel_Adb,
      WSDL.Parameters.To_SOAP
        (N.all,
        Object    =>
          "Result."
            & Format_Name (O, To_String (N.Name)),
        Name      => To_String (N.Name),
        Type_Name => T_Name));
  end if;

when WSDL.Types.K_Enumeration =>

  if Output.Next = null then
    Text_IO.Put
      (Skel_Adb,
      WSDL.Parameters.To_SOAP
        (N.all,
        Object    => "Result",
        Name      => To_String (N.Name),
        Type_Name => T_Name));
  else
    Text_IO.Put
      (Skel_Adb,
      WSDL.Parameters.To_SOAP
        (N.all,
        Object    =>
          "Result."
            & Format_Name (O, To_String (N.Name)),
        Name      => To_String (N.Name),
        Type_Name => T_Name));
  end if;

Всего эта диагностика выявила 62 фрагмента некачественного кода в нашей базе.

Вторая диагностика этого типа ищет бессмысленные присваивания значений локальным переменным, после которых эти значения ни разу не используются. Такие ошибки могут быть и явными, как, например, здесь (строка 1067 файла be-value_numbers-factory.adb в инструменте CodePeer):

Global_Obj.Obj_Id_Number    := Obj_Id_Number (New_Obj_Id);
Global_Obj.Obj_Id_Number    := Obj_Id_Number (New_Obj_Id);

и скрытыми, как в примере ниже (строка 895 файла bt-xml-reader.adb в том же инструменте CodePeer):

if Next_Info.Sloc.Column = Msg_Loc.Column then
  Info := Next_Info;
  Elem := Next_Cursor;
end if;
Elem := Next_Cursor;

Всего эта диагностика обнаружила 9 фрагментов некачественного кода.

Инструкция по установке

Хотите опробовать описанные выше скрипты на своей кодовой базе? Это можно сделать уже сейчас с помощью последней версии GNAT Pro или версии GPL для пользователей сообщества и держателей академической лицензии! Следуя инструкции, размещенной в репозитории Libadalang, вы сможете запустить скрипты внутри вашего интерпретатора для Python2.

Заключение

В общей сложности реализованные на данный момент 8 диагностик (часть из них описана в этой заметке, часть – в предыдущей) позволили нам обнаружить и исправить 24 ошибки и 102 фрагмента некачественного кода в нашей кодовой базе. Такие результаты однозначно говорят в пользу того, что подобные диагностики следует включать в статические анализаторы, и мы надеемся, что вскоре сможем реализовать все эти и многие другие проверки в нашем статическом анализаторе CodePeer для программ на Ada.

Примечательно также то, что благодаря мощному API для Python, реализованному в Libadalang, на создание каждой из этих диагностик ушло не более пары часов. Хотя нам пришлось написать шаблонный код для обхода AST в различных направлениях, а также многочисленные заплатки для компенсации отсутствия семантического анализа в последней доступной на тот момент версии Libadalang, все это заняло сравнительно немного времени, и эти наработки мы затем сможем применить в остальных подобных диагностиках. Теперь мы с нетерпением ожидаем выпуска версии Libadalang, в которой появится опция семантического анализа и которая позволит нам разрабатывать еще более мощные и полезные проверки.

[автор фото – Кортни Лемон]

О Яннике Мое

Янник Мой – старший инженер-разработчик компании AdaCore и соуправляющий совместной лабораторией ProofInUse. В AdaCore он разрабатывает статические анализаторы кода CodePeer и SPARK, предназначенные для выявления ошибок и оценки безопасности и защищенности кода. Янник является ведущим разработчиком продукта SPARK 2014, о котором он регулярно рассказывает в своих статьях, на конференциях, на занятиях в вузах и в блогах (в частности, на сайте www.spark-2014.org). До этого Янник разрабатывал анализаторы кода в компании PolySpace (ныне The MathWorks) и Университете Париж-юг.