Gem #121 Breakpoint Commands — Part 1

by Jerome Guitton —AdaCore

Let's get started...

Consider this basic model of a Bank:

package Bank is
   procedure Open_Account (Cash : Integer);
   procedure Deposit (Cash : Integer);
   procedure Withdraw (Cash : Integer);
end Bank;

This bank maintains only one account that has to be open before doing any transation. The only client of this bank would be a main subprogram P that opens an account and operates several transactions:

with Bank;
procedure P is
begin
   Bank.Open_Account (100);
   Bank.Deposit (45);
   Bank.Withdraw (55);
   Bank.Deposit (80);
end P;

The implementation of package Bank is straightforward; it also contains an additional transaction at elaboration time, that corresponds to a special offer of the bank (and one may already see that it will cause a problem):

package body Bank is
   Balance : Integer;
   procedure Open_Account (Cash : Integer) is
   begin
      Balance := Cash;
   end Open_Account;
   procedure Deposit (Cash : Integer) is
   begin
      Balance := Balance + Cash;
   end Deposit;
   procedure Withdraw (Cash : Integer) is
   begin
      Balance := Balance - Cash;
   end Withdraw;
   -- To celebrate the inauguration of the bank at elaboration time, your
   -- account is credited with $100.
   Special_Offer : constant Integer := 100;
begin
   Deposit (Special_Offer);
end Bank;

There is a implicit property that the account should be opened only once, and before any transaction takes place; would this special offer break this property? This is a good opportunity to see how GDB can help us in checking properties of this form and break whenever the property is violated at run time. To do so, one may use the script language of GDB along with breakpoint commands.

The first way to do so would be set breakpoints on the bank operations:

(gdb) break open_account
Breakpoint 1 at 0x401592: file bank.adb, line 7.
(gdb) break deposit
Breakpoint 2 at 0x4015a2: file bank.adb, line 12.
(gdb) break withdraw
Breakpoint 3 at 0x4015b8: file bank.adb, line 17.

However, we would not like to stop on any transaction, but only on an invalid one. At each breakpoint, we would like to check if our invariants hold, continue if they do, stop with an error if they don't.

First, the properties that we want to check require to maintain a state: whether or not the account has been open. This may be represented by a GDB convenience variable that can be created as follows:

set variable $account_open := False

We can then attach a small program that will be executed each time the breakpoint is hit. e.g. for breakpoint 1 on open_account:

(gdb) commands 1
>if $account_open = True
 >echo error: account opened twice
 >else
 >set variable $account_open := True
 >printf "(info) account created with $%d
", cash
 >continue
 >end
>end

This command will resume the program if the account has not been opened yet, and will stop with an error message if we are trying to open it for the second time. The same kind of program may be used for withdraw and deposit:

(gdb) commands 2
>if $account_open = False
 >echo error: someone tries to deposit before opening an account
 >else
 >printf "(info) deposit: $%d
", cash
 >continue
 >end
>end
(gdb) commands 3
>if $account_open = False
 >echo error: someone tries to withdraw before opening an account
 >else
 >printf "(info) withdrawal: $%d
", cash
 >continue
 >end
>end

Now let us run the program and look for invariant violations. One happens immediately:

(gdb) run

Breakpoint 2, bank.deposit (cash=100) at bank.adb:12 12 Balance := Balance + Cash; error: someone tries to deposit before opening an account (gdb)

Indeed, the special offer is credited before the account is opened:

(gdb) up
#1  0x004015da in  () at bank.adb:25
25         Deposit (Special_Offer);

Let us continue to find other violations. The program exits normally, meaning that no other violations were detected.

(gdb) c
Continuing.

Breakpoint 1, bank.open_account (cash=100) at bank.adb:7 7 Balance := Cash; (info) account created with $100

Breakpoint 2, bank.deposit (cash=45) at bank.adb:12 12 Balance := Balance + Cash; (info) deposit: $45

Breakpoint 3, bank.withdraw (cash=55) at bank.adb:17 17 Balance := Balance - Cash; (info) withdrawal: $55

Breakpoint 2, bank.deposit (cash=80) at bank.adb:12 12 Balance := Balance + Cash; (info) deposit: $80 [Inferior 1 (process 7472) exited normally]

The script language of GDB provides various flow-control commands; you may find their full documentation in the section "Command files" in the GDB user's guide. We have seen that this language of GDB, along with convenience variables and breakpoint commands, provides a simple way to check some simple dynamic properties on a run. In order to check more elaborated properties, the full power of expression of the python interface should be used. This will be the subject of a forthcoming Gem.

breakpoint_commands_1

About the Author

Jerome joined AdaCore in 2002 after completing his studies at the Ecole Nationale des Télécommunations (Paris, France), during which he had already worked with the company on one of its many reseach projects, namely PolyORB. His enthusiasm has remained undimmed during these six years and he has worked on a variety of projects, as well as acquiring expertise in debuggers and cross technologies. He has recently led the effort to port GNAT Pro to various cross targets (VxWorks 6, ELinOS).