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

2017-01-26 Thread 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

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

2017-01-25 Thread Cristian Cadar 
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

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

2017-01-23 Thread Papapanagiotakis-Bousy, Iason 
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