From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 25261 invoked by alias); 16 Oct 2006 10:18:49 -0000 Received: (qmail 25251 invoked by uid 22791); 16 Oct 2006 10:18:49 -0000 X-Spam-Check-By: sourceware.org Received: from wx-out-0506.google.com (HELO wx-out-0506.google.com) (66.249.82.226) by sourceware.org (qpsmtpd/0.31) with ESMTP; Mon, 16 Oct 2006 10:18:47 +0000 Received: by wx-out-0506.google.com with SMTP id s19so1527846wxc for ; Mon, 16 Oct 2006 03:18:45 -0700 (PDT) Received: by 10.70.30.5 with SMTP id d5mr11174209wxd; Mon, 16 Oct 2006 03:18:45 -0700 (PDT) Received: by 10.70.12.9 with HTTP; Mon, 16 Oct 2006 03:18:45 -0700 (PDT) Message-ID: Date: Mon, 16 Oct 2006 10:18:00 -0000 From: "Rob Quill" To: "Michael Snyder" Subject: Re: Light Formal Methods in GDB Cc: gdb@sourceware.org In-Reply-To: <1160765208.14535.251.camel@localhost.localdomain> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <1160682474.14535.188.camel@localhost.localdomain> <1160765208.14535.251.camel@localhost.localdomain> X-IsSubscribed: yes Mailing-List: contact gdb-help@sourceware.org; run by ezmlm Precedence: bulk List-Subscribe: List-Archive: List-Post: List-Help: , Sender: gdb-owner@sourceware.org X-SW-Source: 2006-10/txt/msg00111.txt.bz2 On 13/10/06, Michael Snyder 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