[klee-dev] Unexpected behaviour while learning how to use KLEE

[Alastair Reid]

I think a KLEE dev will need to suggest how to prevent the optimization
from happening.
KLEE has a flag controlling optimization "--optimize" - but it is supposed
to be off by default

--
Alastair

On Wed, Jun 2, 2021 at 4:49 PM Manuel Carrasco <mcarrasco at quarkslab.com>
wrote:

> Thanks for your answer!
>
> You hit the nail on the head. The *assembly.ll *file contains:
>
>   %original_result = call i1 @original(i32 %a_value, i32 %b_value)
>   %final_result = call i1 @final(i32 %a_value, i32 %b_value)
>   %equal = icmp eq i1 %original_result, %final_result
>   %spec.select = select i1 %equal, i32 0, i32 1
>   ret i32 %spec.select
>
> What I understand from this is that KLEE doesn't consider the select
> instruction as a control flow instruction. Thus, only one path is explored.
> Is it correct?
>
> How would you prevent this optimization from happening? The way I'm using
> KLEE is by directly inputting a .ll file (the one I originally shared). The
> only thing that comes to my mind is setting the *optnone* attribute. In
> other words, how would you make sure that KLEE doesn't optimize feasible
> paths?
>
> Kind regards,
> Manuel.
> On 1/6/21 16:58, Alastair Reid wrote:
>
> Hi Manuel,
>
> Maybe your code is being optimized to avoid the conditional branch.
> That is, maybe the preprocessing/transformations performed by KLEE are
> replacing the last three instructions of main with "ret not(%equal)".
>
> I'm not certain that this is what's happening but the
> klee-last/assembly.ll file shows you what KLEE actually executes so it
> should be easy to check.
>
> --
> Alastair
>
>
> On Mon, May 31, 2021 at 9:27 PM Manuel Carrasco <mcarrasco at quarkslab.com>
> wrote:
>
>> Dear klee-dev,
>>
>> I am learning how to use KLEE and the results I am getting are not the
>> ones I would expect. Thus, I would be more than grateful if anyone could
>> spot what I am doing/understanding incorrectly.
>>
>> To the best of my knowledge, in the following example, there are two
>> possible paths starting from main, although KLEE (v2.2) only reports one.
>> declare void @klee_make_symbolic(i8*, i64, i8*)
>>
>> @.stra = private unnamed_addr constant [2 x i8] c"a\00", align 1
>> @.strb = private unnamed_addr constant [2 x i8] c"b\00", align 1
>>
>> define i32 @main() {
>> entry:
>>   %a = alloca i32, align 4
>>   %b = alloca i32, align 4
>>   %a_bitcast = bitcast i32* %a to i8*
>>   %b_bitcast = bitcast i32* %b to i8*
>>
>>   call void @klee_make_symbolic(i8* %a_bitcast, i64 4, i8* getelementptr
>> inbounds ([2 x i8], [2 x i8]* @.stra, i64 0, i64 0))
>>   %a_value = load i32, i32* %a, align 4
>>
>>   call void @klee_make_symbolic(i8* %b_bitcast, i64 4, i8* getelementptr
>> inbounds ([2 x i8], [2 x i8]* @.strb, i64 0, i64 0))
>>   %b_value = load i32, i32* %b, align 4
>>
>>   %original_result = call i1 @original(i32 %a_value, i32 %b_value)
>>   %final_result = call i1 @final(i32 %a_value, i32 %b_value)
>>
>>   %equal = icmp eq i1 %original_result, %final_result
>>   br i1 %equal, label %IfEqual, label %IfUnequal
>>
>> IfEqual:
>>     ret i32 0
>>
>> IfUnequal:
>>     ret i32 1
>> }
>>
>> define i1 @original(i32 %"a", i32 %"b") {
>>   %"c" = icmp ugt i32 %"a", %"b"
>>   ret i1 %"c"
>> }
>>
>> define i1 @final(i32 %"a", i32 %"b") {
>>   %"c" = icmp sgt i32 %"a", %"b"
>>   ret i1 %"c"
>>
>> }
>>
>> Storing the above code as *query.ll*, the command* klee query.ll* prints:
>>
>>
>> klee at 2444e54c9f66:/shared/test$ klee query.ll
>> KLEE: output directory is "/shared/test/klee-out-28"
>> KLEE: Using STP solver backend
>>
>> KLEE: done: total instructions = 17
>> KLEE: done: completed paths = 1
>> KLEE: done: generated tests = 1
>>
>> For instance, these are two possible inputs that would allow me to
>> explore both paths:
>>
>>    - "a" = 0x80000000, "b" = 0x1 (*IfUnequal label*)
>>    - "a" = 0x0, "b" = 0x0 (this is the only one reported by KLEE - *IfEqual
>>    label*)
>>
>> Yet, only one is reported and so far I cannot understand the reason why.
>> Is this related to how i32 integers are represented by KLEE? Conversely, I
>> would not be surprised if I am doing something wrong.
>>
>> Kind regards,
>>
>> Manuel.
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed