[lldb-dev] Symbolic Queries + LLDB
milen at thecosmicmachine.com
Mon Oct 18 10:29:18 PDT 2010
On 18 Oct 2010, at 18:00, Sean Callanan <scallanan at apple.com> wrote:
> 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.
More information about the lldb-dev