Re: Light Formal Methods in GDB

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

On Mon, 2006-10-16 at 11:18 +0100, Rob Quill wrote:
> On 13/10/06, Michael Snyder <Michael.Snyder@palmsource.com> wrote:

> >
> > 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.
> 
> 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.

Sure.  First compose all the rules for your automaton.
Then you can compose a gdb script file that might look, 
in part, something like this:

# Create automaton using GDB user-defined variables

set $automaton_state = 0
set $automaton_value1 = 17
set $automaton_value2 = 44
# etc.

# Set up breakpoints to manage state transitions

break foo
commands
  silent
  if (program_var1 > program_var2) && (program_var3 == 0)
    set $automaton_state = 22
  end
end

Consult the gdb docs and runtime help to learn about the
macro command language.


> 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.

Yep!