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

[Cristian Cadar]

Hi Lei,

Here are the symbolic arguments for those eight tools:

dd: --sym-args 0 3 10 --sym-files 1 8 --sym-stdout
dircolors: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
echo: --sym-args 0 4 300 --sym-files 2 30 --sym-stdout
expr: --sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout
mknod: --sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdout
od: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout
pathchk: --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout
printf: --sym-args 0 3 10 --sym-files 2 12 --sym-stdout

Hope this helps,
Cristian

On 14/01/13 18:28, Lei Zhang wrote:
> Hi Cristian,
>
> Thank you for your quick reply! :-)
>
> Besides, the paper mentions "For eight tools where the coverage results
> of these values were unsatisfactory, we consulted the man page and
> increased the number and size of arguments and files." Could you give us
> more details about that? Thanks!
>
> Best regards,
>
> On Mon, Jan 14, 2013 at 10:44 AM, Cristian Cadar <c.cadar at imperial.ac.uk
> <mailto:c.cadar at imperial.ac.uk>> wrote:
>
>     Hi Lei,
>
>     Our choice was based on a high-level understanding of the Coreutils
>     apps: most behavior can be triggered with no more than 2 short
>     options,  1 long option, and 2 small files (one of which is stdin).
>
>     Best wishes,
>     Cristian
>
>
>     On 14/01/13 14:58, Lei Zhang wrote:
>
>         Hi All,
>
>         We are working on a possible way to improve KLEE. So it would be
>         nice to
>         compare our method's results with the original KLEE's. For a fair
>         comparison, we need to understand how the parameters used in your
>         OSDI'08 paper were chosen. According to your reply on the KLEE
>         mailing
>         list
>         (http://www.mail-archive.com/__klee-dev@imperial.ac.uk/__msg00162.html
>         <http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00162.html>),
>         your OSDI paper uses
>
>         --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 2 8 --sym-stdout
>
>         Could you unveil the rationale/intuition behind these settings, such
>         like why 10 and 2 are used as the maximal lengths? Any help is
>         highly
>         appreciated. Thanks in advance!
>
>         Best regards,
>
>         --
>         Lei
>         Department of Electrical and Computer Engineering
>         University of Waterloo
>         200 University Avenue West
>         Waterloo, Ontario, Canada N2L 3G1
>
>
>         _________________________________________________
>         klee-dev mailing list
>         klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>     _________________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto: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