Thank you! This worked for me as well. I apologize and I will read man pages more thoroughly before sending my next mail to this list.
Regards, Shehbaz ________________________________ From: Andrew Santosa <asantosa1...@gmail.com> Sent: Tuesday, June 20, 2017 9:05:30 PM To: Shehbaz Jaffer; Cristian Cadar; klee-dev@imperial.ac.uk Subject: Re: [klee-dev] KLEE symbolic file input 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.jaf...@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-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on behalf of Cristian Cadar <c.ca...@imperial.ac.uk> Sent: Tuesday, June 20, 2017 11:05 AM To: klee-dev@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@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
