[klee-dev] rationale behind the parameters used in the KLEE OSDI paper

Lei Zhang lei.zhang at uwaterloo.ca
Fri Feb 8 14:44:53 GMT 2013


Hi Cristian,

Thank you very much for your direction!

On Thu, Feb 7, 2013 at 6:03 AM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:

> Hi Lei,
>
>
> On 05/02/13 03:35, Lei Zhang wrote:
>
>> Coreutils experiment. They are very helpful! Now we have set up the
>> environment using Ubuntu 10.04 + LLVM 2.7 (I'd like to contribute to the
>> upgrading to 2.9 after I finish this project).
>>
> That would be useful, thanks.
>
>
>  And we have some
>> questions about replaying ktest and accumulating results. We use
>> klee-replay to replay all the generated ktests in the obj-gcov directory
>> and use gcov to get the line coverage on every single source file. Is
>> that right?
>>
> Yes, that's correct.  You might want to use a tool that Daniel wrote,
> zcov, to visualize the results: http://minormatter.com/zcov/
>
>
>  And is there any possible way to replay in a sandbox? When testing some
>> tools (e.g., chmod), it will do harm to the filesystem or encounter
>> permission errors (which may hurt the coverage). Thank you in advance!
>>
> Yes, the right thing to do would be to replay every test in a new instance
> of a virtual machine (or something similar).  But we didn't do this, we
> just made sure that the replay process doesn't have permissions to do too
> much harm :)  In any case, what's important to remember is to replay each
> test case in a fresh sandbox directory (I'm referring here to the "sandbox"
> discussed at http://klee.llvm.org/**CoreutilsExperiments.html<http://klee.llvm.org/CoreutilsExperiments.html>)
> and to set the same environment variables as the ones set during symbolic
> execution (the ones in test.env).
>
So this means before replay a ktest, I should remove the old sanbox
directory and uncompress sandbox.tgz to create a new one, and then copy the
native utility compiled with gcov support to the new sandbox directory and
then reply the ktest?

>
> Hope this helps,
> Cristian
>
>
> ______________________________**_________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>



-- 
Lei Zhang
Department of Electrical and Computer Engineering
University of Waterloo
 200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list