Ohhh, snap! I was living under the impression that the x86 architecture
shares the same syscall table both for the 32- and 64-bit versions.
Thanks a lot for the quick answer, guys!
Stefan
On Wed, Apr 20, 2011 at 7:35 PM, David A. Ramos <daramos at stanford.edu>wrote:
> Stefan,
>
> Those syscall numbers appear to be for 32-bit Linux. Look in
> your /usr/include/asm/unistd_64.h file for the 64-bit syscall numbers, which
> are significantly different. They should correspond to what KLEE reports.
>
> -David
>
> On Apr 20, 2011, at 10:08 AM, Stefan Bucur wrote:
>
> Hi all,
>
> I recently noticed that whenever an external syscall() function is invoked
> in Klee, the syscall number (the first parameter of the function) is
> wrongfully displayed, although the correct syscall actually gets executed. I
> studied the external call logging code in the Executor to see if there is
> any bug, but I could not find any flaw.
>
> For instance, for the following simple program:
>
> #include <stdio.h>
> #include <string.h>
>
> int main(int argc, char **argv) {
> int a = 1;
> int b = 2;
> char buff[256];
> sprintf(buff, "Hey there %d, %d!\n", a, b);
> write(1, buff, strlen(buff));
> return 0;
> }
>
>
> Klee gives the following output (syscall numbers are in bold):
>
> *$ klee --posix-runtime --libc=uclibc --all-external-warnings test.o*
> KLEE: NOTE: Using model:
> /home/stefan/klee-vanilla/Release/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-1"
> KLEE: WARNING: undefined reference to function: klee_get_valuel
> KLEE: WARNING: calling external: syscall(*16*, 0, 21505, 28322480)
> KLEE: WARNING: calling external: syscall(*16*, 1, 21505, 23118944)
> KLEE: WARNING: calling __user_main with extra arguments.
> KLEE: WARNING: calling external: syscall(*4*, 28261456, 28343024)
> KLEE: WARNING: calling external: syscall(*1*, 1, 28458064, 16)
> Hey there 1, 2!
>
> KLEE: done: total instructions = 15504
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
> While they appear as normal syscall numbers, they are actually incorrect,
> according to the Linux syscall table[1] . For instance, the write() syscall
> is shown as syscall #1, while it should have been #4. The fstat() syscalls
> in the beginning also have the wrong numbers.
>
> Do you have any idea for why this happens? Am I interpreting the output
> incorrectly?
>
> Thanks,
> Stefan
>
>
> [1] http://syscalls.kernelgrok.com/
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110420/7bdb06fb/attachment.html
