[klee-dev] Confusions about coreutils experiments

[Hongxu Chen]

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


On Fri, Nov 8, 2013 at 7:10 PM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:

> 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
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed