Re: [klee-dev] Implementing support for the Firehose file format

[Marko Dimjašević]

Hi again,

On Sat, 2016-07-02 at 20:24 -0600, Marko Dimjašević wrote:
> A thing that I would like to put in the output file is values of input
> arguments to a program for a failing test case when the POSIX runtime
> is used. Usually one calls the klee-replay tool for this. Is there a
> way to use this functionality as a library from within
> tools/klee/main.cpp?

Does anyone have an answer to this?

I guess it shouldn't be hard, but I haven't been able to figure it out.


-- 
Regards,
Marko Dimjašević  .   University of Utah
https://dimjasevic.net/marko . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org


signature.asc
Description: This is a digitally signed message part
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Implementing support for the Firehose file format

[Marko Dimjašević]

Hi KLEE developers,

On Tue, 2016-05-10 at 21:12 -0600, Marko Dimjašević wrote:
> I would like to implement support for the Firehose reporting file
> format in KLEE:
> 
> https://github.com/fedora-static-analysis/firehose

I am close to being done with this one. One will simply add the
-firehose-output command line argument to KLEE and it will generate
firehose.xml in the klee-last directory.

A thing that I would like to put in the output file is values of input
arguments to a program for a failing test case when the POSIX runtime is
used. Usually one calls the klee-replay tool for this. Is there a way to
use this functionality as a library from within tools/klee/main.cpp?

An attempt I made is to simply read from m_argv in the KleeHandler
class, but that doesn't work if there are symbolic inputs to the
program (e.g., I obtain things like "--sym-arg 3" instead of a concrete
value that lead to the failure). Then there is
Executor::getSymbolicSolution, which is probably related, but I don't
know how to make the solution concrete.

My hunch is I'd maybe have to call the klee_init_env function from
runtime/POSIX/klee_init_env.c. However, I've been wondering if it's
safe to do so from the KleeHandler::processTestCase function in
tools/klee/main.cpp. In other words, does klee_init_env impact a global
state and does it have side-effects?

If I should do something else to obtain concrete input values, I will be
more than happy to hear your suggestion.


-- 
Regards,
Marko Dimjašević  .   University of Utah
https://dimjasevic.net/marko . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org



signature.asc
Description: This is a digitally signed message part
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Implementing support for the Firehose file format

[Martin Nowack]

Hi Marko,

I guess you want to collect bugs found,
in that case maybe hooking into the test generation function might be a good 
idea:

https://github.com/klee/klee/blob/master/tools/klee/main.cpp#L419
void KleeHandler::processTestCase(const ExecutionState , const char 
*errorMessage, const char *errorSuffix)

This function gets called overtime a new test case is generated.

Maybe that helps you.

Another issue, which might be interesting for you is:
https://github.com/klee/klee/issues/393
So maybe you can get involved into the discussion as well.

Cheers,
Martin


> On 11 May 2016, at 05:12, Marko Dimjašević  wrote:
> 
> Dear all,
> 
> I would like to implement support for the Firehose reporting file format
> in KLEE:
> 
> https://github.com/fedora-static-analysis/firehose
> 
> So far I haven't really looked at KLEE's code base, so I am not familiar
> with it. If you have any pointers where to start looking where this
> would be implemented, that would be highly appreciated.
> 
> 
> --
> Regards,
> Marko Dimjašević  .   University of Utah
> https://dimjasevic.net/marko . PGP key ID: 1503F0AA
> Learn email self-defense!  https://emailselfdefense.fsf.org
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_now...@tu-dresden.de




signature.asc
Description: Message signed with OpenPGP using GPGMail
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev