Re: Light Formal Methods in GDB

["Rob Quill" <rob.quill@gmail.com>]

On 13/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:
> On Fri, 2006-10-13 at 11:04 +0100, Rob Quill wrote:
> > Hi,
> >
> > The principle works as follows:
> >
> > It it possible to create an automaton from an LTL formula, with
> > expressions for values of variables as the transitions from one state
> > to the next.
> >
> > Then the tricky part is building an automaton which represents the
> > program. But once you have these it is possible to see if the
> > automaton 'match' and if they do then the property holds.
> >
> > With regards to building the system automaton, at the very simplest
> > you could single step the code, get values of variables at each step
> > and make an appropriate transition on the automaton. However, this is
> > obviously very inefficient, and improvements would most likely be made
> > by building a control flow graph of the program (in some way) and use
> > the nodes of that graph as the points get get values, or something
> > like that.
> >
> > The advantage of including something like this in GDB is that once the
> > property that the programmer expected to hold becomes false, program
> > execution can stop and he programmer can use the standard GDB tools.
> > Well, that'd be the idea anyway.
> >
> > The original idea was to do the same thing but for concurrent programs
> > because there is research which says that using LTL formulas and the
> > automaton technique, you can say whether properties of concurrent
> > programs hold for all the possible interleavings. However, it was
> > decided that that was too complicated, so it was narrowed to
> > non-concurrent programs.
>
> OK.  Well, once you have your list of nodes and properties (values),
> maybe you could have your software emit a set of breakpoint definitions
> for gdb, with appropriate rules for evaluating sets of values at each
> breakpoint.  Gdb already has a scripting language that includes "if"
> and "while", and you can define debugger-local variables to define
> your finite automaton and control its state.  Then, depending on those
> state variables, gdb can stop the program or let it continue.  You
> can also include "print" statements to log your state.
>
> This sounds like an interesting project, and I don't think
> it should require any modifications to gdb (or at least, any
> major ones).  You would generate a script for gdb to set up
> the breakpoints and states, then run gdb in batch mode with
> the output piped into a file.  You would then post-process
> that file for your results.

Hi.

Could you elaborate on this please. I am confused as to how I could
use the GDB scripting language. Can I say things such as "if val = 1"
then do some transition of the automaton and then single step the
program? Or, say that I has somehow already figured out where I wanted
the breakpoints to be I could just set GDB to break there, make
automaton transitions and then keep going.

Is that what you meant? Because that sounds excellent and a lot
simpler than trying to build it into GDB some how, which was what I
thought I would have to do.

Rob