[klee-dev] One question about external dispatcher

[Qiuping Yi]

Dear all,

I encountered a strange problem when testing the next code snippet:

1 if (pw = getpwuid(getuid()) == NULL)
2   return ;

3 .. = pw->pw_dir;

When handling line 1, KLEE firstly invokes *externalDispatcher->executeCall*
which will invoke *runProtectedCall* to execute the external function and
store
the result to a given memory location. Then, it will invoke *fromMemory* to
get the
return value from the location. However, it encounters an "out of bound"
error
when handling line 3. I printed the value of variable *pw* at line 1, and
got something like *139894903382656*, which definitely does not equal to '
*null*',
thus it will arrive line 3. Actually, *139894903382656* seems an invalid
address.

So why does this strange situation happen?

Thank you all in advance.

Best regards,

Qiuping Yi
Parasol Laboratory
Department of Computer Science and Engineering
Texas A University
College Station
TX 77843
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Target-Directed Symbolic Execution with KLEE

[Yannic Noller]

Hi Cristian,

thanks for the hint, I will take a look.

— Yannic

> On 25 Jan 2017, at 16:01, Cristian Cadar  wrote:
> 
> Hi Yannic, you might like to take a look at KATCH: 
> http://srg.doc.ic.ac.uk/projects/katch/ 
> 
> 
> The code is available, but unfortunately not integrated into the mainline.
> 
> Cristian
> 
> On 23/01/17 15:31, Yannic Noller wrote:
>> Hi Jason,
>> 
>> thanks, I know the example and you are right: this is probably the
>> fastest way to try my idea. But this means that there is no special
>> option for an target-oriented search, right? For example I do not want
>> to follow paths that cannot reach my specified target line in order to
>> cut down the possible state space. If not, is it easy to implement such
>> a feature in KLEE?
>> 
>> Thanks!
>> — Yannic
>> 
>> 
>>> On 23 Jan 2017, at 14:12, Papapanagiotakis-Bousy, Iason
>>> >> >> >> wrote:
>>> 
>>> Hi Yannic,
>>> 
>>> Have you looked into the maze
>>> tutorial https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ 
>>>  ?
>>> 
>>> I am no KLEE veteran but here is my suggestion:
>>> If I understand correctly what you are trying to achieve, then you
>>> could use what is shown in the tutorial and at the end instead of
>>> looking at the .ktest files that will have concrete examples, read the
>>> corresponding .kquery files that contain the path constraints.
>>> 
>>> (because the tutorial uses an older version of KLEE, constraints are
>>> stored in a .pc instead of .kquery)
>>> 
>>> Hope it helps.
>>> 
>>> Best regards,
>>> Jason
>>> 
>>> *From:* klee-dev-boun...@imperial.ac.uk 
>>> 
>>> >> >
>>> [mailto:klee-dev-boun...@imperial.ac.uk 
>>> ] *On Behalf Of *Yannic Noller
>>> *Sent:* Monday, January 23, 2017 2:54 PM
>>> *To:* klee-dev@imperial.ac.uk  
>>> >
>>> *Subject:* [klee-dev] Target-Directed Symbolic Execution with KLEE
>>> 
>>> Hi all,
>>> 
>>> I would like to create all path conditions (or an under-approximation)
>>> that reach a certain source code line (something like "directed
>>> symbolic execution"). Is there an option in KLEE to do that? Or is
>>> there an extension of KLEE that can do that?
>>> 
>>> Any help is very appreciated :)
>>> 
>>> Thanks,
>>> Yannic
>> 
>> 
>> 
>> ___
>> 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