Re: [PATCH] pinctrl: s32cc: fix unmet dependency for PINCTRL_S32CC

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