Hi, (resending everything with smaller patches) Configuring a kernel requires a forward enabling approach where one enables each option one needs at a time. If one enables an option that selects other options, these options are no longer de-selectable by design. Likewise, if one has enabled an option which creates a conflict with a secondary option one wishes to enable, one cannot easily enable that secondary option, unless one is willing to spend time analyzing the dependencies that led to this conflict. Sometimes, these conflicts are not easy to understand [0,1]. This patch series (for linux-next) provides support to enable users to express their desired target configuration and display possible resolutions to their conflicts. This support is provided within xconfig. Conflict resolution is provided by translating kconfig's configuration option tree to a propositional formula, and then allowing our resolution algorithm, which uses a SAT solver (picosat, implemented in C) calculate the possible fixes for an expressed target kernel configuration. New UI extensions are made to xconfig with panes and buttons to allow users to express new desired target options, calculate fixes, and apply any of found solutions. We created a separate test infrastructure that we used to validate the correctness of the suggestions made. It shows that our resolution algorithm resolves around 95% of the conflicts. We plan to incorporate this with a later patch series. We envision that our translation of the kconfig option tree into into a propositional formula could potentially also later be repurposed to address other problems. An example is checking the consistency between the use of ifdefs and logic expressed in kconfig files. We suspect that this could, for example, help avoid invalid kconfig configurations and help with ifdef maintenance. You can see a YouTube video demonstrating this work [2]. This effort is part of the kernelnewbies Kconfig-SAT project [3], the approach and effort is also explained in detail in our paper [4]. It is also our attempt at contributing back to the kernel community, whose configurator researchers studied a lot. Patches applicable to linux-next. [0] https://gsd.uwaterloo.ca/sites/default/files/vamos12-survey.pdf [1] https://www.linux-magazine.com/Issues/2021/244/Kconfig-Deep-Dive [2] https://youtu.be/vyX7zCRiLKU [3] https://kernelnewbies.org/KernelProjects/kconfig-sat [4] http://www.cse.chalmers.se/~bergert/paper/2021-icseseip-configfix.pdf Thanks from the team! (and thanks to Luis Chamberlain for guiding us here) Co-developed-by: Patrick Franz <deltaone@xxxxxxxxxx> Signed-off-by: Patrick Franz <deltaone@xxxxxxxxxx> Co-developed-by: Ibrahim Fayaz <phayax@xxxxxxxxx> Signed-off-by: Ibrahim Fayaz <phayax@xxxxxxxxx> Reviewed-by: Luis Chamberlain <mcgrof@xxxxxxxx> Tested-by: Evgeny Groshev <eugene.groshev@xxxxxxxxx> Suggested-by: Sarah Nadi <nadi@xxxxxxxxxxx> Suggested-by: Thorsten Berger <thorsten.berger@xxxxxx> Signed-off-by: Thorsten Berger <thorsten.berger@xxxxxx> Patrick Franz (12): Add picosat.h Add picosat.c (1/3) Add picosat.c (2/3) Add picosat.c (3/3) Add definitions Add files for building constraints Add files for handling expressions Add files for RangeFix Add files with utility functions Add tools Add xconfig-modifications Simplify dependencies for MODULE_SIG_KEY_TYPE_RSA & MODULE_SIG_KEY_TYPE_ECDSA certs/Kconfig | 3 +- scripts/kconfig/Makefile | 19 +- scripts/kconfig/cf_constraints.c | 1219 +++++ scripts/kconfig/cf_constraints.h | 23 + scripts/kconfig/cf_defs.h | 233 + scripts/kconfig/cf_expr.c | 2146 ++++++++ scripts/kconfig/cf_expr.h | 237 + scripts/kconfig/cf_rangefix.c | 1017 ++++ scripts/kconfig/cf_rangefix.h | 18 + scripts/kconfig/cf_satutils.c | 536 ++ scripts/kconfig/cf_satutils.h | 30 + scripts/kconfig/cf_utils.c | 510 ++ scripts/kconfig/cf_utils.h | 90 + scripts/kconfig/cfconfig.c | 176 + scripts/kconfig/cfoutconfig.c | 128 + scripts/kconfig/configfix.c | 420 ++ scripts/kconfig/configfix.h | 41 + scripts/kconfig/expr.h | 13 + scripts/kconfig/picosat.c | 8502 ++++++++++++++++++++++++++++++ scripts/kconfig/picosat.h | 658 +++ scripts/kconfig/qconf.cc | 1003 +++- scripts/kconfig/qconf.h | 179 +- 22 files changed, 16943 insertions(+), 258 deletions(-) create mode 100644 scripts/kconfig/cf_constraints.c create mode 100644 scripts/kconfig/cf_constraints.h create mode 100644 scripts/kconfig/cf_defs.h create mode 100644 scripts/kconfig/cf_expr.c create mode 100644 scripts/kconfig/cf_expr.h create mode 100644 scripts/kconfig/cf_rangefix.c create mode 100644 scripts/kconfig/cf_rangefix.h create mode 100644 scripts/kconfig/cf_satutils.c create mode 100644 scripts/kconfig/cf_satutils.h create mode 100644 scripts/kconfig/cf_utils.c create mode 100644 scripts/kconfig/cf_utils.h create mode 100644 scripts/kconfig/cfconfig.c create mode 100644 scripts/kconfig/cfoutconfig.c create mode 100644 scripts/kconfig/configfix.c create mode 100644 scripts/kconfig/configfix.h create mode 100644 scripts/kconfig/picosat.c create mode 100644 scripts/kconfig/picosat.h -- 2.33.0 -- Prof. Dr. Thorsten Berger Chair of Software Engineering Faculty of Computer Science Ruhr University Bochum, Germany http://www.thorsten-berger.net Tel.: +49 (0) 234 32 25975 Mob.: +49 (0) 160 926 878 10 Skype: tberger.work
