[klee-dev] Different behavior when invoking the "error" function with the argument buffer from heap or stack

[TU Haoxin]

Dear KLEE developers,

Hope you are all doing well, and hope this is the right place to raise questions about KLEE.

I have a question regarding the modeling of the function `error` function in `klee-uclibc` when I used KLEE. Since I couldn't find similar cases either in the GitHub issue or the klee-dev mailing list, I would like to seek your suggestions here. I do apologize if I missed anything.

Please consider the following simple code (test.c):
```
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdbool.h>
#include <error.h>

static void * //_GL_ATTRIBUTE_PURE
nonnull (void *p)
{
  if (!p){
    exit(1);
  }
  return p;
}

void * xxmalloc (int s){
    return nonnull (malloc(s));
}

int main(){
    char *p =(char*) xxmalloc(10); // p from heap
    memset(p, 'A', 10);
    error(1, 1, p, p); // this is problematic
    //char* pp = "hello world.\n"; // pp from stack
    //error(1, 1, pp, pp); // this is ok
    free(p);
    return 0;
}
```

Commands to compile the above code and run klee (execute.sh):
```
#!/bin/bash
clang -emit-llvm -c -g test.c
klee --libc=uclibc --posix-runtime test.bc
```

Execute the script `execute.sh`, I got the following:

```
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 93825035744416) at runtime/POSIX/fd.c:1007 10
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: ERROR: libc/stdio/_vfprintf.c:572: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 17386
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1
```

Here is the stack information when the error occurs:
```
Error: memory error: out of bound pointer
File: libc/stdio/_vfprintf.c
Line: 572
assembly.ll line: 18473
State: 1
Stack:
      #000018473 in _ppfs_init (=93825004575232, =93825035189056) at libc/stdio/_vfprintf.c:572
      #100015268 in vfprintf (=93825004959696, =93825035189056, =93825035841056) at libc/stdio/_vfprintf.c:1888
      #200012650 in __error (=1, =1, =93825035189056) at libc/misc/error/error.c:57
      #300009767 in __klee_posix_wrapped_main () at test.c:24
      #400007354 in __user_main (=1, =93825013002624, =93825013002640) at runtime/POSIX/klee_init_env.c:245
      #500000592 in __uClibc_main (=93825035146016, =1, =93825013002624, =0, =0, =0, =0) at libc/misc/internals/__uClibc_main.c:401
      #600000757 in main (=1, =93825013002624)
Info:
      address: 93825035189066
      next: object at 93825004575232 of size 256
            MO7712[256] allocated at vfprintf():  %7 = alloca %struct.ppfs_t.715, align 16
```
I tested the above code using clang-9 with klee-2.1 (as well as klee-2.3-pre).
```
$klee --version
KLEE 2.3-pre (https://klee.github.io)
  Build mode: Debug (Asserts: ON)
  Build revision: 0ba95edbad26fe70c8132f0731778d94f9609874

LLVM (http://llvm.org/):
  LLVM version 9.0.0

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake-avx512
```

The confusion is that when I replaced the pointer `p` from the heap to `pp` from the stack (as shown in the two commented lines), KLEE could execute the function `error` well. I think both the buffers from the heap or stack should work (I tested the native execution and these two versions of code both work ok) but it does not in KLEE, and I don't know why that is the case. Since the `error` function involves variadic arguments (https://github.com/klee/klee-uclibc/blob/klee_0_9_29/libc/misc/error/error.c#L50), I suspect that this is because KLEE has some implementation limitations of the handling of variadic functions when it involves the pointers from the heap (I also tried to find the reason behind it but failed). Could you please take a look and help me understand about this case? Why does KLLE behave differently when the pointer is from the heap or stack? Any ideas or insights are welcome!

Thank you so much for your time and help!


Best regards,
Haoxin
-------------- next part --------------
HTML attachment scrubbed and removed