[klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

[TU Haoxin]

Hi Daniel,

Thanks for your further investigation. Your explanation makes sense to me.

I started my project a few years ago so I used a relatively older version of KLEE&LLVM. I believe I will build on my next project on the newest versions of them to avoid similar issues and catch up with KLEE's new features.

Thank you very much again for your help and continuous contributions to making KLEE more and more powerful! Have a great week ahead!


Best regards,
Haoxin
________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Daniel Schemmel <d.schemmel at imperial.ac.uk>
Sent: Thursday, February 1, 2024 7:26
To: klee-dev at imperial.ac.uk <klee-dev at imperial.ac.uk>
Subject: Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option


Hi Haoxin,


The described behavior is indeed very odd. Luckily, the `assembly.ll` that is generated by KLEE shows that this is an actual optimization error - the code that is intended to print your messages does not exist anymore. This means that the issue lies either with the LLVM optimization passes, or in our usage of them.


As you were using fairly old LLVM versions (LLVM 9 & 10 support is about to be removed from KLEE<https://github.com/klee/klee/pull/1686>), I tried to reproduce the issue in a few different configurations:

- LLVM 9 (KLEE master): REPRODUCED

- LLVM 10 (KLEE master): REPRODUCED
- LLVM 11 (KLEE master): NOT reproduced
- LLVM 12 (KLEE master): NOT reproduced

- LLVM 13 (docker.io/klee/klee): NOT reproduced
- LLVM 14 (KLEE master): NOT reproduced
- LLVM 15 (#1664<https://github.com/klee/klee/pull/1664>): NOT reproduced
- LLVM 16 (#1664<https://github.com/klee/klee/pull/1664>): requires an additional include in xmalloc.c to compile; NOT reproduced


Since this bug only occurs with the two LLVM versions that are about to be removed in the next few days anyway, and there is a hard break (none of the newer versions exhibit the same behavior), I tend towards assuming that this specific issue probably stems from an old LLVM bug that has since been rectified.


Best,
Daniel


On 2024-01-31 06:58, TU Haoxin wrote:
Hi Nguyen,

Just installed and run this case using KLEE-3.0 with LLVM-10, and it seems the issue is still reproducible for KLEE 3.

Please check more here: https://gist.github.com/haoxintu/183dda2923965d1e33f64ad59c7f5338#other-trials


Thanks,
Haoxin



________________________________
From: Nguyễn Gia Phong
Sent: Wednesday, January 31, 2024 13:34
To: TU Haoxin; klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
Subject: Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

On 2024-01-31 at 05:07+00:00, TU Haoxin wrote:
> The behavior is that KLEE fails to fork at a branch
> that should be forked with the option --optimize option enabled
> (i.e., --optimize=true).  While the --optimize option is disabled
> i.e., --optimize=false), the branch can be successfully forked [...]
>
> ### Reproduce the behavior
> #### Enviroment
> * KLEE-2.1 (also tested KLEE-2.3, and they behave the same)

Just curious, is the issue reproducible for KLEE 3?



_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed