Gem #124 : Scripting GPS for Static Analysis

by Yannick MoyNicolas Setton —AdaCoreAdaCore

Let's get started...

Being able to quickly query a code base for some simple properties is a valuable capability both during development and debugging. Most of the time one can get by with coarse grep-like queries, or maybe a simple script based on syntactic queries. For more complex queries that require semantic knowledge, one must resort to using existing tools, which might not always be a perfect fit.

This Gem provides a way to perform these queries using the Python scripting capabilities of GPS, the GNAT Programming Studio IDE.

As an example, consider a critical section whose API defines the procedures Enter and Leave:

package Critical_Section is

    procedure Enter;
    --  Enter the critical section

    procedure Leave;
    --  Leave the critical section.
    --  Important: every procedure calling Enter should also call Leave.

end Critical_Section;

For purposes of illustration, their implementation can be as simple as:

package body Critical_Section is

    In_Critical : Boolean := False;

    procedure Enter is
    begin
       In_Critical := True;
    end Enter;

    procedure Leave is
    begin
       In_Critical := False;
    end Leave;

end Critical_Section;

These critical sections may be used in a main program, in ways that are more or less correct:

with Critical_Section; use Critical_Section;

procedure Main is

   procedure A is
   begin
      Enter; -- Do some processing Leave;
   end A;

   procedure B is
   begin
      Enter; -- Do some processing
   end B;

begin
   A;
   B;
end Main;

Ideally, we would like every subprogram that enters the critical section to also leave it. This requires knowledge of the call graph of the application, not something that a grep-like approach can solve, and you would be unlikely to have a tool that already computes this information for you.

Well, this is very easy to do in GPS!

Open GPS on the project and compile the code with GNAT. This generates cross-reference information, saved in the .ali files, containing in particular references to all entities in the code. The Python API in GPS allows one to query this information, know where each entity is referenced, determine an entity's kind, etc.

Open a Python shell with Window->Python, and enter the following lines in the shell (except comments introduced by #):

# get the entities corresponding to the functions
enter_entity = GPS.Entity("Enter", GPS.File("critical_section.ads"))
leave_entity = GPS.Entity("Leave", GPS.File("critical_section.ads"))

# get the list of calls for each function

enter_called_by = enter_entity.called_by()
leave_called_by = leave_entity.called_by()

# print the result
print ["Enter is called by %s, which does not call Leave" % fun for fun in enter_called_by if not fun in leave_called_by]

This should print the following result:

['Enter is called by B:main.adb:12:14, which does not call Leave']

That's the information we were looking for!

Now, you may find this kind of query common enough that you would like to have a simple button to press in GPS to compute this result. The plug-in capabilities of GPS allow you to register the code above, so that the user will be prompted for the two subprograms Enter and Leave. The plug-in itself is simply:

""" Given the names of two subprograms Enter and Leave defining a critical
     section, this plug-in detects subprograms which only enter the critical
     section without leaving it.
"""

import GPS

def detect_critical_section_violation(self):
     enter_name, enter_file, leave_name, leave_file= 
GPS.MDI.input_dialog("Enter the names of subprograms defining the critical section:", "Enter", "File containing Enter", "Leave", "File containing Leave")

     # get the entities corresponding to the functions
     enter_entity = GPS.Entity(enter_name, GPS.File(enter_file))
     leave_entity = GPS.Entity(leave_name, GPS.File(leave_file))

     # get the list of calls for each function

     enter_called_by = enter_entity.called_by()
     leave_called_by = leave_entity.called_by()

     # compute the violations
     violations = [fun for fun in enter_called_by if not fun in leave_called_by]
     if violations == []:
         GPS.MDI.dialog ("No violation found")
     else:
         GPS.MDI.dialog(str(["Enter is called by %s, which does not call Leave" % fun for fun in violations]))

def on_gps_started (hook_name):
     menu = GPS.Menu.create("/Tools/Browsers/Detect critical section violation", detect_critical_section_violation)

GPS.Hook ("gps_started").add (on_gps_started)

Put this code in a file critical_section.py under either one of INSTALL/share/gps/plug-ins or HOME/.gps/plug-ins and the menu will be there the next time you open GPS.

For more information on how to use the Python API in GPS, we refer you to section 16 of the GPS User's Guide (Customizing and Extending GPS) and the Python API reachable under Help->Python extensions in GPS.


About the Author

Yannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined INRIA Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research.

Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.