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

[Alastair Reid]

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