[musl] Concerns about MUSL sqrt function math implementation in Formal Verification

[musl] Concerns about MUSL sqrt function math implementation in Formal Verification

[Mahmoud Ahmad Alawneh [C]]

[-- Attachment #1.1: Type: text/plain, Size: 1406 bytes --]

Hi MUSL team,
I am a Software Engineer at Cadence Design Systems working on Formal Verification for chip designs.
We use the MUSL math library in our internal code base and we detected issues from the math functions (specifically sqrt)
We have a linting app called "C Autoformal" aka CAF and we have noticed that we detect ArithmeticOverflow from sqrt function MUSL implementation.

When compiling the following code within our tool:

int main()
{
                int arr[3] = {1, 2, 3};
                int* ptr = arr;
                ptr += 4;
                int k = *ptr;
                double y = my_sqrt(k);
                return 0;
}

Attached below is a screenshot from out linting app (CAF), showing possible design overflows:
On the left panel: we show the possible overflow from the design (i.e: cpp_ArithmeticOverflow_3)
On the right panel: we show the source code line of the design that caused the overflow.

As you can see below, the detected ArithmeticOverflow points to a line (inside of math/sqrt.c : double sqrt(double x) ) that decreases 1 from top and then compares it to another value, this seems to cause ArithmeticOverflow:
[cid:image003.png@01DC9F65.AF9393F0]

We want to know if this would affect the effeciency of the math funcitons?
Should this be a top concern for us or is it something under control and should be ignored?


Regards,
Mahmoud


[-- Attachment #1.2: Type: text/html, Size: 5824 bytes --]

[-- Attachment #2: image003.png --]
[-- Type: image/png, Size: 121145 bytes --]

Re: [musl] Concerns about MUSL sqrt function math implementation in Formal Verification

[Thorsten Glaser]

On Mon, 16 Feb 2026, Mahmoud Ahmad Alawneh [C] wrote:

>int main()
>{
>                int arr[3] = {1, 2, 3};
>                int* ptr = arr;
>                ptr += 4;
>                int k = *ptr;

This is a dereference beyond array bounds. This is UB.

Are you using “AI” slop to test things or what?

bye,
//mirabilos
-- 
<ch> you introduced a merge commit        │<mika> % g rebase -i HEAD^^
<mika> sorry, no idea and rebasing just fscked │<mika> Segmentation
<ch> should have cloned into a clean repo      │  fault (core dumped)
<ch> if I rebase that now, it's really ugh     │<mika:#grml> wuahhhhhh

[musl] RE: Concerns about MUSL sqrt function math implementation in Formal Verification

[Ayman Hanna]

[-- Attachment #1.1: Type: text/plain, Size: 2792 bytes --]

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.
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?
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?

Thanks,
Ayman

From: Mahmoud Ahmad Alawneh [C] <mahmoud@cadence.com>
Sent: Monday, February 16, 2026 5:00 PM
To: musl@lists.openwall.com
Cc: Ayman Hanna <ayman@cadence.com>; Cesar Rodriguez <rcesar@cadence.com>; Mariam Flayyan [C] <mariamf@cadence.com>
Subject: Concerns about MUSL sqrt function math implementation in Formal Verification

Hi MUSL team,
I am a Software Engineer at Cadence Design Systems working on Formal Verification for chip designs.
We use the MUSL math library in our internal code base and we detected issues from the math functions (specifically sqrt)
We have a linting app called "C Autoformal" aka CAF and we have noticed that we detect ArithmeticOverflow from sqrt function MUSL implementation.

When compiling the following code within our tool:

int main()
{
                int arr[3] = {1, 2, 3};
                int* ptr = arr;
                ptr += 4;
                int k = *ptr;
                double y = my_sqrt(k);
                return 0;
}

Attached below is a screenshot from out linting app (CAF), showing possible design overflows:
On the left panel: we show the possible overflow from the design (i.e: cpp_ArithmeticOverflow_3)
On the right panel: we show the source code line of the design that caused the overflow.

As you can see below, the detected ArithmeticOverflow points to a line (inside of math/sqrt.c : double sqrt(double x) ) that decreases 1 from top and then compares it to another value, this seems to cause ArithmeticOverflow:
[cid:image001.png@01DCA017.0F0F1190]

We want to know if this would affect the effeciency of the math funcitons?
Should this be a top concern for us or is it something under control and should be ignored?


Regards,
Mahmoud


[-- Attachment #1.2: Type: text/html, Size: 9957 bytes --]

[-- Attachment #2: image001.png --]
[-- Type: image/png, Size: 121145 bytes --]

Re: [musl] RE: Concerns about MUSL sqrt function math implementation in Formal Verification

[Rich Felker]

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

RE: [musl] RE: Concerns about MUSL sqrt function math implementation in Formal Verification

[Ayman Hanna]

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@libc.org> 
Sent: Tuesday, February 17, 2026 4:42 PM
To: Ayman Hanna <ayman@cadence.com>
Cc: Thorsten Glaser <tg@mirbsd.de>; Cesar Rodriguez <rcesar@cadence.com>; Mariam Flayyan [C] <mariamf@cadence.com>; musl@lists.openwall.com; Mahmoud Ahmad Alawneh [C] <mahmoud@cadence.com>
Subject: Re: [musl] RE: Concerns about MUSL sqrt function math implementation in Formal Verification

EXTERNAL MAIL


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

Re: [musl] RE: Concerns about MUSL sqrt function math implementation in Formal Verification

[Jeffrey Walton]

[-- Attachment #1: Type: text/plain, Size: 3294 bytes --]

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@cadence.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@libc.org>
> Sent: Tuesday, February 17, 2026 4:42 PM
> To: Ayman Hanna <ayman@cadence.com>
> Cc: Thorsten Glaser <tg@mirbsd.de>; Cesar Rodriguez <rcesar@cadence.com>;
> Mariam Flayyan [C] <mariamf@cadence.com>; musl@lists.openwall.com;
> Mahmoud Ahmad Alawneh [C] <mahmoud@cadence.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
>

[-- Attachment #2: Type: text/html, Size: 4263 bytes --]