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
