[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <20260217144201.GX1827@brightrain.aerifal.cx>
Date: Tue, 17 Feb 2026 09:42:05 -0500
From: Rich Felker <dalias@...c.org>
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" <musl@...ts.openwall.com>,
"Mahmoud Ahmad Alawneh [C]" <mahmoud@...ence.com>
Subject: Re: 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
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.
