[<prev] [<thread-prev] [day] [month] [year] [list]
Message-ID: <CAH8yC8nNssf5GWeJPLRY-ZXHOpvPb5rrS8o79V3LAmMnLcYQ9w@mail.gmail.com>
Date: Wed, 18 Feb 2026 12:12:40 -0500
From: Jeffrey Walton <noloader@...il.com>
To: musl@...ts.openwall.com
Cc: Cesar Rodriguez <rcesar@...ence.com>, "Mariam Flayyan [C]" <mariamf@...ence.com>,
"Mahmoud Ahmad Alawneh [C]" <mahmoud@...ence.com>
Subject: Re: RE: Concerns about MUSL sqrt function math implementation
in Formal Verification
Be careful of your choice of words:
> I think that relying on the compiler behavior in case of
> arithmetic overflow is not related to style guidelines ...
Integer wrap using unsigned types is well defined in C. Arithmetic
overflow using signed types is undefined behavior in C. Use of undefined
behavior needs to be fixed.
Jeff
On Wed, Feb 18, 2026 at 11:16 AM Ayman Hanna <ayman@...ence.com> wrote:
> Thank you for the detailed answer.
> I think that relying on the compiler behavior in case of arithmetic
> overflow is not related to style guidelines, but as it is getting the
> expected behavior, I agree that it is not a bogus code. We will continue
> testing and will approach you again if we will find more critical issues.
> Your fast and professional response is highly appreciated.
>
> Best regards,
> Ayman
>
> -----Original Message-----
> From: Rich Felker <dalias@...c.org>
> Sent: Tuesday, February 17, 2026 4:42 PM
> To: Ayman Hanna <ayman@...ence.com>
> Cc: Thorsten Glaser <tg@...bsd.de>; Cesar Rodriguez <rcesar@...ence.com>;
> Mariam Flayyan [C] <mariamf@...ence.com>; musl@...ts.openwall.com;
> Mahmoud Ahmad Alawneh [C] <mahmoud@...ence.com>
> Subject: Re: [musl] RE: Concerns about MUSL sqrt function math
> implementation in Formal Verification
>
> On Tue, Feb 17, 2026 at 12:27:09PM +0000, Ayman Hanna wrote:
> > Hi Glaser,
> >
> > Let me clarify.
> > We are running our linting tool (based on formal verification) on musl
> > code (no AI usage is done here), and we are finding some issues,
> > specifically, in the sqrt function code we found ~10 linting problems.
> > The problem Mahmoud is referring to here bellow is happening when sqrt
> > is getting 0 as input, the (if you go to musl internal implementation
> > of the function) ix will be also 0, and top becomes 0 as well.
>
> The test case code submitted was completely invalid LLM-slop and does not
> demonstrate anything because its behavior is entirely undefined.
>
> > In the line highlighted in the screenshot below (line 32), the code is
> > doing top-0x001, as both operands are unsigned, and according to the C
> > language specification the result is unsigned, but when top is
> > 0 there will be an overflow, and the value will be max unsigned
> > instead of -1.
> > We would like to hear your opinion about this specific case, is it
> > considered a bug in the implementation, or it is a safe code?
>
> The code is doing exactly what it was intended to do, and the behavior is
> well-defined by the C language. C unsigned arithmetic is modular
> arithmetic, modulo one plus the max value of the type. If top is 0, the
> condition top - 0x001 >= 0x7ff - 0x001 will be true, and the special case
> path for handling denormals, infs, and nans will be taken.
>
> > And more generally, we are going to test all musl code using our tool,
> > should we report the issues found to musl support? Do you/they have a
> > bandwidth to analyze our reports?
>
> If the tool is identifying actual flaws and you can confirm they're flaws,
> you're welcome to report this. If it's just reporting that musl source does
> not meet your style guidelines, that's expected; we don't know or use your
> style guidelines.
>
> Rich
>
Content of type "text/html" skipped
Powered by blists - more mailing lists
Confused about mailing lists and their use?
Read about mailing lists on Wikipedia
and check out these
guidelines on proper formatting of your messages.
