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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
