Hi Pengfei, I think this work http://dl.acm.org/citation.cfm?id=2483778 is quite relevant to your question. In the first stage, they use fortifty to analyze source code and then get a bunch of possible bugs. Fortify gives the possible path segment to trigger the bug. In the second stage, they use concolic execution to find a path containing the target path segment.
On Wed, Jul 22, 2015 at 5:50 AM, Pengfei Sun <[email protected]> wrote: > Hi Daniel, > > Great! This is very useful for me. I still have some questions about your > solution. For example, I can mark several paths "important", and then make > klee only explore these "important" branch instructions. Whether there are > special functions for klee to recognize these "important" instructions and > then only explore these instructions? > > Thank you very much! > > Best Regards, > Pengfei > > > On Mon, Jul 20, 2015 at 1:31 PM, Daniel Guo <[email protected]> > wrote: > >> Hi, >> KLEE forks new states at branching points, which makes it can explore >> different paths. >> The detailed code is in Executor::executeInstruction(...) function >> (Executor.cpp, i guess). >> You can add some meta data to the llvm IR instruction, to mark it >> "important" (by a llvm pass), then just fully explore the two outgoing >> states of "important" branch instructions by klee. >> >> Daniel. >> >> >> On Mon, Jul 20, 2015 at 10:58 AM, Pengfei Sun <[email protected]> >> wrote: >> >>> Hi All, >>> >>> I wonder how to set precondition for klee to do symbolic execution? >>> >>> For example, I firstly choose several interesting paths of one >>> application by static analysis, and make one profile based on these paths. >>> And then I can make klee to run this application based on the profile, >>> which means klee will only explore the limited paths in the profile. Now I >>> cannot find out how to make the klee to choose paths based on the profile? >>> >>> Can you give me any hints which functions help klee to choose different >>> paths? How is it possible to make klee to choose paths based on my profile >>> which includes several paths? >>> >>> Thank you very much! >>> >>> >>> Best Regards, >>> Pengfei Sun >>> >>> _______________________________________________ >>> 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 > > -- Dingbao Xie
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
