Re: [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  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 

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

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

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

; :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.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] One question about external dispatcher

[Dan Liew]

On 27 January 2017 at 04:18, Qiuping Yi  wrote:
> Dear all,
>
> I encountered a strange problem when testing the next code snippet:
>
> 1 if (pw = getpwuid(getuid()) == NULL)
> 2   return ;
>
> 3 .. = pw->pw_dir;

Please use the correct mailing list (klee-dev@imperial.ac.uk) instead
of the old klee-...@keeda.stanford.edu mailing list.

It would be better if you provided a small complete example. Like this.

```
#include 
#include 
#include 
#include 
#include 

int main(int arc, char** argv) {
  struct passwd* pw;
  uid_t uid = getuid();
  printf("uid is %d\n", uid);
  if (pw = getpwuid(getuid()) == NULL) {
printf("Failed\n");
return 1;
  }
  assert(pw && "pw cannot be NULL");

  char* pw_dir = pw->pw_dir;
  printf("pw_dir: %s\n", pw_dir);
  return 0;
}
```

Your code is wrong.

if (pw = getpwuid(getuid()) == NULL)

is doing this

if ( pw = ( getpwuid(getuid()) == NULL )

so a pointer is returned by `getpwuid()` and then we compare with NULL
which is false so then `pw` gets assigned the value zero.

However once I fix your code to

if ((pw = getpwuid(getuid())) == NULL) {

then I can reproduce the problem if I just run `klee program.bc`

I suspect it's to do with the fact `getpwuid()` returns a pointer to
"real memory" which does not point to anything in KLEE's own model of
the memory (i.e. the address space of the program under).

To fix this you need not call `getpwuid()` as an external function but
instead call it from klee-uclibc so that it can be symbolically
executed.

If you run

```
klee -libc=uclibc program.bc
```

no out of bounds access is reported.

HTH,
Dan.


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev