[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ć <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160702/693e05fe/attachment.sig>