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

[Manuel Carrasco]

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>
>
-------------- next part --------------
HTML attachment scrubbed and removed