[klee-dev] Symbolic Files
daniel at zuster.org
Mon Feb 8 23:41:20 PST 2010
On Sun, Feb 7, 2010 at 5:27 PM, lokesh agarwal
<lokesh.agarwal1986 at gmail.com> wrote:
> Hey everyone,
> I was trying to work out how exactly klee handles symbolic files.
> So i looked into the definition of the __fd_open() call stub, in
> This is what I could make out:
> The code tries to retrieve an unused file descriptor by scanning linearly.
> Then if a fd is found, it tries to see if the pathname provided in the
> argument actually exists. if so, it opens the system file and returns back.
> If not, then it tries to create a symbolic file.
> It does this by calling :
> syscall(__NR_open, __concretize_string(pathname), flags, mode);
> This call is failing. I am guessing that the reason for that is
> __concretize_string() is producing strings which cannot be valid filenames.
> I simply printfed this value. I am unable to find the definition of
> __concretize_string. Can anyone help me? Also, am I missing out something?
> Should I be doing something different to create symbolic files?
Are you using the klee_init_env code?
The basic scheme for symbolic files is to look for filenames which
*could* symbolically match a single character filename like "A", "B",
... for example, if the code tries to open "A" then it will get the
first symbolic file. The idea is that when the application tries to
open a file with a symbolic string, then the code will explore the
case when that string was "A".
The model is quite simple, but worked well enough for testing
coreutils. It needs a fair amount of work to extend to testing larger
Also, the code for __concretize_string is in POSIX/fd.c.
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
More information about the klee-dev