[klee] [zesti] ZESTI Coreutils Experiments

[Anton Vasilyev]

Hello,

I'm interesting in integration KLEE with version control (e.g. git). It
seems to be similar with project ZESTI.
But due to lack of ZESTI documentation it requires source investigation
before using.


First I tried to reproduce ZESTI Coreutils Experiment and faced with
several mistypes in bash script "run-test.sh" published at
http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html

---------
#!/bin/bash

-if [ "X$1" == X ]; then
+if [ "X$1" == "X" ]; then
echo "Usage: $0 <executable> [test folder] [tests]"
else
- if [ "X$2" == X ]; then
+ if [ "X$2" == "X" ]; then
TDIR=$1
else
TDIR=$2
fi
fi

cd src

-for f in \*.bc; do
+for f in *.bc; do
fsimple=${f%.*}
rm -f $fsimple

- if [ -x /bin/$fsimple ]; then
+ if [ -x "/bin/$fsimple" ]; then
ln -s /bin/$fsimple
- elif [ -x /usr/bin/$fsimple ]; then
+ elif [ -x "/usr/bin/$fsimple" ]; then
ln -s /usr/bin/$fsimple
fi
done

rm -f $1

cd ..
sed "s/TEMPLATE-EXE/$1/g" zesti.tmpl > src/$1
chmod 755 src/$1

if [ "X$3" == "X" ]; then
make check -C tests/$TDIR/
else
make check -C tests/$TDIR/ "TESTS=$3"
fi
---------


I have several questions:

1. Whether it is necessary to replace compiled coreutils-6.11/src with
links to installed on system?
2. Is it correct that we need to mark patch by functions
"klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?



--
With best regards,
Anton Vasilyev

[Jonathan Neuschäfer]

On Tue, Jun 25, 2013 at 03:41:59PM +0400, Anton Vasilyev wrote:
> Hello,
>
> I'm interesting in integration KLEE with version control (e.g. git).
> It seems to be similar with project ZESTI.

You can get a version controlled copy of the KLEE source code either
with:
git clone http://llvm.org/git/klee.git
or with:
svn co http://llvm.org/svn/llvm-project/klee/trunk klee

[...]
> 1. Whether it is necessary to replace compiled coreutils-6.11/src with
> links to installed on system?

I am not sure what you mean, but the coreutils package installed on your
system will not be tested by any KLEE or ZESTI experiment.

> 2. Is it correct that we need to mark patch by functions
> "klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?

I haven't read enough of the ZESTI source code to answer that question,
sorry.


HTH,
Jonathan Neuschäfer

[Anton Vasilyev]

2013/6/25 Jonathan Neuschäfer <j.neuschaefer-***@public.gmane.org>

> On Tue, Jun 25, 2013 at 03:41:59PM +0400, Anton Vasilyev wrote:
> > Hello,
> >
> > I'm interesting in integration KLEE with version control (e.g. git).
> > It seems to be similar with project ZESTI.
>
> You can get a version controlled copy of the KLEE source code either
> with:
> git clone http://llvm.org/git/klee.git
> or with:
> svn co http://llvm.org/svn/llvm-project/klee/trunk klee
>

I mean not to get klee.git, but integrate patch testing as described at
publication "High-Coverage Symbolic Patch Testing" (
http://www.doc.ic.ac.uk/~cristic/papers/highcovpatch-spin-12.pdf)
for native git patch syntax.
ZESTI project contains "klee_patch_begin()" and "klee_patch_end()"
implementation.
But it is not clear whether ZESTI is the same project relative to the
publication.


> [...]
> > 1. Whether it is necessary to replace compiled coreutils-6.11/src with
> > links to installed on system?
>
> I am not sure what you mean, but the coreutils package installed on your
> system will not be tested by any KLEE or ZESTI experiment.
>

This is done by ZESTI provided script at
http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html for "setup the
wrapper for a particular program and run the tests" by following lines:

if [ -x /bin/$fsimple ]; then
ln -s /bin/$fsimple
elif [ -x /usr/bin/$fsimple ]; then
ln -s /usr/bin/$fsimple

Probably regression tests invoke not only application under testing (as
"cut" in example) but also other coreutils binaries.
In this case it is strange to link system package instead of compile
coreutils-6.11 with native gcc at separate location and link these binaries
to zesti testing directory.

> 2. Is it correct that we need to mark patch by functions
> > "klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?
>
> I haven't read enough of the ZESTI source code to answer that question,
> sorry.
>
>
> HTH,
> Jonathan Neuschäfer
>



--
With best regards,
Anton Vasilyev

[Urmas Repinski]

Hello, Anton.

> But it is not clear whether ZESTI is the same project relative to the publication.

Maybe it is worth to investigate ZESTI a little more?

Project page is
http://srg.doc.ic.ac.uk/projects/zesti/
Some additional information can be surely found at
http://www.doc.ic.ac.uk/~cristic/papers/zesti-icse-12.pdf

This can really improve your progress with integration,
Urmas Repinski.

Date: Tue, 25 Jun 2013 17:52:36 +0400
From: anton.vasilyev.87-***@public.gmane.org
To: j.neuschaefer-***@public.gmane.org
CC: klee-dev-AQ/***@public.gmane.org
Subject: Re: [klee-dev] [klee] [zesti] ZESTI Coreutils Experiments


2013/6/25 Jonathan Neuschäfer <j.neuschaefer-***@public.gmane.org>

On Tue, Jun 25, 2013 at 03:41:59PM +0400, Anton Vasilyev wrote:

> Hello,

>

> I'm interesting in integration KLEE with version control (e.g. git).

> It seems to be similar with project ZESTI.



You can get a version controlled copy of the KLEE source code either

with:

git clone http://llvm.org/git/klee.git

or with:

svn co http://llvm.org/svn/llvm-project/klee/trunk klee

I mean not to get klee.git, but integrate patch testing as described at publication "High-Coverage Symbolic Patch Testing" (http://www.doc.ic.ac.uk/~cristic/papers/highcovpatch-spin-12.pdf)
for native git patch syntax.ZESTI project contains "klee_patch_begin()" and "klee_patch_end()" implementation.But it is not clear whether ZESTI is the same project relative to the publication.

[...]

> 1. Whether it is necessary to replace compiled coreutils-6.11/src with

> links to installed on system?



I am not sure what you mean, but the coreutils package installed on your

system will not be tested by any KLEE or ZESTI experiment.

This is done by ZESTI provided script at http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html for "setup the wrapper for a particular program and run the tests" by following lines:

if [ -x /bin/$fsimple ]; then
ln -s /bin/$fsimple
elif [ -x /usr/bin/$fsimple ]; then
ln -s /usr/bin/$fsimple
Probably regression tests invoke not only application under testing (as "cut" in example) but also other coreutils binaries.
In this case it is strange to link system package instead of compile coreutils-6.11 with native gcc at separate location and link these binaries to zesti testing directory.


> 2. Is it correct that we need to mark patch by functions

> "klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?



I haven't read enough of the ZESTI source code to answer that question,

sorry.





HTH,

Jonathan Neuschäfer



--
With best regards,

Anton Vasilyev

[Jonathan Neuschäfer]

On Tue, Jun 25, 2013 at 05:52:36PM +0400, Anton Vasilyev wrote:
[...]
> This is done by ZESTI provided script at
> http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html for "setup the
> wrapper for a particular program and run the tests" by following lines:
>
> if [ -x /bin/$fsimple ]; then
> ln -s /bin/$fsimple
> elif [ -x /usr/bin/$fsimple ]; then
> ln -s /usr/bin/$fsimple

I missed that, sorry.

> Probably regression tests invoke not only application under testing (as
> "cut" in example) but also other coreutils binaries.
> In this case it is strange to link system package instead of compile
> coreutils-6.11 with native gcc at separate location and link these binaries
> to zesti testing directory.

I'd guess it is done this way, because the system binaries are simply
assumed to work correctly (enough), so that recompiling them would not
help, but just waste CPU time.


--
Jonathan Neuschäfer

[Paul Marinescu]

Hello Anton,
From your emails, it doesn't seem that ZESTI is what you're looking for. The paper that you mention is related to KATCH (http://srg.doc.ic.ac.uk/projects/katch/), which is a different project. We don't currently offer KATCH for download but we might do so in the near future; we'll also post early next week a more comprehensive paper on this topic.

If you have further questions specific to KATCH, you can directly send them to me.

Best,
Paul

P.S.
Thanks for spotting the typos on the coreutils page.

On 25 Jun 2013, at 14:52, Anton Vasilyev <anton.vasilyev.87-***@public.gmane.org> wrote:

>
> 2013/6/25 Jonathan Neuschäfer <j.neuschaefer-***@public.gmane.org>
> On Tue, Jun 25, 2013 at 03:41:59PM +0400, Anton Vasilyev wrote:
> > Hello,
> >
> > I'm interesting in integration KLEE with version control (e.g. git).
> > It seems to be similar with project ZESTI.
>
> You can get a version controlled copy of the KLEE source code either
> with:
> git clone http://llvm.org/git/klee.git
> or with:
> svn co http://llvm.org/svn/llvm-project/klee/trunk klee
>
> I mean not to get klee.git, but integrate patch testing as described at publication "High-Coverage Symbolic Patch Testing" (http://www.doc.ic.ac.uk/~cristic/papers/highcovpatch-spin-12.pdf)
> for native git patch syntax.
> ZESTI project contains "klee_patch_begin()" and "klee_patch_end()" implementation.
> But it is not clear whether ZESTI is the same project relative to the publication.
>
> [...]
> > 1. Whether it is necessary to replace compiled coreutils-6.11/src with
> > links to installed on system?
>
> I am not sure what you mean, but the coreutils package installed on your
> system will not be tested by any KLEE or ZESTI experiment.
>
> This is done by ZESTI provided script at http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html for "setup the wrapper for a particular program and run the tests" by following lines:
>
> if [ -x /bin/$fsimple ]; then
> ln -s /bin/$fsimple
> elif [ -x /usr/bin/$fsimple ]; then
> ln -s /usr/bin/$fsimple
>
> Probably regression tests invoke not only application under testing (as "cut" in example) but also other coreutils binaries.
> In this case it is strange to link system package instead of compile coreutils-6.11 with native gcc at separate location and link these binaries to zesti testing directory.
>
> > 2. Is it correct that we need to mark patch by functions
> > "klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?
>
> I haven't read enough of the ZESTI source code to answer that question,
> sorry.
>
>
> HTH,
> Jonathan Neuschäfer
>
>
>
> --
> With best regards,
> Anton Vasilyev

[Jonathan Neuschäfer]

On Tue, Jun 25, 2013 at 05:35:34PM +0100, Paul Marinescu wrote:
> Hello Anton,
> From your emails, it doesn't seem that ZESTI is what you're looking
> for. [...]

But what is the purpose of klee_patch_begin/_end in ZESTI?


Best regards,
Jonathan Neuschäfer

[Paul Marinescu]

The idea with klee_patch_begin/end was to allow developers to annotate code blocks inside the program (originally patches) which they want to be more thoroughly tested by ZESTI. We didn't pursue it much further because it's a bit cumbersome from the developer's perspective. KATCH instead, pulls this information from the version control system. We never got to port this functionality back to ZESTI though.

Paul

On 25 Jun 2013, at 18:00, Jonathan Neuschäfer <j.neuschaefer-***@public.gmane.org> wrote:

> On Tue, Jun 25, 2013 at 05:35:34PM +0100, Paul Marinescu wrote:
>> Hello Anton,
>> From your emails, it doesn't seem that ZESTI is what you're looking
>> for. [...]
>
> But what is the purpose of klee_patch_begin/_end in ZESTI?
>
>
> Best regards,
> Jonathan Neuschäfer