[klee-dev] Regarding getting variable names from KLEE

[Nowack, Martin]

Hi Tareq,

I can highly recommend you the following documents to get an understanding of the internal details of debug information and LLVM that KLEE uses in the first place:
* https://llvm.org/docs/SourceLevelDebugging.html
* https://llvm.org/docs/HowToUpdateDebugInfo.html

For the examples that you asked for, a good starting point for me are often the transformation passes of LLVM, i.e. (llvm-project/llvm/lib/Transforms/) to get an idea how different concepts are implemented and might work.
(Just one example: https://github.com/llvm/llvm-project/blob/53dc0f107877acad44824b1426986c7f88f4bc50/llvm/lib/Transforms/IPO/MergeFunctions.cpp#L566)

A good IDE support makes a huge difference in working through the source code and makes it slightly less painful.

Best,
Martin

> On 5. Oct 2022, at 20:58, Nazir, Tareq Mohammed <Tareq.Nazir at aau.at> wrote:
> 
> Hi Frank,
> 
> Thanks for the reply,
> 
> Yes I have used the second option and -fno-discard-value-names and I am able to see the variable name in the llvm bitcode .ll file. But what I need is the access to this variables in KLEE engine. Also I am trying to use DILocalVariable. I would like to know if it is possible to share any example where DILocalVariable can be used to extract the variable name. This would be really helpful.
> 
> Thanks and Best Regards,
> Tareq Mohammed Nazir
> From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Frank Busse <f.busse at imperial.ac.uk>
> Sent: Wednesday, 5 October 2022 13:05
> Cc: klee-dev at imperial.ac.uk
> Subject: Re: [klee-dev] Regarding getting variable names from KLEE
>  
> Hi,
> 
> 
> On Wed, 5 Oct 2022 09:26:35 +0000
> "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.
> > 
> > 
> > For example : From the below C code I want to get the buffer variable
> > name is it possible or not.
> > 
> > 
> > int main(int argc, char *argv[])
> > {
> >        char *buffer = malloc(5);
> >        buffer[6] = 'a';
> >        return 0;
> > }
> 
> There are at least two options:
> 
> 1) you compile your code with debug information (-g) and recover the
>    information from there (LLVM API):
> 
> !15 = !DILocalVariable(name: "buffer", scope: !10, file: !1, line: 4, type: !16)
> 
> 2) or you tell clang to keep variable names (-fno-discard-value-names)
>    and it will generate bitcode like:
> 
> %buffer = alloca i8*, align 8
> store i8* %call, i8** %buffer, align 8
> %0 = load i8*, i8** %buffer, align 8
> 
>    instead of:
> 
> %2 = alloca i8*, align 8
> store i8* %3, i8** %2, align 8
> %4 = load i8*, i8** %2, align 8
> 
> 
> Kind regards,
> 
> Frank
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev