[klee-dev] Set precondition for symbolic execution

[Dingbao Xie]

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 <shaotian330 at gmail.com> 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 <realdaniel2013 at gmail.com>
> 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 <shaotian330 at gmail.com>
>> 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
>>> klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>>
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>


-- 
Dingbao Xie
-------------- next part --------------
HTML attachment scrubbed and removed