Re: Light Formal Methods in GDB

[Michael Snyder <Michael.Snyder@palmsource.com>]

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.