Hi Stefan,
I cannot reproduce your problem on my machine. I created a simple
program that uses your function, but I don't get any memory errors
regardless of whether I use --optimize or not: the optimized code does
inline the function, but seems to do so correctly. Can you provide more
details about your setup and precise benchmarks?
BTW, the bug would most likely be in LLVM (I'm using LLVM 2.7), not
KLEE: the --optimize option simply calls a series of compile- and
link-time LLVM optimizations (take a look at lib/Module/Optimize.cpp for
details).
Best,
Cristian
On 10/01/2010 08:50 PM, Stefan Bucur wrote:
> Hi,
>
> I've run into a strange problem after implementing a Klee model for
> the __ctype_b_loc library call, responsible with delivering locale
> information to the<ctype.h> library functions.
>
> Whenever I set the --optimize flag in Klee, I start getting (false)
> memory errors. After analyzing the generated assembly.ll file, I saw
> that Klee inlined the call to this function, and replaced it with just
> a memory access to a static variable that I use in the function body.
> However, that static variable is also initialized in the function, but
> the initialization code ends up not being there, hence the systematic
> memory errors.
>
> The offending code is the following:
>
> static const unsigned short *b_locale = NULL;
>
> const unsigned short model__ctype_b_loc(void) {
> if (b_locale != NULL)
> return&b_locale;
>
> unsigned short *cached = (unsigned short*)malloc(384*sizeof(unsigned
> short));
>
> const unsigned short **locale = __ctype_b_loc();
> memcpy(cached,&((*locale)[-128]), 384*sizeof(unsigned short));
> b_locale =&cached[128];
> return&b_locale;
> }
>
> Basically, the function simply returns the address of b_locale, unless
> b_locale was not initialized. The initialization part seems to be
> skipped after the optimizations.
>
> Do you have any idea what could be wrong?
>
> Thank you,
> Stefan
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
