Re: [klee-dev] Symbolic input b'\x00'
Hi Yuanfei, Please have a look at the end of https://klee.github.io/tutorials/testing-function/ , it should describe what you need. Thanks On Tue, Nov 13, 2018, 22:52 Yuanfei Bi Hi, all, > > I run klee and got following result from ktest-tool: > > object1: name: b'arg0' > object1: size: 41 > object1: data: > b'\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\x00\x00\x00\x00\x00' > > I think the \x00 means null, how can I pass this parameter to > uninstrumented program to reproduce the desired behavior? > > Thanks. > > Yuanfei > ___ > 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] Possibly incorrect models generated
Hi,
Thanks for you reply. So in the file I can only see information about the
conditions encountered? If the assignment are not tracked how is it
possible to understand which value can a variable assume at the end of the
path? For example I don't how I could verify if another, for instance, can
be 9 (or any other value) athe end of ktest3.
Thanks
On Sat, Nov 10, 2018, 20:29 Frank Busse Hi,
>
>
> On Sat, 10 Nov 2018 07:07:13 +
> Alberto Barbaro wrote:
>
> > I feel I'm missing something because, for instance, I cannot see the
> > case where a = 0 and another = 12.
>
> That's the 2nd if statement:
>
> | if ( a == 77 ) { // a=77, another=?[0] = ktest 1
> | } else { // (a!=77)
> | if ( another == 12 ) { // a!=77[0], another=12 = ktest 3
> | } else { // a!=77[0], another!=12[0] = ktest 2
>
> Seems fine to me (values generated by solver in brackets).
>
>
> Kind regards,
>
> Frank
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Possibly incorrect models generated
Hi all,
I'm generating the .smt2 file for the following simple c program:
#include
int main() {
int a;
int another;
klee_make_symbolic(, sizeof(a), "a");
klee_make_symbolic(, sizeof(another), "another");
if ( a == 77 ) {
a += 6;
another = 5;
} else {
a = 9;
if ( another == 12 ) {
a += 7;
} else {
a += 10;
}
}
return 0;
}
I can compile it using clang -I ../../include -emit-llvm -c -g simple.c and
obtain the .smt2 running klee -write-smt2s simple.bc. At this point I would
like to see the model for the 3 test case and I have the following results:
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test01.ktest
ktest file : 'klee-last/test01.ktest'
args : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 77
object1: name: b'another'
object1: size: 4
object1: data: 0
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test02.ktest
ktest file : 'klee-last/test02.ktest'
args : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 0
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test03.ktest
ktest file : 'klee-last/test03.ktest'
args : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 12
I feel I'm missing something because, for instance, I cannot see the case
where a = 0 and another = 12.
Can you help me to understand if the models are correct and why?
Thanks
Alberto
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Inline assembly not supported
Hi all, I was able to compile httpd but unfortunately I cannot really execute it because the sockets are not really supported. I've seen that also someone else had the same problem a while ago. In my opinion, this is an important issue because sockets are everywhere... What's your view on that? Any plan to fix it? Thanks ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to remove the current state from states?
Thanks Frank, ASAP I'll try to use the approach you suggest and if working fine I could submit a PR if for you is OK. Thanks Il giorno lun 29 ott 2018 alle ore 16:00 Frank Busse < f.buss...@imperial.ac.uk> ha scritto: > Hi Alberto, > > > On Mon, 29 Oct 2018 14:21:28 + > Alberto Barbaro wrote: > > > Thanks for your email I've seen that the BaseSearcher has 2 utility > > functions for adding and removing a state. Since I'm working on a > searcher, > > if I don't add the states in added states() into states() it'd be like > > remove them isn't it? > > if you don't add the states in addedStates to your local (in your > searcher) state set, they still exist (Executor::states) but you won't > select() them. This has two disadvantages: > > 1.) you'll waste resources > 2.) the main loop won't terminate (see Executor::run) > > > Kind regards, > > Frank > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to remove the current state from states?
Hi Frank, Thanks for your email I've seen that the BaseSearcher has 2 utility functions for adding and removing a state. Since I'm working on a searcher, if I don't add the states in added states() into states() it'd be like remove them isn't it? Thanks On Mon, Oct 29, 2018, 11:57 Frank Busse wrote: > Hi Alberto, > > > On Fri, 26 Oct 2018 13:41:45 +0100 > Alberto Barbaro wrote: > > > I'm on a searcher and I would like to remove the current state from > states. > > Should I added it to removedStates or do something else? Can I have the > > example one line code if not too much? > > to gracefully shut down a state in Executor you have to call one > of the terminate functions and afterwards call updateStates() to notify > the searchers. The resp. state is added to removedStates automatically > in terminateState() and removedStates is only used to forward the > information to the searchers. Currently there is no clean way to > terminate a state in a searcher (we discussed that internally a while > ago). What you could do is: > > - initialise your searcher with a reference to the executor or > - mark the state (or return tuple in select() etc.) and adapt the main > interpreter loop (select/delete until un-marked state found) > > The 2nd option is less error-prone. > > > Kind regards, > > Frank > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] How to remove the current state from states?
Hi all, I'm on a searcher and I would like to remove the current state from states. Should I added it to removedStates or do something else? Can I have the example one line code if not too much? Thanks ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Guided Search - Help
Hi Andrew, I checked again and the number of completed of paths is not set to 1. Even after few seconds it is set to 4. In my opinion this is due to the fact that the input is symbolic so in case of an if with symbolic path, as expected, multiple paths may be followed. Isn't it? This is why my main goal is to have a searcher that follows specifically one path based on the image passed to pngpixel in the first instance. I'm working on it but for now it does not work properly. Thanks Il giorno sab 20 ott 2018 alle ore 16:16 Andrew Santosa < asantosa1...@gmail.com> ha scritto: > Hi Alberto, > > KLEE prints the number of tests and paths at the end of its run, but this > is not shown in your log. With the options that you provided KLEE with > (-only-replay-seeds) and with only one seed (png-files-download.bout), I > expect the number of paths to be 1, in which case only one path is > traversed. > > Best, > Andrew > > Sent from Yahoo Mail on Android > <https://go.onelink.me/107872968?pid=InProduct=Global_Internal_YGrowth_AndroidEmailSig__AndroidUsers_wl=ym_sub1=Internal_sub2=Global_YGrowth_sub3=EmailSignature> > > On Sat, Oct 20, 2018 at 6:30 PM, Alberto Barbaro > wrote: > Hi Andrew, > Thanks a lot. I understand now, so it would follow all the paths because > the input is symbolic. > > In my mind I would like to have a searcher that would follow only and only > one path with symbolic data. This path should be generated with a concrete > file. This is I'm working on a searcher but I cannot do it properly for now. > > Thanks > > On Sat, Oct 20, 2018, 09:58 Andrew Santosa wrote: > > Hi Alberto, > > Please keep in mind that, although KLEE still tries to follow the seed's > path, the state it maintains is no longer > the concrete state, but the symbolic state. So, the symbolic file A no > longer contains a concrete RGB value at coordinate > (1, 1), but instead a symbolic value. By looking at the log you sent, > especially the following lines, this symbolic value could > have been concretized by KLEE into a value you were not expecting. > > KLEE: WARNING ONCE: silently concretizing (reason: floating point) > expression (Select w32 (Slt 4294967295 > N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8 > 55 A-data)) > 16) > (Shl w32 (ZExt w32 (Read w8 > 54 A-data)) > 24)) > (Shl w32 (ZExt w32 (Read w8 56 > A-data)) > 8)) > (ZExt w32 (Read w8 57 A-data > N0 > 4294967295) to value 541597261 > (/home/klee/target/libpng-1.6.35/png.c:3371) > > Best, > Andrew > On Saturday, 20 October 2018, 1:51:56 AM GMT+8, Alberto Barbaro < > barbaro.albe...@gmail.com> wrote: > > > Hi all, > I think we are getting there but I'm still missing something. So I was > able to generate pngpixel.bc and successfully use it. My next step was to > generate the seed an I used the following command: > > gen-bout --sym-file ../images/png-files-download.png && mv file.bout > png-files-download.bout > > Now, as suggested, I have used that seed with klee: > > klee@a8a6399e6799:~/seeds$ time klee -only-seed > -seed-out=png-files-download.bout -only-replay-seeds --posix-runtime > -libc=uclibc ../target/libpng-1.6.35/contrib/examples/pngpixel.bc 1 1 A > --sym-files 1 89760 > KLEE: NOTE: Using klee-uclibc : > /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca > KLEE: NOTE: Using POSIX model: > /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca > KLEE: output directory is > "/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41" > KLEE: Using STP solver backend > KLEE: WARNING: undefined reference to function: floor > KLEE: WARNING: undefined reference to function: modf > KLEE: WARNING: undefined reference to function: pow > KLEE: KLEE: using 1 seeds > > KLEE: 1 seeds remaining over: 1 states > KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at > /home/klee/klee-gen-bout/runtime/POSIX/fd.c:980 > KLEE: WARNING ONCE: calling __user_main with extra arguments. > KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not > modelled. Using alignment of 8. > KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model > KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: > MO504[8192] allocated at global:crc_table > KLEE: 1 seeds remaining over: 1 states > KLEE: 1 seeds remaining over: 1 states > KLE
Re: [klee-dev] Guided Search - Help
Hi Andrew, Thanks a lot. I understand now, so it would follow all the paths because the input is symbolic. In my mind I would like to have a searcher that would follow only and only one path with symbolic data. This path should be generated with a concrete file. This is I'm working on a searcher but I cannot do it properly for now. Thanks On Sat, Oct 20, 2018, 09:58 Andrew Santosa wrote: > Hi Alberto, > > Please keep in mind that, although KLEE still tries to follow the seed's > path, the state it maintains is no longer > the concrete state, but the symbolic state. So, the symbolic file A no > longer contains a concrete RGB value at coordinate > (1, 1), but instead a symbolic value. By looking at the log you sent, > especially the following lines, this symbolic value could > have been concretized by KLEE into a value you were not expecting. > > KLEE: WARNING ONCE: silently concretizing (reason: floating point) > expression (Select w32 (Slt 4294967295 > N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8 > 55 A-data)) > 16) > (Shl w32 (ZExt w32 (Read w8 > 54 A-data)) > 24)) > (Shl w32 (ZExt w32 (Read w8 56 > A-data)) > 8)) > (ZExt w32 (Read w8 57 A-data > N0 > 4294967295) to value 541597261 > (/home/klee/target/libpng-1.6.35/png.c:3371) > > Best, > Andrew > On Saturday, 20 October 2018, 1:51:56 AM GMT+8, Alberto Barbaro < > barbaro.albe...@gmail.com> wrote: > > > Hi all, > I think we are getting there but I'm still missing something. So I was > able to generate pngpixel.bc and successfully use it. My next step was to > generate the seed an I used the following command: > > gen-bout --sym-file ../images/png-files-download.png && mv file.bout > png-files-download.bout > > Now, as suggested, I have used that seed with klee: > > klee@a8a6399e6799:~/seeds$ time klee -only-seed > -seed-out=png-files-download.bout -only-replay-seeds --posix-runtime > -libc=uclibc ../target/libpng-1.6.35/contrib/examples/pngpixel.bc 1 1 A > --sym-files 1 89760 > KLEE: NOTE: Using klee-uclibc : > /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca > KLEE: NOTE: Using POSIX model: > /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca > KLEE: output directory is > "/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41" > KLEE: Using STP solver backend > KLEE: WARNING: undefined reference to function: floor > KLEE: WARNING: undefined reference to function: modf > KLEE: WARNING: undefined reference to function: pow > KLEE: KLEE: using 1 seeds > > KLEE: 1 seeds remaining over: 1 states > KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at > /home/klee/klee-gen-bout/runtime/POSIX/fd.c:980 > KLEE: WARNING ONCE: calling __user_main with extra arguments. > KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not > modelled. Using alignment of 8. > KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model > KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: > MO504[8192] allocated at global:crc_table > KLEE: 1 seeds remaining over: 1 states > KLEE: 1 seeds remaining over: 1 states > KLEE: WARNING ONCE: silently concretizing (reason: floating point) > expression (Select w32 (Slt 4294967295 > N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8 > 55 A-data)) > 16) > (Shl w32 (ZExt w32 (Read w8 > 54 A-data)) > 24)) > (Shl w32 (ZExt w32 (Read w8 56 > A-data)) > 8)) > (ZExt w32 (Read w8 57 A-data > N0 > 4294967295) to value 541597261 > (/home/klee/target/libpng-1.6.35/png.c:3371) > KLEE: WARNING: seeds patched for violating constraint > KLEE: WARNING ONCE: calling external: floor(4621195801218788662) at > /home/klee/target/libpng-1.6.35/png.c:3375 > KLEE: 1 seeds remaining over: 1 states > KLEE: WARNING ONCE: calling external: vprintf(146758144, 154438432) at > /home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:35 > > libpng warning: : gamma value does not match sRGB > > From my initial understanding now klee should follow only one path but i > feel that is not the case because at this po
Re: [klee-dev] Guided Search - Help
Hi all, I think we are getting there but I'm still missing something. So I was able to generate pngpixel.bc and successfully use it. My next step was to generate the seed an I used the following command: gen-bout --sym-file ../images/png-files-download.png && mv file.bout png-files-download.bout Now, as suggested, I have used that seed with klee: klee@a8a6399e6799:~/seeds$ time klee -only-seed -seed-out=png-files-download.bout -only-replay-seeds --posix-runtime -libc=uclibc ../target/libpng-1.6.35/contrib/examples/pngpixel.bc 1 1 A --sym-files 1 89760 KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca KLEE: NOTE: Using POSIX model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: floor KLEE: WARNING: undefined reference to function: modf KLEE: WARNING: undefined reference to function: pow KLEE: KLEE: using 1 seeds KLEE: 1 seeds remaining over: 1 states KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at /home/klee/klee-gen-bout/runtime/POSIX/fd.c:980 KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8. KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: MO504[8192] allocated at global:crc_table KLEE: 1 seeds remaining over: 1 states KLEE: 1 seeds remaining over: 1 states KLEE: WARNING ONCE: silently concretizing (reason: floating point) expression (Select w32 (Slt 4294967295 N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8 55 A-data)) 16) (Shl w32 (ZExt w32 (Read w8 54 A-data)) 24)) (Shl w32 (ZExt w32 (Read w8 56 A-data)) 8)) (ZExt w32 (Read w8 57 A-data N0 4294967295) to value 541597261 (/home/klee/target/libpng-1.6.35/png.c:3371) KLEE: WARNING: seeds patched for violating constraint KLEE: WARNING ONCE: calling external: floor(4621195801218788662) at /home/klee/target/libpng-1.6.35/png.c:3375 KLEE: 1 seeds remaining over: 1 states KLEE: WARNING ONCE: calling external: vprintf(146758144, 154438432) at /home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:35 libpng warning: : gamma value does not match sRGB >From my initial understanding now klee should follow only one path but i feel that is not the case because at this point the input is symbolic so it would follow all the paths.. I'm a bit confused at the moment. Just to clarify, the expect output should be: klee@a8a6399e6799:~/seeds$ ../target/libpng-1.6.35/contrib/examples/pngpixel 1 1 ../images/png-files-download.png RGBA 255 255 255 255 klee@a8a6399e6799:~/seeds$ What am I missing? :) Thanks for your help! Alberto Il giorno mar 16 ott 2018 alle ore 14:27 Alberto Barbaro < barbaro.albe...@gmail.com> ha scritto: > Thanks I'll try that one later :) > > On Tue, Oct 16, 2018, 14:08 Sang Phan wrote: > >> You need to pass -allow-seed-extension (or -allow-seed-truncation) when >> the seed is shorter (or longer) than the symbolic file >> >> On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro < >> barbaro.albe...@gmail.com> wrote: >> >>> Hi Andrew and Sang, >>> Thanks a lot for your explanation. I tried and I think we are getting >>> there. >>> >>> @Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc >>> -only-seed A -sym-files 1 10. Now klee is complaining about the different >>> file size. When I generated the file.bout of course the file was just 1 >>> byte, now I would like to use a symbolic file. Can you suggest me how to >>> solve my problem please? >>> >>> @Sang: I'll have a look and try to use it and get back to you. >>> >>> Once I solved this problem I'll try to create a PR so next time should >>> be easier for all of us. >>> >>> Thanks again >>> >>> >>> On Tue, Oct 16, 2018, 00:50 Sang Phan wrote: >>> >>>> Hi Alberto, >>>> >>>> What you described is called concolic execution ( >>>> https://en.wikipedia.org/wiki/Concolic_testing) >>>> So the easiest way is to use an existing concolic execution engine, and >>>> you will have what you want out-of-the-box. >>>> >>>> KLEE had a concolic execut
Re: [klee-dev] Guided Search - Help
Thanks I'll try that one later :) On Tue, Oct 16, 2018, 14:08 Sang Phan wrote: > You need to pass -allow-seed-extension (or -allow-seed-truncation) when > the seed is shorter (or longer) than the symbolic file > > On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro < > barbaro.albe...@gmail.com> wrote: > >> Hi Andrew and Sang, >> Thanks a lot for your explanation. I tried and I think we are getting >> there. >> >> @Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc >> -only-seed A -sym-files 1 10. Now klee is complaining about the different >> file size. When I generated the file.bout of course the file was just 1 >> byte, now I would like to use a symbolic file. Can you suggest me how to >> solve my problem please? >> >> @Sang: I'll have a look and try to use it and get back to you. >> >> Once I solved this problem I'll try to create a PR so next time should be >> easier for all of us. >> >> Thanks again >> >> >> On Tue, Oct 16, 2018, 00:50 Sang Phan wrote: >> >>> Hi Alberto, >>> >>> What you described is called concolic execution ( >>> https://en.wikipedia.org/wiki/Concolic_testing) >>> So the easiest way is to use an existing concolic execution engine, and >>> you will have what you want out-of-the-box. >>> >>> KLEE had a concolic execution engine, called ZESTI, but it is no longer >>> supported. You may want to try Crete, it is based on KLEE, but maintained >>> by a different group. >>> https://github.com/SVL-PSU/crete-dev >>> I have not checked it. >>> >>> KLEE can be run with (concrete) seeds, and when there is only one seed, >>> it is somewhat similar to concolic execution. But you need to: >>> + tell KLEE that you only want to run seed (-only-seed) and you only >>> want to replay seeds (-only-replay-seeds), and >>> + re-start KLEE for each run of each seed. >>> >>> Cheers, >>> Sang >>> >>> On Sun, Oct 14, 2018 at 5:25 AM Alberto Barbaro < >>> barbaro.albe...@gmail.com> wrote: >>> >>>> Hi all, >>>> I have already asked this in the past and received few suggestions but >>>> I was not able to do it. I'm trying to test pngpixel[1] that takes as input >>>> an image file. My goal is to execute pngpixel with a real file and >>>> subsequently execute pngpixel with a symbolic file and follow the path >>>> followed by the first execution.I would like to describe my approach so >>>> before spending to much time on it and I can understand if I'm doing it >>>> right or not :) >>>> >>>> 1 - Execute pngpixel enabling -debug-print-instructions=src:file >>>> 2 - Inside my searcher create a map from instruction.txt so I know >>>> which is the next instruction >>>> 3 - Inside the update() function for my searcher, get the current >>>> instruction, get the next instruction, >>>> 4 - Check for each state in addedStates if the next instruction would >>>> be execute at the next step in the state >>>> 5 - If yes add the state using state.push_back(state) else remove the >>>> state ( adding the state to removedStates? ) >>>> >>>> I'm sure this flow is not optimized but at least is it correct? How >>>> would you approach this problem? >>>> >>>> Thanks for your time >>>> Alberto >>>> >>>> [1] >>>> https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c >>>> ___ >>>> 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] Guided Search - Help
Hi Andrew and Sang, Thanks a lot for your explanation. I tried and I think we are getting there. @Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc -only-seed A -sym-files 1 10. Now klee is complaining about the different file size. When I generated the file.bout of course the file was just 1 byte, now I would like to use a symbolic file. Can you suggest me how to solve my problem please? @Sang: I'll have a look and try to use it and get back to you. Once I solved this problem I'll try to create a PR so next time should be easier for all of us. Thanks again On Tue, Oct 16, 2018, 00:50 Sang Phan wrote: > Hi Alberto, > > What you described is called concolic execution ( > https://en.wikipedia.org/wiki/Concolic_testing) > So the easiest way is to use an existing concolic execution engine, and > you will have what you want out-of-the-box. > > KLEE had a concolic execution engine, called ZESTI, but it is no longer > supported. You may want to try Crete, it is based on KLEE, but maintained > by a different group. > https://github.com/SVL-PSU/crete-dev > I have not checked it. > > KLEE can be run with (concrete) seeds, and when there is only one seed, it > is somewhat similar to concolic execution. But you need to: > + tell KLEE that you only want to run seed (-only-seed) and you only want > to replay seeds (-only-replay-seeds), and > + re-start KLEE for each run of each seed. > > Cheers, > Sang > > On Sun, Oct 14, 2018 at 5:25 AM Alberto Barbaro > wrote: > >> Hi all, >> I have already asked this in the past and received few suggestions but I >> was not able to do it. I'm trying to test pngpixel[1] that takes as input >> an image file. My goal is to execute pngpixel with a real file and >> subsequently execute pngpixel with a symbolic file and follow the path >> followed by the first execution.I would like to describe my approach so >> before spending to much time on it and I can understand if I'm doing it >> right or not :) >> >> 1 - Execute pngpixel enabling -debug-print-instructions=src:file >> 2 - Inside my searcher create a map from instruction.txt so I know which >> is the next instruction >> 3 - Inside the update() function for my searcher, get the current >> instruction, get the next instruction, >> 4 - Check for each state in addedStates if the next instruction would be >> execute at the next step in the state >> 5 - If yes add the state using state.push_back(state) else remove the >> state ( adding the state to removedStates? ) >> >> I'm sure this flow is not optimized but at least is it correct? How would >> you approach this problem? >> >> Thanks for your time >> Alberto >> >> [1] >> https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c >> ___ >> 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] Guided Search - Help
Hi Andrew, Thanks for your email and PR. So I tested gen-bout on a simple project called first that prints a different message depending on the first byte of file passed as a parameter. I think I did it properly because at the end I had the file.bout file. At this point I was able to use klee-replay with it and have the same stdout. Now I don't know how to use file.bout as a seed. Are you happy to show me a simple example please? I would like to able to use it in conjunction with a new searcher in order to 'execute,' queries at runtime on the code. Thanks a lot! Alberto On Mon, Oct 15, 2018, 01:19 Andrew Santosa wrote: > Hi Alberto, > > Thank you for describing your problem. I had submitted this PR some while > ago: > https://github.com/klee/klee/pull/956 > > Basically I would use gen-bout implemented in the PR to create a ktest > file using concrete inputs, then use the ktest file as a seed. In this way, > all inputs will be symbolic, yet the path is the one that would have been > executed using the concrete inputs. > > Best, > Andrew > > On Sun, Oct 14, 2018 at 8:25 PM, Alberto Barbaro > wrote: > Hi all, > I have already asked this in the past and received few suggestions but I > was not able to do it. I'm trying to test pngpixel[1] that takes as input > an image file. My goal is to execute pngpixel with a real file and > subsequently execute pngpixel with a symbolic file and follow the path > followed by the first execution.I would like to describe my approach so > before spending to much time on it and I can understand if I'm doing it > right or not :) > > 1 - Execute pngpixel enabling -debug-print-instructions=src:file > 2 - Inside my searcher create a map from instruction.txt so I know which > is the next instruction > 3 - Inside the update() function for my searcher, get the current > instruction, get the next instruction, > 4 - Check for each state in addedStates if the next instruction would be > execute at the next step in the state > 5 - If yes add the state using state.push_back(state) else remove the > state ( adding the state to removedStates? ) > > I'm sure this flow is not optimized but at least is it correct? How would > you approach this problem? > > Thanks for your time > Alberto > > [1] > https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c > ___ > 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] Guided Search - Help
Hi all, I have already asked this in the past and received few suggestions but I was not able to do it. I'm trying to test pngpixel[1] that takes as input an image file. My goal is to execute pngpixel with a real file and subsequently execute pngpixel with a symbolic file and follow the path followed by the first execution.I would like to describe my approach so before spending to much time on it and I can understand if I'm doing it right or not :) 1 - Execute pngpixel enabling -debug-print-instructions=src:file 2 - Inside my searcher create a map from instruction.txt so I know which is the next instruction 3 - Inside the update() function for my searcher, get the current instruction, get the next instruction, 4 - Check for each state in addedStates if the next instruction would be execute at the next step in the state 5 - If yes add the state using state.push_back(state) else remove the state ( adding the state to removedStates? ) I'm sure this flow is not optimized but at least is it correct? How would you approach this problem? Thanks for your time Alberto [1] https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] How to skip the current state?
Hi all, I'm working on a new searcher and I'm at a point where I would skip the current state and just continue with the new added states. Is there a way to do that in the updateState() function? If not, how should I do it? Thanks a lot ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to introduce the "Exploration Technique" concept
Thanks Martin, I think tipically within the update function all the states within the 'removedStates' vector are removed from the 'states' variable so I thought I should do the same in my case. If in other cases states are added I think my approach to remove or add states depending on the condition described in the .path file it would not work. Are you happy to describe an approach that I should use for creating this kind of searcher? Just to clarify, I have a ,path file with 0's and 1's because a program was executed with a real input file as parameter and now I would like to execute again the same program but with symbolic input and be able to follow exactly the same path had before. Thanks On Wed, May 2, 2018, 22:11 Nowack, Martin <m.now...@imperial.ac.uk> wrote: > Hi Alberto, > > The function `selectState()` returns the state you would like KLEE to work > on next. > So this always only one state. > > The update function is KLEE’s callback to your searcher to inform you > which states have been added or removed. > > But, you should not make any assumption on the order of states coming in > nor how many states you will have. > Forking of states can happen at different positions not only the branch > instruction. > > The only information you can currently consider as exact is the one you > get from the state itself: e.g. the old > instruction pointer and the new instruction pointer, but of course there > is much more there. > > Hope that helps you a bit further. > > Best, > Martin > > On 2. May 2018, at 20:16, Alberto Barbaro <barbaro.albe...@gmail.com> > wrote: > > Hi all, > thanks for the answer. I was able to create another searcher called > "guided" that should do what i want but I have problem for now. From my > understanding the crucial function to implement are: update and selectState. > > I think in the selectState function I should return *states[0] or > *states[1] depending if in the condition is false or true. I'm not sure > that the first state represents the false condition so please let me know > if I'm wrong. Instead, within the update function I should remove all the > states apart states[0] or states[1] depending on the content of the file > again. > > Unfortunately I'm not sure that if my idea is correct. Can someone let me > know what I'm missing and maybe give me an example? > > Thanks > Alberto > > On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > >> My recommendation is to implement such an exploration technique as an >> independent search heuristic. The bar for changing the core of KLEE is >> much higher, as it affects all users. >> >> Best, >> Cristian >> >> On 18/03/2018 17:41, Alberto Barbaro wrote: >> > Hi, >> > I'm working on a possible PULL request that would allow to execute a >> > project but excluding paths based on a .path previously generated using >> > KLEE. Doing so it would be possible to have some sort of "exploration >> > technique" that would help to follow specific paths. >> > >> > I think, after having generated the .path file, it would be possible to >> > do so amending Executor.cpp main switch for the Instruction::Br case. >> > I'm able to keep track of the "index" for the current branch so I would >> > check cond.get().isTrue() comparing with value on line "index". At this >> > point I'm not sure how to skip a branch ( I cannot use exit(0) like >> > klee_silent_exit I think ). Should I just modify the if for the "br" >> > branch of the switch? >> > >> > Thanks for any suggesiton, >> > A >> > >> > >> > ___ >> > 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] How to introduce the "Exploration Technique" concept
Hi all, thanks for the answer. I was able to create another searcher called "guided" that should do what i want but I have problem for now. From my understanding the crucial function to implement are: update and selectState. I think in the selectState function I should return *states[0] or *states[1] depending if in the condition is false or true. I'm not sure that the first state represents the false condition so please let me know if I'm wrong. Instead, within the update function I should remove all the states apart states[0] or states[1] depending on the content of the file again. Unfortunately I'm not sure that if my idea is correct. Can someone let me know what I'm missing and maybe give me an example? Thanks Alberto On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > My recommendation is to implement such an exploration technique as an > independent search heuristic. The bar for changing the core of KLEE is > much higher, as it affects all users. > > Best, > Cristian > > On 18/03/2018 17:41, Alberto Barbaro wrote: > > Hi, > > I'm working on a possible PULL request that would allow to execute a > > project but excluding paths based on a .path previously generated using > > KLEE. Doing so it would be possible to have some sort of "exploration > > technique" that would help to follow specific paths. > > > > I think, after having generated the .path file, it would be possible to > > do so amending Executor.cpp main switch for the Instruction::Br case. > > I'm able to keep track of the "index" for the current branch so I would > > check cond.get().isTrue() comparing with value on line "index". At this > > point I'm not sure how to skip a branch ( I cannot use exit(0) like > > klee_silent_exit I think ). Should I just modify the if for the "br" > > branch of the switch? > > > > Thanks for any suggesiton, > > A > > > > > > ___ > > 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] How to get the returned address after an malloc
Thanks Andrew, I'll try to do as you said. Thanks again for the help. A 2018-04-28 2:34 GMT+01:00 Andrew Santosa <asantosa1...@gmail.com>: > Hi Alberto, > > Perhaps you can simply dump the expression before the call to bindLocal(). > That is, if you see bindLocal() call of the form: > > bindLocal(kinst, state, expr); > > you can do > > expr->dump(); > > immediately after/before the call to see the expression being locally > bound. > > I hope this helps. > > Best, > Andrew > > > On Sunday, 18 March 2018, 7:56:03 pm GMT+8, Alberto Barbaro < > barbaro.albe...@gmail.com> wrote: > > > Hi all, > I have seen that the malloc function is handled via handleMallc() in > Executor.cpp relying on executeAlloc(). I would like to understand the best > way to access, for instance, to address associated with the memory > allocated by the malloc. I think the function bindLocal() is used for > storing that information within the state object but I cannot really > understand how to retrieve it. > > Any help please with an example? > > Thanks > ___ > 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] How to introduce the "Exploration Technique" concept
Hi, I was able to create a new Searcher called Guided where I have implemented my selectState() and updateStates(). The problem I have now is to identify what state I should return in select selectState() and how to remove all the other states(). I guessed that with symbolic input when and if is encountered 2 states are returned, the first should be the false branch instead the second should be the true branch. Am I right? At this point should I terminate the other state? Thanks for your time. A 2018-03-18 20:43 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>: > Thanks I'll do, do you think my approach is correct or should I do it on a > different way? How would you approach it? > > Thanks > > On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > >> My recommendation is to implement such an exploration technique as an >> independent search heuristic. The bar for changing the core of KLEE is >> much higher, as it affects all users. >> >> Best, >> Cristian >> >> On 18/03/2018 17:41, Alberto Barbaro wrote: >> > Hi, >> > I'm working on a possible PULL request that would allow to execute a >> > project but excluding paths based on a .path previously generated using >> > KLEE. Doing so it would be possible to have some sort of "exploration >> > technique" that would help to follow specific paths. >> > >> > I think, after having generated the .path file, it would be possible to >> > do so amending Executor.cpp main switch for the Instruction::Br case. >> > I'm able to keep track of the "index" for the current branch so I would >> > check cond.get().isTrue() comparing with value on line "index". At this >> > point I'm not sure how to skip a branch ( I cannot use exit(0) like >> > klee_silent_exit I think ). Should I just modify the if for the "br" >> > branch of the switch? >> > >> > Thanks for any suggesiton, >> > A >> > >> > >> > ___ >> > 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] How to introduce the "Exploration Technique" concept
Thanks I'll do, do you think my approach is correct or should I do it on a different way? How would you approach it? Thanks On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > My recommendation is to implement such an exploration technique as an > independent search heuristic. The bar for changing the core of KLEE is > much higher, as it affects all users. > > Best, > Cristian > > On 18/03/2018 17:41, Alberto Barbaro wrote: > > Hi, > > I'm working on a possible PULL request that would allow to execute a > > project but excluding paths based on a .path previously generated using > > KLEE. Doing so it would be possible to have some sort of "exploration > > technique" that would help to follow specific paths. > > > > I think, after having generated the .path file, it would be possible to > > do so amending Executor.cpp main switch for the Instruction::Br case. > > I'm able to keep track of the "index" for the current branch so I would > > check cond.get().isTrue() comparing with value on line "index". At this > > point I'm not sure how to skip a branch ( I cannot use exit(0) like > > klee_silent_exit I think ). Should I just modify the if for the "br" > > branch of the switch? > > > > Thanks for any suggesiton, > > A > > > > > > ___ > > 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] How to introduce the "Exploration Technique" concept
Hi, I'm working on a possible PULL request that would allow to execute a project but excluding paths based on a .path previously generated using KLEE. Doing so it would be possible to have some sort of "exploration technique" that would help to follow specific paths. I think, after having generated the .path file, it would be possible to do so amending Executor.cpp main switch for the Instruction::Br case. I'm able to keep track of the "index" for the current branch so I would check cond.get().isTrue() comparing with value on line "index". At this point I'm not sure how to skip a branch ( I cannot use exit(0) like klee_silent_exit I think ). Should I just modify the if for the "br" branch of the switch? Thanks for any suggesiton, A ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] How to get the returned address after an malloc
Hi all, I have seen that the malloc function is handled via handleMallc() in Executor.cpp relying on executeAlloc(). I would like to understand the best way to access, for instance, to address associated with the memory allocated by the malloc. I think the function bindLocal() is used for storing that information within the state object but I cannot really understand how to retrieve it. Any help please with an example? Thanks ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] How to add a new class to KLEE?
Hi,
sure i'll prepare something as soon as I have some free time. Would you
prefer a full example or just a comment about updating CMakeList.txt?
Thanks
2018-03-10 10:30 GMT+00:00 Cristian Cadar <c.ca...@imperial.ac.uk>:
> We would welcome updates and improvements to the documentation. Just open
> a pull request at https://github.com/klee/klee.github.io
>
> Best,
> Cristian
>
> On 10/03/2018 07:08, Alberto Barbaro wrote:
>
>> Hi,
>> sorry for the email... I fix it adding the file to the CMakeList.txt, I
>> would suggest to update the documentation on the website as well. I think
>> it would be useful to everybody.
>>
>> Thanks
>>
>> 2018-03-10 6:17 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com
>> <mailto:barbaro.albe...@gmail.com>>:
>>
>>
>> Hi all,
>> I would like to add a new class to KLEE but I have few problems. I
>> tried to follow the help that is present on the website but not luck
>> so far.
>>
>> In my case, I have created TestObject,h and TestObject.cpp in
>> lib/Core and included TestObject.h in lib/Core/Executor.cpp using
>> #include "TestObject.h" and finally added into the function
>> executeInstruction the line TestObject t;
>>
>> The code for the class in pretty standard:
>>
>> TestObject.h
>> #ifndef TESTOBJECT_H
>> #define TESTOBJECT_H
>>
>> namespace klee
>> {
>>
>> class TestObject
>> {
>> public:
>> TestObject();
>> ~TestObject();
>>
>> };
>>
>> }
>>
>> #endif // TESTOBJECT_H
>>
>> TestObject.cpp
>> #include "TestObject.h"
>>
>> klee::TestObject::TestObject()
>> {
>> }
>>
>> klee::TestObject::~TestObject()
>> {
>> }
>>
>> The error I got is:
>> [ 98%] Built target kleeModule
>> Linking CXX executable ../../bin/klee
>> ../../lib/libkleeCore.a(Executor.cpp.o): In function
>> `klee::Executor::executeInstruction(klee::ExecutionState&,
>> klee::KInstruction*)':
>> /home/klee/klee-taint/lib/Core/Executor.cpp:1447: undefined
>> reference to `klee::TestObject::TestObject()'
>> /home/klee/klee-taint/lib/Core/Executor.cpp:2459: undefined
>> reference to `klee::TestObject::~TestObject()'
>>
>> What am I missing? I cannot understand the problem in this case.
>>
>> Thanks a lot,
>> A
>>
>>
>>
>>
>> ___
>> 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] How to add a new class to KLEE?
Hi,
sorry for the email... I fix it adding the file to the CMakeList.txt, I
would suggest to update the documentation on the website as well. I think
it would be useful to everybody.
Thanks
2018-03-10 6:17 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>:
> Hi all,
> I would like to add a new class to KLEE but I have few problems. I tried
> to follow the help that is present on the website but not luck so far.
>
> In my case, I have created TestObject,h and TestObject.cpp in lib/Core and
> included TestObject.h in lib/Core/Executor.cpp using #include
> "TestObject.h" and finally added into the function executeInstruction the
> line TestObject t;
>
> The code for the class in pretty standard:
>
> TestObject.h
> #ifndef TESTOBJECT_H
> #define TESTOBJECT_H
>
> namespace klee
> {
>
> class TestObject
> {
> public:
> TestObject();
> ~TestObject();
>
> };
>
> }
>
> #endif // TESTOBJECT_H
>
> TestObject.cpp
> #include "TestObject.h"
>
> klee::TestObject::TestObject()
> {
> }
>
> klee::TestObject::~TestObject()
> {
> }
>
> The error I got is:
> [ 98%] Built target kleeModule
> Linking CXX executable ../../bin/klee
> ../../lib/libkleeCore.a(Executor.cpp.o): In function `klee::Executor::
> executeInstruction(klee::ExecutionState&, klee::KInstruction*)':
> /home/klee/klee-taint/lib/Core/Executor.cpp:1447: undefined reference to
> `klee::TestObject::TestObject()'
> /home/klee/klee-taint/lib/Core/Executor.cpp:2459: undefined reference to
> `klee::TestObject::~TestObject()'
>
> What am I missing? I cannot understand the problem in this case.
>
> Thanks a lot,
> A
>
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] How to add a new class to KLEE?
Hi all,
I would like to add a new class to KLEE but I have few problems. I tried to
follow the help that is present on the website but not luck so far.
In my case, I have created TestObject,h and TestObject.cpp in lib/Core and
included TestObject.h in lib/Core/Executor.cpp using #include
"TestObject.h" and finally added into the function executeInstruction the
line TestObject t;
The code for the class in pretty standard:
TestObject.h
#ifndef TESTOBJECT_H
#define TESTOBJECT_H
namespace klee
{
class TestObject
{
public:
TestObject();
~TestObject();
};
}
#endif // TESTOBJECT_H
TestObject.cpp
#include "TestObject.h"
klee::TestObject::TestObject()
{
}
klee::TestObject::~TestObject()
{
}
The error I got is:
[ 98%] Built target kleeModule
Linking CXX executable ../../bin/klee
../../lib/libkleeCore.a(Executor.cpp.o): In function
`klee::Executor::executeInstruction(klee::ExecutionState&,
klee::KInstruction*)':
/home/klee/klee-taint/lib/Core/Executor.cpp:1447: undefined reference to
`klee::TestObject::TestObject()'
/home/klee/klee-taint/lib/Core/Executor.cpp:2459: undefined reference to
`klee::TestObject::~TestObject()'
What am I missing? I cannot understand the problem in this case.
Thanks a lot,
A
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] /usr/bin/ld: cannot find -lkleeRunTest
Hi all, I'm sorry to ask a question that was already asked but I cannot figure out what I'm missing. I'm recompiling libpng and I'm using klee_make_symbolic in the main function as a test. The ./configure goes well but the make does not. I have changed the Makefile and I have an error like this: /bin/bash ./libtool --tag=CC --mode=link wllvm -g -O2 -L/home/klee/klee_build/klee/lib/ -Wl,-rpath=/home/klee/klee_build/klee/lib/ -o pngfix contrib/tools/pngfix.o libpng16.la -lm -lz -lm -lkleeRunTest libtool: link: wllvm -g -O2 -Wl,-rpath=/home/klee/klee_build/klee/lib/ -o .libs/pngfix contrib/tools/pngfix.o -L/home/klee/klee_build/klee/lib/*.* ./.libs/libpng16.so -lz -lm -lkleeRunTest /usr/bin/ld: cannot find -lkleeRunTest I have seen the libkleeRuntest.so in the /home/klee/klee_build/klee/lib/ path... I'm doing all using the Docker image... Can you suggest me how to solve it please? Thanks, A ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Missing floor, modf and pow
Thanks Dan, all clear now. Thanks again 2018-03-03 21:23 GMT+00:00 Dan Liew <d...@su-root.co.uk>: > Hi, > > On 3 March 2018 at 07:29, Alberto Barbaro <barbaro.albe...@gmail.com> > wrote: > > Hi all, > > few months ago I was trying to understand how to test pngpixel via KLEE > and > > after few suggestion I was able to do it. > > > > I have just one more question. When I run KLEE I have this output: > > > > klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee > > --libc=uclibc --posix-runtime pngpixel.bc 1 1 file.png > > KLEE: NOTE: Using klee-uclibc : > > /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca > > KLEE: NOTE: Using model: > > /home/klee/klee_build/klee/Release+Debug+Asserts/lib/ > libkleeRuntimePOSIX.bca > > KLEE: output directory is > > "/home/klee/targets/libpng-1.6.34/contrib/examples/klee-out-3" > > KLEE: Using STP solver backend > > KLEE: WARNING: undefined reference to function: floor > > KLEE: WARNING: undefined reference to function: modf > > KLEE: WARNING: undefined reference to function: pow > > KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 92453184) at > > /home/klee/klee_src/runtime/POSIX/fd.c:1044 > > KLEE: WARNING ONCE: calling __user_main with extra arguments. > > KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not > modelled. > > Using alignment of 8. > > KLEE: WARNING ONCE: _setjmp: ignoring > > > > KLEE: done: total instructions = 106954 > > KLEE: done: completed paths = 1 > > KLEE: done: generated tests = 1 > > klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ > > > > Can I "ignore" the fact that floor, modf and pow are missing because I'm > > using uclibc? > > You can ignore the warning as long as the code you run doesn't call > these with symbolic arguments. You'll see a warning if this happens > because KLEE has to concretize the arguments and call the function via > LLVM's JIT. > In your case it doesn't look like you're passing any symbolic data to > the application so you're running concretely so you should be fine. If > any function gets called that's external (i.e. is not in the LLVM > bitcode, like floor is in your example) > KLEE will emit a message telling you its calling an external. > > The reason these functions aren't available is because KLEE doesn't > link in Uclibc's C library. My fork of KLEE that supports symbolic > floating-point arithmetic [1] does link this library. > > [1] https://github.com/srg-imperial/klee-float > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Possible improvement for --write-paths
The Cristian, honestly I was think about something with a different structure. Maybe something like: . . Of course the path should track also intra-procedural calls and all the other calls/returns/... Do you think it would useful? Thanks 2018-03-03 21:10 GMT+00:00 Cristian Cadar <c.ca...@imperial.ac.uk>: > Hi, there in an open PR about this, which you might like to use, although > it still requires some work: https://github.com/klee/klee/pull/473 > > Best, > Cristian > > > On 03/03/2018 08:06, Alberto Barbaro wrote: > >> Hi again, >> I have seen that it is possible to save the paths using the option >> --write-paths, the output contains a lot of 0 and 1 which I guess are the >> result for branches. Is it possible to have a more verbose output >> containing for example the list of addresses encountered? If so, can I have >> an idea on how to do it please? >> >> Thanks >> >> >> ___ >> 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] Missing floor, modf and pow
Hi all, few months ago I was trying to understand how to test pngpixel via KLEE and after few suggestion I was able to do it. I have just one more question. When I run KLEE I have this output: klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee --libc=uclibc --posix-runtime pngpixel.bc 1 1 file.png KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/klee/targets/libpng-1.6.34/contrib/examples/klee-out-3" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: floor KLEE: WARNING: undefined reference to function: modf KLEE: WARNING: undefined reference to function: pow KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 92453184) at /home/klee/klee_src/runtime/POSIX/fd.c:1044 KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8. KLEE: WARNING ONCE: _setjmp: ignoring KLEE: done: total instructions = 106954 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ Can I "ignore" the fact that floor, modf and pow are missing because I'm using uclibc? Thanks ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Compiling error
Hi, OK i found the solution after a break: https://keeda.stanford.edu/pipermail/klee-dev/2012-January/000794.html HTH, Alberto 2015-11-07 7:49 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>: > Hi, > i'm trying to compiling Klee and once i run make ENABLE_OPTIMZED=1 i have > the following error: > > llvm[2]: === Finished Linking Release+Asserts Executable klee-replay > (without symbols) > make[2]: Leaving directory > '/home/alberto/Desktop/progetti/klee/tools/klee-replay' > make[1]: Leaving directory '/home/alberto/Desktop/progetti/klee/tools' > make[1]: Entering directory '/home/alberto/Desktop/progetti/klee/runtime' > make[2]: Entering directory > '/home/alberto/Desktop/progetti/klee/runtime/Intrinsic' > llvm[2]: Compiling klee_div_zero_check.c for Release+Asserts build > (bytecode) > llvm[2]: Compiling klee_div_zero_check.ll to klee_div_zero_check.bc for > Release+Asserts build (bytecode) > llvm[2]: Compiling klee_int.c for Release+Asserts build (bytecode) > In file included from klee_int.c:10: > /usr/include/assert.h:69: error: expected ‘=’, ‘,’, ‘;’, ‘asm’ or > ‘__attribute__’ before ‘extern’ > /usr/include/assert.h: In function ‘__assert_perror_fail’: > /usr/include/assert.h:76: error: expected declaration specifiers before > ‘__THROW’ > /usr/include/assert.h:82: error: expected ‘=’, ‘,’, ‘;’, ‘asm’ or > ‘__attribute__’ before ‘__THROW’ > /usr/include/assert.h:85: error: expected declaration specifiers before > ‘__END_DECLS’ > > I can't use docker because I'm a 32bit box. > > Any idea on how to solve this? > > Thanks > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Invalid recordLoading
Dan, Thanks for you answer. I think I've followed exactly the web site but maybe I'm wrong. This eve I'll retry and send over here the output of the command that you have suggested. Thanks, Alberto On 25 Mar 2015 13:36, Dan Liew d...@su-root.co.uk wrote: On 24 March 2015 at 21:16, Alberto Barbaro barbaro.albe...@gmail.com wrote: Hi all, I'm trying to set up klee with llvm 3.4 following the step by step guide. Everything looks good apart the last step. When I execute lit -v . I have this error: Klee-uclibc.bca failed: invalid record loading module failed: Invalid record That error message suggests that you didn't build klee-uclibc correctly. Try openining the ``klee-uclibc.bca`` file with ``llvm-ar`` to check its a proper archive ``` $ llvm-ar p /path/to/klee-uclibc.bca ``` ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Invalid recordLoading
Hi, Should I see the files contained in it? I can see just not printable characters.. I followed the guide on the web site. Any advice? Thanks, Alberto On 25 Mar 2015 13:47, Alberto Barbaro barbaro.albe...@gmail.com wrote: Dan, Thanks for you answer. I think I've followed exactly the web site but maybe I'm wrong. This eve I'll retry and send over here the output of the command that you have suggested. Thanks, Alberto On 25 Mar 2015 13:36, Dan Liew d...@su-root.co.uk wrote: On 24 March 2015 at 21:16, Alberto Barbaro barbaro.albe...@gmail.com wrote: Hi all, I'm trying to set up klee with llvm 3.4 following the step by step guide. Everything looks good apart the last step. When I execute lit -v . I have this error: Klee-uclibc.bca failed: invalid record loading module failed: Invalid record That error message suggests that you didn't build klee-uclibc correctly. Try openining the ``klee-uclibc.bca`` file with ``llvm-ar`` to check its a proper archive ``` $ llvm-ar p /path/to/klee-uclibc.bca ``` ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
