[klee-dev] Unexpected behaviour while learning how to use KLEE
Manuel Carrasco
mcarrasco at quarkslab.com
Thu Jun 3 16:27:38 BST 2021
Thanks a lot.
I am going to move forward taking into account your suggestions.
Kind regards,
Manuel
On 2/6/21 21:39, Nowack, Martin wrote:
> Hi Manuel, hi Alastair,
>
> Currently, KLEE runs still the `CFGSimplificationPass` even with
> `—optimize` off.
> https://github.com/klee/klee/blob/24badb5bf17ff586dc3f1856901f27210713b2ac/lib/Module/KModule.cpp#L288
> <https://github.com/klee/klee/blob/24badb5bf17ff586dc3f1856901f27210713b2ac/lib/Module/KModule.cpp#L288>
>
> This might be not necessary anymore for recent LLVM versions.
>
> The best way forward is indeed using the `optnone` attribute for
> functions you are interested in, e.g. compile your code with `-O0`
> explicitly. There is an option `—klee-call-optimisation=false` which
> marks functions as `optnone` that contain klee function calls
> (`klee_make_symbolic`, `klee_assume`, ...), maybe this option might be
> already sufficient for your use case.
>
> Alternatively, try to comment out the line referenced in the link.
> This might help you in general to workaround this problem.
>
> Hope that helps,
> Martin
>
>
>
>
>> On 2. Jun 2021, at 19:02, Alastair Reid <adreid at google.com
>> <mailto:adreid at google.com>> wrote:
>>
>> 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 <mailto: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 <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list