From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.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 807C942846E for ; Thu, 14 May 2026 15:21:47 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1778772110; cv=none; b=GbPcRMb6ZiuuNK/hDs06KfeqsIZdoWhLzo2+ray4RrDkF4rVaELuYtXY7cpTQS0No+WUiGkfQvz3AQR9z53zWyuI8DtEi6CoGjOtqsP1ZFC+l5t/mjo4xaFaayhnQmOal+958hwrxv/GgmuxCLLp9W7617pfkcDwhdz+SS8ylmo= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1778772110; c=relaxed/simple; bh=0C6RfvaonJpqY5+r3oZmoyYaaprqQ+dSZ/HR09CNLNc=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=rwdVqxJJz8hNuwKew14TARHcn4b+zBxFYeo5giV6tpmMjfYcMEabWH+5qBZdE7EJvoMpLOLf0dv0Pr9xQe01g5cbuSq3wn/ZP3KFKFQnnAQajy4ewWDS3O2jC4ZolENK/nyZvE71NTLKrf4X64nAkeJNYRvYYkTYmLqEK9BD33k= 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=HyqNOGub; arc=none smtp.client-ip=170.10.129.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="HyqNOGub" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1778772106; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=Yr0V9/34qco1aQYqxDHUIvyNht8oHMlUR7CJ+DlzE58=; b=HyqNOGubndsAnI1LGasmbJT8ZNdsjssWRptfXVoKO4wu5N31JoOnO0RMALP3gt4xg27TEW p20hw7z0ujHhAgHVwenJpjJtT/jIP91oPukGljUJK7hfgTr2cVSiEnQjynKOisCS26Lyqd MrzQ1Auz3QuH4WpHZwdQyql8cuGJUiM= Received: from mx-prod-mc-06.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-43-Y5-WadFFM_6U8Dhj7q9lNA-1; Thu, 14 May 2026 11:21:43 -0400 X-MC-Unique: Y5-WadFFM_6U8Dhj7q9lNA-1 X-Mimecast-MFC-AGG-ID: Y5-WadFFM_6U8Dhj7q9lNA_1778772102 Received: from mx-prod-int-01.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-01.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.4]) (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-06.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 2FC40180061D; Thu, 14 May 2026 15:21:42 +0000 (UTC) Received: from gmonaco-thinkpadt14gen3.rmtit.csb (unknown [10.44.48.32]) by mx-prod-int-01.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 20F6430001A2; Thu, 14 May 2026 15:21:38 +0000 (UTC) From: Gabriele Monaco To: linux-kernel@vger.kernel.org, linux-trace-kernel@vger.kernel.org, Steven Rostedt , Gabriele Monaco , Nam Cao Cc: Thomas Weissschuh , Tomas Glozar , John Kacur , Wen Yang Subject: [PATCH v2 07/14] verification/rvgen: Fix ltl2k writing True as a literal Date: Thu, 14 May 2026 17:20:48 +0200 Message-ID: <20260514152055.229162-8-gmonaco@redhat.com> In-Reply-To: <20260514152055.229162-1-gmonaco@redhat.com> References: <20260514152055.229162-1-gmonaco@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: 8bit X-Scanned-By: MIMEDefang 3.4.1 on 10.30.177.4 The rvgen parser for LTL stores literal true values in the python representation (capitalised True), this doesn't build in C. The Literal class should already handle this case but ASTNode skips its strigification method and converts the value (true/false) directly. Fix by delegating ASTNode stringification to the Literal and Variable classes instead of bypassing them. Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic") Signed-off-by: Gabriele Monaco --- tools/verification/rvgen/rvgen/ltl2ba.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index 7f538598a868..016e7cf93bbb 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -122,10 +122,8 @@ class ASTNode: return self.op.expand(self, node, node_set) def __str__(self): - if isinstance(self.op, Literal): - return str(self.op.value) - if isinstance(self.op, Variable): - return self.op.name.lower() + if isinstance(self.op, (Literal, Variable)): + return str(self.op) return "val" + str(self.id) def normalize(self): @@ -382,6 +380,9 @@ class Variable: def __iter__(self): yield from () + def __str__(self): + return self.name.lower() + def negate(self): new = ASTNode(self) return NotOp(new) -- 2.54.0