linux-kernel - Re: [PATCH 17/26] rv/rvgen: fix possibly unbound variable in ltl2k

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <3507c2f454ca66aa27dd3a24e33f5941fac96639.camel@redhat.com>
Date: Tue, 20 Jan 2026 13:30:35 +0100
From: Gabriele Monaco <gmonaco@...hat.com>
To: Wander Lairson Costa <wander@...hat.com>
Cc: Steven Rostedt <rostedt@...dmis.org>, Nam Cao <namcao@...utronix.de>, 
 open list <linux-kernel@...r.kernel.org>, "open list:RUNTIME VERIFICATION
 (RV)"	 <linux-trace-kernel@...r.kernel.org>
Subject: Re: [PATCH 17/26] rv/rvgen: fix possibly unbound variable in ltl2k

On Tue, 2026-01-20 at 08:37 -0300, Wander Lairson Costa wrote:
> On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:
> > On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
> > > Initialize loop variable `i` before the for loop in abbreviate_atoms
> > > function to fix pyright static type checker error. The previous code
> > > left `i` potentially unbound in edge cases where the range could be
> > > empty, though this would not occur in practice since the loop always
> > > executes at least once with the given range parameters.
> > > 
> > > The initialization to zero ensures that `i` has a defined value before
> > > entering the loop scope, satisfying static analysis requirements
> > > while preserving the existing logic. The for loop immediately assigns
> > > i to the first value from the range, so the initialization value is
> > > never actually used in normal execution paths.
> > > 
> > > This change resolves the pyright reportPossiblyUnbound error without
> > > altering the function's behavior or performance characteristics.
> > 
> > So are we just pleasing the tool or is there a real implication of this?
> > 
> > Apparently code like
> > 
> > for i in range(len([]), -1, -1):
> >     pass
> > print(i)
> > 
> > works just fine since range() returns at least 0 (as you mentioned in the
> > commit
> > message) and i is not used before assignation in the loop, so I don't really
> > see
> > a problem.
> > 
> > Apparently pyright devs don't want ([1]) to implement a logic to sort out
> > the
> > /possibly/ unbound error here.
> > 
> > From what I understand, this code is already not pythonic, so rather than
> > silence the warning to please this tool I'd just refactor the code not to
> > use i
> > after the loop (or leave it as it is, since it works fine).
> > 
> > What do you think?
> 
> You're right, I could have done:
> 
> for atom in reversed(atoms): ...
> 

I'm missing what you mean with this, the range is iterating over the string
representation of atom (in reverse) not the array of atoms.

You basically want i to be the length of the longest prefix common to at least
another atom.

You could assign i to some python trick doing the exact same thing the loop
does, like:

    i = next((i for i in range(len(atom), -1, -1)
        if sum(a.startswith(atom[:i]) for a in atoms) > 1))

next() is basically doing the break at the first occurrence from the generator,
just now your i doesn't live (only) inside the loop.

So now you save 2 lines and get any C developer scratch their head when they
look at the code, but hey, pyright is happy!

If you do find the trick with next() readable or have any better idea, feel free
to try though.

Thanks,
Gabriele

> I will modify it in v2.
> 
> > 
> > Thanks,
> > Gabriele
> > 
> > [1] - https://github.com/microsoft/pyright/issues/844
> > 
> > > 
> > > Signed-off-by: Wander Lairson Costa <wander@...hat.com>
> > > ---
> > >  tools/verification/rvgen/rvgen/ltl2k.py | 1 +
> > >  1 file changed, 1 insertion(+)
> > > 
> > > diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> > > b/tools/verification/rvgen/rvgen/ltl2k.py
> > > index fa9ea6d597095..94dc64af1716d 100644
> > > --- a/tools/verification/rvgen/rvgen/ltl2k.py
> > > +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> > > @@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
> > >  
> > >      abbrs = []
> > >      for atom in atoms:
> > > +        i = 0
> > >          for i in range(len(atom), -1, -1):
> > >              if sum(a.startswith(atom[:i]) for a in atoms) > 1:
> > >                  break
> >