From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 24056 invoked by alias); 13 Oct 2006 18:47:15 -0000 Received: (qmail 24040 invoked by uid 22791); 13 Oct 2006 18:47:09 -0000 X-Spam-Check-By: sourceware.org Received: from mx2.palmsource.com (HELO mx2.palmsource.com) (12.7.175.14) by sourceware.org (qpsmtpd/0.31) with ESMTP; Fri, 13 Oct 2006 18:46:52 +0000 Received: from localhost (localhost [127.0.0.1]) by localhost.domain.tld (Postfix) with ESMTP id 834E427A2E; Fri, 13 Oct 2006 11:46:51 -0700 (PDT) Received: from mx2.palmsource.com ([127.0.0.1]) by localhost (mx2.palmsource.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 15817-09-36; Fri, 13 Oct 2006 11:46:50 -0700 (PDT) Received: from ussunex01.palmsource.com (unknown [192.168.101.9]) by mx2.palmsource.com (Postfix) with ESMTP id 633A827A2C; Fri, 13 Oct 2006 11:46:50 -0700 (PDT) Received: from 192.168.92.75 ([192.168.92.75]) by ussunex01.palmsource.com ([192.168.101.9]) via Exchange Front-End Server owa.palmsource.com ([10.0.20.17]) with Microsoft Exchange Server HTTP-DAV ; Fri, 13 Oct 2006 18:46:50 +0000 Received: from svmsnyderlnx by owa.palmsource.com; 13 Oct 2006 11:46:48 -0700 Subject: Re: Light Formal Methods in GDB From: Michael Snyder To: Rob Quill Cc: gdb@sourceware.org In-Reply-To: References: <1160682474.14535.188.camel@localhost.localdomain> Content-Type: text/plain Content-Transfer-Encoding: 7bit Date: Fri, 13 Oct 2006 18:47:00 -0000 Message-Id: <1160765208.14535.251.camel@localhost.localdomain> Mime-Version: 1.0 X-Mailer: Evolution 2.4.1 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/msg00091.txt.bz2 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.