[klee-dev] Regarding getting variable names from KLEE

[Nazir, Tareq Mohammed]

Hi Ryan,


Thanks for the reply,

Yes I would be needing the source-level variable names and source-level info. We are currently trying to understand the vulnerabilities such as heap overflow that can be present in the source code. We are able to understand the how KLEE engine is able to detect a vulnerability. But we need a map between the information available to us from Memory space of KLEE to the source code. It would be really helpful if I can get this map between the KLEE memory space and source code.


Thanks and Best Regards,

Tareq Mohammed Nazir

________________________________
From: J. Ryan Stinnett <jryans at gmail.com>
Sent: Wednesday, 5 October 2022 14:59:43
To: Nazir, Tareq Mohammed
Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Regarding getting variable names from KLEE

On Wed, 5 Oct 2022 at 10:28, Nazir, Tareq Mohammed <Tareq.Nazir at aau.at> wrote:
> I would like to know if I can get variable names of the source code in KLEE engine. Would also like to know if KLEE engine is storing the variable name information while executing the llvm bitcode symbolically.

KLEE currently thinks in terms of names at the LLVM IR level only, so
this means it does not know about source-level local variables such as
`buffer` in your example.

When you compile with debug info enabled (e.g. the `-g` option with
Clang), the IR does include additional DWARF-like metadata that maps
back to source-level concepts. My current research involves using KLEE
to test this debug info, and as part of that work, I've been enhancing
KLEE so that it can think in terms of source-level info using this
metadata. I hope to eventually add this enhancement to upstream KLEE,
but it may be a few months before I can do so.

It sounds like this enhancement would be useful to you as well. Do you
need only the source-level variable names, or other source-level info
as well?

- Ryan
-------------- next part --------------
HTML attachment scrubbed and removed