Confusions about coreutils experiments

Discussion:

Hongxu Chen

2013-11-05 10:00:08 UTC

Hi,

I'm trying to reproduce the coreutils results in klee08 paper(klee "make
check" has been passed).

We were following KLEE "Coreutils Experiments" page(
http://ccadar.github.io/klee/CoreutilsExperiments.html). And the major
variants are:

1. used KLEE svn r165499 rather than revisions before r161056, and I got
STP from KLEE "Getting Started" page(
http://ccadar.github.io/klee/GetStarted.html).
2. used coreutils-6.10 rather than 6.11.
3. didn't use "--environ=test.env" and "--run-in=/tmp/sandbox"; also
customized a "--output-dir" option. (I guess these are really trivial
changes)

The 89 cases are running on a x86_64 machine whose OS is ubuntu12.04
LTS. And here is some extra information about it:

1. > sudo fdisk -l

Disk /dev/sda: 250.0 GB, 250000000000 bytes
255 heads, 63 sectors/track, 30394 cylinders, total 488281250 sectors
Units = sectors of 1 * 512 = 512 bytes
Sector size (logical/physical): 512 bytes / 512 bytes
I/O size (minimum/optimal): 512 bytes / 512 bytes
Disk identifier: 0x00039844

Device Boot Start End Blocks Id System
/dev/sda1 * 2048 480026623 240012288 83 Linux
/dev/sda2 480028670 488280063 4125697 5 Extended
/dev/sda5 480028672 488280063 4125696 82 Linux swap / Solaris

2. > grep "model name" /proc/cpuinfo
model name : Intel(R) Core(TM)2 CPU 6400 @ 2.13GHz
model name : Intel(R) Core(TM)2 CPU 6400 @ 2.13GHz

We ran the cases for 3 times, and it took several days(sorry I didn't get
the exact hours); I noticed some results with the help of "klee-stats
--print-all" for each case:

1. There are several "*.external.err", and the failed external calls are
"__overflow" and "__uflow". they both result from
"/usr/include/bits/stdio.h" of Line 66, however I didn't find any
defitinition of them.

2. For those cases that KLEE halts without any external function fail, I
find KLEE halt mainly because they are timed-out(I infer this since the
"Time" results are typically a bit larger than "3600"). Should I increase
the "--max-time" number?

3. The *ICov* and *BCov* I run isn't quite high(the highest are about 45%
and 35% respectively). Should I trust the statistics or I am using the
wrong results?

4. "TSolver" still occupies most of the time(most of them are above 98%
and the lowest is 95.23%).

I believe I must have missed something and might have configured
incorrectly.

So I really need your kind help; any advice will be appreciated, thanks in
advance!

Best Regards,
Hongxu Chen

Cristian Cadar

2013-11-08 11:10:22 UTC

Permalink

Hi Hongxu,

You would need to debug the __overflow issue; could you also open an
issue on GitHub?

It is important to read the info on that webpage and follow the
instructions there. Coverage numbers were obtained using replay+gcov,
as mentioned in the paper. (The KLEE stats are at the level of bitcode,
and also refer to library code.) Lei Zhang submitted a useful patch
that makes replaying easier; I still need to review it, but you can find
it at https://github.com/ccadar/klee/pull/31. There are also other
issues to take care when using gcov -- e.g, gcov doesn't record coverage
on _exit -- which might require small adjustments.

Cristian

Post by Hongxu Chen
Hi,
I'm trying to reproduce the coreutils results in klee08 paper(klee
"make check" has been passed).
We were following KLEE "Coreutils Experiments"
page(http://ccadar.github.io/klee/CoreutilsExperiments.html). And the
1. used KLEE svn r165499 rather than revisions before r161056, and I got
STP from KLEE "Getting Started"
page(http://ccadar.github.io/klee/GetStarted.html).
2. used coreutils-6.10 rather than 6.11.
3. didn't use "--environ=test.env" and "--run-in=/tmp/sandbox"; also
customized a "--output-dir" option. (I guess these are really trivial
changes)
The 89 cases are running on a x86_64 machine whose OS is ubuntu12.04
1. > sudo fdisk -l
Disk /dev/sda: 250.0 GB, 250000000000 bytes
255 heads, 63 sectors/track, 30394 cylinders, total 488281250 sectors
Units = sectors of 1 * 512 = 512 bytes
Sector size (logical/physical): 512 bytes / 512 bytes
I/O size (minimum/optimal): 512 bytes / 512 bytes
Disk identifier: 0x00039844
Device Boot Start End Blocks Id System
/dev/sda1 * 2048 480026623 240012288 83 Linux
/dev/sda2 480028670 488280063 4125697 5 Extended
/dev/sda5 480028672 488280063 4125696 82 Linux swap / Solaris
2. > grep "model name" /proc/cpuinfo
We ran the cases for 3 times, and it took several days(sorry I didn't
get the exact hours); I noticed some results with the help of
1. There are several "*.external.err", and the failed external calls are
"__overflow" and "__uflow". they both result from
"/usr/include/bits/stdio.h" of Line 66, however I didn't find any
defitinition of them.
2. For those cases that KLEE halts without any external function fail, I
find KLEE halt mainly because they are timed-out(I infer this since the
"Time" results are typically a bit larger than "3600"). Should I
increase the "--max-time" number?
3. The *ICov* and *BCov* I run isn't quite high(the highest are about
45% and 35% respectively). Should I trust the statistics or I am using
the wrong results?
4. "TSolver" still occupies most of the time(most of them are above 98%
and the lowest is 95.23%).
I believe I must have missed something and might have configured
incorrectly.
So I really need your kind help; any advice will be appreciated, thanks
in advance!
Best Regards,
Hongxu Chen
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Hongxu Chen

2013-11-08 11:55:19 UTC

Permalink

Mr. Cadar, thanks so much for your advice.

I later used the exact r165499 version(we personally changed it a bit,
although it's really trivial), and compiled coreutils bitcode without any
optimizations(seems that the default is -O2) they linked as klee-gcc
does(llvm-ld), then I didn't see such external functions in the cases I
used before(it's weird, really).

Also, thanks for the extra information and I'll open an issue when I meet
this issue once more.

Thanks,
Hongxu Chen

Post by Cristian Cadar
Hi Hongxu,
You would need to debug the __overflow issue; could you also open an issue
on GitHub?
It is important to read the info on that webpage and follow the
instructions there. Coverage numbers were obtained using replay+gcov, as
mentioned in the paper. (The KLEE stats are at the level of bitcode, and
also refer to library code.) Lei Zhang submitted a useful patch that makes
replaying easier; I still need to review it, but you can find it at
https://github.com/ccadar/klee/pull/31. There are also other issues to
take care when using gcov -- e.g, gcov doesn't record coverage on _exit --
which might require small adjustments.
Cristian

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev