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 <[email protected]> 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 <[email protected]> > 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
