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

[Nowack, Martin]

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

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
_______________________________________________
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