On Sat, Oct 2, 2010 at 7:13 AM, Cristian Cadar <c.cadar at imperial.ac.uk>
wrote:
>
> 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).
Right. It is certainly possible to encounter compiler bugs in the LLVM
backend when using --optimize.
If you think that might be what is going on, I recommend trying with
2.7 or 2.8 (soon to be released) -- we have made a lot of quality
improvements in the backend in the 2.7 to 2.8 timeframe.
- Daniel
> 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
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
