xref: /linux/Documentation/kbuild/kconfig-language.rst (revision 03f76ddff5b04a808ae16c06418460151e2fdd4b)
1================
2Kconfig Language
3================
4
5Introduction
6------------
7
8The configuration database is a collection of configuration options
9organized in a tree structure::
10
11	+- Code maturity level options
12	|  +- Prompt for development and/or incomplete code/drivers
13	+- General setup
14	|  +- Networking support
15	|  +- System V IPC
16	|  +- BSD Process Accounting
17	|  +- Sysctl support
18	+- Loadable module support
19	|  +- Enable loadable module support
20	|     +- Set version information on all module symbols
21	|     +- Kernel module loader
22	+- ...
23
24Every entry has its own dependencies. These dependencies are used
25to determine the visibility of an entry. Any child entry is only
26visible if its parent entry is also visible.
27
28Menu entries
29------------
30
31Most entries define a config option; all other entries help to organize
32them. A single configuration option is defined like this::
33
34  config MODVERSIONS
35	bool "Set version information on all module symbols"
36	depends on MODULES
37	help
38	  Usually, modules have to be recompiled whenever you switch to a new
39	  kernel.  ...
40
41Every line starts with a key word and can be followed by multiple
42arguments.  "config" starts a new config entry. The following lines
43define attributes for this config option. Attributes can be the type of
44the config option, input prompt, dependencies, help text and default
45values. A config option can be defined multiple times with the same
46name, but every definition can have only a single input prompt and the
47type must not conflict.
48
49Menu attributes
50---------------
51
52A menu entry can have a number of attributes. Not all of them are
53applicable everywhere (see syntax).
54
55- type definition: "bool"/"tristate"/"string"/"hex"/"int"
56
57  Every config option must have a type. There are only two basic types:
58  tristate and string; the other types are based on these two. The type
59  definition optionally accepts an input prompt, so these two examples
60  are equivalent::
61
62	bool "Networking support"
63
64  and::
65
66	bool
67	prompt "Networking support"
68
69- input prompt: "prompt" <prompt> ["if" <expr>]
70
71  Every menu entry can have at most one prompt, which is used to display
72  to the user. Optionally dependencies only for this prompt can be added
73  with "if". If a prompt is not present, the config option is a non-visible
74  symbol, meaning its value cannot be directly changed by the user (such as
75  altering the value in ``.config``) and the option will not appear in any
76  config menus. Its value can only be set via "default" and "select" (see
77  below).
78
79- default value: "default" <expr> ["if" <expr>]
80
81  A config option can have any number of default values. If multiple
82  default values are visible, only the first defined one is active.
83  Default values are not limited to the menu entry where they are
84  defined. This means the default can be defined somewhere else or be
85  overridden by an earlier definition.
86  The default value is only assigned to the config symbol if no other
87  value was set by the user (via the input prompt above). If an input
88  prompt is visible the default value is presented to the user and can
89  be overridden by him.
90  Optionally, dependencies only for this default value can be added with
91  "if".
92
93 The default value deliberately defaults to 'n' in order to avoid bloating the
94 build. With few exceptions, new config options should not change this. The
95 intent is for "make oldconfig" to add as little as possible to the config from
96 release to release.
97
98 Note:
99	Things that merit "default y/m" include:
100
101	a) A new Kconfig option for something that used to always be built
102	   should be "default y".
103
104	b) A new gatekeeping Kconfig option that hides/shows other Kconfig
105	   options (but does not generate any code of its own), should be
106	   "default y" so people will see those other options.
107
108	c) Sub-driver behavior or similar options for a driver that is
109	   "default n". This allows you to provide sane defaults.
110
111	d) Hardware or infrastructure that everybody expects, such as CONFIG_NET
112	   or CONFIG_BLOCK. These are rare exceptions.
113
114- type definition + default value::
115
116	"def_bool"/"def_tristate" <expr> ["if" <expr>]
117
118  This is a shorthand notation for a type definition plus a value.
119  Optionally dependencies for this default value can be added with "if".
120
121- dependencies: "depends on" <expr>
122
123  This defines a dependency for this menu entry. If multiple
124  dependencies are defined, they are connected with '&&'. Dependencies
125  are applied to all other options within this menu entry (which also
126  accept an "if" expression), so these two examples are equivalent::
127
128	bool "foo" if BAR
129	default y if BAR
130
131  and::
132
133	depends on BAR
134	bool "foo"
135	default y
136
137- reverse dependencies: "select" <symbol> ["if" <expr>]
138
139  While normal dependencies reduce the upper limit of a symbol (see
140  below), reverse dependencies can be used to force a lower limit of
141  another symbol. The value of the current menu symbol is used as the
142  minimal value <symbol> can be set to. If <symbol> is selected multiple
143  times, the limit is set to the largest selection.
144  Reverse dependencies can only be used with boolean or tristate
145  symbols.
146
147  Note:
148	select should be used with care. select will force
149	a symbol to a value without visiting the dependencies.
150	By abusing select you are able to select a symbol FOO even
151	if FOO depends on BAR that is not set.
152	In general use select only for non-visible symbols
153	(no prompts anywhere) and for symbols with no dependencies.
154	That will limit the usefulness but on the other hand avoid
155	the illegal configurations all over.
156
157	If "select" <symbol> is followed by "if" <expr>, <symbol> will be
158	selected by the logical AND of the value of the current menu symbol
159	and <expr>. This means, the lower limit can be downgraded due to the
160	presence of "if" <expr>. This behavior may seem weird, but we rely on
161	it. (The future of this behavior is undecided.)
162
163- weak reverse dependencies: "imply" <symbol> ["if" <expr>]
164
165  This is similar to "select" as it enforces a lower limit on another
166  symbol except that the "implied" symbol's value may still be set to n
167  from a direct dependency or with a visible prompt.
168
169  Given the following example::
170
171    config FOO
172	tristate "foo"
173	imply BAZ
174
175    config BAZ
176	tristate "baz"
177	depends on BAR
178
179  The following values are possible:
180
181	===		===		=============	==============
182	FOO		BAR		BAZ's default	choice for BAZ
183	===		===		=============	==============
184	n		y		n		N/m/y
185	m		y		m		M/y/n
186	y		y		y		Y/m/n
187	n		m		n		N/m
188	m		m		m		M/n
189	y		m		m		M/n
190	y		n		*		N
191	===		===		=============	==============
192
193  This is useful e.g. with multiple drivers that want to indicate their
194  ability to hook into a secondary subsystem while allowing the user to
195  configure that subsystem out without also having to unset these drivers.
196
197  Note: If the feature provided by BAZ is highly desirable for FOO,
198  FOO should imply not only BAZ, but also its dependency BAR::
199
200    config FOO
201	tristate "foo"
202	imply BAR
203	imply BAZ
204
205  Note: If "imply" <symbol> is followed by "if" <expr>, the default of <symbol>
206  will be the logical AND of the value of the current menu symbol and <expr>.
207  (The future of this behavior is undecided.)
208
209- limiting menu display: "visible if" <expr>
210
211  This attribute is only applicable to menu blocks, if the condition is
212  false, the menu block is not displayed to the user (the symbols
213  contained there can still be selected by other symbols, though). It is
214  similar to a conditional "prompt" attribute for individual menu
215  entries. Default value of "visible" is true.
216
217- numerical ranges: "range" <symbol> <symbol> ["if" <expr>]
218
219  This allows to limit the range of possible input values for int
220  and hex symbols. The user can only input a value which is larger than
221  or equal to the first symbol and smaller than or equal to the second
222  symbol.
223
224- help text: "help"
225
226  This defines a help text. The end of the help text is determined by
227  the indentation level, this means it ends at the first line which has
228  a smaller indentation than the first line of the help text.
229
230- module attribute: "modules"
231  This declares the symbol to be used as the MODULES symbol, which
232  enables the third modular state for all config symbols.
233  At most one symbol may have the "modules" option set.
234
235- transitional attribute: "transitional"
236  This declares the symbol as transitional, meaning it should be processed
237  during configuration but omitted from newly written .config files.
238  Transitional symbols are useful for backward compatibility during config
239  option migrations - they allow olddefconfig to process existing .config
240  files while ensuring the old option doesn't appear in new configurations.
241
242  A transitional symbol:
243  - Has no prompt (is not visible to users in menus)
244  - Is processed normally during configuration (values are read and used)
245  - Can be referenced in default expressions of other symbols
246  - Is not written to new .config files
247  - Cannot have any other properties (it is a pass-through option)
248
249  Example migration from OLD_NAME to NEW_NAME::
250
251    config NEW_NAME
252	bool "New option name"
253	default OLD_NAME
254	help
255	  This replaces the old CONFIG_OLD_NAME option.
256
257    config OLD_NAME
258	bool
259	transitional
260	help
261	  Transitional config for OLD_NAME to NEW_NAME migration.
262
263  With this setup, existing .config files with "CONFIG_OLD_NAME=y" will
264  result in "CONFIG_NEW_NAME=y" being set, while CONFIG_OLD_NAME will be
265  omitted from newly written .config files.
266
267Menu dependencies
268-----------------
269
270Dependencies define the visibility of a menu entry and can also reduce
271the input range of tristate symbols. The tristate logic used in the
272expressions uses one more state than normal boolean logic to express the
273module state. Dependency expressions have the following syntax::
274
275  <expr> ::= <symbol>                           (1)
276           <symbol> '=' <symbol>                (2)
277           <symbol> '!=' <symbol>               (3)
278           <symbol1> '<' <symbol2>              (4)
279           <symbol1> '>' <symbol2>              (4)
280           <symbol1> '<=' <symbol2>             (4)
281           <symbol1> '>=' <symbol2>             (4)
282           '(' <expr> ')'                       (5)
283           '!' <expr>                           (6)
284           <expr> '&&' <expr>                   (7)
285           <expr> '||' <expr>                   (8)
286
287Expressions are listed in decreasing order of precedence.
288
289(1) Convert the symbol into an expression. Boolean and tristate symbols
290    are simply converted into the respective expression values. All
291    other symbol types result in 'n'.
292(2) If the values of both symbols are equal, it returns 'y',
293    otherwise 'n'.
294(3) If the values of both symbols are equal, it returns 'n',
295    otherwise 'y'.
296(4) If value of <symbol1> is respectively lower, greater, lower-or-equal,
297    or greater-or-equal than value of <symbol2>, it returns 'y',
298    otherwise 'n'.
299(5) Returns the value of the expression. Used to override precedence.
300(6) Returns the result of (2-/expr/).
301(7) Returns the result of min(/expr/, /expr/).
302(8) Returns the result of max(/expr/, /expr/).
303
304An expression can have a value of 'n', 'm' or 'y' (or 0, 1, 2
305respectively for calculations). A menu entry becomes visible when its
306expression evaluates to 'm' or 'y'.
307
308There are two types of symbols: constant and non-constant symbols.
309Non-constant symbols are the most common ones and are defined with the
310'config' statement. Non-constant symbols consist entirely of alphanumeric
311characters or underscores.
312Constant symbols are only part of expressions. Constant symbols are
313always surrounded by single or double quotes. Within the quote, any
314other character is allowed and the quotes can be escaped using '\'.
315
316Menu structure
317--------------
318
319The position of a menu entry in the tree is determined in two ways. First
320it can be specified explicitly::
321
322  menu "Network device support"
323	depends on NET
324
325  config NETDEVICES
326	...
327
328  endmenu
329
330All entries within the "menu" ... "endmenu" block become a submenu of
331"Network device support". All subentries inherit the dependencies from
332the menu entry, e.g. this means the dependency "NET" is added to the
333dependency list of the config option NETDEVICES.
334
335The other way to generate the menu structure is done by analyzing the
336dependencies. If a menu entry somehow depends on the previous entry, it
337can be made a submenu of it. First, the previous (parent) symbol must
338be part of the dependency list and then one of these two conditions
339must be true:
340
341- the child entry must become invisible, if the parent is set to 'n'
342- the child entry must only be visible, if the parent is visible::
343
344    config MODULES
345	bool "Enable loadable module support"
346
347    config MODVERSIONS
348	bool "Set version information on all module symbols"
349	depends on MODULES
350
351    comment "module support disabled"
352	depends on !MODULES
353
354MODVERSIONS directly depends on MODULES, this means it's only visible if
355MODULES is different from 'n'. The comment on the other hand is only
356visible when MODULES is set to 'n'.
357
358
359Kconfig syntax
360--------------
361
362The configuration file describes a series of menu entries, where every
363line starts with a keyword (except help texts). The following keywords
364end a menu entry:
365
366- config
367- menuconfig
368- choice/endchoice
369- comment
370- menu/endmenu
371- if/endif
372- source
373
374The first five also start the definition of a menu entry.
375
376config::
377
378	"config" <symbol>
379	<config options>
380
381This defines a config symbol <symbol> and accepts any of above
382attributes as options.
383
384menuconfig::
385
386	"menuconfig" <symbol>
387	<config options>
388
389This is similar to the simple config entry above, but it also gives a
390hint to front ends, that all suboptions should be displayed as a
391separate list of options. To make sure all the suboptions will really
392show up under the menuconfig entry and not outside of it, every item
393from the <config options> list must depend on the menuconfig symbol.
394In practice, this is achieved by using one of the next two constructs::
395
396  (1):
397  menuconfig M
398  if M
399      config C1
400      config C2
401  endif
402
403  (2):
404  menuconfig M
405  config C1
406      depends on M
407  config C2
408      depends on M
409
410In the following examples (3) and (4), C1 and C2 still have the M
411dependency, but will not appear under menuconfig M anymore, because
412of C0, which doesn't depend on M::
413
414  (3):
415  menuconfig M
416      config C0
417  if M
418      config C1
419      config C2
420  endif
421
422  (4):
423  menuconfig M
424  config C0
425  config C1
426      depends on M
427  config C2
428      depends on M
429
430choices::
431
432	"choice"
433	<choice options>
434	<choice block>
435	"endchoice"
436
437This defines a choice group and accepts "prompt", "default", "depends on", and
438"help" attributes as options.
439
440A choice only allows a single config entry to be selected.
441
442comment::
443
444	"comment" <prompt>
445	<comment options>
446
447This defines a comment which is displayed to the user during the
448configuration process and is also echoed to the output files. The only
449possible options are dependencies.
450
451menu::
452
453	"menu" <prompt>
454	<menu options>
455	<menu block>
456	"endmenu"
457
458This defines a menu block, see "Menu structure" above for more
459information. The only possible options are dependencies and "visible"
460attributes.
461
462if::
463
464	"if" <expr>
465	<if block>
466	"endif"
467
468This defines an if block. The dependency expression <expr> is appended
469to all enclosed menu entries.
470
471source::
472
473	"source" <prompt>
474
475This reads the specified configuration file. This file is always parsed.
476
477mainmenu::
478
479	"mainmenu" <prompt>
480
481This sets the config program's title bar if the config program chooses
482to use it. It should be placed at the top of the configuration, before any
483other statement.
484
485'#' Kconfig source file comment:
486
487An unquoted '#' character anywhere in a source file line indicates
488the beginning of a source file comment.  The remainder of that line
489is a comment.
490
491
492Kconfig hints
493-------------
494This is a collection of Kconfig tips, most of which aren't obvious at
495first glance and most of which have become idioms in several Kconfig
496files.
497
498Adding common features and make the usage configurable
499~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
500It is a common idiom to implement a feature/functionality that are
501relevant for some architectures but not all.
502The recommended way to do so is to use a config variable named HAVE_*
503that is defined in a common Kconfig file and selected by the relevant
504architectures.
505An example is the generic IOMAP functionality.
506
507We would in lib/Kconfig see::
508
509  # Generic IOMAP is used to ...
510  config HAVE_GENERIC_IOMAP
511
512  config GENERIC_IOMAP
513	depends on HAVE_GENERIC_IOMAP && FOO
514
515And in lib/Makefile we would see::
516
517	obj-$(CONFIG_GENERIC_IOMAP) += iomap.o
518
519For each architecture using the generic IOMAP functionality we would see::
520
521  config X86
522	select ...
523	select HAVE_GENERIC_IOMAP
524	select ...
525
526Note: we use the existing config option and avoid creating a new
527config variable to select HAVE_GENERIC_IOMAP.
528
529Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is
530introduced to overcome the limitation of select which will force a
531config option to 'y' no matter the dependencies.
532The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the
533situation where select forces a symbol equals to 'y'.
534
535Adding features that need compiler support
536~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
537
538There are several features that need compiler support. The recommended way
539to describe the dependency on the compiler feature is to use "depends on"
540followed by a test macro::
541
542  config STACKPROTECTOR
543	bool "Stack Protector buffer overflow detection"
544	depends on $(cc-option,-fstack-protector)
545	...
546
547If you need to expose a compiler capability to makefiles and/or C source files,
548`CC_HAS_` is the recommended prefix for the config option::
549
550  config CC_HAS_FOO
551	def_bool $(success,$(srctree)/scripts/cc-check-foo.sh $(CC))
552
553Build as module only
554~~~~~~~~~~~~~~~~~~~~
555To restrict a component build to module-only, qualify its config symbol
556with "depends on m".  E.g.::
557
558  config FOO
559	depends on BAR && m
560
561limits FOO to module (=m) or disabled (=n).
562
563Compile-testing
564~~~~~~~~~~~~~~~
565If a config symbol has a dependency, but the code controlled by the config
566symbol can still be compiled if the dependency is not met, it is encouraged to
567increase build coverage by adding an "|| COMPILE_TEST" clause to the
568dependency. This is especially useful for drivers for more exotic hardware, as
569it allows continuous-integration systems to compile-test the code on a more
570common system, and detect bugs that way.
571Note that compile-tested code should avoid crashing when run on a system where
572the dependency is not met.
573
574Architecture and platform dependencies
575~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
576Due to the presence of stubs, most drivers can now be compiled on most
577architectures. However, this does not mean it makes sense to have all drivers
578available everywhere, as the actual hardware may only exist on specific
579architectures and platforms. This is especially true for on-SoC IP cores,
580which may be limited to a specific vendor or SoC family.
581
582To prevent asking the user about drivers that cannot be used on the system(s)
583the user is compiling a kernel for, and if it makes sense, config symbols
584controlling the compilation of a driver should contain proper dependencies,
585limiting the visibility of the symbol to (a superset of) the platform(s) the
586driver can be used on. The dependency can be an architecture (e.g. ARM) or
587platform (e.g. ARCH_OMAP4) dependency. This makes life simpler not only for
588distro config owners, but also for every single developer or user who
589configures a kernel.
590
591Such a dependency can be relaxed by combining it with the compile-testing rule
592above, leading to:
593
594  config FOO
595	bool "Support for foo hardware"
596	depends on ARCH_FOO_VENDOR || COMPILE_TEST
597
598Optional dependencies
599~~~~~~~~~~~~~~~~~~~~~
600
601Some drivers are able to optionally use a feature from another module
602or build cleanly with that module disabled, but cause a link failure
603when trying to use that loadable module from a built-in driver.
604
605The most common way to express this optional dependency in Kconfig logic
606uses the slightly counterintuitive::
607
608  config FOO
609	tristate "Support for foo hardware"
610	depends on BAR || !BAR
611
612This means that there is either a dependency on BAR that disallows
613the combination of FOO=y with BAR=m, or BAR is completely disabled. The BAR
614module must provide all the stubs for !BAR case.
615
616For a more formalized approach if there are multiple drivers that have
617the same dependency, a helper symbol can be used, like::
618
619  config FOO
620	tristate "Support for foo hardware"
621	depends on BAR_OPTIONAL
622
623  config BAR_OPTIONAL
624	def_tristate BAR || !BAR
625
626Much less favorable way to express optional dependency is IS_REACHABLE() within
627the module code, useful for example when the module BAR does not provide
628!BAR stubs::
629
630	foo_init()
631	{
632		if (IS_REACHABLE(CONFIG_BAR))
633			bar_register(&foo);
634		...
635	}
636
637IS_REACHABLE() is generally discouraged, because the code will be silently
638discarded, when CONFIG_BAR=m and this code is built-in. This is not what users
639usually expect when enabling BAR as module.
640
641Kconfig recursive dependency limitations
642~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
643
644If you've hit the Kconfig error: "recursive dependency detected" you've run
645into a recursive dependency issue with Kconfig, a recursive dependency can be
646summarized as a circular dependency. The kconfig tools need to ensure that
647Kconfig files comply with specified configuration requirements. In order to do
648that kconfig must determine the values that are possible for all Kconfig
649symbols, this is currently not possible if there is a circular relation
650between two or more Kconfig symbols. For more details refer to the "Simple
651Kconfig recursive issue" subsection below. Kconfig does not do recursive
652dependency resolution; this has a few implications for Kconfig file writers.
653We'll first explain why this issues exists and then provide an example
654technical limitation which this brings upon Kconfig developers. Eager
655developers wishing to try to address this limitation should read the next
656subsections.
657
658Simple Kconfig recursive issue
659~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
660
661Read: Documentation/kbuild/Kconfig.recursion-issue-01
662
663Test with::
664
665  make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
666
667Cumulative Kconfig recursive issue
668~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
669
670Read: Documentation/kbuild/Kconfig.recursion-issue-02
671
672Test with::
673
674  make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
675
676Practical solutions to kconfig recursive issue
677~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678
679Developers who run into the recursive Kconfig issue have two options
680at their disposal. We document them below and also provide a list of
681historical issues resolved through these different solutions.
682
683  a) Remove any superfluous "select FOO" or "depends on FOO"
684  b) Match dependency semantics:
685
686	b1) Swap all "select FOO" to "depends on FOO" or,
687
688	b2) Swap all "depends on FOO" to "select FOO"
689
690The resolution to a) can be tested with the sample Kconfig file
691Documentation/kbuild/Kconfig.recursion-issue-01 through the removal
692of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
693since CORE_BELL_A depends on CORE. At times it may not be possible to remove
694some dependency criteria, for such cases you can work with solution b).
695
696The two different resolutions for b) can be tested in the sample Kconfig file
697Documentation/kbuild/Kconfig.recursion-issue-02.
698
699Below is a list of examples of prior fixes for these types of recursive issues;
700all errors appear to involve one or more "select" statements and one or more
701"depends on".
702
703============    ===================================
704commit          fix
705============    ===================================
70606b718c01208    select A -> depends on A
707c22eacfe82f9    depends on A -> depends on B
7086a91e854442c    select A -> depends on A
709118c565a8f2e    select A -> select B
710f004e5594705    select A -> depends on A
711c7861f37b4c6    depends on A -> (null)
71280c69915e5fb    select A -> (null)              (1)
713c2218e26c0d0    select A -> depends on A        (1)
714d6ae99d04e1c    select A -> depends on A
71595ca19cf8cbf    select A -> depends on A
7168f057d7bca54    depends on A -> (null)
7178f057d7bca54    depends on A -> select A
718a0701f04846e    select A -> depends on A
7190c8b92f7f259    depends on A -> (null)
720e4e9e0540928    select A -> depends on A        (2)
7217453ea886e87    depends on A > (null)           (1)
7227b1fff7e4fdf    select A -> depends on A
72386c747d2a4f0    select A -> depends on A
724d9f9ab51e55e    select A -> depends on A
7250c51a4d8abd6    depends on A -> select A        (3)
726e98062ed6dc4    select A -> depends on A        (3)
72791e5d284a7f1    select A -> (null)
728============    ===================================
729
730(1) Partial (or no) quote of error.
731(2) That seems to be the gist of that fix.
732(3) Same error.
733
734Future kconfig work
735~~~~~~~~~~~~~~~~~~~
736
737Work on kconfig is welcomed on both areas of clarifying semantics and on
738evaluating the use of a full SAT solver for it. A full SAT solver can be
739desirable to enable more complex dependency mappings and / or queries,
740for instance one possible use case for a SAT solver could be that of handling
741the current known recursive dependency issues. It is not known if this would
742address such issues but such evaluation is desirable. If support for a full SAT
743solver proves too complex or that it cannot address recursive dependency issues
744Kconfig should have at least clear and well defined semantics which also
745addresses and documents limitations or requirements such as the ones dealing
746with recursive dependencies.
747
748Further work on both of these areas is welcomed on Kconfig. We elaborate
749on both of these in the next two subsections.
750
751Semantics of Kconfig
752~~~~~~~~~~~~~~~~~~~~
753
754The use of Kconfig is broad, Linux is now only one of Kconfig's users:
755one study has completed a broad analysis of Kconfig use in 12 projects [0]_.
756Despite its widespread use, and although this document does a reasonable job
757in documenting basic Kconfig syntax a more precise definition of Kconfig
758semantics is welcomed. One project deduced Kconfig semantics through
759the use of the xconfig configurator [1]_. Work should be done to confirm if
760the deduced semantics matches our intended Kconfig design goals.
761Another project formalized a denotational semantics of a core subset of
762the Kconfig language [10]_.
763
764Having well defined semantics can be useful for tools for practical
765evaluation of dependencies, for instance one such case was work to
766express in boolean abstraction of the inferred semantics of Kconfig to
767translate Kconfig logic into boolean formulas and run a SAT solver on this to
768find dead code / features (always inactive), 114 dead features were found in
769Linux using this methodology [1]_ (Section 8: Threats to validity).
770The kismet tool, based on the semantics in [10]_, finds abuses of reverse
771dependencies and has led to dozens of committed fixes to Linux Kconfig files [11]_.
772
773Confirming this could prove useful as Kconfig stands as one of the leading
774industrial variability modeling languages [1]_ [2]_. Its study would help
775evaluate practical uses of such languages, their use was only theoretical
776and real world requirements were not well understood. As it stands though
777only reverse engineering techniques have been used to deduce semantics from
778variability modeling languages such as Kconfig [3]_.
779
780.. [0] https://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
781.. [1] https://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
782.. [2] https://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
783.. [3] https://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf
784
785Full SAT solver for Kconfig
786~~~~~~~~~~~~~~~~~~~~~~~~~~~
787
788Although SAT solvers [4]_ haven't yet been used by Kconfig directly, as noted
789in the previous subsection, work has been done however to express in boolean
790abstraction the inferred semantics of Kconfig to translate Kconfig logic into
791boolean formulas and run a SAT solver on it [5]_. Another known related project
792is CADOS [6]_ (former VAMOS [7]_) and the tools, mainly undertaker [8]_, which
793has been introduced first with [9]_.  The basic concept of undertaker is to
794extract variability models from Kconfig and put them together with a
795propositional formula extracted from CPP #ifdefs and build-rules into a SAT
796solver in order to find dead code, dead files, and dead symbols. If using a SAT
797solver is desirable on Kconfig one approach would be to evaluate repurposing
798such efforts somehow on Kconfig. There is enough interest from mentors of
799existing projects to not only help advise how to integrate this work upstream
800but also help maintain it long term. Interested developers should visit:
801
802https://kernelnewbies.org/KernelProjects/kconfig-sat
803
804.. [4] https://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf
805.. [5] https://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
806.. [6] https://cados.cs.fau.de
807.. [7] https://vamos.cs.fau.de
808.. [8] https://undertaker.cs.fau.de
809.. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf
810.. [10] https://paulgazzillo.com/papers/esecfse21.pdf
811.. [11] https://github.com/paulgazz/kmax
812