[klee-dev] Please help me figure out what is happening in External Dispatcher

Chace Clark chace3 at tamu.edu
Fri Apr 10 20:56:47 BST 2015


Yeah I though I mentioned that its present on my forked version of klee. I
am trying to update klee to be able to use llvm 3.6, so I have modified
many parts of the klee code. I have put some time into this and it is at
the state where I can pass most of the regression tests. Here is my reg
test output:

Failing Tests (17):
    KLEE :: Feature/Envp.c
    KLEE :: Feature/FunctionPointer.c
    KLEE :: Feature/LongDouble.cpp
    KLEE :: Feature/MultipleReadResolution.c
    KLEE :: Feature/MultipleWriteResolution.c
    KLEE :: Runtime/POSIX/FDNumbers.c
    KLEE :: Runtime/POSIX/FD_Fail.c
    KLEE :: Runtime/POSIX/Fcntl.c
    KLEE :: Runtime/POSIX/FilePerm.c
    KLEE :: Runtime/POSIX/Futimesat.c
    KLEE :: Runtime/POSIX/Getenv.c
    KLEE :: Runtime/POSIX/Ioctl.c
    KLEE :: Runtime/POSIX/Isatty.c
    KLEE :: Runtime/POSIX/Openat.c
    KLEE :: Runtime/POSIX/PrgName.c
    KLEE :: Runtime/POSIX/Read1.c
    KLEE :: Runtime/POSIX/Stdin.c

  Expected Passes    : 141
  Expected Failures  : 2
  Unsupported Tests  : 1
  Unexpected Failures: 17

Anyway its only present in my forked version, which lives here:

https://github.com/ccadeptic23/klee

When I run the code against the unmodified klee using llvm 3.4.2 the code
works fine. So I was hoping for some help understanding the external
dispatcher process. I finally found where the args are stored before the
runFunction call and they look fine, but am having trouble debugging this
process. ie Trying to step into the external Function call in my debugger.

I want to see the stupid thing access that memory location ugg... I mean
somehow that string "a" is being printed, just cannot figure out how.

I encountered this problem when running the Envp.c test. So the example I
gave before is just a simplified version of that test.

Anyway any tips or thoughts would be helpful.



On Fri, Apr 10, 2015 at 2:35 PM, Dan Liew <dan at su-root.co.uk> wrote:

> Hi,
>
> On 10 April 2015 at 18:28, Chace Clark <chace3 at tamu.edu> wrote:
> > I am trying to figure out why some of my calls to external functions are
> > producing odd behaviors. Its like some functions are leaving things on
> the
> > stack.
> > For example when I run my version of KLEE on:
> >
> > void main(){
> >   printf("hi\n");
> >   int haspwd = strncmp("a", "PWD=", 4)==0;
> >   printf("bye\n");
> > }
>
> I can't reproduce this issue
>
> ```
> $ clang -c -emit-llvm foo.c -o foo.bc
> foo.c:1:1: warning: return type of 'main' is not 'int' [-Wmain-return-type]
> void main(){
> ^
> foo.c:1:1: note: change return type to 'int'
> void main(){
> ^~~~
> int
> foo.c:2:3: warning: implicitly declaring library function 'printf'
> with type 'int (const char *, ...)'
>   printf("hi\n");
>   ^
> foo.c:2:3: note: please include the header <stdio.h> or explicitly
> provide a declaration for 'printf'
> foo.c:3:16: warning: implicitly declaring library function 'strncmp'
> with type 'int (const char *, const char *, unsigned long)'
>   int haspwd = strncmp("a", "PWD=", 4)==0;
>                ^
> foo.c:3:16: note: please include the header <string.h> or explicitly
> provide a declaration for 'strncmp'
> 3 warnings generated.
>
> $ klee foo.bc
> KLEE: output directory is "/home/klee/klee-out-0"
> KLEE: WARNING: undefined reference to function: printf
> KLEE: WARNING: undefined reference to function: strncmp
> KLEE: WARNING ONCE: calling external: printf(42827920)
> hi
> KLEE: WARNING ONCE: calling external: strncmp(42746256, 42651584, 4)
> bye
>
> KLEE: done: total instructions = 8
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
> ```
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list