[klee-dev] Confusions about coreutils experiments

[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

On 05/11/2013 10:00, Hongxu Chen wrote:
> 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
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>