make reading from file symbolic

[Urmas Repinski]

Hello.

I have some program, named schedule.c, that i want symbolically evaluate using klee, to generate inputs.

Inside the program i have some fscanf(stdin, "%d", &command) comes, and with "%f" argument also.

I want to make this command variable symbolic, no difference to generate symbolic input file for it, ot to make it as usual variable and to generate inputs.

When i compile the code with llvm-gcc, then compilation is success and .o file is generated.

But when i execute .o file using klee -

klee schedule.o

I get :

KLEE: WARNING: undefined reference to function:
__isoc99_fscanf
KLEE: WARNING: undefined reference to variable: stdin
KLEE: WARNING ONCE: calling external:
__isoc99_fscanf(140528011303360, 51367536, 51252160)

and no inputs is generated, execution stops.

Obviously necessary to replace the reading from stdin by --sym-files parameters, but if i add

klee schedule.o --sym-files 0 20

0 - means that no addition files needed, stdin only, and 20 some arbitrary number, size of data.

When i hit Ctrl+C then 5 inputs are generated, but not in this variables what i want.

Please suggest any possible parameters combination, i think to avoid warnings necessary to remove fscanf from original code, but in this case klee will not know what variables to make symbolic.....

Urmas Repinski

[Daniel Liew]

Hi Urmas,

Are you running the posix runtime (--posix-runtime)? Without the POSIX
runtime the following does not work..

$ klee thing.o --help
KLEE: output directory = "klee-out-12"

KLEE: done: total instructions = 37
KLEE: done: completed paths = 3

where as with the POSIX runtime...

$ klee --posix-runtime thing.o --help
KLEE: NOTE: Using model:
/data/dev/KLEE/klee/bin/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-13"
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: ERROR: /data/dev/KLEE/klee/src/runtime/POSIX/klee_init_env.c:24:
klee_init_env

usage: (klee_init_env) [options] [program arguments]
-sym-arg <N> - Replace by a symbolic argument with length N
-sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
MAX arguments, each with maximum length N
-sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
with maximum size N.
-sym-stdout - Make stdout symbolic.
-max-fail <N> - Allow up to <N> injected failures
-fd-fail - Shortcut for '-max-fail 1'


KLEE: NOTE: now ignoring this error at this location

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

It might be the case that the -sym-arg family of options does not work
without POSIX run time being enabled (although I'm not sure).

Regards,
Dan Liew.


On 19 April 2013 07:06, Urmas Repinski <urrimus-***@public.gmane.org> wrote:

> Hello.
>
> I have some program, named schedule.c, that i want symbolically evaluate
> using klee, to generate inputs.
>
> Inside the program i have some fscanf(stdin, "%d", &command) comes, and
> with "%f" argument also.
>
> I want to make this command variable symbolic, no difference to generate
> symbolic input file for it, ot to make it as usual variable and to generate
> inputs.
>
> When i compile the code with llvm-gcc, then compilation is success and .o
> file is generated.
>
> But when i execute .o file using klee -
>
> klee schedule.o
>
> I get :
>
> KLEE: WARNING: undefined reference to function:
__isoc99_fscanf
> KLEE: WARNING: undefined reference to variable: stdin
> KLEE: WARNING ONCE: calling external:
__isoc99_fscanf(140528011303360,
> 51367536, 51252160)
>
> and no inputs is generated, execution stops.
>
> Obviously necessary to replace the reading from stdin by --sym-files
> parameters, but if i add
>
> klee schedule.o --sym-files 0 20
>
> 0 - means that no addition files needed, stdin only, and 20 some arbitrary
> number, size of data.
>
> When i hit Ctrl+C then 5 inputs are generated, but not in this variables
> what i want.
>
> Please suggest any possible parameters combination, i think to avoid
> warnings necessary to remove fscanf from original code, but in this case
> klee will not know what variables to make symbolic.....
>
> Urmas Repinski
>

[Urmas Repinski]

Hi Dan.

I have markable progress, but klee does not work still.

I am using now
klee -libc=uclibc -posix-runtime schedule.o --sym-files 0 10

but, accourding to the tutorial (http://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html), i can use
klee -libc=uclibc -posix-runtime schedule.o A --sym-files 1 10
and to use file, whose name is in args[1], instead of stdin.

But lets check first case.

I setted klee_warning_once("w1") before fscanf(stdin, ...) call and klee_warning_once("w2") after fscanf(stdin, ...) call.

As the result i have following output:

klee -libc=uclibc -posix-runtime schedule.o --sym-files 0 10
KLEE: NOTE: Using model: /home/urmas/forensic/thirdparty-install/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-55"
KLEE: WARNING: undefined reference to function:
__isoc99_fscanf
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 53277392)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: __user_main: w1
KLEE: WARNING ONCE: calling external:
__isoc99_fscanf(53164400, 53153200, 53453008)


And execution halts at the fscanf statement again.

I think i installed uclibc correctly, as it were necessary to do in http://klee.llvm.org/GetStarted.html but if problem can be in uclibc installation i can try to reinstall it, but i am not sure.

The problem is in the same statement as before.

Urmas Repinski.


Date: Fri, 19 Apr 2013 10:49:34 +0100
Subject: Re: [klee-dev] make reading from file symbolic
From: daniel.liew-AQ/***@public.gmane.org
To: urrimus-***@public.gmane.org
CC: klee-dev-AQ/***@public.gmane.org

Hi Urmas,

Are you running the posix runtime (--posix-runtime)? Without the POSIX runtime the following does not work..

$ klee thing.o --help
KLEE: output directory = "klee-out-12"


KLEE: done: total instructions = 37
KLEE: done: completed paths = 3

where as with the POSIX runtime...

$ klee --posix-runtime thing.o --help
KLEE: NOTE: Using model: /data/dev/KLEE/klee/bin/Release+Asserts/lib/libkleeRuntimePOSIX.bca

KLEE: output directory = "klee-out-13"
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: ERROR: /data/dev/KLEE/klee/src/runtime/POSIX/klee_init_env.c:24: klee_init_env

usage: (klee_init_env) [options] [program arguments]

-sym-arg <N> - Replace by a symbolic argument with length N
-sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
MAX arguments, each with maximum length N

-sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
with maximum size N.
-sym-stdout - Make stdout symbolic.
-max-fail <N> - Allow up to <N> injected failures

-fd-fail - Shortcut for '-max-fail 1'


KLEE: NOTE: now ignoring this error at this location

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


It might be the case that the -sym-arg family of options does not work without POSIX run time being enabled (although I'm not sure).

Regards,
Dan Liew.



On 19 April 2013 07:06, Urmas Repinski <urrimus-***@public.gmane.org> wrote:







Hello.



I have some program, named schedule.c, that i want symbolically evaluate using klee, to generate inputs.



Inside the program i have some fscanf(stdin, "%d", &command) comes, and with "%f" argument also.



I want to make this command variable symbolic, no difference to generate symbolic input file for it, ot to make it as usual variable and to generate inputs.



When i compile the code with llvm-gcc, then compilation is success and .o file is generated.



But when i execute .o file using klee -



klee schedule.o



I get :



KLEE: WARNING: undefined reference to function:
__isoc99_fscanf

KLEE: WARNING: undefined reference to variable: stdin

KLEE: WARNING ONCE: calling external:
__isoc99_fscanf(140528011303360, 51367536, 51252160)



and no inputs is generated, execution stops.



Obviously necessary to replace the reading from stdin by --sym-files parameters, but if i add



klee schedule.o --sym-files 0 20



0 - means that no addition files needed, stdin only, and 20 some arbitrary number, size of data.



When i hit Ctrl+C then 5 inputs are generated, but not in this variables what i want.



Please suggest any possible parameters combination, i think to avoid warnings necessary to remove fscanf from original code, but in this case klee will not know what variables to make symbolic.....




Urmas Repinski