diff mbox series

[v4,09/12] kconfig: Add files with utility functions

Message ID 20240710065255.10338-10-ole0811sch@gmail.com (mailing list archive)
State New
Headers show
Series kconfig: Add support for conflict resolution | expand

Commit Message

Ole Schuerks July 10, 2024, 6:52 a.m. UTC
This commit contains various helper functions used in the project.

Co-developed-by: Patrick Franz <deltaone@debian.org>
Signed-off-by: Patrick Franz <deltaone@debian.org>
Co-developed-by: Ibrahim Fayaz <phayax@gmail.com>
Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
Reviewed-by: Luis Chamberlain <mcgrof@kernel.org>
Tested-by: Evgeny Groshev <eugene.groshev@gmail.com>
Suggested-by: Sarah Nadi <nadi@ualberta.ca>
Suggested-by: Thorsten Berger <thorsten.berger@rub.de>
Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>
Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
---
 scripts/kconfig/cf_utils.c | 1031 ++++++++++++++++++++++++++++++++++++
 scripts/kconfig/cf_utils.h |  115 ++++
 2 files changed, 1146 insertions(+)
 create mode 100644 scripts/kconfig/cf_utils.c
 create mode 100644 scripts/kconfig/cf_utils.h

Comments

Masahiro Yamada Aug. 12, 2024, 8:48 a.m. UTC | #1
On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@gmail.com> wrote:
>
> This commit contains various helper functions used in the project.
>
> Co-developed-by: Patrick Franz <deltaone@debian.org>
> Signed-off-by: Patrick Franz <deltaone@debian.org>
> Co-developed-by: Ibrahim Fayaz <phayax@gmail.com>
> Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
> Reviewed-by: Luis Chamberlain <mcgrof@kernel.org>
> Tested-by: Evgeny Groshev <eugene.groshev@gmail.com>
> Suggested-by: Sarah Nadi <nadi@ualberta.ca>
> Suggested-by: Thorsten Berger <thorsten.berger@rub.de>
> Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>
> Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
> ---
>  scripts/kconfig/cf_utils.c | 1031 ++++++++++++++++++++++++++++++++++++
>  scripts/kconfig/cf_utils.h |  115 ++++
>  2 files changed, 1146 insertions(+)
>  create mode 100644 scripts/kconfig/cf_utils.c
>  create mode 100644 scripts/kconfig/cf_utils.h
>
> diff --git a/scripts/kconfig/cf_utils.c b/scripts/kconfig/cf_utils.c
> new file mode 100644
> index 000000000000..bcffd0a4fc1b
> --- /dev/null
> +++ b/scripts/kconfig/cf_utils.c
> @@ -0,0 +1,1031 @@
> +// SPDX-License-Identifier: GPL-2.0
> +/*
> + * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
> + */
> +
> +#define _GNU_SOURCE
> +#include <assert.h>
> +#include <locale.h>
> +#include <stdarg.h>
> +#include <stdbool.h>
> +#include <stdio.h>
> +#include <stdlib.h>
> +#include <string.h>
> +#include <time.h>
> +#include <unistd.h>
> +#include <ctype.h>
> +
> +#include "configfix.h"
> +#include "internal.h"
> +
> +#define SATMAP_INIT_SIZE 2
> +
> +static PicoSAT *pico;
> +
> +static void unfold_cnf_clause(struct pexpr *e);
> +static void build_cnf_tseytin(struct pexpr *e, struct cfdata *data);
> +
> +static void build_cnf_tseytin_top_and(struct pexpr *e, struct cfdata *data);
> +static void build_cnf_tseytin_top_or(struct pexpr *e, struct cfdata *data);
> +
> +static void build_cnf_tseytin_tmp(struct pexpr *e, struct fexpr *t, struct cfdata *data);
> +static void build_cnf_tseytin_and(struct pexpr *e, struct fexpr *t, struct cfdata *data);
> +static void build_cnf_tseytin_or(struct pexpr *e, struct fexpr *t, struct cfdata *data);
> +static int pexpr_satval(struct pexpr *e);
> +
> +/*
> + * parse Kconfig-file and read .config
> + */
> +void init_config(const char *Kconfig_file)
> +{
> +       conf_parse(Kconfig_file);
> +       conf_read(NULL);
> +}
> +
> +/*
> + * initialize satmap
> + */
> +void init_data(struct cfdata *data)
> +{
> +       /* create hashtable with all fexpr */
> +       data->satmap = xcalloc(SATMAP_INIT_SIZE, sizeof(**data->satmap));
> +       data->satmap_size = SATMAP_INIT_SIZE;


This is a bug.

xcalloc() allocated much bigger memory than used.




> +       printd("done.\n");
> +}
> +
> +/*
> + * create SAT-variables for all fexpr
> + */
> +void create_sat_variables(struct cfdata *data)
> +{
> +       struct symbol *sym;
> +
> +       printd("Creating SAT-variables...");
> +
> +       for_all_symbols(sym) {
> +               sym->constraints = pexpr_list_init();
> +               sym_create_fexpr(sym, data);
> +       }
> +
> +       printd("done.\n");
> +}
> +
> +/*
> + * create various constants
> + */
> +void create_constants(struct cfdata *data)
> +{
> +       printd("Creating constants...");
> +
> +       /* create TRUE and FALSE constants */
> +       data->constants->const_false = fexpr_create(data->sat_variable_nr++, FE_FALSE, "False");
> +       // const_false = fexpr_create(sat_variable_nr++, FE_FALSE, "False");
> +       fexpr_add_to_satmap(data->constants->const_false, data);
> +
> +       data->constants->const_true = fexpr_create(data->sat_variable_nr++, FE_TRUE, "True");
> +       fexpr_add_to_satmap(data->constants->const_true, data);
> +
> +       /* add fexpr of constants to tristate constants */
> +       symbol_yes.fexpr_y = data->constants->const_true;
> +       symbol_yes.fexpr_m = data->constants->const_false;
> +
> +       symbol_mod.fexpr_y = data->constants->const_false;
> +       symbol_mod.fexpr_m = data->constants->const_true;
> +
> +       symbol_no.fexpr_y = data->constants->const_false;
> +       symbol_no.fexpr_m = data->constants->const_false;
> +
> +       /* create symbols yes/mod/no as fexpr */
> +       data->constants->symbol_yes_fexpr = fexpr_create(0, FE_SYMBOL, "y");
> +       data->constants->symbol_yes_fexpr->sym = &symbol_yes;
> +       data->constants->symbol_yes_fexpr->tri = yes;
> +
> +       data->constants->symbol_mod_fexpr = fexpr_create(0, FE_SYMBOL, "m");
> +       data->constants->symbol_mod_fexpr->sym = &symbol_mod;
> +       data->constants->symbol_mod_fexpr->tri = mod;
> +
> +       data->constants->symbol_no_fexpr = fexpr_create(0, FE_SYMBOL, "n");
> +       data->constants->symbol_no_fexpr->sym = &symbol_no;
> +       data->constants->symbol_no_fexpr->tri = no;
> +
> +       printd("done.\n");
> +}
> +
> +/*
> + * create a temporary SAT-variable
> + */
> +struct fexpr *create_tmpsatvar(struct cfdata *data)
> +{
> +       char *name = get_tmp_var_as_char(data->tmp_variable_nr);
> +       struct fexpr *t = fexpr_create(data->sat_variable_nr++, FE_TMPSATVAR, name);
> +
> +       ++data->tmp_variable_nr;
> +       fexpr_add_to_satmap(t, data);
> +
> +       free(name);
> +       return t;
> +}
> +
> +/*
> + * return a temporary SAT variable as string
> + */
> +char *get_tmp_var_as_char(int i)
> +{
> +       char *val = malloc(sizeof(char) * 18);
> +
> +       snprintf(val, 18, "T_%d", i);
> +       return val;
> +}
> +
> +/*
> + * return a tristate value as a char *
> + */
> +char *tristate_get_char(tristate val)
> +{
> +       switch (val) {
> +       case yes:
> +               return "yes";
> +       case mod:
> +               return "mod";
> +       case no:
> +               return "no";
> +       default:
> +               return "";
> +       }
> +}
> +
> +/*
> + *check whether an expr can evaluate to mod
> + */
> +bool expr_can_evaluate_to_mod(struct expr *e)
> +{
> +       if (!e)
> +               return false;
> +
> +       switch (e->type) {
> +       case E_SYMBOL:
> +               return e->left.sym == &symbol_mod || e->left.sym->type == S_TRISTATE ? true : false;
> +       case E_AND:
> +       case E_OR:
> +               return expr_can_evaluate_to_mod(e->left.expr) ||
> +                      expr_can_evaluate_to_mod(e->right.expr);
> +       case E_NOT:
> +               return expr_can_evaluate_to_mod(e->left.expr);
> +       default:
> +               return false;
> +       }
> +}
> +
> +/*
> + * check whether an expr is a non-Boolean constant
> + */
> +bool expr_is_nonbool_constant(struct expr *e)
> +{
> +       if (e->type != E_SYMBOL)
> +               return false;
> +       if (e->left.sym->type != S_UNKNOWN)
> +               return false;
> +
> +       if (e->left.sym->flags & SYMBOL_CONST)
> +               return true;
> +
> +       return string_is_number(e->left.sym->name) || string_is_hex(e->left.sym->name);
> +}
> +
> +/*
> + * check whether a symbol is a non-Boolean constant
> + */
> +bool sym_is_nonbool_constant(struct symbol *sym)
> +{
> +       if (sym->type != S_UNKNOWN)
> +               return false;
> +
> +       if (sym->flags & SYMBOL_CONST)
> +               return true;
> +
> +       return string_is_number(sym->name) || string_is_hex(sym->name);
> +}
> +
> +/*
> + * print an expr
> + */
> +static void print_expr_util(struct expr *e, int prevtoken)
> +{
> +       if (!e)
> +               return;
> +
> +       switch (e->type) {
> +       case E_SYMBOL:
> +               if (sym_get_name(e->left.sym) != NULL)
> +                       printf("%s", sym_get_name(e->left.sym));
> +               else
> +                       printf("left was null\n");
> +               break;
> +       case E_NOT:
> +               printf("!");
> +               print_expr_util(e->left.expr, E_NOT);
> +               break;
> +       case E_AND:
> +               if (prevtoken != E_AND && prevtoken != 0)
> +                       printf("(");
> +               print_expr_util(e->left.expr, E_AND);
> +               printf(" && ");
> +               print_expr_util(e->right.expr, E_AND);
> +               if (prevtoken != E_AND && prevtoken != 0)
> +                       printf(")");
> +               break;
> +       case E_OR:
> +               if (prevtoken != E_OR && prevtoken != 0)
> +                       printf("(");
> +               print_expr_util(e->left.expr, E_OR);
> +               printf(" || ");
> +               print_expr_util(e->right.expr, E_OR);
> +               if (prevtoken != E_OR && prevtoken != 0)
> +                       printf(")");
> +               break;
> +       case E_EQUAL:
> +       case E_UNEQUAL:
> +               if (e->left.sym->name)
> +                       printf("%s", e->left.sym->name);
> +               else
> +                       printf("left was null\n");
> +               printf("%s", e->type == E_EQUAL ? "=" : "!=");
> +               printf("%s", e->right.sym->name);
> +               break;
> +       case E_LEQ:
> +       case E_LTH:
> +               if (e->left.sym->name)
> +                       printf("%s", e->left.sym->name);
> +               else
> +                       printf("left was null\n");
> +               printf("%s", e->type == E_LEQ ? "<=" : "<");
> +               printf("%s", e->right.sym->name);
> +               break;
> +       case E_GEQ:
> +       case E_GTH:
> +               if (e->left.sym->name)
> +                       printf("%s", e->left.sym->name);
> +               else
> +                       printf("left was null\n");
> +               printf("%s", e->type == E_GEQ ? ">=" : ">");
> +               printf("%s", e->right.sym->name);
> +               break;
> +       case E_RANGE:
> +               printf("[");
> +               printf("%s", e->left.sym->name);
> +               printf(" ");
> +               printf("%s", e->right.sym->name);
> +               printf("]");
> +               break;
> +       default:
> +               break;
> +       }
> +}
> +void print_expr(char *tag, struct expr *e, int prevtoken)
> +{
> +       printf("%s ", tag);
> +       print_expr_util(e, prevtoken);
> +       printf("\n");
> +}
> +


This is the same as the existing expr_fprint() except that
it prints the 'tag'.


If you need this, presumably you need to do code refactoring.







> +/*
> + * check, if the symbol is a tristate-constant
> + */
> +bool sym_is_tristate_constant(struct symbol *sym)
> +{
> +       return sym == &symbol_yes || sym == &symbol_mod || sym == &symbol_no;
> +}
> +
> +/*
> + * check, if a symbol is of type boolean or tristate
> + */
> +bool sym_is_boolean(struct symbol *sym)
> +{
> +       return sym->type == S_BOOLEAN || sym->type == S_TRISTATE;
> +}
> +
> +/*
> + * check, if a symbol is a boolean/tristate or a tristate constant
> + */
> +bool sym_is_bool_or_triconst(struct symbol *sym)
> +{
> +       return sym_is_tristate_constant(sym) || sym_is_boolean(sym);
> +}
> +
> +/*
> + * check, if a symbol is of type int, hex, or string
> + */
> +bool sym_is_nonboolean(struct symbol *sym)
> +{
> +       return sym->type == S_INT || sym->type == S_HEX || sym->type == S_STRING;
> +}
> +
> +/*
> + * check, if a symbol has a prompt
> + */
> +bool sym_has_prompt(struct symbol *sym)
> +{
> +       struct property *prop;
> +
> +       for_all_prompts(sym, prop)
> +               return true;
> +
> +       return false;
> +}
> +
> +/*
> + * return the prompt of the symbol if there is one, NULL otherwise
> + */
> +struct property *sym_get_prompt(struct symbol *sym)
> +{
> +       struct property *prop;
> +
> +       for_all_prompts(sym, prop)
> +               return prop;
> +
> +       return NULL;
> +}
> +
> +/*
> + * return the condition for the property, NULL if there is none. To be pexpr_put
> + * by caller.
> + */
> +struct pexpr *prop_get_condition(struct property *prop, struct cfdata *data)
> +{
> +       if (prop == NULL)
> +               return NULL;
> +
> +       /* if there is no condition, return True */
> +       if (!prop->visible.expr)
> +               return pexf(data->constants->const_true);
> +
> +       return expr_calculate_pexpr_both(prop->visible.expr, data);
> +}
> +
> +/*
> + * return the default property, NULL if none exists or can be satisfied
> + */
> +struct property *sym_get_default_prop(struct symbol *sym)
> +{
> +       struct property *prop;
> +
> +       for_all_defaults(sym, prop) {
> +               prop->visible.tri = expr_calc_value(prop->visible.expr);
> +               if (prop->visible.tri != no)
> +                       return prop;
> +       }
> +       return NULL;
> +}
> +
> +/*
> + * check whether a non-boolean symbol has a value set
> + */
> +bool sym_nonbool_has_value_set(struct symbol *sym)
> +{
> +       /*
> +        * The built constraints make the following constraints:
> +        *
> +        * visible -> not 'n'
> +        * sym->dir_dep not fulfilled -> 'n'
> +        * invisible -> (no default's condition is fulfilled <-> 'n')
> +        */
> +       struct property *prompt;
> +       struct property *p;
> +
> +       if (!sym_is_nonboolean(sym))
> +               return false;
> +
> +       /* cannot have a value with unmet dependencies */
> +       if (sym->dir_dep.expr && sym->dir_dep.tri == no)
> +               return false;
> +
> +       /* visible prompt => value set */
> +       prompt = sym_get_prompt(sym);
> +       if (prompt != NULL && prompt->visible.tri != no)
> +               return true;
> +
> +       /* invisible prompt => must get value from default value */
> +       p = sym_get_default_prop(sym);
> +       return p != NULL;
> +}
> +
> +/*
> + * return pointer to the name of the symbol or the current prompt-text, if it
> + * is a choice symbol
> + */
> +const char *sym_get_name(struct symbol *sym)
> +{
> +       if (sym_is_choice(sym)) {
> +               struct property *prompt = sym_get_prompt(sym);
> +
> +               if (prompt == NULL)
> +                       return "";
> +
> +               return prompt->text;
> +       } else {
> +               return sym->name;
> +       }
> +}
> +
> +/*
> + * check whether symbol is to be changed
> + */
> +bool sym_is_sdv(struct sdv_list *list, struct symbol *sym)
> +{
> +       struct sdv_node *node;
> +
> +       sdv_list_for_each(node, list)
> +               if (sym == node->elem->sym)
> +                       return true;
> +
> +       return false;
> +}
> +
> +/*
> + * print a symbol's name
> + */
> +void print_sym_name(struct symbol *sym)
> +{
> +       printf("Symbol: ");
> +       if (sym_is_choice(sym)) {
> +               struct property *prompt = sym_get_prompt(sym);
> +
> +               printf("(Choice) %s", prompt->text);
> +       } else  {
> +               printf("%s", sym->name);
> +       }
> +       printf("\n");
> +}
> +
> +/*
> + * print all constraints for a symbol
> + */
> +void print_sym_constraint(struct symbol *sym)
> +{
> +       struct pexpr_node *node;
> +
> +       pexpr_list_for_each(node, sym->constraints)
> +               pexpr_print("::", node->elem, -1);
> +}
> +
> +/*
> + * print a default map
> + */
> +void print_default_map(struct defm_list *map)
> +{
> +       struct default_map *entry;
> +       struct defm_node *node;
> +
> +       defm_list_for_each(node, map) {
> +               struct gstr s = str_new();
> +
> +               entry = node->elem;
> +
> +               str_append(&s, "\t");
> +               str_append(&s, str_get(&entry->val->name));
> +               str_append(&s, " ->");
> +               pexpr_print(strdup(str_get(&s)), entry->e, -1);
> +               str_free(&s);
> +       }
> +}
> +
> +/*
> + * check whether a string is a number
> + */
> +bool string_is_number(char *s)
> +{
> +       int len = strlen(s);
> +       int i = 0;
> +
> +       while (i < len) {
> +               if (!isdigit(s[i]))
> +                       return false;
> +               i++;
> +       }
> +
> +       return true;
> +}
> +
> +/*
> + * check whether a string is a hexadecimal number
> + */
> +bool string_is_hex(char *s)
> +{
> +       int len = strlen(s);
> +       int i = 2;
> +
> +       if (len >= 3 && s[0] == '0' && s[1] == 'x') {
> +               while (i < len) {
> +                       if (!isxdigit(s[i]))
> +                               return false;
> +                       i++;
> +               }
> +               return true;
> +       } else {
> +               return false;
> +       }
> +}
> +
> +/*
> + * initialize PicoSAT
> + */
> +PicoSAT *initialize_picosat(void)
> +{
> +       PicoSAT *pico;
> +
> +       printd("\nInitializing PicoSAT...");
> +       pico = picosat_init();
> +       picosat_enable_trace_generation(pico);
> +       printd("done.\n");
> +
> +       return pico;
> +}
> +
> +/*
> + * construct the CNF-clauses from the constraints
> + */
> +void construct_cnf_clauses(PicoSAT *p, struct cfdata *data)
> +{
> +       struct symbol *sym;
> +
> +       pico = p;
> +
> +       /* adding unit-clauses for constants */
> +       sat_add_clause(2, pico, -(data->constants->const_false->satval));
> +       sat_add_clause(2, pico, data->constants->const_true->satval);
> +
> +       for_all_symbols(sym) {
> +               struct pexpr_node *node;
> +
> +               if (sym->type == S_UNKNOWN)
> +                       continue;
> +
> +               pexpr_list_for_each(node, sym->constraints) {
> +                       if (pexpr_is_cnf(node->elem)) {
> +                               unfold_cnf_clause(node->elem);
> +                               picosat_add(pico, 0);
> +                       } else {
> +                               build_cnf_tseytin(node->elem, data);
> +                       }
> +
> +               }
> +       }
> +}
> +
> +/*
> + * helper function to add an expression to a CNF-clause
> + */
> +static void unfold_cnf_clause(struct pexpr *e)
> +{
> +       switch (e->type) {
> +       case PE_SYMBOL:
> +               picosat_add(pico, e->left.fexpr->satval);
> +               break;
> +       case PE_OR:
> +               unfold_cnf_clause(e->left.pexpr);
> +               unfold_cnf_clause(e->right.pexpr);
> +               break;
> +       case PE_NOT:
> +               picosat_add(pico, -(e->left.pexpr->left.fexpr->satval));
> +               break;
> +       default:
> +               perror("Not in CNF, FE_EQUALS.");
> +       }
> +}
> +
> +/*
> + * build CNF-clauses for a pexpr not in CNF
> + */
> +static void build_cnf_tseytin(struct pexpr *e, struct cfdata *data)
> +{
> +       switch (e->type) {
> +       case PE_AND:
> +               build_cnf_tseytin_top_and(e, data);
> +               break;
> +       case PE_OR:
> +               build_cnf_tseytin_top_or(e, data);
> +               break;
> +       default:
> +               perror("Expression not a propositional logic formula. root.");
> +       }
> +}
> +
> +/*
> + * split up a pexpr of type AND as both sides must be satisfied
> + */
> +static void build_cnf_tseytin_top_and(struct pexpr *e, struct cfdata *data)
> +{
> +       if (pexpr_is_cnf(e->left.pexpr))
> +               unfold_cnf_clause(e->left.pexpr);
> +       else
> +               build_cnf_tseytin(e->left.pexpr, data);
> +
> +       if (pexpr_is_cnf(e->right.pexpr))
> +               unfold_cnf_clause(e->right.pexpr);
> +       else
> +               build_cnf_tseytin(e->right.pexpr, data);
> +
> +}
> +
> +static void build_cnf_tseytin_top_or(struct pexpr *e, struct cfdata *data)
> +{
> +       struct fexpr *t1 = NULL, *t2 = NULL;
> +       int a, b;
> +
> +       /* set left side */
> +       if (pexpr_is_symbol(e->left.pexpr)) {
> +               a = pexpr_satval(e->left.pexpr);
> +       } else {
> +               t1 = create_tmpsatvar(data);
> +               a = t1->satval;
> +       }
> +
> +       /* set right side */
> +       if (pexpr_is_symbol(e->right.pexpr)) {
> +               b = pexpr_satval(e->right.pexpr);
> +       } else {
> +               t2 = create_tmpsatvar(data);
> +               b = t2->satval;
> +       }
> +
> +       /* A v B */
> +       sat_add_clause(3, pico, a, b);
> +
> +       /* traverse down the tree to build more constraints if needed */
> +       if (!pexpr_is_symbol(e->left.pexpr)) {
> +               if (t1 == NULL)
> +                       perror("t1 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
> +       }
> +
> +       if (!pexpr_is_symbol(e->right.pexpr)) {
> +               if (t2 == NULL)
> +                       perror("t2 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
> +       }
> +}
> +
> +/*
> + * build the sub-expressions
> + */
> +static void build_cnf_tseytin_tmp(struct pexpr *e, struct fexpr *t, struct cfdata *data)
> +{
> +       switch (e->type) {
> +       case PE_AND:
> +               build_cnf_tseytin_and(e, t, data);
> +               break;
> +       case PE_OR:
> +               build_cnf_tseytin_or(e, t, data);
> +               break;
> +       default:
> +               perror("Expression not a propositional logic formula. root.");
> +       }
> +}
> +
> +/*
> + * build the Tseytin sub-expressions for a pexpr of type AND
> + */
> +static void build_cnf_tseytin_and(struct pexpr *e, struct fexpr *t, struct cfdata *data)
> +{
> +       struct fexpr *t1 = NULL, *t2 = NULL;
> +       int a, b, c;
> +
> +       assert(t != NULL);
> +
> +       /* set left side */
> +       if (pexpr_is_symbol(e->left.pexpr)) {
> +               a = pexpr_satval(e->left.pexpr);
> +       } else {
> +               t1 = create_tmpsatvar(data);
> +               a = t1->satval;
> +       }
> +
> +       /* set right side */
> +       if (pexpr_is_symbol(e->right.pexpr)) {
> +               b = pexpr_satval(e->right.pexpr);
> +       } else {
> +               t2 = create_tmpsatvar(data);
> +               b = t2->satval;
> +       }
> +
> +       c = t->satval;
> +
> +       /* -A v -B v C */
> +       sat_add_clause(4, pico, -a, -b, c);
> +       /* A v -C */
> +       sat_add_clause(3, pico, a, -c);
> +       /* B v -C */
> +       sat_add_clause(3, pico, b, -c);
> +
> +       /* traverse down the tree to build more constraints if needed */
> +       if (!pexpr_is_symbol(e->left.pexpr)) {
> +               if (t1 == NULL)
> +                       perror("t1 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
> +       }
> +       if (!pexpr_is_symbol(e->right.pexpr)) {
> +               if (t2 == NULL)
> +                       perror("t2 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
> +       }
> +}
> +
> +/*
> + * build the Tseytin sub-expressions for a pexpr of type
> + */
> +static void build_cnf_tseytin_or(struct pexpr *e, struct fexpr *t, struct cfdata *data)
> +{
> +       struct fexpr *t1 = NULL, *t2 = NULL;
> +       int a, b, c;
> +
> +       assert(t != NULL);
> +
> +       /* set left side */
> +       if (pexpr_is_symbol(e->left.pexpr)) {
> +               a = pexpr_satval(e->left.pexpr);
> +       } else {
> +               t1 = create_tmpsatvar(data);
> +               a = t1->satval;
> +       }
> +
> +       /* set right side */
> +       if (pexpr_is_symbol(e->right.pexpr)) {
> +               b = pexpr_satval(e->right.pexpr);
> +       } else {
> +               t2 = create_tmpsatvar(data);
> +               b = t2->satval;
> +       }
> +
> +       c = t->satval;
> +
> +       /* A v B v -C */
> +       sat_add_clause(4, pico, a, b, -c);
> +       /* -A v C */;
> +       sat_add_clause(3, pico, -a, c);
> +       /* -B v C */
> +       sat_add_clause(3, pico, -b, c);
> +
> +       /* traverse down the tree to build more constraints if needed */
> +       if (!pexpr_is_symbol(e->left.pexpr)) {
> +               if (t1 == NULL)
> +                       perror("t1 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
> +       }
> +       if (!pexpr_is_symbol(e->right.pexpr)) {
> +               if (t2 == NULL)
> +                       perror("t2 is NULL.");
> +
> +               build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
> +       }
> +}
> +
> +/*
> + * add a clause to PicoSAT
> + * First argument must be the SAT solver
> + */
> +void sat_add_clause(int num, ...)
> +{
> +       va_list valist;
> +       int lit;
> +       PicoSAT *pico;
> +
> +       if (num <= 1)
> +               return;
> +
> +       va_start(valist, num);
> +
> +       pico = va_arg(valist, PicoSAT *);
> +
> +       /* access all the arguments assigned to valist */
> +       for (int i = 1; i < num; i++) {
> +               lit = va_arg(valist, int);
> +               picosat_add(pico, lit);
> +       }
> +       picosat_add(pico, 0);
> +
> +       va_end(valist);
> +}
> +
> +/*
> + * return the SAT-variable for a pexpr that is a symbol
> + */
> +static int pexpr_satval(struct pexpr *e)
> +{
> +       if (!pexpr_is_symbol(e)) {
> +               perror("pexpr is not a symbol.");
> +               return -1;
> +       }
> +
> +       switch (e->type) {
> +       case PE_SYMBOL:
> +               return e->left.fexpr->satval;
> +       case PE_NOT:
> +               return -(e->left.pexpr->left.fexpr->satval);
> +       default:
> +               perror("Not a symbol.");
> +       }
> +
> +       return -1;
> +}
> +
> +/*
> + * start PicoSAT
> + */
> +void picosat_solve(PicoSAT *pico, struct cfdata *data)
> +{
> +       clock_t start, end;
> +       double time;
> +       int res;
> +
> +       printd("Solving SAT-problem...");
> +
> +       start = clock();
> +       res = picosat_sat(pico, -1);
> +       end = clock();
> +
> +       time = ((double) (end - start)) / CLOCKS_PER_SEC;
> +       printd("done. (%.6f secs.)\n\n", time);
> +
> +       if (res == PICOSAT_SATISFIABLE) {
> +               printd("===> PROBLEM IS SATISFIABLE <===\n");
> +
> +       } else if (res == PICOSAT_UNSATISFIABLE) {
> +               struct fexpr *e;
> +               int lit;
> +               const int *i;
> +
> +               printd("===> PROBLEM IS UNSATISFIABLE <===\n");
> +
> +               /* print unsat core */
> +               printd("\nPrinting unsatisfiable core:\n");
> +
> +               i = picosat_failed_assumptions(pico);
> +               lit = abs(*i++);
> +
> +               while (lit != 0) {
> +                       e = data->satmap[lit];
> +
> +                       printd("(%d) %s <%d>\n", lit, str_get(&e->name), e->assumption);
> +                       lit = abs(*i++);
> +               }
> +       } else {
> +               printd("Unknown if satisfiable.\n");
> +       }
> +}
> +
> +/*
> + * add assumption for a symbol to the SAT-solver
> + */
> +void sym_add_assumption(PicoSAT *pico, struct symbol *sym)
> +{
> +       if (sym_is_boolean(sym)) {
> +               int tri_val = sym_get_tristate_value(sym);
> +
> +               sym_add_assumption_tri(pico, sym, tri_val);
> +               return;
> +       }
> +
> +       if (sym_is_nonboolean(sym)) {
> +               struct fexpr *e = sym->nb_vals->head->elem;
> +               struct fexpr_node *node;
> +
> +               const char *string_val = sym_get_string_value(sym);
> +
> +               if (sym->type == S_STRING && !strcmp(string_val, ""))
> +                       return;
> +
> +               /* symbol does not have a value */
> +               if (!sym_nonbool_has_value_set(sym)) {
> +                       /* set value for sym=n */
> +                       picosat_assume(pico, e->satval);
> +                       e->assumption = true;
> +
> +                       for (node = sym->nb_vals->head->next; node != NULL; node = node->next) {
> +                               picosat_assume(pico, -(node->elem->satval));
> +                               node->elem->assumption = false;
> +                       }
> +
> +                       return;
> +               }
> +
> +               /* symbol does have a value set */
> +
> +               /* set value for sym=n */
> +               picosat_assume(pico, -(e->satval));
> +               e->assumption = false;
> +
> +               /* set value for all other fexpr */
> +               fexpr_list_for_each(node, sym->nb_vals) {
> +                       if (node->prev == NULL)
> +                               continue;
> +
> +                       if (strcmp(str_get(&node->elem->nb_val), string_val) == 0) {
> +                               picosat_assume(pico, node->elem->satval);
> +                               node->elem->assumption = true;
> +                       } else {
> +                               picosat_assume(pico, -(node->elem->satval));
> +                               node->elem->assumption = false;
> +                       }
> +               }
> +       }
> +}
> +
> +/*
> + * add assumption for a boolean symbol to the SAT-solver
> + */
> +void sym_add_assumption_tri(PicoSAT *pico, struct symbol *sym, tristate tri_val)
> +{
> +       if (sym->type == S_BOOLEAN) {
> +               int a = sym->fexpr_y->satval;
> +
> +               switch (tri_val) {
> +               case no:
> +                       picosat_assume(pico, -a);
> +                       sym->fexpr_y->assumption = false;
> +                       break;
> +               case mod:
> +                       perror("Should not happen. Boolean symbol is set to mod.\n");
> +                       break;
> +               case yes:
> +
> +                       picosat_assume(pico, a);
> +                       sym->fexpr_y->assumption = true;
> +                       break;
> +               }
> +       }
> +       if (sym->type == S_TRISTATE) {
> +               int a = sym->fexpr_y->satval;
> +               int a_m = sym->fexpr_m->satval;
> +
> +               switch (tri_val) {
> +               case no:
> +                       picosat_assume(pico, -a);
> +                       picosat_assume(pico, -a_m);
> +                       sym->fexpr_y->assumption = false;
> +                       sym->fexpr_m->assumption = false;
> +                       break;
> +               case mod:
> +                       picosat_assume(pico, -a);
> +                       picosat_assume(pico, a_m);
> +                       sym->fexpr_y->assumption = false;
> +                       sym->fexpr_m->assumption = true;
> +                       break;
> +               case yes:
> +                       picosat_assume(pico, a);
> +                       picosat_assume(pico, -a_m);
> +                       sym->fexpr_y->assumption = true;
> +                       sym->fexpr_m->assumption = false;
> +                       break;
> +               }
> +       }
> +}
> +
> +/*
> + * add assumptions for the symbols to be changed to the SAT solver
> + */
> +void sym_add_assumption_sdv(PicoSAT *pico, struct sdv_list *list)
> +{
> +       struct symbol_dvalue *sdv;
> +       struct sdv_node *node;
> +       int lit_y, lit_m;
> +
> +       sdv_list_for_each(node, list) {
> +               sdv = node->elem;
> +               lit_y = sdv->sym->fexpr_y->satval;
> +
> +               if (sdv->sym->type == S_BOOLEAN) {
> +                       switch (sdv->tri) {
> +                       case yes:
> +                               picosat_assume(pico, lit_y);
> +                               break;
> +                       case no:
> +                               picosat_assume(pico, -lit_y);
> +                               break;
> +                       case mod:
> +                               perror("Should not happen.\n");
> +                       }
> +               } else if (sdv->sym->type == S_TRISTATE) {
> +                       lit_m = sdv->sym->fexpr_m->satval;
> +
> +                       switch (sdv->tri) {
> +                       case yes:
> +                               picosat_assume(pico, lit_y);
> +                               picosat_assume(pico, -lit_m);
> +                               break;
> +                       case mod:
> +                               picosat_assume(pico, -lit_y);
> +                               picosat_assume(pico, lit_m);
> +                               break;
> +                       case no:
> +                               picosat_assume(pico, -lit_y);
> +                               picosat_assume(pico, -lit_m);
> +                       }
> +               }
> +       }
> +}
> diff --git a/scripts/kconfig/cf_utils.h b/scripts/kconfig/cf_utils.h
> new file mode 100644
> index 000000000000..b71c8731a8ff
> --- /dev/null
> +++ b/scripts/kconfig/cf_utils.h
> @@ -0,0 +1,115 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
> + */
> +
> +#ifndef CF_UTILS_H
> +#define CF_UTILS_H
> +
> +#include "expr.h"
> +#include "cf_defs.h"
> +#include "picosat.h"
> +
> +/* parse Kconfig-file and read .config */
> +void init_config(const char *Kconfig_file);
> +
> +/* initialize satmap and cnf_clauses */
> +void init_data(struct cfdata *data);
> +
> +/* assign SAT-variables to all fexpr and create the sat_map */
> +void create_sat_variables(struct cfdata *data);
> +
> +/* create True/False constants */
> +void create_constants(struct cfdata *data);
> +
> +/* create a temporary SAT-variable */
> +struct fexpr *create_tmpsatvar(struct cfdata *data);
> +
> +/* return a temporary SAT variable as string */
> +char *get_tmp_var_as_char(int i);
> +
> +/* return a tristate value as a char * */
> +char *tristate_get_char(tristate val);
> +
> +/* check whether an expr can evaluate to mod */
> +bool expr_can_evaluate_to_mod(struct expr *e);
> +
> +/* check whether an expr is a non-Boolean constant */
> +bool expr_is_nonbool_constant(struct expr *e);
> +
> +/* check whether a symbol is a non-Boolean constant */
> +bool sym_is_nonbool_constant(struct symbol *sym);
> +
> +/* print an expr */
> +void print_expr(char *tag, struct expr *e, int prevtoken);
> +
> +/* check, if the symbol is a tristate-constant */
> +bool sym_is_tristate_constant(struct symbol *sym);
> +
> +/* check, if a symbol is of type boolean or tristate */
> +bool sym_is_boolean(struct symbol *sym);
> +
> +/* check, if a symbol is a boolean/tristate or a tristate constant */
> +bool sym_is_bool_or_triconst(struct symbol *sym);
> +
> +/* check, if a symbol is of type int, hex, or string */
> +bool sym_is_nonboolean(struct symbol *sym);
> +
> +/* check, if a symbol has a prompt */
> +bool sym_has_prompt(struct symbol *sym);
> +
> +/* return the prompt of the symbol, if there is one */
> +struct property *sym_get_prompt(struct symbol *sym);
> +
> +/* return the condition for the property, True if there is none */
> +struct pexpr *prop_get_condition(struct property *prop, struct cfdata *data);
> +
> +/* return the default property, NULL if none exists or can be satisfied */
> +struct property *sym_get_default_prop(struct symbol *sym);
> +
> +/* check whether a non-boolean symbol has a value set */
> +bool sym_nonbool_has_value_set(struct symbol *sym);
> +
> +/* return the name of the symbol */
> +const char *sym_get_name(struct symbol *sym);
> +
> +/* check whether symbol is to be changed */
> +bool sym_is_sdv(struct sdv_list *list, struct symbol *sym);
> +
> +/* print a symbol's name */
> +void print_sym_name(struct symbol *sym);
> +
> +/* print all constraints for a symbol */
> +void print_sym_constraint(struct symbol *sym);
> +
> +/* print a default map */
> +void print_default_map(struct defm_list *map);
> +
> +/* check whether a string is a number */
> +bool string_is_number(char *s);
> +
> +/* check whether a string is a hexadecimal number */
> +bool string_is_hex(char *s);
> +
> +/* initialize PicoSAT */
> +PicoSAT *initialize_picosat(void);
> +
> +/* construct the CNF-clauses from the constraints */
> +void construct_cnf_clauses(PicoSAT *pico, struct cfdata *data);
> +
> +/* add a clause to PicoSAT */
> +void sat_add_clause(int num, ...);
> +
> +/* start PicoSAT */
> +void picosat_solve(PicoSAT *pico, struct cfdata *data);
> +
> +/* add assumption for a symbol to the SAT-solver */
> +void sym_add_assumption(PicoSAT *pico, struct symbol *sym);
> +
> +/* add assumption for a boolean symbol to the SAT-solver */
> +void sym_add_assumption_tri(PicoSAT *pico, struct symbol *sym, tristate tri_val);
> +
> +/* add assumptions for the symbols to be changed to the SAT solver */
> +void sym_add_assumption_sdv(PicoSAT *pico, struct sdv_list *list);
> +
> +#endif
> --
> 2.39.2
>


--
Best Regards

Masahiro Yamada
diff mbox series

Patch

diff --git a/scripts/kconfig/cf_utils.c b/scripts/kconfig/cf_utils.c
new file mode 100644
index 000000000000..bcffd0a4fc1b
--- /dev/null
+++ b/scripts/kconfig/cf_utils.c
@@ -0,0 +1,1031 @@ 
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
+ */
+
+#define _GNU_SOURCE
+#include <assert.h>
+#include <locale.h>
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+#include <unistd.h>
+#include <ctype.h>
+
+#include "configfix.h"
+#include "internal.h"
+
+#define SATMAP_INIT_SIZE 2
+
+static PicoSAT *pico;
+
+static void unfold_cnf_clause(struct pexpr *e);
+static void build_cnf_tseytin(struct pexpr *e, struct cfdata *data);
+
+static void build_cnf_tseytin_top_and(struct pexpr *e, struct cfdata *data);
+static void build_cnf_tseytin_top_or(struct pexpr *e, struct cfdata *data);
+
+static void build_cnf_tseytin_tmp(struct pexpr *e, struct fexpr *t, struct cfdata *data);
+static void build_cnf_tseytin_and(struct pexpr *e, struct fexpr *t, struct cfdata *data);
+static void build_cnf_tseytin_or(struct pexpr *e, struct fexpr *t, struct cfdata *data);
+static int pexpr_satval(struct pexpr *e);
+
+/*
+ * parse Kconfig-file and read .config
+ */
+void init_config(const char *Kconfig_file)
+{
+	conf_parse(Kconfig_file);
+	conf_read(NULL);
+}
+
+/*
+ * initialize satmap
+ */
+void init_data(struct cfdata *data)
+{
+	/* create hashtable with all fexpr */
+	data->satmap = xcalloc(SATMAP_INIT_SIZE, sizeof(**data->satmap));
+	data->satmap_size = SATMAP_INIT_SIZE;
+
+	printd("done.\n");
+}
+
+/*
+ * create SAT-variables for all fexpr
+ */
+void create_sat_variables(struct cfdata *data)
+{
+	struct symbol *sym;
+
+	printd("Creating SAT-variables...");
+
+	for_all_symbols(sym) {
+		sym->constraints = pexpr_list_init();
+		sym_create_fexpr(sym, data);
+	}
+
+	printd("done.\n");
+}
+
+/*
+ * create various constants
+ */
+void create_constants(struct cfdata *data)
+{
+	printd("Creating constants...");
+
+	/* create TRUE and FALSE constants */
+	data->constants->const_false = fexpr_create(data->sat_variable_nr++, FE_FALSE, "False");
+	// const_false = fexpr_create(sat_variable_nr++, FE_FALSE, "False");
+	fexpr_add_to_satmap(data->constants->const_false, data);
+
+	data->constants->const_true = fexpr_create(data->sat_variable_nr++, FE_TRUE, "True");
+	fexpr_add_to_satmap(data->constants->const_true, data);
+
+	/* add fexpr of constants to tristate constants */
+	symbol_yes.fexpr_y = data->constants->const_true;
+	symbol_yes.fexpr_m = data->constants->const_false;
+
+	symbol_mod.fexpr_y = data->constants->const_false;
+	symbol_mod.fexpr_m = data->constants->const_true;
+
+	symbol_no.fexpr_y = data->constants->const_false;
+	symbol_no.fexpr_m = data->constants->const_false;
+
+	/* create symbols yes/mod/no as fexpr */
+	data->constants->symbol_yes_fexpr = fexpr_create(0, FE_SYMBOL, "y");
+	data->constants->symbol_yes_fexpr->sym = &symbol_yes;
+	data->constants->symbol_yes_fexpr->tri = yes;
+
+	data->constants->symbol_mod_fexpr = fexpr_create(0, FE_SYMBOL, "m");
+	data->constants->symbol_mod_fexpr->sym = &symbol_mod;
+	data->constants->symbol_mod_fexpr->tri = mod;
+
+	data->constants->symbol_no_fexpr = fexpr_create(0, FE_SYMBOL, "n");
+	data->constants->symbol_no_fexpr->sym = &symbol_no;
+	data->constants->symbol_no_fexpr->tri = no;
+
+	printd("done.\n");
+}
+
+/*
+ * create a temporary SAT-variable
+ */
+struct fexpr *create_tmpsatvar(struct cfdata *data)
+{
+	char *name = get_tmp_var_as_char(data->tmp_variable_nr);
+	struct fexpr *t = fexpr_create(data->sat_variable_nr++, FE_TMPSATVAR, name);
+
+	++data->tmp_variable_nr;
+	fexpr_add_to_satmap(t, data);
+
+	free(name);
+	return t;
+}
+
+/*
+ * return a temporary SAT variable as string
+ */
+char *get_tmp_var_as_char(int i)
+{
+	char *val = malloc(sizeof(char) * 18);
+
+	snprintf(val, 18, "T_%d", i);
+	return val;
+}
+
+/*
+ * return a tristate value as a char *
+ */
+char *tristate_get_char(tristate val)
+{
+	switch (val) {
+	case yes:
+		return "yes";
+	case mod:
+		return "mod";
+	case no:
+		return "no";
+	default:
+		return "";
+	}
+}
+
+/*
+ *check whether an expr can evaluate to mod
+ */
+bool expr_can_evaluate_to_mod(struct expr *e)
+{
+	if (!e)
+		return false;
+
+	switch (e->type) {
+	case E_SYMBOL:
+		return e->left.sym == &symbol_mod || e->left.sym->type == S_TRISTATE ? true : false;
+	case E_AND:
+	case E_OR:
+		return expr_can_evaluate_to_mod(e->left.expr) ||
+		       expr_can_evaluate_to_mod(e->right.expr);
+	case E_NOT:
+		return expr_can_evaluate_to_mod(e->left.expr);
+	default:
+		return false;
+	}
+}
+
+/*
+ * check whether an expr is a non-Boolean constant
+ */
+bool expr_is_nonbool_constant(struct expr *e)
+{
+	if (e->type != E_SYMBOL)
+		return false;
+	if (e->left.sym->type != S_UNKNOWN)
+		return false;
+
+	if (e->left.sym->flags & SYMBOL_CONST)
+		return true;
+
+	return string_is_number(e->left.sym->name) || string_is_hex(e->left.sym->name);
+}
+
+/*
+ * check whether a symbol is a non-Boolean constant
+ */
+bool sym_is_nonbool_constant(struct symbol *sym)
+{
+	if (sym->type != S_UNKNOWN)
+		return false;
+
+	if (sym->flags & SYMBOL_CONST)
+		return true;
+
+	return string_is_number(sym->name) || string_is_hex(sym->name);
+}
+
+/*
+ * print an expr
+ */
+static void print_expr_util(struct expr *e, int prevtoken)
+{
+	if (!e)
+		return;
+
+	switch (e->type) {
+	case E_SYMBOL:
+		if (sym_get_name(e->left.sym) != NULL)
+			printf("%s", sym_get_name(e->left.sym));
+		else
+			printf("left was null\n");
+		break;
+	case E_NOT:
+		printf("!");
+		print_expr_util(e->left.expr, E_NOT);
+		break;
+	case E_AND:
+		if (prevtoken != E_AND && prevtoken != 0)
+			printf("(");
+		print_expr_util(e->left.expr, E_AND);
+		printf(" && ");
+		print_expr_util(e->right.expr, E_AND);
+		if (prevtoken != E_AND && prevtoken != 0)
+			printf(")");
+		break;
+	case E_OR:
+		if (prevtoken != E_OR && prevtoken != 0)
+			printf("(");
+		print_expr_util(e->left.expr, E_OR);
+		printf(" || ");
+		print_expr_util(e->right.expr, E_OR);
+		if (prevtoken != E_OR && prevtoken != 0)
+			printf(")");
+		break;
+	case E_EQUAL:
+	case E_UNEQUAL:
+		if (e->left.sym->name)
+			printf("%s", e->left.sym->name);
+		else
+			printf("left was null\n");
+		printf("%s", e->type == E_EQUAL ? "=" : "!=");
+		printf("%s", e->right.sym->name);
+		break;
+	case E_LEQ:
+	case E_LTH:
+		if (e->left.sym->name)
+			printf("%s", e->left.sym->name);
+		else
+			printf("left was null\n");
+		printf("%s", e->type == E_LEQ ? "<=" : "<");
+		printf("%s", e->right.sym->name);
+		break;
+	case E_GEQ:
+	case E_GTH:
+		if (e->left.sym->name)
+			printf("%s", e->left.sym->name);
+		else
+			printf("left was null\n");
+		printf("%s", e->type == E_GEQ ? ">=" : ">");
+		printf("%s", e->right.sym->name);
+		break;
+	case E_RANGE:
+		printf("[");
+		printf("%s", e->left.sym->name);
+		printf(" ");
+		printf("%s", e->right.sym->name);
+		printf("]");
+		break;
+	default:
+		break;
+	}
+}
+void print_expr(char *tag, struct expr *e, int prevtoken)
+{
+	printf("%s ", tag);
+	print_expr_util(e, prevtoken);
+	printf("\n");
+}
+
+/*
+ * check, if the symbol is a tristate-constant
+ */
+bool sym_is_tristate_constant(struct symbol *sym)
+{
+	return sym == &symbol_yes || sym == &symbol_mod || sym == &symbol_no;
+}
+
+/*
+ * check, if a symbol is of type boolean or tristate
+ */
+bool sym_is_boolean(struct symbol *sym)
+{
+	return sym->type == S_BOOLEAN || sym->type == S_TRISTATE;
+}
+
+/*
+ * check, if a symbol is a boolean/tristate or a tristate constant
+ */
+bool sym_is_bool_or_triconst(struct symbol *sym)
+{
+	return sym_is_tristate_constant(sym) || sym_is_boolean(sym);
+}
+
+/*
+ * check, if a symbol is of type int, hex, or string
+ */
+bool sym_is_nonboolean(struct symbol *sym)
+{
+	return sym->type == S_INT || sym->type == S_HEX || sym->type == S_STRING;
+}
+
+/*
+ * check, if a symbol has a prompt
+ */
+bool sym_has_prompt(struct symbol *sym)
+{
+	struct property *prop;
+
+	for_all_prompts(sym, prop)
+		return true;
+
+	return false;
+}
+
+/*
+ * return the prompt of the symbol if there is one, NULL otherwise
+ */
+struct property *sym_get_prompt(struct symbol *sym)
+{
+	struct property *prop;
+
+	for_all_prompts(sym, prop)
+		return prop;
+
+	return NULL;
+}
+
+/*
+ * return the condition for the property, NULL if there is none. To be pexpr_put
+ * by caller.
+ */
+struct pexpr *prop_get_condition(struct property *prop, struct cfdata *data)
+{
+	if (prop == NULL)
+		return NULL;
+
+	/* if there is no condition, return True */
+	if (!prop->visible.expr)
+		return pexf(data->constants->const_true);
+
+	return expr_calculate_pexpr_both(prop->visible.expr, data);
+}
+
+/*
+ * return the default property, NULL if none exists or can be satisfied
+ */
+struct property *sym_get_default_prop(struct symbol *sym)
+{
+	struct property *prop;
+
+	for_all_defaults(sym, prop) {
+		prop->visible.tri = expr_calc_value(prop->visible.expr);
+		if (prop->visible.tri != no)
+			return prop;
+	}
+	return NULL;
+}
+
+/*
+ * check whether a non-boolean symbol has a value set
+ */
+bool sym_nonbool_has_value_set(struct symbol *sym)
+{
+	/*
+	 * The built constraints make the following constraints:
+	 *
+	 * visible -> not 'n'
+	 * sym->dir_dep not fulfilled -> 'n'
+	 * invisible -> (no default's condition is fulfilled <-> 'n')
+	 */
+	struct property *prompt;
+	struct property *p;
+
+	if (!sym_is_nonboolean(sym))
+		return false;
+
+	/* cannot have a value with unmet dependencies */
+	if (sym->dir_dep.expr && sym->dir_dep.tri == no)
+		return false;
+
+	/* visible prompt => value set */
+	prompt = sym_get_prompt(sym);
+	if (prompt != NULL && prompt->visible.tri != no)
+		return true;
+
+	/* invisible prompt => must get value from default value */
+	p = sym_get_default_prop(sym);
+	return p != NULL;
+}
+
+/*
+ * return pointer to the name of the symbol or the current prompt-text, if it
+ * is a choice symbol
+ */
+const char *sym_get_name(struct symbol *sym)
+{
+	if (sym_is_choice(sym)) {
+		struct property *prompt = sym_get_prompt(sym);
+
+		if (prompt == NULL)
+			return "";
+
+		return prompt->text;
+	} else {
+		return sym->name;
+	}
+}
+
+/*
+ * check whether symbol is to be changed
+ */
+bool sym_is_sdv(struct sdv_list *list, struct symbol *sym)
+{
+	struct sdv_node *node;
+
+	sdv_list_for_each(node, list)
+		if (sym == node->elem->sym)
+			return true;
+
+	return false;
+}
+
+/*
+ * print a symbol's name
+ */
+void print_sym_name(struct symbol *sym)
+{
+	printf("Symbol: ");
+	if (sym_is_choice(sym)) {
+		struct property *prompt = sym_get_prompt(sym);
+
+		printf("(Choice) %s", prompt->text);
+	} else  {
+		printf("%s", sym->name);
+	}
+	printf("\n");
+}
+
+/*
+ * print all constraints for a symbol
+ */
+void print_sym_constraint(struct symbol *sym)
+{
+	struct pexpr_node *node;
+
+	pexpr_list_for_each(node, sym->constraints)
+		pexpr_print("::", node->elem, -1);
+}
+
+/*
+ * print a default map
+ */
+void print_default_map(struct defm_list *map)
+{
+	struct default_map *entry;
+	struct defm_node *node;
+
+	defm_list_for_each(node, map) {
+		struct gstr s = str_new();
+
+		entry = node->elem;
+
+		str_append(&s, "\t");
+		str_append(&s, str_get(&entry->val->name));
+		str_append(&s, " ->");
+		pexpr_print(strdup(str_get(&s)), entry->e, -1);
+		str_free(&s);
+	}
+}
+
+/*
+ * check whether a string is a number
+ */
+bool string_is_number(char *s)
+{
+	int len = strlen(s);
+	int i = 0;
+
+	while (i < len) {
+		if (!isdigit(s[i]))
+			return false;
+		i++;
+	}
+
+	return true;
+}
+
+/*
+ * check whether a string is a hexadecimal number
+ */
+bool string_is_hex(char *s)
+{
+	int len = strlen(s);
+	int i = 2;
+
+	if (len >= 3 && s[0] == '0' && s[1] == 'x') {
+		while (i < len) {
+			if (!isxdigit(s[i]))
+				return false;
+			i++;
+		}
+		return true;
+	} else {
+		return false;
+	}
+}
+
+/*
+ * initialize PicoSAT
+ */
+PicoSAT *initialize_picosat(void)
+{
+	PicoSAT *pico;
+
+	printd("\nInitializing PicoSAT...");
+	pico = picosat_init();
+	picosat_enable_trace_generation(pico);
+	printd("done.\n");
+
+	return pico;
+}
+
+/*
+ * construct the CNF-clauses from the constraints
+ */
+void construct_cnf_clauses(PicoSAT *p, struct cfdata *data)
+{
+	struct symbol *sym;
+
+	pico = p;
+
+	/* adding unit-clauses for constants */
+	sat_add_clause(2, pico, -(data->constants->const_false->satval));
+	sat_add_clause(2, pico, data->constants->const_true->satval);
+
+	for_all_symbols(sym) {
+		struct pexpr_node *node;
+
+		if (sym->type == S_UNKNOWN)
+			continue;
+
+		pexpr_list_for_each(node, sym->constraints) {
+			if (pexpr_is_cnf(node->elem)) {
+				unfold_cnf_clause(node->elem);
+				picosat_add(pico, 0);
+			} else {
+				build_cnf_tseytin(node->elem, data);
+			}
+
+		}
+	}
+}
+
+/*
+ * helper function to add an expression to a CNF-clause
+ */
+static void unfold_cnf_clause(struct pexpr *e)
+{
+	switch (e->type) {
+	case PE_SYMBOL:
+		picosat_add(pico, e->left.fexpr->satval);
+		break;
+	case PE_OR:
+		unfold_cnf_clause(e->left.pexpr);
+		unfold_cnf_clause(e->right.pexpr);
+		break;
+	case PE_NOT:
+		picosat_add(pico, -(e->left.pexpr->left.fexpr->satval));
+		break;
+	default:
+		perror("Not in CNF, FE_EQUALS.");
+	}
+}
+
+/*
+ * build CNF-clauses for a pexpr not in CNF
+ */
+static void build_cnf_tseytin(struct pexpr *e, struct cfdata *data)
+{
+	switch (e->type) {
+	case PE_AND:
+		build_cnf_tseytin_top_and(e, data);
+		break;
+	case PE_OR:
+		build_cnf_tseytin_top_or(e, data);
+		break;
+	default:
+		perror("Expression not a propositional logic formula. root.");
+	}
+}
+
+/*
+ * split up a pexpr of type AND as both sides must be satisfied
+ */
+static void build_cnf_tseytin_top_and(struct pexpr *e, struct cfdata *data)
+{
+	if (pexpr_is_cnf(e->left.pexpr))
+		unfold_cnf_clause(e->left.pexpr);
+	else
+		build_cnf_tseytin(e->left.pexpr, data);
+
+	if (pexpr_is_cnf(e->right.pexpr))
+		unfold_cnf_clause(e->right.pexpr);
+	else
+		build_cnf_tseytin(e->right.pexpr, data);
+
+}
+
+static void build_cnf_tseytin_top_or(struct pexpr *e, struct cfdata *data)
+{
+	struct fexpr *t1 = NULL, *t2 = NULL;
+	int a, b;
+
+	/* set left side */
+	if (pexpr_is_symbol(e->left.pexpr)) {
+		a = pexpr_satval(e->left.pexpr);
+	} else {
+		t1 = create_tmpsatvar(data);
+		a = t1->satval;
+	}
+
+	/* set right side */
+	if (pexpr_is_symbol(e->right.pexpr)) {
+		b = pexpr_satval(e->right.pexpr);
+	} else {
+		t2 = create_tmpsatvar(data);
+		b = t2->satval;
+	}
+
+	/* A v B */
+	sat_add_clause(3, pico, a, b);
+
+	/* traverse down the tree to build more constraints if needed */
+	if (!pexpr_is_symbol(e->left.pexpr)) {
+		if (t1 == NULL)
+			perror("t1 is NULL.");
+
+		build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
+	}
+
+	if (!pexpr_is_symbol(e->right.pexpr)) {
+		if (t2 == NULL)
+			perror("t2 is NULL.");
+
+		build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
+	}
+}
+
+/*
+ * build the sub-expressions
+ */
+static void build_cnf_tseytin_tmp(struct pexpr *e, struct fexpr *t, struct cfdata *data)
+{
+	switch (e->type) {
+	case PE_AND:
+		build_cnf_tseytin_and(e, t, data);
+		break;
+	case PE_OR:
+		build_cnf_tseytin_or(e, t, data);
+		break;
+	default:
+		perror("Expression not a propositional logic formula. root.");
+	}
+}
+
+/*
+ * build the Tseytin sub-expressions for a pexpr of type AND
+ */
+static void build_cnf_tseytin_and(struct pexpr *e, struct fexpr *t, struct cfdata *data)
+{
+	struct fexpr *t1 = NULL, *t2 = NULL;
+	int a, b, c;
+
+	assert(t != NULL);
+
+	/* set left side */
+	if (pexpr_is_symbol(e->left.pexpr)) {
+		a = pexpr_satval(e->left.pexpr);
+	} else {
+		t1 = create_tmpsatvar(data);
+		a = t1->satval;
+	}
+
+	/* set right side */
+	if (pexpr_is_symbol(e->right.pexpr)) {
+		b = pexpr_satval(e->right.pexpr);
+	} else {
+		t2 = create_tmpsatvar(data);
+		b = t2->satval;
+	}
+
+	c = t->satval;
+
+	/* -A v -B v C */
+	sat_add_clause(4, pico, -a, -b, c);
+	/* A v -C */
+	sat_add_clause(3, pico, a, -c);
+	/* B v -C */
+	sat_add_clause(3, pico, b, -c);
+
+	/* traverse down the tree to build more constraints if needed */
+	if (!pexpr_is_symbol(e->left.pexpr)) {
+		if (t1 == NULL)
+			perror("t1 is NULL.");
+
+		build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
+	}
+	if (!pexpr_is_symbol(e->right.pexpr)) {
+		if (t2 == NULL)
+			perror("t2 is NULL.");
+
+		build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
+	}
+}
+
+/*
+ * build the Tseytin sub-expressions for a pexpr of type
+ */
+static void build_cnf_tseytin_or(struct pexpr *e, struct fexpr *t, struct cfdata *data)
+{
+	struct fexpr *t1 = NULL, *t2 = NULL;
+	int a, b, c;
+
+	assert(t != NULL);
+
+	/* set left side */
+	if (pexpr_is_symbol(e->left.pexpr)) {
+		a = pexpr_satval(e->left.pexpr);
+	} else {
+		t1 = create_tmpsatvar(data);
+		a = t1->satval;
+	}
+
+	/* set right side */
+	if (pexpr_is_symbol(e->right.pexpr)) {
+		b = pexpr_satval(e->right.pexpr);
+	} else {
+		t2 = create_tmpsatvar(data);
+		b = t2->satval;
+	}
+
+	c = t->satval;
+
+	/* A v B v -C */
+	sat_add_clause(4, pico, a, b, -c);
+	/* -A v C */;
+	sat_add_clause(3, pico, -a, c);
+	/* -B v C */
+	sat_add_clause(3, pico, -b, c);
+
+	/* traverse down the tree to build more constraints if needed */
+	if (!pexpr_is_symbol(e->left.pexpr)) {
+		if (t1 == NULL)
+			perror("t1 is NULL.");
+
+		build_cnf_tseytin_tmp(e->left.pexpr, t1, data);
+	}
+	if (!pexpr_is_symbol(e->right.pexpr)) {
+		if (t2 == NULL)
+			perror("t2 is NULL.");
+
+		build_cnf_tseytin_tmp(e->right.pexpr, t2, data);
+	}
+}
+
+/*
+ * add a clause to PicoSAT
+ * First argument must be the SAT solver
+ */
+void sat_add_clause(int num, ...)
+{
+	va_list valist;
+	int lit;
+	PicoSAT *pico;
+
+	if (num <= 1)
+		return;
+
+	va_start(valist, num);
+
+	pico = va_arg(valist, PicoSAT *);
+
+	/* access all the arguments assigned to valist */
+	for (int i = 1; i < num; i++) {
+		lit = va_arg(valist, int);
+		picosat_add(pico, lit);
+	}
+	picosat_add(pico, 0);
+
+	va_end(valist);
+}
+
+/*
+ * return the SAT-variable for a pexpr that is a symbol
+ */
+static int pexpr_satval(struct pexpr *e)
+{
+	if (!pexpr_is_symbol(e)) {
+		perror("pexpr is not a symbol.");
+		return -1;
+	}
+
+	switch (e->type) {
+	case PE_SYMBOL:
+		return e->left.fexpr->satval;
+	case PE_NOT:
+		return -(e->left.pexpr->left.fexpr->satval);
+	default:
+		perror("Not a symbol.");
+	}
+
+	return -1;
+}
+
+/*
+ * start PicoSAT
+ */
+void picosat_solve(PicoSAT *pico, struct cfdata *data)
+{
+	clock_t start, end;
+	double time;
+	int res;
+
+	printd("Solving SAT-problem...");
+
+	start = clock();
+	res = picosat_sat(pico, -1);
+	end = clock();
+
+	time = ((double) (end - start)) / CLOCKS_PER_SEC;
+	printd("done. (%.6f secs.)\n\n", time);
+
+	if (res == PICOSAT_SATISFIABLE) {
+		printd("===> PROBLEM IS SATISFIABLE <===\n");
+
+	} else if (res == PICOSAT_UNSATISFIABLE) {
+		struct fexpr *e;
+		int lit;
+		const int *i;
+
+		printd("===> PROBLEM IS UNSATISFIABLE <===\n");
+
+		/* print unsat core */
+		printd("\nPrinting unsatisfiable core:\n");
+
+		i = picosat_failed_assumptions(pico);
+		lit = abs(*i++);
+
+		while (lit != 0) {
+			e = data->satmap[lit];
+
+			printd("(%d) %s <%d>\n", lit, str_get(&e->name), e->assumption);
+			lit = abs(*i++);
+		}
+	} else {
+		printd("Unknown if satisfiable.\n");
+	}
+}
+
+/*
+ * add assumption for a symbol to the SAT-solver
+ */
+void sym_add_assumption(PicoSAT *pico, struct symbol *sym)
+{
+	if (sym_is_boolean(sym)) {
+		int tri_val = sym_get_tristate_value(sym);
+
+		sym_add_assumption_tri(pico, sym, tri_val);
+		return;
+	}
+
+	if (sym_is_nonboolean(sym)) {
+		struct fexpr *e = sym->nb_vals->head->elem;
+		struct fexpr_node *node;
+
+		const char *string_val = sym_get_string_value(sym);
+
+		if (sym->type == S_STRING && !strcmp(string_val, ""))
+			return;
+
+		/* symbol does not have a value */
+		if (!sym_nonbool_has_value_set(sym)) {
+			/* set value for sym=n */
+			picosat_assume(pico, e->satval);
+			e->assumption = true;
+
+			for (node = sym->nb_vals->head->next; node != NULL; node = node->next) {
+				picosat_assume(pico, -(node->elem->satval));
+				node->elem->assumption = false;
+			}
+
+			return;
+		}
+
+		/* symbol does have a value set */
+
+		/* set value for sym=n */
+		picosat_assume(pico, -(e->satval));
+		e->assumption = false;
+
+		/* set value for all other fexpr */
+		fexpr_list_for_each(node, sym->nb_vals) {
+			if (node->prev == NULL)
+				continue;
+
+			if (strcmp(str_get(&node->elem->nb_val), string_val) == 0) {
+				picosat_assume(pico, node->elem->satval);
+				node->elem->assumption = true;
+			} else {
+				picosat_assume(pico, -(node->elem->satval));
+				node->elem->assumption = false;
+			}
+		}
+	}
+}
+
+/*
+ * add assumption for a boolean symbol to the SAT-solver
+ */
+void sym_add_assumption_tri(PicoSAT *pico, struct symbol *sym, tristate tri_val)
+{
+	if (sym->type == S_BOOLEAN) {
+		int a = sym->fexpr_y->satval;
+
+		switch (tri_val) {
+		case no:
+			picosat_assume(pico, -a);
+			sym->fexpr_y->assumption = false;
+			break;
+		case mod:
+			perror("Should not happen. Boolean symbol is set to mod.\n");
+			break;
+		case yes:
+
+			picosat_assume(pico, a);
+			sym->fexpr_y->assumption = true;
+			break;
+		}
+	}
+	if (sym->type == S_TRISTATE) {
+		int a = sym->fexpr_y->satval;
+		int a_m = sym->fexpr_m->satval;
+
+		switch (tri_val) {
+		case no:
+			picosat_assume(pico, -a);
+			picosat_assume(pico, -a_m);
+			sym->fexpr_y->assumption = false;
+			sym->fexpr_m->assumption = false;
+			break;
+		case mod:
+			picosat_assume(pico, -a);
+			picosat_assume(pico, a_m);
+			sym->fexpr_y->assumption = false;
+			sym->fexpr_m->assumption = true;
+			break;
+		case yes:
+			picosat_assume(pico, a);
+			picosat_assume(pico, -a_m);
+			sym->fexpr_y->assumption = true;
+			sym->fexpr_m->assumption = false;
+			break;
+		}
+	}
+}
+
+/*
+ * add assumptions for the symbols to be changed to the SAT solver
+ */
+void sym_add_assumption_sdv(PicoSAT *pico, struct sdv_list *list)
+{
+	struct symbol_dvalue *sdv;
+	struct sdv_node *node;
+	int lit_y, lit_m;
+
+	sdv_list_for_each(node, list) {
+		sdv = node->elem;
+		lit_y = sdv->sym->fexpr_y->satval;
+
+		if (sdv->sym->type == S_BOOLEAN) {
+			switch (sdv->tri) {
+			case yes:
+				picosat_assume(pico, lit_y);
+				break;
+			case no:
+				picosat_assume(pico, -lit_y);
+				break;
+			case mod:
+				perror("Should not happen.\n");
+			}
+		} else if (sdv->sym->type == S_TRISTATE) {
+			lit_m = sdv->sym->fexpr_m->satval;
+
+			switch (sdv->tri) {
+			case yes:
+				picosat_assume(pico, lit_y);
+				picosat_assume(pico, -lit_m);
+				break;
+			case mod:
+				picosat_assume(pico, -lit_y);
+				picosat_assume(pico, lit_m);
+				break;
+			case no:
+				picosat_assume(pico, -lit_y);
+				picosat_assume(pico, -lit_m);
+			}
+		}
+	}
+}
diff --git a/scripts/kconfig/cf_utils.h b/scripts/kconfig/cf_utils.h
new file mode 100644
index 000000000000..b71c8731a8ff
--- /dev/null
+++ b/scripts/kconfig/cf_utils.h
@@ -0,0 +1,115 @@ 
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
+ */
+
+#ifndef CF_UTILS_H
+#define CF_UTILS_H
+
+#include "expr.h"
+#include "cf_defs.h"
+#include "picosat.h"
+
+/* parse Kconfig-file and read .config */
+void init_config(const char *Kconfig_file);
+
+/* initialize satmap and cnf_clauses */
+void init_data(struct cfdata *data);
+
+/* assign SAT-variables to all fexpr and create the sat_map */
+void create_sat_variables(struct cfdata *data);
+
+/* create True/False constants */
+void create_constants(struct cfdata *data);
+
+/* create a temporary SAT-variable */
+struct fexpr *create_tmpsatvar(struct cfdata *data);
+
+/* return a temporary SAT variable as string */
+char *get_tmp_var_as_char(int i);
+
+/* return a tristate value as a char * */
+char *tristate_get_char(tristate val);
+
+/* check whether an expr can evaluate to mod */
+bool expr_can_evaluate_to_mod(struct expr *e);
+
+/* check whether an expr is a non-Boolean constant */
+bool expr_is_nonbool_constant(struct expr *e);
+
+/* check whether a symbol is a non-Boolean constant */
+bool sym_is_nonbool_constant(struct symbol *sym);
+
+/* print an expr */
+void print_expr(char *tag, struct expr *e, int prevtoken);
+
+/* check, if the symbol is a tristate-constant */
+bool sym_is_tristate_constant(struct symbol *sym);
+
+/* check, if a symbol is of type boolean or tristate */
+bool sym_is_boolean(struct symbol *sym);
+
+/* check, if a symbol is a boolean/tristate or a tristate constant */
+bool sym_is_bool_or_triconst(struct symbol *sym);
+
+/* check, if a symbol is of type int, hex, or string */
+bool sym_is_nonboolean(struct symbol *sym);
+
+/* check, if a symbol has a prompt */
+bool sym_has_prompt(struct symbol *sym);
+
+/* return the prompt of the symbol, if there is one */
+struct property *sym_get_prompt(struct symbol *sym);
+
+/* return the condition for the property, True if there is none */
+struct pexpr *prop_get_condition(struct property *prop, struct cfdata *data);
+
+/* return the default property, NULL if none exists or can be satisfied */
+struct property *sym_get_default_prop(struct symbol *sym);
+
+/* check whether a non-boolean symbol has a value set */
+bool sym_nonbool_has_value_set(struct symbol *sym);
+
+/* return the name of the symbol */
+const char *sym_get_name(struct symbol *sym);
+
+/* check whether symbol is to be changed */
+bool sym_is_sdv(struct sdv_list *list, struct symbol *sym);
+
+/* print a symbol's name */
+void print_sym_name(struct symbol *sym);
+
+/* print all constraints for a symbol */
+void print_sym_constraint(struct symbol *sym);
+
+/* print a default map */
+void print_default_map(struct defm_list *map);
+
+/* check whether a string is a number */
+bool string_is_number(char *s);
+
+/* check whether a string is a hexadecimal number */
+bool string_is_hex(char *s);
+
+/* initialize PicoSAT */
+PicoSAT *initialize_picosat(void);
+
+/* construct the CNF-clauses from the constraints */
+void construct_cnf_clauses(PicoSAT *pico, struct cfdata *data);
+
+/* add a clause to PicoSAT */
+void sat_add_clause(int num, ...);
+
+/* start PicoSAT */
+void picosat_solve(PicoSAT *pico, struct cfdata *data);
+
+/* add assumption for a symbol to the SAT-solver */
+void sym_add_assumption(PicoSAT *pico, struct symbol *sym);
+
+/* add assumption for a boolean symbol to the SAT-solver */
+void sym_add_assumption_tri(PicoSAT *pico, struct symbol *sym, tristate tri_val);
+
+/* add assumptions for the symbols to be changed to the SAT solver */
+void sym_add_assumption_sdv(PicoSAT *pico, struct sdv_list *list);
+
+#endif