[klee-dev] Confusions about coreutils experiments

[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 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
-------------- next part --------------
HTML attachment scrubbed and removed