[lldb-dev] Symbolic Queries + LLDB

[Sean Callanan]

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.

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.

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?

Sean

On Oct 16, 2010, at 8:48 AM, Milen Dzhumerov wrote:

> Hi all,
> 
> I'm a CS student on a Masters program at Imperial (UK) and Cristian Cadar (one of the authors of the original KLEE paper, http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf) and I will be undertaking a project related to KLEE. One of our ideas is adding symbolic queries to LLDB, so users can not only get the value of a particular variable but also the range of values it can take.
> 
> Before choosing any particular project, I wanted to ask whether there's any external interest in adding symbolic queries to LLDB.
> 
> Thanks,
> Milen
> _______________________________________________
> lldb-dev mailing list
> lldb-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/lldb-dev