From nobody Thu Apr 2 01:54:03 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 81EEA30BB83 for ; Mon, 23 Feb 2026 16:30:17 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864218; cv=none; b=qxodz6iNu+zpqV9VbrGnz8br6kJjtoShxuFdRVUpUa0OdbyIWE4O5YOWeJCy0QT7RALPpVSVgzJazVKkFhsiEQ0hJI466uh+Y0J+QibYWHyvwRHMZDbGi74pSJP8LijzaNMwk1H0dOXfuGqmBhO/Qh2XGMzCwwKocqJA4uBkgI0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1771864218; c=relaxed/simple; bh=3+1mH0oEHDjZM17U3urFB35D5e/V331jenjy+2qK/Cc=; h=From:To:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=ONnf5sjR0j1ZOkBLLvBsaLXGA3i4vicAUa8Yk/dAwGb63yt5wV1uxpHT4ThSRzeSbyqc1+WAJWf6RtMbZvTU2Lq7UvuD0JoNEFbraS02Bjay5gS+pvw3EiA9qyhiQwWIpCqTqMlfQgPTbEZu4IVi0JZRMIoYKcIZwBq09LnoNt0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=ABmulni9; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="ABmulni9" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1771864216; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=PUGGPkspJ3zMYbMOZig+zlLmAaK6PE0VrPjeBJRZrt8=; b=ABmulni96Q9Ac0lqs+0kgbPYg/J7Y9vsGkd37MARuPo5Zd8uV5MjraFpsoDhbOFuj0SLqL 4HIlgwKQVey2uOVveelzAPN6zcfgKlV2g0f7i0I2dHlXlhMNWXo/a3Ib+PzlzS0X41QSGP 79fb89fajNTW5Yk3aByutbkfyTwK0hM= Received: from mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (ec2-54-186-198-63.us-west-2.compute.amazonaws.com [54.186.198.63]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-256-AfcpOgBhMtaRRtK-iLCWvA-1; Mon, 23 Feb 2026 11:30:11 -0500 X-MC-Unique: AfcpOgBhMtaRRtK-iLCWvA-1 X-Mimecast-MFC-AGG-ID: AfcpOgBhMtaRRtK-iLCWvA_1771864210 Received: from mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.93]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-03.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id EE5F01955F2D; Mon, 23 Feb 2026 16:30:09 +0000 (UTC) Received: from fedora.redhat.com (unknown [10.22.88.94]) by mx-prod-int-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id D606C1800669; Mon, 23 Feb 2026 16:30:07 +0000 (UTC) From: Wander Lairson Costa To: Steven Rostedt , Gabriele Monaco , Nam Cao , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org (open list:RUNTIME VERIFICATION (RV)), linux-kernel@vger.kernel.org (open list) Subject: [PATCH v3 15/19] rv/rvgen: fix isinstance check in Variable.expand() Date: Mon, 23 Feb 2026 13:17:58 -0300 Message-ID: <20260223162407.147003-16-wander@redhat.com> In-Reply-To: <20260223162407.147003-1-wander@redhat.com> References: <20260223162407.147003-1-wander@redhat.com> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.93 Content-Type: text/plain; charset="utf-8" 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 Reviewed-by: Nam Cao --- 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 f9855dfa3bc1c..7f538598a8681 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -395,7 +395,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 |=3D {n} return node.expand(node_set) --=20 2.53.0