linux-kernel - [PATCH v2 15/20] rv/rvgen: fix isinstance check in Variable.expand()

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 for Android: free password hash cracker in your pocket

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

Message-ID: <20260204144914.104028-16-wander@redhat.com>
Date: Wed,  4 Feb 2026 11:42:41 -0300
From: Wander Lairson Costa <wander@...hat.com>
To: Steven Rostedt <rostedt@...dmis.org>,
	Gabriele Monaco <gmonaco@...hat.com>,
	Nam Cao <namcao@...utronix.de>,
	Wander Lairson Costa <wander@...hat.com>,
	linux-trace-kernel@...r.kernel.org (open list:RUNTIME VERIFICATION (RV)),
	linux-kernel@...r.kernel.org (open list)
Subject: [PATCH v2 15/20] rv/rvgen: fix isinstance check in Variable.expand()

The Variable.expand() method in ltl2ba.py performs contradiction
detection by checking if a negated variable already exists in the
graph node's old set. However, the isinstance check was incorrectly
testing the ASTNode wrapper instead of the wrapped operator, causing
the check to always return False.

The old set contains ASTNode instances which wrap LTL operators via
their .op attribute. The fix changes isinstance(f, NotOp) to
isinstance(f.op, NotOp) to correctly examine the wrapped operator
type. This follows the established pattern used elsewhere in the
file, such as the iteration at lines 572-574 which accesses
o.op.is_temporal() on items from node.old.

Signed-off-by: Wander Lairson Costa <wander@...hat.com>
Reviewed-by: Nam Cao <namcao@...utronix.de>
---
 tools/verification/rvgen/rvgen/ltl2ba.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index f14e6760ac3db..28f9a5682c830 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -394,7 +394,7 @@ class Variable:
     @staticmethod
     def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
         for f in node.old:
-            if isinstance(f, NotOp) and f.op.child is n:
+            if isinstance(f.op, NotOp) and f.op.child is n:
                 return node_set
         node.old |= {n}
         return node.expand(node_set)
-- 
2.52.0