Simple code for KLEE

[Aleksandr Malyutin]

Hi,

I tried to use klee on simple c-code example:

#include <stdio.h>

int plus(int first){
if(first+2 == 4)return 1;
return 0;
}

int main(int argc, char *argv[]){
if(argc == 2) return plus(atoi(*argv[1]));
return -1;
}

My steps were:

1) Create object file by:

llvm-gcc --emit-llvm -c 2plus2.c



2) Generate test-cases:

klee --posix-runtime 2plus2.o --sym-arg 1

KLEE: NOTE: Using model: /home/malyutin/klee/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/malyutin/klee/klee/examples/my_example/klee-out-0"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: atoi
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: __xstat64(1, 53487840, 53587488)
KLEE: WARNING ONCE: calling external: atoi(53548944)

KLEE: done: total instructions = 581
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1


3) After that I checked resulting test-case:

ktest-tool klee-last/test000001.ktest


ktest file : 'klee-last/test000001.ktest'
args : ['2plus2.o', '--sym-arg', '1']
num objects: 2
object 0: name: 'arg0'
object 0: size: 2
object 0: data: ' \x00'
object 1: name: 'model_version'
object 1: size: 4
object 1: data: '\x01\x00\x00\x00'

It's simple to see that klee generates test-case for one of three branches. Maybe my code is incorrect or my method for generating test-cases is wrong, but all my attempts to get three test-cases for three branches of my program were absolutely useless.

Help me please and say what I do wrong.

Many thanks,
Aleksander.

[Daniel Liew]

Your code uses atoi() which isn't part of your 2plus2 program. Notice
that KLEE warns about this

KLEE: WARNING: undefined reference to function: atoi

and later calls this function

KLEE: WARNING ONCE: calling external: atoi(53548944)

An external function, is a function that isn't in the bitcode being
executed (which is your 2plus2.o code linked with which ever libraries
you asked KLEE to use. In your case you asked only for the POSIX
runtime).

When KLEE encounters an external function it makes the arguments to
that function concrete and then calls the native function ``atoi()``.
In your case making arguments to atoi() concrete will cause test cases
to be lost.

Try linking with klee-uclibc (use -libc=uclibc) which probably
provides an implementation of atoi(). If it doesn't you can always add
your own.

Note atoi() probably has quite a lot of branching behaviour so you may
generate many more paths that you might expect. In which case you
might just want to do something much simpler like this...

```
int plus(int first){

if(first+2 == 4)return 1;

return 0;
}


int main(int argc, char *argv[]){

int x;
klee_make_symbolic(&x, sizeof(x));
return plus(x);
}
```

Hope that helps.

[Urmas Repinski]

Hi.
Exactly that i suggested too. :)
Urmas.

> Date: Thu, 10 Jul 2014 14:47:53 +0100
> From: daniel.liew-AQ/***@public.gmane.org
> To: Aleksandr.Malyutin-O7H/y4DKl+***@public.gmane.org
> CC: klee-dev-AQ/***@public.gmane.org
> Subject: Re: [klee-dev] Simple code for KLEE
>
> Your code uses atoi() which isn't part of your 2plus2 program. Notice
> that KLEE warns about this
>
> KLEE: WARNING: undefined reference to function: atoi
>
> and later calls this function
>
> KLEE: WARNING ONCE: calling external: atoi(53548944)
>
> An external function, is a function that isn't in the bitcode being
> executed (which is your 2plus2.o code linked with which ever libraries
> you asked KLEE to use. In your case you asked only for the POSIX
> runtime).
>
> When KLEE encounters an external function it makes the arguments to
> that function concrete and then calls the native function ``atoi()``.
> In your case making arguments to atoi() concrete will cause test cases
> to be lost.
>
> Try linking with klee-uclibc (use -libc=uclibc) which probably
> provides an implementation of atoi(). If it doesn't you can always add
> your own.
>
> Note atoi() probably has quite a lot of branching behaviour so you may
> generate many more paths that you might expect. In which case you
> might just want to do something much simpler like this...
>
> ```
> int plus(int first){
>
> if(first+2 == 4)return 1;
>
> return 0;
> }
>
>
> int main(int argc, char *argv[]){
>
> int x;
> klee_make_symbolic(&x, sizeof(x));
> return plus(x);
> }
> ```
>
> Hope that helps.
>
> _______________________________________________
> klee-dev mailing list
> klee-dev-AQ/***@public.gmane.org
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Urmas Repinski]

Hi, Aleksander.
I had found 2 problems, maybe correcting them will solve the question.
Problem N1 i found:
> My steps were:........... > 2) Generate test-cases:> klee --posix-runtime 2plus2.o --sym-arg 1 ..............
"--sym-arg 1" means that one symbolic argument will be generated, with size 1 bytes, that were generated, argv[1] should be in the program if i understood right:

> object 0: name: 'arg0'> object 0: size: 2> object 0: data: ' \x00'
http://klee.github.io/klee/TestingCoreutils.html -sym-arg - Replace by a symbolic argument with length N
Probably it is necessary to use "--sym-args 1 2 1"Then MIN 1 and MAX 2 arguments of size 1 should be generated, this should cover the "return -1" branch.

Problem N2 i found:
There is"KLEE: WARNING: undefined reference to function: atoi" WARNING.
This possibly means that atoi() function does not function correctly when KLEE is executed, i am not sure about it.
I dont know how to use KLEE in this case, but it is possible to generate integer arguments for the plus() function only, and this can solve this problem:
#include <stdio.h> int plus(int first){ if(first+2 == 4) return 1; return 0;} int main(int argc, char *argv[]){
int a; klee_make_symbolic(&a, sizeof(a), "a"); return plus(a); // return -1;} Then try it:
1) Create object file by:llvm-gcc --emit-llvm -c 2plus2.c 2) Generate test-cases:klee --posix-runtime 2plus2.o

This is not exactly that were needed, but, at least, should generate some reasonable output.
Urmas Repinski.
From: Aleksandr.Malyutin-O7H/y4DKl+***@public.gmane.org
To: klee-dev-AQ/***@public.gmane.org
Date: Thu, 10 Jul 2014 11:26:35 +0000
Subject: [klee-dev] Simple code for KLEE









Hi,

I tried to use klee on simple c-code example:


#include <stdio.h>

int plus(int first){
if(first+2 == 4)return 1;
return 0;
}

int main(int argc, char *argv[]){
if(argc == 2) return plus(atoi(*argv[1]));
return -1;
}

My steps were:
1)
Create object file by:
llvm-gcc --emit-llvm -c 2plus2.c

2)
Generate test-cases:
klee --posix-runtime 2plus2.o --sym-arg 1

KLEE: NOTE: Using model: /home/malyutin/klee/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/malyutin/klee/klee/examples/my_example/klee-out-0"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: atoi
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: __xstat64(1, 53487840, 53587488)
KLEE: WARNING ONCE: calling external: atoi(53548944)

KLEE: done: total instructions = 581
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

3)
After that I checked resulting test-case:
ktest-tool klee-last/test000001.ktest

ktest file : 'klee-last/test000001.ktest'
args : ['2plus2.o', '--sym-arg', '1']
num objects: 2
object 0: name: 'arg0'
object 0: size: 2
object 0: data: ' \x00'
object 1: name: 'model_version'
object 1: size: 4
object 1: data: '\x01\x00\x00\x00'

It’s simple to see that klee generates test-case for one of three branches. Maybe my code is incorrect or my method for generating test-cases is wrong, but all my attempts to get three test-cases for three branches of
my program were absolutely useless.

Help me please and say what I do wrong.

Many thanks,
Aleksander.