[klee-dev] KLEE symbolic file input

[Andrew Santosa]

I think an issue here is that there is no such thing as --sym-file option; there is only --sym-files.

klee --libc=uclibc --posix-runtime sock_simple.bc A --sym-files 1 1000

worked for me.

Best,
Andrew


On Wednesday, 21 June 2017, 1:05, Shehbaz Jaffer <shehbaz.jaffer at mail.utoronto.ca> wrote:



Thank you for your reply, I apologize if I am doing something glaringly wrong here. I am running KLEE version:

klee --version
KLEE 1.2.0 (https://klee.github.io)
LLVM (http://llvm.org/):
  LLVM version 3.4

from the docker image. here is simplified socket program with only the open command. I check the errno to make sure that there isn't a permission denied error. I get "No such file or directory" error:


program
-----------

int main(int argc, char *argv[])
{
        int sock;
        FILE *dev;
        long pos;
        char blocks[64];
        if ((sock = open(argv[1], O_RDONLY)) < 0) {
                printf("argv[1] assigned %s\n", argv[1]);
                printf("%s\n", strerror(errno));
                exit(1);
        }else { 
                printf ("PASS\n");
        }
}

command:
--------------
$ klee --libc=uclibc --posix-runtime sock_simple.bc A --sym-file 1000


Output:
----------
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/testfs/klee-out-9"
Using STP solver backend
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 61939712)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: printf(55322256, 52223600)
argv[1] assigned A
No such file or directory

KLEE: done: total instructions = 7610
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
-----------

A is assigned to argv[1] but it fails to open the file with "No such file or directory" error. Could I be missing some pre-required environment setup that makes sure the symbolic files A, B, C are accessible? If I pre-create a file A (which I do not think I should do), it only goes to else condition as expected as it is a concrete file which can be opened.

Thanks,
Shehbaz



________________________________

From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Cristian Cadar <c.cadar at imperial.ac.uk>
Sent: Tuesday, June 20, 2017 11:05 AM
To: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] KLEE symbolic file input 
 
Hi,

If you run instead
klee --libc=uclibc --posix-runtime sock.bc A --sym-file 1000

the test should behave as expected.

As briefly documented at 
http://klee.github.io/docs/options/#symbolic-environment, the symbolic 
files are called A, B, C, etc.

Best,
Cristian


On 20/06/17 14:26, Shehbaz Jaffer wrote:
> Hello!
>
> I have looked at previous discussions on symbolic file inputs [1][2][3], but I am unable to run an example for how KLEE could be run for symbolic file inputs.
> Please consider the sample program which opens a file, seeks to start of file, reads 64 bytes of data, and seeks back to start of file, and then exits.
>
> int main(int argc, char *argv[])
> {
>         int sock;
>         FILE *dev;
>         long pos;
>         char blocks[64];
>         if ((sock = open(argv[1], O_RDWR)) < 0) {
>         // tried replacing argv[1] with 'A', 'A-data'
>         // but none seem to work?
>                 EXIT("open failed\n");
>         }else if((dev = fdopen(sock, "r+")) == NULL){
>                 EXIT("open read mode failed\n");
>         }
>         if ((pos = ftell(dev)) < 0) {
>                 EXIT("ftell");
>         }
>         if (fseek(dev,  0 , SEEK_SET) < 0) {
>                 EXIT("fseek");
>         }
>         if (fread(blocks, 64, 1 , dev) != 1) {
>                 EXIT("freed");
>         }
>         if (fseek(dev, pos, SEEK_SET) < 0) {
>                 EXIT("fseek");
>         }
>         printf ("PASS\n");
> }
>
> If I run the program with a concrete file input:
>
> ./sock /tmp/testfile
> OUTPUT: PASS
>
> However, if I try KLEE with --sym-file argument:
> klee --libc=uclibc --posix-runtime sock.bc --sym-file 1000
>
> KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 52082608)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: calling external: printf(52815248, 47655712)
> open failed // OPEN FAILS!!
> KLEE: done: total instructions = 6402
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
> I have also looked at POSIX/runtime/fd_init.c and it looks like a symbolic file "A-data" is created (for 1 symbolic file) but the contents of the file are malloc'ed and marked symbolic using klee_mark_symbolic on a fixed sized in-memory buffer of size specified
by user. The actual file is not created on disk.  Is this the reason why a call to open() of argv[1] fails? What is the alternative method to ensure argv[1] corresponds to symbolic file created using --symfile 1000 option? I also tried instrumenting code and
replacing argv[1] with "A" and "A-data". Still, open call fails and KLEE does not successfully execute open command.
>
> Thanks and Regards,
> Shehbaz
>
> [1] http://mailman.ic.ac.uk/pipermail/klee-dev/2013-April/000156.html
> [2] https://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html
> [3] http://klee-dev.keeda.stanford.narkive.com/5t9M1H0i/symbolic-file-inputs
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev