[lldb-dev] Symbolic Queries + LLDB

[Milen Dzhumerov]

Greg,

On 18 Oct 2010, at 21:29, Greg Clayton wrote:

> What is the information would you like to get out of the debugger that isn't available just from the AST's and the symbolic query stuff that already works with llvm/clang? 

The crucial information that the debugger would provide are actual values. As a concrete example, let's suppose there's an expression like if(a + b < 10) and the execution has taken that branch. Let's also suppose the value of b = 4. Then we can infer that a < 6 which would be available to the programmer as a debugging aid.

Another level on top of that would be to allow the programmer to ask symbolic queries - for example, can a + b > 5 or can a < 10 etc. If we combine this with history tracking, we can tell what actual value ranges those variables ever took. That could be useful when writing tests - not only can it be determined whether all code paths are covered but also what part of the whole value range has been tested in reality.

Some of the examples described above are available in KLEE (the range analysis is not although it's another project that is being considered) but the crucial difference is coupling those ideas in a real debugger. Whether the benefits are worth it is quite a subjective matter and that's one of the reasons why I asked the question on the mailing list.

If the LLDB leaders decide that the project that I've described is not appropriate as part of the codebase, that would be completely understandable. Actually, I'm more than interested in any opportunities for research-grade LLDB-related projects, so please email me on / off list if there are any other suggestions / opportunities available.

In summary, the aim of the original proposal was to couple symbolic queries and actual data collected at runtime by the debugger to be able to answer symbolic queries about variables.

Milen