[klee-dev] KLEE symbolic file input
Shehbaz Jaffer
shehbaz.jaffer at mail.utoronto.ca
Wed Jun 21 02:15:16 BST 2017
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 <asantosa1999 at gmail.com>
Sent: Tuesday, June 20, 2017 9:05:30 PM
To: Shehbaz Jaffer; Cristian Cadar; klee-dev at 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.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
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list