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

[Cristian Cadar]

Hi Haoxin,

It looks to me that you are not passing a null-terminated string to 
error() in the heap case, and the error reported by KLEE is genuine.

Best,
Cristian

On 24/01/2024 15:53, TU Haoxin wrote:
> 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 <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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev