[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" opti
From: Daniel Schemmel <d.schemmel () imperial ! ac ! uk>
Date: 2024-01-31 23:26:15
Message-ID: faa18127-5bc7-45f5-8a03-024f751441b3 () imperial ! ac ! uk
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
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
> <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@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@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[Attachment #5 (text/html)]
<!DOCTYPE html><html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<p>Hi Haoxin,</p>
<p><br>
</p>
<p>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.<br>
</p>
<p><br>
</p>
<p>As you were using fairly old LLVM versions (LLVM 9 & 10
support is about to be <a href="https://github.com/klee/klee/pull/1686">removed \
from KLEE</a>),
I tried to reproduce the issue in a few different configurations:<br>
</p>
<p><br>
- LLVM 9 (KLEE master): REPRODUCED</p>
<p>- LLVM 10 (KLEE master): REPRODUCED<br>
- LLVM 11 (KLEE master): NOT reproduced<br>
- LLVM 12 (KLEE master): NOT reproduced<br>
</p>
<p>- LLVM 13 (docker.io/klee/klee): NOT reproduced<br>
- LLVM 14 (KLEE master): NOT reproduced<br>
- LLVM 15 (<a moz-do-not-send="true" \
href="https://github.com/klee/klee/pull/1664">#1664</a>): NOT reproduced<br>
- LLVM 16 (<a href="https://github.com/klee/klee/pull/1664">#1664</a>):
requires an additional include in xmalloc.c to compile; NOT
reproduced</p>
<p><br>
</p>
<p>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.<br>
</p>
<p><br>
</p>
<p>Best,<br>
Daniel</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 2024-01-31 06:58, TU Haoxin wrote:<br>
</div>
<blockquote type="cite" \
cite="mid:SI2PR01MB38334EC8AA91772825A20606857C2@SI2PR01MB3833.apcprd01.prod.exchangelabs.com">
<style type="text/css" style="display:none;">P \
{margin-top:0;margin-bottom:0;}</style>
<span style="font-family: Aptos, Aptos_EmbeddedFont, Aptos_MSFontService, \
Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">Hi \
Nguyen,</span> <div style="text-align: left; margin: 0px;"><span style="font-family: \
Aptos, Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; \
font-size: 12pt; color: rgb(0, 0, 0);"><br> </span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);">Just installed and run this case using KLEE-3.0 with \
LLVM-10, and
it seems the issue is still reproducible for KLEE 3.</span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);"><br> </span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);">Please check more here: <a \
href="https://gist.github.com/haoxintu/183dda2923965d1e33f64ad59c7f5338#other-trials" \
id="OWAd5e7855c-2704-30d0-6dea-37b1ba685872" class="OWAAutoLink \
moz-txt-link-freetext" style="margin: 0px;" \
moz-do-not-send="true">https://gist.github.com/haoxintu/183dda2923965d1e33f64ad59c7f5338#other-trials</a></span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);"><br> </span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);"><br> </span></div>
<div style="text-align: left; margin: 0px;"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);">Thanks,</span></div> <div style="text-align: left; \
margin: 0px;" class="elementToProof"><span style="font-family: Aptos, \
Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);">Haoxin</span></div> <div class="elementToProof" \
style="font-family: Aptos, Aptos_EmbeddedFont, Aptos_MSFontService, Calibri, \
Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);"> <br>
</div>
<div><br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);"> <br>
</div>
<hr style="display: inline-block; width: 98%;">
<span style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: \
12pt; color: rgb(0, 0, 0);"><b>From:</b> Nguyá»
n Gia Phong<br>
<b>Sent:</b> Wednesday, January 31, 2024 13:34<br>
<b>To:</b> TU Haoxin; <a class="moz-txt-link-abbreviated" \
href="mailto:klee-dev@imperial.ac.uk">klee-dev@imperial.ac.uk</a><br>
<b>Subject:</b> Re: [klee-dev] Different behavior of KLEE when
testing `dircolors` with "--optimize=true/false" option
</span>
<div><span style="font-family: Calibri, Arial, Helvetica, sans-serif; \
font-size: 12pt; color: rgb(0, 0, 0);"><br> </span></div>
<div><span style="font-size: 11pt;">On 2024-01-31 at 05:07+00:00,
TU Haoxin wrote:<br>
> The behavior is that KLEE fails to fork at a branch<br>
> that should be forked with the option --optimize option
enabled<br>
> (i.e., --optimize=true). While the --optimize option is
disabled<br>
> i.e., --optimize=false), the branch can be successfully
forked [...]<br>
><br>
> ### Reproduce the behavior<br>
> #### Enviroment<br>
> * KLEE-2.1 (also tested KLEE-2.3, and they behave the
same)<br>
<br>
Just curious, is the issue reproducible for KLEE 3?<br>
</span></div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" \
wrap="">_______________________________________________ klee-dev mailing list
<a class="moz-txt-link-abbreviated" \
href="mailto:klee-dev@imperial.ac.uk">klee-dev@imperial.ac.uk</a> <a \
class="moz-txt-link-freetext" \
href="https://mailman.ic.ac.uk/mailman/listinfo/klee-dev">https://mailman.ic.ac.uk/mailman/listinfo/klee-dev</a>
</pre>
</blockquote>
</body>
</html>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic