Yes, I see the same behavior on my machine: KLEE finds the bug in
unoptimized mode, but does not find it with --optimize because that
access is eliminated by LLVM's optimizations. John, it would be
interesting to look into klee-last/assembly.ll to see if something more
interesting is going on there.
Cristian
On 01/25/2012 09:53 AM, Ott Tinn wrote:
> Hi John,
>
> In this case the linkage of "storage" keeps it from being optimized
> away during the initial compilation but afterwards KLEE's optimization
> pass will internalize it anyway and then run the other optimizations.
> Thus at least on my machine the program that ends up being
> symbolically executed when -optimize is used is the following:
>
> define i32 @main(i32 %argc, i8** nocapture %argv) nounwind {
> entry:
> %i = alloca i32, align 4
> %i1 = bitcast i32* %i to i8*
> call void @klee_make_symbolic(i8* %i1, i32 4, i8* getelementptr
> inbounds ([2 x i8]* @.str, i32 0, i32 0)) nounwind
> ret i32 0
> }
>
> If the internalization is skipped by not using -optimize or
> specifically using -disable-internalize then the bug could be found.
> You can confirm the final code by looking at the assembly.ll file in
> the klee-out-N directory. If you didn't use KLEE's optimization pass
> at all then this is could be something more interesting as David
> suggested.
>
> Ott
>
> On Tue, Jan 24, 2012 at 10:16 PM, John Regehr<[email protected]> wrote:
>> Hi Ott,
>>
>> I'm pretty sure optimizations are not the problem.
>>
>> First, "storage" has external linkage -- the compiler cannot infer that it
>> is not subsequently used.
>>
>> Second, llvm-gcc's output for this code (even with optimizations turned on)
>> is a pretty obvious translation of the C code.
>>
>> John
>>
>>
>>
>> On Tue, 24 Jan 2012, Ott Tinn wrote:
>>
>>> Hi John,
>>>
>>> The most obvious problem I see is that the code sample is too simple -
>>> the compiler optimizations could also see that the value you are
>>> storing to the storage array is never used. Since accessing array
>>> elements that are out of bounds is undefined in C then the compiler
>>> can optimize this away by assuming that it isn't out of bounds. To
>>> make this example work you could try compiling without any
>>> optimizations and without using KLEE's -optimize flag or otherwise
>>> making sure the dangerous operations can't be optimized away.
>>>
>>> Ott
>>>
>>> On Tue, Jan 24, 2012 at 9:18 PM, John Regehr<[email protected]> wrote:
>>>>
>>>> Perhaps interesting to people here:
>>>>
>>>> http://blog.regehr.org/archives/672
>>>>
>>>> While writing this up I discovered that when "i" is symbolic Klee cannot
>>>> find a value for i that makes this code access an OOB array element:
>>>>
>>>> int indices[] = { 0,2,1,5,3,0,-77,0,3,6 };
>>>>
>>>> value_t storage[7];
>>>>
>>>> void stash (int i, value_t v)
>>>> {
>>>> if (i<0 || i>=10) {
>>>> error();
>>>> } else {
>>>> int index = indices[i];
>>>> // assert (index>=0);
>>>> // assert (index<7);
>>>> storage[index] = v;
>>>> }
>>>> }
>>>>
>>>> On the other hand, given the assertions, Klee generates the test case
>>>> where
>>>> i==6.
>>>>
>>>> I infer that Klee does not automatically assert in-boundedness of array
>>>> accesses. But these assertions seem obviously desirable, so I'm trying
>>>> to
>>>> figure out why not. Maybe Klee doesn't have enough runtime information
>>>> to
>>>> make this happen?
>>>>
>>>> John
>>>> _______________________________________________
>>>> klee-dev mailing list
>>>> [email protected]
>>>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
