[lldb-dev] Symbolic Queries + LLDB

[Milen Dzhumerov]

Sean,

On 18 Oct 2010, at 18:00, Sean Callanan <scallanan at apple.com> wrote:

> Milen,
> 
> when you say "the range of values it can take," are you referring to adding a kind of watchpoint that records range information, so that you can perform integer range analysis etc?  Or are you referring to a query that operates on all instances of a variable (say, a class member) existent at the current time?  Given what KLEE does, I assume the former.

Yes, I was referring to the former. As an example, the programmer would turn on range tracking for a particular variable. Let's assume execution has gone down the path if(x < 5) and the debugger stopped at a breakpoint along that execution. The programmer can then ask what the possible values of x are and it will say [int_min, 5). 

I would assume that's relatively easy to do - is there anything in particular I should be aware of? 

> Right now, even before you start looking at the query infrastructure – or even the watchpoints, really – LLDB really needs support for keeping time-stamped metadata about variables and user interactions.  Because LLDB uses editline, it gets some level of command-line history, but that's pretty much it right now.  A proper metadata infrastructure could provide full history for variable values and function executions, providing a foundation for a variety of LLDB-based program analysis tools.

That sounds quite interesting. I'll be happy to implement the metadata infrastructure, time permitting. Another question - doing the range analysis does not depend on the aforementioned metadata subsystem, as far as I understand? 

> Adding this kind of metadata support to LLDB would be a sizable piece of work, but it could allow you to bring over versions of some KLEE-based tests.  What do you think?

Sounds appealing to me. As the project would need to make measurable progress, ideally it should be possible to do the range analysis / symbolic queries as a starting point and optionally go a lot further.

Milen
>