[klee-dev] a question about kleaver
Hi,
When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be
used at the same time.
the logic is simple:
if( sn > 5) {
if( sn < 8 ) {
if (sn==0) printf("hello");
}
}
the query is as follows:
array sn[4] : w32 -> w8 = symbolic
(query [(Ult 5
N0:(ReadLSB w8 0 sn))
(Ugt N0 8) ]
(Eq N0 0) [] [ sn ] )
it crashes the kleaver, but when I change the file to :
array sn[4] : w32 -> w8 = symbolic
(query [(Ult 5
N0:(ReadLSB w8 0 sn))
(Ult N0 8) ]
(Eq N0 0) [] [ sn ] )
=
it works normal.
could you tell me why ?
What is different between "Ugt" and "Ult", or I have made some mistake when
using kleaver?
Thanks.
Good Luck!
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] make all the variables in the program as symbolic
I think you could write a static analysis pass to find all the variables and then make them symbolic. But, why do you make the local variables symbolic ? At 2015-06-01 16:47:46, "张若虚" wrote: Dear All, My name is Eli and I just begin to use KLEE. I can use KLEE intrinsic function klee_make_symbolic() to make a variable as a symbolic. I am wondering that can I make all the variables (local variables, global variables) in the programs as symbolic? Is there a KLEE option to achieve that? Thank you :-) Eli___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] question about concolic execution using klee
Hi, all I used klee’s seed-mode and zesti to test in concolic mode. I thought it would execute the program and keep the path constraints with solving them. Because the seeds could tell which branch would be taken. But klee and zesti took much time to evaluate or solve conditions when I did some test whose symbolic input greater than 100 bytes. The test commands as follows: klee --libc=uclibc --posix-runtime -libz --start-debug-inst=0 --dump-func-trace --check-div-zero=false --check-overshift=false -xlib --lib-path=/home/xqx/test/libpng-test/libpng-1.2.4/libpng.bca --seed-out=/tmp/seed208.ktest -only-seed -named-seed-matching /home/xq x/test/libpng-test/test-libpng124/pngtest.bc /tmp/1.png --xqx-sym-file /tmp/1.png 0 104 2 (--xqx-sym-file to specify the symbolic file and data) Zesti-klee --zest --use-symbex=1 --symbex-for=10 --search=zest --zest-search-heuristic=br --zest-continue-after-error=true --libc=uclibc --posix-runtime -libz -emit-all-errors /home/xqx/test/libpng-test/test-libpng124/pngtest.bc /tmp/basn0g02.png I used klee to run “pngtest.bc /tmp/basn0g02.png”, it could complete in 68s, However, It could not run over when I use klee seed-mode or zesti in 20 hours. And I think it need not to solve the constraints when we have a seed. I have search the mail-list for the related discussions, but none has an answer. The related discussions as follows: https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2013-November/000488.html https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2013-November/000489.html https://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00680.html Did I run klee or zesti in wrong command? Could you give me some solution? Best Regards xqx ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] execute function with symbolic argument
Hi， I think it could be done well with klee if you only want run a function without complex memory accessing. and we have done some experiments. the challenges are : 1. how to handle the pointer argument , when it pointing to a structure. further more, if there are pointers in the structure. 2. how to address the globalvariables. may be more.. best regards xqx At 2014-12-20 23:33:28, "Hongxu Chen" wrote: Hi Dingbao, AFAIK, If you wanna make a memory location M symbolic, the only public API is klee_make_symbolic(FIRST_ADDR(M), SIZE(M), "specified_name"). If you simply make pointer P symbolic, that's exactly the same as a normal variable, i.e., klee_make_symbolic(&P, sizeof(P), "p"), which means that P's value is uncertain. However if you also need to deference it(in most of the cases you do), you've to make the pointed area symbolic rather than P itself; also notice that KLEE cannot make symbolic if the length of the pointed area is uncertain. Thanks and Regards, Hongxu On Sat, Dec 20, 2014 at 9:58 AM, Dingbao Xie wrote: Hi, everyone. I want to test functions of a program one by one with klee. It's easy to change the entry function of a program when using klee to execute it. But I don't know how to make the arguments of the function to be symbolic and the type of an argument may be pointer, struct etc. What's the easiest way to achieve that? Thanks in advance. -- Dingbao Xie ___ 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] a question about use klee with zcov
Hi, everyone I find some commands which using zcov to calculate code coverage in Makefile of Klee project , as follows: zcov-scan --look-up-dirs=1 klee.zcov . zcov-genhtml --root $$(pwd) klee.zcov klee-cov But I did not how to use it. I have used --write-cov to generate *.cov of testcases. and I make the target code(coreutils6.10) with gcc with -fprofile-arcs -ftest-coverage. How can I use these information to generate code coverage by zcov ? thanks Best Regards xqx ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
