From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-wm1-f54.google.com (mail-wm1-f54.google.com [209.85.128.54]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 4C5014399F7 for ; Wed, 22 Jul 2026 21:14:24 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.128.54 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1784754865; cv=none; b=SQrtbYIs6S6TtQsjG/tcWgwJGaT687WFQLNjDvmND5bNc2RgJul4y9hQKr7WgN7hm48pN9923i5be6nV8/whHeSf9MF6l2Q+mFx81qTjmv82NgtjOITyIaZ4Y+ZUz9lEp/lGmBuelMGKIgM+3tVzQsZzCi8yZtVSHc3aB5vbHM0= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1784754865; c=relaxed/simple; bh=sGs0rfz9r6IQCOxNIuyFl8cjjmJTI88JpUD6LUtWFpQ=; h=Message-ID:Date:MIME-Version:Subject:To:Cc:References:From: In-Reply-To:Content-Type; b=GGuBhyfuPA2W/X9tz3zTBt4QRHxWG48rEANSH3Q7VR5ih9bu0jJ/HU0FKkba3NQPTEF96T7QbnmQd/5GApxzEGtMmXOW3gzn5/KYyhQgpU2lwMFfRWUAJYN8VFwIPXXKB0FN+7y/JzH7WfaCwTmyYkXFcyCUd6yGXFnfOOLpLbw= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=fYd1wBrq; arc=none smtp.client-ip=209.85.128.54 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="fYd1wBrq" Received: by mail-wm1-f54.google.com with SMTP id 5b1f17b1804b1-4955aa106b1so35835565e9.0 for ; Wed, 22 Jul 2026 14:14:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20251104; t=1784754862; x=1785359662; darn=vger.kernel.org; h=content-transfer-encoding:content-type:in-reply-to:from :content-language:references:cc:to:subject:user-agent:mime-version :date:message-id:sender:from:to:cc:subject:date:message-id:reply-to :content-type; bh=sGs0rfz9r6IQCOxNIuyFl8cjjmJTI88JpUD6LUtWFpQ=; b=fYd1wBrqsC4GM8p5o94n4HNLJzHHbLKhAQ35YG0kdbX3g4YIWKfJz2jcSo96XFgqlD FjfqYNwntsiIavPhgLbC/bJwdJqMBqqBsWuEdNwvOo+/T0PiLdoGlrHvizNzXe5GCf7Y dqbdY4gSUiw1efeyhVpc8oHVaYjgBwb5b4kf6NQZguS7M7vE5tBD2kZfgBFjvWQwBZmD 7WytHo2UTGNAJyM/Ct6wEWOSEpeGU9TEDL+g0hQrU0EoDxx2VDPVv8P9wIN11tN+gFss ysP2MuVq3jVmNU/Olngn5DeslFZp710cbJOuUy1TLZ7bQEw/i/b3HObRxcay3e55k5Zx Vtvw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1784754862; x=1785359662; h=content-transfer-encoding:content-type:in-reply-to:from :content-language:references:cc:to:subject:user-agent:mime-version :date:message-id:sender:x-gm-gg:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to:content-type; bh=sGs0rfz9r6IQCOxNIuyFl8cjjmJTI88JpUD6LUtWFpQ=; b=oeofQy1dA6je75SRtvq4zDqbE15ZkrjkPvNslYQ3Jl4AZaKbwFjj1MC1l8Y0b40f3v PgK1vpAIGCSApaQzPITI/ajdskLOLFl6qh0M+BZaoe3VH1MXLEOQQuve9Z35OkWk+nZF gwRz/7pFKm9Q4U9yz6kKgIedF6Bagz1SaFjBzYHDlZux77g1ngke2FgdeaFuS48NXYkd 1810BQ1pQg28BBCxAkOVzBan5Vhu+mMEh5jtSZCWJN1xUxQV/wJc6XpFbGqiaB5emBfR dPSZnNmdo6meUW5vVThvhT40WDY/wnOWYrG2zGEt3OEcSqbsZVNEBHekbShZqNzfXP0b Rx9w== X-Forwarded-Encrypted: i=1; AHgh+Rp0+bW503mPAlb7lEXtPW7Z+it8gaHfeT+CcqKlhoaMO64xRKQmnZyyW+kESvN/Y2OUrwIeTTH2YrtCDoY=@vger.kernel.org X-Gm-Message-State: AOJu0YyqJA4cL//vpcsYpMlFgTkoaXUd/Wj81JHwh2hal8KJ1jEGo75O eMzVQIOTsuQ2a+/oQIg087v3gyQOQ6pjXfXe7TmCKQikh34cpB86UdhN X-Gm-Gg: AR+sD10daaK16MaKxkNlKa6uOQYj77Y9gVssvYdup6CZlpnow5bCMg20GGPXIQL5WF+ NBW4QTliUYf1y2sp2sNMjZRWqleFpMhM45ZwK15bpnSYLwOBrXmNag0uhQgXm+9xSwfyteoo0DX gh7V3t+YTB90ph+MwmGGb2omoDhZyFmRDyYFsYm0q+Pb+2F0/kCnDJalH0c/UXJVYwBb6LxRkIr geEZpWxzT59LTych9T7H1QopcNKjqY4WsIkd9AoMGA7ERvDLo//J8RiTgawGdoUVyfsbzfsaGKD aru6PvV3tWs2t8LKx2saYn262Duum+6qedcyCJcyc8u/wZx1+5IRNnXmdW8ZaFGPRkbAS7XdEow E/wcell+DHMFGPRiA90hDnrm6++OaZ/NaK9M2c2vpNqdPSK32E0Ld+OPBNgvU4Fz38YHpT61AOU RXGCGKbEstVi6wZWBF6/Pt6GJeW4AhAGyBNz4knxldrdJemyCb+r2XZWx0V10QkXhIv8fp3A== X-Received: by 2002:a05:600c:46c7:b0:493:c47f:3c55 with SMTP id 5b1f17b1804b1-49573cb966cmr3744405e9.5.1784754862459; Wed, 22 Jul 2026 14:14:22 -0700 (PDT) Received: from [10.128.10.232] (195-23-151-163.net.novis.pt. [195.23.151.163]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-4956b021fa6sm66296175e9.2.2026.07.22.14.14.20 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 22 Jul 2026 14:14:21 -0700 (PDT) Sender: Julian Braha Message-ID: <9b2d40b1-a21e-4ccb-a80b-27f1a24afc82@gmail.com> Date: Wed, 22 Jul 2026 22:14:20 +0100 Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 User-Agent: Mozilla Thunderbird Subject: Re: [PATCH] pinctrl: s32cc: fix unmet dependency for PINCTRL_S32CC To: Arnd Bergmann , Aisheng Dong , Fabio Estevam , Frank Li , Jacky Bai , Linus Walleij Cc: Chester Lin , Matthias Brugger , Ghennadi Procopciuc , NXP S32 Linux Team , Pengutronix Kernel Team , Bartosz Golaszewski , Andrei Stefanescu , Khristine Andreea Barbulescu , linux-kernel@vger.kernel.org, "open list:GPIO SUBSYSTEM" , linux-arm-kernel@lists.infradead.org References: <20260722202638.135277-1-julianbraha@gmail.com> <0a99e10e-b4c4-4a64-bcb4-fee8d777d0b7@app.fastmail.com> Content-Language: en-US From: Julian Braha In-Reply-To: <0a99e10e-b4c4-4a64-bcb4-fee8d777d0b7@app.fastmail.com> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On 7/22/26 21:39, Arnd Bergmann wrote: > The patch looks fine, but I'm curious about what type of rule found > the mistake. Is this a heuristic that found that drivers/pinctrl/* > overwhelmingly uses select instead of depends, or did kconfirm > find a circular dependency that was caused by inconsistent > rules? Not a heuristic, kconfirm-smt is the first complete SMT solver for Kconfig (as in, all semantics of the Kconfig language are used to automatically encode all Kconfig files as SMT constraints). There have been many previous SAT solvers for Kconfig, and there was one that attempted to detect unmet dependencies (Kismet) but that one has both false positives and false negatives because it approximates everything as boolean logic. In contrast, kconfirm-smt uses SMT integers and strings to model Kconfig int/hex and strings (unsurprisingly). I believe I am the first to do this. So, to detect unmet dependencies, kconfirm-smt runs a check on every single selector-selectee pair using this routine: 1. Add the constraints to the model that the option is enabled, and its selector is enabled, and its dependencies aren't met. 2. If Z3 finds a solution (as in, the constraints are still satisfiable) then we know that there is an unmet dependency. 3. Reset the constraints back to the original model, and loop ^^^ You can also use kconfirm-smt to do better random config generation than randconfig ;) Also, you can give it a partial .config file, and it will randomize the rest of the options that are not in it. Give it a try, I would love some feedback: https://github.com/julianbraha/kconfirm/tree/smt#usage-examples - Julian Braha