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
