[klee-dev] Can klee generate a combined path expression to reach a particular statement?

[Dan Liew]

Hi,

On 27 January 2017 at 22:20, Cong Yan <congyan.apply at gmail.com> wrote:
> Hi,
>
> Is klee able to generate an expression combining different paths? For
> example,
>
> if (a)
>     stmt1;
> else
>     stmt2;
> stmt3;

The answer is yes and no. It is all dependent on how the C program
above is translated into LLVM IR

For Clang if the code is not optimized these would be broken into
basic blocks with a branch instruction. It that case KLEE
will fork and generate two paths that reach `stmt3`.

To see this

run

clang -S -emit-llvm x.c -o -

on

```
#include <stdio.h>

int main() {
  int a = 0;
  if (a) {
    a = 1;
  }
  else {
    a = 2;
  }
  printf("done %d\n", a);
  return 0;
}
```

You'll see something like

```
; Function Attrs: nounwind uwtable
define i32 @main() #0 {
  %1 = alloca i32, align 4
  %2 = alloca i32, align 4
  store i32 0, i32* %1, align 4
  store i32 0, i32* %2, align 4
  %3 = load i32, i32* %2, align 4
  %4 = icmp ne i32 %3, 0
  br i1 %4, label %5, label %6

; <label>:5:                                      ; preds = %0
  store i32 1, i32* %2, align 4
  br label %7

; <label>:6:                                      ; preds = %0
  store i32 2, i32* %2, align 4
  br label %7

; <label>:7:                                      ; preds = %6, %5
  %8 = load i32, i32* %2, align 4
  %9 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x
i8], [9 x i8]* @.str, i32 0, i32 0), i32 %8)
  ret i32 0
}
```

Note the branching (`br` instruction). KLEE will fork if more than one
path from the branch is feasible.

However if certain passes are run the branching can be removed.

clang -S -emit-llvm x.c -o - | opt -mem2reg -simplifycfg -S

You'll see output like this.

```
...
define i32 @main() #0 {
  %1 = icmp ne i32 0, 0
  %. = select i1 %1, i32 1, i32 2
  %2 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x
i8], [9 x i8]* @.str, i32 0, i32 0), i32 %.)
  ret i32 0
}
...
```

You can see there are no branches here and there is a `select`
instruction instead.

This is a special case though. If you put code that has side effects
in the `if` or `else` blocks then LLVM will not
be able to simplify the control flow graph to remove the branches.


Instead you may want to experiment with the `klee_merge()` instrinsic
with I believe is supposed to do state merging.
Note that this instrinsic is experimental and I have no idea if it
still (did it ever?) works.

HTH,
Dan.