[klee-dev] make reading from file symbolic

[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 at imperial.ac.uk
To: urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk

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 at hotmail.com> 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






 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed