Both timeout and return value of imx_gpt_update_count() are unsigned.
Thus "limit" can not be negative, but obviously it was implied.

Found by Linux Verification Center (linuxtesting.org) with SVACE.

Signed-off-by: Dmitry Frolov <frolov@swemel.ru>
---
 hw/timer/imx_gpt.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hw/timer/imx_gpt.c b/hw/timer/imx_gpt.c
index 23b3d79bdb..06e4837fed 100644
--- a/hw/timer/imx_gpt.c
+++ b/hw/timer/imx_gpt.c
@@ -238,7 +238,7 @@ static void imx_gpt_compute_next_timeout(IMXGPTState *s, bool event)
     }
 
     /* the new range to count down from */
-    limit = timeout - imx_gpt_update_count(s);
+    limit = (long long)timeout - imx_gpt_update_count(s);
 
     if (limit < 0) {
         /*
-- 
2.43.0

On Wed, 6 Nov 2024 at 10:41, Dmitry Frolov <frolov@swemel.ru> wrote:
>
> Both timeout and return value of imx_gpt_update_count() are unsigned.
> Thus "limit" can not be negative, but obviously it was implied.

For changes to device models, you need to look at the
data sheet for the device to determine the correct
behaviour so you can confirm that the change you're
making is right. This commit message doesn't include
any of that reasoning, which means reviewers have to
do it all for themselves.

> Found by Linux Verification Center (linuxtesting.org) with SVACE.
>
> Signed-off-by: Dmitry Frolov <frolov@swemel.ru>
> ---
>  hw/timer/imx_gpt.c | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
>
> diff --git a/hw/timer/imx_gpt.c b/hw/timer/imx_gpt.c
> index 23b3d79bdb..06e4837fed 100644
> --- a/hw/timer/imx_gpt.c
> +++ b/hw/timer/imx_gpt.c
> @@ -238,7 +238,7 @@ static void imx_gpt_compute_next_timeout(IMXGPTState *s, bool event)
>      }
>
>      /* the new range to count down from */
> -    limit = timeout - imx_gpt_update_count(s);
> +    limit = (long long)timeout - imx_gpt_update_count(s);

We really shouldn't be using "long long" here in the
first place. If we need a 64-bit signed integer to
give correct behaviour then that's int64_t. Almost
all the handful of uses of 'long long' in hw/ are
doing it just as a lazy way to avoid PRIx64 in a
printf format string.

The GPT has a 32-bit up-counter. If timeout is, for
instance, 0x9000_0000 and the current count is
0x2000_0000 then we want the new "limit" value to
be 0x7000_0000 because we still have 0x7000_0000
cycles to go til we hit the next point where we want
to generate a compare event. So I think we do indeed
want to cast to a 64-bit signed value here.

(More broadly I think the problem with this device is
that it's trying to use ptimer (which is a down-counter)
to model an up-counter. This doesn't work very well,
and it's better to not do that. Arguably we should have
some nicer abstractions over raw qtimers for the
up-counter case and/or get ptimer to handle that
too, but that's a lot of work...)

thanks
-- PMM

Hello, Peter.
I beg a pardon, but I guess, we have a misunderstanding here.

The problem is that comparison "if (limit < 0)" will never
be true. Thus, "true" branch is unreachable. According to
the comment below, it was assumed that "limit" may be
negative, and this means, that "QEMU is running too slow...".

"limit" is declared as "long long" and it is initialized
with diff of two unsigned values:
"timeout - imx_gpt_update_count(s)".
Unsigned subtraction will never give a signed result!
if timeout > imx_gpt_update_count(s), the result will be > 0.
if timeout < imx_gpt_update_count(s), the result will also
be > 0 (underflow). Then, actually, this (positive) result
will be implicitly casted to "long long" and assigned to
"limit". This makes no sense!

So, to my opinion, explicit cast to "long long" is necessary
here to get the expected behavior.

With best regards,
Dmitry.

On Tue, 14 Jan 2025 at 06:41, Дмитрий Фролов <frolov@swemel.ru> wrote:
>
> Hello, Peter.
> I beg a pardon, but I guess, we have a misunderstanding here.
>
> The problem is that comparison "if (limit < 0)" will never
> be true. Thus, "true" branch is unreachable. According to
> the comment below, it was assumed that "limit" may be
> negative, and this means, that "QEMU is running too slow...".
>
> "limit" is declared as "long long" and it is initialized
> with diff of two unsigned values:
> "timeout - imx_gpt_update_count(s)".
> Unsigned subtraction will never give a signed result!
> if timeout > imx_gpt_update_count(s), the result will be > 0.
> if timeout < imx_gpt_update_count(s), the result will also
> be > 0 (underflow). Then, actually, this (positive) result
> will be implicitly casted to "long long" and assigned to
> "limit". This makes no sense!
>
> So, to my opinion, explicit cast to "long long" is necessary
> here to get the expected behavior.

I wasn't saying the existing code was necessarily correct,
or that your proposed change was necessarily wrong.
I was saying your patch didn't come with any analysis of
what the actual hardware behaviour is, which is
how you would determine whether the fix you propose
is the correct one, or if it should be some other
change instead. (Some of my response was trying to
provide some of that analysis.)

thanks
-- PMM

On 1/14/25 11:14, Peter Maydell wrote:
>> So, to my opinion, explicit cast to "long long" is necessary
>> here to get the expected behavior.
> 
> I wasn't saying the existing code was necessarily correct,
> or that your proposed change was necessarily wrong.
> I was saying your patch didn't come with any analysis of
> what the actual hardware behaviour is, which is
> how you would determine whether the fix you propose
> is the correct one, or if it should be some other
> change instead. (Some of my response was trying to
> provide some of that analysis.)
I would say that the patch is more or less obvious in the sense that the 
intent of the code is to model a counter (which counts up by 1 and 
cannot miss a step) with a timer within a process that could be 
preempted.  You probably will not find an answer in the datasheet, other 
than by analyzing the signal diagrams, because this scenario simply 
cannot exist with a hardware counter.

However, the patch has another problem, which is that it can cause a 
stack overflow at imx_gpt_compute_next_timeout(s, event).

Paolo

On Tue, 14 Jan 2025 at 10:40, Paolo Bonzini <pbonzini@redhat.com> wrote:
>
> On 1/14/25 11:14, Peter Maydell wrote:
> >> So, to my opinion, explicit cast to "long long" is necessary
> >> here to get the expected behavior.
> >
> > I wasn't saying the existing code was necessarily correct,
> > or that your proposed change was necessarily wrong.
> > I was saying your patch didn't come with any analysis of
> > what the actual hardware behaviour is, which is
> > how you would determine whether the fix you propose
> > is the correct one, or if it should be some other
> > change instead. (Some of my response was trying to
> > provide some of that analysis.)
> I would say that the patch is more or less obvious in the sense that the
> intent of the code is to model a counter (which counts up by 1 and
> cannot miss a step) with a timer within a process that could be
> preempted.  You probably will not find an answer in the datasheet, other
> than by analyzing the signal diagrams, because this scenario simply
> cannot exist with a hardware counter.

Well, for a start, you want to look at the datasheet
to check that this really is modelling a counter and
how wide the counter is (32 bits in this case).

thanks
-- PMM

Hi Dmitry,

On 6/11/24 11:40, Dmitry Frolov wrote:
> Both timeout and return value of imx_gpt_update_count() are unsigned.
> Thus "limit" can not be negative, but obviously it was implied.
> 
> Found by Linux Verification Center (linuxtesting.org) with SVACE.
> 
> Signed-off-by: Dmitry Frolov <frolov@swemel.ru>
> ---
>   hw/timer/imx_gpt.c | 2 +-
>   1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/hw/timer/imx_gpt.c b/hw/timer/imx_gpt.c
> index 23b3d79bdb..06e4837fed 100644
> --- a/hw/timer/imx_gpt.c
> +++ b/hw/timer/imx_gpt.c
> @@ -238,7 +238,7 @@ static void imx_gpt_compute_next_timeout(IMXGPTState *s, bool event)
>       }
>   
>       /* the new range to count down from */
> -    limit = timeout - imx_gpt_update_count(s);
> +    limit = (long long)timeout - imx_gpt_update_count(s);

You posted similar automatic change in at least 3 different
code areas. Each time different maintainers made similar
comments. At this point you should be able to auto-review
this patch and respin a proper follow up IMHO. Reviewers and
maintainers time is scarce.

Regards,

Phil.

Hi, Phil.

On 26.11.2024 11:39, Philippe Mathieu-Daudé wrote:
> Hi Dmitry,
>
> On 6/11/24 11:40, Dmitry Frolov wrote:
>> Both timeout and return value of imx_gpt_update_count() are unsigned.
>> Thus "limit" can not be negative, but obviously it was implied.
>>
>> Found by Linux Verification Center (linuxtesting.org) with SVACE.
>>
>> Signed-off-by: Dmitry Frolov <frolov@swemel.ru>
>> ---
>>   hw/timer/imx_gpt.c | 2 +-
>>   1 file changed, 1 insertion(+), 1 deletion(-)
>>
>> diff --git a/hw/timer/imx_gpt.c b/hw/timer/imx_gpt.c
>> index 23b3d79bdb..06e4837fed 100644
>> --- a/hw/timer/imx_gpt.c
>> +++ b/hw/timer/imx_gpt.c
>> @@ -238,7 +238,7 @@ static void 
>> imx_gpt_compute_next_timeout(IMXGPTState *s, bool event)
>>       }
>>         /* the new range to count down from */
>> -    limit = timeout - imx_gpt_update_count(s);
>> +    limit = (long long)timeout - imx_gpt_update_count(s);
>
> You posted similar automatic change in at least 3 different
> code areas.
The patches, I've sent, are not "automatic".
The problems were found by static analyzer in different code
areas, maintained by different people. These problems were
reviewed and fixed by me manually.
> Each time different maintainers made similar
> comments. At this point you should be able to auto-review
> this patch and respin a proper follow up IMHO. Reviewers and
> maintainers time is scarce.
Sorry, if do something wrong.
What is the proper workflow in this case from your point of view?

> Regards,
>
> Phil.

Regards,
Dmitry.
>

ping