Re: [klee-dev] Test cases generated for symbolic file
Thanks Sang. I hope to find time to write the tests to make codecov happy. Andrew On Saturday, 23 June 2018, 2:33:20 pm GMT+8, Sang Phan wrote: Hi Andrew, I only build the tool for my own task, and I don't intend to submit a PR, so please go ahead with yours. Sang On Fri, Jun 22, 2018 at 9:32 PM, Andrew Santosa wrote: > Hi Sang, > > I urgently need a tool like you mentioned, so I wrote one myself within KLEE > source tree. You can find the source as tools/gen-bout.cpp in the gen-bout > branch > of my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout > > I don't exactly know the answer to your question. For normal files, I get > the stat from the > actual files whose contents are loaded into the symbolic files. For stdin > and stdout, > I get the stats using fstat64 of file descriptors 0 and 1, respectively. > > I think model_version is mandatory if one wants to use the produced file as > a seed. > > I had submitted PR 917 > https://github.com/klee/klee/pull/917 > > But probably this PR will not pass the CI tests since I had not added the > tests. > I will also close it now since you publicly announced your tool first. > > Best, > Andrew > > On Saturday, 23 June 2018, 1:13:31 am GMT+8, Sang Phan > wrote: > > > Thanks Cristian. > > I want to feed KLEE with my customized seeds, instead of random ones. > So I need a tool similar to gen-random-bout to generate .ktest file. > To write such a tool, I would like to know how to generate the stat > and model-version > > Here is my quick implementation: > https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp > + stat is generated randomly, copied from to gen-random-bout > + model version is always set to 1 > > It seems to work just fine right now. But as both stat and > model-version appear in the path condition, is there any possible > problem with this settings? > > Best, > Sang > > > On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar > wrote: >> Hi, you can ignore the model_version, it just keeps track of the version >> for >> the POSIX model. The stat buffer keeps the stat info associated with the >> file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you >> have time, it would be useful to document this on the website (e.g., at >> http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at >> https://github.com/klee/klee.github.io >> >> Best, >> Cristian >> >> >> On 21/06/18 21:55, Sang Phan wrote: >>> >>> Hello, >>> >>> I'm trying to understand the test cases generated when the input is >>> symbolic file. >>> For the password example under this link: >>> https://klee.github.io/tutorials/using-symbolic/, a test case viewed >>> by ktest-tool is the following: >>> >>> https://klee.github.io/tutorials/using-symbolic/ >>> >>> >>> ktest file : 'test04.ktest' >>> args : ['password.bc', 'A', '-sym-files', '1', '10'] >>> num objects: 3 >>> object 0: name: b'A-data' >>> object 0: size: 10 >>> object 0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' >>> object 1: name: b'A-data-stat' >>> object 1: size: 144 >>> object 1: data: >>> >>> >>> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' >>> object 2: name: b'model_version' >>> object 2: size: 4 >>> object 2: data: b'\x01\x00\x00\x00' >>> >>> + I understand A-data is the content of the file, but what is >>> A-data-stat and model-version? >>> + From the gen-random-bout, it seems data-stat can be generated >>> randomly, but how about model-version? >>> >>> Thanks, >>> Sang >>> >>> ___ >>> 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
Re: [klee-dev] Test cases generated for symbolic file
Hi Andrew, I only build the tool for my own task, and I don't intend to submit a PR, so please go ahead with yours. Sang On Fri, Jun 22, 2018 at 9:32 PM, Andrew Santosa wrote: > Hi Sang, > > I urgently need a tool like you mentioned, so I wrote one myself within KLEE > source tree. You can find the source as tools/gen-bout.cpp in the gen-bout > branch > of my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout > > I don't exactly know the answer to your question. For normal files, I get > the stat from the > actual files whose contents are loaded into the symbolic files. For stdin > and stdout, > I get the stats using fstat64 of file descriptors 0 and 1, respectively. > > I think model_version is mandatory if one wants to use the produced file as > a seed. > > I had submitted PR 917 > https://github.com/klee/klee/pull/917 > > But probably this PR will not pass the CI tests since I had not added the > tests. > I will also close it now since you publicly announced your tool first. > > Best, > Andrew > > On Saturday, 23 June 2018, 1:13:31 am GMT+8, Sang Phan > wrote: > > > Thanks Cristian. > > I want to feed KLEE with my customized seeds, instead of random ones. > So I need a tool similar to gen-random-bout to generate .ktest file. > To write such a tool, I would like to know how to generate the stat > and model-version > > Here is my quick implementation: > https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp > + stat is generated randomly, copied from to gen-random-bout > + model version is always set to 1 > > It seems to work just fine right now. But as both stat and > model-version appear in the path condition, is there any possible > problem with this settings? > > Best, > Sang > > > On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar > wrote: >> Hi, you can ignore the model_version, it just keeps track of the version >> for >> the POSIX model. The stat buffer keeps the stat info associated with the >> file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you >> have time, it would be useful to document this on the website (e.g., at >> http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at >> https://github.com/klee/klee.github.io >> >> Best, >> Cristian >> >> >> On 21/06/18 21:55, Sang Phan wrote: >>> >>> Hello, >>> >>> I'm trying to understand the test cases generated when the input is >>> symbolic file. >>> For the password example under this link: >>> https://klee.github.io/tutorials/using-symbolic/, a test case viewed >>> by ktest-tool is the following: >>> >>> https://klee.github.io/tutorials/using-symbolic/ >>> >>> >>> ktest file : 'test04.ktest' >>> args : ['password.bc', 'A', '-sym-files', '1', '10'] >>> num objects: 3 >>> object0: name: b'A-data' >>> object0: size: 10 >>> object0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' >>> object1: name: b'A-data-stat' >>> object1: size: 144 >>> object1: data: >>> >>> >>> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' >>> object2: name: b'model_version' >>> object2: size: 4 >>> object2: data: b'\x01\x00\x00\x00' >>> >>> + I understand A-data is the content of the file, but what is >>> A-data-stat and model-version? >>> + From the gen-random-bout, it seems data-stat can be generated >>> randomly, but how about model-version? >>> >>> Thanks, >>> Sang >>> >>> ___ >>> 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
Re: [klee-dev] Test cases generated for symbolic file
Hi Sang, I urgently need a tool like you mentioned, so I wrote one myself within KLEEsource tree. You can find the source as tools/gen-bout.cpp in the gen-bout branchof my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout I don't exactly know the answer to your question. For normal files, I get the stat from theactual files whose contents are loaded into the symbolic files. For stdin and stdout,I get the stats using fstat64 of file descriptors 0 and 1, respectively. I think model_version is mandatory if one wants to use the produced file as a seed. I had submitted PR 917https://github.com/klee/klee/pull/917 But probably this PR will not pass the CI tests since I had not added the tests.I will also close it now since you publicly announced your tool first. Best,Andrew On Saturday, 23 June 2018, 1:13:31 am GMT+8, Sang Phan wrote: Thanks Cristian. I want to feed KLEE with my customized seeds, instead of random ones. So I need a tool similar to gen-random-bout to generate .ktest file. To write such a tool, I would like to know how to generate the stat and model-version Here is my quick implementation: https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp + stat is generated randomly, copied from to gen-random-bout + model version is always set to 1 It seems to work just fine right now. But as both stat and model-version appear in the path condition, is there any possible problem with this settings? Best, Sang On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar wrote: > Hi, you can ignore the model_version, it just keeps track of the version for > the POSIX model. The stat buffer keeps the stat info associated with the > file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you > have time, it would be useful to document this on the website (e.g., at > http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at > https://github.com/klee/klee.github.io > > Best, > Cristian > > > On 21/06/18 21:55, Sang Phan wrote: >> >> Hello, >> >> I'm trying to understand the test cases generated when the input is >> symbolic file. >> For the password example under this link: >> https://klee.github.io/tutorials/using-symbolic/, a test case viewed >> by ktest-tool is the following: >> >> https://klee.github.io/tutorials/using-symbolic/ >> >> >> ktest file : 'test04.ktest' >> args : ['password.bc', 'A', '-sym-files', '1', '10'] >> num objects: 3 >> object 0: name: b'A-data' >> object 0: size: 10 >> object 0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' >> object 1: name: b'A-data-stat' >> object 1: size: 144 >> object 1: data: >> >> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' >> object 2: name: b'model_version' >> object 2: size: 4 >> object 2: data: b'\x01\x00\x00\x00' >> >> + I understand A-data is the content of the file, but what is >> A-data-stat and model-version? >> + From the gen-random-bout, it seems data-stat can be generated >> randomly, but how about model-version? >> >> Thanks, >> Sang >> >> ___ >> 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
Re: [klee-dev] Test cases generated for symbolic file
Thanks Cristian. I want to feed KLEE with my customized seeds, instead of random ones. So I need a tool similar to gen-random-bout to generate .ktest file. To write such a tool, I would like to know how to generate the stat and model-version Here is my quick implementation: https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp + stat is generated randomly, copied from to gen-random-bout + model version is always set to 1 It seems to work just fine right now. But as both stat and model-version appear in the path condition, is there any possible problem with this settings? Best, Sang On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar wrote: > Hi, you can ignore the model_version, it just keeps track of the version for > the POSIX model. The stat buffer keeps the stat info associated with the > file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you > have time, it would be useful to document this on the website (e.g., at > http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at > https://github.com/klee/klee.github.io > > Best, > Cristian > > > On 21/06/18 21:55, Sang Phan wrote: >> >> Hello, >> >> I'm trying to understand the test cases generated when the input is >> symbolic file. >> For the password example under this link: >> https://klee.github.io/tutorials/using-symbolic/, a test case viewed >> by ktest-tool is the following: >> >> https://klee.github.io/tutorials/using-symbolic/ >> >> >> ktest file : 'test04.ktest' >> args : ['password.bc', 'A', '-sym-files', '1', '10'] >> num objects: 3 >> object0: name: b'A-data' >> object0: size: 10 >> object0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' >> object1: name: b'A-data-stat' >> object1: size: 144 >> object1: data: >> >> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' >> object2: name: b'model_version' >> object2: size: 4 >> object2: data: b'\x01\x00\x00\x00' >> >> + I understand A-data is the content of the file, but what is >> A-data-stat and model-version? >> + From the gen-random-bout, it seems data-stat can be generated >> randomly, but how about model-version? >> >> Thanks, >> Sang >> >> ___ >> 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
Re: [klee-dev] Test cases generated for symbolic file
Hi, you can ignore the model_version, it just keeps track of the version for the POSIX model. The stat buffer keeps the stat info associated with the file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you have time, it would be useful to document this on the website (e.g., at http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at https://github.com/klee/klee.github.io Best, Cristian On 21/06/18 21:55, Sang Phan wrote: Hello, I'm trying to understand the test cases generated when the input is symbolic file. For the password example under this link: https://klee.github.io/tutorials/using-symbolic/, a test case viewed by ktest-tool is the following: https://klee.github.io/tutorials/using-symbolic/ ktest file : 'test04.ktest' args : ['password.bc', 'A', '-sym-files', '1', '10'] num objects: 3 object0: name: b'A-data' object0: size: 10 object0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' object1: name: b'A-data-stat' object1: size: 144 object1: data: b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' object2: name: b'model_version' object2: size: 4 object2: data: b'\x01\x00\x00\x00' + I understand A-data is the content of the file, but what is A-data-stat and model-version? + From the gen-random-bout, it seems data-stat can be generated randomly, but how about model-version? Thanks, Sang ___ 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
