More Simple Bugs [Hell Language] / PVS-Studio Blog

Note by the translator. On Habré there are almost completely no publications related to the language of Hell. But this is a living language in which programs are written, for which static analysis tools are developed. In order to at least slightly fill this informational vacuum on Habré, I decided to translate a small note related to this language. Why her? PVS-Studio is mentioned in it, and I am pleased :). Plus, perhaps, Russian developers in the Ada language will learn about new tools for themselves and see that they are not alone at all, and life continues to boil in the world of Ada.

In the previous notewe talked about our experiments in creating compact and easy diagnostics for Ada source code based on the new Libadalang technology. The two diagnostics described there found 12 errors in the code base of the tools developed by our team in AdaCore. In this note, we will talk about 6 more small checks with which 114 defects were detected. Out of these 6 diagnostics, 4 found errors and low-quality code fragments (check_deref_null, check_test_not_null, check_same_test, check_bad_unequal), the other 2 - refactoring options (check_same_then_else, check_useless_assign). Due to the fact that the run of each diagnostics on our code takes a matter of seconds, we were able to debug them without problems until they stopped issuing false positives. At the moment, none of these diagnostics uses the mechanism of semantic analysis, which appeared recently in Libadalang, however, in the future it will improve the accuracy of the analysis. When developing each of the tests, we were inspired by similar compact diagnostics in other tools, in particular, the PVS-Studio rules andits error base from real applications .

Pointer dereferencing diagnostics before validation

The first diagnostics we have implemented is one of the most popular in many tools. She searches for pointers that are dereferenced and then checked for zero. This situation is suspicious, since it is logical to expect the reverse order of actions, and indicates either an error (the pointer should not be dereferenced without first checking for zero) or a problem with poor-quality code (checking for zero is superfluous). The code base of our tools found both problems. Here is an example of an error found in the GNAT compiler in the g-spipat.adb file, where in the Dump procedure the PP pointer is dereferenced at line 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.

and then, much later, on line 2156, it is checked for zero:

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

The solution to the problem is that the Refs array is now declared after the PP pointer inequality is exactly set to zero. And here is an example of poor-quality code, also found in the GNAT compiler on line 2797 of the g-comlin.adb file. The Line parameter is first declared and then checked for zero:

  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;

We fixed this code by declaring Line as a parameter of a nonzero access type. Sometimes dereferencing and verification occur in the same expression, as, for example, in the following code snippet of our GNATstack tool - line 97 of the dispatching_calls.adb file:

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

The code has been fixed in such a way that the Explored_Method pointer is checked for zero before it is dereferenced. In total, this error accounted for 11 errors and 9 fragments of poor-quality code.

The second diagnostics in this category finds a code in which the dereferencing of a pointer to zero follows its dereferencing. As a rule, this is a sign of a logical error, especially in complex Boolean expressions, which is shown in the examples from the error database found by PVS-Studio . No errors of this type were found in our code, which may indicate a high quality of testing on our part. As a matter of fact, the execution of such code in Ada would immediately lead to an exception.

Diagnostics of checked expressions

The first diagnostics in this series looks for checks of identical subexpressions in the if-elsif statement chain . Such checks indicate either errors or low-quality code. The following is an example of an error found in the GNAT compiler on line 7380 of the sem_ch4.adb file:

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;

The edit was to replace Right_Opnd (N) with Left_Opnd (N) in the second check. In total, this diagnostic detected 3 errors and 7 fragments of poor-quality code.

The second diagnostics looks for expressions of the form “A / = B or A / = C”, where the literals B and C are different. Such conditions are always true. As a rule, they should use “and” instead of the “or” operator. Using this diagnostic, one error was found in our QGen code generator in line 675 of himoco-blockdiagramcmg.adb:

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

Duplicate Code Diagnostics

The first diagnosis of duplicate code looks for identical blocks of code in different branches of the if and case statements . Situations of this kind indicate typos or logical errors, but in our case they revealed only fragments to be refactored. However, some of them contain over 20 duplicate lines of code, as in the following example, line 1023 of the be-checks.adb file in the CodePeer tool:

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);

or on line 545 of the soap-generator-skel.adb file in the GPRbuild tool:

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;

In total, this diagnosis revealed 62 fragments of poor-quality code in our database.

The second diagnosis of this type is looking for meaningless assignments of values ​​to local variables, after which these values ​​are never used. Such errors can also be obvious, such as here (line 1067 of the be-value_numbers-factory.adb file in the CodePeer tool):

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

and hidden, as in the example below (line 895 of the bt-xml-reader.adb file in the same CodePeer tool):

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

In total, this diagnosis revealed 9 fragments of poor-quality code.

Installation Instructions

Want to try out the scripts described above on your code base? This can be done now with the latest version of GNAT Pro or the GPL version for community users and academic license holders! Following the instructions posted in the Libadalang repository , you can run scripts inside your interpreter for Python2.

Conclusion

In total, 8 diagnostics implemented at the moment (some of them are described in this note, some in the previous one ) allowed us to detect and fix 24 errors and 102 fragments of poor-quality code in our code base. Such results clearly support the fact that such diagnostics should be included in static analyzers, and we hope that soon we will be able to implement all these and many other checks in our static CodePeer analyzer for Ada programs.

It is also noteworthy that thanks to the powerful Python API implemented in Libadalang, it took no more than a couple of hours to create each of these diagnostics. Although we had to write template code to bypass AST in various directions, as well as numerous patches to compensate for the lack of semantic analysis in the latest version of Libadalang available at that time, all this took relatively little time, and we can then apply these developments to other similar diagnostics. Now we are looking forward to the release of the Libadalang version, which will have the option of semantic analysis and which will allow us to develop even more powerful and useful checks.

[author photo - Courtney Lemon ]

About My Yannick

Yannick Moy is a senior development engineer at AdaCore and co-managing the ProofInUse joint lab. At AdaCore, he is developing static code analyzers CodePeer and SPARK, designed to detect errors and assess the security and security of the code. Yannik is a leading developer of the SPARK 2014 product, which he regularly talks about in his articles, at conferences, in university classes and in blogs (in particular, on the site www.spark-2014.org ). Prior to this, Yannick developed code analyzers at PolySpace (now The MathWorks) and the University of Paris-South.